Conversation
Collaborator
Author
|
👍
…On Wed, Aug 28, 2024, 6:07 PM Jireh Loreaux ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In Mathlib/Analysis/InnerProductSpace/Simultaneous.lean
<#15012 (comment)>
:
> +then the eigenspaces of the restriction of B to any eigenspace of A exhaust that eigenspace.-/
+theorem iSup_inf_eq_top: (⨆ γ , (eigenspace (LinearMap.restrict B
+ (eigenspace_invariant_of_commute hAB α)) γ)) = ⊤ := by
+ rw [← Submodule.orthogonal_eq_bot_iff]
+ exact orthogonalComplement_iSup_eigenspaces_eq_bot (LinearMap.IsSymmetric.restrict_invariant hB
+ (eigenspace_invariant_of_commute hAB α))
I don't see an obvious way to use generalized eigenspaces further here.
When congr or convert don't do what I expect / want (or produce a million
goals), it's generally because they have gone too deep. So, if it doesn't
do exactly what I think it should, I immediately go for limiting depth.
Sometimes this makes me realize I was being stupid, and I *shouldn't*
have expected them to work. Other times, limiting the depth is exactly
what's needed.
—
Reply to this email directly, view it on GitHub
<#15012 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AOJJJTQYC7ERTGACLZNI7O3ZTZCYTAVCNFSM6AAAAABLIGFE5CVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDENRXGM2TANBXHA>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
j-loreaux
reviewed
Aug 29, 2024
…result, as well as changing `simultaneous` to `joint` in order to align with the name of the file
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
…nprover-community/mathlib4 into Simultaneous-Diagonalization
Contributor
|
I've had a lot of input in this. maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by j-loreaux. |
dupuisf
reviewed
Aug 30, 2024
Contributor
dupuisf
left a comment
There was a problem hiding this comment.
Can you merge master into this? The variable inclusion mechanism has changed in the latest version of Lean and might lead to breakage here, so it's easier to do this before trying to merge.
Contributor
|
Good catch, thanks |
…ied some places that the finite dimensional assumption was not used, so reorganized accordingly.
Contributor
|
Great; thanks! bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Aug 30, 2024
…l Inner Product Space as Direct Sum of Simultaneous Eigenspaces of Commuting Symmetric Operators (#15012) Introduced `Mathlib.Analysis.InnerProductSpace.Simultaneous.lean` as a receptacle for results concerning simultaneous eigenspace decomposition results for tuples of commuting symmetric operators on (finite-dimensional) Hilbert space. Includes decomposition of finite-dimensional Hilbert space as internal direct sum of simultaneous eigenspaces of a commuting pair of symmetric operators. Co-Authored by: Jack Cheverton <jt18chev@siena.edu> Co-Authored by: Samyak Dhar Tuladhar <sd10tula@siena.edu> Co-authored-by: JonBannon <59937998+JonBannon@users.noreply.github.com>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 9, 2024
…l Inner Product Space as Direct Sum of Simultaneous Eigenspaces of Commuting Symmetric Operators (#15012) Introduced `Mathlib.Analysis.InnerProductSpace.Simultaneous.lean` as a receptacle for results concerning simultaneous eigenspace decomposition results for tuples of commuting symmetric operators on (finite-dimensional) Hilbert space. Includes decomposition of finite-dimensional Hilbert space as internal direct sum of simultaneous eigenspaces of a commuting pair of symmetric operators. Co-Authored by: Jack Cheverton <jt18chev@siena.edu> Co-Authored by: Samyak Dhar Tuladhar <sd10tula@siena.edu> Co-authored-by: JonBannon <59937998+JonBannon@users.noreply.github.com>
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 9, 2024
…l Inner Product Space as Direct Sum of Simultaneous Eigenspaces of Commuting Symmetric Operators (#15012) Introduced `Mathlib.Analysis.InnerProductSpace.Simultaneous.lean` as a receptacle for results concerning simultaneous eigenspace decomposition results for tuples of commuting symmetric operators on (finite-dimensional) Hilbert space. Includes decomposition of finite-dimensional Hilbert space as internal direct sum of simultaneous eigenspaces of a commuting pair of symmetric operators. Co-Authored by: Jack Cheverton <jt18chev@siena.edu> Co-Authored by: Samyak Dhar Tuladhar <sd10tula@siena.edu> Co-authored-by: JonBannon <59937998+JonBannon@users.noreply.github.com>
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 12, 2024
…l Inner Product Space as Direct Sum of Simultaneous Eigenspaces of Commuting Symmetric Operators (#15012) Introduced `Mathlib.Analysis.InnerProductSpace.Simultaneous.lean` as a receptacle for results concerning simultaneous eigenspace decomposition results for tuples of commuting symmetric operators on (finite-dimensional) Hilbert space. Includes decomposition of finite-dimensional Hilbert space as internal direct sum of simultaneous eigenspaces of a commuting pair of symmetric operators. Co-Authored by: Jack Cheverton <jt18chev@siena.edu> Co-Authored by: Samyak Dhar Tuladhar <sd10tula@siena.edu> Co-authored-by: JonBannon <59937998+JonBannon@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
6 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Introduced
Mathlib.Analysis.InnerProductSpace.Simultaneous.leanas a receptacle for results concerning simultaneous eigenspace decomposition results for tuples of commuting symmetric operators on (finite-dimensional) Hilbert space.Includes decomposition of finite-dimensional Hilbert space as internal direct sum of simultaneous eigenspaces of a commuting pair of symmetric operators.
Co-Authored by: Jack Cheverton jt18chev@siena.edu
Co-Authored by: Samyak Dhar Tuladhar sd10tula@siena.edu