Section 10 — Definitions

Auxiliary definitions for the commutativity-at-points argument from Section 10 of the low individual degree paper. This file packages the sampled diagonal-line questions, point/line bridge families, and the error terms used by commutativityPoints.

References

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

@[reducible, inline]

abbrev MIPStarRE.LDT.CommutativityPoints.PointPairOutcome (params : Parameters) : Type

Outcomes (a, b) for the ordered or reversed product of two point measurements.

Equations

• MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params = (MIPStarRE.LDT.Fq params × MIPStarRE.LDT.Fq params)

@[reducible, inline]

abbrev MIPStarRE.LDT.CommutativityPoints.PointDiagonalLineQuestion (params : Parameters) : Type

A diagonal line together with a sampled parameter on that line.

Equations

• MIPStarRE.LDT.CommutativityPoints.PointDiagonalLineQuestion params = (MIPStarRE.LDT.DiagonalLine params × MIPStarRE.LDT.Fq params)

@[reducible, inline]

abbrev MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion (params : Parameters) : Type

A diagonal line together with the two sampled parameters used for a point pair.

Equations

• MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params = (MIPStarRE.LDT.DiagonalLine params × MIPStarRE.LDT.Fq params × MIPStarRE.LDT.Fq params)

@[instance_reducible]

noncomputable instance MIPStarRE.LDT.CommutativityPoints.instFintypeDiagonalLine (params : Parameters) : Fintype (DiagonalLine params)

Diagonal lines form a finite type via their base point and direction vector.

Equations

• MIPStarRE.LDT.CommutativityPoints.instFintypeDiagonalLine params = Fintype.ofInjective (fun (ℓ : MIPStarRE.LDT.DiagonalLine params) => (ℓ.base, ℓ.direction)) ⋯

noncomputable def MIPStarRE.LDT.CommutativityPoints.orderedProductOpFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) : OpFamily (α × β) ι

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

Equations

• MIPStarRE.LDT.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 MIPStarRE.LDT.CommutativityPoints.reversedProductOpFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) : OpFamily (α × β) ι

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

Equations

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

theorem MIPStarRE.LDT.CommutativityPoints.tensorProductSubMeas_sum_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) : ∑ ab : α × β, leftTensor (A.outcome ab.1) * rightTensor (B.outcome ab.2) = leftTensor A.total * rightTensor B.total

The outcome effects of tensorProductSubMeas sum to its total effect.

noncomputable def MIPStarRE.LDT.CommutativityPoints.tensorProductSubMeas {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) : SubMeas (α × β) (ι × ι)

Tensor-product bridge A_a ⊗ B_b on the bipartite space ι × ι.

Equations

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

def MIPStarRE.LDT.CommutativityPoints.sampledPointFromDiagonalQuestion (params : Parameters) [FieldModel params.q] (q : PointDiagonalLineQuestion params) : Point params

Recover the sampled point from a diagonal-line/parameter sample.

Equations

• MIPStarRE.LDT.CommutativityPoints.sampledPointFromDiagonalQuestion params q = q.1.pointAt q.2

def MIPStarRE.LDT.CommutativityPoints.sampledPointPairFromSharedDiagonalQuestion (params : Parameters) [FieldModel params.q] (q : PointPairDiagonalLineQuestion params) : GlobalVariance.PointPairQuestion params

Recover the two sampled points from a shared diagonal-line sample.

Equations

• MIPStarRE.LDT.CommutativityPoints.sampledPointPairFromSharedDiagonalQuestion params q = (q.1.pointAt q.2.1, q.1.pointAt q.2.2)

noncomputable def MIPStarRE.LDT.CommutativityPoints.pointMeasurementProductLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) : IdxOpFamily (GlobalVariance.PointPairQuestion params) (PointPairOutcome params) (ι × ι)

The ordered point product (A^u_a A^v_b) ⊗ I on the bipartite space d * d.

Equations

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

noncomputable def MIPStarRE.LDT.CommutativityPoints.pointMeasurementProductRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) : IdxOpFamily (GlobalVariance.PointPairQuestion params) (PointPairOutcome params) (ι × ι)

The reversed point product (A^v_b A^u_a) ⊗ I on the bipartite space ι × ι.

Equations

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

noncomputable def MIPStarRE.LDT.CommutativityPoints.pointWithDiagonalLineDistribution (params : Parameters) [FieldModel params.q] : Distribution (PointDiagonalLineQuestion params)

Distribution obtained by sampling a diagonal line together with a parameter on that line.

Equations

• MIPStarRE.LDT.CommutativityPoints.pointWithDiagonalLineDistribution params = MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.CommutativityPoints.PointDiagonalLineQuestion params)

theorem MIPStarRE.LDT.CommutativityPoints.pointWithDiagonalLineDistribution_isProbability (params : Parameters) [FieldModel params.q] : (pointWithDiagonalLineDistribution params).IsProbability

The diagonal-line/parameter question distribution is a probability distribution.

