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

[JonBannon]

Updates Mathlib.Analysis.InnerProductSpace.Simultaneous.lean from the pairwise to the finite tuple case: i.e. gives decomposition of finite-dimensional Hilbert space as internal direct sum of joint eigenspaces of a commuting tuple of symmetric operators.

Co-Authored by: Jack Cheverton [email protected]

Co-Authored by: Samyak Dhar Tuladhar [email protected]

---

[github-actions]

PR summary c223fef4ca

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ LinearMap.IsSymmetric.directSum_isInternal_of_commute_of_fintype
+ directSum_isInternal_of_commute
+ genEigenspace_one
+ iSup_eigenspace_restrict
+ mapsTo_iInf_genEigenspace_of_forall_comm
+ orthogonalComplement_iSup_iInf_eigenspaces_eq_bot
+ orthogonalFamily_iInf_eigenspaces
- directSum_isInteral_of_commute
- eigenspace_inf_eigenspace
- eigenspace_invariant_of_commute

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[JonBannon]

Thanks, man! I'll try to squeeze a look during office hours.

…

On Tue, Sep 17, 2024, 3:30 PM Jireh Loreaux ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean <#16569 (comment)> : > + 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 There's also this, starting from my line 185 conv at H, replacing that and everything below with: rw [← (Equiv.funSplitAt i 𝕜).symm.iSup_comp, iSup_prod, iSup_comm] convert H with γ rw [← iSup_eigenspace_restrict (T i) (hT i) (iInf_eigenspace_invariant_of_commute hC i γ)] congr! with μ -- need a `genEigenspace_one` lemma change _ = map (Submodule.subtype _) (genEigenspace ((T i).restrict <| iInf_eigenspace_invariant_of_commute hC i γ) μ 1) rw [← Submodule.inf_genEigenspace _ _ _ (k := 1), inf_comm, iInf_split_single _ i, iInf_subtype] congr! with x hx · simp; rfl -- `rfl` isn't necessary with a `genEigenspace_one` lemma · simp [dif_neg hx] — Reply to this email directly, view it on GitHub <#16569 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AOJJJTWB2F5C22STSTU53DTZXB7O5AVCNFSM6AAAAABNZ7R4DOVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDGMJQGY3DSNJVGQ> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[j-loreaux]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

[ocfnash]

Thanks for this.

I have some concerns about whether these results are being developed at the right level of generality. I have highlighted two results which work for any generalised eigenspace, not just the strict eigenspace (k = 1 case). I am also a bit surprised that my changes proposed in #16915 have not been implemented (even though that PR was closed on this promise 😱)

I also wonder what other results might be split out which are true for coefficients other than ℝ or ℂ.

Unfortunately I don't have more time to give to this at the moment but I encourage you to think carefully about these points: it's sometimes a lot more work but I think we all benefit hugely from working more generally where this is possible.

[ocfnash]

For example this can be proved without using eigenspace_invariant_of_commute as follows:

Suggested change

	exact fun j ↦ eigenspace_invariant_of_commute (hC j i) (γ j) v (hv j)
	exact fun j ↦ mapsTo_genEigenspace_of_comm (hC j i) (γ j) 1 (hv j)

(though actually I think this whole lemma should be generalised and moved)

[JonBannon]

I'll try to maximally generalize this and move it.

[JonBannon]

Thanks for this.

I have some concerns about whether these results are being developed at the right level of generality. I have highlighted two results which work for any generalised eigenspace, not just the strict eigenspace (k = 1 case). I am also a bit surprised that my changes proposed in #16915 have not been implemented (even though that PR was closed on this promise 😱)

I also wonder what other results might be split out which are true for coefficients other than ℝ or ℂ.

Unfortunately I don't have more time to give to this at the moment but I encourage you to think carefully about these points: it's sometimes a lot more work but I think we all benefit hugely from working more generally where this is possible.

I will think carefully about these, @ocfnash. Just for the record, I actually thought I had incorporated the suggestions from #16915 by changing the top two results to work over a CommRing. Evidently, I did not see this as clearly as I thought I had. Sorry! It seems like most of the orthogonality results required RCLike. Maybe the idea for generalizing is to remove the use of the orthogonality as much as possible.

[ocfnash]

Thanks for all your great work on this @JonBannon I really appreciate that you're sticking with it and I know very well that it can be tough going when working in a corner of the library that is less familiar.

I had very little time this morning so I'm going to take a closer look now and see if I can be more helpful.

[ocfnash]

I thought a little more about this and here are my thoughts.

1. I'd probably first prove the result that for symmetric operators, (maximal) generalised eigenspaces and true eigenspaces are the same thing.

2. I claim it is usually better to work within the lattice of submodules and so I think rather than proving a headline result in the language of DirectSum.IsInternal I'd prove the equivalent pair of conditions according to DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top [Feel free to disagree with me here; I mention this primarily because I use this language below]

3. I think the right level of generality is to prove the following first:

