paretoPDF — Mathlib

English

The Pareto pdf, viewed as a function with values in the extended nonnegative reals, is obtained by applying the nonnegative-Real embedding to the real-valued pdf.

Русский

Плотность Парето, рассматриваемая как функция, значения которой лежат в расширенных неотрицательных числах, получается путём применения вложения из вещественных чисел в ℝ≥0∞ к вещественной плотности.

LaTeX

$$$\\mathrm{paretoPDF}(t,r,x)=\\mathrm{ENNReal.ofReal}(\\mathrm{paretoPDFReal}(t,r,x))$$$

Lean4

/-- The pdf of the Pareto distribution, as a function valued in `ℝ≥0∞`. -/
noncomputable def paretoPDF (t r x : ℝ) : ℝ≥0∞ :=
  ENNReal.ofReal (paretoPDFReal t r x)

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