Spectral von Neumann entropy (K1-A)

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

The von Neumann entropy of a density operator, defined spectrally as

S(ρ) = ∑ᵢ negMulLog (λᵢ) = − ∑ᵢ λᵢ log λᵢ,

where λᵢ are the (real) eigenvalues of the Hermitian ρ and Real.negMulLog x = −x log x. This is the K1-A tranche of specs/k1-plan.md; it reuses the spectral machinery already staged in TraceDistance.lean (Matrix.IsHermitian.cfc, re_trace_cfc, the IsHermitian.cfc algebra layer).

Delivered:

• vonNeumannEntropy hρ := ∑ i, Real.negMulLog (hρ.eigenvalues i);
• the operator-form headline S(ρ) = Re Tr(cfc negMulLog ρ) = − Re Tr(ρ log ρ) (vonNeumannEntropy_eq_re_trace_cfc, vonNeumannEntropy_eq_neg_re_trace_mul_log), identifying the spectral sum with −Tr(ρ log ρ) via re_trace_cfc;
• non-negativity 0 ≤ S(ρ) for a density operator (vonNeumannEntropy_nonneg), from λᵢ ∈ [0,1] (PSD ⟹ λᵢ ≥ 0; ∑ λᵢ = trace = 1 ⟹ λᵢ ≤ 1) and Real.negMulLog_nonneg;
• pure-state vanishing S(ρ) = 0 for a rank-1 projection (ρ * ρ = ρ, trace ρ = 1) (vonNeumannEntropy_eq_zero_of_pure), since the spectrum is {0,1} and negMulLog vanishes there;
• unitary invariance S(U ρ Uᴴ) = S(ρ) (vonNeumannEntropy_conj_unitary), via charpoly conjugation-invariance + eigenvalues_eq_eigenvalues_iff;
• unconditional additivity on tensor products S(ρ ⊗ σ) = S(ρ) + S(σ) for density operators (PSD, unit trace) (vonNeumannEntropy_kronecker), via the Kronecker spectrum spectral_sum_kronecker (the eigenvalues of ρ ⊗ₖ σ are the products λᵢ μⱼ, in permutation-invariant spectral-sum form); the explicit-hypothesis form vonNeumannEntropy_kronecker_of_eigenvalues is retained for callers holding a sorted eigenvalue-product witness. See the note below.

Note on the Kronecker spectrum (K1-A.2, done)

Mathlib has no lemma identifying the eigenvalues of a Kronecker product ρ ⊗ₖ σ with the products λᵢ μⱼ of the factor eigenvalues (no Kronecker spectral theorem). We supply it here, in the spectral-sum form that additivity needs (spectral_sum_kronecker):

∑_c g(λ(ρ⊗σ)_c) = ∑_{i,j} g(λρ(i)·λσ(j)) for every g : ℝ → ℝ.

The route is charpoly-based and permutation-invariant, so it sidesteps the subtlety that Mathlib's eigenvalues is the sorted spectrum (matching it pointwise to the products along an ad-hoc reindexing is the easy-to-get-wrong step; the spectral sum avoids it). Concretely: ρ⊗σ = (U_ρ⊗U_σ) · diagonal(λρ·λσ) · (U_ρ⊗U_σ)ᴴ (kronecker_eq_conj_diagonal_eigenvalues, from the two spectral theorems + mul_kronecker_mul + diagonal_kronecker_diagonal), so its charpoly is ∏_p (X − ↑(λρ(p.1)·λσ(p.2))) (charpoly_conj_unitary + charpoly_diagonal); the spectral sum is then read off the charpoly root multiset by spectral_sum_eq_of_charpoly_prod. No external axiom is incurred (foundational triple only). This discharges the former K1-A.2 item; the conditional vonNeumannEntropy_kronecker_of_eigenvalues is kept as a convenience.

theorem Real.negMulLog_pos {x : ℝ} (h0 : 0 < x) (h1 : x < 1) : 0 < x.negMulLog

