fourier_inversion — Mathlib

English

The inversion formula also holds for the inverse transform 𝓕⁻, recovering f from 𝓕⁻ f when both f and its Fourier transform are integrable.

Русский

Формула инверсии справедлива и для инверса 𝓕⁻ и восстанавливает f из 𝓕⁻ f при условии интегрируемости как f, так и 𝓕 f.

LaTeX

$$$$ \mathcal{F}(\mathcal{F}^{-1} f) = f $$$$

Lean4

/-- **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 fourier_inversion (h : Continuous f) (hf : Integrable f) (h'f : Integrable (𝓕 f)) : 𝓕⁻ (𝓕 f) = f :=
  by
  ext v
  exact hf.fourier_inversion h'f h.continuousAt

Похожие утверждения