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 L¹
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 #
tendsto_integral_mul_exp_at_top_of_continuous_compact_support
: the Riemann-Lebesgue lemma for continuous compactly-supported functions onℝ
.
The integrand in the Riemann-Lebesgue lemma is integrable.
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.