Entropy and relative entropy of finite matrices

This file develops the entropy calculus of finite quantum systems. A state of such a system is a density matrix: a positive semidefinite matrix of trace one. The matrices have entries in any RCLike field, the physical case being ℂ.

• The von Neumann entropy of ρ is S(ρ) = -Tr (ρ log ρ) = ∑ᵢ -λᵢ log λᵢ, the trace of the functional calculus of Real.negMulLog; the convention 0 log 0 = 0 is built in. Matrix.vonNeumannEntropy.
• The relative entropy (Umegaki) of ρ with respect to σ is D(ρ ‖ σ) = Tr (ρ (log ρ - log σ)) when the kernel of σ is contained in the kernel of ρ, and ⊤ otherwise. It takes values in EReal, since for references σ which are not normalized it may be negative. Matrix.relativeEntropy.

The basic inequality is Klein's inequality Tr ρ - Tr σ ≤ D(ρ ‖ σ) for positive semidefinite ρ and σ, which gives the positivity of relative entropy between density matrices. The trace formula Matrix.IsHermitian.trace_cfc_mul_cfc reduces it to the scalar inequality a - b ≤ a log a - a log b between the eigenvalues a of ρ and b of σ, weighted by the doubly stochastic overlaps ‖⟪uᵢ, vⱼ⟫‖² of their eigenvectors; the support condition removes the pairs with b = 0 < a, for which the scalar inequality fails.

Klein's inequality against a product state gives the subadditivity of the von Neumann entropy: for a density matrix ρ of a bipartite system, indexed by m × n, with reduced density matrices ρ_A = Tr₂ ρ and ρ_B = Tr₁ ρ, S(ρ) ≤ S(ρ_A) + S(ρ_B). Since log (σ_A ⊗ₖ σ_B) = log σ_A ⊗ₖ 1 + 1 ⊗ₖ log σ_B for positive definite σ_A and σ_B, the partial traces turn Tr (ρ log (σ_A ⊗ₖ σ_B)) into Tr (ρ_A log σ_A) + Tr (ρ_B log σ_B). The reduced density matrices may be singular, so we compare ρ with σ_A ⊗ₖ σ_B, where σ_A and σ_B replace the zero eigenvalues of ρ_A and ρ_B by t > 0. This leaves Tr (ρ_A log σ_A) = -S(ρ_A) unchanged, and the error in the traces vanishes as t → 0.

If 0 ≤ A ≤ B, that is A and B - A are positive semidefinite, then Tr (A log A) ≤ Tr (A log B), or equivalently D(A ‖ B) ≤ 0; this trace inequality is a consequence of the operator monotonicity of the logarithm. It bounds the entropy of a sum: S(A + B) ≤ S(A) + S(B) for positive semidefinite A and B, and hence the upper mixture bound S(∑ᵢ pᵢ ρᵢ) ≤ ∑ᵢ pᵢ S(ρᵢ) - ∑ᵢ pᵢ log pᵢ for density matrices ρᵢ and a probability vector p. The matching lower bound is the concavity of the entropy: ∑ᵢ pᵢ S(ρᵢ) ≤ S(∑ᵢ pᵢ ρᵢ). Together these mixture bounds control the entropy of a mixture by the entropies of its components up to the Shannon entropy of the weights, as needed for the affinity of the mean entropy of quantum spin systems.

Main results

• Matrix.PosSemidef.re_trace_sub_trace_le_relativeEntropy — Klein's inequality: for positive semidefinite ρ and σ, Tr ρ - Tr σ ≤ D(ρ ‖ σ);
• Matrix.PosSemidef.relativeEntropy_nonneg — positivity of the relative entropy of two positive semidefinite matrices of equal trace, in particular of two density matrices;
• Matrix.PosSemidef.vonNeumannEntropy_nonneg and Matrix.PosSemidef.vonNeumannEntropy_le_log_card — 0 ≤ S(ρ) ≤ log (card n) for a density matrix ρ;
• Matrix.PosSemidef.vonNeumannEntropy_le_partialTraceRight_add_partialTraceLeft — subadditivity, S(ρ) ≤ S(Tr₂ ρ) + S(Tr₁ ρ) for a density matrix ρ of a bipartite system;
• Matrix.PosSemidef.re_trace_mul_cfc_log_le and Matrix.PosSemidef.relativeEntropy_nonpos — if 0 ≤ A ≤ B, then Tr (A log A) ≤ Tr (A log B) and D(A ‖ B) ≤ 0;
• Matrix.concaveOn_vonNeumannEntropy and Matrix.sum_mul_vonNeumannEntropy_le — concavity, ∑ᵢ pᵢ S(ρᵢ) ≤ S(∑ᵢ pᵢ ρᵢ);
• Matrix.vonNeumannEntropy_sum_smul_le — the upper mixture bound S(∑ᵢ pᵢ ρᵢ) ≤ ∑ᵢ (pᵢ S(ρᵢ) - pᵢ log pᵢ · Tr ρᵢ).

