The quantile function of a real law

The quantile function, or generalized inverse cumulative distribution function, of a measure μ on ℝ sends a level t to the least point at which ProbabilityTheory.cdf μ reaches t:

μ.quantile t = sInf {x | t ≤ cdf μ x}.

Because cdf μ is monotone and right continuous with limits 0 at -∞ and 1 at +∞, that infimum is attained for every level t strictly between 0 and 1, and the defining set is exactly the closed ray to the right of the quantile. The quantile is therefore characterized by the Galois property μ.quantile t ≤ x ↔ t ≤ cdf μ x. At levels t ≤ 0 and 1 < t the infimum ranges over all of ℝ or over the empty set, so the value there is the junk value 0. The endpoint level t = 1 is not junk: the quantile there is the least point of full cumulative mass when such a point exists (for instance (dirac a).quantile 1 = a), and 0 when the law has unbounded support to the right. The inverse characterizations below use levels in Ioo 0 1, which is also the interval the uniform law is taken on.

The main result is inverse transform sampling: for a probability measure μ the quantile function pushes the uniform law on the open unit interval forward to μ. It presents every real law as the law of one explicit measurable function of a single uniform variable, and it is what makes the monotone rearrangement of two real laws a transport plan between them.

Main definitions

• MeasureTheory.Measure.quantile — the generalized inverse of the cumulative distribution function.

Main statements

• MeasureTheory.Measure.quantile_le_iff — the Galois characterization of the quantile, with MeasureTheory.Measure.setOf_le_cdf_eq_Ici its set-level form and MeasureTheory.Measure.lt_quantile_iff its negation;
• MeasureTheory.Measure.map_quantile_volume_Ioo — inverse transform sampling: the quantile function pushes the uniform law on Ioo 0 1 forward to the original law, packaged as MeasureTheory.Measure.measurePreserving_quantile;
• MeasureTheory.Measure.cdf_map_eq_volume_restrict — the probability integral transform for an atomless real law;
• MeasureTheory.Measure.cdf_quantile_ae and MeasureTheory.Measure.quantile_cdf_ae — the two almost-everywhere inverse laws, the first for an atomless law and the second for every law;
• MeasureTheory.Measure.realMod0MeasureIso — for an atomless real law, the pair (cdf ν, ν.quantile) as a TauCeti.Mod0MeasureIso between ν and Lebesgue measure restricted to [0, 1].

References

• R. B. Nelsen, An Introduction to Copulas, Springer 2006, §2.3, for the generalized inverse and its Galois property.
• P. Embrechts and M. Hofert, A note on generalized inverses, Mathematical Methods of Operations Research 77 (2013), 423--432.

Adapted from

The probability integral transform cdf_map_eq_volume_restrict, the inverse laws cdf_quantile_ae and quantile_cdf_ae, the inverse transform sampling theorem map_quantile_volume_Ioo and the resulting realMod0MeasureIso instance are adapted from Cameron Freer's independent implementation in Graphon/MeasureIso.lean at commit 9f7be59fa754d260a544b4cfd83d6a5b94f7552e: https://github.com/cameronfreer/graphon/commit/9f7be59fa754d260a544b4cfd83d6a5b94f7552e, where they appear as cdf_map_eq_volume_restrict, cdf_cdfQuantile_ae, cdfQuantile_cdf_ae, map_cdfQuantile_volume_restrict and realMod0MeasureIso, with the generalized inverse called cdfQuantile rather than quantile; the graphon-specific packaging was removed. The original work is copyright Cameron Freer and licensed under Apache 2.0.

The measure-preserving equivalence that this file realizes on the real line is the classical transport of an atomless standard-Borel space to the unit interval, proved as Theorem A.7 in S. Janson, Graphons, cut norm and distance, couplings and rearrangements, Arkiv för Matematik 52 (2014); see also TauCeti.MeasureTheory.Measure.exists_mpModNull_equiv_unitInterval in TauCeti.MeasureTheory.Measure.AtomlessStandardBorel, which composes it with TauCeti.embeddingRealMod0MeasureIso.

noncomputable def MeasureTheory.Measure.quantile (μ : Measure ℝ) (t : ℝ) : ℝ

The quantile function of a measure on ℝ: the least point at which its cumulative distribution function reaches the level t.

This is the honest generalized inverse of ProbabilityTheory.cdf μ for t in Set.Ioo 0 1. At levels t ≤ 0 and 1 < t the defining infimum ranges over all of ℝ or over the empty set, and the value is the junk value 0 (quantile_of_nonpos, quantile_of_one_lt). At the endpoint level t = 1 the value is the least point where the cumulative distribution function reaches 1 if there is one, and 0 otherwise.

Equations

• μ.quantile t = sInf {x : ℝ | t ≤ ↑(ProbabilityTheory.cdf μ) x}

theorem MeasureTheory.Measure.quantile_def (μ : Measure ℝ) (t : ℝ) : μ.quantile t = sInf {x : ℝ | t ≤ ↑(ProbabilityTheory.cdf μ) x}

The quantile function is the infimum of the points at which the cumulative distribution function reaches the level. The definition's body is not exposed, so this is the lemma downstream modules should rewrite with.

theorem MeasureTheory.Measure.nonempty_setOf_le_cdf {t : ℝ} (μ : Measure ℝ) (ht : t < 1) : {x : ℝ | t ≤ ↑(ProbabilityTheory.cdf μ) x}.Nonempty

Below the level 1 some point has cumulative mass at least the level, because the cumulative distribution function tends to 1 at +∞.

theorem MeasureTheory.Measure.bddBelow_setOf_le_cdf {t : ℝ} (μ : Measure ℝ) (ht : 0 < t) : BddBelow {x : ℝ | t ≤ ↑(ProbabilityTheory.cdf μ) x}

