integral_cexp_neg_mul_sq_norm — Mathlib

English

For a finite-dimensional Euclidean space, the Fourier transform of the pure Gaussian e^{-b ||v||^2} is again a Gaussian with parameter b, up to the standard normalization involving the dimension.

Русский

Для конечномерного евклидова пространства преобразование Фурье гауссиана e^{-b ||v||^2} даёт гауссиан с тем же параметром b (с учётом нормализации по размерности).

LaTeX

$$$$\\mathcal{F}(v \\mapsto e^{-b \\|v\\|^2})(t) = (\\\\pi/b)^{\\\\dim/2} e^{-\\\\pi^2 \\|t\\|^2 / b}.$$$$

Lean4

theorem integral_cexp_neg_mul_sq_norm (hb : 0 < b.re) :
    ∫ v : V, cexp (-b * ‖v‖ ^ 2) = (π / b) ^ (Module.finrank ℝ V / 2 : ℂ) := by
  simpa using integral_cexp_neg_mul_sq_norm_add hb 0 (0 : V)

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