Compact self-adjoint operators: spectral theorem (Hilbert basis of eigenvectors)

This file proves the spectral theorem for compact self-adjoint operators on a Hilbert space.

Main results

• iSup_eigenspace_orthogonal_eq_bot_of_isCompactOperator_of_isSelfAdjoint: the (possibly infinite) supremum of eigenspaces is dense (its orthogonal complement is ⊥).
• exists_hilbertBasis_hasEigenvector_of_isCompactOperator_of_isSelfAdjoint: a compact self-adjoint operator admits a HilbertBasis consisting of eigenvectors.

theorem CompactSelfAdjoint.iSup_eigenspace_orthogonal_eq_bot_of_isCompactOperator_of_isSelfAdjoint {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) : (⨆ (μ : 𝕜), Module.End.eigenspace (↑T) μ)ᗮ = ⊥

theorem CompactSelfAdjoint.exists_hilbertBasis_hasEigenvector_of_isCompactOperator_of_isSelfAdjoint {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsSelfAdjoint T) (hTc : IsCompactOperator ⇑T) : ∃ (ι : Type (max u v)) (μ : ι → 𝕜) (b : HilbertBasis ι 𝕜 E), ∀ (i : ι), Module.End.HasEigenvector (↑T) (μ i) (b i)