fourierIntegral_gaussian — Mathlib

English

The Fourier transform of a Gaussian e^{−b x^2} is another Gaussian: ∫ e^{i t x} e^{−b x^2} dx = (π/b)^{1/2} e^{−t^2/(4 b)}.

Русский

Преобразование Фурье Гамма-подобной функции: ∫ e^{i t x} e^{−b x^2} dx = (π/b)^{1/2} e^{−t^2/(4 b)}.

LaTeX

$$$$ \int_{-\infty}^{\infty} e^{i t x} e^{-b x^{2}} \, dx = \left( \frac{\pi}{b} \right)^{1/2} e^{-t^{2}/(4 b)}. $$$$

Lean4

theorem _root_.fourierIntegral_gaussian (hb : 0 < b.re) (t : ℂ) :
    ∫ x : ℝ, cexp (I * t * x) * cexp (-b * x ^ 2) = (π / b) ^ (1 / 2 : ℂ) * cexp (-t ^ 2 / (4 * b)) :=
  by
  conv => enter [1, 2, x]; rw [← Complex.exp_add, add_comm, ← add_zero (-b * x ^ 2 + I * t * x)]
  rw [integral_cexp_quadratic (show (-b).re < 0 by rwa [neg_re, neg_lt_zero]), neg_neg, zero_sub, mul_neg, div_neg,
    neg_neg, mul_pow, I_sq, neg_one_mul, mul_comm]

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