English
For finite ι and b_i with Re(b_i) > 0, the integral of exp(- ∑ b_i (v_i)^2 + ∑ c_i v_i) over ℝ^{ι} equals the product over i of one-variable Gaussian integrals.
Русский
Для конечного индекса ι интеграл 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 integrableOn_rpow_mul_exp_neg_rpow {p s : ℝ} (hs : -1 < s) (hp : 1 ≤ p) :
IntegrableOn (fun x : ℝ => x ^ s * exp (-x ^ p)) (Ioi 0) :=
by
obtain hp | hp := le_iff_lt_or_eq.mp hp
· have h_exp : ∀ x, ContinuousAt (fun x => exp (-x)) x := fun x => continuousAt_neg.rexp
rw [← Ioc_union_Ioi_eq_Ioi zero_le_one, integrableOn_union]
constructor
· rw [← integrableOn_Icc_iff_integrableOn_Ioc]
refine IntegrableOn.mul_continuousOn ?_ ?_ isCompact_Icc
· refine (intervalIntegrable_iff_integrableOn_Icc_of_le zero_le_one).mp ?_
exact intervalIntegral.intervalIntegrable_rpow' hs
· intro x _
change ContinuousWithinAt ((fun x => exp (-x)) ∘ (fun x => x ^ p)) (Icc 0 1) x
refine ContinuousAt.comp_continuousWithinAt (h_exp _) ?_
exact continuousWithinAt_id.rpow_const (Or.inr (le_of_lt (lt_trans zero_lt_one hp)))
· have h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x :=
by
intro _ _ hx
refine continuousWithinAt_id.rpow_const (Or.inl ?_)
exact ne_of_gt (lt_of_lt_of_le zero_lt_one hx)
refine
integrable_of_isBigO_exp_neg (by simp : (0 : ℝ) < 1 / 2)
(ContinuousOn.mul (fun x hx => h_rpow x s hx) (fun x hx => ?_)) (IsLittleO.isBigO ?_)
· change ContinuousWithinAt ((fun x => exp (-x)) ∘ (fun x => x ^ p)) (Ici 1) x
exact ContinuousAt.comp_continuousWithinAt (h_exp _) (h_rpow x p hx)
· convert rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg s hp (by simp : (0 : ℝ) < 1) using 3
rw [neg_mul, one_mul]
· simp_rw [← hp, Real.rpow_one]
convert Real.GammaIntegral_convergent (by linarith : 0 < s + 1) using 2
rw [add_sub_cancel_right, mul_comm]
