betaPDFReal — Mathlib

English

The real-valued beta density function is βPDFReal(α,β,x) = 1/β(α,β) x^{α-1} (1-x)^{β-1} for 0<x<1 and 0 otherwise.

Русский

Плотность бета-распределения на вещественной шкале: βPDFReal(α,β,x) равна 1/β(α,β) x^{α-1} (1-x)^{β-1} при 0<x<1 и 0 иначе.

LaTeX

$$$\betaPDFReal(\alpha,\beta,x) = \begin{cases} \dfrac{1}{\beta(\alpha,\beta)} x^{\alpha-1} (1-x)^{\beta-1}, & 0

Lean4

/-- The probability density function of the beta distribution with shape parameters `α` and `β`.
Returns `(1 / beta α β) * x ^ (α - 1) * (1 - x) ^ (β - 1)`
when `0 < x < 1` and `0` otherwise. -/
noncomputable def betaPDFReal (α β x : ℝ) : ℝ :=
  if 0 < x ∧ x < 1 then (1 / beta α β) * x ^ (α - 1) * (1 - x) ^ (β - 1) else 0

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