Preliminary comparison theorems: completion and chain rules

Completion lemmas and final chain inequalities from the preliminaries chapter.

theorem MIPStarRE.LDT.Preliminaries.completingToMeasurement {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (hperm : PermInvState ψ) (hψ : ψ.IsNormalized) (A : Measurement Outcome ι) (B : SubMeas Outcome ι) (a0 : Outcome) (δ ζ : Error) : BipartiteSSCRel ψ (uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) ζ → SDDRel ψ (uniformDistribution Unit) (constSubMeasFamily A.liftLeft) (constSubMeasFamily B.liftLeft) δ → ∃ (C : Measurement Outcome ι), C = completeAtOutcome B a0 ∧ CompletingToMeasStmt ψ A B C a0 δ ζ

prop:completing-to-measurement.

The paper's hypothesis involves permutation-invariance; the bipartite completion proof needs PermInvState to bridge BipartiteSSCRel to the local SSCRel used in the algebraic completion bound.

theorem MIPStarRE.LDT.Preliminaries.sddOpRel_triangle {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B C : IdxOpFamily Question Outcome ι) (δ₁ δ₂ : Error) : SDDOpRel ψ 𝒟 A B δ₁ → SDDOpRel ψ 𝒟 B C δ₂ → SDDOpRel ψ 𝒟 A C (2 * (δ₁ + δ₂))

Triangle inequality for state-dependent operator distance.

theorem MIPStarRE.LDT.Preliminaries.sddOpRel_mono {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B : IdxOpFamily Question Outcome ι) (δ δ' : Error) : SDDOpRel ψ 𝒟 A B δ → δ ≤ δ' → SDDOpRel ψ 𝒟 A B δ'

Monotonicity for SDDOpRel.

theorem MIPStarRE.LDT.Preliminaries.sddOpRel_chain {Question : Type u_1} {Outcome : Type u_2} {ι' : Type u_3} [Fintype ι'] [DecidableEq ι'] [Fintype Outcome] (ψ : QuantumState ι') (𝒟 : Distribution Question) (n : ℕ) (families : Fin (n + 1) → IdxOpFamily Question Outcome ι') (errors : Fin n → Error) (hsteps : ∀ (i : Fin n), SDDOpRel ψ 𝒟 (families i.castSucc) (families i.succ) (errors i)) : SDDOpRel ψ 𝒟 (families 0) (families (Fin.last n)) (↑n * ∑ i : Fin n, errors i)

n-step SDDOpRel chain lemma via vector Cauchy-Schwarz.

Given n consecutive SDDOpRel bounds, the endpoints satisfy an SDDOpRel bound with error n * (∑ individual errors). This improves on naive triangle-inequality chaining, which would give exponential blowup.

Paper reference: prop:triangle-inequality-for-approx_delta in references/ldt-paper/preliminaries.tex.

Proof sketch: telescoping + ‖∑ dᵢ|ψ⟩‖² ≤ n · ∑ ‖dᵢ|ψ⟩‖² (vector Cauchy-Schwarz / norm triangle inequality).