English
The joint infimum of eigenspaces over a family of symmetric operators forms an orthogonal family.
Русский
Совместное пересечение (инфимин) эвгенспейсов симметричных операторов образует ортогональную семью.
LaTeX
$$$\text{orthogonalFamily}_\text{iInf}(\{\text{eigenspace}(T_j, \gamma_j)\})$ form orthogonal family$$
Lean4
/-- The joint eigenspaces of a family of symmetric operators form an
`OrthogonalFamily`. -/
theorem orthogonalFamily_iInf_eigenspaces (hT : ∀ i, (T i).IsSymmetric) :
OrthogonalFamily 𝕜 (fun γ : n → 𝕜 ↦ (⨅ j, eigenspace (T j) (γ j) : Submodule 𝕜 E)) fun γ : n → 𝕜 ↦
(⨅ j, eigenspace (T j) (γ j)).subtypeₗᵢ :=
by
intro f g hfg Ef Eg
obtain ⟨a, ha⟩ := Function.ne_iff.mp hfg
have H := orthogonalFamily_eigenspaces (hT a) ha
simp only [Submodule.coe_subtypeₗᵢ, Submodule.coe_subtype, Subtype.forall] at H
apply H
· exact (Submodule.mem_iInf <| fun _ ↦ eigenspace (T _) (f _)).mp Ef.2 _
· exact (Submodule.mem_iInf <| fun _ ↦ eigenspace (T _) (g _)).mp Eg.2 _
