Diagonals of unitary orbits: the Schur–Horn theorem for matrices

For a real tuple w, the unitary orbit {U diag(w) Uᴴ | U ∈ U(n)} consists of the Hermitian matrices with spectrum w. Under the pairing ⟨H, X⟩ = -i tr(H X) between Hermitian matrices and the Lie algebra u(n), a diagonal element X = i diag(θ) of the Lie algebra of the diagonal torus pairs with H to ∑ₖ θₖ Hₖₖ (Matrix.neg_I_mul_trace_mul_diagonal_I_mul). So the moment map of the diagonal torus on this orbit sends a matrix to its list of diagonal entries, and the image of this moment map is the set of diagonals of the orbit. This file shows that it is the permutohedron of w, the convex hull of the rearrangements w ∘ σ (Matrix.range_re_diag_unitary_mul_diagonal_mul_star).

The entries of U diag(w) Uᴴ on the diagonal are ∑ᵢ |Uₖᵢ|² wᵢ (Matrix.mul_diagonal_mul_star_apply_self), and the matrix (|Uₖᵢ|²) of a unitary U is doubly stochastic (Matrix.of_norm_sq_mem_doublyStochastic), so by Birkhoff's theorem the diagonal lies in the permutohedron (Schur). Conversely (Horn), every point of the permutohedron is a diagonal of the orbit: the rows of a unitary matrix form an orthonormal basis of EuclideanSpace 𝕜 ι, which turns the operator form of Horn's theorem, LinearMap.IsSymmetric.exists_orthonormalBasis_re_inner_apply_self_eq_of_mem_convexHull, into a statement about unitary matrices. For a Hermitian matrix A, the spectral theorem puts A in the orbit of the diagonal matrix of its eigenvalues, so the diagonals of the matrices U A Uᴴ form the permutohedron of the eigenvalues of A (Matrix.IsHermitian.range_re_diag_unitary_mul_mul_star). Repeated eigenvalues are allowed; they give smaller orbits with the same description of the diagonals.

Two special cases are worked out.

• The orbit of diag(c, 0, …, 0) consists of the matrices c v vᴴ of rank at most one, for unit vectors v (Matrix.mul_diagonal_single_mul_star). When c ≠ 0 it is a copy of the projective space of lines in 𝕜ⁿ: ℂℙⁿ⁻¹ for 𝕜 = ℂ and ℝℙⁿ⁻¹ for 𝕜 = ℝ. Its diagonals form the simplex with vertices c eᵢ, the standard simplex scaled by c (Matrix.range_re_diag_unitary_mul_diagonal_single_mul_star).
• In size two, the explicit real symmetric matrix !![d₁, b; b, d₂] with b = √((l₁ - d₁) (d₁ - l₂)) has characteristic polynomial (X - l₁) (X - l₂) whenever l₂ ≤ d₁ ≤ l₁ and d₁ + d₂ = l₁ + l₂, so it realizes every diagonal majorized by a given pair of eigenvalues; conversely, these inequalities are forced (Matrix.exists_isSymm_fin_two_charpoly_eq_iff).

Main results

• Matrix.neg_I_mul_trace_mul_diagonal_I_mul: the pairing -i tr(H · i diag(θ)) is ∑ₖ θₖ Hₖₖ, so the moment map of the diagonal torus reads off the diagonal.
• Matrix.of_norm_sq_mem_doublyStochastic: the squared moduli of the entries of a unitary matrix form a doubly stochastic matrix.
• Matrix.re_diag_mul_diagonal_mul_star_mem_convexHull: Schur's theorem, the diagonal of U diag(w) Uᴴ lies in the permutohedron of w.
• Matrix.exists_mem_unitaryGroup_re_diag_mul_diagonal_mul_star_eq: Horn's theorem, every point of the permutohedron of w is the diagonal of some U diag(w) Uᴴ.
• Matrix.range_re_diag_unitary_mul_diagonal_mul_star: the diagonals of the unitary orbit of diag(w) form exactly the permutohedron of w.
• Matrix.IsHermitian.range_re_diag_unitary_mul_mul_star: the same for the unitary orbit of a Hermitian matrix and the permutohedron of its eigenvalues.
• Matrix.range_re_diag_unitary_mul_diagonal_single_mul_star: the orbit of diag(c, 0, …, 0) has the simplex with vertices c eᵢ as its diagonals.
• Matrix.exists_isSymm_fin_two_charpoly_eq_iff: the 2 × 2 case, with an explicit matrix.

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.
• M. F. Atiyah, Convexity and commuting Hamiltonians, Bull. London Math. Soc. 14 (1982), 1–15, §1 (the Schur–Horn theorem as a moment-map convexity statement).
• A. Cannas da Silva, Lectures on Symplectic Geometry, Lecture Notes in Mathematics 1764, Springer (2001), §27.

