English
For ι finite, the integral of exp(-∑ b_i (v_i)^2 + ∑ c_i v_i) over ℝ^{ι} equals the product over i of Gaussian factors.
Русский
Для конечного множества индексов ι интеграл exp(-∑ b_i v_i^2 + ∑ c_i v_i) по ℝ^{ι} равен произведению гауссовых множителей по i.
LaTeX
$$$$\\int_{\\\\mathbb{R}^{\\\\lvert ι\\\\rvert}} e^{-\\\\sum_i b_i v_i^2 + \\\\sum_i c_i v_i} \\, dv = \\\\prod_i (\\\\frac{\\\\pi}{b_i})^{1/2} e^{c_i^2/(4 b_i)}.$$$$
Lean4
theorem integral_cexp_neg_sum_mul_add {ι : Type*} [Fintype ι] {b : ι → ℂ} (hb : ∀ i, 0 < (b i).re) (c : ι → ℂ) :
∫ v : ι → ℝ, cexp (-∑ i, b i * (v i : ℂ) ^ 2 + ∑ i, c i * v i) =
∏ i, (π / b i) ^ (1 / 2 : ℂ) * cexp (c i ^ 2 / (4 * b i)) :=
by
simp_rw [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, Complex.exp_sum, ← neg_mul]
rw [integral_fintype_prod_volume_eq_prod (f := fun i (v : ℝ) ↦ cexp (-b i * v ^ 2 + c i * v))]
congr with i
have : (-b i).re < 0 := by simpa using hb i
convert integral_cexp_quadratic this (c i) 0 using 1 <;> simp [div_neg]
