orthogonalFamily_eigenspaces — Mathlib

English

The eigenspaces of a self-adjoint operator form an orthogonal family.

Русский

Собственные пространства самосопряжённого оператора образуют ортогональную семью.

LaTeX

$$$$ \text{For all } \mu,\nu, \; \mu\neq \nu, \; \mathrm{Eig}(T,\mu) \perp \mathrm{Eig}(T,\nu). $$$$

Lean4

/-- The eigenspaces of a self-adjoint operator are mutually orthogonal. -/
theorem orthogonalFamily_eigenspaces (hT : T.IsSymmetric) :
    OrthogonalFamily 𝕜 (fun μ => eigenspace T μ) fun μ => (eigenspace T μ).subtypeₗᵢ :=
  by
  rintro μ ν hμν ⟨v, hv⟩ ⟨w, hw⟩
  by_cases hv' : v = 0
  · simp [hv']
  have H := hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector ⟨hv, hv'⟩)
  rw [mem_eigenspace_iff] at hv hw
  refine Or.resolve_left ?_ hμν.symm
  simpa [inner_smul_left, inner_smul_right, hv, hw, H] using (hT v w).symm

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