The Schur–Horn theorem

Let T be a symmetric endomorphism of a finite-dimensional inner product space over ℝ or ℂ, with eigenvalues λᵢ and orthonormal eigenbasis (vᵢ), and let (eₖ) be any orthonormal basis. The diagonal entries dₖ = Re⟪T eₖ, eₖ⟫ of T in the basis (eₖ) are averages of the eigenvalues:

dₖ = ∑ᵢ wᵢₖ λᵢ, where wᵢₖ = ‖⟪vᵢ, eₖ⟫‖².

The Schur weight matrix w of two orthonormal bases is doubly stochastic: its entries are nonnegative, and each row and each column sums to 1 by Parseval's identity. So the diagonal is the image of the spectrum under a doubly stochastic matrix, and Jensen's inequality gives the forward Schur–Horn inequality in Karamata form: for every convex φ,

∑ₖ φ(dₖ) ≤ ∑ᵢ φ(λᵢ).

By Birkhoff's theorem the doubly stochastic matrices are the convex combinations of permutation matrices, so the diagonal lies in the convex hull of the rearrangements of the spectrum.

The case φ = x² says that the Euclidean norm of the diagonal is at most that of the spectrum. The sum of the diagonal entries is the trace, so it equals the sum of the eigenvalues in every orthonormal basis.

Conversely (Horn), every point of that convex hull is the diagonal of T in some orthonormal basis. Rotating two basis vectors eᵢ, eⱼ in the plane they span moves the diagonal entry at i continuously from dᵢ to dⱼ while keeping dᵢ + dⱼ and the other entries fixed, so the diagonals of T are closed under Robin Hood transfers. Since they contain the spectrum, the transfer closure theorem of TauCeti.Analysis.Convex.Majorization and Rado's description of the permutohedron by majorization show that they fill the convex hull. Thus the diagonals of T are exactly the tuples majorized by its spectrum.

Main definitions

• OrthonormalBasis.schurWeight v e: the matrix of squared overlaps ‖⟪v i, e k⟫‖² of two orthonormal bases.

Main results

• OrthonormalBasis.sum_schurWeight_row, OrthonormalBasis.sum_schurWeight_col: the rows and columns of a Schur weight matrix sum to 1.
• OrthonormalBasis.schurWeight_mem_doublyStochastic: a Schur weight matrix of two orthonormal bases with a common index type is doubly stochastic.
• LinearMap.IsSymmetric.re_inner_apply_self_eq_sum_schurWeight_mul_eigenvalues: the diagonal entries of a symmetric operator are Schur-weighted averages of its eigenvalues; LinearMap.IsSymmetric.re_inner_apply_self_eq_schurWeight_mulVec_eigenvalues is the same statement as a matrix-vector product.
• LinearMap.IsSymmetric.re_inner_apply_self_mem_convexHull_eigenvalues_comp_perm: by Birkhoff's theorem, the diagonal lies in the convex hull of the rearrangements of the spectrum.
• LinearMap.IsSymmetric.sum_map_re_inner_apply_self_le_sum_map_eigenvalues: the forward Schur–Horn inequality ∑ₖ φ(dₖ) ≤ ∑ᵢ φ(λᵢ) for convex φ.
• LinearMap.IsSymmetric.sum_re_inner_apply_self_eq_sum_eigenvalues: the diagonal entries sum to the sum of the eigenvalues in every orthonormal basis.
• LinearMap.IsSymmetric.sum_sq_re_inner_apply_self_le_sum_sq_eigenvalues: ∑ₖ dₖ² ≤ ∑ᵢ λᵢ².
• LinearMap.IsSymmetric.sum_mul_re_inner_apply_self_le_sum_mul_eigenvalues: for a decreasing weight sequence c, ∑ₖ cₖ dₖ ≤ ∑ₖ cₖ λₖ, with the eigenvalues listed in decreasing order.
• LinearMap.IsSymmetric.exists_orthonormalBasis_re_inner_apply_self_eq_robinHood: a rotation in a coordinate plane realizes any Robin Hood transfer from a diagonal entry to a smaller one.
• LinearMap.IsSymmetric.exists_orthonormalBasis_re_inner_apply_self_eq_of_mem_convexHull: Horn's theorem, every point of the permutohedron of the spectrum is a diagonal of T.
• LinearMap.IsSymmetric.range_re_inner_apply_self_eq_convexHull_eigenvalues_comp_perm: the Schur–Horn theorem, the diagonals of T are exactly the permutohedron of its spectrum.
• LinearMap.IsSymmetric.exists_orthonormalBasis_re_inner_apply_self_eq_iff: the Schur–Horn theorem in majorization form.

References

