Full-slice averages and index equivalences #
Zero-family definition, shared average-reindexing helpers, and averaged scalar and tensor
quantities for the full-slice outcome space: the counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Transport/FullSlice/Averages.lean in the
port of planning/c6b-plan.md (milestone M7, section "Port conventions").
The averages are real expectations strategy.state.ev β¦ on the symmetric model of a strategy
strategy : SymStrat params.next π K, the vendored leftTensor (ΞΉβ := ΞΉ) and
rightTensor (ΞΉβ := ΞΉ) being strategy.state.L and strategy.state.R. The tensor-form
averages are internal to the scalar/tensor comparison recorded upstream in
docs/decisions/713-scalar-tensor-decision.md; downstream code should use the scalar API.
zeroFullSliceOpFamily is generic over any type with a zero, so a dependant names the operator
type, zeroFullSliceOpFamily (R := K βL[β] K) params, where the vendored text has
(ΞΉ := ΞΉ). The two swap identities of fullSliceCommutation_avg_swap_terms are one private
reindexing helper applied twice, in place of the vendored product-average calculation. The
data-reindexing equivalences and the point-marginal lemma are classical and imported from the
vendored file, which this file imports alongside its mirrored imports.
Not ported #
xEvaluatedQuestionPointNextEquiv: classical, imported.avgOver_xEvaluatedQuestion_to_pointNext: classical, imported.evaluatedSliceQuestionYDataEquiv: classical, imported.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/commutativity-G.texblueprint/src/chapter/ch08_commutativity.tex
Swapping the full-slice question and outcome identifies the averaged
BAB/ABA terms and the averaged BABA/ABAB terms.
The zero operator family on the full-slice outcome space.
Equations
- MIPRE.LIDT.Co.Commutativity.zeroFullSliceOpFamily params = { outcome := fun (x : MIPStarRE.LDT.Commutativity.FullSliceOutcome params) => 0, total := 0 }
Instances For
Full-slice ABA scalar average: E_{x,y} β_{g,h} β¨Ο| G^x_g G^y_h G^x_g β I |Οβ©.
Full-polynomial analog of the evaluated evaluatedSliceABATerm; obtained from it by replacing
the evaluated outcomes a,b with polynomial outcomes g,h summed over FullSliceOutcome.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Full-slice ABAB scalar average:
E_{x,y} β_{g,h} β¨Ο| G^x_g G^y_h G^x_g G^y_h β I |Οβ©.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluated-slice ABA scalar average:
E_{u,v,x,y} β_{a,b} β¨Ο| G^x_[g(u)=a] G^y_[h(v)=b] G^x_[g(u)=a] β I |Οβ©.
Averaged analog of evaluatedSliceABATerm over the evaluated-slice question.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluated-slice ABAB scalar average:
E_{u,v,x,y} β_{a,b} β¨Ο| G^x_[g(u)=a] G^y_[h(v)=b] G^x_[g(u)=a] G^y_[h(v)=b] β I |Οβ©.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Full-slice BAB β A tensor average (paper eq:gcom4, right-hand side):
E_{x,y} β_{g,h} β¨Ο| G^y_h G^x_g G^y_h β G^x_g |Οβ©.
This is the manifestly positive tensor-form partner of fullSliceABAAvg used by the
marginalization step: each summand factors as V^* V with V = (G^x_g G^y_h) β β(G^x_g), so
the outer absolute value drops and the SchwartzβZippel collision bound applies per outcome.
This tensor-form average is internal to the scalar API (upstream decision #713).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Full-slice ABA β B tensor average (y-side analogue):
E_{x,y} β_{g,h} β¨Ο| G^x_g G^y_h G^x_g β G^y_h |Οβ©.
Naming convention (consistent with the sibling fullSliceBABAtensorAvg for BAB β A): the
four-letter operator string ABAB decomposes as left register ABA followed by right register
B. This is not the same operator as the scalar fullSliceABABAvg, whose left register is
the full quartic G^x_g G^y_h G^x_g G^y_h; the tensorAvg suffix marks the tensor split.
The manifestly positive tensor-form partner of fullSliceABABAvg, reached from it by
closenessOfIP (moving the trailing G^y_h factor from the left register to the right). Each
summand factors as V^* V with V = (G^y_h G^x_g) β β(G^y_h). Internal per upstream decision
#713.
The evaluated-side analogue is evaluatedSliceABABtensorAvg below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluated-slice ABA β B tensor average (evaluated-side analogue of
fullSliceABABtensorAvg):
E_{u,v,x,y} β_{a,b} β¨Ο| G^x_[g(u)=a] G^y_[h(v)=b] G^x_[g(u)=a] β G^y_[h(v)=b] |Οβ©.
This is the second tensor-form endpoint of the paper's commutativity-G.tex (lines 356β360).
The scalar-to-tensor comparison evaluatedSliceABAB_scalar_to_ABABtensor reaches it by moving
the trailing G^y_[h(v)=b] factor from the left register to the right register.
The shared tensor endpoint is defined here so the evaluated-side transport lemmas can use the same notation as the full-slice transport lemmas.
Equations
- One or more equations did not get rendered due to their size.
Instances For
X-evaluated BAB β A tensor average.
This is the intermediate obtained from fullSliceBABAtensorAvg after postprocessing only the
first/full-x polynomial outcome by a sampled point u : Point params; the second/y
polynomial outcome remains full. The x-side tensor marginalization lemma identifies its
difference from the full tensor average with fullSliceBABAxCollisionFactored.
Equations
- One or more equations did not get rendered due to their size.
Instances For
X-evaluated, y-full ABAB scalar average.
This is the scalar endpoint in the display from eq:evaluate-gcom-at-points to
eq:don't-understand-the-numbering-system: the x polynomial outcome has been postprocessed
at u, but the second closenessOfIP move has not yet transferred the trailing G^y_h to the
right register.
Equations
- One or more equations did not get rendered due to their size.
Instances For
X-evaluated, y-full ABA β B tensor average.
This is the y-side intermediate in the paper's eq:evaluate-gcom-at-points-part-dos: the
first/x family has already been postprocessed at u, while the second/y family still
ranges over full polynomial outcomes. The y-side tensor marginalization lemma compares this to
evaluatedSliceABABtensorAvg.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reindex xEvaluatedSliceBABAtensorAvg into the mixed (u,x,y) data order.