lintegral_exponentialPDF_eq_one — Mathlib

English

The integral of the exponential pdf over all real numbers equals 1 for hr>0.

Русский

Интеграл экспоненциальной плотности по всей ℝ равен 1 при hr>0.

LaTeX

$$$ (hr>0) \Rightarrow \int_{-\infty}^{\infty} \text{exponentialPDF}(r, x) \, dx = 1 $$$

Lean4

/-- The pdf of the exponential distribution integrates to 1 -/
@[simp]
theorem lintegral_exponentialPDF_eq_one {r : ℝ} (hr : 0 < r) : ∫⁻ x, exponentialPDF r x = 1 :=
  lintegral_gammaPDF_eq_one zero_lt_one hr

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