exponentialPDF — Mathlib

English

The exponential pdf is the nonnegative extended real-valued density corresponding to the real pdf via ENNReal.ofReal.

Русский

Плотность экспоненциального распределения является неприведённой плотностью на ℝ≥0∞ и задаётся через ENNReal.ofReal.

LaTeX

$$$ \text{exponentialPDF}(r, x) = \mathrm{ENNReal.ofReal}(\text{exponentialPDFReal}(r, x)) $$$

Lean4

/-- The pdf of the exponential distribution, as a function valued in `ℝ≥0∞` -/
noncomputable def exponentialPDF (r x : ℝ) : ℝ≥0∞ :=
  ENNReal.ofReal (exponentialPDFReal r x)

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