fourier_inversion_inv — Mathlib

English

Inverse Fourier inversion statement: 𝓕⁻(𝓕 f) recovers f at continuity points, under mild integrability hypotheses.

Русский

Утверждение инверсии: 𝓕⁻(𝓕 f) восстанавливает f в точках непрерывности при умеренных допущениях интегрируемости.

LaTeX

$$$$ 𝓕^{-}(𝓕 f)(v) = f(v) \quad \text{for } v \text{ where } f \text{ is continuous} $$$$

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

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