integrableOn_rpow_mul_exp_neg_mul_sq

English

The real-valued Gaussian exp(-b x^2) is integrable on the real line for b > 0, reflecting the standard Gaussian tail behavior.

Русский

Гауссова функция exp(-b x^2) интегрируема на всей оси при b > 0.

LaTeX

$$$$\\int_{-\\infty}^{\\infty} e^{-b x^2} \\, dx = \\sqrt{\\\\frac{\\\\pi}{b}}.$$$$

Lean4

theorem integrableOn_rpow_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) {s : ℝ} (hs : -1 < s) :
    IntegrableOn (fun x : ℝ => x ^ s * exp (-b * x ^ 2)) (Ioi 0) :=
  by
  simp_rw [← rpow_two]
  exact integrableOn_rpow_mul_exp_neg_mul_rpow hs one_le_two hb

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