Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes