fourierIntegral_gaussian_pi — Mathlib

English

Let hb be a complex number with Re(b) > 0. Then the Fourier transform of the Gaussian x ↦ exp(-π b x^2) is exp(-π/b t^2) scaled by b^{-1/2}: F[x ↦ e^{-π b x^2}](t) = b^{-1/2} e^{-π/b t^2}.

Русский

Пусть hb — комплексное число с Re(b) > 0. Тогда преобразование Фурье гауссиана x ↦ e^{-π b x^2} задаёт F[x ↦ e^{-π b x^2}](t) = b^{-1/2} e^{-π/b t^2}.

LaTeX

$$$$\\mathcal{F}\\left( x \\mapsto e^{-\\\\pi b x^2} \\right)(t) = \\frac{1}{b^{1/2}} \\, e^{-\\\\pi/b \\, t^2}, \\quad \\Re(b) > 0.$$$$

Lean4

theorem _root_.fourierIntegral_gaussian_pi (hb : 0 < b.re) :
    (𝓕 fun (x : ℝ) ↦ cexp (-π * b * x ^ 2)) = fun t : ℝ ↦ 1 / b ^ (1 / 2 : ℂ) * cexp (-π / b * t ^ 2) := by
  simpa only [mul_zero, zero_mul, add_zero] using fourierIntegral_gaussian_pi' hb 0

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