mathlib documentation


The Riemann-Lebesgue Lemma #

In this file we prove a weak form of the Riemann-Lebesgue lemma, stating that for any compactly-supported continuous function f on (valued in some complete normed space E), the integral

∫ (x : ℝ), exp (↑(t * x) * I) • f x

tends to zero as t → ∞. (The actual lemma is that this holds for all functions f, which follows from the result proved here together with the fact that continuous, compactly-supported functions are dense in L¹(ℝ), which will be proved in a future iteration.)

Main results #

The integrand in the Riemann-Lebesgue lemma is integrable.

theorem fourier_integral_half_period_translate {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E} [complete_space E] {t : } (ht : t 0) :
(x : ), cexp ((t * x) * complex.I) f (x + real.pi / t) = - (x : ), cexp ((t * x) * complex.I) f x

Shifting f by π / t negates the integral in the Riemann-Lebesgue lemma.

Rewrite the Riemann-Lebesgue integral in a form that allows us to use uniform continuity.

Riemann-Lebesgue Lemma for continuous and compactly-supported functions: the integral ∫ x, exp (t * x * I) • f x tends to 0 as t gets large.

Riemann-Lebesgue lemma for continuous compactly-supported functions: the Fourier transform tends to 0 at infinity.