poissonPMFReal_pos — Mathlib

English

For rate r>0, the Poisson pmf is strictly positive for all n ∈ ℕ.

Русский

Для параметра r>0 вероятность Пуассона положительна для каждого n∈ℕ.

LaTeX

$$$0 < \\mathrm{poissonPMFReal}(r,n) \\quad\\text{for } r>0$$$

Lean4

/-- The Poisson pmf is positive for all natural numbers -/
theorem poissonPMFReal_pos {r : ℝ≥0} {n : ℕ} (hr : 0 < r) : 0 < poissonPMFReal r n :=
  by
  rw [poissonPMFReal]
  positivity

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