The spectral theorem for normal operators

A linear operator T on a finite-dimensional complex inner product space is normal when it commutes with its adjoint, IsStarNormal T. The spectral theorem says that T is then diagonalized by an orthonormal basis: there is an orthonormal basis of eigenvectors of T. Mathlib proves this for symmetric (self-adjoint) operators, LinearMap.IsSymmetric.eigenvectorBasis; this file extends it to normal ones.

The proof splits T into its real and imaginary parts, T = ℜ T + i • ℑ T, which are self-adjoint and, exactly because T is normal, commute (isStarNormal_iff_commute_realPart_imaginaryPart). Two commuting self-adjoint operators are simultaneously diagonalizable: the space is the orthogonal direct sum of their joint eigenspaces (LinearMap.IsSymmetric.directSum_isInternal_of_commute). On the joint eigenspace where ℜ T acts by a and ℑ T by b, the operator T acts by a + i b, so an orthonormal basis subordinate to this decomposition consists of eigenvectors of T.

Unlike the self-adjoint case, the eigenvalues are complex, and the statement is specific to complex scalars: a rotation of the real plane is normal but has no real eigenvector.

Main results

• LinearMap.apply_eq_smul_of_mem_eigenspace_realPart_imaginaryPart: on a joint eigenspace of ℜ T and ℑ T with eigenvalues a and b, the operator T acts by a + i b.
• LinearMap.exists_orthonormalBasis_apply_eq_smul_of_isStarNormal: the spectral theorem for normal operators, a normal operator on a finite-dimensional complex inner product space has an orthonormal basis of eigenvectors, indexed by any finite type of the right cardinality.

References

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

theorem LinearMap.apply_eq_smul_of_mem_eigenspace_realPart_imaginaryPart {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (T : E →ₗ[ℂ] E) {a b : ℂ} {v : E} (ha : v ∈ Module.End.eigenspace (↑(realPart T)) a) (hb : v ∈ Module.End.eigenspace (↑(imaginaryPart T)) b) : T v = (a + Complex.I * b) • v

On a joint eigenspace of the real and imaginary parts of T, where ℜ T acts by a and ℑ T by b, the operator T acts by a + i b. Normality is not needed here; finite dimensionality only enters because the adjoint, hence ℜ T and ℑ T, is defined on finite-dimensional spaces.

theorem LinearMap.exists_orthonormalBasis_apply_eq_smul_of_isStarNormal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (T : E →ₗ[ℂ] E) [IsStarNormal T] {ι : Type u_2} [Fintype ι] (hι : Fintype.card ι = Module.finrank ℂ E) : ∃ (b : OrthonormalBasis ι ℂ E) (μ : ι → ℂ), ∀ (i : ι), T (b i) = μ i • b i

The spectral theorem for normal operators. A normal operator on a finite-dimensional complex inner product space has an orthonormal basis of eigenvectors. The basis may be indexed by any finite type whose cardinality is the dimension of the space.