Starting to edit Simulteaneous Diagonalizeation

Samyak-DT · Samyak-DT · commit a0292adb7e77 · 2024-06-28T12:18:21.000-04:00
diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean
@@ -9,6 +9,7 @@ import Mathlib.Analysis.InnerProductSpace.Symmetric
 import Mathlib.Analysis.NormedSpace.RCLike
 import Mathlib.Analysis.RCLike.Lemmas
 import Mathlib.Algebra.DirectSum.Decomposition
+import Mathlib.LinearAlgebra.Eigenspace.Basic
 
 #align_import analysis.inner_product_space.projection from "leanprover-community/mathlib"@"0b7c740e25651db0ba63648fbae9f9d6f941e31b"
 
@@ -477,6 +478,10 @@ def orthogonalProjection : E →L[𝕜] K :=
     nlinarith [orthogonalProjectionFn_norm_sq K x]
 #align orthogonal_projection orthogonalProjection
 
+
+
+
+theorem orthoeigen_commute {A B : E →ₗ[𝕜] E}(α : ℝ )(orthogonalProjection P : eigenspace A )(hAB: A ∘ₗ B = B ∘ₗ  A)(hA : A.IsSymmetric): A * P = P * A  := by sorry
 variable {K}
 
 @[simp]
@@ -1442,4 +1447,5 @@ theorem maximal_orthonormal_iff_basis_of_finiteDimensional (hv : Orthonormal 
     rw [← h.span_eq, coe_h, hv_coe]
 #align maximal_orthonormal_iff_basis_of_finite_dimensional maximal_orthonormal_iff_basis_of_finiteDimensional
 
+
 end OrthonormalBasis
diff --git a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean
@@ -6,6 +6,8 @@ Authors: Moritz Doll, Frédéric Dupuis, Heather Macbeth
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.NormedSpace.Banach
 import Mathlib.LinearAlgebra.SesquilinearForm
+import Mathlib.LinearAlgebra.Eigenspace.Basic
+--import Mathlib.Analysis.InnerProductSpace.Projection
 
 #align_import analysis.inner_product_space.symmetric from "leanprover-community/mathlib"@"3f655f5297b030a87d641ad4e825af8d9679eb0b"
 
@@ -192,3 +194,101 @@ theorem IsSymmetric.inner_map_self_eq_zero {T : E →ₗ[𝕜] E} (hT : T.IsSymm
 #align linear_map.is_symmetric.inner_map_self_eq_zero LinearMap.IsSymmetric.inner_map_self_eq_zero
 
 end LinearMap
+
+namespace Commutive
+
+open LinearMap
+
+open Module
+
+open End
+
+
+theorem comm_simul_diag  {A B :  E →ₗ[𝕜] E}{α : ℝ }(hAB: A ∘ₗ B = B ∘ₗ  A):
+    {B v | v ∈  eigenspace A α } ⊆ eigenspace A α:= by
+  rintro y ⟨z, hz⟩
+  simp only [SetLike.mem_coe , eigenspace, mem_ker, sub_apply, algebraMap_end_apply] at *
+  rw [← hz.2, ← comp_apply, hAB, ← map_smul, comp_apply, ← map_sub, hz.1, map_zero]
+
+
+theorem sharing_eigenspace {A B :  E →ₗ[𝕜] E}(hAB: A ∘ₗ B = B ∘ₗ  A){α β : ℝ}:
+    {B v | v ∈  eigenspace A α ⊓ eigenspace B β} ⊆ (eigenspace A α ⊓ eigenspace B β):= by
+  intro x ⟨ y ,⟨ ⟨hy1, hy2 ⟩, hy3⟩ ⟩
+  constructor
+
+  simp only [SetLike.mem_coe] at *
+  rw[hy3.symm]
+  rw[mem_eigenspace_iff] at *
+  rw[←comp_apply , hAB, ← map_smul, comp_apply, hy1]
+
+  simp only [SetLike.mem_coe] at *
+  rw[mem_eigenspace_iff] at hy2
+  rw[mem_eigenspace_iff, hy3.symm, ← map_smul ]
+  rw[hy2]
+
+
+theorem eigen_subspace {A B : E →ₗ[𝕜] E}{hAB: Commute A B}{α β : ℝ}:
+    (⨆ α , eigenspace A α ⊓ eigenspace B β) = eigenspace A α := by sorry
+
+lemma ortho_eigen_commute{A B : E →ₗ[𝕜] E}(hAB : Commute A B) : A*B = B * A := by sorry
+
+
+theorem indiv_exhaust {A B : E →ₗ[𝕜] E}{hAB: Commute A B}{α β : ℝ}: (⨆ β , (eigenspace B β ⊓ eigenspace A α)) = eigenspace A α := by
+  by_cases h : eigenspace A α = ⊥
+-- when eigenvalues are 0, weird they are coded in like that
+  · conv =>
+      lhs
+      rw [h]
+      conv =>
+        rhs
+        intro t
+        rw [inf_bot_eq]
+    simp only [iSup_bot, h]
+-- when there are eigenvalues
+  · ext v
+    constructor
+    · intro h1
+      simp [iSup, sSup] at h1
+      apply h1
+      refine Set.mem_def.mpr ?_
+      intro a
+      simp only [inf_le_right]
+    · intro h2
+      simp [iSup, sSup]
+      intro K F
+      specialize F α
+      apply F
+      simp only [Submodule.mem_inf]
+      constructor
+      swap
+      exact h2
+
+
+      rw[mem_eigenspace_iff] at *
+
+
+
+      have exh : (⨆ γ , eigenspace B γ) = E := by sorry--showing the 'map' is injective might be the key?
+      have AA : v ∈ (⨆ γ , eigenspace B γ) := by sorry
+      simp only [iSup, sSup, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff,
+        Submodule.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk, Set.mem_iInter,
+        SetLike.mem_coe] at AA
+      apply AA
+      refine Set.mem_def.mpr ?_
+
+
+      have AB : ∃ γ : 𝕜, v ∈ eigenspace B γ := by sorry
+      --apply F
+      --simp only [Submodule.mem_inf]
+      --constructor
+      --swap
+      --exact h
+
+
+    rw [← Submodule.zero_eq_bot] at h
+    --push_neg at h
+    --have h2 := Submodule.exists_mem_ne_zero_of_ne_bot h
+    --obtain ⟨w, hw⟩ := h2
+
+
+end Commutive
