paretoPDFReal — Mathlib

English

For all real t, r, x, the Pareto pdf is given by r t^r x^{-(r+1)} when t ≤ x, and 0 otherwise.

Русский

Плотность Парето для действительных t, r, x задаётся как r t^r x^{-(r+1)} при t ≤ x и 0 иначе.

LaTeX

$$$\\mathrm{paretoPDFReal}(t,r,x)=\\begin{cases} r\\,t^{r}\\,x^{-(r+1)}, & t \\le x, \\\\ 0, & t> x. \\end{cases}$$$

Lean4

/-- The pdf of the Pareto distribution depending on its scale `t` and rate `r`. -/
noncomputable def paretoPDFReal (t r x : ℝ) : ℝ :=
  if t ≤ x then r * t ^ r * x ^ (-(r + 1)) else 0

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