English
Let A and B be commuting symmetric linear operators on a finite-dimensional inner product space. Then every vector lies in a simultaneous eigenspace, i.e. the space is the sum of the intersections eigenspace(A, α) ∩ eigenspace(B, γ) over all eigenvalues α, γ.
Русский
Пусть A и B — сопряженные симметричные линейные отображения на конечномерном внутреннем произведении. Тогда пространство распадается на общие собственные пространства: любое вектор лежит в пересечении собственных пространств Eig(A, α) ∩ Eig(B, γ) для некоторых α, γ, и собранные такие пересечения образуют полный прямой разлож.
LaTeX
$$$\displaystyle \bigvee_{\alpha \in \mathbb{K}}\bigvee_{\gamma \in \mathbb{K}} \operatorname{Eig}(A, \alpha) \cap \operatorname{Eig}(B, \gamma) = \top$$$
Lean4
/-- If A and B are commuting symmetric operators acting on a finite-dimensional inner product space,
then the simultaneous eigenspaces of A and B exhaust the space. -/
theorem iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute (hA : A.IsSymmetric) (hB : B.IsSymmetric)
(hAB : Commute A B) : (⨆ α, ⨆ γ, eigenspace A α ⊓ eigenspace B γ) = ⊤ := by
simpa [iSup_eigenspace_inf_eigenspace_of_commute hB hAB] using
Submodule.orthogonal_eq_bot_iff.mp <| hA.orthogonalComplement_iSup_eigenspaces_eq_bot
