feat(analysis/fourier): Riemann-Lebesgue lemma (#17719)
This PR adds a proof that for any function `f` on a finite-dimensional real vector space `V`, the integral `∫ (v : V), exp (-2 * π * w v * I) • f x` tends to 0 as `w` goes to infinity (wrt the cocompact filter on the dual space `W` of `V`).
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
