Self-consistency: data processing #
prop:self-consistency-implies-data-processing: self-consistency implies that
postprocessing a measurement cannot substantially decrease consistency.
References #
references/ldt-paper/preliminaries.texblueprint/src/chapter/ch03_preliminaries.tex
theorem
MIPStarRE.LDT.Preliminaries.selfConsistencyImpliesDataProcessing
{Question : Type u_1}
{α : Type u_2}
{β : Type u_3}
{ι : Type u_4}
[Fintype ι]
[DecidableEq ι]
[Fintype α]
[Fintype β]
(ψ : QuantumState (ι × ι))
(hperm : PermInvState ψ)
(hψ : ψ.IsNormalized)
(𝒟 : Distribution Question)
(h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1)
(A : IdxSubMeas Question α ι)
(P : IdxProjSubMeas Question α ι)
(δ ε : Error)
(f : Question → α → β)
:
BipartiteSSCRel ψ 𝒟 A δ →
SDDRel ψ 𝒟 P.toIdxSubMeas.liftLeft A.liftLeft ε →
SDDRel ψ 𝒟 (IdxSubMeas.liftLeft fun (q : Question) => postprocess (P q).toSubMeas (f q))
(IdxSubMeas.liftLeft fun (q : Question) => postprocess (A q) (f q)) (8 * δ + 8 * √ε)
prop:self-consistency-implies-data-processing.
A projective approximation to a strongly self-consistent family remains close
after postprocessing on the left register. The proof combines the wrong-side
estimate, self-consistency after evaluation, and the SDDRel triangle
inequality.