English
In Euclidean space with a finite-dimensional index set, the integral of exp(-b ||v||^2 + c ⟪w, v⟫) is finite for Re(b) > 0, and its value is a Gaussian expression involving ||w|| and w.
Русский
В евклидовом пространстве размерность конечна, интеграл exp(-b ||v||^2 + c ⟪w, v⟫) существует при Re(b) > 0 и равен гауссовой формуле, зависящей от ||w||.
LaTeX
$$$$\\int_{\\\\mathbb{R}^{ι}} e^{-b ||v||^2 + c \\langle w, v \\rangle} \\, dv = (\\\\pi/b)^{\\\\lvert ι\\\\rvert/2} \\, e^{c^2 ||w||^2/(4 b)}.$$$$
Lean4
theorem integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace {ι : Type*} [Fintype ι] (hb : 0 < b.re) (c : ℂ)
(w : EuclideanSpace ℝ ι) : Integrable (fun (v : EuclideanSpace ℝ ι) ↦ cexp (-b * ‖v‖ ^ 2 + c * ⟪w, v⟫)) :=
by
have := EuclideanSpace.volume_preserving_measurableEquiv ι
rw [← MeasurePreserving.integrable_comp_emb this.symm (MeasurableEquiv.measurableEmbedding _)]
simp only [neg_mul, Function.comp_def]
convert integrable_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 3 with v
simp only [EuclideanSpace.measurableEquiv, MeasurableEquiv.symm_mk, MeasurableEquiv.coe_mk, EuclideanSpace.norm_eq,
Real.norm_eq_abs, sq_abs, PiLp.inner_apply, RCLike.inner_apply, conj_trivial, ofReal_sum, ofReal_mul,
Finset.mul_sum, neg_mul, Finset.sum_neg_distrib, mul_assoc]
norm_cast
rw [sq_sqrt]
· simp [Finset.mul_sum, mul_comm]
· exact Finset.sum_nonneg (fun i _hi ↦ by positivity)
