{"id":"palomar/PALOMAR-2026-09-01-000004","url":"https://github.com/savarin/lean-spectral-theory/tree/d19e279f0ab244657f02ce678e8d67fa69e2f407","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-01-000004-v1.json","repo":"https://github.com/savarin/lean-spectral-theory","tags":["math.FA","math.OA","msc:47A10","msc:47B15","spectral-theory","functional-analysis","lean","unbounded-operators"],"score":0,"title":"lean-spectral-theory","trust":"high","domain":"math.FA","source":"palomar","authors":["Ezzeri Esa"],"reviews":0,"subject":"math.FA","summary":"The spectral theorem for possibly unbounded self-adjoint operators on complex Hilbert spaces, formalized through the Cayley transform and real projection-valued measures. The selected spectral theorem constructs a PVM whose scalar measures give the exact finite-second-moment domain and first-moment quadratic form, with measurable-set uniqueness, and is proved equivalent to equality with the unbounded coordinate spectral integral. The selected Stone theorem proves both that strongly continuous one-parameter unitary groups have self-adjoint generators and that every self-adjoint operator…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-01","reactions":{},"formalized":true,"formalizes":[{"title":"Unbounded Self-adjoint Operators on Hilbert Space","identifier":"10.1007/978-94-007-4753-1","relationship":"formalizes"},{"title":"Methods of Modern Mathematical Physics I: Functional Analysis","identifier":"ISBN 978-0-12-585050-6","relationship":"formalizes"}]}