English
If f is integrable and its Fourier transform is integrable, then the Fourier inversion formula restores f from 𝓕 f at points of continuity.
Русский
Если f интегрируема и её Фурье-преобразование интегрируемо, то формула обратного Фурье-преобразования восстанавливает f в точках непрерывности.
LaTeX
$$$$ \mathcal{F}^{-1}(\mathcal{F}f) = f \quad \text{at continuity points of } f $$$$
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 (hf : Integrable f) (h'f : Integrable (𝓕 f)) {v : V} (hv : ContinuousAt f v) :
𝓕⁻ (𝓕 f) v = f v :=
tendsto_nhds_unique (Real.tendsto_integral_gaussian_smul hf h'f v) (Real.tendsto_integral_gaussian_smul' hf hv)
