Section 11 commutativity: transport via evaluation specialization #
Postprocessing identities for leftPlacedOpFamily of bilinear products, used
to transport bounds across evaluation specializations of the full-slice
commutation argument.
References #
references/ldt-paper/commutativity-G.texblueprint/src/chapter/ch08_commutativity.tex
theorem
MIPStarRE.LDT.Commutativity.evaluationSpecialization_sddErrorOp_eq
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
:
sddErrorOp strategy.state (uniformDistribution (EvaluatedSliceQuestion params))
(evaluatedFromFullSliceProductLeft params strategy family)
(evaluatedFromFullSliceProductRight params strategy family) = sddErrorOp strategy.state (uniformDistribution (EvaluatedSliceQuestion params))
(evaluatedSliceProductLeft params strategy family) (evaluatedSliceProductRight params strategy family)
The evaluated-from-full-slice SDD error equals the evaluated-slice SDD error, because the postprocessed product equals the product of postprocessed submeasurements at every question-outcome pair.
theorem
MIPStarRE.LDT.Commutativity.evaluatedSliceCommutation_of_evaluationSpecialization
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
(δ : Error)
(hEval :
SDDOpRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params))
(evaluatedFromFullSliceProductLeft params strategy family)
(evaluatedFromFullSliceProductRight params strategy family) δ)
:
SDDOpRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params))
(evaluatedSliceProductLeft params strategy family) (evaluatedSliceProductRight params strategy family) δ
Restate the evaluated-from-full-slice commutation bound as a bound for the evaluated-slice product families, using the pointwise postprocessing identities.