orthogonalComplement_iSup_eigenspaces_eq_bot

English

The mutual orthogonal complement of the eigenspaces is invariant and trivial on finite-dimensional spaces.

Русский

Общее ортогональное дополнение собственных подпространств инвариантно и тривиально на конечномерных пространствах.

LaTeX

$$$$ (\mathrm{Eig}(T,\mu))^{\perp} \\text{ preserves under } T, \; \forall \mu. $$$$

Lean4

/-- The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on a
finite-dimensional inner product space is trivial. -/
theorem orthogonalComplement_iSup_eigenspaces_eq_bot (hT : T.IsSymmetric) : (⨆ μ, eigenspace T μ)ᗮ = ⊥ :=
  by
  have hT' : IsSymmetric _ := hT.restrict_invariant hT.orthogonalComplement_iSup_eigenspaces_invariant
  haveI := hT'.subsingleton_of_no_eigenvalue_finiteDimensional hT.orthogonalComplement_iSup_eigenspaces
  exact Submodule.eq_bot_of_subsingleton

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