Lean 4 - The Spectral Theorem

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

This project

Current maintainers:

• Oliver Butterley
• Yoh Tanimoto

We aren't so wise to know for sure how big a task it will be to formalize this theorem but we believe we can make some good progress so we are trying.

Collaborating

We welcome anyone who wants to be part of this.