exponentialPDF_of_nonneg — Mathlib

English

If x ≥ 0, then exponentialPDF(r, x) = ENNReal.ofReal(r * rexp(- r * x)).

Русский

Если x ≥ 0, то экспоненциальная плотность равна ENNReal.ofReal(r · e^{- r x}).

LaTeX

$$$ x \ge 0 \Rightarrow \text{exponentialPDF}(r, x) = \mathrm{ENNReal.ofReal}( r \cdot \mathrm{rexp}(- r x) ) $$$

Lean4

theorem exponentialPDF_of_nonneg {r x : ℝ} (hx : 0 ≤ x) : exponentialPDF r x = ENNReal.ofReal (r * rexp (-(r * x))) :=
  by simp only [exponentialPDF_eq, if_pos hx]

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