English
The orthogonal complement of the sum of eigenspaces is invariant under T.
Русский
Ортогональное дополнение суммы собственных подпространств инвариантно относительно T.
LaTeX
$$$$ T(\mathrm{Eig}(T,\mu)^{\perp}) \subseteq \mathrm{Eig}(T,\mu)^{\perp} \quad \forall \mu. $$$$
Lean4
/-- *Diagonalization theorem*, *spectral theorem*; version 1: A self-adjoint operator `T` on a
finite-dimensional inner product space `E` acts diagonally on the decomposition of `E` into the
direct sum of the eigenspaces of `T`. -/
theorem diagonalization_apply_self_apply (hT : T.IsSymmetric) (v : E) (μ : Eigenvalues T) :
hT.diagonalization (T v) μ = (μ : 𝕜) • hT.diagonalization v μ :=
by
suffices
∀ w : PiLp 2 fun μ : Eigenvalues T => eigenspace T μ,
T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => (μ : 𝕜) • w μ
by
simpa only [LinearIsometryEquiv.symm_apply_apply, LinearIsometryEquiv.apply_symm_apply] using
congr_arg (fun w => hT.diagonalization w μ) (this (hT.diagonalization v))
intro w
have hwT : ∀ μ, T (w μ) = (μ : 𝕜) • w μ := fun μ => mem_eigenspace_iff.1 (w μ).2
simp only [hwT, diagonalization_symm_apply, map_sum, Submodule.coe_smul_of_tower]
