English
Let b ∈ C with Re(b) > 0 and c ∈ C. Then the Fourier transform of the Gaussian x ↦ exp(-π b x^2 + 2π c x) is again Gaussian with parameter b: F[x ↦ exp(-π b x^2 + 2π c x)](t) = b^{-1/2} exp(-π/b (t + i c)^2).
Русский
Пусть b ∈ C с Re(b) > 0 и c ∈ C. Тогда преобразование Фурье функции x ↦ exp(-π b x^2 + 2π c x) снова даёт гауссиан с параметром b: F[x ↦ exp(-π b x^2 + 2π c x)](t) = b^{-1/2} exp(-π/b (t + i c)^2).
LaTeX
$$$\\\\mathcal{F}\\left( x \\mapsto e^{-\\\\pi b x^2 + 2\\\\pi c x} \\right)(t) = \\frac{1}{b^{1/2}} \\, e^{-\\\\pi/b \\, (t + i c)^2}, \\\\quad \\text{for } \\Re(b) > 0, c \\in \\mathbb{C}, t \\in \\mathbb{R}.$$$
Lean4
theorem _root_.fourierIntegral_gaussian_pi' (hb : 0 < b.re) (c : ℂ) :
(𝓕 fun x : ℝ => cexp (-π * b * x ^ 2 + 2 * π * c * x)) = fun t : ℝ =>
1 / b ^ (1 / 2 : ℂ) * cexp (-π / b * (t + I * c) ^ 2) :=
by
haveI : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
have h : (-↑π * b).re < 0 := by simpa only [neg_mul, neg_re, re_ofReal_mul, neg_lt_zero] using mul_pos pi_pos hb
ext1 t
simp_rw [fourierIntegral_real_eq_integral_exp_smul, smul_eq_mul, ← Complex.exp_add, ← add_assoc]
have (x : ℝ) :
↑(-2 * π * x * t) * I + -π * b * x ^ 2 + 2 * π * c * x = -π * b * x ^ 2 + (-2 * π * I * t + 2 * π * c) * x + 0 := by
push_cast; ring
simp_rw [this, integral_cexp_quadratic h, neg_mul, neg_neg]
congr 2
· rw [← div_div, div_self <| ofReal_ne_zero.mpr pi_ne_zero, one_div, inv_cpow, ← one_div]
rw [Ne, arg_eq_pi_iff, not_and_or, not_lt]
exact Or.inl hb.le
· field_simp
ring_nf
simp only [I_sq]
ring
