Switch-sandwich main: completeness estimate #
prop:switch-sandwich assembled from the left and right transfer steps on a
normalized quantum state with a subprobability distribution.
References #
references/ldt-paper/preliminaries.tex,prop:switch-sandwichblueprint/src/chapter/ch03_preliminaries.tex
theorem
MIPStarRE.LDT.Preliminaries.switchSandwich
{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 δ → SwitchSandwichStmt ψ 𝒟 A B δ
prop:switch-sandwich.
The paper proof assumes a normalized state and a probability distribution
(weights summing to ≤ 1). These are now explicit hypotheses hψ and h𝒟.
theorem
MIPStarRE.LDT.Preliminaries.completenessTransferProjectiveP
{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 : IdxSubMeas Question Outcome ι)
(P : IdxProjSubMeas Question Outcome ι)
(ε : Error)
:
SDDRel ψ 𝒟 A P.toIdxSubMeas ε → CompTransferStmt ψ 𝒟 A P ε
prop:completeness-transfer-projective-P.
The paper proof uses a normalized state and a probability distribution.
These are now explicit hypotheses hψ and h𝒟.