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).