English
For a commuting pair of symmetric linear operators on a finite-dimensional inner product space, the space decomposes as an internal direct sum of simultaneous eigenspaces.
Русский
Для пары симметричных коммутирующих отображений на конечномерном внутреннем произведении пространство распадается на внутренний прямой сумма общих собственных пространств.
LaTeX
$$DirectSum.IsInternal (fun (i : 𝕜 × 𝕜) ↦ (eigenspace A i.2 ⊓ eigenspace B i.1))$$
Lean4
/-- Given a commuting pair of symmetric linear operators on a finite-dimensional inner product
space, the space decomposes as an internal direct sum of simultaneous eigenspaces of these
operators. -/
theorem directSum_isInternal_of_commute (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hAB : Commute A B) :
DirectSum.IsInternal (fun (i : 𝕜 × 𝕜) ↦ (eigenspace A i.2 ⊓ eigenspace B i.1)) :=
by
apply (orthogonalFamily_eigenspace_inf_eigenspace hA hB).isInternal_iff.mpr
rw [Submodule.orthogonal_eq_bot_iff, iSup_prod, iSup_comm]
exact iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute hA hB hAB
