betaPDFReal_pos — Mathlib

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))

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