# 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

λ 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_fourierIntegral and Real.zero_at_infty_vector_fourierIntegral: reformulations explicitly using the Fourier integral.
theorem fourier_integrand_integrable {E : Type u_1} {V : Type u_2} [] {f : VE} [] [] [] [] (w : V) :
MeasureTheory.Integrable fun v => ↑(Real.fourierChar (Multiplicative.ofAdd (-inner v w))) f 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} [] {f : VE} [] [] [] [] {w : V} (hw : w 0) :
∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-inner v w))) f (v + (fun w => (1 / (2 * w ^ 2)) w) w) = -∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-inner v w))) 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} [] {f : VE} [] [] [] [] {w : V} (hw : w 0) (hf : ) :
∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-inner v w))) f v = (1 / 2) ∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-inner v w))) (f v - f (v + (fun w => (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} [] {f : VE} [] [] [] [] (hf1 : ) (hf2 : ) :
Filter.Tendsto (fun w => ∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-inner v w))) 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} [] (f : VE) [] [] [] [] :
Filter.Tendsto (fun w => ∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-inner v w))) 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 → ∞.

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

The Riemann-Lebesgue lemma for functions on ℝ.

theorem Real.zero_at_infty_fourierIntegral {E : Type u_1} [] (f : E) :

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} [] (f : VE) [] [] [] [] (μ : ) :
Filter.Tendsto (fun w => ∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-w v))) f vμ) () (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} [] (f : VE) [] [] [] [] [] [] [] [] (μ : ) :
Filter.Tendsto (fun w => ∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-w v))) f vμ) () (nhds 0)

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

theorem Real.zero_at_infty_vector_fourierIntegral {E : Type u_1} {V : Type u_2} [] (f : VE) [] [] [] [] [] [] [] [] (μ : ) :

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