Section 11 commutativity: evaluated-slice pullback #
Pullback equivalence reindexing evaluated-slice questions into their truncated points and the underlying full-slice question, used to transport full-slice bounds.
References #
references/ldt-paper/commutativity-G.texblueprint/src/chapter/ch08_commutativity.tex
theorem
MIPStarRE.LDT.Commutativity.sddErrorOp_pullback_fullSliceQuestion_eq
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(ψ : QuantumState (ι × ι))
{Outcome : Type u_2}
[Fintype Outcome]
(A B : IdxOpFamily (FullSliceQuestion params) Outcome (ι × ι))
:
(sddErrorOp ψ (uniformDistribution (EvaluatedSliceQuestion params))
(fun (q : EvaluatedSliceQuestion params) => A (fullSliceQuestionOfEvaluatedSlice params q))
fun (q : EvaluatedSliceQuestion params) => B (fullSliceQuestionOfEvaluatedSlice params q)) = sddErrorOp ψ (uniformDistribution (FullSliceQuestion params)) A B
Pulling a family on FullSliceQuestion back along
fullSliceQuestionOfEvaluatedSlice preserves the averaged sddErrorOp.
theorem
MIPStarRE.LDT.Commutativity.sddOpRel_of_pullback_fullSliceQuestion
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(ψ : QuantumState (ι × ι))
{Outcome : Type u_2}
[Fintype Outcome]
(A B : IdxOpFamily (FullSliceQuestion params) Outcome (ι × ι))
(δ : Error)
:
SDDOpRel ψ (uniformDistribution (EvaluatedSliceQuestion params))
(fun (q : EvaluatedSliceQuestion params) => A (fullSliceQuestionOfEvaluatedSlice params q))
(fun (q : EvaluatedSliceQuestion params) => B (fullSliceQuestionOfEvaluatedSlice params q)) δ →
SDDOpRel ψ (uniformDistribution (FullSliceQuestion params)) A B δ
Any SDDOpRel bound proved after pulling back along
fullSliceQuestionOfEvaluatedSlice descends to FullSliceQuestion.