Triangle inequalities for state-dependent distance: simultaneous equivalence

The simultaneous-equivalence triangle inequalities and the approximate-delta triangle estimate: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/Triangles/SimEq.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

The consistency statements take the symmetric model S : SymModel 𝔓 K as an ordinary explicit argument in place of the vendored state, with local measurements in 𝔓, and drop the vendored normalization hypothesis hψ : ψ.IsNormalized; triangleInequalityForApproxDelta is about a single state and takes a vector state V : VecState K. In the symmetric model both tensor factors carry 𝔓, so simeqTriangleInequality_heterogeneous has the type of simeqTriangleInequality up to the order of its arguments, and is that theorem.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/preliminaries.tex

theorem MIPRE.LIDT.Co.Preliminaries.simeqTriangleInequality {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B C D : IdxMeas Question Outcome 𝔓) (ε δ γ : ℝ) (hAB : S.ConsRel 𝒟 A.toIdxSubMeas B.toIdxSubMeas ε) (hCB : S.ConsRel 𝒟 C.toIdxSubMeas B.toIdxSubMeas δ) (hCD : S.ConsRel 𝒟 C.toIdxSubMeas D.toIdxSubMeas γ) : S.ConsRel 𝒟 A.toIdxSubMeas D.toIdxSubMeas (ε + 2 * √(δ + γ))

prop:simeq-triangle-inequality.

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

theorem MIPRE.LIDT.Co.Preliminaries.simeqTriangleInequality_heterogeneous {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A C B D : IdxMeas Question Outcome 𝔓) (ε δ γ : ℝ) (hAB : S.ConsRel 𝒟 A.toIdxSubMeas B.toIdxSubMeas ε) (hCB : S.ConsRel 𝒟 C.toIdxSubMeas B.toIdxSubMeas δ) (hCD : S.ConsRel 𝒟 C.toIdxSubMeas D.toIdxSubMeas γ) : S.ConsRel 𝒟 A.toIdxSubMeas D.toIdxSubMeas (ε + 2 * √(δ + γ))

Heterogeneous form of prop:simeq-triangle-inequality.

The vendored statement is the triangle step for a general bipartite strategy, the first and third measurements acting on Alice's space and the second and fourth on Bob's. In the symmetric model both spaces carry 𝔓, and this is simeqTriangleInequality.

theorem MIPRE.LIDT.Co.Preliminaries.triangleInequalityForApproxDelta {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B C : IdxSubMeas Question Outcome (K →L[ℂ] K)) (δ₁ δ₂ : ℝ) : V.SDDRel 𝒟 A B δ₁ → V.SDDRel 𝒟 B C δ₂ → V.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.