poissonPMFReal_nonneg

Mathlib.Probability.Distributions.Poisson

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.poissonPMFReal_nonneg

English

For any rate r≥0 and n∈ℕ, Poisson pmfReal is nonnegative.

Русский

Для любого r≥0 и n∈ℕ плотность Пуассона неотрицательна.

LaTeX

$$$0 \\le \\mathrm{poissonPMFReal}(r,n)$$$

Lean4

theorem poissonPMFReal_nonneg {r : ℝ≥0} {n : ℕ} : 0 ≤ poissonPMFReal r n :=
  by
  unfold poissonPMFReal
  positivity

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru