Theorems · Theorem · harmonic analysis

MeasureTheory.Integrable.fourierInv_fourier_eq

• 1000+ list: Fourier theorem

∀ {V : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℂ E] {f : V → E} [CompleteSpace E],
  MeasureTheory.Integrable f MeasureTheory.volume →
    MeasureTheory.Integrable (FourierTransform.fourier f) MeasureTheory.volume →
      ∀ {v : V}, ContinuousAt f v → FourierTransformInv.fourierInv (FourierTransform.fourier 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.

Defined in

Mathlib.Analysis.Fourier.Inversion

Cited by

3 results in Mathlib

Foundations

Depth 300 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceFiniteDimensionalNormedAddCommGroupNormedSpaceCompleteSpace