theorem MIPStarRE.LDT.CommutativityPoints.pointWithDiagonalLineDistribution_toPMF (params : Parameters) [FieldModel params.q] : (pointWithDiagonalLineDistribution params).toPMF ⋯ = PMF.uniformOfFintype (PointDiagonalLineQuestion params)

The diagonal-line/parameter question distribution is Mathlib's uniform PMF on its finite question type.

noncomputable def MIPStarRE.LDT.CommutativityPoints.sharedDiagonalLineQuestionOfPointPair (params : Parameters) [FieldModel params.q] (s : GlobalVariance.PointPairQuestion params × Fq params) : PointPairDiagonalLineQuestion params

Realize a shared-line sample from a uniformly random point pair and parameter.

The resulting line is parameterized so that the first point is visited at t and the second at t + 1. This matches the paper's sampling of two random points together with some diagonal line containing both.

Equations

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

noncomputable def MIPStarRE.LDT.CommutativityPoints.pointPairSharedDiagonalLineDistribution (params : Parameters) [FieldModel params.q] : Distribution (PointPairDiagonalLineQuestion params)

Distribution obtained by sampling a uniform point pair and then packaging it as a shared diagonal-line question.

Equations

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

theorem MIPStarRE.LDT.CommutativityPoints.pointPairSharedDiagonalLineDistribution_isProbability (params : Parameters) [FieldModel params.q] : (pointPairSharedDiagonalLineDistribution params).IsProbability

The shared diagonal-line question distribution is a probability distribution.

theorem MIPStarRE.LDT.CommutativityPoints.pointPairSharedDiagonalLineDistribution_toPMF (params : Parameters) [FieldModel params.q] : (pointPairSharedDiagonalLineDistribution params).toPMF ⋯ = PMF.map (sharedDiagonalLineQuestionOfPointPair params) (PMF.uniformOfFintype (GlobalVariance.PointPairQuestion params × Fq params))

The shared diagonal-line question distribution is the Mathlib push-forward of the uniform PMF on point pairs and the auxiliary line parameter.

def MIPStarRE.LDT.CommutativityPoints.sampledPointMeasurement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) : IdxSubMeas (PointDiagonalLineQuestion params) (Fq params) ι

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

Equations

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

noncomputable def MIPStarRE.LDT.CommutativityPoints.sampledDiagonalLineEvaluation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) : IdxSubMeas (PointDiagonalLineQuestion params) (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 MIPStarRE.LDT.CommutativityPoints.pointMeasurementProductAlongSharedLine {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) : IdxOpFamily (PointPairDiagonalLineQuestion params) (PointPairOutcome params) (ι × ι)

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 MIPStarRE.LDT.CommutativityPoints.pointMeasurementProductAlongSharedLineReversed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) : IdxOpFamily (PointPairDiagonalLineQuestion params) (PointPairOutcome params) (ι × ι)

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 MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineMixedProductLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) : IdxSubMeas (PointPairDiagonalLineQuestion params) (PointPairOutcome params) (ι × ι)

The mixed bridge A^u_a ⊗ L^ℓ_[f(v)=b] on the bipartite space d * d.

Equations

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

noncomputable def MIPStarRE.LDT.CommutativityPoints.diagonalLineProductOrdered {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) : IdxOpFamily (PointPairDiagonalLineQuestion params) (PointPairOutcome params) (ι × ι)

The bridge I ⊗ (L^ℓ_[f(v)=b] · L^ℓ_[f(u)=a]) on the bipartite space. 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 MIPStarRE.LDT.CommutativityPoints.diagonalLineProductReversed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) : IdxOpFamily (PointPairDiagonalLineQuestion params) (PointPairOutcome params) (ι × ι)

The swapped bridge I ⊗ (L^ℓ_[f(u)=a] · L^ℓ_[f(v)=b]) on the bipartite space. 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 MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineMixedProductRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) : IdxSubMeas (PointPairDiagonalLineQuestion params) (PointPairOutcome params) (ι × ι)

The mixed bridge A^v_b ⊗ L^ℓ_[f(u)=a] on the bipartite space ι × ι. Outcome (a, b) maps to leftTensor(A^v_b) * rightTensor(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.

def MIPStarRE.LDT.CommutativityPoints.restrictedDiagonalLinesConsistencyError (params : Parameters) (gamma : Error) : Error

The intermediate consistency loss coming from the m-restricted diagonal-lines test.

Equations

• MIPStarRE.LDT.CommutativityPoints.restrictedDiagonalLinesConsistencyError params gamma = gamma * ↑params.m

def MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineApproxError (params : Parameters) (gamma : Error) : Error

The approximation loss obtained from prop:simeq-to-approx.

Equations

• MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineApproxError params gamma = 2 * MIPStarRE.LDT.CommutativityPoints.restrictedDiagonalLinesConsistencyError params gamma

def MIPStarRE.LDT.CommutativityPoints.commutativityPointsError (params : Parameters) (gamma : Error) : Error

The displayed commutativity error from thm:commutativity-points.

Equations

• MIPStarRE.LDT.CommutativityPoints.commutativityPointsError params gamma = 32 * gamma * ↑params.m