paretoPDFReal_pos — Mathlib

English

If t>0 and r>0 and t ≤ x, then the Pareto pdf is strictly positive.

Русский

Если t>0 и r>0 и t ≤ x, то плотность Парето положительна.

LaTeX

$$$0 < \\mathrm{paretoPDFReal}(t,r,x)\\quad\\text{for } t>0, r>0, t\\le x$$$

Lean4

/-- The Pareto pdf is positive for all reals `>= t`. -/
theorem paretoPDFReal_pos (ht : 0 < t) (hr : 0 < r) (hx : t ≤ x) : 0 < paretoPDFReal t r x :=
  by
  rw [paretoPDFReal, if_pos hx]
  have _ : 0 < x := by linarith
  positivity

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