Documentation

TauCeti.Probability.Distributions.Pareto.Basic

Elementary theory of the Pareto distribution #

This file completes the elementary API for Mathlib's Pareto measure. For positive threshold t and shape r, it proves the exact real-power moment criterion and formula, then derives the mean, variance, and the matching non-integrability statements at the sharp thresholds. It also computes the cdf and the exact domain of exponential integrability.

The common calculation is

∫ x, x ^ q ∂paretoMeasure t r = r * t ^ q / (r - q) for q < r.

Here ^ on a real exponent is Real.rpow. The density is supported on [t, ∞), where all bases are positive, so Mathlib's improper-integral criterion for real powers applies directly.

Main results #

References #

source
theorem TauCeti.Probability.paretoMeasure_eq_withDensity_ofReal (t r : ℝ) :
ProbabilityTheory.paretoMeasure t r = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (ProbabilityTheory.paretoPDFReal t r x)

The Pareto law presented by its real-valued density.

source
theorem TauCeti.Probability.integrable_paretoMeasure_iff {t r : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ht : 0 ≤ t) (hr : 0 ≤ r) {g : ℝ → E} :
MeasureTheory.Integrable g (ProbabilityTheory.paretoMeasure t r) ↔ MeasureTheory.Integrable (fun (x : ℝ) => ProbabilityTheory.paretoPDFReal t r x • g x) MeasureTheory.volume

Integrability transfer. A function is integrable against a Pareto law with nonnegative threshold and shape exactly when its density-weighted version is Lebesgue integrable.

source
theorem TauCeti.Probability.integral_paretoMeasure_eq {t r : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ht : 0 ≤ t) (hr : 0 ≤ r) (g : ℝ → E) :
∫ (x : ℝ), g x ∂ProbabilityTheory.paretoMeasure t r = ∫ (x : ℝ), ProbabilityTheory.paretoPDFReal t r x • g x

Integral transfer. An integral against a Pareto law with nonnegative threshold and shape is the density-weighted Lebesgue integral.

source
theorem TauCeti.Probability.ae_paretoMeasure_mem_Ici (t r : ℝ) :
∀ᵐ (x : ℝ) ∂ProbabilityTheory.paretoMeasure t r, t ≤ x

A Pareto law is carried by the half-line [t, ∞) above its threshold.

source
@[simp]
theorem TauCeti.Probability.integrable_rpow_paretoMeasure_iff {t r : ℝ} (ht : 0 < t) (hr : 0 < r) (q : ℝ) :
MeasureTheory.Integrable (fun (x : ℝ) => x ^ q) (ProbabilityTheory.paretoMeasure t r) ↔ q < r

A real power is integrable under a nondegenerate Pareto law exactly below the shape parameter.

source
theorem TauCeti.Probability.integral_rpow_paretoMeasure {t r q : ℝ} (ht : 0 < t) (hr : 0 < r) (hq : q < r) :
∫ (x : ℝ), x ^ q ∂ProbabilityTheory.paretoMeasure t r = r * t ^ q / (r - q)

The q-th real-power moment of a Pareto law is r * t ^ q / (r - q) below the shape parameter.

source
theorem TauCeti.Probability.integral_id_paretoMeasure {t r : ℝ} (ht : 0 < t) (hr : 1 < r) :
∫ (x : ℝ), x ∂ProbabilityTheory.paretoMeasure t r = r * t / (r - 1)

The mean of a Pareto law is r * t / (r - 1) when 1 < r.

source
@[simp]
theorem TauCeti.Probability.integrable_id_paretoMeasure_iff {t r : ℝ} (ht : 0 < t) (hr : 0 < r) :
MeasureTheory.Integrable id (ProbabilityTheory.paretoMeasure t r) ↔ 1 < r

The identity is integrable under a Pareto law exactly when the shape exceeds 1.

source
theorem TauCeti.Probability.not_integrable_id_paretoMeasure {t r : ℝ} (ht : 0 < t) (hr : 0 < r) (h : r ≤ 1) :
¬MeasureTheory.Integrable id (ProbabilityTheory.paretoMeasure t r)

At or below shape 1, a nondegenerate Pareto law has no finite mean.

source
theorem TauCeti.Probability.integral_sq_paretoMeasure {t r : ℝ} (ht : 0 < t) (hr : 2 < r) :
∫ (x : ℝ), x ^ 2 ∂ProbabilityTheory.paretoMeasure t r = r * t ^ 2 / (r - 2)

The second raw moment of a Pareto law is r * t² / (r - 2) when 2 < r.

source
@[simp]
theorem TauCeti.Probability.integrable_sq_paretoMeasure_iff {t r : ℝ} (ht : 0 < t) (hr : 0 < r) :
MeasureTheory.Integrable (fun (x : ℝ) => x ^ 2) (ProbabilityTheory.paretoMeasure t r) ↔ 2 < r

Squaring is integrable under a Pareto law exactly when the shape exceeds 2.

source
theorem TauCeti.Probability.not_integrable_sq_paretoMeasure {t r : ℝ} (ht : 0 < t) (hr : 0 < r) (h : r ≤ 2) :
¬MeasureTheory.Integrable (fun (x : ℝ) => x ^ 2) (ProbabilityTheory.paretoMeasure t r)

At or below shape 2, the second raw moment of a nondegenerate Pareto law diverges.

source
theorem TauCeti.Probability.variance_id_paretoMeasure {t r : ℝ} (ht : 0 < t) (hr : 2 < r) :
ProbabilityTheory.variance id (ProbabilityTheory.paretoMeasure t r) = r * t ^ 2 / ((r - 1) ^ 2 * (r - 2))

The variance of a Pareto law is r * t² / ((r - 1)² * (r - 2)) when 2 < r.

source
@[simp]
theorem TauCeti.Probability.cdf_paretoMeasure_eq {t r : ℝ} (ht : 0 < t) (hr : 0 < r) (x : ℝ) :
↑(ProbabilityTheory.cdf (ProbabilityTheory.paretoMeasure t r)) x = if x < t then 0 else 1 - (t / x) ^ r

The cdf of a nondegenerate Pareto law: it vanishes below the threshold and equals 1 - (t / x) ^ r on and above it.

source
theorem TauCeti.Probability.integrable_exp_mul_id_paretoMeasure_of_nonpos {t r : ℝ} (ht : 0 < t) (hr : 0 < r) {u : ℝ} (hu : u ≤ 0) :
MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (u * x)) (ProbabilityTheory.paretoMeasure t r)

Every nonpositive exponential rate is integrable under a nondegenerate Pareto law.

source
@[simp]
theorem TauCeti.Probability.integrable_exp_mul_id_paretoMeasure_iff {t r : ℝ} (ht : 0 < t) (hr : 0 < r) (u : ℝ) :
MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (u * x)) (ProbabilityTheory.paretoMeasure t r) ↔ u ≤ 0

The exponential of a multiple of the identity is integrable under a nondegenerate Pareto law exactly when the rate is nonpositive.

source
@[simp]
theorem TauCeti.Probability.integrableExpSet_id_paretoMeasure {t r : ℝ} (ht : 0 < t) (hr : 0 < r) :
ProbabilityTheory.integrableExpSet id (ProbabilityTheory.paretoMeasure t r) = Set.Iic 0

The exact exponential-integrability domain of the identity under a nondegenerate Pareto law is the nonpositive half-line.