Zero von Neumann entropy characterises pure states

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

vonNeumannEntropy_eq_zero_of_pure (Entropy.lean) gives S(ρ) = 0 for a rank-one projector. This file gives the converse and packages the equivalence:

• negMulLog_eq_zero_iff — on [0, 1], negMulLog x = 0 iff x ∈ {0, 1};
• isHermitian_eq_sum_eigenvalues_smul_vecMulVec — the spectral theorem in projector form, ρ = ∑ₖ λₖ |vₖ⟩⟨vₖ| over the orthonormal eigenbasis;
• ★ vonNeumannEntropy_eq_zero_iff — for a density matrix (positive semidefinite, trace one), S(ρ) = 0 iff ρ = |ψ⟩⟨ψ| for a unit vector ψ. The eigenvalues lie in [0, 1] and sum to one; each negMulLog term is non-negative, so a zero sum forces each eigenvalue into {0, 1}, and the unit sum then forces exactly one eigenvalue to be 1; the projector form finishes it.

Consumer: CsdLean4/LF2/PreparationPurity.lean (a preparation on Σ has zero entropy iff it is pure).

Zero entropy characterises pure states (matrix level)

theorem QuantumInfo.negMulLog_eq_zero_iff {x : ℝ} (h0 : 0 ≤ x) (h1 : x ≤ 1) : x.negMulLog = 0 ↔ x = 0 ∨ x = 1

theorem QuantumInfo.isHermitian_eq_sum_eigenvalues_smul_vecMulVec {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) : ρ = ∑ k : n, ↑(hρ.eigenvalues k) • Matrix.vecMulVec (hρ.eigenvectorBasis k).ofLp (star (hρ.eigenvectorBasis k).ofLp)

A Hermitian matrix is the sum of its eigenvalues times the rank-one projectors onto an orthonormal eigenbasis.

theorem QuantumInfo.vonNeumannEntropy_eq_zero_iff {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.PosSemidef) (htr : ρ.trace = 1) : vonNeumannEntropy ⋯ = 0 ↔ ∃ (ψ : n → ℂ), star ψ ⬝ᵥ ψ = 1 ∧ ρ = Matrix.vecMulVec ψ (star ψ)

★ Zero entropy characterises pure states. For a density matrix (positive semidefinite, trace one), S(ρ) = 0 iff ρ = |ψ⟩⟨ψ| for a unit vector ψ.