The spectral theorem for compact normal operators

A bounded operator T on a Hilbert space is normal when it commutes with its adjoint, IsStarNormal T. Mathlib's spectral theorem for compact self-adjoint operators (ContinuousLinearMap.orthogonalComplement_iSup_eigenspaces_eq_bot) says that their eigenspaces have trivial mutual orthogonal complement. This file extends it to compact normal operators on complex Hilbert spaces.

Eigenspaces of normal operators. The eigenspaces of a normal operator are mutually orthogonal (IsStarNormal.orthogonalFamily_eigenspaces), and the orthogonal complement of all of them is invariant under both T and T†. Over ℂ, the eigenspace of T at μ is the joint eigenspace of its real part ℜ T at re μ and its imaginary part ℑ T at im μ. These general facts live in TauCeti.Analysis.InnerProductSpace.NormalOperator.

Compact normal operators. In a C⋆-algebra the spectral radius of a normal element is its norm, and the nonzero spectral values of a compact operator are eigenvalues; hence a compact normal operator on a complex Hilbert space whose only eigenvalue is 0 vanishes (IsStarNormal.forall_hasEigenvalue_eq_zero_iff). Restricting a compact normal T to the orthogonal complement of its eigenspaces gives a compact normal operator without eigenvalues, so that complement is trivial: the eigenspaces of a compact normal operator span a dense subspace (IsStarNormal.orthogonalComplement_iSup_eigenspaces_eq_bot). This argument follows Mathlib's proof of the self-adjoint case. The same statement for the joint eigenspaces of ℜ T and ℑ T is the simultaneous diagonalization of these two commuting self-adjoint operators. It follows that a compact normal operator has a Hilbert basis of eigenvectors, and that the closure of the span of its eigenspaces at nonzero eigenvalues is the orthogonal complement of its kernel, so E = ker T ⊕ closure (⨆_{μ ≠ 0} E_μ).

The statements are specific to complex scalars: a rotation of the real plane is a compact normal operator without eigenvectors.

Main results

• IsStarNormal.orthogonalComplement_iSup_eigenspaces_eq_bot: the spectral theorem for compact normal operators, the eigenspaces have trivial mutual orthogonal complement.
• IsStarNormal.orthogonalComplement_iSup_iSup_eigenspace_inf_eigenspace_eq_bot: the joint eigenspaces of the real and imaginary parts have trivial mutual orthogonal complement.
• IsStarNormal.exists_hilbertBasis_forall_hasEigenvector: a compact normal operator has a Hilbert basis of eigenvectors.
• IsStarNormal.isCompl_ker_topologicalClosure_iSup_eigenspaces_ne_zero: the kernel and the closed span of the eigenspaces at nonzero eigenvalues are complementary.

References

• J. B. Conway, A Course in Functional Analysis, 2nd ed., Springer GTM 96 (1990), Section II.7 (the spectral theorem for compact normal operators).

theorem IsStarNormal.forall_hasEigenvalue_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {T : E →L[ℂ] E} (hT : IsStarNormal T) (hc : IsCompactOperator ⇑T) : (∀ (μ : ℂ), Module.End.HasEigenvalue (↑T) μ → μ = 0) ↔ T = 0

A compact normal operator on a complex Hilbert space is zero exactly when its only eigenvalue is zero.

theorem IsStarNormal.orthogonalComplement_iSup_eigenspaces_eq_bot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {T : E →L[ℂ] E} (hT : IsStarNormal T) (hc : IsCompactOperator ⇑T) : (⨆ (μ : ℂ), Module.End.eigenspace (↑T) μ)ᗮ = ⊥

The spectral theorem for compact normal operators: the eigenspaces of a compact normal operator on a complex Hilbert space have trivial mutual orthogonal complement.

theorem IsStarNormal.orthogonalComplement_iSup_iSup_eigenspace_inf_eigenspace_eq_bot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {T : E →L[ℂ] E} (hT : IsStarNormal T) (hc : IsCompactOperator ⇑T) : (⨆ (a : ℂ), ⨆ (b : ℂ), Module.End.eigenspace (↑↑(realPart T)) a ⊓ Module.End.eigenspace (↑↑(imaginaryPart T)) b)ᗮ = ⊥

Simultaneous diagonalization of the real and imaginary parts of a compact normal operator: their joint eigenspaces have trivial mutual orthogonal complement.

theorem IsStarNormal.exists_hilbertBasis_forall_hasEigenvector {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {T : E →L[ℂ] E} (hT : IsStarNormal T) (hc : IsCompactOperator ⇑T) : ∃ (s : Set E) (b : HilbertBasis ↑s ℂ E) (nu : ↑s → ℂ), ⇑b = Subtype.val ∧ ∀ (x : ↑s), Module.End.HasEigenvector (↑T) (nu x) ↑x

A compact normal operator on a complex Hilbert space has an orthonormal basis of eigenvectors. The basis is indexed by a set of vectors of E, and no separability is assumed.

theorem IsStarNormal.orthogonalComplement_iSup_eigenspaces_ne_zero_eq_ker {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {T : E →L[ℂ] E} (hT : IsStarNormal T) (hc : IsCompactOperator ⇑T) : (⨆ (μ : ℂ), ⨆ (_ : μ ≠ 0), Module.End.eigenspace (↑T) μ)ᗮ = (↑T).ker

For a compact normal operator on a complex Hilbert space, the vectors orthogonal to every eigenspace at a nonzero eigenvalue form the kernel.

theorem IsStarNormal.topologicalClosure_iSup_eigenspaces_ne_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {T : E →L[ℂ] E} (hT : IsStarNormal T) (hc : IsCompactOperator ⇑T) : (⨆ (μ : ℂ), ⨆ (_ : μ ≠ 0), Module.End.eigenspace (↑T) μ).topologicalClosure = (↑T).kerᗮ

For a compact normal operator on a complex Hilbert space, the closed span of the eigenspaces at nonzero eigenvalues is the orthogonal complement of the kernel.

theorem IsStarNormal.isCompl_ker_topologicalClosure_iSup_eigenspaces_ne_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {T : E →L[ℂ] E} (hT : IsStarNormal T) (hc : IsCompactOperator ⇑T) : IsCompl (↑T).ker (⨆ (μ : ℂ), ⨆ (_ : μ ≠ 0), Module.End.eigenspace (↑T) μ).topologicalClosure

A complex Hilbert space is the direct sum of the kernel of a compact normal operator and the closed span of its eigenspaces at nonzero eigenvalues.