Documentation

Mathlib.Analysis.Fourier.Inversion

Fourier inversion formula #

In a finite-dimensional real inner product space, we show the Fourier inversion formula, i.e., 𝓕⁻ (𝓕 f) v = f v if f and 𝓕 f are integrable, and f is continuous at v. This is proved in MeasureTheory.Integrable.fourier_inversion. See also Continuous.fourier_inversion giving 𝓕⁻ (𝓕 f) = f under an additional continuity assumption for f.

We use the following proof. A naΓ―ve computation gives 𝓕⁻ (𝓕 f) v = ∫_w exp (2 I Ο€ βŸͺw, v⟫) 𝓕 f (w) dw = ∫_w exp (2 I Ο€ βŸͺw, v⟫) ∫_x, exp (-2 I Ο€ βŸͺw, x⟫) f x dx) dw = ∫_x (∫_ w, exp (2 I Ο€ βŸͺw, v - x⟫ dw) f x dx

However, the Fubini step does not make sense for lack of integrability, and the middle integral ∫_ w, exp (2 I Ο€ βŸͺw, v - x⟫ dw (which one would like to be a Dirac at v - x) is not defined. To gain integrability, one multiplies with a Gaussian function exp (-c⁻¹ β€–wβ€–^2), with a large (but finite) c. As this function converges pointwise to 1 when c β†’ ∞, we get ∫_w exp (2 I Ο€ βŸͺw, v⟫) 𝓕 f (w) dw = lim_c ∫_w exp (-c⁻¹ β€–wβ€–^2 + 2 I Ο€ βŸͺw, v⟫) 𝓕 f (w) dw. One can perform Fubini on the right hand side for fixed c, writing the integral as ∫_x (∫_w exp (-c⁻¹‖wβ€–^2 + 2 I Ο€ βŸͺw, v - x⟫ dw)) f x dx. The middle factor is the Fourier transform of a more and more flat function (converging to the constant 1), hence it becomes more and more concentrated, around the point v. (Morally, it converges to the Dirac at v). Moreover, it has integral one. Therefore, multiplying by f and integrating, one gets a term converging to f v as c β†’ ∞. Since it also converges to 𝓕⁻ (𝓕 f) v, this proves the result.

To check the concentration property of the middle factor and the fact that it has integral one, we rely on the explicit computation of the Fourier transform of Gaussians.

theorem Real.tendsto_integral_cexp_sq_smul {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [NormedAddCommGroup E] [NormedSpace β„‚ E] {f : V β†’ E} (hf : MeasureTheory.Integrable f MeasureTheory.volume) :
Filter.Tendsto (fun (c : ℝ) => ∫ (v : V), Complex.exp (-↑c⁻¹ * ↑‖vβ€– ^ 2) β€’ f v) Filter.atTop (nhds (∫ (v : V), f v))
theorem Real.tendsto_integral_gaussian_smul {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [NormedAddCommGroup E] [NormedSpace β„‚ E] {f : V β†’ E} [CompleteSpace E] (hf : MeasureTheory.Integrable f MeasureTheory.volume) (h'f : MeasureTheory.Integrable (Real.fourierIntegral f) MeasureTheory.volume) (v : V) :
Filter.Tendsto (fun (c : ℝ) => ∫ (w : V), ((↑Real.pi * ↑c) ^ (↑(Module.finrank ℝ V) / 2) * Complex.exp (-↑Real.pi ^ 2 * ↑c * ↑‖v - wβ€– ^ 2)) β€’ f w) Filter.atTop (nhds (Real.fourierIntegralInv (Real.fourierIntegral f) v))
theorem Real.tendsto_integral_gaussian_smul' {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [NormedAddCommGroup E] [NormedSpace β„‚ E] {f : V β†’ E} [CompleteSpace E] (hf : MeasureTheory.Integrable f MeasureTheory.volume) {v : V} (h'f : ContinuousAt f v) :
Filter.Tendsto (fun (c : ℝ) => ∫ (w : V), ((↑Real.pi * ↑c) ^ (↑(Module.finrank ℝ V) / 2) * Complex.exp (-↑Real.pi ^ 2 * ↑c * ↑‖v - wβ€– ^ 2)) β€’ f w) Filter.atTop (nhds (f v))

Fourier inversion formula: If a function f on a finite-dimensional real inner product space is integrable, and its Fourier transform 𝓕 f is also integrable, then 𝓕⁻ (𝓕 f) = f at continuity points of f.

Fourier inversion formula: If a function f on a finite-dimensional real inner product space is continuous, integrable, and its Fourier transform 𝓕 f is also integrable, then 𝓕⁻ (𝓕 f) = f.

Fourier inversion formula: If a function f on a finite-dimensional real inner product space is integrable, and its Fourier transform 𝓕 f is also integrable, then 𝓕 (𝓕⁻ f) = f at continuity points of f.

Fourier inversion formula: If a function f on a finite-dimensional real inner product space is continuous, integrable, and its Fourier transform 𝓕 f is also integrable, then 𝓕 (𝓕⁻ f) = f.