Zulip Chat Archive

Stream: general

Topic: Fintype Induction


Jireh Loreaux (Aug 01 2024 at 00:49):

I have a real life example of Fintype induction. It's work of @Jon Bannon if he wants to share a link to a relevant branch, or at least describe the situation in which it occurred.

Jon Bannon (Aug 01 2024 at 01:14):

I'm happy to share. I don't have an mwe, and the code for the induction part is not in the active branch right now, but it's here (module docstring removed):

variable {𝕜 : Type*} [RCLike 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E]

local notation "⟪" x ", " y "⟫" => @inner 𝕜 E _ x y

open Module.End

namespace LinearMap

namespace IsSymmetric

section Pair

variable {α : 𝕜} {A B : E →ₗ[𝕜] E} (hA : A.IsSymmetric) (hB : B.IsSymmetric)
    (hAB : A ∘ₗ B = B ∘ₗ A)

theorem eigenspace_invariant (α : 𝕜) :  v  (eigenspace A α), (B v  eigenspace A α) := by
  intro v hv
  rw [eigenspace, mem_ker, sub_apply, Module.algebraMap_end_apply,  comp_apply A B v, hAB,
  comp_apply B A v,  map_smul,  map_sub, hv, map_zero] at *

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]

theorem invariant_subspace_inf_eigenspace_eq_restrict' : (fun (γ : 𝕜) 
    Submodule.map (Submodule.subtype (eigenspace A α)) (eigenspace (B.restrict
    (eigenspace_invariant hAB α)) γ)) = (fun (γ : 𝕜)  (eigenspace B γ  eigenspace A α)) := by
  funext γ
  exact Eq.symm (invariant_subspace_inf_eigenspace_eq_restrict B γ (eigenspace_invariant hAB α))

theorem iSup_restrict_eq_top: ( γ , (eigenspace (LinearMap.restrict B
    (eigenspace_invariant hAB α)) γ)) =  := by
    rw [ Submodule.orthogonal_eq_bot_iff]
    exact orthogonalComplement_iSup_eigenspaces_eq_bot (LinearMap.IsSymmetric.restrict_invariant hB
    (eigenspace_invariant hAB α))

theorem iSup_simultaneous_eigenspaces_eq_top :
    ( (α : 𝕜), ( (γ : 𝕜), (eigenspace B γ  eigenspace A α))) =  := by
  have : (fun (α : 𝕜)   eigenspace A α)  = fun (α : 𝕜) 
      ( (γ : 𝕜), (eigenspace B γ  eigenspace A α)) := by
    funext; rw [ invariant_subspace_inf_eigenspace_eq_restrict' hAB,
        Submodule.map_iSup, iSup_restrict_eq_top hB hAB, Submodule.map_top,
       Submodule.range_subtype]
  rw [ Submodule.orthogonal_eq_bot_iff.mp (hA.orthogonalComplement_iSup_eigenspaces_eq_bot), this]

theorem orthogonality_of_simultaneous_eigenspaces_of_pairwise_commuting_symmetric :
    OrthogonalFamily 𝕜 (fun (i : 𝕜 × 𝕜) => (eigenspace B i.1  eigenspace A i.2 : Submodule 𝕜 E))
    (fun i => (eigenspace B i.1  eigenspace A i.2).subtypeₗᵢ) := by
  refine orthogonalFamily_iff_pairwise.mpr ?_
  intro i j hij v hv1 , hv2
  have H:=  (Iff.not (Iff.symm Prod.ext_iff)).mpr hij
  push_neg at H
  by_cases C: i.1 = j.1
  <;> intro w hw1, hw2
  · exact orthogonalFamily_iff_pairwise.mp hA.orthogonalFamily_eigenspaces (H C) hv2 w hw2
  · exact orthogonalFamily_iff_pairwise.mp hB.orthogonalFamily_eigenspaces C hv1 w hw1

/-- Given a commuting pair of symmetric linear operators, the Hilbert space on which they act
decomposes as an internal direct sum of simultaneous eigenspaces. -/
theorem DirectSum.IsInternal_of_simultaneous_eigenspaces_of_commuting_symmetric_pair:
    DirectSum.IsInternal (fun (i : 𝕜 × 𝕜)  (eigenspace B i.1  eigenspace A i.2)):= by
  apply (OrthogonalFamily.isInternal_iff
    (orthogonality_of_simultaneous_eigenspaces_of_pairwise_commuting_symmetric hA hB)).mpr
  rw [Submodule.orthogonal_eq_bot_iff, iSup_prod, iSup_comm]
  exact iSup_simultaneous_eigenspaces_eq_top hA hB hAB

end Pair

section Tuple

universe u

variable {n m : Type u} [Fintype n] [Fintype m] (T : n  (E →ₗ[𝕜] E))
    (hT :( (i : n), ((T i).IsSymmetric)))
    (hC : ( (i j : n), (T i) ∘ₗ (T j) = (T j) ∘ₗ (T i)))

open Classical

theorem invariance_iInf [Nonempty n] (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 (hC (i_1) i) (γ i_1) v (hv i_1)

theorem iSup_iInf_fun_index_split_single {α β γ : Type*} [DecidableEq α] [CompleteLattice γ]
    (i : α) (s : α  β  γ) : ( f : α  β,  x, s x (f x)) =
       f' : {y // y  i}  β,  y : β, s i y   x' : {y // y  i}, (s x' (f' x')) := by
  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]

theorem invariant_subspace_eigenspace_exhaust {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)

theorem orthogonalComplement_iSup_iInf_eigenspaces_eq_bot:
    ( (γ : 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 E : ( (γ : {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) μ
        (invariance_iInf T hC i γ)]
      conv => lhs; rhs; ext γ; rw [invariant_subspace_eigenspace_exhaust (T i) (hT i)
        (invariance_iInf T hC i γ)]
    rw [ E] at D
    rw [iSup_iInf_fun_index_split_single i (fun _  (fun μ  (eigenspace (T _) μ )))]
    exact D

theorem orthogonalFamily_iInf_eigenspaces : 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 Hilbert space on which they
act decomposes as an internal direct sum of simultaneous eigenspaces. -/
theorem DirectSum.IsInternal_of_simultaneous_eigenspaces_of_commuting_symmetric_tuple :
    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

Notification Bot (Aug 01 2024 at 01:25):

A message was moved here from #general > Finset vs Finite by Kyle Miller.

Jon Bannon (Aug 01 2024 at 02:24):

To clarify where the fintype induction appeared, it was in the orthogonalComplement_iSup_iInf_eigenspaces_eq_bot theorem. We ended up using the custom fintype induction result Fintype.induction_subsingleton_or_nontrivial to handle induction on a fintype index set.


Last updated: May 02 2025 at 03:31 UTC