paretoPDF_eq — Mathlib

English

The Pareto pdf equals ENNReal.ofReal of the real-valued pdf with the same piecewise form.

Русский

Плотность Парето равна ENNReal.ofReal от вещественной плотности с тем же разбиением по условиям.

LaTeX

$$$\\mathrm{paretoPDF}(t,r,x)=\\mathrm{ENNReal.ofReal}\\bigl(\\mathrm{if }(t\\le x)\\text{ then } r t^{r} x^{-(r+1)} \\text{ else } 0\\bigr)$$$

Lean4

theorem paretoPDF_eq (t r x : ℝ) : paretoPDF t r x = ENNReal.ofReal (if t ≤ x then r * t ^ r * x ^ (-(r + 1)) else 0) :=
  rfl

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