invariant_orthogonalComplement_eigenspace

English

For a self-adjoint linear operator T, eigen-subspaces corresponding to distinct eigenvalues are mutually orthogonal.

Русский

Для самосопряжённого линейного оператора собственные подпространства, соответствующие различным собственным значениям, взаимно ортогональны.

LaTeX

$$$$ ext{If } \mu \neq \nu, \; \operatorname{Eig}(T,\mu) \perp \operatorname{Eig}(T,\nu). $$$$

Lean4

/-- A self-adjoint operator preserves orthogonal complements of its eigenspaces. -/
theorem invariant_orthogonalComplement_eigenspace (hT : T.IsSymmetric) (μ : 𝕜) (v : E) (hv : v ∈ (eigenspace T μ)ᗮ) :
    T v ∈ (eigenspace T μ)ᗮ := by
  intro w hw
  have : T w = (μ : 𝕜) • w := by rwa [mem_eigenspace_iff] at hw
  simp [← hT w, this, inner_smul_left, hv w hw]

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