betaPDF — Mathlib

English

The beta density function valued in ℝ≥0∞ is given by βPDF(α,β,x) = ENNReal.ofReal(βPDFReal(α,β,x)).

Русский

Плотность Бета-распределения в ℝ≥0∞ задаётся как βPDF(α,β,x) = ENNReal.ofReal(βPDFReal(α,β,x)).

LaTeX

$$$\betaPDF(\alpha,\beta,x) = \operatorname{ENNReal}.ofReal\bigl(\betaPDFReal(\alpha,\beta,x)\bigr).$$$

Lean4

/-- The pdf of the beta distribution, as a function valued in `ℝ≥0∞`. -/
noncomputable def betaPDF (α β x : ℝ) : ℝ≥0∞ :=
  ENNReal.ofReal (betaPDFReal α β x)

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