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 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} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : V → E} [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (w : V) : MeasureTheory.Integrable f ↔ MeasureTheory.Integrable fun (v : V) => ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪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} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : V → E} [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {w : V} (hw : w ≠ 0) : ∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪v, w⟫_ℝ))) • f (v + (fun (w : V) => (1 / (2 * ‖w‖ ^ 2)) • w) w) = -∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪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} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : V → E} [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {w : V} (hw : w ≠ 0) (hf : MeasureTheory.Integrable f) : ∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪v, w⟫_ℝ))) • f v = (1 / 2) • ∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪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.

theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : V → E} [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (hf1 : Continuous f) (hf2 : HasCompactSupport f) : Filter.Tendsto (fun (w : V) => ∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪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.

theorem tendsto_integral_exp_inner_smul_cocompact {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : V → E) [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] : Filter.Tendsto (fun (w : V) => ∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪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 (Multiplicative.ofAdd (-(v * w)))) • f v) (Filter.cocompact ℝ) (nhds 0)

The Riemann-Lebesgue lemma for functions on ℝ.

theorem Real.zero_at_infty_fourierIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) : Filter.Tendsto (Real.fourierIntegral f) (Filter.cocompact ℝ) (nhds 0)

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 : V → E) [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (μ : MeasureTheory.Measure V) [MeasureTheory.Measure.IsAddHaarMeasure μ] : Filter.Tendsto (fun (w : V →L[ℝ] ℝ) => ∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-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 : V → E) [AddCommGroup V] [TopologicalSpace V] [TopologicalAddGroup V] [T2Space V] [MeasurableSpace V] [BorelSpace V] [Module ℝ V] [ContinuousSMul ℝ V] [FiniteDimensional ℝ V] (μ : MeasureTheory.Measure V) [MeasureTheory.Measure.IsAddHaarMeasure μ] : Filter.Tendsto (fun (w : V →L[ℝ] ℝ) => ∫ (v : V), ↑(Real.fourierChar (Multiplicative.ofAdd (-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.

theorem Real.zero_at_infty_vector_fourierIntegral {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : V → E) [AddCommGroup V] [TopologicalSpace V] [TopologicalAddGroup V] [T2Space V] [MeasurableSpace V] [BorelSpace V] [Module ℝ V] [ContinuousSMul ℝ V] [FiniteDimensional ℝ V] (μ : MeasureTheory.Measure V) [MeasureTheory.Measure.IsAddHaarMeasure μ] : Filter.Tendsto (VectorFourier.fourierIntegral Real.fourierChar μ (LinearMap.flip (topDualPairing ℝ V)) f) (Filter.cocompact (V →L[ℝ] ℝ)) (nhds 0)

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