Spectral theorem for bounded normal operators

Stream: maths

[Kevin Buzzard]

I'm on a call right now with Jan van Neerven, who asks how far we are from proving theorem 9.18 in his book https://fa.ewi.tudelft.nl/~neerven/FA/JvN-Functional_Analysis.pdf.

spectral.png

[Heather Macbeth]

@Kevin Buzzard This has definitely been discussed by @Frédéric Dupuis, @Jireh Loreaux, myself and others. It might well be in mathlib within a year. You saw that the corresponding theorem for compact operators is in the preprint from Frédéric, Rob and me? (for self-adjoint rather than normal operators, but the barrier was now-mostly-unlocked results in complex analysis.)

[Jireh Loreaux]

Heather is a bit more optimistic than I am about the timeline, but we're definitely making progress. I would argue that one of the big obstacles to getting this result is the common mathlib problem of doing things in the right generality.

That is, if you're going to prove this result, then you want to do it for normal operators in von Neumann algebras (this is essentially the Borel functional calculus after all), but we haven't even yet defined von Neumann algebras, and we will have to make some highly nontrivial decisions to do so. For example, do we carry around a Hilbert space on which the von Neumann algebra acts, or do we instead carry around its pre-dual? It's not at all obvious to me right now which is preferable.

Of course, we could go directly for 9.18, in which case I'm pretty sure we could get it in mathlib this year, but I don't know why we would do that. While the Borel functional calculus might be a ways off, we are not too far off from the continuous functional calculus for normal operators in C*-algebras.

[Jireh Loreaux]

It also just depends on what we focus on (obviously). For example, if we get the basics of $C^*$-algebras and then focus on von Neumann algebra theory right away, then it will come sooner. But if we instead focus for a while on $C^*$-algebra theory, that will take us in a very different direction. This is likely far from obvious for nonspecialists, but in $C^*$-algebra theory there is rich interplay between the unital and non-unital algebras which drives much of theory (e.g., the 6-term cyclic exact sequence in K-theory), whereas in von Neumann algebras all the algebras are unital and the K-theory is much simpler, or even trivial.