Sum-form local-variance chain

The counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/GlobalVariance/Theorems/TransportChain/SumForm.lean in the port of planning/c6b-plan.md (milestone M6, section "Port conventions"): the polynomial-sum reverse lem:generalize-b bound and the assembly of the six-step chain summed over all polynomials, localVarianceDeviation_sum_le_localVarianceOfPointsError, which closes eq:equivalent-local-variance with no factor of the number of polynomials.

The six sum-form step bounds are

1. pointConditionedEventSelfConsistency_weighted_point_sum (2δ),
2. axisParallelPointLineConsistency_weighted_rightToLeftLineQuestion_sum (2ε),
3. generalizeBDeviationAtPolynomial_polysum_le_error (md/q, forward),
4. generalizeBReversePointwiseBound_polysum_le_error (md/q, reverse; below),
5. axisParallelPointLineConsistency_weighted_leftToRightLineQuestion_sum (2ε),
6. the first again, through ev_adjoint_sub_swap (2δ).

The vendored proof telescopes the six operator differences pointwise with ev_sum_conjTranspose_mul_sum_le, then sums over g, averages and swaps the sums by hand. Here the polynomial g is the outcome of a raw operator family, q ↦ (g ↦ A_i g q), so that a step's SDDOpRel error is exactly its sum over g of averaged squared distances (after avgOver_sum), and the six steps are chained by Preliminaries.sddOpRel_chain, as the per-polynomial chain of TransportChain/Core.lean is. Each step bound is a term: a classical reindexing of the line-pair sample space followed by a ported sum-form endpoint. No statement here carries a swap or normalization hypothesis.

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 305--321

theorem MIPRE.LIDT.Co.GlobalVariance.generalizeBReversePointwiseBound_polysum_le_error {𝔓 : 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, MIPStarRE.LDT.avgOver (MIPStarRE.LDT.GlobalVariance.axisParallelLineQuestionDistribution params) fun (qu : MIPStarRE.LDT.GlobalVariance.AxisParallelLineQuestion params) => have D := weightedGeneralizeBRightOperatorAtPolynomial params strategy G g qu - weightedGeneralizeBLeftOperatorAtPolynomial params strategy G g qu; strategy.state.ev (star D * D)) ≤ MIPStarRE.LDT.GlobalVariance.generalizeBError params

Reverse lem:generalize-b bound summed over all polynomials: the reverse squared distance equals the forward one by ev_adjoint_sub_swap, so this is generalizeBDeviationAtPolynomial_polysum_le_error. The sum-form step 4 (md/q, reverse) of the six-step local-variance chain.

theorem MIPRE.LIDT.Co.GlobalVariance.localVarianceDeviation_sum_le_localVarianceOfPointsError {𝔓 : 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) 𝔓) : ∑ g : MIPStarRE.LDT.Polynomial params, localVarianceDeviationAtPolynomial params strategy strategy.state.toVecState G g ≤ MIPStarRE.LDT.GlobalVariance.localVarianceOfPointsError params eps delta

Chain assembly for eq:equivalent-local-variance: the local-variance deviations summed over all polynomials are at most localVarianceOfPointsError = 24(ε + δ + md/q).

The six steps of lem:local-variance-of-points (expansion.tex, lines 305--311), each summed over g with its sum-form bound, are chained with k = 6 on the line-pair presentation TransportQuestion, which is then reindexed to the hypercube-edge sampler rerandomizeCoord; the transport-chain error 6 (4ε + 4δ + 2md/q) is absorbed into localVarianceOfPointsError.