mathlib

049d2aca - feat(analysis/fourier): Fourier series for functions in L2; Parseval's identity (#11320)