Switch-sandwich main: middle-to-right transfer #
The middle-to-right transfer estimate used in prop:switch-sandwich.
References #
references/ldt-paper/preliminaries.tex,prop:switch-sandwichblueprint/src/chapter/ch03_preliminaries.tex
theorem
MIPStarRE.LDT.Preliminaries.switchSandwich_rightTransfer
{Question : Type u_1}
{Outcome : Type u_2}
{ι : Type u_3}
[Fintype ι]
[DecidableEq ι]
[Fintype Outcome]
(ψ : QuantumState (ι × ι))
(𝒟 : Distribution Question)
(hψ : ψ.IsNormalized)
(h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1)
(A : IdxProjSubMeas Question Outcome ι)
(B : Quantum.Op ι)
(hB : OpBounded01 B)
(δ : Error)
:
BipartiteSDDRel ψ 𝒟 A.toIdxSubMeas A.toIdxSubMeas δ →
|middleSandwichExpectation ψ 𝒟 A B - rightSandwichExpectation ψ 𝒟 A B| ≤ √δ
Middle-to-right transfer estimate used in the switch-sandwich theorem.