beta — Mathlib

English

The normalizing constant for the beta distribution is β(α,β) = Γ(α) Γ(β) / Γ(α+β).

Русский

Нормирующая константа бета-распределения: β(α,β) = Γ(α) Γ(β) / Γ(α+β).

LaTeX

$$$\beta(\alpha,\beta) = \dfrac{\Gamma(\alpha) \Gamma(\beta)}{\Gamma(\alpha+\beta)}$$$

Lean4

/-- The normalizing constant in the beta distribution. -/
noncomputable def beta (α β : ℝ) : ℝ :=
  Real.Gamma α * Real.Gamma β / Real.Gamma (α + β)

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