Eq. (24), p. 9 — the eigenvalues of ρ = W/Tr W are λᵢ/Σⱼλⱼ, where λ₁, …, λₙ are the eigenvalues of the Wishart matrix W

Proved

NechitaRDM.MP.eq_24

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

eigenvaluesp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1random-matrix-theorywishart

Let $X$ be an $n \times k$ complex matrix and $W = XX^*$ . If $\lambda_1, \dots, \lambda_n$ are the eigenvalues of $W$ and $\tilde\lambda_1, \dots, \tilde\lambda_n$ those of $\rho = W/\operatorname{Tr} W$ , then (as lists counted with multiplicity)

\tilde\lambda_i = \frac{\lambda_i}{\sum_{j=1}^n \lambda_j}, \qquad 1 \le i \le n .

This is how the spectrum of a density matrix of law $\mu_{n,k}$ is read off the spectrum of a Wishart matrix; it is used in eq. (51) of the proof of Theorem 5.

Formalization Note The page states it for a Wishart random matrix; since every realization of a Wishart matrix is of the form $XX^*$ , it is stated for every deterministic $X$ . Eigenvalues are multisets (with multiplicity). At $X = 0$ both sides are $n$ zeros in Lean (0⁻¹ = 0, 0 / 0 = 0), so no hypothesis is needed.

Preamble

import Mathlib
import Definitions.Def_NechitaRDM_MP_Basic

Formal statement

namespace NechitaRDM.MP

/-- **Eq. (24)** (p. 9). If `λ₁, …, λₙ` are the eigenvalues of `W = XX*` and `λ̃₁, …, λ̃ₙ` those
of `ρ = W / Tr W`, then `λ̃ᵢ = λᵢ / Σⱼ λⱼ` (as multisets). -/
theorem eq_24 {n k : ℕ} (X : Matrix (Fin n) (Fin k) ℂ) :
    eigs ((wishart X).trace⁻¹ • wishart X) =
      (eigs (wishart X)).map (fun x => x / (eigs (wishart X)).sum) := by sorry

end NechitaRDM.MP

Source

Nechita, Asymptotics of random density matrices, arXiv:quant-ph/0702154v3, p. 9, eq. (24)

Human review

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

View graph