The Spectral Theorem

The principal assertion of the spectral theorem is that every bounded normal operator $T$ on a Hilbert space induces (in a canonical way) a resolution $E$ of the identity on the Borel subsets of its spectrum $\sigma(T)$ and that $T$ can be reconstructed from $E$ by an integral. A large part of the theory of normal operators depends on this fact.

Information about the project

An ongoing multi-author open source project to formalise a proof of The Spectral Theorem in Lean 4.