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
ℝ (valued in some complete normed space
∫ (x : ℝ), exp (↑(t * x) * I) • f x
tends to zero as
t → ∞. (The actual lemma is that this holds for all
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.
π / 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.