Sampling and operator-symmetry utilities

Support lemmas for the good-strategy self-consistency transport (SelfConsistencyTransport):

• ev_adjoint_sub_swap — squared-distance invariance under swapping endpoints (used by the reverse generalize-b step and by pointConditionedEventSelfConsistency_weighted_rightEdge);
• generalizeBReversePointwiseBound — the reverse lem:generalize-b step at expansion.tex:309;
• avgOver_rerandomizeCoord_fst / avgOver_rerandomizeCoord_snd — both marginals of the hypercube-edge sampling distribution are uniform (expansion.tex:300–302).

theorem MIPStarRE.LDT.GlobalVariance.ev_adjoint_sub_swap {κ : Type u_2} [Fintype κ] [DecidableEq κ] (ψ : QuantumState κ) (X Y : Quantum.Op κ) : ev ψ (Matrix.conjTranspose (Y - X) * (Y - X)) = ev ψ (Matrix.conjTranspose (X - Y) * (X - Y))

theorem MIPStarRE.LDT.GlobalVariance.qSDDCore_optionUnit_some_le {α : Type u_2} {κ : Type u_3} [Fintype κ] [DecidableEq κ] (ψ : QuantumState κ) (𝒟 : Distribution α) (A B : α → Option Unit → Quantum.Op κ) : (avgOver 𝒟 fun (x : α) => qSDDCore ψ (fun (x_1 : Unit) => A x (some ())) fun (x_1 : Unit) => B x (some ())) ≤ avgOver 𝒟 fun (x : α) => 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 MIPStarRE.LDT.GlobalVariance.generalizeBReversePointwiseBound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (ψbi : QuantumState (ι × ι)) (G : SubMeas (Polynomial params) ι) (hgen : GeneralizeBStatement params strategy ψbi G) (g : Polynomial params) : (avgOver (axisParallelLineQuestionDistribution params) fun (qu : AxisParallelLineQuestion params) => have D := weightedGeneralizeBRightOperatorAtPolynomial params strategy G g qu - weightedGeneralizeBLeftOperatorAtPolynomial params strategy G g qu; ev ψbi (Matrix.conjTranspose D * D)) ≤ 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 MIPStarRE.LDT.GlobalVariance.avgOver_rerandomizeCoord_fst (params : Parameters) [FieldModel params.q] (f : Point params → Error) : (avgOver (ExpansionHypercubeGraph.rerandomizeCoord params) fun (uv : Point params × Point params) => f uv.1) = avgOver (uniformDistribution (Point params)) f

The first marginal of the rerandomized hypercube-edge distribution is uniform. This is the finite-distribution form of the sampling statement in expansion.tex, lines 300--302.

theorem MIPStarRE.LDT.GlobalVariance.avgOver_rerandomizeCoord_snd (params : Parameters) [FieldModel params.q] (f : Point params → Error) : (avgOver (ExpansionHypercubeGraph.rerandomizeCoord params) fun (uv : Point params × Point params) => f uv.2) = avgOver (uniformDistribution (Point params)) f

The second marginal of the rerandomized hypercube-edge distribution is uniform. This is the symmetric endpoint form of the sampling statement in expansion.tex, lines 300--302.

theorem MIPStarRE.LDT.GlobalVariance.rightPolynomialWeightSqrt_contraction {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : Matrix.conjTranspose (rightTensor (polynomialWeightSqrtOperator params G g)) * rightTensor (polynomialWeightSqrtOperator params G g) ≤ 1

The right tensor 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 MIPStarRE.LDT.GlobalVariance.rightPolynomialWeightSqrt_grouped_contraction {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (G : SubMeas (Polynomial params) ι) (u : Point params) (a : Fq params) : (∑ g : Polynomial params, (if a = g.toFun u then rightTensor (polynomialWeightSqrtOperator params G g) else 0).conjTranspose * if a = g.toFun u then rightTensor (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 the rightTensor of (G_g)^{1/2} * (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 MIPStarRE.LDT.GlobalVariance.cabApproxDelta_sum_from_sdd {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Sample : Type u_2} (params : Parameters) [FieldModel params.q] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Sample) (base : Sample → Point params) (left right : Sample → Fq params → Quantum.Op (ι × ι)) (L R : Sample → Polynomial params → Quantum.Op (ι × ι)) (G : SubMeas (Polynomial params) ι) (η : Error) (hbase : (avgOver 𝒟 fun (s : Sample) => qSDDCore ψ (left s) (right s)) ≤ η) (hleft : ∀ (s : Sample) (g : Polynomial params), rightTensor (polynomialWeightSqrtOperator params G g) * left s (g.toFun (base s)) = L s g) (hright : ∀ (s : Sample) (g : Polynomial params), rightTensor (polynomialWeightSqrtOperator params G g) * right s (g.toFun (base s)) = R s g) : (∑ g : Polynomial params, avgOver 𝒟 fun (s : Sample) => ev ψ (Matrix.conjTranspose (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 I ⊗ (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.