integrable_cexp_quadratic — Mathlib

English

The Gaussian-type integrable function with quadratic exponent is integrable for hb>0 after transformation.

Русский

Гауссово-интегрируемая функция с квадратичным показателем интегрируема при hb>0 после преобразования.

LaTeX

$$$$ \int_{-\infty}^{\infty} e^{b x^2 + c x + d} dx < \infty \quad (\Re(b) < 0). $$$$

Lean4

theorem _root_.integrable_cexp_quadratic (hb : 0 < b.re) (c d : ℂ) :
    Integrable (fun (x : ℝ) ↦ cexp (-b * x ^ 2 + c * x + d)) :=
  by
  have : (-b).re < 0 := by simpa using hb
  exact integrable_cexp_quadratic' this c d

Похожие утверждения