gammaPDFReal_nonneg

Mathlib.Probability.Distributions.Gamma

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

← MathLib Explorer

English

For all a > 0, r > 0, x ∈ ℝ, gammaPDFReal(a, r, x) ≥ 0.

Русский

Для всех a > 0, r > 0, x ∈ ℝ, gammaPDFReal(a, r, x) ≥ 0.

LaTeX

$$$0 \le \gammaPDFReal(a,r,x)$$$

Lean4

/-- The gamma pdf is nonnegative -/
theorem gammaPDFReal_nonneg {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) : 0 ≤ gammaPDFReal a r x :=
  by
  unfold gammaPDFReal
  split_ifs <;> positivity

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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