mathlib3documentation

analysis.fourier.riemann_lebesgue_lemma

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.
theorem fourier_integrand_integrable {E : Type u_1} {V : Type u_2} [ E] {f : V E} [borel_space V] (w : V) :

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

theorem fourier_integral_half_period_translate {E : Type u_1} {V : Type u_2} [ E] {f : V E} [borel_space V] {w : V} (hw : w 0) :
(v : V), f (v + (λ (w : V), (1 / (2 * w ^ 2)) w) w) = - (v : V), f v

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

theorem fourier_integral_eq_half_sub_half_period_translate {E : Type u_1} {V : Type u_2} [ E] {f : V E} [borel_space V] {w : V} (hw : w 0)  :
(v : V), f v = (1 / 2) (v : V), (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.

theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support {E : Type u_1} {V : Type u_2} [ E] {f : V E} [borel_space V] (hf1 : continuous f) (hf2 : has_compact_support f) :
filter.tendsto (λ (w : V), (v : V), f 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.

theorem tendsto_integral_exp_inner_smul_cocompact {E : Type u_1} {V : Type u_2} [ E] (f : V E) [borel_space V]  :
filter.tendsto (λ (w : V), (v : V), f 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 → ∞.

The Riemann-Lebesgue lemma for functions on ℝ.

theorem real.zero_at_infty_fourier_integral {E : Type u_1} [ E] (f : E) :

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

theorem tendsto_integral_exp_smul_cocompact_of_inner_product {E : Type u_1} {V : Type u_2} [ E] (f : V E) [borel_space V] (μ : measure_theory.measure V)  :
filter.tendsto (λ (w : V →L[] ), (v : 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.

theorem tendsto_integral_exp_smul_cocompact {E : Type u_1} {V : Type u_2} [ E] (f : V E) [t2_space V] [borel_space V] [ V] (μ : measure_theory.measure V)  :
filter.tendsto (λ (w : V →L[] ), (v : 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.

theorem real.zero_at_infty_vector_fourier_integral {E : Type u_1} {V : Type u_2} [ E] (f : V E) [t2_space V] [borel_space V] [ V] (μ : measure_theory.measure V)  :
(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).