Lean 4 code of the proof of the Spectral Theorem

Stream: mathlib4

[Oliver]

Could anyone please provide an error-free Lean 4 code of the proof of the Spectral Theorem? Thanks a lot.

[Yury G. Kudryashov]

What exact statement do you mean? git grep -i 'spectral.*theorem' gives some results. Does either of them work for you?

[Oliver]

Yury G. Kudryashov said:

What exact statement do you mean? git grep -i 'spectral.*theorem' gives some results. Does either of them work for you?

Why does it say "fatal: not a git repository (or any of the parent directories): .git" when running "git grep -i 'spectral.*theorem'"? Thanks.

[Yury G. Kudryashov]

Are you in the folder with a git clone of the Mathlib4 repo?

[Shreyas Srinivas]

https://www.moogle.ai/search/raw?q=spectral%20theorem

[Yury G. Kudryashov]

@Oliver Let me repeat my question. Yury G. Kudryashov said:

What exact statement do you mean?

E.g., do you need the infinite-dimensional case?

[Jireh Loreaux]

Yeah, you're really going to need to be more precise about what you mean by "spectral theorem". I'm familiar with more theorems (closely related) than I have fingers that go by that name. For instance, you could mean:

• diagonalization of normal matrices
• diagonalization of selfadjoint matrices
• diagonalization of symmetric linear maps on a finite dimensional inner product space
• diagonalization of symmetric linear maps on a finite dimensional inner product space
• the continuous functional calculus in a C⋆-algebra
• the Borel functional calculus in a von Neumann algebra
• diagonalization of compact normal operators on a Hilbert space
• diagonalization of compact selfadjoint operators on a Hilbert space
• many more variations on these

Some of these we have. Others we don't. Some that we don't have could be obtained with a few hours effort, some with many months effort.

[Kim Morrison]

And that doesn't even mention unbounded operators! :-) One day ...