negMulLog is strictly positive on the open interval (0,1): 0 < x < 1 ⟹ 0 < negMulLog x. Companion to Real.negMulLog_nonneg (the closed-interval ≥ 0). The strict interior positivity is what the entropy-increase witness needs: a genuine superposition Born weight p ∈ (0,1) contributes strictly positive Shannon entropy. Since log x < 0 for 0 < x < 1 and x > 0, negMulLog x = -(x log x) > 0.

noncomputable def QuantumInfo.vonNeumannEntropy {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) : ℝ

The von Neumann entropy S(ρ) = ∑ᵢ negMulLog(λᵢ) = −∑ᵢ λᵢ log λᵢ of a Hermitian operator, defined spectrally from its real eigenvalues.

Equations

• QuantumInfo.vonNeumannEntropy hρ = ∑ i : n, (hρ.eigenvalues i).negMulLog

Operator-form identity: S(ρ) = −Tr(ρ log ρ)

theorem QuantumInfo.vonNeumannEntropy_eq_re_trace_cfc {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) : vonNeumannEntropy hρ = RCLike.re (hρ.cfc Real.negMulLog).trace

Operator-form headline (the negMulLog-trace identity): S(ρ) = Re Tr(cfc negMulLog ρ), directly from re_trace_cfc at f = Real.negMulLog.

theorem QuantumInfo.vonNeumannEntropy_eq_neg_re_trace_mul_log {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) : vonNeumannEntropy hρ = -RCLike.re (hρ.cfc fun (x : ℝ) => x * Real.log x).trace

The −Tr(ρ log ρ) form: S(ρ) = − Re Tr(cfc (x ↦ x log x) ρ). Here cfc (x ↦ x log x) ρ is the operator ρ log ρ (log ρ being cfc log ρ), so this is the standard S(ρ) = −Tr(ρ log ρ).

theorem QuantumInfo.cfc_id_mul_log {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) : ρ * hρ.cfc Real.log = hρ.cfc fun (x : ℝ) => x * Real.log x

The cfc operator ρ log ρ equals the multiplicative cfc cfc (x ↦ x log x) ρ. The product ρ · log ρ of the spectral identity ρ = hρ.cfc id and log ρ = hρ.cfc log is, by cfc_mul, the cfc of the pointwise product. So hρ.cfc (x ↦ x log x) is genuinely ρ log ρ and the headline above reads S(ρ) = −Re Tr(ρ log ρ).

Non-negativity

theorem QuantumInfo.eigenvalues_mem_Icc_of_density {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hpsd : ρ.PosSemidef) (htr : ρ.trace = 1) (i : n) : 0 ≤ ⋯.eigenvalues i ∧ ⋯.eigenvalues i ≤ 1

Helper: a density operator's eigenvalues lie in [0,1]. PSD gives λᵢ ≥ 0; unit trace gives ∑ λᵢ = 1, hence each λᵢ ≤ 1 (a single term bounded by a sum of non-negatives).

theorem QuantumInfo.vonNeumannEntropy_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hpsd : ρ.PosSemidef) (htr : ρ.trace = 1) : 0 ≤ vonNeumannEntropy ⋯

S(ρ) ≥ 0 for a density operator (PSD, unit trace). Each eigenvalue lies in [0,1], where Real.negMulLog is non-negative.

Maximum-entropy bound S ≤ log d

theorem QuantumInfo.vonNeumannEntropy_le_log_card {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hpsd : ρ.PosSemidef) (htr : ρ.trace = 1) : vonNeumannEntropy ⋯ ≤ Real.log ↑(Fintype.card n)

