direct_sum_isInternal — Mathlib

English

There exists an orthonormal basis of eigenvectors for T, provided by the diagonalization construction for a self-adjoint operator on a finite-dimensional space.

Русский

Существует ортонормированный базис собственных векторов для T, получаемый диагонализацией самосопряжённого оператора на конечномерном пространстве.

LaTeX

$$$$ \text{There exists an orthonormal basis } \{v_i\} \text{ of eigenvectors with } T v_i = \lambda_i v_i. $$$$

Lean4

/-- The eigenspaces of a self-adjoint operator on a finite-dimensional inner product space `E` gives
an internal direct sum decomposition of `E`. -/
theorem direct_sum_isInternal (hT : T.IsSymmetric) : DirectSum.IsInternal fun μ : Eigenvalues T => eigenspace T μ :=
  hT.orthogonalFamily_eigenspaces'.isInternal_iff.mpr hT.orthogonalComplement_iSup_eigenspaces_eq_bot'

Похожие утверждения