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) ^ (↑(FiniteDimensional.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) ^ (↑(FiniteDimensional.finrank ℝ V) / 2) * Complex.exp (-↑Real.pi ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w) Filter.atTop (nhds (f v))

theorem MeasureTheory.Integrable.fourier_inversion {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} (hv : ContinuousAt f v) : Real.fourierIntegralInv (Real.fourierIntegral f) v = 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.

theorem Continuous.fourier_inversion {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] (h : Continuous f) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (h'f : MeasureTheory.Integrable (Real.fourierIntegral f) MeasureTheory.volume) : Real.fourierIntegralInv (Real.fourierIntegral f) = 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.

theorem MeasureTheory.Integrable.fourier_inversion_inv {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} (hv : ContinuousAt f v) : Real.fourierIntegral (Real.fourierIntegralInv f) v = 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.

theorem Continuous.fourier_inversion_inv {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] (h : Continuous f) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (h'f : MeasureTheory.Integrable (Real.fourierIntegral f) MeasureTheory.volume) : Real.fourierIntegral (Real.fourierIntegralInv f) = 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.