Option Completion in the Orthonormalization Argument

This file contains the auxiliary algebra used when the orthonormalization theorem is applied to the completion of a submeasurement by a fresh failure outcome. The results compare the completed measurement with the restriction obtained by discarding this fresh outcome.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.Orthonormalization.Completion.optionCompletion_bipartiteSSCRel {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] [DecidableEq Outcome] (ψ : QuantumState (ι × ι)) (hperm : PermInvState ψ) (hψ : ψ.IsNormalized) (A : SubMeas Outcome ι) (ζ : Error) : BipartiteSSCRel ψ (uniformDistribution Unit) (constSubMeasFamily A) ζ → BipartiteSSCRel ψ (uniformDistribution Unit) (constSubMeasFamily (optionCompletion A).toSubMeas) (2 * ζ)

Completing a submeasurement by a fresh failure outcome preserves bipartite strong self-consistency up to the paper's factor 2: the original diagonal gap controls the original outcomes, and the same gap controls the residual none outcome after applying permutation invariance.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.Orthonormalization.Completion.qSDD_liftLeft_restrictSomeProjSubMeas_le {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] [DecidableEq Outcome] (ψ : QuantumState (ι × ι)) (A : SubMeas Outcome ι) (P : ProjSubMeas (Option Outcome) ι) : qSDD ψ A.liftLeft (restrictSomeProjSubMeas P).liftLeft ≤ qSDD ψ (optionCompletion A).liftLeft P.liftLeft

Discarding the extra none outcome from the option-completed measurement can only decrease the qSDD sum: one simply drops a nonnegative summand.