Triangle Inequalities for State-Dependent Distance: Simultaneous Equivalence

This module contains the simultaneous-equivalence triangle inequalities and the final approximate-delta triangle estimate.

theorem MIPStarRE.LDT.Preliminaries.simeqTriangleInequality {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 B C D : IdxMeas Question Outcome ι) (ε δ γ : Error) (hAB : ConsRel ψ 𝒟 A.toIdxSubMeas B.toIdxSubMeas ε) (hCB : ConsRel ψ 𝒟 C.toIdxSubMeas B.toIdxSubMeas δ) (hCD : ConsRel ψ 𝒟 C.toIdxSubMeas D.toIdxSubMeas γ) : ConsRel ψ 𝒟 A.toIdxSubMeas D.toIdxSubMeas (ε + 2 * √(δ + γ))

prop:simeq-triangle-inequality.

Apply simeqToApprox to the two hypotheses through the middle measurement B, use the SDDRel triangle inequality to compare the induced right-side families, and finish with triangleSub. Quantitatively this gives ε + sqrt (4 * (δ + γ)) = ε + 2 * sqrt (δ + γ).

This is stated here with the exact paper-style API needed by downstream files.

theorem MIPStarRE.LDT.Preliminaries.simeqTriangleInequality_heterogeneous {Question : Type u_1} {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (𝒟 : Distribution Question) (hψ : ψ.IsNormalized) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A C : IdxMeas Question Outcome ιA) (B D : IdxMeas Question Outcome ιB) (ε δ γ : Error) (hAB : ConsRel ψ 𝒟 A.toIdxSubMeas B.toIdxSubMeas ε) (hCB : ConsRel ψ 𝒟 C.toIdxSubMeas B.toIdxSubMeas δ) (hCD : ConsRel ψ 𝒟 C.toIdxSubMeas D.toIdxSubMeas γ) : ConsRel ψ 𝒟 A.toIdxSubMeas D.toIdxSubMeas (ε + 2 * √(δ + γ))

Heterogeneous form of prop:simeq-triangle-inequality.

This is the paper's triangle step for a general bipartite strategy: the first and third measurements act on Alice's space, while the second and fourth act on Bob's space. No same-space identification or swap symmetry is used.

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

prop:triangle-inequality-for-approx_delta.

The paper states the iterated telescoping version for an arbitrary chain of approximations. The current API records the binary composition step used throughout the repository; the full iterated form follows by induction on the length of the chain.