English
Let b ∈ C with Re(b) > 0 and x,w ∈ V. Then the Fourier transform of the Gaussian e^{-b||v||^2 + 2π i ⟪x,v⟫} evaluated at w equals (π/b)^{dim/2} e^{-π^2 ||x-w||^2 / b}. This extends the scalar case to inner-product spaces.
Русский
Пусть b ∈ C, Re(b) > 0, и x,w ∈ V. Ещё один формула Фурье для гауссиана с линейным членом: F[ e^{-b||v||^2 + 2π i ⟪x,v⟫} ](w) = (π/b)^{dim/2} e^{-π^2 ||x-w||^2 / b}.
LaTeX
$$$$\\mathcal{F}\\left(v \\mapsto e^{-b \\|v\\|^2 + 2π i ⟪x,v⟫}\\right)(w) = (\\\\pi/b)^{\\\\dim(V)/2} e^{-π^2 \\|x-w\\|^2 / b}.$$$$
Lean4
theorem _root_.fourierIntegral_gaussian_innerProductSpace' (hb : 0 < b.re) (x w : V) :
𝓕 (fun v ↦ cexp (-b * ‖v‖ ^ 2 + 2 * π * Complex.I * ⟪x, v⟫)) w =
(π / b) ^ (Module.finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * ‖x - w‖ ^ 2 / b) :=
by
simp only [neg_mul, fourierIntegral_eq', ofReal_neg, ofReal_mul, ofReal_ofNat, smul_eq_mul, ← Complex.exp_add,
real_inner_comm w]
convert integral_cexp_neg_mul_sq_norm_add hb (2 * π * Complex.I) (x - w) using 3 with v
· congr 1
simp [inner_sub_left]
ring
· have : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
simp [mul_pow]
ring
