43 Abstract harmonic analysis

Fourier inversion theorem

TheoremFourier theorem #

Mathlib records this with 2 declarations.

MeasureTheory.Integrable.fourierInv_fourier_eq: 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.

MeasureTheory.Integrable.fourierInv_fourier_eq.{u_1, u_2} {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 (FourierTransform.fourier f) MeasureTheory.volume) {v : V}
  (hv : ContinuousAt f v) : FourierTransformInv.fourierInv (FourierTransform.fourier f) v = f v

Continuous.fourierInv_fourier_eq: 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.

Continuous.fourierInv_fourier_eq.{u_1, u_2} {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 (FourierTransform.fourier f) MeasureTheory.volume) :
  FourierTransformInv.fourierInv (FourierTransform.fourier f) = f

The wikipedia page is really vague; it's not clear what is meant here. While mathlib has some material already, there is space for more advanced results.