Main variance theorem reductions

The counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/GlobalVariance/Theorems/MainTheorems.lean in the port of planning/c6b-plan.md (milestone M6, section "Port conventions"): the high-level reductions for lem:local-variance-of-points, lem:global-variance-of-points and their polynomial-sum forms, which combine the algebraic identities, the local-to-global transfer and the six-step transport chain of the preceding modules into the statement records of Theorems/Statements.lean, and the paper-facing globalVarianceOfPoints.

The vendored second state ψbi of the records is the strategy's model strategy.state, which coerces to a VecState K. No statement here carries a swap or normalization hypothesis, and the file-wide backward.isDefEq.respectTransparency false of the vendored file is not needed.

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/expansion.tex, lines 292--353

Strategy-state reductions

theorem MIPRE.LIDT.Co.GlobalVariance.localVarianceOfPointsFromEdgeDeviation {𝔓 : 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 : ℝ) (G : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hedge : ∀ (g : MIPStarRE.LDT.Polynomial params), localVarianceDeviationAtPolynomial params strategy strategy.state.toVecState G g ≤ MIPStarRE.LDT.GlobalVariance.localVarianceOfPointsError params eps delta) : LocalVarianceOfPointsStatement params strategy strategy.state.toVecState G eps delta

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

The local-variance bound is not a separate hypothesis: it is derived from the edgewise weighted squared-norm estimate through localVarianceDeviationAtPolynomial_eq_two_pointConditionedLocalVarianceAtPolynomial. The remaining analytic input is exactly the paper's six-step edge transport bound.

theorem MIPRE.LIDT.Co.GlobalVariance.globalVarianceOfPointsFromLocalDeviation {𝔓 : 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 : ℝ) (G : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hlocalDev : ∀ (g : MIPStarRE.LDT.Polynomial params), localVarianceDeviationAtPolynomial params strategy strategy.state.toVecState G g ≤ MIPStarRE.LDT.GlobalVariance.localVarianceOfPointsError params eps delta) : GlobalVarianceOfPointsStatement params strategy strategy.state.toVecState G eps delta

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

The independent-points norm bound follows from the local edge norm estimate by lem:local-to-global on the weighted family and the exact norm/variance identities. The remaining analytic input is the local edge transport estimate of lem:local-variance-of-points.

theorem MIPRE.LIDT.Co.GlobalVariance.globalVarianceDeviation_sum_le_m_mul_localVarianceDeviation_sum {𝔓 : 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) (G : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ∑ g : MIPStarRE.LDT.Polynomial params, globalVarianceDeviationAtPolynomial params strategy strategy.state.toVecState G g ≤ ↑params.m * ∑ g : MIPStarRE.LDT.Polynomial params, localVarianceDeviationAtPolynomial params strategy strategy.state.toVecState G g

Sum-level local-to-global transfer for the polynomial-indexed squared-norm form of lem:global-variance-of-points: the independent-points deviation summed over all polynomials is at most m times the edge-deviation sum, the unnormalized analogue of globalVarianceDeviationAtPolynomial_le_m_localVarianceDeviationAtPolynomial.

theorem MIPRE.LIDT.Co.GlobalVariance.globalVarianceDeviation_sum_le_of_localVarianceDeviation_sum_le {𝔓 : 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 : ℝ) (G : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hlocal : ∑ g : MIPStarRE.LDT.Polynomial params, localVarianceDeviationAtPolynomial params strategy strategy.state.toVecState G g ≤ MIPStarRE.LDT.GlobalVariance.localVarianceOfPointsError params eps delta) : ∑ g : MIPStarRE.LDT.Polynomial params, globalVarianceDeviationAtPolynomial params strategy strategy.state.toVecState G g ≤ MIPStarRE.LDT.GlobalVariance.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 (expansion.tex, lines 317--321); the conclusion is the sum-form squared-norm bound underlying eq:global-variance-of-points-equation (expansion.tex, lines 325--353).

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

Strategy-state reduction for lem:local-variance-of-points from the post-triangle six-step transport-chain bound 2δ + 2ε + md/q + md/q + 2ε + 2δ (prop:triangle-inequality-for-approx_delta with k = 6), absorbed into the public 24(ε + δ + md/q) error.

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

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

theorem MIPRE.LIDT.Co.GlobalVariance.globalVarianceOfPoints {𝔓 : 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) (G : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : GlobalVarianceOfPointsStatement params strategy strategy.state.toVecState G eps delta

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

The global variance lemma for the point measurements: for a good strategy and a polynomial submeasurement G, the independent-points comparison holds with error 24m(ε + δ + md/q). The local and global variance estimates are conclusions, not hypotheses.