Fourier series

Stream: maths

[Heather Macbeth]

I just PR'd a proof of Parseval's identity: #11320. In true mathlib fashion, this project had a lot of unwitting collaborators :). My thanks to

• @Rémy Degenne, who defined Lp spaces of measurable functions
• @Floris van Doorn, who constructed Haar measure
• @Yury G. Kudryashov, who proved Urysohn's lemma
• @Scott Morrison, who proved the Stone-Weierstrass theorem

and to everyone else who has helped to build up the measure theory, calculus and inner product space libraries!

[Kevin Buzzard]

This is mathlib's secret sauce -- everything being able to interact with everything else