Documentation

MIPRE.Background.LIDT.Co.GlobalVariance.Theorems.PolynomialSumBounds

Polynomial-sum (cardinality-free) bounds for the Section 8 transport #

The counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/GlobalVariance/Theorems/PolynomialSumBounds.lean in the port of planning/c6b-plan.md (milestone M6, section "Port conventions"): the sum over all polynomials g of the lem:generalize-b residuals of CollisionExpansion.lean is at most md/q, with no factor of the number of polynomials. The line-measurement identity ∑_f B^ℓ_f = B^ℓ.total and the submeasurement identity ∑_g G_g = G.total collapse the joint tensor mass ∑_g ∑_f ev(B^ℓ_f ⊗ G_g) to ev(B^ℓ.total ⊗ G.total) ≤ ev 1 = 1 (generalizeBLineCollisionTensorMass_polysum_le_one), and the per-polynomial Schwartz–Zippel coefficient bound does the rest.

opTensor is strategy.state.opTensor and ev strategy.state is strategy.state.ev. The normalization ev 1 = 1 is the keystone's hypothesis-free ev_one_of_isNormalized, so the vendored strategy.isNormalized argument disappears; 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:

source
theorem MIPRE.LIDT.Co.GlobalVariance.generalizeBLineCollisionTensorMass_polysum_le_one {𝔓 : 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) 𝔓) (ℓ : MIPStarRE.LDT.AxisParallelLine params) :
∑ g : MIPStarRE.LDT.Polynomial params, ∑ f : MIPStarRE.LDT.AxisLinePolynomial params, strategy.state.ev (strategy.state.opTensor ((strategy.axisParallelMeasurement.toIdxProjMeas ℓ).outcome f) (G.outcome g)) ≤ 1

Polynomial-sum analogue of generalizeBLineCollisionTensorMass_sum_le_one: the joint tensor mass ∑_g ∑_f ev(B^ℓ_f ⊗ G_g) is at most 1, with no cardinality factor in the polynomial index, since it equals ev(B^ℓ.total ⊗ G.total).

source
theorem MIPRE.LIDT.Co.GlobalVariance.generalizeBLineCollisionExpansion_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, generalizeBLineCollisionExpansion params strategy strategy.state.toVecState G g ≤ MIPStarRE.LDT.GlobalVariance.generalizeBError params

Polynomial-sum analogue of generalizeBLineCollisionExpansion_le_error: the line-collision expansion summed over all polynomials is at most generalizeBError = md/q, without the polynomial cardinality. Each line is bounded by the Schwartz–Zippel coefficient bound and generalizeBLineCollisionTensorMass_polysum_le_one; this is the cardinality-free form of expansion.tex, lines 282--289, underlying eq:equivalent-local-variance.

source
theorem MIPRE.LIDT.Co.GlobalVariance.generalizeBSeedCollisionExpansion_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, generalizeBSeedCollisionExpansion params strategy strategy.state.toVecState G g ≤ MIPStarRE.LDT.GlobalVariance.generalizeBError params

Polynomial-sum analogue of generalizeBSeedCollisionExpansion_le_error: the seed/line expansion identity composed with the polynomial-sum line bound.

source
theorem MIPRE.LIDT.Co.GlobalVariance.generalizeBCollisionResidual_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, generalizeBCollisionResidual params strategy strategy.state.toVecState G g ≤ MIPStarRE.LDT.GlobalVariance.generalizeBError params

Polynomial-sum analogue of generalizeBCollisionResidual_le_error: the incident-question reindexing identity composed with the polynomial-sum seed bound.

source
theorem MIPRE.LIDT.Co.GlobalVariance.generalizeBDeviationAtPolynomial_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, generalizeBDeviationAtPolynomial params strategy strategy.state.toVecState G g ≤ MIPStarRE.LDT.GlobalVariance.generalizeBError params

Polynomial-sum analogue of generalizeBPointwiseSchwartzZippel: the weighted Schwartz–Zippel residual summed over all polynomials is at most md/q, not N · md/q (expansion.tex, lines 282--289). This is the form eq:equivalent-local-variance uses for the two md/q steps (3 and 4) of the six-step chain of lem:local-variance-of-points.