# Commit 2023-04-30 20:09 9425b6f8

View on Github →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`

).