Preliminary comparison theorems: distance bounds

Triangle-inequality style bounds for SDDRel and SDDOpRel.

Infrastructure: triangle inequality for SDDRel

theorem MIPStarRE.LDT.Preliminaries.questionSDD_triangle {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A B C : SubMeas Outcome ι) : qSDD ψ A C ≤ 2 * (qSDD ψ A B + qSDD ψ B C)

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

theorem MIPStarRE.LDT.Preliminaries.questionSDD_triangle_three {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A B C D : SubMeas Outcome ι) : qSDD ψ A D ≤ 3 * (qSDD ψ A B + qSDD ψ B C + 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 * (δ₁ + δ₂ + δ₃).

theorem MIPStarRE.LDT.Preliminaries.stateDependentDistanceRel_triangle {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 * (δ₁ + δ₂))

Triangle inequality for state-dependent distance.

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

Three-step triangle inequality for state-dependent distance.

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

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

theorem MIPStarRE.LDT.Preliminaries.questionCabApproxDelta {Outcome : Type u_1} {Aux : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] [Fintype Aux] (ψ : QuantumState ι) (A B : OpFamily Outcome ι) (C : Outcome → Aux → Quantum.Op ι) (hC : ∀ (a : Outcome), ∑ b : Aux, Matrix.conjTranspose (C a b) * C a b ≤ 1) : 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 } ≤ qSDDOp ψ A B

theorem MIPStarRE.LDT.Preliminaries.cabApproxDelta_raw {Question : Type u_1} {Outcome : Type u_2} {Aux : Type u_3} {ι : Type u_4} [Fintype ι] [DecidableEq ι] [Fintype Outcome] [Fintype Aux] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B : IdxOpFamily Question Outcome ι) (C : Question → Outcome → Aux → Quantum.Op ι) (δ : Error) : SDDOpRel ψ 𝒟 A B δ → (∀ (q : Question) (a : Outcome), ∑ b : Aux, Matrix.conjTranspose (C q a b) * C q a b ≤ 1) → 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.

Infrastructure: triangle inequality for SDDOpRel

theorem MIPStarRE.LDT.Preliminaries.qSDDOp_nonneg {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A B : OpFamily Outcome ι) : 0 ≤ qSDDOp ψ A B

The operator-family squared-distance defect is nonnegative.

theorem MIPStarRE.LDT.Preliminaries.stateDependentDistanceOpRel_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 operator-family state-dependent distance.

theorem MIPStarRE.LDT.Preliminaries.stateDependentDistanceOpRel_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) (hle : δ ≤ δ') : SDDOpRel ψ 𝒟 A B δ → SDDOpRel ψ 𝒟 A B δ'

Monotonicity of SDDOpRel in the error bound.

theorem MIPStarRE.LDT.Preliminaries.sddOpRel_symm {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 ψ 𝒟 B A δ

Symmetry of the operator-family state-dependent distance relation.

theorem MIPStarRE.LDT.Preliminaries.sddOpRel_leftPlaced_of_ev_eq {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)) (φ : QuantumState ιA) (𝒟 : Distribution Question) (A B : IdxOpFamily Question Outcome ιA) (δ : Error) (hev : ∀ (X : Quantum.Op ιA), ev ψ (leftTensor X) = ev φ X) : SDDOpRel φ 𝒟 A B δ → SDDOpRel ψ 𝒟 (fun (q : Question) => (A q).leftPlacedOpFamily) (fun (q : Question) => (B q).leftPlacedOpFamily) δ

Transport a local raw-operator state-dependent distance estimate to the left tensor factor of a bipartite state.

The hypothesis hev is the defining marginal identity for the left register: expectations of local operators in φ agree with expectations of their left-tensor placements in ψ. Under this identity, the squared-distance defect of two local raw operator families is exactly the squared-distance defect of their left placements.