Section 10 — Definitions

Auxiliary definitions for the commutativity-at-points argument from Section 10 of the low individual degree paper: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/CommutativityPoints/Defs.lean in the port of planning/c6b-plan.md (milestone M1, section "Port conventions"). This file packages the point/line bridge families used by commutativityPoints, over a symmetric strategy strategy : SymStrat params 𝔓 K: local operators live in the C*-algebra 𝔓, joint ones in K →L[ℂ] K, and the vendored placements leftTensor (ι₂ := ι), rightTensor (ι₁ := ι) are the model's strategy.state.L, strategy.state.R.

The products of two submeasurements, orderedProductOpFamily and reversedProductOpFamily, are generic over the ordered ⋆-ring R of Co/Basic/SubMeasurementCore.lean (the vendored Op ι). The bipartite bridge tensorProductSubMeas needs both placements, so it takes the symmetric model S as an explicit argument (the vendored one is fixed by its carrier ι × ι).

The classical half of the vendored file (the question and outcome types, the Fintype instance on diagonal lines, the sampling maps and distributions, and the error constants) is not ported: this file imports the vendored file and names those declarations through an explicit open MIPStarRE.LDT.CommutativityPoints (…) list.

Not ported

• PointPairOutcome: classical, imported.
• PointDiagonalLineQuestion: classical, imported.
• PointPairDiagonalLineQuestion: classical, imported.
• sampledPointFromDiagonalQuestion: classical, imported.
• sampledPointPairFromSharedDiagonalQuestion: classical, imported.
• pointWithDiagonalLineDistribution: classical, imported.
• pointWithDiagonalLineDistribution_isProbability: classical, imported.
• pointWithDiagonalLineDistribution_toPMF: classical, imported.
• sharedDiagonalLineQuestionOfPointPair: classical, imported.
• pointPairSharedDiagonalLineDistribution: classical, imported.
• pointPairSharedDiagonalLineDistribution_isProbability: classical, imported.
• pointPairSharedDiagonalLineDistribution_toPMF: classical, imported.
• restrictedDiagonalLinesConsistencyError: classical, imported.
• pointDiagonalLineApproxError: classical, imported.
• commutativityPointsError: classical, imported.

The anonymous Fintype (DiagonalLine params) instance of the vendored file is classical too, and in force here through the import.

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.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.orderedProductOpFamily {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α R) (B : SubMeas β R) : OpFamily (α × β) R

Ordered product of two submeasurements viewed as a raw operator family.

Equations

• MIPRE.LIDT.Co.CommutativityPoints.orderedProductOpFamily A B = { outcome := fun (x : α × β) => match x with | (a, b) => A.outcome a * B.outcome b, total := A.total * B.total }

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.reversedProductOpFamily {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α R) (B : SubMeas β R) : OpFamily (α × β) R

Reversed product of two submeasurements viewed as a raw operator family.

Equations

• MIPRE.LIDT.Co.CommutativityPoints.reversedProductOpFamily A B = { outcome := fun (x : α × β) => match x with | (a, b) => B.outcome b * A.outcome a, total := B.total * A.total }

theorem MIPRE.LIDT.Co.CommutativityPoints.tensorProductSubMeas_sum_outcome {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (A : SubMeas α 𝔓) (B : SubMeas β 𝔓) : ∑ ab : α × β, S.L (A.outcome ab.1) * S.R (B.outcome ab.2) = S.L A.total * S.R B.total

The outcome effects of tensorProductSubMeas sum to its total effect.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.tensorProductSubMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (A : SubMeas α 𝔓) (B : SubMeas β 𝔓) : SubMeas (α × β) (K →L[ℂ] K)

Tensor-product bridge A_a ⊗ B_b, placed by the symmetric model S as S.L A_a * S.R B_b.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.pointMeasurementProductLeft {𝔓 : 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) : IdxOpFamily (MIPStarRE.LDT.GlobalVariance.PointPairQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The ordered point product (A^u_a A^v_b) ⊗ I, placed by strategy.state.L.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.pointMeasurementProductRight {𝔓 : 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) : IdxOpFamily (MIPStarRE.LDT.GlobalVariance.PointPairQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The reversed point product (A^v_b A^u_a) ⊗ I, placed by strategy.state.L.

Equations

• One or more equations did not get rendered due to their size.

def MIPRE.LIDT.Co.CommutativityPoints.sampledPointMeasurement {𝔓 : 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) : IdxSubMeas (MIPStarRE.LDT.CommutativityPoints.PointDiagonalLineQuestion params) (MIPStarRE.LDT.Fq params) 𝔓

The point measurement, reindexed by a sampled diagonal line and a parameter on it.

Equations

• MIPRE.LIDT.Co.CommutativityPoints.sampledPointMeasurement params strategy q = (strategy.pointMeasurement (MIPStarRE.LDT.CommutativityPoints.sampledPointFromDiagonalQuestion params q)).toSubMeas

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.sampledDiagonalLineEvaluation {𝔓 : 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) : IdxSubMeas (MIPStarRE.LDT.CommutativityPoints.PointDiagonalLineQuestion params) (MIPStarRE.LDT.Fq params) 𝔓

Evaluate the diagonal-line measurement at the sampled parameter.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.pointMeasurementProductAlongSharedLine {𝔓 : 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) : IdxOpFamily (MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The ordered point product (A^u_a A^v_b) ⊗ I, indexed by a shared sampled line.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.pointMeasurementProductAlongSharedLineReversed {𝔓 : 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) : IdxOpFamily (MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The reversed point product (A^v_b A^u_a) ⊗ I, indexed by a shared sampled line.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.pointDiagonalLineMixedProductLeft {𝔓 : 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) : IdxSubMeas (MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The mixed bridge A^u_a ⊗ L^ℓ_[f(v)=b], placed by strategy.state.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.diagonalLineProductOrdered {𝔓 : 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) : IdxOpFamily (MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The bridge I ⊗ (L^ℓ_[f(v)=b] · L^ℓ_[f(u)=a]), placed by strategy.state.R. Paper's "ordered" step: Lv * Lu (line measurement at v times line measurement at u).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.diagonalLineProductReversed {𝔓 : 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) : IdxOpFamily (MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The swapped bridge I ⊗ (L^ℓ_[f(u)=a] · L^ℓ_[f(v)=b]), placed by strategy.state.R. Paper's "reversed" step: Lu * Lv (projectively swapped from ordered).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.pointDiagonalLineMixedProductRight {𝔓 : 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) : IdxSubMeas (MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The mixed bridge A^v_b ⊗ L^ℓ_[f(u)=a], placed by strategy.state. Outcome (a, b) maps to strategy.state.L (A^v_b) * strategy.state.R (L^ℓ_[f(u)=a]), i.e. a indexes the line evaluation and b indexes the point measurement.

Equations

• One or more equations did not get rendered due to their size.