Section 11 commutativity: evaluated-slice averaged expansion #
Averaged evaluated-slice expansion of qSDDOp into the four projector terms
BAB + ABA - BABA - ABAB, used to reduce the commutation to per-projector
estimates.
References #
references/ldt-paper/commutativity-G.texblueprint/src/chapter/ch08_commutativity.tex
theorem
MIPStarRE.LDT.Commutativity.evaluatedSliceCommutation_avg_swap_terms
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
:
((avgOver (uniformDistribution (EvaluatedSliceQuestion params)) fun (q : EvaluatedSliceQuestion params) =>
∑ ab : EvaluatedSliceOutcome params, evaluatedSliceBABTerm params strategy family q ab) = avgOver (uniformDistribution (EvaluatedSliceQuestion params)) fun (q : EvaluatedSliceQuestion params) =>
∑ ab : EvaluatedSliceOutcome params, evaluatedSliceABATerm params strategy family q ab) ∧ (avgOver (uniformDistribution (EvaluatedSliceQuestion params)) fun (q : EvaluatedSliceQuestion params) =>
∑ ab : EvaluatedSliceOutcome params, evaluatedSliceBABATerm params strategy family q ab) = avgOver (uniformDistribution (EvaluatedSliceQuestion params)) fun (q : EvaluatedSliceQuestion params) =>
∑ ab : EvaluatedSliceOutcome params, evaluatedSliceABABTerm params strategy family q ab
Swapping the evaluated question and outcome identifies the averaged
BAB/ABA terms and the averaged BABA/ABAB terms.
theorem
MIPStarRE.LDT.Commutativity.evaluatedSliceCommutation_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))
(evaluatedSliceProductLeft params strategy family) (evaluatedSliceProductRight params strategy family) = 2 * ((avgOver (uniformDistribution (EvaluatedSliceQuestion params)) fun (q : EvaluatedSliceQuestion params) =>
∑ ab : EvaluatedSliceOutcome params, evaluatedSliceABATerm params strategy family q ab) - avgOver (uniformDistribution (EvaluatedSliceQuestion params)) fun (q : EvaluatedSliceQuestion params) =>
∑ ab : EvaluatedSliceOutcome params, evaluatedSliceABABTerm params strategy family q ab)
Averaged evaluated-slice qSDDOp collapses to the paper's two scalar terms
after swapping the sampled questions and outcomes.