English
Let a > 0 and r > 0. The gamma density with parameters (a, r) is supported on [0, ∞) and satisfies gammaPDF(a, r, x) = ENNReal.ofReal((r^a / Γ(a)) x^(a−1) e^(−r x)) for x ≥ 0, and gammaPDF(a, r, x) = 0 for x < 0.
Русский
Пусть a > 0 и r > 0. Плотность гамма-распределения с параметрами (a, r) поддерживается на [0, ∞) и выполняется gammaPDF(a, r, x) = ENNReal.ofReal((r^a / Γ(a)) x^(a−1) e^(−r x)) при x ≥ 0, а при x < 0 gammaPDF(a, r, x) = 0.
LaTeX
$$$\gammaPDF(a,r,x) = \mathrm{ENNReal.ofReal}\left(\text{if } 0 \le x \text{ then } \frac{r^{a}}{\Gamma(a)} x^{a-1} e^{-r x} \text{ else } 0\right)$$$
Lean4
theorem gammaPDF_eq (a r x : ℝ) :
gammaPDF a r x = ENNReal.ofReal (if 0 ≤ x then r ^ a / (Gamma a) * x ^ (a - 1) * exp (-(r * x)) else 0) :=
rfl
