Algebraic identities and variance reductions

theorem MIPStarRE.LDT.GlobalVariance.pointConditionedExpansionTransfer {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : pointConditionedGlobalVarianceAtPolynomial params strategy G g ≤ ↑params.m * pointConditionedLocalVarianceAtPolynomial params strategy G g

theorem MIPStarRE.LDT.GlobalVariance.globalVarianceOfPoints_bound_of_local (params : Parameters) [FieldModel params.q] (eps delta : Error) (globalVariance localVariance : Polynomial params → Error) (hexpansion : ∀ (g : Polynomial params), globalVariance g ≤ ↑params.m * localVariance g) (hlocal : ∀ (g : Polynomial params), localVariance g ≤ localVarianceOfPointsError params eps delta) (g : Polynomial params) : globalVariance g ≤ globalVarianceOfPointsError params eps delta

Algebraic norm/variance reductions

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

theorem MIPStarRE.LDT.GlobalVariance.polynomialWeightSqrtOperator_mul_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : polynomialWeightSqrtOperator params G g * polynomialWeightSqrtOperator params G g = G.outcome g

theorem MIPStarRE.LDT.GlobalVariance.weightedPointConditionedOperator_sub {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) (u v : Point params) : weightedPointConditionedOperatorAtPolynomial params strategy G g u - weightedPointConditionedOperatorAtPolynomial params strategy G g v = opTensor (pointConditionedOutcomeOperatorAtPolynomial params strategy g u - pointConditionedOutcomeOperatorAtPolynomial params strategy g v) (polynomialWeightSqrtOperator params G g)

The difference of the two weighted point-conditioned operators factors as the tensor product of the point-operator difference and the square root of the polynomial outcome.

theorem MIPStarRE.LDT.GlobalVariance.weightedPointConditionedOperator_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) (u v : Point params) : have D := weightedPointConditionedOperatorAtPolynomial params strategy G g u - weightedPointConditionedOperatorAtPolynomial params strategy G g v; Matrix.conjTranspose D * D = opTensor (Matrix.conjTranspose (pointConditionedOutcomeOperatorAtPolynomial params strategy g u - pointConditionedOutcomeOperatorAtPolynomial params strategy g v) * (pointConditionedOutcomeOperatorAtPolynomial params strategy g u - pointConditionedOutcomeOperatorAtPolynomial params strategy g v)) (G.outcome g)

The square of the weighted point-conditioned difference is the tensor of the squared point-operator difference with the polynomial outcome.

theorem MIPStarRE.LDT.GlobalVariance.generalizeBDeviationAtPolynomial_eq_collisionResidual {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (ψbi : QuantumState (ι × ι)) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : generalizeBDeviationAtPolynomial params strategy ψbi G g = generalizeBCollisionResidual params strategy ψbi G g

Projective expansion for the pointwise lem:generalize-b deviation.

For incident line questions, the right event f = g|_ℓ is a subevent of the left event f(u)=g(u). Since B^ℓ is projective, the squared difference is exactly the residual line-collision event f(u)=g(u) ∧ f≠g|_ℓ, with the right-register square root collapsed to G_g.

theorem MIPStarRE.LDT.GlobalVariance.localVarianceDeviationAtPolynomial_eq_two_pointConditionedLocalVarianceAtPolynomial {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : localVarianceDeviationAtPolynomial params strategy strategy.state G g = 2 * pointConditionedLocalVarianceAtPolynomial params strategy G g

The edgewise weighted squared-difference expression is exactly twice the local variance of the point-conditioned family on the weighted state. This is eq:equivalent-local-variance unpacked at a fixed polynomial.

theorem MIPStarRE.LDT.GlobalVariance.globalVarianceDeviationAtPolynomial_eq_two_pointConditionedGlobalVarianceAtPolynomial {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : globalVarianceDeviationAtPolynomial params strategy strategy.state G g = 2 * pointConditionedGlobalVarianceAtPolynomial params strategy G g

The independent-points weighted squared-difference expression is exactly twice the global variance of the point-conditioned family on the weighted state.

theorem MIPStarRE.LDT.GlobalVariance.pointConditionedLocalVarianceAtPolynomial_le_of_deviation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) {g : Polynomial params} {η : Error} (hdev : localVarianceDeviationAtPolynomial params strategy strategy.state G g ≤ η) : pointConditionedLocalVarianceAtPolynomial params strategy G g ≤ η

A bound on the edgewise weighted norm expression implies the corresponding bound on the local variance. The factor 1/2 in localVariance only strengthens the estimate.

theorem MIPStarRE.LDT.GlobalVariance.globalVarianceDeviationAtPolynomial_le_m_localVarianceDeviationAtPolynomial {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : globalVarianceDeviationAtPolynomial params strategy strategy.state G g ≤ ↑params.m * localVarianceDeviationAtPolynomial params strategy strategy.state G g

Pointwise local-to-global transfer for the paper's weighted squared-norm form: the independent-points expression is at most m times the edge expression. This combines lem:local-to-global with the two exact norm/variance identities above, so no independent global-deviation hypothesis is needed.