English
For hb with Re(b) > 0, the half-line integral equals (π/b)^{1/2} / 2.
Русский
Пусть Re(b) > 0. Тогда частичный интеграл по положительной полувинге равен (π/b)^{1/2} / 2.
LaTeX
$$$$\\int_{0}^{\\infty} e^{-b x^2}\\, dx = \\frac{1}{2}\\,(\\pi/b)^{1/2}.$$$$
Lean4
theorem integral_gaussian_complex_Ioi {b : ℂ} (hb : 0 < re b) :
∫ x : ℝ in Ioi 0, cexp (-b * (x : ℂ) ^ 2) = (π / b) ^ (1 / 2 : ℂ) / 2 :=
by
have full_integral := integral_gaussian_complex hb
have : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi
rw [← integral_add_compl this (integrable_cexp_neg_mul_sq hb), compl_Ioi] at full_integral
suffices ∫ x : ℝ in Iic 0, cexp (-b * (x : ℂ) ^ 2) = ∫ x : ℝ in Ioi 0, cexp (-b * (x : ℂ) ^ 2)
by
rw [this, ← mul_two] at full_integral
rwa [eq_div_iff]; exact two_ne_zero
have : ∀ c : ℝ, ∫ x in (0 : ℝ)..c, cexp (-b * (x : ℂ) ^ 2) = ∫ x in -c..0, cexp (-b * (x : ℂ) ^ 2) :=
by
intro c
have := intervalIntegral.integral_comp_sub_left (a := 0) (b := c) (fun x => cexp (-b * (x : ℂ) ^ 2)) 0
simpa [zero_sub, neg_sq, neg_zero] using this
have t1 := intervalIntegral_tendsto_integral_Ioi 0 (integrable_cexp_neg_mul_sq hb).integrableOn tendsto_id
have t2 :
Tendsto (fun c : ℝ => ∫ x : ℝ in (0 : ℝ)..c, cexp (-b * (x : ℂ) ^ 2)) atTop
(𝓝 (∫ x : ℝ in Iic 0, cexp (-b * (x : ℂ) ^ 2))) :=
by
simp_rw [this]
refine intervalIntegral_tendsto_integral_Iic _ ?_ tendsto_neg_atTop_atBot
apply (integrable_cexp_neg_mul_sq hb).integrableOn
exact tendsto_nhds_unique t2 t1
