The Riemann-Lebesgue Lemma #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove the Riemann-Lebesgue lemma, for functions on finite-dimensional real vector spaces V: if f is a function on V (valued in a complete normed space E), then the Fourier transform of f, viewed as a function on the dual space of V, tends to 0 along the cocompact filter. Here the Fourier transform is defined by

λ w : V →L[ℝ] ℝ, ∫ (v : V), exp (↑(2 * π * w v) * I) • f x.

This is true for arbitrary functions, but is only interesting for L¹ functions (if f is not integrable then the integral is zero for all w). This is proved first for continuous compactly-supported functions on inner-product spaces; then we pass to arbitrary functions using the density of continuous compactly-supported functions in L¹ space. Finally we generalise from inner-product spaces to arbitrary finite-dimensional spaces, by choosing a continuous linear equivalence to an inner-product space.

Main results #

tendsto_integral_exp_inner_smul_cocompact : for V a finite-dimensional real inner product space and f : V → E, the function λ w : V, ∫ v : V, exp (2 * π * ⟪w, v⟫ * I) • f v tends to 0 along cocompact V.
tendsto_integral_exp_smul_cocompact : for V a finite-dimensional real vector space (endowed with its unique Hausdorff topological vector space structure), and W the dual of V, the function λ w : W, ∫ v : V, exp (2 * π * w v * I) • f v tends to along cocompact W.
real.tendsto_integral_exp_smul_cocompact: special case of functions on ℝ.
real.zero_at_infty_fourier_integral and real.zero_at_infty_vector_fourier_integral: reformulations explicitly using the Fourier integral.

source

theorem fourier_integrand_integrable {E : Type u_1} {V : Type u_2} [normed_add_comm_group E] [normed_space ℂ E] {f : V → E} [normed_add_comm_group V] [measurable_space V] [borel_space V] [inner_product_space ℝ V] [finite_dimensional ℝ V] (w : V) :

measure_theory.integrable f measure_theory.measure_space.volume ↔ measure_theory.integrable (λ (v : V), ↑(⇑real.fourier_char (⇑multiplicative.of_add (-has_inner.inner v w))) • f v) measure_theory.measure_space.volume

The integrand in the Riemann-Lebesgue lemma for f is integrable iff f is.

source

theorem fourier_integral_half_period_translate {E : Type u_1} {V : Type u_2} [normed_add_comm_group E] [normed_space ℂ E] {f : V → E} [normed_add_comm_group V] [measurable_space V] [borel_space V] [inner_product_space ℝ V] [finite_dimensional ℝ V] [complete_space E] {w : V} (hw : w ≠ 0) :

∫ (v : V), ↑(⇑real.fourier_char (⇑multiplicative.of_add (-has_inner.inner v w))) • f (v + (λ (w : V), (1 / (2 * ‖w‖ ^ 2)) • w) w) = -∫ (v : V), ↑(⇑real.fourier_char (⇑multiplicative.of_add (-has_inner.inner v w))) • f v

Shifting f by (1 / (2 * ‖w‖ ^ 2)) • w negates the integral in the Riemann-Lebesgue lemma.

source

theorem fourier_integral_eq_half_sub_half_period_translate {E : Type u_1} {V : Type u_2} [normed_add_comm_group E] [normed_space ℂ E] {f : V → E} [normed_add_comm_group V] [measurable_space V] [borel_space V] [inner_product_space ℝ V] [finite_dimensional ℝ V] [complete_space E] {w : V} (hw : w ≠ 0) (hf : measure_theory.integrable f measure_theory.measure_space.volume) :

∫ (v : V), ↑(⇑real.fourier_char (⇑multiplicative.of_add (-has_inner.inner v w))) • f v = (1 / 2) • ∫ (v : V), ↑(⇑real.fourier_char (⇑multiplicative.of_add (-has_inner.inner v w))) • (f v - f (v + (λ (w : V), (1 / (2 * ‖w‖ ^ 2)) • w) w))

Rewrite the Fourier integral in a form that allows us to use uniform continuity.

source

theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support {E : Type u_1} {V : Type u_2} [normed_add_comm_group E] [normed_space ℂ E] {f : V → E} [normed_add_comm_group V] [measurable_space V] [borel_space V] [inner_product_space ℝ V] [finite_dimensional ℝ V] [complete_space E] (hf1 : continuous f) (hf2 : has_compact_support f) :

