Preliminary comparison theorems: distance bounds #

Triangle-inequality style bounds for SDDRel and SDDOpRel: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/DistanceBounds.lean in the port of planning/c6b-plan.md (milestone M0, section "Port conventions").

As in Co/Preliminaries/Defs.lean, the declarations live in MIPRE.LIDT.Co.Preliminaries and take the state as an ordinary explicit argument in place of the vendored state ψ. The vendored statements are about a state on a single space, so the state is a vector state V : VecState K (Co/Basic/QuantumState.lean; a symmetric model S is accepted through its coercion) and the families are joint, with operators in K →L[ℂ] K.

The pointwise core of questionCabApproxDelta is the repository's fact:add-a-proj, MIPRE.StateModel.sum_snorm_sq_mul_le_of_le (MIPRE/Foundations/StateModel.lean) on V.toStateModel, through VecState.qSDDCore_eq_sum_snorm_sq of Co/Test/Defs.lean; the vendored proof expands the sandwich and uses conjTranspose_mul_mono. The triangle inequalities questionSDD_triangle, questionSDD_triangle_three and questionSDDOp_triangle are, term by term, MIPRE.StateModel.sum_snorm_sq_triangle and sum_snorm_sq_triangle3, through VecState.ev_diff_triangle and ev_diff_triangle_three (Co/Basic/OperatorExpectations.lean).

Not ported #

sddOpRel_leftPlaced_of_ev_eq: its hypothesis is a second state φ on the first tensor factor with the marginal identity ev ψ (leftTensor X) = ev φ X, a reduced density matrix. The model has no local state: the restriction of S.ev to S.L is a state of 𝔓, not a vector state on a space where the local operators act, and a family placed by S.L is measured against S itself (V : VecState K with V := S), so the statement has no counterpart; its only vendored consumer is the matrix orthonormalization route of MakingMeasurementsProjective/LocalityPreservingRepair.lean, which the port replaces by the dimension-free orthonormalization (planning/c6b-plan.md, M8).

Infrastructure: triangle inequality for `SDDRel` #

source

theorem MIPRE.LIDT.Co.Preliminaries.questionSDD_triangle {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (A B C : SubMeas Outcome (K →L[ℂ ] K)) :

V.qSDD A C ≤ 2 * (V.qSDD A B + V.qSDD B C)

Atomic mathematical fact: the parallelogram-style inequality for qSDD.

source

theorem MIPRE.LIDT.Co.Preliminaries.questionSDD_triangle_three {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (A B C D : SubMeas Outcome (K →L[ℂ ] K)) :

V.qSDD A D ≤ 3 * (V.qSDD A B + V.qSDD B C + V.qSDD C D)

Atomic mathematical fact: the three-step triangle inequality for qSDD.

This is the k = 3 instance of prop:triangle-inequality-for-approx_delta, with the sharp paper constant 3 * (δ₁ + δ₂ + δ₃).

source

theorem MIPRE.LIDT.Co.Preliminaries.stateDependentDistanceRel_triangle {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {Outcome : Type u_3} [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 * (δ₁ + δ₂))

Triangle inequality for state-dependent distance.

source

theorem MIPRE.LIDT.Co.Preliminaries.stateDependentDistanceRel_triangle_three {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B C D : IdxSubMeas Question Outcome (K →L[ℂ ] K)) (δ₁ δ₂ δ₃ : ℝ) :

V.SDDRel 𝒟 A B δ₁ → V.SDDRel 𝒟 B C δ₂ → V.SDDRel 𝒟 C D δ₃ → V.SDDRel 𝒟 A D (3 * (δ₁ + δ₂ + δ₃))

Three-step triangle inequality for state-dependent distance.

source

theorem MIPRE.LIDT.Co.Preliminaries.stateDependentDistanceRel_mono {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxSubMeas Question Outcome (K →L[ℂ ] K)) (δ δ' : ℝ) (hle : δ ≤ δ') :

V.SDDRel 𝒟 A B δ → V.SDDRel 𝒟 A B δ'

Monotonicity: if SDDRel holds for δ, it holds for any δ' ≥ δ.

source

theorem MIPRE.LIDT.Co.Preliminaries.questionCabApproxDelta {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} {Aux : Type u_3} [Fintype Outcome] [Fintype Aux] (V : VecState K) (A B : OpFamily Outcome (K →L[ℂ ] K)) (C : Outcome → Aux → K →L[ℂ ] K) (hC : ∀ (a : Outcome), ∑ b : Aux, star (C a b) * C a b ≤ 1) :

V.qSDDOp { outcome := fun (ab : Outcome × Aux) => C ab.1 ab.2 * A.outcome ab.1, total := ∑ ab : Outcome × Aux, C ab.1 ab.2 * A.outcome ab.1 } { outcome := fun (ab : Outcome × Aux) => C ab.1 ab.2 * B.outcome ab.1, total := ∑ ab : Outcome × Aux, C ab.1 ab.2 * B.outcome ab.1 } ≤ V.qSDDOp A B

Left multiplication by a column contraction C a (∑_b (C a b)* C a b ≤ 1) does not increase the operator-family squared distance.

source

theorem MIPRE.LIDT.Co.Preliminaries.cabApproxDelta_raw {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {Outcome : Type u_3} {Aux : Type u_4} [Fintype Outcome] [Fintype Aux] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxOpFamily Question Outcome (K →L[ℂ ] K)) (C : Question → Outcome → Aux → K →L[ℂ ] K) (δ : ℝ) :

V.SDDOpRel 𝒟 A B δ → (∀ (q : Question) (a : Outcome), ∑ b : Aux, star (C q a b) * C q a b ≤ 1) → V.SDDOpRel 𝒟 (fun (q : Question) => { outcome := fun (ab : Outcome × Aux) => C q ab.1 ab.2 * (A q).outcome ab.1, total := ∑ ab : Outcome × Aux, C q ab.1 ab.2 * (A q).outcome ab.1 }) (fun (q : Question) => { outcome := fun (ab : Outcome × Aux) => C q ab.1 ab.2 * (B q).outcome ab.1, total := ∑ ab : Outcome × Aux, C q ab.1 ab.2 * (B q).outcome ab.1 }) δ

prop:cab-approx-delta.