orthogonalComplement_iSup_eigenspaces

English

The orthogonal complement of the iSup of all eigenspaces is the zero subspace.

Русский

Ортогональное дополнение iSup всех эйгенпространств равно нулевому подпространству.

LaTeX

$$$$ (\bigoplus_{\mu} \mathrm{Eig}(T,\mu))^{\perp} = \{0\}. $$$$

Lean4

/-- The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on an inner
product space has no eigenvalues. -/
theorem orthogonalComplement_iSup_eigenspaces (hT : T.IsSymmetric) (μ : 𝕜) :
    eigenspace (T.restrict hT.orthogonalComplement_iSup_eigenspaces_invariant) μ = ⊥ :=
  by
  set p : Submodule 𝕜 E := (⨆ μ, eigenspace T μ)ᗮ
  refine eigenspace_restrict_eq_bot hT.orthogonalComplement_iSup_eigenspaces_invariant ?_
  have H₂ : eigenspace T μ ⟂ p := (Submodule.isOrtho_orthogonal_right _).mono_left (le_iSup _ _)
  exact H₂.disjoint

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