Section 8 global variance: weighted operators and variance families #
The counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/GlobalVariance/Defs/Operators.lean in
the port of planning/c6b-plan.md (milestone M6, section "Port conventions"): the weight
(G_g)^{1/2} of a polynomial submeasurement, the point and axis-line event operators of
lem:local-variance-of-points and lem:generalize-b, their weighted bipartite forms
A ā (G_g)^{1/2}, and the point-conditioned local and global variances.
Local operators live in the local algebra š of a symmetric strategy
strategy : SymStrat params š K, and joint ones in K āL[ā] K: opTensor A B is
strategy.state.opTensor A B = S.L A * S.R B and rightTensor B is strategy.state.R B. The
square root (G_g)^{1/2} is CFC.sqrt in the Cā-algebra š, as the vendored file takes it in
the matrix algebra.
The weighted state. The vendored point-conditioned variances evaluate the left-placed family
u ā¦ A^u_{g(u)} ā 1 on the weighted state Ļ_g = W Ļ Wį““, W = 1 ā (G_g)^{1/2}, which is not
normalized (weightedPolynomialState). A vector state has no density, and the weighted vector
W ĪØ is not a unit vector, so it is not a VecState. Since ev_{WĻWį““}(X) = ev_Ļ(Wį““ X W) and
Wį““ (A_u - A_v)į““ (A_u - A_v) W = ((A_u - A_v) W)į““ ((A_u - A_v) W), with (A_u ā 1) W = A_u ā (G_g)^{1/2}, the vendored variance on Ļ_g is the variance on the strategy's own state of
the weighted family u ā¦ A^u_{g(u)} ā (G_g)^{1/2} (weightedPointConditionedOperatorAtPolynomial).
So pointConditionedLocalVarianceAtPolynomial and pointConditionedGlobalVarianceAtPolynomial
are defined that way, as the plan's note "For M6" prescribes (Co/ExpansionHypercubeGraph/ Theorems/Results.lean, module docstring), and localToGlobal applies to them unchanged.
Not ported #
weightedPolynomialState: a vector state has no density, and the weighted vector(1 ā (G_g)^{1/2}) ĪØis not normalized; the variances on it are the variances of the weighted family on the strategy's state (pointConditionedLocalVarianceAtPolynomial,pointConditionedGlobalVarianceAtPolynomial).
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/expansion.texblueprint/src/chapter/ch06_variance.tex
Weighted operators and variance families #
The operator (G_g)^{1/2} used throughout expansion.tex.
Uses CFC.sqrt (continuous functional calculus) to compute the square root of the positive
operator G.outcome g in the local algebra.
Equations
- MIPRE.LIDT.Co.GlobalVariance.polynomialWeightSqrtOperator params G g = CFC.sqrt (G.outcome g)
Instances For
The concrete operator A^u_{g(u)} for a fixed polynomial g.
Equations
- MIPRE.LIDT.Co.GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy g u = (strategy.pointMeasurement u).outcome (g.toFun u)
Instances For
The two-outcome point event selecting the answer g(u).
This is the submeasurement form of the point operator used in the first and last
steps of lem:local-variance-of-points (expansion.tex, lines 305 and 311).
Its some () outcome is exactly A^u_{g(u)}; the none outcome is the
complementary point-answer mass.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The selected outcome of pointConditionedEventSubMeasAtPolynomial is
A^u_{g(u)}.
The paper's weighted operator A^u_{g(u)} ā (G_g)^{1/2}, the joint operator
S.L (A^u_{g(u)}) * S.R ((G_g)^{1/2}) of the strategy's model.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The right-register intermediate I ā (G_g)^{1/2} A^u_{g(u)}
from the first and last self-consistency moves of
lem:local-variance-of-points (expansion.tex, lines 306 and 310).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The local variance of A(g) on the weighted state |Ļ_gā© = (I ā āG_g)|Ļā©.
The vendored definition evaluates the left-placed family u ā¦ A^u_{g(u)} ā 1 on the
unnormalized weighted state; here it is, equivalently, the local variance of the weighted family
u ā¦ A^u_{g(u)} ā (G_g)^{1/2} on the strategy's state (module docstring).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The global variance of A(g) on the weighted state |Ļ_gā© = (I ā āG_g)|Ļā©.
As for pointConditionedLocalVarianceAtPolynomial, it is the global variance of the weighted
family u ā¦ A^u_{g(u)} ā (G_g)^{1/2} on the strategy's state (module docstring).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The polynomial-averaged local variance of the conditioned points family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The polynomial-averaged global variance of the conditioned points family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Option Unit event submeasurement selecting axis-line answers that
match g(u) at the queried point u on the left side of lem:generalize-b.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Option Unit event submeasurement selecting axis-line answers that
match the restriction of g to ā on the right side of lem:generalize-b.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The residual projective Option Unit event from the proof of
lem:generalize-b: axis-line answers that collide with g at the sampled point
u, but are not the restricted polynomial g|_ā. After the
projective-measurement expansion, the squared difference is controlled by this
collision event.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The residual event above, forgetting projectivity to a submeasurement. Keeping
this definition as the toSubMeas of generalizeBCollisionEventProjMeasAtPolynomial
prevents the projective and submeasurement views from drifting apart.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The event operator for the residual line-collision event in lem:generalize-b.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The event operator B^ā_{[f(u)=g(u)]}: sum of axis-line measurement
outcomes f that evaluate to the same value as g at point u.
Equations
- MIPRE.LIDT.Co.GlobalVariance.generalizeBLeftOperatorAtPolynomial params strategy g qu = (MIPRE.LIDT.Co.GlobalVariance.generalizeBLeftEventSubMeasAtPolynomial params strategy g qu).outcome (some ())
Instances For
The event operator B^ā_{[f = g|_ā]}: sum of axis-line measurement
outcomes f that agree with g restricted to line ā.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The weighted left operator B^ā_{[f(u)=g(u)]} ā (G_g)^{1/2} in lem:generalize-b,
a joint operator of the strategy's model.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The weighted right operator B^ā_{[f = g|_ā]} ā (G_g)^{1/2} in lem:generalize-b,
a joint operator of the strategy's model.
Equations
- One or more equations did not get rendered due to their size.