Trace distance and von Neumann entropy

To prove more results here we should probably work with the characteristic polynomial of a density matrix.

noncomputable def traceDistance {R : Type u_1} [RCLike R] {q : ℕ} (ρ σ : densityMatrix (Fin q)) : ℝ

The trace distance between two density matrices.

Equations

• traceDistance ρ σ = 1 / 2 * ∑ i : Fin q, |⋯.eigenvalues i|

noncomputable def vonNeumannEntropy {R : Type u_1} [RCLike R] {q : ℕ} (ρ : densityMatrix (Fin q)) : ℝ

The von Neumann entropy of a density matrix.

Equations

• vonNeumannEntropy ρ = -∑ i : Fin q, ⋯.eigenvalues i * Real.log (⋯.eigenvalues i)

theorem densityMatrix_one {R : Type u_1} [Ring R] [PartialOrder R] [StarRing R] (ρ : densityMatrix (Fin 1)) : ↑ρ = !![1]

A 1x1 density matrix has 1 as its single entry.

theorem traceDistance_zero {R : Type u_1} [RCLike R] {q : ℕ} (ρ : densityMatrix (Fin q)) : traceDistance ρ ρ = 0

The trace distance satisfies the axiom d(x,x)=0 of a metric.

theorem unitary_iff₁₁ (z : ℂ) : star z * z = 1 ↔ !![z] ∈ unitary (Matrix (Fin 1) (Fin 1) ℂ)

theorem unitary_iff₂₂ (a b c d : ℂ) : star a * a + star c * c = 1 ∧ star b * b + star d * d = 1 ∧ star a * b + star c * d = 0 ↔ !![a, b; c, d] ∈ unitary (Matrix (Fin 2) (Fin 2) ℂ)