Unitary diagonalization of normal matrices

A complex square matrix A is normal when it commutes with its conjugate transpose, IsStarNormal A. The spectral theorem for normal matrices says that such a matrix is unitarily diagonalizable: star U * A * U is diagonal for some unitary U. Mathlib proves this for Hermitian matrices (Matrix.IsHermitian.spectral_theorem); this file extends it to normal ones, by reading the spectral theorem for normal operators (LinearMap.exists_orthonormalBasis_apply_eq_smul_of_isStarNormal) in the standard basis of EuclideanSpace ℂ n. The columns of U are an orthonormal basis of eigenvectors of A.

Unitary matrices are normal, so in particular every unitary matrix is conjugate within the unitary group to a diagonal one. This is the statement that every element of U(n) lies in a conjugate of the diagonal torus.

Main results

• Matrix.isStarNormal_toEuclideanLin: a normal matrix acts on EuclideanSpace 𝕜 n as a normal operator.
• Matrix.exists_mem_unitaryGroup_star_mul_mul_eq_diagonal: the spectral theorem for normal matrices, a normal complex matrix is diagonalized by a unitary matrix.

References

• S. Axler, Linear Algebra Done Right, 3rd ed., Springer (2015), Theorem 7.24 (the complex spectral theorem).

instance Matrix.isStarNormal_toEuclideanLin {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (A : Matrix n n 𝕜) [IsStarNormal A] : IsStarNormal (toEuclideanLin A)

The operator of a normal matrix on EuclideanSpace 𝕜 n is normal.

theorem Matrix.exists_mem_unitaryGroup_star_mul_mul_eq_diagonal {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) [IsStarNormal A] : ∃ U ∈ unitaryGroup n ℂ, ∃ (d : n → ℂ), star U * A * U = diagonal d

The spectral theorem for normal matrices. A normal complex matrix is unitarily diagonalizable: there is a unitary matrix U with star U * A * U diagonal.