Maximum-entropy bound S(ρ) ≤ log d for a density operator (PSD, unit trace) on a space of dimension d = Fintype.card n ≥ 1. The maximally mixed state ρ = I/d saturates it. Route: negMulLog is concave on Ici 0 (Real.concaveOn_negMulLog); Finset Jensen (ConcaveOn.le_map_sum) with uniform weights wᵢ = 1/d and pᵢ = λᵢ ∈ [0,1] ⊂ Ici 0 gives ∑ᵢ (1/d)·negMulLog(λᵢ) ≤ negMulLog(∑ᵢ (1/d)·λᵢ) = negMulLog(1/d) (using ∑λᵢ = trace = 1), and negMulLog(1/d) = (1/d)·log d. Multiply through by d.

cfc injectivity on the spectrum

theorem QuantumInfo.cfc_eq_iff_on_eigenvalues {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) {f g : ℝ → ℝ} (h : hρ.cfc f = hρ.cfc g) (i : n) : f (hρ.eigenvalues i) = g (hρ.eigenvalues i)

IsHermitian.cfc injectivity on eigenvalues: if hρ.cfc f = hρ.cfc g then f and g agree on every eigenvalue. Conjugating U · diag(↑∘f∘λ) · Uᴴ = U · diag(↑∘g∘λ) · Uᴴ by Uᴴ … U collapses (via UᴴU = 1) to the diagonals, whose entries are f(λᵢ) and g(λᵢ).

Pure-state vanishing

theorem QuantumInfo.vonNeumannEntropy_eq_zero_of_projection {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) (hidem : ρ * ρ = ρ) : vonNeumannEntropy hρ = 0

S(ρ) = 0 for a projection (ρ Hermitian, idempotent ρ·ρ = ρ). The idempotency forces λᵢ² = λᵢ, so the spectrum is {0,1}, where negMulLog vanishes. The pure-state case is the rank-1 instance ρ = |ψ⟩⟨ψ| (a projection with trace ρ = 1); see vonNeumannEntropy_eq_zero_of_pure for that named form. Unit trace is not needed for S = 0 itself (every projection, including 0 and I, has spectrum in {0,1}).

theorem QuantumInfo.vonNeumannEntropy_eq_zero_of_pure {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) (hidem : ρ * ρ = ρ) (_htr : ρ.trace = 1) : vonNeumannEntropy hρ = 0

S(ρ) = 0 for a pure state — a rank-1 density projection (ρ Hermitian, idempotent ρ·ρ = ρ, unit trace trace ρ = 1). Direct corollary of vonNeumannEntropy_eq_zero_of_projection. The unit-trace hypothesis is non-vacuous and non-degenerate: it forces ∑ λᵢ = 1 with λᵢ ∈ {0,1}, i.e. exactly one eigenvalue equal to 1, so ρ ≠ 0; this is the genuine rank-1 pure state |ψ⟩⟨ψ|, not the trivial ρ = 0.

Unitary invariance

theorem QuantumInfo.charpoly_conj_unitary {n : Type u_1} [Fintype n] [DecidableEq n] {ρ U : Matrix n n ℂ} (hU : star U * U = 1) : (U * ρ * star U).charpoly = ρ.charpoly

Charpoly conjugation-invariance: (U ρ Uᴴ).charpoly = ρ.charpoly for U unitary (Uᴴ U = 1). Two applications of charpoly_mul_comm plus Uᴴ U = 1.

theorem QuantumInfo.vonNeumannEntropy_conj_unitary {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) {U : Matrix n n ℂ} (hU : star U * U = 1) (hUρU : (U * ρ * star U).IsHermitian) : vonNeumannEntropy hUρU = vonNeumannEntropy hρ

Unitary invariance S(U ρ Uᴴ) = S(ρ). Conjugation by a unitary preserves the characteristic polynomial, hence (by eigenvalues_eq_eigenvalues_iff) the eigenvalue function, hence the spectral entropy sum.

Tensor additivity

theorem QuantumInfo.isHermitian_kronecker {n : Type u_1} {m : Type u_2} [Fintype m] [DecidableEq m] {ρ : Matrix n n ℂ} {σ : Matrix m m ℂ} (hρ : ρ.IsHermitian) (hσ : σ.IsHermitian) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρ σ).IsHermitian