filter.tendsto (λ (w : V), ∫ (v : V), ↑(⇑real.fourier_char (⇑multiplicative.of_add (-has_inner.inner v w))) • f v) (filter.cocompact V) (nhds 0)

Riemann-Lebesgue Lemma for continuous and compactly-supported functions: the integral ∫ v, exp (-2 * π * ⟪w, v⟫ * I) • f v tends to 0 wrt cocompact V. Note that this is primarily of interest as a preparatory step for the more general result tendsto_integral_exp_inner_smul_cocompact in which f can be arbitrary.

source

theorem tendsto_integral_exp_inner_smul_cocompact {E : Type u_1} {V : Type u_2} [normed_add_comm_group E] [normed_space ℂ E] (f : V → E) [normed_add_comm_group V] [measurable_space V] [borel_space V] [inner_product_space ℝ V] [finite_dimensional ℝ V] [complete_space E] :

filter.tendsto (λ (w : V), ∫ (v : V), ↑(⇑real.fourier_char (⇑multiplicative.of_add (-has_inner.inner v w))) • f v) (filter.cocompact V) (nhds 0)

Riemann-Lebesgue lemma for functions on a real inner-product space: the integral ∫ v, exp (-2 * π * ⟪w, v⟫ * I) • f v tends to 0 as w → ∞.

source

theorem real.tendsto_integral_exp_smul_cocompact {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : ℝ → E) :

filter.tendsto (λ (w : ℝ), ∫ (v : ℝ), ↑(⇑real.fourier_char (⇑multiplicative.of_add (-(v * w)))) • f v) (filter.cocompact ℝ) (nhds 0)

The Riemann-Lebesgue lemma for functions on ℝ.

source

theorem real.zero_at_infty_fourier_integral {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : ℝ → E) :

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

The Riemann-Lebesgue lemma for functions on ℝ, formulated via real.fourier_integral.

source

theorem tendsto_integral_exp_smul_cocompact_of_inner_product {E : Type u_1} {V : Type u_2} [normed_add_comm_group E] [normed_space ℂ E] (f : V → E) [normed_add_comm_group V] [measurable_space V] [borel_space V] [inner_product_space ℝ V] [finite_dimensional ℝ V] [complete_space E] (μ : measure_theory.measure V) [μ.is_add_haar_measure] :

filter.tendsto (λ (w : V →L[ℝ ] ℝ), ∫ (v : V), ↑(⇑real.fourier_char (⇑multiplicative.of_add (-⇑w v))) • f v ∂μ) (filter.cocompact (V →L[ℝ ] ℝ)) (nhds 0)

Riemann-Lebesgue lemma for functions on a finite-dimensional inner-product space, formulated via dual space. Do not use -- it is only a stepping stone to tendsto_integral_exp_smul_cocompact where the inner-product-space structure isn't required.

source

theorem tendsto_integral_exp_smul_cocompact {E : Type u_1} {V : Type u_2} [normed_add_comm_group E] [normed_space ℂ E] (f : V → E) [add_comm_group V] [topological_space V] [topological_add_group V] [t2_space V] [measurable_space V] [borel_space V] [module ℝ V] [has_continuous_smul ℝ V] [finite_dimensional ℝ V] [complete_space E] (μ : measure_theory.measure V) [μ.is_add_haar_measure] :

filter.tendsto (λ (w : V →L[ℝ ] ℝ), ∫ (v : V), ↑(⇑real.fourier_char (⇑multiplicative.of_add (-⇑w v))) • f v ∂μ) (filter.cocompact (V →L[ℝ ] ℝ)) (nhds 0)

Riemann-Lebesgue lemma for functions on a finite-dimensional real vector space, formulated via dual space.

source

theorem real.zero_at_infty_vector_fourier_integral {E : Type u_1} {V : Type u_2} [normed_add_comm_group E] [normed_space ℂ E] (f : V → E) [add_comm_group V] [topological_space V] [topological_add_group V] [t2_space V] [measurable_space V] [borel_space V] [module ℝ V] [has_continuous_smul ℝ V] [finite_dimensional ℝ V] [complete_space E] (μ : measure_theory.measure V) [μ.is_add_haar_measure] :

filter.tendsto (vector_fourier.fourier_integral real.fourier_char μ (top_dual_pairing ℝ V).flip f) (filter.cocompact (V →L[ℝ ] ℝ)) (nhds 0)

The Riemann-Lebesgue lemma, formulated in terms of vector_fourier.fourier_integral (with the pairing in the definition of fourier_integral taken to be the canonical pairing between V and its dual space).