Switch-sandwich main: left-to-middle transfer #
The left-to-middle transfer estimate used in prop:switch-sandwich, bounding
the gap between the left and middle expressions via the Cauchy–Schwarz-based
gap bounds.
References #
references/ldt-paper/preliminaries.tex,prop:switch-sandwichblueprint/src/chapter/ch03_preliminaries.tex
theorem
MIPStarRE.LDT.Preliminaries.switchSandwich_leftTransfer
{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 δ →
|leftSandwichExpectation ψ 𝒟 A B - middleSandwichExpectation ψ 𝒟 A B| ≤ 2 * √δ
Left-to-middle transfer estimate used in the switch-sandwich theorem.