Revision #3036 → #3561 · back to history
modifiedSpectral theorem for unbounded self-adjoint operators (box)6c20e7031758
| Field | From #3036 | To #3561 |
|---|
| note | The unbounded spectral theorem (resolution of identity for unbounded self-adjoint operators) is notin Mathlib. | The unbounded spectral theorem (resolution of identity for unbounded self-adjoint operators) is not in Mathlib. |
modifiedCompact operator has convergent subsequence characterization11cbc150b1cd
| Field | From #3036 | To #3561 |
|---|
| note | Duplicates the compact-operator definition annotation; kept for the sequential characterization phrasing. | Sequential characterization of compact operators; specializes the general `IsCompactOperator` definition to Hilbert-space sequences. |
| provenance | ai | ai-moderated |
| section | — | — |
addedSymmetry of the dot product on ℝ³48da3faf8085
addedBilinearity of the dot product5131b92d06cd
addedPositive definiteness of the dot productb3128763a5d6
addedNorm from inner product (‖x‖ = √⟨x,x⟩)bcd05b16e283
addedFock space42326ec03fdb
addedDensity matrix (mixed state)41164498825b
addedBra–ket / Riesz correspondenceda724ea56aaf
addedBergman space is a closed subspace of L²(D)05b6e57335a7
addedSpectral theorem for compact self-adjoint operators (box)5e4ba8c30546