Continuity of ordered Hermitian eigenvalues

The decreasing eigenvalue list of a Hermitian matrix is 1-Lipschitz from the Euclidean operator norm to the sup norm on the list. In particular it is continuous, including at repeated eigenvalues, and measurable for the entrywise Borel structure on matrices. These results allow eigenvalues of a measurable random Hermitian matrix to be treated as random variables, without choosing measurable eigenvectors.

We use the subtype of Hermitian matrices, with its inherited topology and measurable structure. Continuity uses the usual entrywise topology: Mathlib's Euclidean operator norm induces this same topology. Empty index types are allowed.

References

• R. Bhatia, Matrix Analysis, Springer (1997), Chapter III, for Weyl's perturbation bound and continuity of ordered eigenvalues.

theorem Matrix.lipschitzWith_eigenvalues₀ {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] : LipschitzWith 1 fun (A : { A : Matrix n n 𝕜 // A.IsHermitian }) => ⋯.eigenvalues₀

The decreasing eigenvalue list is 1-Lipschitz for the Euclidean operator norm on Hermitian matrices and the sup norm on the eigenvalue list.

theorem Matrix.continuous_eigenvalues₀ {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] : Continuous fun (A : { A : Matrix n n 𝕜 // A.IsHermitian }) => ⋯.eigenvalues₀

Ordered Hermitian eigenvalues depend continuously on the matrix, even at repeated eigenvalues.

theorem Matrix.continuous_eigenvalues {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] : Continuous fun (A : { A : Matrix n n 𝕜 // A.IsHermitian }) => ⋯.eigenvalues

Mathlib's matrix-indexed eigenvalue list is continuous on Hermitian matrices.

theorem Matrix.measurable_eigenvalues₀ {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] [MeasurableSpace 𝕜] [BorelSpace 𝕜] : Measurable fun (A : { A : Matrix n n 𝕜 // A.IsHermitian }) => ⋯.eigenvalues₀

The ordered eigenvalue list of a Hermitian matrix is measurable for the entrywise Borel structure.

theorem Matrix.measurable_eigenvalues {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] [MeasurableSpace 𝕜] [BorelSpace 𝕜] : Measurable fun (A : { A : Matrix n n 𝕜 // A.IsHermitian }) => ⋯.eigenvalues

Mathlib's matrix-indexed eigenvalue list is measurable on Hermitian matrices.