← Copula mathematical handbook

Quantiles of laws on the unit interval

The compact unit interval allows a total quantile, including at zero and one. The proof of the quantile adjunction follows the construction in mathlib's Probability.Kernel.Representation, specialized to a single probability law.

noncomputable def ProbabilityTheory.unitQuantile (μ : MeasureTheory.Measure ↑unitInterval) (t : ↑unitInterval) : ↑unitInterval

The generalized inverse of the distribution function of a law on [0,1].

Equations

• ProbabilityTheory.unitQuantile μ t = sSup {x : ↑unitInterval | μ.real (Set.Iic x) < ↑t}

theorem ProbabilityTheory.monotone_unitQuantile (μ : MeasureTheory.Measure ↑unitInterval) : Monotone (unitQuantile μ)

theorem ProbabilityTheory.measurable_unitQuantile (μ : MeasureTheory.Measure ↑unitInterval) : Measurable (unitQuantile μ)

theorem ProbabilityTheory.unitQuantile_le_iff (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure μ] (t x : ↑unitInterval) : unitQuantile μ t ≤ x ↔ ↑t ≤ μ.real (Set.Iic x)

The quantile adjunction holds at atoms and at both endpoints.

theorem ProbabilityTheory.map_unitQuantile (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.Measure.map (unitQuantile μ) MeasureTheory.volume = μ

Inverse-transform sampling is valid for arbitrary laws, including atomic laws.