Above the level 0 the points whose cumulative mass reaches the level are bounded below, because the cumulative distribution function tends to 0 at -∞.

@[simp]

theorem MeasureTheory.Measure.quantile_of_nonpos {t : ℝ} (μ : Measure ℝ) (ht : t ≤ 0) : μ.quantile t = 0

At a nonpositive level the quantile function takes the junk value 0: every point has cumulative mass at least the level.

@[simp]

theorem MeasureTheory.Measure.quantile_of_one_lt {t : ℝ} (μ : Measure ℝ) (ht : 1 < t) : μ.quantile t = 0

Above the level 1 the quantile function takes the junk value 0: no point has cumulative mass that large.

theorem MeasureTheory.Measure.le_cdf_quantile {t : ℝ} (μ : Measure ℝ) (h1 : t < 1) : t ≤ ↑(ProbabilityTheory.cdf μ) (μ.quantile t)

The cumulative distribution function at the quantile reaches every level strictly below 1.

@[simp]

theorem MeasureTheory.Measure.quantile_le_iff {t x : ℝ} (μ : Measure ℝ) (h0 : 0 < t) (h1 : t < 1) : μ.quantile t ≤ x ↔ t ≤ ↑(ProbabilityTheory.cdf μ) x

The Galois characterization of the quantile. For a level strictly between 0 and 1, the quantile lies below a point exactly when the cumulative distribution function at that point reaches the level.

theorem MeasureTheory.Measure.setOf_le_cdf_eq_Ici {t : ℝ} (μ : Measure ℝ) (h0 : 0 < t) (h1 : t < 1) : {x : ℝ | t ≤ ↑(ProbabilityTheory.cdf μ) x} = Set.Ici (μ.quantile t)

The set of points whose cumulative mass reaches a level strictly between 0 and 1 is the closed ray to the right of the quantile at that level.

@[simp]

theorem MeasureTheory.Measure.lt_quantile_iff {t x : ℝ} (μ : Measure ℝ) (h0 : 0 < t) (h1 : t < 1) : x < μ.quantile t ↔ ↑(ProbabilityTheory.cdf μ) x < t

A point lies strictly below the quantile at a level exactly when its cumulative mass has not yet reached that level.

theorem MeasureTheory.Measure.monotoneOn_quantile (μ : Measure ℝ) : MonotoneOn μ.quantile (Set.Ioo 0 1)

The quantile function is monotone on the levels where it is the honest generalized inverse.

theorem MeasureTheory.Measure.measurable_quantile (μ : Measure ℝ) : Measurable μ.quantile

The quantile function is measurable.

theorem MeasureTheory.Measure.map_quantile_volume_Ioo (μ : Measure ℝ) [IsProbabilityMeasure μ] : map μ.quantile (volume.restrict (Set.Ioo 0 1)) = μ

Inverse transform sampling. The quantile function of a probability law on ℝ pushes the uniform law on the open unit interval forward to that law.

theorem MeasureTheory.Measure.measurePreserving_quantile (μ : Measure ℝ) [IsProbabilityMeasure μ] : MeasurePreserving μ.quantile (volume.restrict (Set.Ioo 0 1)) μ

Inverse transform sampling, as a measure-preserving map from the uniform law on the open unit interval.

@[simp]

theorem MeasureTheory.Measure.cdf_map_eq_volume_restrict (ν : Measure ℝ) [IsProbabilityMeasure ν] [NullSingletonClass ν] : map (↑(ProbabilityTheory.cdf ν)) ν = volume.restrict (Set.Icc 0 1)

The probability integral transform. The CDF of an atomless probability measure on ℝ pushes the measure forward to Lebesgue measure restricted to [0, 1].

theorem MeasureTheory.Measure.cdf_quantile_ae (ν : Measure ℝ) [IsProbabilityMeasure ν] [NullSingletonClass ν] : (fun (u : ℝ) => ↑(ProbabilityTheory.cdf ν) (ν.quantile u)) =ᵐ[volume.restrict (Set.Icc 0 1)] id

On the closed unit interval, the CDF and quantile are inverse almost everywhere.

theorem MeasureTheory.Measure.quantile_cdf_ae (ν : Measure ℝ) [IsProbabilityMeasure ν] : (fun (x : ℝ) => ν.quantile (↑(ProbabilityTheory.cdf ν) x)) =ᵐ[ν] id

The quantile of the CDF is the identity almost everywhere, for every real probability measure. The cumulative distribution function of a law with atoms has plateaus, but the part of a plateau strictly to the right of a point whose cumulative mass is below 1 is null, so almost every point is the least point reaching its own level.

noncomputable def MeasureTheory.Measure.realMod0MeasureIso (ν : Measure ℝ) [IsProbabilityMeasure ν] [NullSingletonClass ν] : TauCeti.Mod0MeasureIso ℝ ℝ ν (volume.restrict (Set.Icc 0 1))

The CDF/quantile transport of an atomless real law. The cumulative distribution function and the quantile function of an atomless probability measure ν on ℝ push ν and Lebesgue measure restricted to [0, 1] forward onto one another, and are mutually inverse almost everywhere; together they are a mod-zero isomorphism between ν and the unit interval.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.Measure.realMod0MeasureIso_toFun (ν : Measure ℝ) [IsProbabilityMeasure ν] [NullSingletonClass ν] : ν.realMod0MeasureIso.toFun = ↑(ProbabilityTheory.cdf ν)

@[simp]

theorem MeasureTheory.Measure.realMod0MeasureIso_invFun (ν : Measure ℝ) [IsProbabilityMeasure ν] [NullSingletonClass ν] : ν.realMod0MeasureIso.invFun = ν.quantile