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.

Equations

• ProbabilityTheory.paretoPDFReal t r x = if t ≤ x then r * t ^ r * x ^ (-(r + 1)) else 0

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

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

Equations

• ProbabilityTheory.paretoPDF t r x = ENNReal.ofReal (ProbabilityTheory.paretoPDFReal t r x)

theorem ProbabilityTheory.paretoPDF_eq (t r x : ℝ) : ProbabilityTheory.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) : ProbabilityTheory.paretoPDF t r x = 0

theorem ProbabilityTheory.paretoPDF_of_le {t r x : ℝ} (hx : t ≤ x) : ProbabilityTheory.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, ProbabilityTheory.paretoPDF t r y = 0

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

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

The Pareto pdf is measurable.

theorem ProbabilityTheory.stronglyMeasurable_paretoPDFReal (t r : ℝ) : MeasureTheory.StronglyMeasurable (ProbabilityTheory.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 < ProbabilityTheory.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 ≤ ProbabilityTheory.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 : ℝ), ProbabilityTheory.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.

Equations

• ProbabilityTheory.paretoMeasure t r = MeasureTheory.volume.withDensity (ProbabilityTheory.paretoPDF t r)

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

theorem ProbabilityTheory.paretoCDFReal_eq_integral {t r : ℝ} (ht : 0 < t) (hr : 0 < r) (x : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.paretoMeasure t r)) x = ∫ (x : ℝ) in Set.Iic x, ProbabilityTheory.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 : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.paretoMeasure t r)) x = (∫⁻ (x : ℝ) in Set.Iic x, ProbabilityTheory.paretoPDF t r x).toReal