integral_rexp_neg_mul_sq_norm — Mathlib

English

The Gaussian Fourier transform identities extend to mixed-type theorems relating quadratic forms and linear terms in complex variables, preserving the Gaussian shape after transformation.

Русский

Гауссовы формулы Фурье распространяются на смешанные случаи, сохраняющие гауссову форму после преобразования.

LaTeX

$$$$\\mathcal{F}\\bigl( e^{-x^T B x + c^T x} \\bigr)(t) = \\text{Gaussian}(t; B, c).$$$$

Lean4

theorem integral_rexp_neg_mul_sq_norm {b : ℝ} (hb : 0 < b) :
    ∫ v : V, rexp (-b * ‖v‖ ^ 2) = (π / b) ^ (Module.finrank ℝ V / 2 : ℝ) :=
  by
  rw [← ofReal_inj]
  convert integral_cexp_neg_mul_sq_norm (show 0 < (b : ℂ).re from hb) (V := V)
  · change ofRealLI (∫ (v : V), rexp (-b * ‖v‖ ^ 2)) = ∫ (v : V), cexp (-↑b * ↑‖v‖ ^ 2)
    rw [← ofRealLI.integral_comp_comm]
    simp [ofRealLI]
  · rw [← ofReal_div, ofReal_cpow (by positivity)]
    simp

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