• I. Schur, Über eine Klasse von Mittelbildungen mit Anwendungen auf die Determinantentheorie, Sitzungsber. Berl. Math. Ges. 22 (1923), 9–20.
• A. Horn, Doubly stochastic matrices and the diagonal of a rotation matrix, Amer. J. Math. 76 (1954), 620–630.
• A. W. Marshall, I. Olkin, B. C. Arnold, Inequalities: Theory of Majorization and Its Applications, 2nd ed., Springer (2011), Theorems 9.B.1 and 9.B.2.
• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer (1997), §II.1.

noncomputable def OrthonormalBasis.schurWeight {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} {κ : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype κ] (v : OrthonormalBasis ι 𝕜 E) (e : OrthonormalBasis κ 𝕜 E) : Matrix ι κ ℝ

The Schur weight matrix of two orthonormal bases v and e: its (i, k) entry is the squared overlap ‖⟪v i, e k⟫‖². When v is an eigenbasis of a symmetric operator, it expresses the diagonal of the operator in the basis e as an average of the eigenvalues.

@[simp]

theorem OrthonormalBasis.schurWeight_apply {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} {κ : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype κ] (v : OrthonormalBasis ι 𝕜 E) (e : OrthonormalBasis κ 𝕜 E) (i : ι) (k : κ) : v.schurWeight e i k = ‖inner 𝕜 (v i) (e k)‖ ^ 2

theorem OrthonormalBasis.schurWeight_nonneg {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} {κ : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype κ] (v : OrthonormalBasis ι 𝕜 E) (e : OrthonormalBasis κ 𝕜 E) (i : ι) (k : κ) : 0 ≤ v.schurWeight e i k

theorem OrthonormalBasis.transpose_schurWeight {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} {κ : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype κ] (v : OrthonormalBasis ι 𝕜 E) (e : OrthonormalBasis κ 𝕜 E) : (v.schurWeight e).transpose = e.schurWeight v

Exchanging the two bases transposes the Schur weight matrix.

theorem OrthonormalBasis.sum_schurWeight_row {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} {κ : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype κ] (v : OrthonormalBasis ι 𝕜 E) (e : OrthonormalBasis κ 𝕜 E) (i : ι) : ∑ k : κ, v.schurWeight e i k = 1

Each row of a Schur weight matrix sums to 1.

theorem OrthonormalBasis.sum_schurWeight_col {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} {κ : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype κ] (v : OrthonormalBasis ι 𝕜 E) (e : OrthonormalBasis κ 𝕜 E) (k : κ) : ∑ i : ι, v.schurWeight e i k = 1

Each column of a Schur weight matrix sums to 1.

