integrable_mul_exp_neg_mul_sq — Mathlib

English

Let b > 0. The function f(x) = x e^{-b x^2} is Lebesgue-integrable on the real line.

Русский

Пусть b > 0. Функция f(x) = x e^{-b x^2} интегрируема по мере Лебега на всей прямой.

LaTeX

$$$$\\int_{-\\infty}^{\\infty} |x|\, e^{-b x^2}\\, dx < \\infty.$$$$

Lean4

theorem integrable_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) : Integrable fun x : ℝ => x * exp (-b * x ^ 2) := by
  simpa using integrable_rpow_mul_exp_neg_mul_sq hb (by simp : (-1 : ℝ) < 1)

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