feat(Analysis.InnerProductSpace): Decomposition of finite-dimensional inner product space as direct sum of joint eigenspaces of commuting finite tuples of symmetric operators

Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean

@@ -9,9 +9,9 @@ import Mathlib.Analysis.InnerProductSpace.Projection
 import Mathlib.Order.CompleteLattice
 import Mathlib.LinearAlgebra.Eigenspace.Basic
 
-/-! # Joint eigenspaces of a commuting pair of symmetric operators
+/-! # Joint eigenspaces of a commuting finite tuple of symmetric operators
 
-This file collects various decomposition results for joint eigenspaces of a commuting pair
+This file collects various decomposition results for joint eigenspaces of a commuting finite tuples
 of symmetric operators on a finite-dimensional inner product space.
 
 # Main Result
@@ -20,6 +20,9 @@ of symmetric operators on a finite-dimensional inner product space.
    if `{A B : E →ₗ[𝕜] E}`, then `IsSymmetric A`, `IsSymmetric B` and `A ∘ₗ B = B ∘ₗ A` imply that
    `E` decomposes as an internal direct sum of the pairwise orthogonal spaces
    `eigenspace B μ ⊓ eigenspace A ν`
+* `DirectSum.IsInternal_of_simultaneous_eigenspaces_of_commuting_symmetric_tuple` establishes the
+   analogous result to `LinearMap.IsSymmetric.directSum_isInternal_of_commute` for finite commuting
+   tuples of symmetric operators.
 
 ## TODO
 
@@ -28,7 +31,7 @@ and a proof obligation that the basis vectors are eigenvectors.
 
 ## Tags
 
-self-adjoint operator, simultaneous eigenspaces, joint eigenspaces
+self-adjoint operator, symmetric operator, simultaneous eigenspaces, joint eigenspaces
 
 -/
 
