integrable_cexp_neg_mul_sum_add — Mathlib

English

For a finite index set ι and b_i ∈ C with Re(b_i) > 0, the integrability of exp(-∑ b_i (v_i)^2 + ∑ c_i v_i) factorizes into the product of one-variable integrals, giving the same Gaussian form as in the previous statement.

Русский

Для конечного множества индексов ι интегропликативная функция 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_mul_sum_add {ι : Type*} [Fintype ι] (hb : 0 < b.re) (c : ι → ℂ) :
    Integrable (fun (v : ι → ℝ) ↦ cexp (-b * ∑ i, (v i : ℂ) ^ 2 + ∑ i, c i * v i)) :=
  by
  simp_rw [neg_mul, Finset.mul_sum]
  exact integrable_cexp_neg_sum_mul_add (fun _ ↦ hb) c

Похожие утверждения