betaPDF_eq — Mathlib

English

The Beta density equals ENNReal.ofReal of the piecewise expression giving 0 outside the interval and the beta density inside.

Русский

Плотность Бета равна ENNReal.ofReal указанной покомпонентной функции: 0 вне интервала, внутри — плотность Бета.

LaTeX

$$$\betaPDF(\alpha,\beta,x) = \operatorname{ENNReal}.ofReal\Big(\begin{cases} 0, & \text{если } x \notin (0,1), \\ \dfrac{1}{\beta(\alpha,\beta)} x^{\alpha-1} (1-x)^{\beta-1}, & \text{если } 0 < x < 1. \end{cases}\Big)$$$

Lean4

theorem betaPDF_eq (α β x : ℝ) :
    betaPDF α β x = ENNReal.ofReal (if 0 < x ∧ x < 1 then (1 / beta α β) * x ^ (α - 1) * (1 - x) ^ (β - 1) else 0) :=
  rfl

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