English
For Re(b)<0, the integral of e^{b x^2 + c x + d} over R has a closed form: (π/−b)^{1/2} e^{d − c^2/(4 b)}.
Русский
При Re(b)<0 интеграл e^{b x^2 + c x + d} по R имеет closed form: (π/−b)^{1/2} e^{d − c^2/(4 b)}.
LaTeX
$$$$ \int_{-\infty}^{\infty} e^{b x^2 + c x + d} dx = \left( \frac{\pi}{-b} \right)^{1/2} e^{d - \frac{c^2}{4 b}}. $$$$
Lean4
theorem _root_.integral_cexp_quadratic (hb : b.re < 0) (c d : ℂ) :
∫ x : ℝ, cexp (b * x ^ 2 + c * x + d) = (π / -b) ^ (1 / 2 : ℂ) * cexp (d - c ^ 2 / (4 * b)) :=
by
have hb' : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
have h (x : ℝ) : cexp (b * x ^ 2 + c * x + d) = cexp (- -b * (x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b)) :=
by
simp_rw [← Complex.exp_add]
congr 1
field_simp
ring_nf
simp_rw [h, MeasureTheory.integral_mul_const]
rw [← re_add_im (c / (2 * b))]
simp_rw [← add_assoc, ← ofReal_add]
rw [integral_add_right_eq_self fun a : ℝ ↦ cexp (- -b * (↑a + ↑(c / (2 * b)).im * I) ^ 2),
integral_cexp_neg_mul_sq_add_real_mul_I ((neg_re b).symm ▸ (neg_pos.mpr hb))]
