integral_cexp_neg_mul_sq_norm_add

English

The integral of exp(-Σ b_i (v_i)^2 + Σ c_i v_i) over a finite product space evaluates to a product of one-dimensional Gaussian contributions.

Русский

Интеграл exp(-∑ b_i v_i^2 + ∑ c_i v_i) над произведением пространств равен произведению одномерных гауссовых вкладов.

LaTeX

$$$$\\int_{\\\\mathbb{R}^{ι}} 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_mul_sq_norm_add (hb : 0 < b.re) (c : ℂ) (w : V) :
    ∫ v : V, cexp (-b * ‖v‖ ^ 2 + c * ⟪w, v⟫) =
      (π / b) ^ (Module.finrank ℝ V / 2 : ℂ) * cexp (c ^ 2 * ‖w‖ ^ 2 / (4 * b)) :=
  by
  let e := (stdOrthonormalBasis ℝ V).repr.symm
  rw [← e.measurePreserving.integral_comp e.toHomeomorph.measurableEmbedding]
  convert integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace hb c (e.symm w) <;>
    simp [LinearIsometryEquiv.inner_map_eq_flip]

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