Switch-sandwich gap bounds: middle gap #
The middle gap estimate question_switchSandwich_middle_gap, bounding the
question-level middle gap of the switch-sandwich argument.
References #
references/ldt-paper/preliminaries.tex,prop:switch-sandwichblueprint/src/chapter/ch03_preliminaries.tex
theorem
MIPStarRE.LDT.Preliminaries.question_switchSandwich_middle_gap
{Outcome : Type u_1}
{ι : Type u_2}
[Fintype ι]
[DecidableEq ι]
[Fintype Outcome]
(ψ : QuantumState (ι × ι))
(hψ : ψ.IsNormalized)
(A : ProjSubMeas Outcome ι)
(B : Quantum.Op ι)
(hB : OpBounded01 B)
:
|∑ a : Outcome, ev ψ (leftTensor (A.outcome a) * leftTensor B * rightTensor (A.outcome a)) - ∑ a : Outcome, ev ψ (leftTensor B * rightTensor (A.outcome a))| ≤ √(qSDD ψ A.liftLeft A.liftRight)