Section 8 global variance: operator families #
The counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/GlobalVariance/Defs/Families.lean in
the port of planning/c6b-plan.md (milestone M6, section "Port conventions"): positivity and
normalization of the weighted operators A ⊗ (G_g)^{1/2}, the aggregated one-outcome families
of lem:generalize-b, lem:local-variance-of-points and lem:global-variance-of-points, and
the squared-norm deviations those lemmas control.
The weighted operators are joint operators S.L A * S.R (G_g)^{1/2} of a symmetric model S,
so the two lemmas that bound them for an arbitrary local A take the model as an explicit first
argument (weightedPolynomialOperator_pos S params G g hA), as M1's and M3's placement helpers
do. The positivity and the bound ≤ 1 are the keystone's SymModel.opTensor_nonneg and
SymModel.opTensor_le_one; the bound (G_g)^{1/2} ≤ 1 is operator monotonicity of CFC.sqrt
(CFC.sqrt_le_sqrt) in place of the vendored spectral argument.
The deviations evaluate joint operators of the strategy's model against a second state ψbi on
the same space; they use only that state, so ψbi is a vector state V : VecState K (section
"Same-space and bipartite quantities" of the plan), and a caller passes the strategy's model
strategy.state, which coerces to it.
The four error terms at the end of the vendored file (generalizeBError and the three displayed
errors of lem:local-variance-of-points and lem:global-variance-of-points) are real-valued
functions of the parameters alone: this file imports the vendored file for them, and the ported
files of GlobalVariance name them through explicit open MIPStarRE.LDT.GlobalVariance (…)
lists.
Not ported #
generalizeBError: classical, imported.localVarianceTransportChainError: classical, imported.localVarianceOfPointsError: classical, imported.globalVarianceOfPointsError: classical, imported.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/expansion.texblueprint/src/chapter/ch06_variance.tex
CFC.sqrt (G.outcome g) ≤ 1 when G is a submeasurement: CFC.sqrt is operator monotone
and CFC.sqrt 1 = 1.
A weighted operator A ⊗ (G_g)^{1/2} of a positive local operator A is positive.
A weighted operator A ⊗ (G_g)^{1/2} of an effect 0 ≤ A ≤ 1 is at most 1.
The weighted point operator A^u_{g(u)} ⊗ (G_g)^{1/2} is positive.
The weighted point operator A^u_{g(u)} ⊗ (G_g)^{1/2} is at most 1.
The squared norm expression controlled by lem:generalize-b for a fixed g,
evaluated on the vector state V (the vendored bipartite state ψbi).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The polynomial-averaged deviation controlled by lem:generalize-b.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The line-collision residual obtained after expanding the projective line
measurement in lem:generalize-b and moving the polynomial weight from
(G_g)^{1/2} to G_g. The remaining analytic step is to bound this
quantity by Schwartz--Zippel and the submeasurement property of G.
Paper origin: references/ldt-paper/expansion.tex:273-288
(\label{lem:generalize-b}).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Uniform line/parameter seed expansion of the lem:generalize-b collision residual.
This is the paper's expansion.tex, lines 286--288, after replacing an
incident line question (ℓ,u) by a line ℓ and affine parameter t with
u = ℓ(t), but before commuting the finite average over t past the finite
sum over line answers f. The vendored file proves the equality from the original collision
residual to this seed expansion in generalizeBCollisionResidual_eq_seedCollisionExpansion.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Explicit line/parameter expansion of the lem:generalize-b collision residual.
This is the commuted finite-sum form of generalizeBSeedCollisionExpansion: for
fixed ℓ and f, the coefficient is the fraction of parameters where the line
answer f both collides with g|_ℓ at t and is not equal to g|_ℓ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Aggregated family for the left-hand side of lem:generalize-b: the uniform polynomial
average of B^ℓ_{[f(u)=g(u)]} ⊗ (G_g)^{1/2}, as a one-outcome family of joint operators.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Aggregated family for the right-hand side of lem:generalize-b: the uniform polynomial
average of B^ℓ_{[f = g|_ℓ]} ⊗ (G_g)^{1/2}, as a one-outcome family of joint operators.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Aggregated family for A^u_[g(u)] ⊗ (G_g)^{1/2}, the uniform polynomial average at the
first point of a pair, as a one-outcome family of joint operators.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Aggregated family for A^v_[g(v)] ⊗ (G_g)^{1/2}, the uniform polynomial average at the
second point of a pair, as a one-outcome family of joint operators.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The same weighted operator on the first independently sampled point.
Equations
- MIPRE.LIDT.Co.GlobalVariance.globalVarianceLeftFamily params strategy G = MIPRE.LIDT.Co.GlobalVariance.localVarianceLeftFamily params strategy G
Instances For
The same weighted operator on the second independently sampled point.
Equations
- MIPRE.LIDT.Co.GlobalVariance.globalVarianceRightFamily params strategy G = MIPRE.LIDT.Co.GlobalVariance.localVarianceRightFamily params strategy G
Instances For
The edgewise squared norm expression in lem:local-variance-of-points,
evaluated on the vector state V (the vendored bipartite state ψbi).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The independently sampled squared norm expression in lem:global-variance-of-points,
evaluated on the vector state V (the vendored bipartite state ψbi).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The polynomial-averaged local squared norm expression.
Equations
- One or more equations did not get rendered due to their size.