Schur–Horn majorization (forward direction, Karamata form)

Let T be a symmetric operator on a finite-dimensional inner product space over 𝕜 = ℝ, ℂ, with sorted eigenvalues λ (hT.eigenvalues hn) and orthonormal eigenbasis v (hT.eigenvectorBasis hn). Fix any orthonormal basis e. The "diagonal" of T in e is the tuple d k = re ⟪T (e k), e k⟫.

The forward direction of the Schur–Horn theorem (due to Schur, 1923) says the diagonal is majorized by the spectrum, diag T ≺ spec T. We prove the equivalent Hardy–Littlewood–Pólya / Karamata characterisation: ∑ φ (d k) ≤ ∑ φ (λ i) for every convex φ defined on a set containing the eigenvalues.

The mechanism is the doubly-stochastic weight matrix w i k = ‖⟪vᵢ, e k⟫‖² (schurWeight): its rows and columns sum to 1 by Parseval, and the diagonal is its image of the spectrum, d k = ∑ i, λ i * w i k. Row-wise Jensen followed by a sum swap over the column sums gives the inequality.

Mathlib has the spectral theorem and Birkhoff's theorem but no majorization predicate and no Schur–Horn theorem (only a comment in Mathlib/Analysis/InnerProductSpace/Spectrum.lean); this file supplies the forward direction in the self-contained convex-function form.

Main results

• TauCeti.schurWeight and schurWeight_row_sum / schurWeight_col_sum: the doubly-stochastic weight matrix.
• TauCeti.re_inner_orthonormalBasis_self_eq_sum_eigenvalues_mul: the diagonal is the doubly-stochastic image of the spectrum.
• TauCeti.convexOn_sum_re_inner_orthonormalBasis_self_le: forward Schur–Horn (Karamata form), ∑ φ (d k) ≤ ∑ φ (λ i).
• TauCeti.sum_re_inner_orthonormalBasis_self_eq_sum_eigenvalues: basis independence of the trace (the equality case).
• TauCeti.sum_sq_re_inner_orthonormalBasis_self_le_sum_sq_eigenvalues: the φ = (·)² instance — the diagonal has Euclidean length ≤ that of the spectrum.

References

• I. Schur, Über eine Klasse von Mittelbildungen mit Anwendungen auf die Determinantentheorie, Sitzungsber. Berl. Math. Ges. 22 (1923), 9–20.
• A. W. Marshall, I. Olkin, B. C. Arnold, Inequalities: Theory of Majorization and Its Applications, 2nd ed., Theorem 9.B.1.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: ForMathlib.Analysis.InnerProductSpace.SchurHorn, moved to ForTauCeti in the Wave-1 staging migration; introduced at Davis--Kahan commit 9543631.
• Extraction class: moved. The Wave-1 migration renamed the namespace ForMathlib to TauCeti; declaration names and proofs are unchanged.
• Original authors / copyright: Jon Crall, Claude Opus 4.8; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — this module imports only Mathlib and sibling ForTauCeti staging modules.

noncomputable def TauCeti.schurWeight {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (e : OrthonormalBasis (Fin n) 𝕜 E) (i k : Fin n) : ℝ

The doubly-stochastic weight w i k = ‖⟪vᵢ, e k⟫‖² of the i-th eigenvector vᵢ of T against the k-th vector of a chosen orthonormal basis e.

Equations

• TauCeti.schurWeight hT hn e i k = ‖inner 𝕜 ((hT.eigenvectorBasis hn) i) (e k)‖ ^ 2

theorem TauCeti.schurWeight_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (e : OrthonormalBasis (Fin n) 𝕜 E) (i k : Fin n) : 0 ≤ schurWeight hT hn e i k

Schur--Horn weights are nonnegative, being squared moduli of basis coefficients.

theorem TauCeti.schurWeight_row_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (e : OrthonormalBasis (Fin n) 𝕜 E) (k : Fin n) : ∑ i : Fin n, schurWeight hT hn e i k = 1

Rows sum to one. By Parseval for the eigenbasis v, ∑ i, ‖⟪vᵢ, e k⟫‖² = ‖e k‖² = 1.

theorem TauCeti.schurWeight_col_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (e : OrthonormalBasis (Fin n) 𝕜 E) (i : Fin n) : ∑ k : Fin n, schurWeight hT hn e i k = 1

Columns sum to one. By Parseval for the basis e, ∑ k, ‖⟪vᵢ, e k⟫‖² = ‖vᵢ‖² = 1.

theorem TauCeti.re_inner_orthonormalBasis_self_eq_sum_eigenvalues_mul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (e : OrthonormalBasis (Fin n) 𝕜 E) (k : Fin n) : RCLike.re (inner 𝕜 (T (e k)) (e k)) = ∑ i : Fin n, hT.eigenvalues hn i * schurWeight hT hn e i k

Diagonal = doubly-stochastic image of the spectrum. The diagonal entry re ⟪T (e k), e k⟫ of T in the basis e is the convex combination ∑ i, λ i * w i k of the eigenvalues. Immediate from the diagonalisation of the quadratic form together with vⱼ.repr (e k) i = ⟪vᵢ, e k⟫.

theorem TauCeti.convexOn_sum_re_inner_orthonormalBasis_self_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (e : OrthonormalBasis (Fin n) 𝕜 E) {φ : ℝ → ℝ} {s : Set ℝ} (hφ : ConvexOn ℝ s φ) (hmem : ∀ (i : Fin n), hT.eigenvalues hn i ∈ s) : ∑ k : Fin n, φ (RCLike.re (inner 𝕜 (T (e k)) (e k))) ≤ ∑ i : Fin n, φ (hT.eigenvalues hn i)

Forward Schur–Horn theorem (convex / Karamata form). For any convex function φ on a set s containing all eigenvalues of the symmetric operator T, the diagonal of T in any orthonormal basis e satisfies ∑ k, φ (re ⟪T (e k), e k⟫) ≤ ∑ i, φ (λ i), i.e. diag T ≺ spec T.

Row-by-row Jensen against the doubly-stochastic weight matrix schurWeight, followed by a sum swap collapsing the column sums.

theorem TauCeti.sum_re_inner_orthonormalBasis_self_eq_sum_eigenvalues {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (e : OrthonormalBasis (Fin n) 𝕜 E) : ∑ k : Fin n, RCLike.re (inner 𝕜 (T (e k)) (e k)) = ∑ i : Fin n, hT.eigenvalues hn i

Basis independence of the trace (the equality case of Schur majorization). The sum of the diagonal entries of T in any orthonormal basis equals the sum of its eigenvalues. No convexity needed.

theorem TauCeti.sum_sq_re_inner_orthonormalBasis_self_le_sum_sq_eigenvalues {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (e : OrthonormalBasis (Fin n) 𝕜 E) : ∑ k : Fin n, RCLike.re (inner 𝕜 (T (e k)) (e k)) ^ 2 ≤ ∑ i : Fin n, hT.eigenvalues hn i ^ 2

Sum-of-squares bound (the φ = (·)² instance of Schur majorization). The diagonal of T in any orthonormal basis has Euclidean length no larger than the spectrum: ∑ k, (re ⟪T (e k), e k⟫)² ≤ ∑ i, (λ i)².