fourier_inversion_inv — Mathlib

English

A version of the inversion formula showing convergence of Gaussian-smoothed transforms to f at points of continuity.

Русский

Версия формулы инверсии с гауссовым сглаживанием, сходящаяся к f в точках непрерывности.

LaTeX

$$$$ \mathcal{F}^{-1} (\mathcal{F} 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 integrable, and its Fourier transform `𝓕 f` is also integrable, then `𝓕 (𝓕⁻ f) = f` at
continuity points of `f`. -/
theorem fourier_inversion_inv (hf : Integrable f) (h'f : Integrable (𝓕 f)) {v : V} (hv : ContinuousAt f v) :
    𝓕 (𝓕⁻ f) v = f v := by
  rw [fourierIntegralInv_comm]
  exact fourier_inversion hf h'f hv

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