Revision #2325 → #3031 · back to history
modifiedEigenvalue (corresponding factor)c0a2f64affa2
| Field | From #2325 | To #3031 |
|---|
| note | `HasEigenvalue f μ` is the scaling factor of an eigenvector. | `HasEigenvalue f μ` (defined as `eigenspace f μ ≠ ⊥`) is the scaling factor of an eigenvector. |
modifiedEigenvector of a matrix0a898addaa78
| Field | From #2325 | To #3031 |
|---|
| note | Matrix eigenvectors are handled by applying `HasEigenvector` to `Matrix.toLin'` or `toLin b b`, e.g. `hasEigenvector_toLin'_diagonal`. | Matrix eigenvectors are handled by applying `HasEigenvector` to `Matrix.toLin'` or `toLin b b`; e.g. `hasEigenvector_toLin'_diagonal` in `Eigenspace.Matrix`. |
modifiedMona Lisa shear mappingb94648eaa6a2
| Field | From #2325 | To #3031 |
|---|
| note | This is an illustrative pictorial example not formalized in Mathlib. | Illustrative pictorial example, not formalized. |
modifiedEigenfunctions of a differential operator593b735058a5
| Field | From #2325 | To #3031 |
|---|
| note | Eigenfunctions are special cases of `HasEigenvector` for a linear differential operator, but no dedicated `eigenfunction` API exists. | Eigenfunctions are special cases of `HasEigenvector` applied to a linear differential operator, but no dedicated `eigenfunction` API exists. |
modifiedEigensystem, eigenspace, eigenbasisdc347363b61c
| Field | From #2325 | To #3031 |
|---|
| note | `eigenspace` and `Eigenvalues` are defined; `Matrix.IsHermitian.eigenvectorBasis` gives an eigenbasis in the Hermitian case, but no general `eigenbasis`/`eigensystem` term. | `eigenspace` and `Eigenvalues` are defined; `Matrix.IsHermitian.eigenvectorBasis` gives an eigenbasis in the Hermitian case, but there is no general `eigenbasis`/`eigensystem` term. |
modifiedEquivalent form using identity matrixe3fe4f617be5
| Field | From #2325 | To #3031 |
|---|
| note | `eigenspace_def` shows `eigenspace f μ = LinearMap.ker (f - μ • 1)`, i.e. `(A - λI)v = 0`. | `eigenspace_def` shows `eigenspace f μ = LinearMap.ker (f - μ • 1)`, i.e. `(A − λI)v = 0`. |
modifiedFactoring the characteristic polynomial2258deabe732
| Field | From #2325 | To #3031 |
|---|
| note | `charpoly_natDegree` gives degree `n`; combined with degree bounds on root counts, this matches the at-most-n claim. | `charpoly_natDegree` gives degree `n`; combined with degree bounds on root counts, this matches the at-most-`n` claim. |
addedOdd-order real matrix has a real eigenvaluefc203e83fde7
modifiedAlgebraic multiplicityfb7068b487d5
| Field | From #2325 | To #3031 |
|---|
| note | `rootMultiplicity` of `charpoly` gives algebraic multiplicity but no dedicated `algebraicMultiplicity` for eigenvalues. | `rootMultiplicity` of `charpoly` gives algebraic multiplicity, but there is no dedicated `algebraicMultiplicity` for eigenvalues. |
addedEigenspace is the nullspace of A − λI0af6d6413aa8
modifiedGeometric multiplicity bounded by algebraic multiplicity972f3ee99a2d
| Field | From #2325 | To #3031 |
|---|
| mathlib.decl | — | LinearMap.finrank_eigenspace_le |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.LinearAlgebra.Eigenspace.Zero |
| note | Could not locate this inequality formalized in Mathlib. | `LinearMap.finrank_eigenspace_le` states `finrank K (eigenspace f μ) ≤ rootMultiplicity μ (charpoly f)`, i.e. geometric ≤ algebraic multiplicity. |
| status | not_formalized | formalized |
modifiedProof that geometric ≤ algebraic multiplicity9c5e23fedfa9
| Field | From #2325 | To #3031 |
|---|
| mathlib.decl | — | LinearMap.finrank_eigenspace_le |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.LinearAlgebra.Eigenspace.Zero |
| note | Proof of the geometric-vs-algebraic multiplicity inequality not located. | The inequality itself is proved as `LinearMap.finrank_eigenspace_le`, from `LinearMap.finrank_genEigenspace_le` in `Eigenspace.Zero`. |
| status | not_formalized | formalized |
modifiedHermitian matrices have real eigenvalues899e47b0f9e3
| Field | From #2325 | To #3031 |
|---|
| note | `IsHermitian.eigenvalues : n → ℝ` returns real eigenvalues; `eigenvalues_mem_spectrum_real` puts them in `spectrum ℝ A`. | `IsHermitian.eigenvalues : n → ℝ` returns real eigenvalues; `eigenvalues_mem_spectrum_real` places them in `spectrum ℝ A`. |
modifiedMatrix and transpose share eigenvaluesc61397839533
| Field | From #2325 | To #3031 |
|---|
| note | `(Aᵀ).charpoly = A.charpoly`, so by `mem_spectrum_iff_isRoot_charpoly` they share eigenvalues. | `(Aᵀ).charpoly = A.charpoly`, so by `Matrix.mem_spectrum_iff_isRoot_charpoly` they share eigenvalues. |
modifiedDiagonalizability iff eigenvectors form a basis008e5f28db65
| Field | From #2325 | To #3031 |
|---|
| note | Captured via semisimplicity / eigenspaces spanning; no explicit `diagonalizable_iff_eigenvectors_basis` lemma. | Captured via semisimplicity/eigenspaces spanning; no explicit `diagonalizable_iff_eigenvectors_basis` lemma. |
modifiedDefective matrix and Jordan normal form52f3757be9c0
| Field | From #2325 | To #3031 |
|---|
| note | Generalized eigenspaces exist and Jordan–Chevalley decomposition is formalized; full Jordan normal form and `defective` predicate are not. | Generalized eigenspaces exist and Jordan–Chevalley decomposition is formalized; full Jordan normal form and a `defective` predicate are not. |
modifiedAt most n distinct eigenvalues in dimension n34e9947f1947
| Field | From #2325 | To #3031 |
|---|
| mathlib.match_kind | exact | generalization |
| note | `instFintypeEigenvalues` makes `f.Eigenvalues` a `Fintype` for an endomorphism of a finite-dimensional module. | `instFintypeEigenvalues` makes `f.Eigenvalues` a `Fintype` (and `Module.End.finite_spectrum` gives finiteness in finite dimensions); the tight bound `≤ n` follows from `eigenvectors_linearIndependent` but is not stated as a single lemma. |
modifiedEigenvalues of the inverse are reciprocals00ffc4baf231
| Field | From #2325 | To #3031 |
|---|
| note | `spectrum.inv_mem_iff` shows `↑r ∈ spectrum R ↑a ↔ ↑r⁻¹ ∈ spectrum R ↑a⁻¹`, giving the reciprocal-eigenvalues fact for units. | `spectrum.inv_mem_iff` shows `↑r ∈ spectrum R ↑a ↔ ↑r⁻¹ ∈ spectrum R ↑a⁻¹`, giving reciprocal eigenvalues for units. |
modifiedGeneralized eigenvectors and generalized eigenspacesc192c3e14a63
| Field | From #2325 | To #3031 |
|---|
| note | `Module.End.genEigenspace f μ k` defines the generalized eigenspaces; `iSup_genEigenspace_eq_top_of_isAlgClosed` decomposes the whole space over an algebraically closed field. | `Module.End.genEigenspace f μ k` defines the generalized eigenspaces. |
modifiedDecomposition into generalized eigenspaces over algebraically closed fieldsf88634d6b1cf
| Field | From #2325 | To #3031 |
|---|
| note | The decomposition into generalized eigenspaces is formalized over algebraically closed fields (in `Eigenspace.Triangularizable`); the full Jordan normal form classification itself is not yet in Mathlib. | The decomposition into generalized eigenspaces is formalized over algebraically closed fields (in `Eigenspace.Triangularizable`); full Jordan normal form itself is not yet in Mathlib. |