Documentation

Mathlib.Analysis.Fourier.RiemannLebesgueLemma

The Riemann-Lebesgue Lemma #

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

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

This is true for arbitrary functions, but is only interesting for 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 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 #

theorem fourierIntegral_half_period_translate {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {f : VE} [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProductSpace V] [FiniteDimensional V] {w : V} (hw : w 0) :
∫ (v : V), Real.fourierChar (-inner v w) f (v + (fun (w : V) => (1 / (2 * w ^ 2)) w) w) = -∫ (v : V), Real.fourierChar (-inner v w) f v

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

theorem fourierIntegral_eq_half_sub_half_period_translate {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {f : VE} [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProductSpace V] [FiniteDimensional V] {w : V} (hw : w 0) (hf : MeasureTheory.Integrable f MeasureTheory.volume) :
∫ (v : V), Real.fourierChar (-inner v w) f v = (1 / 2) ∫ (v : V), Real.fourierChar (-inner v w) (f v - f (v + (fun (w : V) => (1 / (2 * w ^ 2)) w) w))

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

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} [NormedAddCommGroup E] [NormedSpace E] (f : VE) [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProductSpace V] [FiniteDimensional V] :
Filter.Tendsto (fun (w : V) => ∫ (v : V), Real.fourierChar (-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 → ∞.

theorem Real.tendsto_integral_exp_smul_cocompact {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (f : E) :
Filter.Tendsto (fun (w : ) => ∫ (v : ), Real.fourierChar (-(v * w)) f v) (Filter.cocompact ) (nhds 0)

The Riemann-Lebesgue lemma for functions on .

The Riemann-Lebesgue lemma for functions on , formulated via Real.fourierIntegral.

theorem tendsto_integral_exp_smul_cocompact_of_inner_product {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (f : VE) [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProductSpace V] [FiniteDimensional V] (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure] :
Filter.Tendsto (fun (w : V →L[] ) => ∫ (v : V), Real.fourierChar (-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.

theorem tendsto_integral_exp_smul_cocompact {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (f : VE) [AddCommGroup V] [TopologicalSpace V] [TopologicalAddGroup V] [T2Space V] [MeasurableSpace V] [BorelSpace V] [Module V] [ContinuousSMul V] [FiniteDimensional V] (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure] :
Filter.Tendsto (fun (w : V →L[] ) => ∫ (v : V), Real.fourierChar (-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.

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