English
For complex b with Re(b) > 0, the half-line integral equals (2 b)^{-1}.
Русский
Для комплексного b с Re(b) > 0 выполнено: ∫_0^∞ r e^{-b r^2} dr = (2b)^{-1}.
LaTeX
$$$$\\int_{0}^{\\infty} r\\, e^{-b r^2}\\, dr = \\frac{1}{2b}.$$$
Lean4
theorem integral_mul_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) :
∫ r : ℝ in Ioi 0, (r : ℂ) * cexp (-b * (r : ℂ) ^ 2) = (2 * b)⁻¹ :=
by
have hb' : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
have A : ∀ x : ℂ, HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x :=
by
intro x
convert ((hasDerivAt_pow 2 x).const_mul (-b)).cexp.const_mul (-(2 * b)⁻¹) using 1
field_simp
ring
have B : Tendsto (fun y : ℝ ↦ -(2 * b)⁻¹ * cexp (-b * (y : ℂ) ^ 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0)) :=
by
refine Tendsto.const_mul _ (tendsto_zero_iff_norm_tendsto_zero.mpr ?_)
simp_rw [norm_cexp_neg_mul_sq b]
exact tendsto_exp_atBot.comp ((tendsto_pow_atTop two_ne_zero).const_mul_atTop_of_neg (neg_lt_zero.2 hb))
convert
integral_Ioi_of_hasDerivAt_of_tendsto' (fun x _ => (A ↑x).comp_ofReal)
(integrable_mul_cexp_neg_mul_sq hb).integrableOn B using
1
simp only [mul_zero, ofReal_zero, zero_pow, Ne, not_false_iff, Complex.exp_zero, mul_one, sub_neg_eq_add, zero_add,
reduceCtorEq]