The Kronecker product of two Hermitian matrices is Hermitian.

theorem QuantumInfo.negMulLog_mul {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a * b).negMulLog = b * a.negMulLog + a * b.negMulLog

negMulLog of a product factorises: negMulLog(a·b) = b·negMulLog a + a·negMulLog b for a, b ≥ 0. (At a = 0 or b = 0 both sides vanish; otherwise log(ab) = log a + log b.)

theorem QuantumInfo.vonNeumannEntropy_kronecker_of_eigenvalues {n : Type u_1} [Fintype n] [DecidableEq n] {m : Type u_2} {k : Type u_3} [Fintype m] [DecidableEq m] [Fintype k] [DecidableEq k] {ρ : Matrix n n ℂ} {σ : Matrix m m ℂ} {τ : Matrix k k ℂ} (hρ : ρ.IsHermitian) (hσ : σ.IsHermitian) (hτ : τ.IsHermitian) (e : n × m ≃ k) (heig : ∀ (c : k), hτ.eigenvalues c = hρ.eigenvalues (e.symm c).1 * hσ.eigenvalues (e.symm c).2) (hnnρ : ∀ (i : n), 0 ≤ hρ.eigenvalues i) (hnnσ : ∀ (j : m), 0 ≤ hσ.eigenvalues j) (hsumρ : ∑ i : n, hρ.eigenvalues i = 1) (hsumσ : ∑ j : m, hσ.eigenvalues j = 1) : vonNeumannEntropy hτ = vonNeumannEntropy hρ + vonNeumannEntropy hσ

Additivity on tensor products S(ρ ⊗ σ) = S(ρ) + S(σ), under the explicit hypothesis that the eigenvalues of ρ ⊗ₖ σ are the products λ(e c).1 · μ(e c).2 of factor eigenvalues along a reindexing e : (n × m) ≃ k of the Kronecker index.

This is the conditional form: it takes the eigenvalue-product fact as a hypothesis. The unconditional headline vonNeumannEntropy_kronecker discharges it via the Kronecker spectrum spectral_sum_kronecker (K1-A.2, done); this form is retained for callers that already hold a sorted eigenvalue-product witness along a specific reindexing e. The negMulLog-product algebra and the ∑ λ = ∑ μ = 1 collapse are proved here.

hsumρ/hsumσ are the unit-trace conditions ∑ λᵢ = ∑ μⱼ = 1; hnnρ/hnnσ the PSD non-negativity of the factor eigenvalues.

The Kronecker spectrum (discharging the K1-A.2 hypothesis)

theorem QuantumInfo.spectral_sum_eq_of_charpoly_prod {k : Type u_2} [Fintype k] [DecidableEq k] {A : Matrix k k ℂ} (hA : A.IsHermitian) (d : k → ℝ) (g : ℝ → ℝ) (h : A.charpoly = ∏ c : k, (Polynomial.X - Polynomial.C ↑(d c))) : ∑ c : k, g (hA.eigenvalues c) = ∑ c : k, g (d c)

Spectral-sum diagonalization invariance (charpoly form). If a Hermitian A has characteristic polynomial ∏ c, (X − ↑(d c)) for a real d : k → ℝ (i.e. its spectrum, with multiplicity, is the multiset {d c}), then for every g : ℝ → ℝ the spectral sum ∑ c, g(λᵢ(A)) equals ∑ c, g(d c).

The eigenvalue function hA.eigenvalues is Mathlib's sorted spectrum, so it is not equal to d pointwise; only the multiset {λᵢ} equals {d c} (both are the charpoly root multiset, via roots_charpoly_eq_eigenvalues and roots_prod). The spectral sum is permutation-invariant, which is what lets us pass from the multiset equality to the sum equality (mapping by g ∘ re and summing). This is the tool that sidesteps the eigenvalue-sorting subtlety.

