English
If T is a symmetric (self-adjoint) endomorphism on an inner product space and we restrict T to any finite-dimensional subspace, then that restriction is semisimple (i.e., decomposes into a direct sum of its eigenspaces).
Русский
Если T является самосопряжённым концом пространства с внутренним произведением, ограничение T на любом конечномерном подпространстве разлагается на прямую сумму собственных подпространств.
LaTeX
$$$$E ext{ finite-dimensional},\quad T \text{ self-adjoint on } E \Rightarrow E = \bigoplus_{\mu} \mathrm{Eig}(T,\mu), \quad \mathrm{Eig}(T,\mu) \perp \mathrm{Eig}(T,\nu)\ (\mu \neq \nu).$$$$
Lean4
/-- Symmetric operators are semisimple on finite-dimensional subspaces. -/
theorem isFinitelySemisimple : T.IsFinitelySemisimple :=
by
refine
Module.End.isFinitelySemisimple_iff.mpr fun p hp₁ hp₂ q hq₁ hq₂ ↦
⟨qᗮ ⊓ p, inf_le_right, Module.End.invtSubmodule.inf_mem ?_ hp₁, ?_, ?_⟩
· exact orthogonalComplement_mem_invtSubmodule hT hq₁
· simp [disjoint_iff, ← inf_assoc, Submodule.inf_orthogonal_eq_bot q]
· suffices q ⊔ qᗮ = ⊤ by rw [← sup_inf_assoc_of_le _ hq₂, this, top_inf_eq p]
replace hp₂ : Module.Finite 𝕜 q := Submodule.finiteDimensional_of_le hq₂
exact Submodule.sup_orthogonal_of_hasOrthogonalProjection
