Trace distance

• “Operational interpretation of the Trace distance: Distinguish quantum states.”

variables
(ℋ₁ ℋ₂ : Type)
[complex_Hilbert_space ℋ₁]
[complex_Hilbert_space ℋ₂]
(M N : ℋ₁ →ₗ[ℂ] ℋ₂)

def trace_norm (M) :=
Tr(√{M†M})

notation `∥`M`∥₁` = trace_norm M

def trace_dist (M) (N) :=
∥M - N∥₁

def trace_dist' [quantum_state ρreal ρideal] :=
max {tr(M * (ρreal − ρideal)) | 0 \leq M \leq 1} 

theorem trace_dist_eq_trace_dist' [quantum_state ρreal ρideal] :
  trace_dist ρreal ρideal = trace_dist' ρreal ρideal :=
sorry

theroem trace_norm_geq_zero {M} :
  ∥M∥₁ ≥ 0 :=
sorry

theroem trace_dist_geq_zero {M} {N} :
  ∥M - N∥₁ ≥ 0 :=
by exact trace_norm_geq_zero M N,

theorem trace_norm_homogenous {c : ℂ} {M} :
  ∥c * M∥₁ = |c| * ∥M∥₁ :=
sorry

theorem trace_norm_sum_leq_sum_trace_norm {M} {N} : 
  ∥M + N∥₁ ≤ ∥M∥₁ + ∥N∥₁ :=
sorry

variables
(ρ σ : ℋ₁ →ₗ[ℂ] ℋ₁)

theorem trace_dist_leq_two (ρ) (σ) :
  ∥ρ - σ∥₁ ≤ 2 :=
sorry

/-- Triangle inequality -/
theorem trace_dist_triangle_inequality :
  ∥ρ - σ∥₁ ≤ ∥ρ - τ∥₁ + ∥τ - σ∥₁ :=
sorry

import Quantum_channel

/-- "noisy channel “blur” two states so they appear more similar" -/
theorem states_after_channel_are_closer_in_trace_dist [quantum_channel 𝒩] :
  ∥𝒩 ρ - 𝒩 σ∥₁ ≤ ∥ρ - σ∥₁ :=
sorry

import POVM

theorem trace_dist_geq_sum_abs_prob_diff :
  ∀ [POVM Λ], ∥ρ - σ∥₁ ≥ ∑ x, ∣Tr((Λ x) ρ) - Tr((Λ x) σ)∣ :=
sorry

/-- A measurement achieves the trace distance -/
theorem trace_dist_max_over_POVM :
  ∥ρ - σ∥₁ = max {∑ x, ∣Tr((Λ x) ρ) - Tr((Λ x) σ)∣ | POVM Λ} :=
sorry

---

“consider diagonalization of ρ1 − ρ2. can be done by first calculating its eigenvalues, solving the following equation:”

det (1/2 - lambda  -1/2  / -1/2  -1/2 - lambda)

---

/-- ε-ball of ρ -/
def eps_ball (ε : ℝ) [quantum_state ρ] :=
{ρ' | quantum_state ρ' ∧ ∥ρ - ρ'∥₁ ≤ ε}

References

• Wilde2011;

• edX Quantum Cryptography Lecture 3 notes;