English
For a fixed b with Re(b) > 0, the integral of exp(-b ||v||^2) over the relevant space equals (π/b)^{dim/2}. This is the special case c = 0 of the Gaussian integral formula.
Русский
При Re(b) > 0 интеграл exp(-b ||v||^2) по пространству равен (π/b)^{dim/2}. Это частный случай формулы гауссового интеграла при c = 0.
LaTeX
$$$$\\\\int_V e^{-b \\\\|v\\|^2} \\, dv = (\\\\pi/b)^{\\\\dim(V)/2}. $$$$
Lean4
theorem integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace {ι : Type*} [Fintype ι] (hb : 0 < b.re) (c : ℂ)
(w : EuclideanSpace ℝ ι) :
∫ v : EuclideanSpace ℝ ι, cexp (-b * ‖v‖ ^ 2 + c * ⟪w, v⟫) =
(π / b) ^ (Fintype.card ι / 2 : ℂ) * cexp (c ^ 2 * ‖w‖ ^ 2 / (4 * b)) :=
by
have := (EuclideanSpace.volume_preserving_measurableEquiv ι).symm
rw [← this.integral_comp (MeasurableEquiv.measurableEmbedding _)]
simp only [neg_mul]
convert integral_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 5 with _x y
· simp only [EuclideanSpace.coe_measurableEquiv_symm, EuclideanSpace.norm_eq, PiLp.toLp_apply, Real.norm_eq_abs,
sq_abs, neg_mul, neg_inj, mul_eq_mul_left_iff]
norm_cast
left
rw [sq_sqrt]
exact Finset.sum_nonneg (fun i _hi ↦ by positivity)
· simp [PiLp.inner_apply, EuclideanSpace.measurableEquiv, Finset.mul_sum, mul_assoc]
simp_rw [mul_comm]
· simp only [EuclideanSpace.norm_eq, Real.norm_eq_abs, sq_abs, mul_pow, ← Finset.mul_sum]
congr
norm_cast
rw [sq_sqrt]
exact Finset.sum_nonneg (fun i _hi ↦ by positivity)
