Full-slice qSDDOp averaging identity #
Averaging identities expanding the full-slice qSDDOp and proving the scalar
commutation identity fullSliceCommutation_qSDDOp_avg_eq.
This scalar expansion is used by the full-slice transport theorems that compare
the quartic scalar averages appearing in commutativity-G.tex.
References #
references/ldt-paper/commutativity-G.texblueprint/src/chapter/ch08_commutativity.tex
theorem
MIPStarRE.LDT.Commutativity.fullSliceCommutation_qSDDOp_avg_eq
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
:
(sddErrorOp strategy.state (uniformDistribution (EvaluatedSliceQuestion params))
(fun (q : EvaluatedSliceQuestion params) =>
fullSliceProductLeft params strategy family (fullSliceQuestionOfEvaluatedSlice params q))
fun (q : EvaluatedSliceQuestion params) =>
fullSliceProductRight params strategy family (fullSliceQuestionOfEvaluatedSlice params q)) = 2 * (fullSliceABAAvg params strategy family - fullSliceABABAvg params strategy family)
Paper eq:gcomterms (commutativity-G.tex lines 286-290).
Full-slice analog of evaluatedSliceCommutation_qSDDOp_avg_eq (line 878): the
pulled-back sddErrorOp on the full-slice product equals 2·(ABAAvg − ABABAvg)
after using projectivity and the (x,g) ↔ (y,h) symmetry to collapse
BAB + ABA − BABA − ABAB into the two surviving scalar quartic terms.