Plancherel's theorem

Stream: Is there code for X?

[Joseph Tooby-Smith]

I know there is an incomplete version of Plancherel's theorem in the Bonn Analysis project of
@Floris van Doorn's. I just wanted to check whether a complete version made it in to Mathlib or somewhere else?

I'm needing it to prove the completeness of polynomials in a weighted L^2 space.

[Floris van Doorn]

Unfortunately not, although @Michael Rothgang (currently on holiday) is also interested in cleaning it up.
If you want to use the incomplete proofs there as a basis for a full formalization and put that into Mathlib, please do!

[Joseph Tooby-Smith]

Ok, many thanks for this info!