Main variance theorem reductions

This module contains the high-level theorem reductions for lem:local-variance-of-points, lem:global-variance-of-points, and lem:generalize-b. These combine the algebraic identities, collision expansions, and transport estimates from the preceding modules into the final statement records used by downstream consumers.

Strategy-state reductions

theorem MIPStarRE.LDT.GlobalVariance.localVarianceOfPointsFromEdgeDeviation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (G : SubMeas (Polynomial params) ι) (hedge : ∀ (g : Polynomial params), localVarianceDeviationAtPolynomial params strategy strategy.state G g ≤ localVarianceOfPointsError params eps delta) : LocalVarianceOfPointsStatement params strategy strategy.state G eps delta

Strict reduction for lem:local-variance-of-points on the strategy state.

Compared with the former supplied-bounds reduction, this theorem does not require the local-variance bound as a separate hypothesis: it derives it from the edgewise weighted squared-norm estimate using localVarianceDeviationAtPolynomial_eq_two_pointConditionedLocalVarianceAtPolynomial. The remaining analytic input is exactly the paper's six-step edge transport bound, not a conclusion-shaped local-variance hypothesis.

theorem MIPStarRE.LDT.GlobalVariance.globalVarianceOfPointsFromLocalDeviation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (G : SubMeas (Polynomial params) ι) (hlocalDev : ∀ (g : Polynomial params), localVarianceDeviationAtPolynomial params strategy strategy.state G g ≤ localVarianceOfPointsError params eps delta) : GlobalVarianceOfPointsStatement params strategy strategy.state G eps delta

Reduction for lem:global-variance-of-points on the strategy state.

This theorem proves the independent-points norm bound from the local edge norm estimate by applying lem:local-to-global to the weighted state and using the exact norm/variance identities above. The remaining analytic input is the local edge transport estimate from lem:local-variance-of-points.

theorem MIPStarRE.LDT.GlobalVariance.globalVarianceDeviation_sum_le_m_mul_localVarianceDeviation_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) : ∑ g : Polynomial params, globalVarianceDeviationAtPolynomial params strategy strategy.state G g ≤ ↑params.m * ∑ g : Polynomial params, localVarianceDeviationAtPolynomial params strategy strategy.state G g

Sum-level local-to-global transfer for the polynomial-indexed squared-norm form of lem:global-variance-of-points.

This is the unnormalized analogue of the pointwise globalVarianceDeviationAtPolynomial_le_m_localVarianceDeviationAtPolynomial: the independent-points deviation summed over all polynomials is at most m times the corresponding edge-deviation sum.

theorem MIPStarRE.LDT.GlobalVariance.globalVarianceDeviation_sum_le_of_localVarianceDeviation_sum_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (G : SubMeas (Polynomial params) ι) (hlocal : ∑ g : Polynomial params, localVarianceDeviationAtPolynomial params strategy strategy.state G g ≤ localVarianceOfPointsError params eps delta) : ∑ g : Polynomial params, globalVarianceDeviationAtPolynomial params strategy strategy.state G g ≤ globalVarianceOfPointsError params eps delta

A polynomial-sum local-variance bound implies the corresponding sum-form global-variance bound with the paper's 24m(ε + δ + md/q) error term.

The hypothesis hlocal is the paper's eq:equivalent-local-variance (references/ldt-paper/expansion.tex:317--321). The conclusion is the sum-form squared-norm bound underlying eq:global-variance-of-points-equation (references/ldt-paper/expansion.tex:325--353).

theorem MIPStarRE.LDT.GlobalVariance.localVarianceOfPointsFromTransportChainBound {ι : 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) ι) (hchain : ∀ (g : Polynomial params), localVarianceDeviationAtPolynomial params strategy strategy.state G g ≤ localVarianceTransportChainError params eps delta) : LocalVarianceOfPointsStatement params strategy strategy.state G eps delta

Strategy-state reduction for lem:local-variance-of-points from the post-triangle six-step transport-chain bound.

This replaces the final displayed edge estimate by the bound produced after applying prop:triangle-inequality-for-approx_delta with k = 6 to the six paper steps (2δ + 2ε + md/q + md/q + 2ε + 2δ). Thus the named estimate is ∀ g, localVarianceDeviationAtPolynomial … g ≤ localVarianceTransportChainError …. The absorption into the public 24(ε + δ + md/q) statement is proved above.

theorem MIPStarRE.LDT.GlobalVariance.globalVarianceOfPointsFromTransportChainBound {ι : 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) ι) (hchain : ∀ (g : Polynomial params), localVarianceDeviationAtPolynomial params strategy strategy.state G g ≤ localVarianceTransportChainError params eps delta) : GlobalVarianceOfPointsStatement params strategy strategy.state G eps delta

Strategy-state global-variance reduction from the post-triangle six-step local-variance transport-chain bound.

theorem MIPStarRE.LDT.GlobalVariance.globalVarianceOfPoints {ι : 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) ι) : GlobalVarianceOfPointsStatement params strategy strategy.state G eps delta

Paper origin: references/ldt-paper/expansion.tex:325-353 (\label{lem:global-variance-of-points}).

Statement of the global variance lemma for the point measurements. The paper assumes a good projective strategy and a polynomial submeasurement G, and proves the independent-points comparison with error 24m(ε + δ + md/q). In particular, the local and global variance estimates are conclusions to be proved, not additional hypotheses of the theorem.