-
Notifications
You must be signed in to change notification settings - Fork 316
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(Analysis.InnerProductSpace): Decomposition of finite-dimensional inner product space as direct sum of joint eigenspaces of commuting finite tuples of symmetric operators #16569
base: master
Are you sure you want to change the base?
Conversation
…sional hypothesis that was somehow out of scope.
…result that may be possible to omit or inline because an existing result in the library might be able to play the role...
PR summary 98d76025a5
|
File | Base Count | Head Count | Change |
---|---|---|---|
Mathlib.Analysis.InnerProductSpace.JointEigenspace | 1723 | 1753 | +30 (+1.74%) |
Import changes for all files
Files | Import difference |
---|---|
Mathlib.Analysis.InnerProductSpace.JointEigenspace |
30 |
Declarations diff
+ LinearMap.IsSymmetric.directSum_isInternal_of_commute_of_fintype
+ LinearMap.IsSymmetric.genEigenspace_eq_eigenspace
+ LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute_of_fintype
+ LinearMap.IsSymmetric.maxGenEigenspace_eq_eigenspace
+ directSum_isInternal_of_commute
+ iSup_eigenspace_restrict
+ iSup_iInf_maxGenEigenspace_eq_top_of_iSup_maxGenEigenspace_eq_top_of_commute
+ 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.
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:
***@***.***>
|
…ace_invariant_of_commute`. I'm not sure how to get this last input from the infoview.
…or eigenspace_inf_eigenspace using the new simp lemma in the pair part.
…alized eigenspaces in the result in the main file, as these agree with eigenspaces for symmetric operators.
…enEigenspace_of_forall_comm` to work on line 143
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. |
…r-community/mathlib4 into JointEigenspacesTuples
I thought a little more about this and here are my thoughts.
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)
P.S. A commuting family of endomorphisms actually forms an Abelian (therefore nilpotent) Lie subalgebra of |
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:
***@***.***>
|
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 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. |
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:
***@***.***>
|
Sorry about that, Oliver! I've been playing around with the theorem you
suggested just for fun...I totally forgot it would mess with the PR.
Ultimately, as you say, we will use your new result!
(I'm a newbie to this...)😁
…On Mon, Oct 7, 2024, 9:24 AM Oliver Nash ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean
<#16569 (comment)>
:
> +lemma iSup_iInf_maxGenEigenspace_eq_top_of_commute {ι K V : Type*}
+ [Finite ι] [Field K] [DecidableEq 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
+ have _ := Fintype.ofFinite ι
+ revert f
+ refine Fintype.induction_subsingleton_or_nontrivial ι (fun m _ hhm f hf x ↦ ?_)
+ (fun m hm hmm H f hf hC ↦ ?_)
+ · obtain (hm | hm) := isEmpty_or_nonempty m
+ · simp
+ · have := uniqueOfSubsingleton (Classical.choice hm)
+ simpa [ciInf_unique, ← (Equiv.funUnique m K).symm.iSup_comp] using x default
+ · have i := Classical.arbitrary m
+ classical
+ specialize H {x // x ≠ i} (Fintype.card_subtype_lt (x := i) (by simp))
+ (Subtype.restrict (· ≠ i) f) (fun _ _ _ ↦ hf <| by simpa [Subtype.coe_ne_coe]) (hC ·)
+ rw [← (Equiv.funSplitAt i K).symm.iSup_comp, iSup_prod, iSup_comm]
+ convert H with γ
+ rw [← iSup_eigenspace_restrict (f i) (hf i) (F := ⨅ j, eigenspace _ _)] --use genEigenspace ver.
+ swap
+ · exact mapsTo_iInf_genEigenspace_of_forall_comm (fun j : {j // j ≠ i} ↦ hC j i) γ 1
+ congr! with μ
+ rw [← Module.End.genEigenspace_one, ← Submodule.inf_genEigenspace _ _ _ (k := 1), inf_comm,
+ iInf_split_single _ i, iInf_subtype]
+ congr! with x hx
+ · simp
+ · simp [dif_neg hx]
Are you sure we want this now?
Isn't it just a special case of the lemma
Triangularizable.html#Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo
<https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.html#Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo>
that I added in #17194
<#17194> ?
To be precise, the following should work (after merging master):
example {ι 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
refine Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo _
(fun i j ↦ mapsTo_iSup_genEigenspace_of_comm ?_) h'
rcases eq_or_ne j i with rfl | hij <;> tauto -- Maybe we should have API to golf this line.
—
Reply to this email directly, view it on GitHub
<#16569 (review)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AOJJJTQN6VDI2LCZ7NEYVSDZ2KDQTAVCNFSM6AAAAABNZ7R4DOVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDGNJRHE2DINBZGE>
.
You are receiving this because you were mentioned.Message ID:
***@***.***>
|
One question: you earlier mentioned so mething about a dependency on Lie
Theory perhaps posing a problem. I gather from this comment that we can
ignore that concern?
…On Mon, Oct 7, 2024, 9:41 AM Bannon, Jon ***@***.***> wrote:
Sorry about that, Oliver! I've been playing around with the theorem you
suggested just for fun...I totally forgot it would mess with the PR.
Ultimately, as you say, we will use your new result!
(I'm a newbie to this...)😁
On Mon, Oct 7, 2024, 9:24 AM Oliver Nash ***@***.***> wrote:
> ***@***.**** commented on this pull request.
> ------------------------------
>
> In Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean
> <#16569 (comment)>
> :
>
> > +lemma iSup_iInf_maxGenEigenspace_eq_top_of_commute {ι K V : Type*}
> + [Finite ι] [Field K] [DecidableEq 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
> + have _ := Fintype.ofFinite ι
> + revert f
> + refine Fintype.induction_subsingleton_or_nontrivial ι (fun m _ hhm f hf x ↦ ?_)
> + (fun m hm hmm H f hf hC ↦ ?_)
> + · obtain (hm | hm) := isEmpty_or_nonempty m
> + · simp
> + · have := uniqueOfSubsingleton (Classical.choice hm)
> + simpa [ciInf_unique, ← (Equiv.funUnique m K).symm.iSup_comp] using x default
> + · have i := Classical.arbitrary m
> + classical
> + specialize H {x // x ≠ i} (Fintype.card_subtype_lt (x := i) (by simp))
> + (Subtype.restrict (· ≠ i) f) (fun _ _ _ ↦ hf <| by simpa [Subtype.coe_ne_coe]) (hC ·)
> + rw [← (Equiv.funSplitAt i K).symm.iSup_comp, iSup_prod, iSup_comm]
> + convert H with γ
> + rw [← iSup_eigenspace_restrict (f i) (hf i) (F := ⨅ j, eigenspace _ _)] --use genEigenspace ver.
> + swap
> + · exact mapsTo_iInf_genEigenspace_of_forall_comm (fun j : {j // j ≠ i} ↦ hC j i) γ 1
> + congr! with μ
> + rw [← Module.End.genEigenspace_one, ← Submodule.inf_genEigenspace _ _ _ (k := 1), inf_comm,
> + iInf_split_single _ i, iInf_subtype]
> + congr! with x hx
> + · simp
> + · simp [dif_neg hx]
>
> Are you sure we want this now?
>
> Isn't it just a special case of the lemma
> Triangularizable.html#Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo
> <https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.html#Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo>
> that I added in #17194
> <#17194> ?
>
> To be precise, the following should work (after merging master):
>
> example {ι 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
> refine Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo _
> (fun i j ↦ mapsTo_iSup_genEigenspace_of_comm ?_) h'
> rcases eq_or_ne j i with rfl | hij <;> tauto -- Maybe we should have API to golf this line.
>
> —
> Reply to this email directly, view it on GitHub
> <#16569 (review)>,
> or unsubscribe
> <https://github.com/notifications/unsubscribe-auth/AOJJJTQN6VDI2LCZ7NEYVSDZ2KDQTAVCNFSM6AAAAABNZ7R4DOVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDGNJRHE2DINBZGE>
> .
> You are receiving this because you were mentioned.Message ID:
> ***@***.***>
>
|
Yes, now that we have P.S. I see the phrase "asap" in a commit message but just to emphasise there is absolutely no urgency at my end with regard to this PR. |
Great!
…On Mon, Oct 7, 2024, 10:18 AM Oliver Nash ***@***.***> wrote:
One question: you earlier mentioned so mething about a dependency on Lie
Theory perhaps posing a problem. I gather from this comment that we can
ignore that concern?
Yes, now that we have
Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo, there is
no dependence on Lie theory.
—
Reply to this email directly, view it on GitHub
<#16569 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AOJJJTQAUHIKE2MZRNJBEILZ2KJ2RAVCNFSM6AAAAABNZ7R4DOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGOJXGA3DINRVGU>
.
You are receiving this because you were mentioned.Message ID:
***@***.***>
|
…eing for symmetric operators.
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]