orthogonalComplement_iSup_eigenspaces_invariant

English

The operator restricted to the orthogonal complement of the eigenspaces has no eigenvalues.

Русский

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

LaTeX

$$$$ \forall \mu, \; \operatorname{Eig}(T|_{V}, \mu) = \{0\}, \; V = \mathrm{Eig}(T,\cdot)^{\perp}. $$$$

Lean4

/-- The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on an inner
product space is an invariant subspace of the operator. -/
theorem orthogonalComplement_iSup_eigenspaces_invariant (hT : T.IsSymmetric) ⦃v : E⦄ (hv : v ∈ (⨆ μ, eigenspace T μ)ᗮ) :
    T v ∈ (⨆ μ, eigenspace T μ)ᗮ := by
  rw [← Submodule.iInf_orthogonal] at hv ⊢
  exact T.iInf_invariant hT.invariant_orthogonalComplement_eigenspace v hv

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