English
For a real vector space V with inner product and finite dimension, the integral of exp(-b ||v||^2 + c ⟪w, v⟫) over V is finite when Re(b) > 0, and equals a Gaussian expression depending on w and b.
Русский
Для вещественного векторного пространства V с скалярным произведением и конечной размерностью интеграл exp(-b ||v||^2 + c ⟪w, v⟫) по V существует при Re(b) > 0 и равен гауссовой формуле.
LaTeX
$$$$\\int_{V} e^{-b \\|v\\|^2 + c \\langle w, v \\rangle} \\, dv = (\\\\pi / b)^{\\\\text{dim}(V)/2} \\, e^{c^2 ||w||^2/(4 b)}.$$$$
Lean4
/-- In a real inner product space, the complex exponential of minus the square of the norm plus
a scalar product is integrable. Useful when discussing the Fourier transform of a Gaussian. -/
theorem integrable_cexp_neg_mul_sq_norm_add (hb : 0 < b.re) (c : ℂ) (w : V) :
Integrable (fun (v : V) ↦ cexp (-b * ‖v‖ ^ 2 + c * ⟪w, v⟫)) :=
by
let e := (stdOrthonormalBasis ℝ V).repr.symm
rw [← e.measurePreserving.integrable_comp_emb e.toHomeomorph.measurableEmbedding]
convert integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace hb c (e.symm w) with v
simp only [neg_mul, Function.comp_apply, LinearIsometryEquiv.norm_map, LinearIsometryEquiv.symm_symm,
LinearIsometryEquiv.inner_map_eq_flip]
