English
For 0 < x < 1 and α > 0, β > 0, we have 0 < betaPDFReal α β x.
Русский
Пусть 0 < x < 1, α > 0 и β > 0. Тогда betaPDFReal α β x > 0.
LaTeX
$$$0 < \betaPDFReal(\alpha,\beta,x)\quad\text{при}\quad 0 < x < 1,\ 0 < \alpha,\ 0 < \beta$$$
Lean4
/-- The beta pdf is positive for all positive reals with positive parameters. -/
theorem betaPDFReal_pos {α β x : ℝ} (hx1 : 0 < x) (hx2 : x < 1) (hα : 0 < α) (hβ : 0 < β) : 0 < betaPDFReal α β x :=
by
rw [betaPDFReal, if_pos ⟨hx1, hx2⟩]
exact
mul_pos (mul_pos (one_div_pos.2 (beta_pos hα hβ)) (Real.rpow_pos_of_pos hx1 (α - 1)))
(Real.rpow_pos_of_pos (by linarith) (β - 1))