Revision #1577 → #1797 · back to history
modifiedCauchy: real symmetric matrices are diagonalizable2fe9b30d4b08
| Field | From #1577 | To #1797 |
|---|
| mathlib.match_kind | special_case | generalization |
| note | Mathlib's spectral theorem unitarily diagonalizes any Hermitian matrix over an RCLike field; real symmetric matrices are the special case 𝕜 = ℝ. | Mathlib's `Matrix.IsHermitian.spectral_theorem` unitarily diagonalizes any Hermitian matrix over an RCLike field; real symmetric matrices are the special case 𝕜 = ℝ. |
modifiedHermitian condition4321fa255016
| Field | From #1577 | To #1797 |
|---|
| anchors | [{"section":"Hermitian maps and Hermitian matrices","snippet":"The Hermitian condition on"},{"type":"math_alttext","value":"{\\displaystyle \\langle Ax,y\\rangle =\\langle x,Ay\\rangle .}"}] | — |
addedFundamental theorem of algebra (used in proof)46186301d7ef
modifiedSpectral decomposition394617882454
| Field | From #1577 | To #1797 |
|---|
| anchors | [{"section":"Hermitian maps and Hermitian matrices","snippet":"called its spectral decomposition"},{"type":"math_alttext","value":"{\\displaystyle V_{\\lambda }=\\{v\\in V:Av=\\lambda v\\}}"}] | — |
| mathlib.match_kind | special_case | exact |
modifiedEigenspaced229f4d67e4d
| Field | From #1577 | To #1797 |
|---|
| anchors | [{"section":"Hermitian maps and Hermitian matrices","snippet":"be the eigenspace corresponding to an eigenvalue"},{"type":"math_alttext","value":"{\\displaystyle V_{\\lambda }=\\{v\\in V:Av=\\lambda v\\}}"}] | — |
modifiedNormal operator5fb0461ca161
| Field | From #1577 | To #1797 |
|---|
| mathlib.module | Mathlib.Algebra.Star.Basic | Mathlib.Algebra.Star.SelfAdjoint |
modifiedMultiplication by t with no eigenvectorsdb166985c77c
| Field | From #1577 | To #1797 |
|---|
| anchors | [{"section":"Possible absence of eigenvectors","snippet":"let A be the operator of multiplication by t"},{"type":"math_alttext","value":"{\\displaystyle [Af](t)=tf(t).}"}] | — |
modifiedProjection-valued measure formulation1d50c204f37f
| Field | From #1577 | To #1797 |
|---|
| anchors | [{"section":"Spectral subspaces and projection-valued measures","snippet":"One formulation of the spectral theorem expresses the operator A as an integral"},{"type":"math_alttext","value":"{\\displaystyle A=\\int _{\\sigma (A)}\\lambda \\,d\\pi (\\lambda ).}"}] | — |
addedOperator norm equals magnitude of largest eigenvalue7dc75dd755f0
modifiedDirect integral Hilbert space02cc1e500a97
| Field | From #1577 | To #1797 |
|---|
| anchors | [{"section":"Direct integrals","snippet":"We then form the direct integral Hilbert space"},{"type":"math_alttext","value":"{\\displaystyle \\int _{\\mathbf {R} }^{\\oplus }H_{\\lambda }\\,d\\mu (\\lambda ).}"}] | — |
modifiedFunctional calculus88bcb6018336
| Field | From #1577 | To #1797 |
|---|
| anchors | [{"section":"Functional calculus","snippet":"the idea of defining a functional calculus"},{"type":"math_alttext","value":"{\\displaystyle [f(A)s](\\lambda )=f(\\lambda )s(\\lambda ).}"}] | — |