The Riemann-Lebesgue Lemma #
In this file we prove the Riemann-Lebesgue lemma, for functions on finite-dimensional real vector
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 #
Va finite-dimensional real inner product space and
f : V → E, the function
λ w : V, ∫ v : V, exp (2 * π * ⟪w, v⟫ * I) • f vtends to 0 along
Va finite-dimensional real vector space (endowed with its unique Hausdorff topological vector space structure), and
Wthe dual of
V, the function
λ w : W, ∫ v : V, exp (2 * π * w v * I) • f vtends to along
Real.tendsto_integral_exp_smul_cocompact: special case of functions on
Real.zero_at_infty_vector_fourierIntegral: reformulations explicitly using the Fourier integral.
The integrand in the Riemann-Lebesgue lemma for
f is integrable iff
(1 / (2 * ‖w‖ ^ 2)) • w negates the integral in the Riemann-Lebesgue lemma.
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.
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 → ∞.
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.
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
its dual space).