open Module in
lemma iSup_iInf_maxGenEigenspace_eq_top_of_commute {ι K V : Type*}
    [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V]
    (f : ι → End K V)
    (h : Pairwise fun i j ↦ Commute (f i) (f j))
    (h' : ∀ i, ⨆ μ, (f i).maxGenEigenspace μ = ⊤) :
    ⨆ χ : ι → K, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤ := by
sorry

(and a similar statement for independence)

4. Assuming I've got the above right, combining 1 and 3 should give you what you need for symmetric operators in the more restrictive setting of an InnerProductSpace (with coeffs in ℝ or ℂ).

P.S. A commuting family of endomorphisms actually forms an Abelian (therefore nilpotent) Lie subalgebra of End K V and so the above lemma actually follows from https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Lie/Weights/Basic.html#LieModule.iSup_genWeightSpace_eq_top. Likewise independence. However having briefly tried this approach, I don't advocate it --- not least for the dependence it would create on Lie theory.

[JonBannon]

This is very cool! I'm looking forward to seeing how this turns out. Thanks, @ocfnash for looking over the PR!

…

On Tue, Sep 24, 2024, 5:47 PM Oliver Nash ***@***.***> wrote: I thought a little more about this and here are my thoughts. 1. I'd probably first prove the result that for symmetric operators, (maximal) generalised eigenspaces and true eigenspaces are the same thing. 2. I claim is usually better to work within the lattice of submodules and so I think rather than proving a headline result in the language of DirectSum.IsInternal I'd prove the equivalent pair of conditions according to DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top <https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/DirectSum/Module.html#DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top> [Feel free to disagree with me here; I mention this primarily because I use this language below 3. I think the right level of generality is to prove the following first: open Module inlemma iSup_iInf_maxGenEigenspace_eq_top_of_commute {ι K V : Type*} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : ι → End K V) (h : Pairwise fun i j ↦ Commute (f i) (f j)) (h' : ∀ i, ⨆ μ, (f i).maxGenEigenspace μ = ⊤) : ⨆ χ : ι → K, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤ := bysorry (and a similar statement for independence) 4. Assuming I've got the above right, combining 1 and 3 should give you what you need for symmetric operators in the more restrictive setting of an InnerProductSpace (with coeffs in ℝ or ℂ). P.S. A commuting family of endomorphisms actually forms an Abelian (therefore nilpotent) Lie subalgebra of End K V and so the above lemma actually follows from https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Lie/Weights/Basic.html#LieModule.iSup_genWeightSpace_eq_top <http://LieModule.iSup_genWeightSpace_eq_top>. Likewise independence. However having briefly tried this approach, I don't advocate it --- not least for the dependence it would create on Lie theory. — Reply to this email directly, view it on GitHub <#16569 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AOJJJTQXDMBAEXXA2AHEHZDZYHMX3AVCNFSM6AAAAABNZ7R4DOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGNZSGQ2DOMZYGI> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[ocfnash]

I realised that I should have proved the relevant result in Lie theory in a more general setting so I've opened #17194 to implement this.

The headline result is the lemma Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_commute. Note that it only assumes (h : ∀ i j φ, MapsTo (f i) ((f j).maxGenEigenspace φ) ((f j).maxGenEigenspace φ)), i.e., that the family of maps preserve each others' generalised eigenspaces. This is true for commuting families of maps but is a strictly weaker assumption (and this is useful, e.g., where I apply it to nilpotent but not necessarily Abelian Lie algebras).

So if this is merged and you prove that for symemtric operators, generalised eigenspaces are just eigenspaces, then the only remaining work will be to establish independence. A similar generalisation of LieModule.independent_genWeightSpace should work for this. I think this will be slightly easier than what I've done in #17194 but I won't have time to do it in the near future.

[JonBannon]

Thanks for the heads up, Oliver! Jireh already has the result identifying gen eigenspaces with eigenspaces, so we can try to finish this up. Thanks for working on this!

…

On Fri, Sep 27, 2024, 5:29 PM Oliver Nash ***@***.***> wrote: I realised that I should have proved the relevant result in Lie theory in a more general setting so I've opened #17194 <#17194> to implement this. The headline result is the lemma Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_commute. Note that it only assumes (h : ∀ i j φ, MapsTo (f i) ((f j).maxGenEigenspace φ) ((f j).maxGenEigenspace φ)), i.e., that the family of maps preserve each others' generalised eigenspaces. This is true for commuting families of maps but is a strictly weaker assumption (and this is useful, e.g., where I apply it to nilpotent but not necessarily Abelian Lie algebras). So if this is merged and you prove that for symemtric operators, generalised eigenspaces are just eigenspaces, then the only remaining work will be to establish independence. A similar generalisation of LieModule.independent_genWeightSpace <https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Lie/Weights/Basic.html#LieModule.independent_genWeightSpace> should work for this. I think this will be slightly easier than what I've done in #17194 <#17194> but I won't have time to do it in the near future. — Reply to this email directly, view it on GitHub <#16569 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AOJJJTRIUBCENQOLIGLCSB3ZYXE2DAVCNFSM6AAAAABNZ7R4DOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGOBQGA4DEMRRHA> . You are receiving this because you were mentioned.Message ID: ***@***.***>