theorem OrthonormalBasis.schurWeight_mem_doublyStochastic {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (v e : OrthonormalBasis ι 𝕜 E) : v.schurWeight e ∈ doublyStochastic ℝ ι

The Schur weight matrix of two orthonormal bases with a common index type is doubly stochastic.

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

The diagonal of a symmetric operator is a Schur-weighted average of its spectrum. For every orthonormal basis e, the diagonal entry Re⟪T (e k), e k⟫ equals ∑ᵢ wᵢₖ λᵢ, where w is the Schur weight matrix of the eigenbasis of T and e.

theorem LinearMap.IsSymmetric.re_inner_apply_self_eq_schurWeight_mulVec_eigenvalues {𝕜 : Type u_1} {E : Type u_2} {κ : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype κ] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (e : OrthonormalBasis κ 𝕜 E) : (fun (k : κ) => RCLike.re (inner 𝕜 (T (e k)) (e k))) = (e.schurWeight (hT.eigenvectorBasis hn)).mulVec (hT.eigenvalues hn)

The diagonal of a symmetric operator is the image of its spectrum under a Schur weight matrix. For every orthonormal basis e, the vector of diagonal entries Re⟪T (e k), e k⟫ is w *ᵥ λ, where w is the Schur weight matrix of e and the eigenbasis of T.

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

Forward Schur–Horn inequality, Karamata form. If φ is convex on a set s containing the eigenvalues of a symmetric operator T, then for every orthonormal basis e, the sum of φ over the diagonal entries Re⟪T (e k), e k⟫ is at most the sum of φ over the eigenvalues.

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

The trace in an orthonormal basis. For every orthonormal basis e, the diagonal entries Re⟪T (e k), e k⟫ of a symmetric operator sum to the sum of its eigenvalues.

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

The diagonal is shorter than the spectrum. For every orthonormal basis e, the squared diagonal entries Re⟪T (e k), e k⟫ of a symmetric operator sum to at most the sum of the squared eigenvalues.

theorem LinearMap.IsSymmetric.re_inner_apply_self_mem_convexHull_eigenvalues_comp_perm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (e : OrthonormalBasis (Fin n) 𝕜 E) : (fun (k : Fin n) => RCLike.re (inner 𝕜 (T (e k)) (e k))) ∈ (convexHull ℝ) (Set.range fun (σ : Equiv.Perm (Fin n)) => hT.eigenvalues hn ∘ ⇑σ)

The diagonal lies in the permutohedron of the spectrum. For every orthonormal basis e indexed by Fin n, the vector of diagonal entries Re⟪T (e k), e k⟫ of a symmetric operator T lies in the convex hull of the rearrangements λ ∘ σ of its eigenvalues.

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

Sorted weights of the diagonal. For a symmetric T, an orthonormal basis e, and a decreasing weight sequence c, the c-weighted sum of the diagonal entries Re⟪T eₖ, eₖ⟫ is at most the c-weighted sum of the eigenvalues of T, listed in decreasing order.

The converse: Horn's theorem

theorem LinearMap.IsSymmetric.exists_orthonormalBasis_re_inner_apply_self_eq_robinHood {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {T : E →ₗ[𝕜] E} [DecidableEq ι] (hT : T.IsSymmetric) (e : OrthonormalBasis ι 𝕜 E) (i j : ι) {δ : ℝ} (hδ : 0 ≤ δ) (hδ' : δ ≤ RCLike.re (inner 𝕜 (T (e i)) (e i)) - RCLike.re (inner 𝕜 (T (e j)) (e j))) : ∃ (e' : OrthonormalBasis ι 𝕜 E), (fun (k : ι) => RCLike.re (inner 𝕜 (T (e' k)) (e' k))) = TauCeti.robinHood (fun (k : ι) => RCLike.re (inner 𝕜 (T (e k)) (e k))) i j δ

A plane rotation realizes a Robin Hood transfer of the diagonal. Let dₖ = Re⟪T eₖ, eₖ⟫ be the diagonal of a symmetric operator T in an orthonormal basis e. For 0 ≤ δ ≤ dᵢ - dⱼ, rotating eᵢ and eⱼ in the plane they span gives an orthonormal basis in which the diagonal of T is robinHood d i j δ: the entry at i drops by δ, the entry at j rises by δ, and the other entries are unchanged.

theorem LinearMap.IsSymmetric.exists_orthonormalBasis_re_inner_apply_self_eq_of_mem_convexHull {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} [FiniteDimensional 𝕜 E] (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {d : Fin n → ℝ} (hd : d ∈ (convexHull ℝ) (Set.range fun (σ : Equiv.Perm (Fin n)) => hT.eigenvalues hn ∘ ⇑σ)) : ∃ (e : OrthonormalBasis (Fin n) 𝕜 E), ∀ (k : Fin n), RCLike.re (inner 𝕜 (T (e k)) (e k)) = d k

Horn's theorem. Every point d of the convex hull of the rearrangements of the spectrum of a symmetric operator T is the diagonal of T in some orthonormal basis: there is an orthonormal basis e with Re⟪T eₖ, eₖ⟫ = dₖ for every k.

theorem LinearMap.IsSymmetric.range_re_inner_apply_self_eq_convexHull_eigenvalues_comp_perm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} [FiniteDimensional 𝕜 E] (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) : (Set.range fun (e : OrthonormalBasis (Fin n) 𝕜 E) (k : Fin n) => RCLike.re (inner 𝕜 (T (e k)) (e k))) = (convexHull ℝ) (Set.range fun (σ : Equiv.Perm (Fin n)) => hT.eigenvalues hn ∘ ⇑σ)

The Schur–Horn theorem. The diagonals (Re⟪T eₖ, eₖ⟫)ₖ of a symmetric operator T in the orthonormal bases e indexed by Fin n form exactly the convex hull of the rearrangements of the spectrum of T.

theorem LinearMap.IsSymmetric.exists_orthonormalBasis_re_inner_apply_self_eq_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} [FiniteDimensional 𝕜 E] (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {d : Fin n → ℝ} : (∃ (e : OrthonormalBasis (Fin n) 𝕜 E), ∀ (k : Fin n), RCLike.re (inner 𝕜 (T (e k)) (e k)) = d k) ↔ (∀ (k : ℕ), TauCeti.prefixSum k (d ∘ ⇑(Tuple.sortDesc d)) ≤ TauCeti.prefixSum k (hT.eigenvalues hn)) ∧ ∑ i : Fin n, d i = ∑ i : Fin n, hT.eigenvalues hn i

The Schur–Horn theorem, majorization form. A real tuple d is the diagonal (Re⟪T eₖ, eₖ⟫)ₖ of a symmetric operator T in some orthonormal basis e exactly when d is majorized by the spectrum of T: the prefix sums of the decreasing rearrangement of d are at most the corresponding sums of the largest eigenvalues, and the sum of d is the trace.