Full-slice y-marginalization endpoint

The y-side evaluated tensor marginalization block for the ABAB full-slice tensor average: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Transport/FullSlice/Machinery/Marginalization/Y.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions"). It uses the collision and postprocessing machinery of Machinery.Marginalization.Core.

The terms and 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 vendored hypothesis hnorm : strategy.state.IsNormalized of fullSliceABAB_tensor_marginalize_y is a theorem of the model and is dropped. The reindexing equivalence evaluatedSliceQuestionYDataEquiv is classical and imported from the vendored Transport/FullSlice/Averages, through the mirrored imports.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/commutativity-G.tex
• blueprint/src/chapter/ch08_commutativity.tex

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedSliceABABtensorYDataTerm {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (r : (MIPStarRE.LDT.Point params × MIPStarRE.LDT.Commutativity.FullSliceQuestion params) × MIPStarRE.LDT.Point params) : ℝ

The evaluated ABA ⊗ B tensor summand block reindexed as ((u, (x, y)), v) and with the outcome sum in y-first order.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedSliceABABtensorYDataAvg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) : ℝ

The evaluated ABA ⊗ B tensor average reindexed as ((u, (x, y)), v) and with the outcome sum in y-first order.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSliceABABtensorYData_point {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (u : MIPStarRE.LDT.Point params) (x y : MIPStarRE.LDT.Fq params) (v : MIPStarRE.LDT.Point params) : ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, strategy.state.ev (strategy.state.L ((evaluatedSliceFirstFactor params family (MIPStarRE.LDT.appendPoint params u x, MIPStarRE.LDT.appendPoint params v y)).outcome ab.1 * (evaluatedSliceSecondFactor params family (MIPStarRE.LDT.appendPoint params u x, MIPStarRE.LDT.appendPoint params v y)).outcome ab.2 * (evaluatedSliceFirstFactor params family (MIPStarRE.LDT.appendPoint params u x, MIPStarRE.LDT.appendPoint params v y)).outcome ab.1) * strategy.state.R ((evaluatedSliceSecondFactor params family (MIPStarRE.LDT.appendPoint params u x, MIPStarRE.LDT.appendPoint params v y)).outcome ab.2)) = evaluatedSliceABABtensorYDataTerm params strategy family ((u, x, y), v)

Pointwise form of evaluatedSliceABABtensorAvg_eq_yData, after expanding the question reindexing equivalence.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSliceABABtensorAvg_eq_yData {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) : evaluatedSliceABABtensorAvg params strategy family = evaluatedSliceABABtensorYDataAvg params strategy family

Reindex the evaluated ABA ⊗ B tensor average by ((u, (x, y)), v) and write the outcome sum in the y-first order used by the generic postprocessing expansion.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSliceABABtensor_yEvaluation_eq_xFull_add_collision {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) : evaluatedSliceABABtensorAvg params strategy family = xEvaluatedFullSliceABABtensorAvg params strategy family + MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params × MIPStarRE.LDT.Commutativity.FullSliceQuestion params)) fun (ux : MIPStarRE.LDT.Point params × MIPStarRE.LDT.Commutativity.FullSliceQuestion params) => fullSliceABAByCollisionFactored params strategy family ux.1 ux.2

Exact y-side postprocessing identity: the fully evaluated ABA ⊗ B tensor average is the x-evaluated/y-full tensor average plus the y-collision residual.

theorem MIPRE.LIDT.Co.Commutativity.fullSliceABAB_tensor_marginalize_y {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) : |xEvaluatedFullSliceABABtensorAvg params strategy family - evaluatedSliceABABtensorAvg params strategy family| ≤ ↑params.m * ↑params.d / ↑params.q

Y-side tensor marginalization bound for the ABABtensor endpoint (the vendored hypothesis hnorm : strategy.state.IsNormalized is a theorem of the model).

This is the Lean-local tensor form of the Schwartz-Zippel step labelled eq:numbering-system-diff after eq:evaluate-gcom-at-points-part-dos in the proof of blueprint theorem thm:com-main.