Section 8 global variance: algebraic identities and variance reductions #
The counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/GlobalVariance/Theorems/AlgebraicIdentity.lean in the port
of planning/c6b-plan.md (milestone M6, section "Port conventions"): the local-to-global transfer
for the point-conditioned variances (pointConditionedExpansionTransfer), the algebra of the
weight (G_g)^{1/2} and of the weighted operators A ⊗ (G_g)^{1/2}, the projective expansion of
the lem:generalize-b deviation into the line-collision residual
(generalizeBDeviationAtPolynomial_eq_collisionResidual), and the identities between the
weighted squared-norm deviations and the point-conditioned variances.
opTensor is strategy.state.opTensor, leftTensor (ι₂ := ι) is strategy.state.L, ᴴ is
star, and the vendored second state ψbi is a vector state V : VecState K, as in
Defs/Families.lean.
The weighted state. The vendored point-conditioned variances evaluate the family
u ↦ A^u_{g(u)} ⊗ 1 on the weighted state (1 ⊗ √G_g) ρ (1 ⊗ √G_g)ᴴ; the ported ones are the
variances of the weighted family u ↦ A^u_{g(u)} ⊗ (G_g)^{1/2} on the strategy's own state
(Defs/Operators.lean, module docstring). So the vendored bridge between the two,
weightedPolynomialState_ev_leftTensor, is not needed, and its consumer
weightedNormDeviation_eq_pointConditionedDifferenceAvg is translated with the variance summand
of the weighted family on its right side, where it holds by definition; the two identities with
the variances and the local-to-global transfer become one-line consequences, and
pointConditionedExpansionTransfer is ExpansionHypercubeGraph.localToGlobal itself.
Not ported #
globalVarianceOfPoints_bound_of_local: classical, imported.weightedPolynomialState_ev_leftTensor: the weighted state(1 ⊗ √G_g) ρ (1 ⊗ √G_g)ᴴis not ported (a vector state has no density, and the weighted vector is not normalized); the point-conditioned variances are those of the weighted family on the strategy's state, so no move between the two states is needed.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/expansion.texblueprint/src/chapter/ch06_variance.tex
Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.
Algebraic identities and variance reductions #
lem:local-to-global for the point-conditioned variances at a fixed polynomial.
Algebraic norm/variance reductions #
The weight (G_g)^{1/2} is self-adjoint.
The weight (G_g)^{1/2} squares to 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.
The square of the weighted point-conditioned difference is the tensor of the squared point-operator difference with the polynomial outcome.
On an incident line question, the left lem:generalize-b event is the right event plus the
residual line-collision event.
On an incident line question, the squared difference of the two lem:generalize-b events is
the residual line-collision event, a projection.
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.
The averaged weighted squared differences are the averaged variance summands of the weighted
family u ↦ A^u_{g(u)} ⊗ (G_g)^{1/2}. The vendored right side is the variance summand of the
family u ↦ A^u_{g(u)} ⊗ 1 on the weighted state; here the weight sits in the family (module
docstring), and the identity holds by definition.
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.
The independent-points weighted squared-difference expression is exactly twice the global variance of the point-conditioned family on the weighted state.
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.
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.