def TrDistance {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) : ℝ

The trace distance between two quantum states: half the trace norm of the difference (ρ - σ).

Equations

• TrDistance ρ σ = 1 / 2 * (ρ.m - σ.m).traceNorm

theorem TrDistance.ge_zero {d : Type u_2} [Fintype d] (ρ σ : MState d) : 0 ≤ TrDistance ρ σ

theorem TrDistance.le_one {d : Type u_2} [Fintype d] (ρ σ : MState d) : TrDistance ρ σ ≤ 1

def TrDistance.prob {d : Type u_2} [Fintype d] (ρ σ : MState d) : Prob

The trace distance, as a Prob probability with value between 0 and 1.

Equations

• TrDistance.prob ρ σ = ⟨TrDistance ρ σ, ⋯⟩

theorem TrDistance.symm {d : Type u_2} [Fintype d] (ρ σ : MState d) : TrDistance ρ σ = TrDistance σ ρ

The trace distance is a symmetric quantity.

theorem TrDistance.eq_abs_eigenvalues {d : Type u_2} [Fintype d] (ρ σ : MState d) : TrDistance ρ σ = 1 / 2 * ∑ i : d, |⋯.eigenvalues i|

The trace distance is equal to half the 1-norm of the eigenvalues of their difference .