Density matrices are exactly the unit-trace positive semidefinite matrices

Proved

QAlgorithms.Nannicini.densityMatrix_iff

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

lecture-notesnanniciniquantum-information

Let $\rho$ be a complex $2^q\times 2^q$ matrix acting on $q$ qubits. An ensemble of pure states is a family $\{p_j,|\psi_j\rangle\}_{j=1,\dots,m}$ of unit vectors $|\psi_j\rangle\in(\mathbb C^2)^{\otimes q}$ with probabilities $p_j\ge 0$ , $\sum_j p_j=1$ . Its density matrix is $\sum_j p_j|\psi_j\rangle\langle\psi_j|$ (Definition 1.55). Then

\exists\, m,\ \{p_j,|\psi_j\rangle\}_{j=1}^m \text{ an ensemble with } \rho=\sum_{j=1}^m p_j|\psi_j\rangle\langle\psi_j| \iff \operatorname{Tr}\rho=1 \text{ and } \rho\succeq 0.

This is the standard intrinsic description of mixed states. Later chapters use it to recognize a matrix as a quantum state without exhibiting an ensemble.

Formalization Note Positive semidefiniteness is Mathlib's Matrix.PosSemidef, which includes Hermiticity.

Preamble

import Definitions.Def_QAlgorithms_Defs_Measurement
set_option autoImplicit false

Formal statement

namespace QAlgorithms.Nannicini

open QAlgorithms

open scoped ComplexOrder


/-- Nannicini p.36, Theorem 1.60 (characterization of density matrices): a `q`-qubit matrix `ρ`
is the density matrix `∑_j p_j |ψ_j⟩⟨ψ_j|` of some ensemble `{p_j, |ψ_j⟩}_{j=1..m}` of pure
states (unit vectors) with probabilities `p_j ≥ 0`, `∑_j p_j = 1`, for some `m`, if and only if
`ρ` has unit trace and is positive semidefinite. -/
theorem densityMatrix_iff {q : ℕ} (ρ : Matrix (Qubits q) (Qubits q) ℂ) :
    (∃ (m : ℕ) (p : Fin m → ℝ) (ψ : Fin m → EuclideanSpace ℂ (Qubits q)),
        (∀ j, 0 ≤ p j) ∧ ∑ j, p j = 1 ∧ (∀ j, IsState (ψ j)) ∧ ρ = ensembleDensity p ψ) ↔
      ρ.trace = 1 ∧ ρ.PosSemidef := by sorry



end QAlgorithms.Nannicini

Source

Giacomo Nannicini, Quantum algorithms for optimizers, 2025, v5; notes dated 9 July 2025, PDF p. 36, Theorem 1.60. https://arxiv.org/pdf/2408.07086v5

Read-back

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

Setting. Let $q \ge 0$ and let $\rho$ be a complex $2^q \times 2^q$ matrix whose rows and columns are indexed by $\{0,1\}^q$ .

Claim. The following two conditions are equivalent.

Ensemble form. There exist a natural number $m$ $m$ , real weights $p_0,\dots,p_{m-1}$ $p_{0}, \dots, p_{m - 1}$ and vectors $\psi_0,\dots,\psi_{m-1} \in \mathbb{C}^{\{0,1\}^q}$ $ψ_{0}, \dots, ψ_{m - 1} \in C^{{0, 1}^{q}}$ such that:
- every $p_j \ge 0$ ,
- $\sum_j p_j = 1$ (this forces $m \ge 1$ ),
- every $\psi_j$ has norm $1$ ,
- and

\rho = \sum_{j=0}^{m-1} p_j\, \psi_j \psi_j^{*},

meaning the $(a,b)$ entry of $\rho$ is $\sum_j p_j\, (\psi_j)_a \overline{(\psi_j)_b}$ .

Matrix conditions. $\operatorname{tr}\rho = 1$ and $\rho$ is positive semidefinite. Positive semidefinite means $\rho$ is Hermitian and $x^{*}\rho x \ge 0$ for every complex vector $x$ .

No bound on $m$ is imposed, and the $\psi_j$ need not be distinct or orthogonal.

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