gammaPDF_of_neg

Mathlib.Probability.Distributions.Gamma

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

English

For any a, r ∈ ℝ and x ∈ ℝ, if x < 0 then gammaPDF(a, r, x) = 0.

Русский

Для любых a, r ∈ ℝ и x ∈ ℝ, если x < 0, то gammaPDF(a, r, x) = 0.

LaTeX

$$$\gammaPDF(a,r,x) = 0 \quad\text{if } x<0$$$

Lean4

theorem gammaPDF_of_neg {a r x : ℝ} (hx : x < 0) : gammaPDF a r x = 0 := by
  simp only [gammaPDF_eq, if_neg (not_le.mpr hx), ENNReal.ofReal_zero]

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

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

Разделы

Аффилиация

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