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

source

theorem fourier_integrand_integrable {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {f : ℝ → E} (hf : measure_theory.integrable f measure_theory.measure_space.volume) (t : ℝ) :

measure_theory.integrable (λ (x : ℝ), cexp (↑(t * x) * complex.I) • f x) measure_theory.measure_space.volume

The integrand in the Riemann-Lebesgue lemma is integrable.

source

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.

source

theorem fourier_integral_eq_half_sub_half_period_translate {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {f : ℝ → E} [complete_space E] {t : ℝ} (ht : t ≠ 0) (hf : measure_theory.integrable f measure_theory.measure_space.volume) :

∫ (x : ℝ), cexp (↑(t * x) * complex.I) • f x = (1 / 2) • ∫ (x : ℝ), cexp (↑(t * x) * complex.I) • (f x - f (x + real.pi / t))

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

source

theorem tendsto_integral_mul_exp_at_top_of_continuous_compact_support {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {f : ℝ → E} [complete_space E] (hf1 : continuous f) (hf2 : has_compact_support f) :

filter.tendsto (λ (t : ℝ), ∫ (x : ℝ), cexp (↑(t * x) * complex.I) • f x) filter.at_top (nhds 0)

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.

source

theorem tendsto_integral_mul_exp_at_bot_of_continuous_compact_support {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {f : ℝ → E} [complete_space E] (hf1 : continuous f) (hf2 : has_compact_support f) :

filter.tendsto (λ (t : ℝ), ∫ (x : ℝ), cexp (↑(t * x) * complex.I) • f x) filter.at_bot (nhds 0)

source

theorem zero_at_infty_integral_mul_exp_of_continuous_compact_support {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {f : ℝ → E} [complete_space E] (hf1 : continuous f) (hf2 : has_compact_support f) :

filter.tendsto (λ (t : ℝ), ∫ (x : ℝ), cexp (↑(t * x) * complex.I) • f x) (filter.cocompact ℝ) (nhds 0)

source

theorem real.fourier_integral_zero_at_infty_of_continuous_compact_support {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {f : ℝ → E} [complete_space E] (hc : continuous f) (hs : has_compact_support f) :

filter.tendsto (real.fourier_integral f) (filter.cocompact ℝ) (nhds 0)

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