@@ -99,7 +102,7 @@ theorem iSup_iSup_eigenspace_inf_eigenspace_eq_top (hA : A.IsSymmetric) (hB : B.
 /-- 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_isInteral_of_commute (hA : A.IsSymmetric) (hB : B.IsSymmetric)
+theorem directSum_isInternal_of_commute (hA : A.IsSymmetric) (hB : B.IsSymmetric)
     (hAB : A ∘ₗ B = B ∘ₗ A) :
     DirectSum.IsInternal (fun (i : 𝕜 × 𝕜) ↦ (eigenspace A i.2 ⊓ eigenspace B i.1)):= by
   apply (orthogonalFamily_eigenspace_inf_eigenspace hA hB).isInternal_iff.mpr
@@ -108,6 +111,131 @@ theorem directSum_isInteral_of_commute (hA : A.IsSymmetric) (hB : B.IsSymmetric)
 
 end Pair
 
+section Tuple
+
+universe u
+
+variable {n m : Type u}
+
+/--The indexed infimum of eigenspaces of a commuting family of linear operators is
+invariant under each operator-/
+theorem iInf_eigenspace_invariant_of_commute (T : n → (E →ₗ[𝕜] E))
+    (hC : (∀ (i j : n), (T i) ∘ₗ (T j) = (T j) ∘ₗ (T i))) (i : n) :
+    ∀ γ : {x // x ≠ i} → 𝕜, ∀ v ∈ (⨅ (j : {x // x ≠ i}),
+    eigenspace ((Subtype.restrict (fun x ↦ x ≠ i) T) j) (γ j)), (T i) v ∈ (⨅ (j : {x // x ≠ i}),
+    eigenspace ((Subtype.restrict (fun x ↦ x ≠ i) T) j) (γ j)) := by
+  intro γ v hv
+  simp only [Submodule.mem_iInf] at *
+  exact fun i_1 ↦ eigenspace_invariant_of_commute (hC (↑i_1) i) (γ i_1) v (hv i_1)
+
+/--Simultaneous eigenspaces of a symmetric linear operator on a finite dimensional inner product
+space restricted to an invariant subspace exhaust that subspace-/
+theorem iSup_simultaneous_eigenspaces_eq_top [FiniteDimensional 𝕜 E] {F : Submodule 𝕜 E}
+    (S : E →ₗ[𝕜] E) (hS: IsSymmetric S) (hInv : ∀ v ∈ F, S v ∈ F) : ⨆ μ, Submodule.map F.subtype
+    (eigenspace (S.restrict hInv) μ)  = F := by
+ conv_lhs => rw [← Submodule.map_iSup]
+ conv_rhs => rw [← Submodule.map_subtype_top F]
+ congr!
+ have H : IsSymmetric (S.restrict hInv) := fun x y ↦ hS (F.subtype x) ↑y
+ apply Submodule.orthogonal_eq_bot_iff.mp (H.orthogonalComplement_iSup_eigenspaces_eq_bot)
+
+/--Given an invariant subspace for an operator, its intersection with an eigenspace is
+the eigenspace of the restriction the operator to the invariant subspace. -/
+theorem invariant_subspace_inf_eigenspace_eq_restrict {F : Submodule 𝕜 E} (S : E →ₗ[𝕜] E)
+    (μ : 𝕜) (hInv : ∀ v ∈ F, S v ∈ F) : (eigenspace S μ) ⊓ F =
+    Submodule.map (Submodule.subtype F)
+    (eigenspace (S.restrict (hInv)) μ) := by
+  ext v
+  constructor
+  · intro h
+    simp only [Submodule.mem_map, Submodule.coeSubtype, Subtype.exists, exists_and_right,
+      exists_eq_right, mem_eigenspace_iff]; use h.2
+    exact Eq.symm (SetCoe.ext (_root_.id (Eq.symm (mem_eigenspace_iff.mp h.1))))
+  · intro h
+    simp only [Submodule.mem_inf]
+    constructor
+    · simp only [Submodule.mem_map, Submodule.coeSubtype, Subtype.exists, exists_and_right,
+      exists_eq_right, mem_eigenspace_iff, SetLike.mk_smul_mk, restrict_apply,
+      Subtype.mk.injEq] at h
+      obtain ⟨_, hy⟩ := h
+      simpa [mem_eigenspace_iff]
+    · simp only [Submodule.coeSubtype] at h
+      obtain ⟨_, hy⟩ := h
+      simp only [← hy.2, Submodule.coeSubtype, SetLike.coe_mem]
+
+open Classical
+
+/--The orthocomplement of the indexed supremum of joint eigenspaces of a finite commuting tuple of
+symmetric operators is trivial. -/
+theorem orthogonalComplement_iSup_iInf_eigenspaces_eq_bot [Fintype n] [FiniteDimensional 𝕜 E]
+    (T : n → (E →ₗ[𝕜] E)) (hT :(∀ (i : n), ((T i).IsSymmetric)))
+    (hC : (∀ (i j : n), (T i) ∘ₗ (T j) = (T j) ∘ₗ (T i))) :
+    (⨆ (γ : n → 𝕜), (⨅ (j : n), (eigenspace (T j) (γ j)) : Submodule 𝕜 E))ᗮ = ⊥ := by
+  revert T
+  refine Fintype.induction_subsingleton_or_nontrivial n ?_ ?_
+  · intro m _ hhm T hT _
+    simp only [Submodule.orthogonal_eq_bot_iff]
+    by_cases case : Nonempty m
+    · have i := choice case
+      have := uniqueOfSubsingleton i
+      conv => lhs; rhs; ext γ; rw [ciInf_subsingleton i]
+      rw [← (Equiv.funUnique m 𝕜).symm.iSup_comp]
+      apply Submodule.orthogonal_eq_bot_iff.mp ((hT i).orthogonalComplement_iSup_eigenspaces_eq_bot)
+    · simp only [not_nonempty_iff] at case
+      simp only [iInf_of_empty, ciSup_unique]
+  · intro m hm hmm H T hT hC
+    obtain ⟨w, i , h⟩ := exists_pair_ne m
+    simp only [ne_eq] at h
+    have D := H {x // x ≠ i} (Fintype.card_subtype_lt (p := fun (x : m) ↦ ¬x = i) (x := i)
+      (by simp only [not_true_eq_false, not_false_eq_true])) (Subtype.restrict (fun x ↦ x ≠ i) T)
+        (fun (i_1 : {x // x ≠ i}) ↦ hT ↑i_1) (fun (i_1 j : { x // x ≠ i }) ↦ hC ↑i_1 ↑j)
+    simp only [Submodule.orthogonal_eq_bot_iff] at *
+    have G : (⨆ (γ : {x // x ≠ i} → 𝕜), (⨆ μ : 𝕜, (eigenspace (T i) μ ⊓ (⨅ (j : {x // x ≠ i}),
+    eigenspace (Subtype.restrict (fun x ↦ x ≠ i) T j) (γ j))))) = ⨆ (γ : {x // x ≠ i} → 𝕜),
+    (⨅ (j : {x // x ≠ i}), eigenspace (Subtype.restrict (fun x ↦ x ≠ i) T j) (γ j)) := by
+      conv => lhs; rhs; ext γ; rhs; ext μ; rw [invariant_subspace_inf_eigenspace_eq_restrict (T i) μ
+        (iInf_eigenspace_invariant_of_commute T hC i γ)]
+      conv => lhs; rhs; ext γ; rw [iSup_simultaneous_eigenspaces_eq_top (T i) (hT i)
+        (iInf_eigenspace_invariant_of_commute T hC i γ)]
+    have H1 : ∀ (i : m), ∀ (s : m → 𝕜 → Submodule 𝕜 E), (⨆ f : m → 𝕜, ⨅ x, s x (f x)) =
+        ⨆ f' : {y // y ≠ i} → 𝕜, ⨆ y : 𝕜, s i y ⊓ ⨅ x' : {y // y ≠ i}, (s x' (f' x')) := by
+      intro i s
+      rw [← (Equiv.funSplitAt i 𝕜).symm.iSup_comp, iSup_prod, iSup_comm]
+      congr! with f' y
+      rw [iInf_split_single _ i, iInf_subtype]
+      congr! with x hx
+      · simp
+      · simp [dif_neg hx]
+    rw [← G] at D
+    rw [H1 i (fun _ ↦ (fun μ ↦ (eigenspace (T _) μ )))]
+    exact D
+
+/--Given a finite commuting family of symmetric linear operators, the family of joint eigenspaces
+is an orthogonal family. -/
+theorem orthogonalFamily_iInf_eigenspaces (T : n → (E →ₗ[𝕜] E))
+    (hT :(∀ (i : n), ((T i).IsSymmetric))) : OrthogonalFamily 𝕜 (fun (γ : n → 𝕜) =>
+    (⨅ (j : n), (eigenspace (T j) (γ j)) : Submodule 𝕜 E))
+    (fun (γ : n → 𝕜) => (⨅ (j : n), (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.coeSubtype, 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 _
+
+/-- Given a finite commuting family of symmetric linear operators, the inner product space on which
+they act decomposes as an internal direct sum of simultaneous eigenspaces. -/
+theorem DirectSum.IsInternal_of_simultaneous_eigenspaces_of_commuting_symmetric_tuple [Fintype n]
+    [FiniteDimensional 𝕜 E] (T : n → (E →ₗ[𝕜] E)) (hT :(∀ (i : n), ((T i).IsSymmetric)))
+    (hC : (∀ (i j : n), (T i) ∘ₗ (T j) = (T j) ∘ₗ (T i))) :
+    DirectSum.IsInternal (fun (α : n → 𝕜) ↦ ⨅ (j : n), (eigenspace (T j) (α j))) := by
+  rw [OrthogonalFamily.isInternal_iff]
+  · exact orthogonalComplement_iSup_iInf_eigenspaces_eq_bot T hT hC
+  · exact orthogonalFamily_iInf_eigenspaces T hT
+
+end Tuple
+
 end IsSymmetric
 
 end LinearMap