Pareto distributions over ℝ #
Define the Pareto measure over the reals.
Main definitions #
paretoPDFReal
: the functiont r x ↦ r * t ^ r * x ^ -(r + 1)
fort ≤ x
or0
else, which is the probability density function of a Pareto distribution with scalet
and shaper
(whenht : 0 < t
andhr : 0 < r
).paretoPDF
:ℝ≥0∞
-valued pdf,paretoPDF t r = ENNReal.ofReal (paretoPDFReal t r)
.paretoMeasure
: a Pareto measure onℝ
, parametrized by its scalet
and shaper
.
The pdf of the Pareto distribution, as a function valued in ℝ≥0∞
.
Equations
Instances For
The Pareto pdf is measurable.
The Pareto pdf is strongly measurable.
The Pareto pdf is positive for all reals >= t
.
The Pareto pdf is nonnegative.
Measure defined by the Pareto distribution.
Equations
Instances For
theorem
ProbabilityTheory.cdf_paretoMeasure_eq_integral
{t r : ℝ}
(ht : 0 < t)
(hr : 0 < r)
(x : ℝ)
:
CDF of the Pareto distribution equals the integral of the PDF.
@[deprecated ProbabilityTheory.cdf_paretoMeasure_eq_integral (since := "2025-08-28")]
Alias of ProbabilityTheory.cdf_paretoMeasure_eq_integral
.
CDF of the Pareto distribution equals the integral of the PDF.
@[deprecated ProbabilityTheory.cdf_paretoMeasure_eq_lintegral (since := "2025-08-28")]