English
If A,B are commuting symmetric operators, the supremum across eigen-space intersections equals the eigenspace of A.
Русский
Если A,B – симметричные операторы, коммутируют, то объединяющее пространство из пересечений собственных пространств равно собственному пространству A.
LaTeX
$$$\sup_\gamma (\text{eigenspace}(A, \alpha) \cap \text{eigenspace}(B, \gamma)) = \text{eigenspace}(A, \alpha)$$$
Lean4
/-- If A and B are commuting symmetric operators on a finite-dimensional inner product space
then the eigenspaces of the restriction of B to any eigenspace of A exhaust that eigenspace. -/
theorem iSup_eigenspace_inf_eigenspace_of_commute (hB : B.IsSymmetric) (hAB : Commute A B) :
(⨆ γ, eigenspace A α ⊓ eigenspace B γ) = eigenspace A α :=
by
conv_rhs => rw [← (eigenspace A α).map_subtype_top]
simp only [← Submodule.map_iSup, (eigenspace A α).inf_genEigenspace _ (mapsTo_genEigenspace_of_comm hAB α 1)]
congr 1
simpa only [genEigenspace_eq_eigenspace, Submodule.orthogonal_eq_bot_iff] using
orthogonalComplement_iSup_eigenspaces_eq_bot <| hB.restrict_invariant <| mapsTo_genEigenspace_of_comm hAB α 1
