[Merged by Bors] - feat: the spectrum of a diagonal matrix is the range of the diagonal #13837
Conversation
This file contains 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
4 tasks
PR summary 0561c3b868Import changesNo significant changes to the import graph
|
JonBannon
added
awaiting-review
new-contributor
eric-wieser
reviewed
Jun 15, 2024
eric-wieser
reviewed
Jun 15, 2024
eric-wieser
added
awaiting-author
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…dule docstring, still.
… occurrences of`Matrix._` from within body of file.
… the one suggested by Jireh.
JonBannon
added
awaiting-review
and removed
awaiting-author
j-loreaux
reviewed
Jun 23, 2024
….basisFun` versions of `hasEigenvalue_toLin_diagonal_iff`
|
Ah, cool. To clarify, we want the standard basis version here, right?
Should I provide versions for toEuclideanLin as well?
…On Sun, Jun 23, 2024, 10:51 AM Jireh Loreaux ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In Mathlib/LinearAlgebra/Eigenspace/Matrix.lean
<#13837 (comment)>
:
> +lemma hasEigenvector_toLin_basis_diagonal (d : n → R) (i : n) (b : Basis n R M) :
+ Module.End.HasEigenvector (toLin b b (diagonal d)) (d i) (b i) := by
+ constructor
+ · refine mem_eigenspace_iff.mpr ?left.a
+ simp only [diagonal, Pi.basisFun_apply, toLin'_apply, mulVec_stdBasis_apply, transpose_apply,
+ of_apply, Pi.smul_apply, LinearMap.stdBasis_apply', smul_eq_mul, mul_ite, mul_one, mul_zero]
+ all_goals simp_all
+ · exact Basis.ne_zero b i
+
+/-- Standard basis vectors are eigenvectors of any associated diagonal linear operator. -/
+lemma hasEigenvector_toLin'_diagonal (d : n → R) (i : n) :
+ Module.End.HasEigenvector (toLin' (diagonal d)) (d i) (Pi.basisFun R n i) :=
+ hasEigenvector_toLin_basis_diagonal (d : n → R) (i : n) (b := Pi.basisFun R n)
+
+/-- Eigenvalues of a diagonal linear operator are the diagonal entries. -/
+lemma hasEigenvalue_toLin'_diagonal_iff (d : n → R) {μ : R} :
Actually, toLin' is just the standard basis version, but with the max
norm. toEuclideanLin is the PiLp 2 version.
—
Reply to this email directly, view it on GitHub
<#13837 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AOJJJTRBKP74GILZ5JC4TVTZI3OHDAVCNFSM6AAAAABJKQ6XSSVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDCMZUGI4TOMJYG4>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
j-loreaux
reviewed
Jun 24, 2024
Comment on lines
13
to
14
| This file collects results about eigenvectors, eigenvalues and spectrum specific to matrices | ||
| over a field. |
There was a problem hiding this comment.
I think only the last result needs R to be a field. The rest hold under weaker assumptions. Please try to minimize the assumptions you need on R by changing them per theorem as needed.
There was a problem hiding this comment.
Cool. Will do this first thing tomorrow. Thanks!
There was a problem hiding this comment.
Can you also adjust the docstring accordingly?
There was a problem hiding this comment.
Certainly! I'll do this now...
j-loreaux
reviewed
Jun 24, 2024
j-loreaux
reviewed
Jun 24, 2024
j-loreaux
added
awaiting-author
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
j-loreaux
reviewed
Jun 25, 2024
j-loreaux
added
awaiting-author
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
…ted the hypotheses in the theorems they went with, as Jireh suggested.
JonBannon
added
awaiting-review
and removed
awaiting-author
|
maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by j-loreaux. |
j-loreaux
changed the title
SpectrumDiagonal section
|
Thanks! bors r+ |
github-actions
bot
added
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jun 27, 2024
…13837) We add various theorems that assert the spectrum of a diagonal matrix is the range of the diagonal viewed as a function. Co-Authored by @j-loreaux Co-authored-by: JonBannon <59937998+JonBannon@users.noreply.github.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
dagurtomas
pushed a commit
that referenced
this pull request
Jul 2, 2024
…13837) We add various theorems that assert the spectrum of a diagonal matrix is the range of the diagonal viewed as a function. Co-Authored by @j-loreaux Co-authored-by: JonBannon <59937998+JonBannon@users.noreply.github.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jul 9, 2024
…atrices over an RCLike Field (#13697) This file contains the requisite lemmas needed to define a `ContinuousFunctionalCalculus` for Hermitian Matrices over an RCLike Field. - [x] depends on: #13729 - [x] depends on: #13765 - [x] depends on : #13837 - [x] depends on : #13838 Co-Authored by @j-loreaux Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jul 9, 2024
…atrices over an RCLike Field (#13697) This file contains the requisite lemmas needed to define a `ContinuousFunctionalCalculus` for Hermitian Matrices over an RCLike Field. - [x] depends on: #13729 - [x] depends on: #13765 - [x] depends on : #13837 - [x] depends on : #13838 Co-Authored by @j-loreaux Co-authored-by: JonBannon <59937998+JonBannon@users.noreply.github.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
We add various theorems that assert the spectrum of a diagonal matrix is the range of the diagonal viewed as a function.
Co-Authored by @j-loreaux