Documentation

MIPStarRE.LDT.Commutativity.Transport.FullSlice.Machinery.Marginalization.Y

Full-slice y-marginalization endpoint #

This module contains the y-side evaluated tensor marginalization block for the ABAB full-slice tensor average. It imports the collision and postprocessing machinery from Machinery.Marginalization.Core and preserves the original public marginalization theorem.

References #

source
theorem MIPStarRE.LDT.Commutativity.fullSliceABAB_tensor_marginalize_y {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (hnorm : strategy.state.IsNormalized) :
|xEvaluatedFullSliceABABtensorAvg params strategy family - evaluatedSliceABABtensorAvg params strategy family| ≤ ↑params.m * ↑params.d / ↑params.q

Y-side tensor marginalization bound for the ABABtensor endpoint.

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.