English
Let hb with Re(b) > 0. Then ∫ e^{-b x^2} dx = (π/b)^{1/2}.
Русский
Пусть Re(b) > 0. Тогда ∫ e^{-b x^2} dx = (π/b)^{1/2}.
LaTeX
$$$$\\int_{-\\infty}^{\\infty} e^{-b x^2}\\, dx = (\\pi/b)^{1/2}.$$$$
Lean4
theorem integral_gaussian_complex {b : ℂ} (hb : 0 < re b) : ∫ x : ℝ, cexp (-b * (x : ℂ) ^ 2) = (π / b) ^ (1 / 2 : ℂ) :=
by
have nv : ∀ {b : ℂ}, 0 < re b → b ≠ 0 := by intro b hb; contrapose! hb; rw [hb]; simp
apply
(convex_halfSpace_re_gt 0).isPreconnected.eq_of_sq_eq ?_ ?_ (fun c hc => ?_) (fun {c} hc => ?_)
(by simp : 0 < re (1 : ℂ)) ?_ hb
· -- integral is continuous
exact continuousOn_of_forall_continuousAt continuousAt_gaussian_integral
· -- `(π / b) ^ (1 / 2 : ℂ)` is continuous
refine
continuousOn_of_forall_continuousAt fun b hb =>
(continuousAt_cpow_const (Or.inl ?_)).comp (continuousAt_const.div continuousAt_id (nv hb))
rw [div_re, ofReal_im, ofReal_re, zero_mul, zero_div, add_zero]
exact div_pos (mul_pos pi_pos hb) (normSq_pos.mpr (nv hb))
· -- equality at 1
have : ∀ x : ℝ, cexp (-(1 : ℂ) * (x : ℂ) ^ 2) = exp (-(1 : ℝ) * x ^ 2) :=
by
intro x
simp only [ofReal_exp, neg_mul, one_mul, ofReal_neg, ofReal_pow]
simp_rw [this, ← coe_algebraMap, RCLike.algebraMap_eq_ofReal, integral_ofReal, ← RCLike.algebraMap_eq_ofReal,
coe_algebraMap]
conv_rhs =>
congr
· rw [← ofReal_one, ← ofReal_div]
· rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div]
rw [← ofReal_cpow, ofReal_inj]
· convert integral_gaussian (1 : ℝ) using 1
rw [sqrt_eq_rpow]
· rw [div_one]; exact pi_pos.le
· -- squares of both sides agree
dsimp only [Pi.pow_apply]
rw [integral_gaussian_sq_complex hc, sq]
conv_lhs => rw [← cpow_one (↑π / c)]
rw [← cpow_add _ _ (div_ne_zero (ofReal_ne_zero.mpr pi_ne_zero) (nv hc))]
norm_num
· -- RHS doesn't vanish
rw [Ne, cpow_eq_zero_iff, not_and_or]
exact
Or.inl
(div_ne_zero (ofReal_ne_zero.mpr pi_ne_zero) (nv hc))
-- The Gaussian integral on the half-line, `∫ x in Ioi 0, exp (-b * x^2)`, for complex `b`.
