English
The eigenspaces of a self-adjoint operator on a finite-dimensional inner product space give an internal direct sum decomposition of E.
Русский
Собственные пространства самосопряжённого оператора на конечномерном пространстве образуют внутреннее разложение по прямым суммам для E.
LaTeX
$$$$ E = \bigoplus_{\mu} \mathrm{Eig}(T,\mu). $$$$
Lean4
/-- The eigenspaces of a self-adjoint operator on a finite-dimensional inner product space `E` gives
an internal direct sum decomposition of `E`.
Note this takes `hT` as a `Fact` to allow it to be an instance. -/
noncomputable instance directSumDecomposition [hT : Fact T.IsSymmetric] :
DirectSum.Decomposition fun μ : Eigenvalues T => eigenspace T μ :=
haveI h : ∀ μ : Eigenvalues T, CompleteSpace (eigenspace T μ) := fun μ => by infer_instance
hT.out.orthogonalFamily_eigenspaces'.decomposition
(Submodule.orthogonal_eq_bot_iff.mp hT.out.orthogonalComplement_iSup_eigenspaces_eq_bot')
