betaPDF_of_pos_lt_one — Mathlib

English

If 0 < x < 1, then betaPDF α β x equals ENNReal.ofReal of ((1 / beta α β) * x^(α - 1) * (1 - x)^(β - 1)).

Русский

Если 0 < x < 1, то betaPDF α β x равняется ENNReal.ofReal( (1 / beta(α,β)) * x^(α-1) * (1 - x)^(β-1) ).

LaTeX

$$$\forall \alpha,\beta, x \in \mathbb{R},\ 0 < x \Rightarrow x < 1 \Rightarrow \betaPDF(\alpha,\beta,x)=\mathrm{ENNReal}.ofReal\left(\frac{1}{\beta(\alpha,\beta)} x^{\alpha-1}(1-x)^{\beta-1}\right)$$$

Lean4

theorem betaPDF_of_pos_lt_one {α β x : ℝ} (hx_pos : 0 < x) (hx_lt : x < 1) :
    betaPDF α β x = ENNReal.ofReal ((1 / beta α β) * x ^ (α - 1) * (1 - x) ^ (β - 1)) := by
  rw [betaPDF_eq, if_pos ⟨hx_pos, hx_lt⟩]

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