theorem Matrix.neg_I_mul_trace_mul_diagonal_I_mul {ι : Type u_2} [Fintype ι] [DecidableEq ι] (H : Matrix ι ι ℂ) (θ : ι → ℝ) : -Complex.I * (H * diagonal fun (k : ι) => Complex.I * ↑(θ k)).trace = ∑ k : ι, ↑(θ k) * H k k

The diagonal torus reads off the diagonal. Under the pairing ⟨H, X⟩ = -i tr(H X) between Hermitian matrices and u(n), the element X = i diag(θ) of the Lie algebra of the diagonal torus pairs with H to ∑ₖ θₖ Hₖₖ. Hence the moment map of the diagonal torus on a unitary orbit of Hermitian matrices sends a matrix to its diagonal.

Schur's theorem: diagonals lie in the permutohedron

theorem Matrix.mul_diagonal_mul_star_apply_self {𝕜 : Type u_1} {ι : Type u_2} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] (U : Matrix ι ι 𝕜) (w : ι → ℝ) (k : ι) : ((U * diagonal fun (i : ι) => ↑(w i)) * star U) k k = ↑(∑ i : ι, ‖U k i‖ ^ 2 * w i)

The diagonal entries of U diag(w) Uᴴ are the weighted sums ∑ᵢ |Uₖᵢ|² wᵢ of w; when U is unitary these are averages of w.

theorem Matrix.re_mul_diagonal_mul_star_apply_self {𝕜 : Type u_1} {ι : Type u_2} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] (U : Matrix ι ι 𝕜) (w : ι → ℝ) (k : ι) : RCLike.re (((U * diagonal fun (i : ι) => ↑(w i)) * star U) k k) = ∑ i : ι, ‖U k i‖ ^ 2 * w i

The real parts of the diagonal entries of U diag(w) Uᴴ are the weighted sums ∑ᵢ |Uₖᵢ|² wᵢ of w; when U is unitary these are averages of w.

theorem Matrix.of_norm_sq_mem_doublyStochastic {𝕜 : Type u_1} {ι : Type u_2} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] {U : Matrix ι ι 𝕜} (hU : U ∈ unitaryGroup ι 𝕜) : (of fun (k i : ι) => ‖U k i‖ ^ 2) ∈ doublyStochastic ℝ ι

Unitary matrices are unistochastic. The squared moduli |Uₖᵢ|² of the entries of a unitary matrix form a doubly stochastic matrix.

theorem Matrix.re_diag_mul_diagonal_mul_star_mem_convexHull {𝕜 : Type u_1} {ι : Type u_2} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] {U : Matrix ι ι 𝕜} (hU : U ∈ unitaryGroup ι 𝕜) (w : ι → ℝ) : (fun (k : ι) => RCLike.re (((U * diagonal fun (i : ι) => ↑(w i)) * star U) k k)) ∈ (convexHull ℝ) (Set.range fun (σ : Equiv.Perm ι) => w ∘ ⇑σ)

Schur's theorem. For a unitary U, the diagonal of U diag(w) Uᴴ lies in the convex hull of the rearrangements w ∘ σ of w.

Horn's theorem: every point of the permutohedron is a diagonal

theorem Matrix.exists_mem_unitaryGroup_re_diag_mul_diagonal_mul_star_eq {𝕜 : Type u_1} {ι : Type u_2} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] {w d : ι → ℝ} (hd : d ∈ (convexHull ℝ) (Set.range fun (σ : Equiv.Perm ι) => w ∘ ⇑σ)) : ∃ U ∈ unitaryGroup ι 𝕜, ∀ (k : ι), RCLike.re (((U * diagonal fun (i : ι) => ↑(w i)) * star U) k k) = d k

