Pareto distributions over ℝ

Define the Pareto measure over the reals.

Main definitions

• paretoPDFReal: the function t r x ↦ r * t ^ r * x ^ -(r + 1) for t ≤ x or 0 else, which is the probability density function of a Pareto distribution with scale t and shape r (when ht : 0 < t and hr : 0 < r).
• paretoPDF: ℝ≥0∞-valued pdf, paretoPDF t r = ENNReal.ofReal (paretoPDFReal t r).
• paretoMeasure: a Pareto measure on ℝ, parametrized by its scale t and shape r.
• paretoCDFReal: the CDF given by the definition of CDF in ProbabilityTheory.CDF applied to the Pareto measure.

noncomputable def ProbabilityTheory.paretoPDFReal (t r x : ℝ) : ℝ

The pdf of the Pareto distribution depending on its scale t and rate r.

noncomputable def ProbabilityTheory.paretoPDF (t r x : ℝ) : ENNReal

The pdf of the Pareto distribution, as a function valued in ℝ≥0∞.

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

theorem ProbabilityTheory.paretoPDF_of_lt {t r x : ℝ} (hx : x < t) : paretoPDF t r x = 0

theorem ProbabilityTheory.paretoPDF_of_le {t r x : ℝ} (hx : t ≤ x) : paretoPDF t r x = ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))

theorem ProbabilityTheory.lintegral_paretoPDF_of_le {t r x : ℝ} (hx : x ≤ t) : ∫⁻ (y : ℝ) in Set.Iio x, paretoPDF t r y = 0

The Lebesgue integral of the Pareto pdf over reals ≤ t equals 0.

theorem ProbabilityTheory.measurable_paretoPDFReal (t r : ℝ) : Measurable (paretoPDFReal t r)

The Pareto pdf is measurable.

theorem ProbabilityTheory.stronglyMeasurable_paretoPDFReal (t r : ℝ) : MeasureTheory.StronglyMeasurable (paretoPDFReal t r)

The Pareto pdf is strongly measurable.

theorem ProbabilityTheory.paretoPDFReal_pos {t r x : ℝ} (ht : 0 < t) (hr : 0 < r) (hx : t ≤ x) : 0 < paretoPDFReal t r x

The Pareto pdf is positive for all reals >= t.

theorem ProbabilityTheory.paretoPDFReal_nonneg {t r : ℝ} (ht : 0 ≤ t) (hr : 0 ≤ r) (x : ℝ) : 0 ≤ paretoPDFReal t r x

The Pareto pdf is nonnegative.

@[simp]

theorem ProbabilityTheory.lintegral_paretoPDF_eq_one {t r : ℝ} (ht : 0 < t) (hr : 0 < r) : ∫⁻ (x : ℝ), paretoPDF t r x = 1

The pdf of the Pareto distribution integrates to 1.

noncomputable def ProbabilityTheory.paretoMeasure (t r : ℝ) : MeasureTheory.Measure ℝ

Measure defined by the Pareto distribution.

theorem ProbabilityTheory.isProbabilityMeasure_paretoMeasure {t r : ℝ} (ht : 0 < t) (hr : 0 < r) : MeasureTheory.IsProbabilityMeasure (paretoMeasure t r)

theorem ProbabilityTheory.paretoCDFReal_eq_integral {t r : ℝ} (ht : 0 < t) (hr : 0 < r) (x : ℝ) : ↑(cdf (paretoMeasure t r)) x = ∫ (x : ℝ) in Set.Iic x, paretoPDFReal t r x

CDF of the Pareto distribution equals the integral of the PDF.

theorem ProbabilityTheory.paretoCDFReal_eq_lintegral {t r : ℝ} (ht : 0 < t) (hr : 0 < r) (x : ℝ) : ↑(cdf (paretoMeasure t r)) x = (∫⁻ (x : ℝ) in Set.Iic x, paretoPDF t r x).toReal