poissonPMFReal — Mathlib

English

The Poisson pmf real-valued density is given by exp(-r) r^n / n! for rate r and count n.

Русский

Плотность Пуассоновской смеси в вещественном виде задаётся как e^{-r} r^n / n! для параметра скорости r и счётчика n.

LaTeX

$$$\\mathrm{poissonPMFReal}(r,n)=e^{-r}\\,\\frac{r^{n}}{n!}$$$

Lean4

/-- The pmf of the Poisson distribution depending on its rate, as a function to ℝ -/
noncomputable def poissonPMFReal (r : ℝ≥0) (n : ℕ) : ℝ :=
  exp (-r) * r ^ n / n !

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