Horn's theorem. Every point d of the convex hull of the rearrangements of w is the diagonal of U diag(w) Uᴴ for some unitary U.

theorem Matrix.range_re_diag_unitary_mul_diagonal_mul_star {𝕜 : Type u_1} {ι : Type u_2} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] (w : ι → ℝ) : (Set.range fun (U : ↥(unitaryGroup ι 𝕜)) (k : ι) => RCLike.re (((↑U * diagonal fun (i : ι) => ↑(w i)) * ↑(star U)) k k)) = (convexHull ℝ) (Set.range fun (σ : Equiv.Perm ι) => w ∘ ⇑σ)

The Schur–Horn theorem. The diagonals of the matrices U diag(w) Uᴴ, for U unitary, form exactly the convex hull of the rearrangements of w. In the language of moment maps: the image of the unitary orbit of diag(w) under the moment map of the diagonal torus is the permutohedron of w.

theorem Matrix.IsHermitian.range_re_diag_unitary_mul_mul_star {𝕜 : Type u_1} {ι : Type u_2} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] {A : Matrix ι ι 𝕜} (hA : A.IsHermitian) : (Set.range fun (U : ↥(unitaryGroup ι 𝕜)) (k : ι) => RCLike.re ((↑U * A * ↑(star U)) k k)) = (convexHull ℝ) (Set.range fun (σ : Equiv.Perm ι) => hA.eigenvalues ∘ ⇑σ)

The Schur–Horn theorem for a Hermitian matrix. The diagonals of the matrices U A Uᴴ, for U unitary, form exactly the convex hull of the rearrangements of the eigenvalues of the Hermitian matrix A.

Orbits of rank at most one and the standard simplex

theorem Matrix.mul_diagonal_single_mul_star {𝕜 : Type u_1} {ι : Type u_2} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] (U : Matrix ι ι 𝕜) (i₀ : ι) (c : ℝ) : (U * diagonal fun (i : ι) => ↑(Pi.single i₀ c i)) * star U = ↑c • vecMulVec (fun (k : ι) => U k i₀) (star fun (k : ι) => U k i₀)

The unitary orbit of diag(0, …, c, …, 0) consists of matrices of rank at most one: U conjugates it to c v vᴴ, where v is the column of U at the position of c.

theorem Matrix.range_re_diag_unitary_mul_diagonal_single_mul_star {𝕜 : Type u_1} {ι : Type u_2} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] (i₀ : ι) (c : ℝ) : (Set.range fun (U : ↥(unitaryGroup ι 𝕜)) (k : ι) => RCLike.re (((↑U * diagonal fun (i : ι) => ↑(Pi.single i₀ c i)) * ↑(star U)) k k)) = (convexHull ℝ) (Set.range fun (i : ι) => Pi.single i c)

The Schur–Horn theorem in rank at most one. The diagonals of the unitary orbit of diag(0, …, c, …, 0), the matrices c v vᴴ for unit vectors v, form the simplex with vertices c eᵢ, the standard simplex scaled by c. For c ≠ 0 this orbit is the projective space of lines in 𝕜ⁿ (ℂℙⁿ⁻¹ when 𝕜 = ℂ), and the simplex is its moment image.

The 2 × 2 case

theorem Matrix.exists_isSymm_fin_two_charpoly_eq_iff {l₁ l₂ d₁ d₂ : ℝ} (hl : l₂ ≤ l₁) : (∃ (A : Matrix (Fin 2) (Fin 2) ℝ), A.IsSymm ∧ A 0 0 = d₁ ∧ A 1 1 = d₂ ∧ A.charpoly = (Polynomial.X - Polynomial.C l₁) * (Polynomial.X - Polynomial.C l₂)) ↔ l₂ ≤ d₁ ∧ d₁ ≤ l₁ ∧ d₁ + d₂ = l₁ + l₂

The 2 × 2 Schur–Horn theorem. For l₂ ≤ l₁, a real symmetric 2 × 2 matrix with diagonal (d₁, d₂) and characteristic polynomial (X - l₁) (X - l₂) exists exactly when (d₁, d₂) is majorized by (l₁, l₂), that is, when l₂ ≤ d₁ ≤ l₁ and d₁ + d₂ = l₁ + l₂. In that case !![d₁, b; b, d₂] with b = √((l₁ - d₁) (d₁ - l₂)) is such a matrix.