Subadditivity of von Neumann entropy

Open

QAlgorithms.Arunachalam.vnEntropy_subadditive

by Goku · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

arunachalamlecture-notesquantum-information

Let $\mathcal H_A$ and $\mathcal H_B$ be finite-dimensional Hilbert spaces and let $\rho_{AB}$ be a density matrix (positive semidefinite, trace one) on $\mathcal H_A\otimes\mathcal H_B$ . Write $\rho_A=\operatorname{Tr}_B\rho_{AB}$ and $\rho_B=\operatorname{Tr}_A\rho_{AB}$ for its reduced states and $S(\rho)=-\operatorname{Tr}(\rho\log_2\rho)$ for the von Neumann entropy (with $0\log 0=0$ ). Then

S(\rho_{AB})\le S(\rho_A)+S(\rho_B).

This inequality is used to bound the mutual information between a concept and $T$ examples by $T$ times the information in one example.

Formalization Note $\rho\log_2\rho$ is computed by the continuous functional calculus applied to $x\mapsto x\log_2 x$ ; Lean's $\log 0=0$ gives the convention $0\log 0=0$ .

Preamble

import Definitions.Def_QAlgorithms_Defs_Learning
set_option autoImplicit false

Formal statement

namespace QAlgorithms.Arunachalam

open QAlgorithms.Learning

/-- Arunachalam p.162, Fact 7.3.10 (subadditivity of quantum entropy): for every bipartite
density matrix `ρ_AB` on `H_A ⊗ H_B`, `S(ρ_AB) ≤ S(ρ_A) + S(ρ_B)`, where `S(ρ) = −Tr(ρ log ρ)`
(log base 2, §7.3.1) and `ρ_A = Tr_B ρ_AB`, `ρ_B = Tr_A ρ_AB` are the partial traces. -/
theorem vnEntropy_subadditive {ι κ : Type*} [Fintype ι] [DecidableEq ι] [Fintype κ]
    [DecidableEq κ] (ρ : Matrix (ι × κ) (ι × κ) ℂ) (hρ : IsDensityMatrix ρ) :
    vnEntropy ρ ≤ vnEntropy (traceRight ρ) + vnEntropy (traceLeft ρ) := by
  sorry






end QAlgorithms.Arunachalam

Source

Srinivasan Arunachalam, Quantum Algorithms and Learning Theory — Part II, 2018 thesis, ILLC DS-2018-08, PDF p. 162, Fact 7.3.10. https://ir.cwi.nl/pub/27536/Thesis_S_Arunachalam

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $\iota$ and $\kappa$ be arbitrary finite types with decidable equality. Let $\rho$ be a complex square matrix indexed by $\iota\times\kappa$ , viewed as an operator on a bipartite system whose first factor is $\iota$ and second factor is $\kappa$ . Assume $\rho$ is a density matrix: it is positive semidefinite and $\operatorname{Tr}\rho = 1$ .

Two partial traces appear:

The reduced matrix on the first factor, an $\iota\times\iota$ matrix:

\rho_A := \operatorname{tr}_\kappa\rho,\qquad (\rho_A)_{j,k} = \sum_{h\in\kappa}\rho_{(j,h),(k,h)}.

The reduced matrix on the second factor, a $\kappa\times\kappa$ matrix:

\rho_B := \operatorname{tr}_\iota\rho,\qquad (\rho_B)_{b,b'} = \sum_{a\in\iota}\rho_{(a,b),(a,b')}.

For any square matrix $\sigma$ , the von Neumann entropy is defined as

S(\sigma) = -\operatorname{Re}\operatorname{Tr}\big(f(\sigma)\big),\qquad f(x) = x\log_2 x,

where $f(\sigma)$ is the continuous functional calculus: $f$ is applied to the eigenvalues of the self-adjoint matrix $\sigma$ . At $x=0$ we have $f(0)=0\cdot\log_2 0 = 0$ , since the logarithm of $0$ is taken to be $0$ . For non-self-adjoint input the functional calculus returns the junk value $0$ , but $\rho$ , $\rho_A$ and $\rho_B$ are all Hermitian here.

The theorem asserts subadditivity:

S(\rho)\;\le\;S(\rho_A)+S(\rho_B).

If $\iota$ or $\kappa$ is empty, then $\rho$ is the empty matrix with trace $0\neq 1$ . The hypothesis is then unsatisfiable, so only nonempty $\iota,\kappa$ matter.

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Goku · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph