fourierIntegral_gaussian_innerProductSpace

English

A variant of the Gaussian Fourier transform formula in an abstract inner product space expresses the Fourier transform of a Gaussian in terms of the inner product and the norm in the space.

Русский

Вариант формулы гауссова преобразования Фурье в абстрактном пространстве с скалярным произведением выражает преобразование гауссиана через скалярное произведение и норму.

LaTeX

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

Lean4

theorem _root_.fourierIntegral_gaussian_innerProductSpace (hb : 0 < b.re) (w : V) :
    𝓕 (fun v ↦ cexp (-b * ‖v‖ ^ 2)) w = (π / b) ^ (Module.finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * ‖w‖ ^ 2 / b) := by
  simpa using fourierIntegral_gaussian_innerProductSpace' hb 0 w

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