Zero-family bounds on the full-slice product #
Pointwise qSDDOp bounds and averaged SDDOpRel bounds for the
ordered fullSliceProductLeft and reversed fullSliceProductRight
factors against the zero family, each at most 1.
References #
references/ldt-paper/commutativity-G.texblueprint/src/chapter/ch08_commutativity.tex
theorem
MIPStarRE.LDT.Commutativity.fullSliceProductLeft_to_zero_le_one
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
(hnorm : strategy.state.IsNormalized)
:
SDDOpRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params))
(fun (q : EvaluatedSliceQuestion params) =>
fullSliceProductLeft params strategy family (fullSliceQuestionOfEvaluatedSlice params q))
(fun (x : EvaluatedSliceQuestion params) => zeroFullSliceOpFamily params) 1
Averaging the ordered full-slice product against zero costs at most 1.
theorem
MIPStarRE.LDT.Commutativity.zero_to_fullSliceProductRight_le_one
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
(hnorm : strategy.state.IsNormalized)
:
SDDOpRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params))
(fun (x : EvaluatedSliceQuestion params) => zeroFullSliceOpFamily params)
(fun (q : EvaluatedSliceQuestion params) =>
fullSliceProductRight params strategy family (fullSliceQuestionOfEvaluatedSlice params q))
1
Averaging zero against the reversed full-slice product costs at most 1.