English
For hb with Re(b) > 0, the square of the Gaussian integral is π/b.
Русский
Пусть Re(b) > 0. Квадрат гауссиана: (∫ e^{-b x^2} dx)^2 = π/b.
LaTeX
$$$$\\left(\\int_{-\\infty}^{\\infty} e^{-b x^2}\\, dx\\right)^2 = \\frac{\\pi}{b}.$$$$
Lean4
/-- The *square* of the Gaussian integral `∫ x:ℝ, exp (-b * x^2)` is equal to `π / b`. -/
theorem integral_gaussian_sq_complex {b : ℂ} (hb : 0 < b.re) : (∫ x : ℝ, cexp (-b * (x : ℂ) ^ 2)) ^ 2 = π / b := by
/- We compute `(∫ exp (-b x^2))^2` as an integral over `ℝ^2`, and then make a polar change
of coordinates. We are left with `∫ r * exp (-b r^2)`, which has been computed in
`integral_mul_cexp_neg_mul_sq` using the fact that this function has an obvious primitive. -/
calc
(∫ x : ℝ, cexp (-b * (x : ℂ) ^ 2)) ^ 2 = ∫ p : ℝ × ℝ, cexp (-b * (p.1 : ℂ) ^ 2) * cexp (-b * (p.2 : ℂ) ^ 2) := by
rw [pow_two, ← integral_prod_mul]; rfl
_ = ∫ p : ℝ × ℝ, cexp (-b * ((p.1 : ℂ) ^ 2 + (p.2 : ℂ) ^ 2)) :=
by
congr
ext1 p
rw [← Complex.exp_add, mul_add]
_ = ∫ p in polarCoord.target, p.1 • cexp (-b * ((p.1 * Complex.cos p.2) ^ 2 + (p.1 * Complex.sin p.2) ^ 2)) :=
by
rw [← integral_comp_polarCoord_symm]
simp only [polarCoord_symm_apply, ofReal_mul, ofReal_cos, ofReal_sin]
_ = (∫ r in Ioi (0 : ℝ), r * cexp (-b * (r : ℂ) ^ 2)) * ∫ θ in Ioo (-π) π, 1 :=
by
rw [← setIntegral_prod_mul]
congr with p : 1
rw [mul_one]
congr
conv_rhs => rw [← one_mul ((p.1 : ℂ) ^ 2), ← sin_sq_add_cos_sq (p.2 : ℂ)]
ring
_ = ↑π / b :=
by
simp only [integral_const, MeasurableSet.univ, measureReal_restrict_apply, univ_inter, real_smul, mul_one,
integral_mul_cexp_neg_mul_sq hb]
rw [volume_real_Ioo_of_le (by linarith [pi_nonneg])]
simp
ring