theorem QuantumInfo.kronecker_eq_conj_diagonal_eigenvalues {n : Type u_1} [Fintype n] [DecidableEq n] {m : Type u_2} [Fintype m] [DecidableEq m] {ρ : Matrix n n ℂ} {σ : Matrix m m ℂ} (hρ : ρ.IsHermitian) (hσ : σ.IsHermitian) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρ σ = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑hρ.eigenvectorUnitary ↑hσ.eigenvectorUnitary * Matrix.diagonal fun (p : n × m) => ↑(hρ.eigenvalues p.1) * ↑(hσ.eigenvalues p.2)) * star (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑hρ.eigenvectorUnitary ↑hσ.eigenvectorUnitary)

The Kronecker product is unitarily similar to the diagonal of eigenvalue products. With W := U_ρ ⊗ U_σ (the Kronecker of the eigenvector unitaries), ρ ⊗ₖ σ = W · diagonal(λρ(p.1)·λσ(p.2)) · Wᴴ. From the two spectral theorems ρ = U_ρ diag(λρ) U_ρᴴ, σ = U_σ diag(λσ) U_σᴴ, mul_kronecker_mul (×2), and diagonal_kronecker_diagonal.

theorem QuantumInfo.star_kronecker_eigenvectorUnitary_mul_self {n : Type u_1} [Fintype n] [DecidableEq n] {m : Type u_2} [Fintype m] [DecidableEq m] {ρ : Matrix n n ℂ} {σ : Matrix m m ℂ} (hρ : ρ.IsHermitian) (hσ : σ.IsHermitian) : star (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑hρ.eigenvectorUnitary ↑hσ.eigenvectorUnitary) * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑hρ.eigenvectorUnitary ↑hσ.eigenvectorUnitary = 1

The Kronecker eigenvector-unitary is unitary: (U_ρ ⊗ U_σ)ᴴ · (U_ρ ⊗ U_σ) = 1. From conjTranspose_kronecker, mul_kronecker_mul, one_kronecker_one.

theorem QuantumInfo.spectral_sum_kronecker {n : Type u_1} [Fintype n] [DecidableEq n] {m : Type u_2} [Fintype m] [DecidableEq m] {ρ : Matrix n n ℂ} {σ : Matrix m m ℂ} (hρ : ρ.IsHermitian) (hσ : σ.IsHermitian) (g : ℝ → ℝ) : ∑ c : n × m, g (⋯.eigenvalues c) = ∑ i : n, ∑ j : m, g (hρ.eigenvalues i * hσ.eigenvalues j)

The Kronecker spectrum (eigenvalue-product fact). The spectral sum of any g : ℝ → ℝ over the eigenvalues of ρ ⊗ₖ σ equals the double sum over the products λρ(i)·λσ(j):

∑_c g(λ(ρ⊗σ)_c) = ∑_{i,j} g(λρ(i)·λσ(j)).

This is the load-bearing fact that discharges the heig hypothesis of vonNeumannEntropy_kronecker_of_eigenvalues. Proof route: ρ⊗σ is unitarily similar to diagonal(λρ·λσ) (kronecker_eq_conj_diagonal_eigenvalues), so its charpoly is ∏ p, (X − ↑(λρ(p.1)·λσ(p.2))) (charpoly_conj_unitary + charpoly_diagonal); the spectral sum is then read off the charpoly root multiset by spectral_sum_eq_of_charpoly_prod, which is permutation-invariant and so avoids matching Mathlib's sorted eigenvalues to the products pointwise. No Kronecker spectral theorem is assumed; this is one (in spectral-sum form).

theorem QuantumInfo.vonNeumannEntropy_kronecker {n : Type u_1} [Fintype n] [DecidableEq n] {m : Type u_2} [Fintype m] [DecidableEq m] {ρ : Matrix n n ℂ} {σ : Matrix m m ℂ} (hpsdρ : ρ.PosSemidef) (hpsdσ : σ.PosSemidef) (htrρ : ρ.trace = 1) (htrσ : σ.trace = 1) : vonNeumannEntropy ⋯ = vonNeumannEntropy ⋯ + vonNeumannEntropy ⋯

