English
Let b > 0. Then ∫_{0}^{∞} e^{-b x^2} dx = sqrt(pi/b)/2.
Русский
Пусть b > 0. Тогда ∫_{0}^{∞} e^{-b x^2} dx = \\frac{1}{2} \\sqrt{\\pi/b}.
LaTeX
$$$$\\int_{0}^{\\infty} e^{-b x^2}\\, dx = \\frac{1}{2}\\sqrt{\\pi/b}.$$$$
Lean4
theorem integral_gaussian_Ioi (b : ℝ) : ∫ x in Ioi (0 : ℝ), exp (-b * x ^ 2) = √(π / b) / 2 :=
by
rcases le_or_gt b 0 with (hb | hb)
· rw [integral_undef, sqrt_eq_zero_of_nonpos, zero_div]
· exact div_nonpos_of_nonneg_of_nonpos pi_pos.le hb
· rwa [← IntegrableOn, integrableOn_Ioi_exp_neg_mul_sq_iff, not_lt]
rw [← RCLike.ofReal_inj (K := ℂ), ← integral_ofReal, ← RCLike.algebraMap_eq_ofReal, coe_algebraMap]
convert integral_gaussian_complex_Ioi (by rwa [ofReal_re] : 0 < (b : ℂ).re)
· simp
· rw [sqrt_eq_rpow, ← ofReal_div, ofReal_div, ofReal_cpow]
· simp
· exact (div_pos pi_pos hb).le
