Section 10 commutativity points: lift comparisons

Comparison lemmas lifting the ordered shared-line point product to the mixed line family, used in the lift direction of the Section 10 point-commutativity argument: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/CommutativityPoints/BridgeTheorems/LiftBridges.lean in the port of planning/c6b-plan.md (milestone M1, section "Port conventions"). The strategy is a symmetric one, strategy : SymStrat params 𝔓 K; the point answers are placed by strategy.state.L, the line answers by strategy.state.R, and the distance relations are those of the vector state of strategy.state.

Each comparison multiplies a known approximation on the left by a placed submeasurement (Preliminaries.cabApproxDelta_raw), whose hypothesis ∑ b, star C_b * C_b ≤ 1 the vendored file proves with subMeas_sum_adjoint_mul_le_one on the lifted, joint submeasurement. Here that lemma is about a local submeasurement in 𝔓, and the joint bound is transported along the placement: liftLeft_sum_adjoint_mul_le_one and liftRight_sum_adjoint_mul_le_one (new; also used by BridgeTheorems/DropBridges.lean), so that no positivity of K →L[ℂ] K is reproved.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/commutativity-points.tex
• blueprint/src/chapter/ch08_commutativity.tex

In this repository: lem:co-commutativity-points in blueprint/src/content/08_downstream.tex.

theorem MIPRE.LIDT.Co.CommutativityPoints.liftLeft_sum_adjoint_mul_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (A : SubMeas Outcome 𝔓) : ∑ a : Outcome, star ((SubMeas.liftLeft S A).outcome a) * (SubMeas.liftLeft S A).outcome a ≤ 1

The bound of subMeas_sum_adjoint_mul_le_one, for a submeasurement lifted to the first factor: the sum is the left placement of the local one.

theorem MIPRE.LIDT.Co.CommutativityPoints.liftRight_sum_adjoint_mul_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (A : SubMeas Outcome 𝔓) : ∑ a : Outcome, star ((SubMeas.liftRight S A).outcome a) * (SubMeas.liftRight S A).outcome a ≤ 1

The bound of subMeas_sum_adjoint_mul_le_one, for a submeasurement lifted to the second factor: the sum is the right placement of the local one.

theorem MIPRE.LIDT.Co.CommutativityPoints.orderedLiftToMixedLine {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (eps delta gamma : ℝ) (hgood : strategy.IsGood eps delta gamma) : strategy.state.SDDOpRel (MIPStarRE.LDT.CommutativityPoints.pointPairSharedDiagonalLineDistribution params) (pointMeasurementProductAlongSharedLine params strategy) (pointDiagonalLineMixedProductLeft params strategy).toIdxOpFamily (MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineApproxError params gamma)

Lift the ordered shared-line point product to the mixed line family.

theorem MIPRE.LIDT.Co.CommutativityPoints.orderedLiftToLineProduct {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (eps delta gamma : ℝ) (hgood : strategy.IsGood eps delta gamma) : strategy.state.SDDOpRel (MIPStarRE.LDT.CommutativityPoints.pointPairSharedDiagonalLineDistribution params) (pointDiagonalLineMixedProductLeft params strategy).toIdxOpFamily (diagonalLineProductOrdered params strategy) (MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineApproxError params gamma)

Lift the mixed line family to the ordered shared-line line product.