Six-step local-variance transport-chain assembly

This module assembles the six steps of lem:local-variance-of-points (expansion.tex, lines 305--311) into a single triangle-inequality bound on the hypercube-edge distribution, producing the main transport estimate localVarianceTransportChainBound.

@[reducible, inline]

abbrev MIPStarRE.LDT.GlobalVariance.TransportQuestion (params : Parameters) [FieldModel params.q] : Type

Equations

• MIPStarRE.LDT.GlobalVariance.TransportQuestion params = ((MIPStarRE.LDT.AxisParallelLine params × MIPStarRE.LDT.Fq params) × MIPStarRE.LDT.Fq params)

theorem MIPStarRE.LDT.GlobalVariance.avgOver_transport_leftQuestion (params : Parameters) [FieldModel params.q] (f : AxisParallelLineQuestion params → Error) : (avgOver (uniformDistribution (TransportQuestion params)) fun (q : TransportQuestion params) => f (q.1.1, q.1.1.pointAt q.1.2)) = avgOver (axisParallelLineQuestionDistribution params) f

theorem MIPStarRE.LDT.GlobalVariance.avgOver_transport_rightQuestion (params : Parameters) [FieldModel params.q] (f : AxisParallelLineQuestion params → Error) : (avgOver (uniformDistribution (TransportQuestion params)) fun (q : TransportQuestion params) => f (q.1.1, q.1.1.pointAt q.2)) = avgOver (axisParallelLineQuestionDistribution params) f

theorem MIPStarRE.LDT.GlobalVariance.avgOver_transport_leftPoint (params : Parameters) [FieldModel params.q] (f : Point params → Error) : (avgOver (uniformDistribution (TransportQuestion params)) fun (q : TransportQuestion params) => f (q.1.1.pointAt q.1.2)) = avgOver (uniformDistribution (Point params)) f

theorem MIPStarRE.LDT.GlobalVariance.avgOver_transport_rightPoint (params : Parameters) [FieldModel params.q] (f : Point params → Error) : (avgOver (uniformDistribution (TransportQuestion params)) fun (q : TransportQuestion params) => f (q.1.1.pointAt q.2)) = avgOver (uniformDistribution (Point params)) f

theorem MIPStarRE.LDT.GlobalVariance.avgOver_transport_pointPair (params : Parameters) [FieldModel params.q] (f : Point params × Point params → Error) : (avgOver (uniformDistribution (TransportQuestion params)) fun (q : TransportQuestion params) => f (q.1.1.pointAt q.1.2, q.1.1.pointAt q.2)) = avgOver (uniformDistribution (AxisParallelTestSample params × Fq params)) fun (sx : AxisParallelTestSample params × Fq params) => f (sx.1.1, Function.update sx.1.1 sx.1.2 sx.2)

theorem MIPStarRE.LDT.GlobalVariance.avgOver_axisParallelTestSample_update_eq_rerandomizeCoord (params : Parameters) [FieldModel params.q] (f : Point params × Point params → Error) : (avgOver (uniformDistribution (AxisParallelTestSample params × Fq params)) fun (sx : AxisParallelTestSample params × Fq params) => f (sx.1.1, Function.update sx.1.1 sx.1.2 sx.2)) = avgOver (ExpansionHypercubeGraph.rerandomizeCoord params) f

theorem MIPStarRE.LDT.GlobalVariance.weightedGeneralizeBRightOperatorAtPolynomial_point_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) (ℓ : AxisParallelLine params) (u v : Point params) : weightedGeneralizeBRightOperatorAtPolynomial params strategy G g (ℓ, u) = weightedGeneralizeBRightOperatorAtPolynomial params strategy G g (ℓ, v)

theorem MIPStarRE.LDT.GlobalVariance.localVarianceTransportChainBound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : localVarianceDeviationAtPolynomial params strategy strategy.state G g ≤ localVarianceTransportChainError params eps delta

The paper's six-step edge transport estimate in the native rerandomizeCoord presentation.

The triangle chain is proved on the line-pair presentation above; this theorem reindexes that presentation back to the hypercube-edge sampler u, i, x ↦ (u, u[i ↦ x]), which is exactly rerandomizeCoord.

theorem MIPStarRE.LDT.GlobalVariance.localVarianceTransportChainError_le_localVarianceOfPointsError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] {eps delta gamma : Error} (strategy : SymStrat params ι) (hgood : strategy.IsGood eps delta gamma) : localVarianceTransportChainError params eps delta ≤ localVarianceOfPointsError params eps delta

The post-triangle six-step transport error is absorbed by the paper's 24(ε + δ + md/q) slack from lem:local-variance-of-points.

This is only the scalar arithmetic after applying prop:triangle-inequality-for-approx_delta with k = 6 to the estimates at references/ldt-paper/expansion.tex, lines 305--311; it does not assert the transport estimates themselves.