Unconditional additivity of the von Neumann entropy on tensor products: S(ρ ⊗ σ) = S(ρ) + S(σ) for two density operators ρ, σ (PSD, unit trace). The eigenvalue-product hypothesis of vonNeumannEntropy_kronecker_of_eigenvalues is discharged here via the Kronecker spectrum spectral_sum_kronecker; the negMulLog-product algebra (negMulLog_mul) and the ∑λ = ∑μ = 1 collapse close the argument.

This is K1-A.2 of specs/k1-plan.md, now done: additivity holds with no spectral hypothesis, only the density conditions. (The conditional form vonNeumannEntropy_kronecker_of_eigenvalues is retained for callers that already hold a sorted eigenvalue-product witness.)

Entropy of a real-scalar (maximally-mixed) state

theorem QuantumInfo.const_smul_one_isHermitian {N : ℕ} (c : ℝ) : (↑c • 1).IsHermitian

A real-scalar multiple of the identity is Hermitian: (↑c)·I for c : ℝ. Via diagonal_conjTranspose and star (↑c) = ↑c.

theorem QuantumInfo.vonNeumannEntropy_const_smul_one {N : ℕ} (c : ℝ) (h : (↑c • 1).IsHermitian) : vonNeumannEntropy h = ↑N * c.negMulLog

Entropy of a real-scalar identity. S((↑c)·I_N) = N · negMulLog c for c : ℝ. Route: (↑c)·I = diagonal (fun _ => ↑c) has charpoly ∏ (X − ↑c), so its spectral sum collapses by spectral_sum_eq_of_charpoly_prod (permutation-invariant, avoiding the sorted-eigenvalue subtlety); the constant sum gives N · negMulLog c.

theorem QuantumInfo.vonNeumannEntropy_maximally_mixed {N : ℕ} (hN : 0 < N) (h : (↑(1 / ↑N) • 1).IsHermitian) : vonNeumannEntropy h = Real.log ↑N

Maximally-mixed entropy saturates the max-entropy bound: S((1/N)·I) = log N for N ≥ 1. Companion to vonNeumannEntropy_le_log_card (the ≤ log d bound); the uniform state is the saturating case.

Entropy of a general diagonal state

theorem QuantumInfo.vonNeumannEntropy_diagonal {n : Type u_1} [Fintype n] [DecidableEq n] {d : n → ℝ} (h : (Matrix.diagonal fun (i : n) => ↑(d i)).IsHermitian) : vonNeumannEntropy h = ∑ i : n, (d i).negMulLog

Entropy of a diagonal density. S(diagonal (fun i => ↑(d i))) = ∑ i, negMulLog (d i) for a real diagonal d : n → ℝ (Hermitian witness supplied). The charpoly of diagonal (↑ ∘ d) is ∏ i, (X − ↑(d i)) (charpoly_diagonal), so the spectral sum collapses to ∑ i, negMulLog (d i) by spectral_sum_eq_of_charpoly_prod (permutation-invariant, avoiding the sorted-eigenvalue subtlety). Generalises vonNeumannEntropy_const_smul_one (the constant case d ≡ c).

theorem QuantumInfo.entropy_congr_of_eq {n : Type u_1} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n ℂ} (heq : ρ = σ) (hρ : ρ.IsHermitian) (hσ : σ.IsHermitian) : vonNeumannEntropy hρ = vonNeumannEntropy hσ

Entropy is independent of the supplied Hermitian witness and transports across a matrix equality: if ρ = σ then S(ρ) = S(σ) (the eigenvalue values are matrix-determined). The proof-irrelevance / matrix-equality hinge used to move an entropy computation onto a diagonal form.