English
Let ι be finite, b : ι → C with Re(b_i) > 0, and c : ι → C. Then the function v ↦ exp(-∑ b_i v_i^2 + ∑ c_i v_i) is integrable over ℝ^{ι} with respect to the product Lebesgue measure.
Русский
Пусть ι — конечное множество, b_i ∈ C так, что Re(b_i) > 0, и c_i ∈ C. Тогда функция v \mapsto exp(-∑ b_i v_i^2 + ∑ c_i v_i) интегрируема по мере произведения на ℝ^{ι}.
LaTeX
$$$$\\int_{\\\\mathbb{R}^{\\\\lvert ι\\\\rvert}} \\exp\\left(-\\\\sum_{i} b_i v_i^2 + \\sum_{i} c_i v_i\\right) \\, dv = \\prod_{i} \\left(\\\\frac{\\\\pi}{b_i}\\\\right)^{1/2} \\, \\exp\\left( \\frac{c_i^2}{4 b_i}\\\\right).$$$$
Lean4
theorem integrable_cexp_neg_sum_mul_add {ι : Type*} [Fintype ι] {b : ι → ℂ} (hb : ∀ i, 0 < (b i).re) (c : ι → ℂ) :
Integrable (fun (v : ι → ℝ) ↦ cexp (-∑ i, b i * (v i : ℂ) ^ 2 + ∑ i, c i * v i)) :=
by
simp_rw [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, Complex.exp_sum, ← neg_mul]
apply Integrable.fintype_prod (f := fun i (v : ℝ) ↦ cexp (-b i * v ^ 2 + c i * v)) (fun i ↦ ?_)
convert integrable_cexp_quadratic (hb i) (c i) 0 using 3 with x
simp only [add_zero]
