Sampling and operator-symmetry utilities

The counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/GlobalVariance/Theorems/SelfConsistencyTransport/Utilities.lean in the port of planning/c6b-plan.md (milestone M6, section "Port conventions"): support lemmas for the good-strategy self-consistency transport of lem:local-variance-of-points.

• ev_adjoint_sub_swap — the squared distance is unchanged by swapping the two operators;
• qSDDCore_optionUnit_some_le — the selected some () term of a two-outcome defect is at most the whole defect;
• generalizeBReversePointwiseBound — the reverse lem:generalize-b step at expansion.tex:309;
• rightPolynomialWeightSqrt_contraction, rightPolynomialWeightSqrt_grouped_contraction — S.R ((G_g)^{1/2}) is a contraction, and so is the column of them over a fiber g(u) = a;
• cabApproxDelta_sum_from_sdd — prop:cab-approx-delta with the grouped multiplier, summed over polynomials with no cardinality loss.

A same-space lemma (ev_adjoint_sub_swap, qSDDCore_optionUnit_some_le) takes a vector state V : VecState K. A lemma that places the weight (G_g)^{1/2} on the right factor takes the model S : SymModel 𝔓 K as its explicit first argument, rightTensor (ι₁ := ι) X being S.R X; cabApproxDelta_sum_from_sdd takes S where the vendored lemma takes its state ψ, and evaluates on it. generalizeBReversePointwiseBound takes V where the vendored lemma takes ψbi, as Theorems/CollisionExpansion.lean does.

The two marginal identities of the rerandomized hypercube-edge distribution are statements about distributions alone; this file imports the vendored file for them.

Not ported

• avgOver_rerandomizeCoord_fst: classical, imported.
• avgOver_rerandomizeCoord_snd: classical, imported.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/expansion.tex

theorem MIPRE.LIDT.Co.GlobalVariance.ev_adjoint_sub_swap {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (X Y : K →L[ℂ] K) : V.ev (star (Y - X) * (Y - X)) = V.ev (star (X - Y) * (X - Y))

The squared distance ev((Y - X)† (Y - X)) is symmetric in X and Y.

theorem MIPRE.LIDT.Co.GlobalVariance.qSDDCore_optionUnit_some_le {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution α) (A B : α → Option Unit → K →L[ℂ] K) : (MIPStarRE.LDT.avgOver 𝒟 fun (x : α) => V.qSDDCore (fun (x_1 : Unit) => A x (some ())) fun (x_1 : Unit) => B x (some ())) ≤ MIPStarRE.LDT.avgOver 𝒟 fun (x : α) => V.qSDDCore (A x) (B x)

The selected some () contribution is bounded by the full Option Unit summed squared-distance core.

This extracts the common monotonicity step used when a two-outcome postprocessed event is passed to cabApproxDelta: the singleton selected outcome is one summand of the full Option Unit sum defining qSDDCore.

theorem MIPRE.LIDT.Co.GlobalVariance.generalizeBReversePointwiseBound {𝔓 : 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) (V : VecState K) (G : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hgen : GeneralizeBStatement params strategy V G) (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; V.ev (star D * D)) ≤ MIPStarRE.LDT.GlobalVariance.generalizeBError params

The reverse lem:generalize-b step used at references/ldt-paper/expansion.tex, line 309.

The paper first moves from the evaluated line event to the exact restriction (line 308), then uses the same estimate in the reverse direction at the second sampled point (line 309). The squared-distance expression is unchanged by swapping the two endpoints, because (Y - X) = -(X - Y).

theorem MIPRE.LIDT.Co.GlobalVariance.rightPolynomialWeightSqrt_contraction {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (G : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (g : MIPStarRE.LDT.Polynomial params) : star (S.R (polynomialWeightSqrtOperator params G g)) * S.R (polynomialWeightSqrtOperator params G g) ≤ 1

The right placement of the square-root polynomial weight is a contraction.

The square of (G_g)^{1/2} is the submeasurement outcome G_g, and every outcome of a submeasurement is bounded by the identity.

theorem MIPRE.LIDT.Co.GlobalVariance.rightPolynomialWeightSqrt_grouped_contraction {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (G : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (u : MIPStarRE.LDT.Point params) (a : MIPStarRE.LDT.Fq params) : (∑ g : MIPStarRE.LDT.Polynomial params, star (if a = g.toFun u then S.R (polynomialWeightSqrtOperator params G g) else 0) * if a = g.toFun u then S.R (polynomialWeightSqrtOperator params G g) else 0) ≤ 1

Grouped-by-evaluation-value submeasurement contraction for (G_g)^{1/2}.

For a fixed point u and a field element a, sum over all polynomials g with g(u) = a of S.R ((G_g)^{1/2})† S.R ((G_g)^{1/2}). The contraction ∑_{g : g(u)=a} G_g ≤ I follows from the submeasurement inequality G.total ≤ I. This is the key algebraic input that allows the cabApproxDelta multiplier family in cabApproxDelta_sum_from_sdd and the sum-form 2ε endpoints to group polynomials by their evaluation value without incurring a cardinality factor.

theorem MIPRE.LIDT.Co.GlobalVariance.cabApproxDelta_sum_from_sdd {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Sample : Type u_3} (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Sample) (base : Sample → MIPStarRE.LDT.Point params) (left right : Sample → MIPStarRE.LDT.Fq params → K →L[ℂ] K) (L R : Sample → MIPStarRE.LDT.Polynomial params → K →L[ℂ] K) (G : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (η : ℝ) (hbase : (MIPStarRE.LDT.avgOver 𝒟 fun (s : Sample) => S.qSDDCore (left s) (right s)) ≤ η) (hleft : ∀ (s : Sample) (g : MIPStarRE.LDT.Polynomial params), S.R (polynomialWeightSqrtOperator params G g) * left s (g.toFun (base s)) = L s g) (hright : ∀ (s : Sample) (g : MIPStarRE.LDT.Polynomial params), S.R (polynomialWeightSqrtOperator params G g) * right s (g.toFun (base s)) = R s g) : (∑ g : MIPStarRE.LDT.Polynomial params, MIPStarRE.LDT.avgOver 𝒟 fun (s : Sample) => S.ev (star (L s g - R s g) * (L s g - R s g))) ≤ η

Shared polynomial-sum cabApproxDelta transport.

The argument keeps the answer space at Fq params, applies prop:cab-approx-delta with multiplier if a = g(base s) then S.R ((G_g)^{1/2}) else 0, and uses the grouped contraction rightPolynomialWeightSqrt_grouped_contraction. The bridge hypotheses identify the surviving fiber a = g(base s) with the weighted left and right operators desired by the caller.