References

• M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press (2000), Section 11.3 (von Neumann entropy, quantum relative entropy, Klein's inequality, subadditivity, concavity and the upper mixture bound).
• E. A. Carlen, Trace inequalities and quantum entropy: an introductory course, Contemporary Mathematics 529 (2010), Section 2 (Klein's inequality).
• O. Bratteli, D. W. Robinson, Operator Algebras and Quantum Statistical Mechanics 2, second edition, Springer (1997), Section 6.2 (the entropy of quantum spin systems).

Von Neumann entropy

noncomputable def Matrix.vonNeumannEntropy {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (ρ : Matrix n n 𝕜) : ℝ

The von Neumann entropy S(ρ) = -Tr (ρ log ρ) of a matrix ρ: the real part of the trace of the functional calculus of x ↦ -x log x, so that 0 log 0 = 0. It is the entropy of a quantum state when ρ is a density matrix. The functional calculus of a non-Hermitian matrix is zero, so then S(ρ) = 0.

theorem Matrix.vonNeumannEntropy_def {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (ρ : Matrix n n 𝕜) : ρ.vonNeumannEntropy = RCLike.re (cfc Real.negMulLog ρ).trace

The defining equation of the von Neumann entropy, valid for every matrix ρ.

@[simp]

theorem Matrix.vonNeumannEntropy_zero {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] : vonNeumannEntropy 0 = 0

@[simp]

theorem Matrix.vonNeumannEntropy_one {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] : vonNeumannEntropy 1 = 0

theorem Matrix.IsHermitian.vonNeumannEntropy_eq_sum_negMulLog {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ρ : Matrix n n 𝕜} (hρ : ρ.IsHermitian) : ρ.vonNeumannEntropy = ∑ i : n, (hρ.eigenvalues i).negMulLog

The von Neumann entropy of a Hermitian matrix is ∑ᵢ -λᵢ log λᵢ over its eigenvalues.

theorem Matrix.IsHermitian.vonNeumannEntropy_eq_neg_re_trace_mul_cfc_log {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ρ : Matrix n n 𝕜} (hρ : ρ.IsHermitian) : ρ.vonNeumannEntropy = -RCLike.re (ρ * cfc Real.log ρ).trace

The von Neumann entropy of a Hermitian matrix is -Tr (ρ log ρ).

theorem Matrix.PosSemidef.vonNeumannEntropy_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ρ : Matrix n n 𝕜} (hρ : ρ.PosSemidef) (htr : RCLike.re ρ.trace ≤ 1) : 0 ≤ ρ.vonNeumannEntropy

The von Neumann entropy of a positive semidefinite matrix of trace at most one is nonnegative.

Relative entropy

noncomputable def Matrix.relativeEntropy {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (ρ σ : Matrix n n 𝕜) : EReal

The relative entropy (Umegaki) D(ρ ‖ σ) = Tr (ρ (log ρ - log σ)) of a matrix ρ with respect to σ. It is finite exactly when the support condition holds, that is, when the kernel of σ is contained in the kernel of ρ; otherwise it is ⊤. For density matrices it is the quantum analogue of the Kullback–Leibler divergence, and it is nonnegative, Matrix.PosSemidef.relativeEntropy_nonneg.

theorem Matrix.relativeEntropy_of_ker_le {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n 𝕜} (h : σ.mulVecLin.ker ≤ ρ.mulVecLin.ker) : ρ.relativeEntropy σ = ↑(RCLike.re (ρ * (cfc Real.log ρ - cfc Real.log σ)).trace)

Under the support condition the relative entropy is the real number Tr (ρ (log ρ - log σ)).

theorem Matrix.relativeEntropy_of_not_ker_le {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n 𝕜} (h : ¬σ.mulVecLin.ker ≤ ρ.mulVecLin.ker) : ρ.relativeEntropy σ = ⊤

Without the support condition the relative entropy is ⊤.

@[simp]

theorem Matrix.relativeEntropy_eq_top_iff {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n 𝕜} : ρ.relativeEntropy σ = ⊤ ↔ ¬σ.mulVecLin.ker ≤ ρ.mulVecLin.ker

The relative entropy is infinite exactly when the support condition fails.

@[simp]

theorem Matrix.relativeEntropy_self {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (ρ : Matrix n n 𝕜) : ρ.relativeEntropy ρ = 0

@[simp]

theorem Matrix.relativeEntropy_zero_left {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (σ : Matrix n n 𝕜) : relativeEntropy 0 σ = 0

theorem Matrix.relativeEntropy_of_posDef {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n 𝕜} (hσ : σ.PosDef) : ρ.relativeEntropy σ = ↑(RCLike.re (ρ * (cfc Real.log ρ - cfc Real.log σ)).trace)

The relative entropy with respect to a positive definite reference is always finite: the support condition holds for every ρ.

theorem Matrix.IsHermitian.relativeEntropy_eq_neg_vonNeumannEntropy_sub {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n 𝕜} (hρ : ρ.IsHermitian) (h : σ.mulVecLin.ker ≤ ρ.mulVecLin.ker) : ρ.relativeEntropy σ = ↑(-ρ.vonNeumannEntropy - RCLike.re (ρ * cfc Real.log σ).trace)

Under the support condition, D(ρ ‖ σ) = -S(ρ) - Tr (ρ log σ).

theorem Matrix.IsHermitian.relativeEntropy_smul_one {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ρ : Matrix n n 𝕜} (hρ : ρ.IsHermitian) {c : ℝ} (hc : c ≠ 0) : ρ.relativeEntropy (c • 1) = ↑(-ρ.vonNeumannEntropy - Real.log c * RCLike.re ρ.trace)

The relative entropy with respect to a nonzero real multiple c • 1 of the identity is D(ρ ‖ c • 1) = -S(ρ) - log c · Tr ρ.

theorem Matrix.PosSemidef.re_trace_sub_trace_le_relativeEntropy {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n 𝕜} (hρ : ρ.PosSemidef) (hσ : σ.PosSemidef) : ↑(RCLike.re (ρ.trace - σ.trace)) ≤ ρ.relativeEntropy σ

Klein's inequality for the relative entropy. For positive semidefinite ρ and σ, Tr ρ - Tr σ ≤ D(ρ ‖ σ).

theorem Matrix.PosSemidef.relativeEntropy_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n 𝕜} (hρ : ρ.PosSemidef) (hσ : σ.PosSemidef) (htr : ρ.trace = σ.trace) : 0 ≤ ρ.relativeEntropy σ

Positivity of relative entropy. For positive semidefinite ρ and σ of equal trace, in particular for two density matrices, 0 ≤ D(ρ ‖ σ).

theorem Matrix.PosSemidef.vonNeumannEntropy_le_log_card {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ρ : Matrix n n 𝕜} (hρ : ρ.PosSemidef) (htr : ρ.trace = 1) : ρ.vonNeumannEntropy ≤ Real.log ↑(Fintype.card n)

The von Neumann entropy of a density matrix is at most log (card n), the entropy of the maximally mixed state (card n)⁻¹ • 1.

Subadditivity

theorem Matrix.PosSemidef.vonNeumannEntropy_le_partialTraceRight_add_partialTraceLeft {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {m : Type u_3} [Fintype m] [DecidableEq m] {ρ : Matrix (m × n) (m × n) 𝕜} (hρ : ρ.PosSemidef) (htr : ρ.trace = 1) : ρ.vonNeumannEntropy ≤ ρ.partialTraceRight.vonNeumannEntropy + ρ.partialTraceLeft.vonNeumannEntropy

Subadditivity of the von Neumann entropy. For a density matrix ρ of a bipartite system, indexed by m × n, the entropy is at most the sum of the entropies of its reduced density matrices: S(ρ) ≤ S(Tr₂ ρ) + S(Tr₁ ρ).

The relative entropy below the reference in the Loewner order

theorem Matrix.PosSemidef.re_trace_mul_cfc_log_le {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A B : Matrix n n 𝕜} (hA : A.PosSemidef) (hBA : (B - A).PosSemidef) : RCLike.re (A * cfc Real.log A).trace ≤ RCLike.re (A * cfc Real.log B).trace

A trace inequality for the logarithm. If A and B - A are positive semidefinite, that is 0 ≤ A ≤ B, then Tr (A log A) ≤ Tr (A log B). The matrix A may be singular; the convention 0 log 0 = 0 applies.

theorem Matrix.PosSemidef.relativeEntropy_nonpos {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A B : Matrix n n 𝕜} (hA : A.PosSemidef) (hBA : (B - A).PosSemidef) : A.relativeEntropy B ≤ 0

Nonpositivity of the relative entropy under Loewner domination. If A and B - A are positive semidefinite, that is 0 ≤ A ≤ B, then D(A ‖ B) ≤ 0. The support condition holds automatically, so the relative entropy is finite.

Concavity and mixture bounds

theorem Matrix.IsHermitian.vonNeumannEntropy_smul {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ρ : Matrix n n 𝕜} (hρ : ρ.IsHermitian) (c : ℝ) : (c • ρ).vonNeumannEntropy = c * ρ.vonNeumannEntropy + c.negMulLog * RCLike.re ρ.trace

Scaling a Hermitian matrix by a real number c scales its entropy and adds -c log c times its trace: S(c ρ) = c S(ρ) - c log c · Tr ρ.

theorem Matrix.PosSemidef.vonNeumannEntropy_add_le {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A B : Matrix n n 𝕜} (hA : A.PosSemidef) (hB : B.PosSemidef) : (A + B).vonNeumannEntropy ≤ A.vonNeumannEntropy + B.vonNeumannEntropy

The von Neumann entropy is subadditive on positive semidefinite summands: S(A + B) ≤ S(A) + S(B).

theorem Matrix.vonNeumannEntropy_sum_le {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ι : Type u_4} (s : Finset ι) {ρ : ι → Matrix n n 𝕜} (hρ : ∀ i ∈ s, (ρ i).PosSemidef) : (∑ i ∈ s, ρ i).vonNeumannEntropy ≤ ∑ i ∈ s, (ρ i).vonNeumannEntropy

The entropy of a finite sum of positive semidefinite matrices is at most the sum of their entropies.

theorem Matrix.vonNeumannEntropy_sum_smul_le {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ι : Type u_4} (s : Finset ι) {p : ι → ℝ} {ρ : ι → Matrix n n 𝕜} (hp : ∀ i ∈ s, 0 ≤ p i) (hρ : ∀ i ∈ s, (ρ i).PosSemidef) : (∑ i ∈ s, p i • ρ i).vonNeumannEntropy ≤ ∑ i ∈ s, (p i * (ρ i).vonNeumannEntropy + (p i).negMulLog * RCLike.re (ρ i).trace)

Upper mixture bound for the entropy. For positive semidefinite ρᵢ and weights pᵢ ≥ 0, S(∑ᵢ pᵢ ρᵢ) ≤ ∑ᵢ (pᵢ S(ρᵢ) - pᵢ log pᵢ · Tr ρᵢ). For density matrices and a probability vector p the error term is the Shannon entropy -∑ᵢ pᵢ log pᵢ of p.

theorem Matrix.concaveOn_vonNeumannEntropy {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] : ConcaveOn ℝ {ρ : Matrix n n 𝕜 | ρ.PosSemidef} vonNeumannEntropy

Concavity of the von Neumann entropy on the positive semidefinite matrices: for positive semidefinite x and y and weights a, b ≥ 0 with a + b = 1, a S(x) + b S(y) ≤ S(a x + b y).

theorem Matrix.sum_mul_vonNeumannEntropy_le {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {ι : Type u_4} (s : Finset ι) {p : ι → ℝ} {ρ : ι → Matrix n n 𝕜} (hp : ∀ i ∈ s, 0 ≤ p i) (hp₁ : ∑ i ∈ s, p i = 1) (hρ : ∀ i ∈ s, (ρ i).PosSemidef) : ∑ i ∈ s, p i * (ρ i).vonNeumannEntropy ≤ (∑ i ∈ s, p i • ρ i).vonNeumannEntropy

Lower mixture bound for the entropy, the finite form of its concavity: for positive semidefinite ρᵢ and a probability vector p, ∑ᵢ pᵢ S(ρᵢ) ≤ S(∑ᵢ pᵢ ρᵢ).