← Copula mathematical handbook

The left-continuous quantile of a real law

For a probability measure ν on ℝ with distribution function F, the generalized inverse realQuantile ν t = inf {y | t ≤ F y} is monotone on the open unit interval. If F is continuous, then realQuantile ν (F y) = y for ν-almost every y: the exceptional points lie in countably many level sets of F (one for each rational number, and the zero level), each of which is null because F pushes ν forward to the uniform law.

This is the device used for the converse of Nelsen, An Introduction to Copulas, second edition, Theorem 2.5.4 (Copula.RandomVariable.Monotone).

noncomputable def ProbabilityTheory.realQuantile (ν : MeasureTheory.Measure ℝ) (t : ℝ) : ℝ

The left-continuous generalized inverse t ↦ inf {y | t ≤ F y} of the CDF F of ν. Outside (0, 1) the value is Lean's junk value of sInf.

Equations

• ProbabilityTheory.realQuantile ν t = sInf {y : ℝ | t ≤ ↑(ProbabilityTheory.cdf ν) y}

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

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

theorem ProbabilityTheory.monotoneOn_realQuantile (ν : MeasureTheory.Measure ℝ) : MonotoneOn (realQuantile ν) (Set.Ioo 0 1)

The quantile is monotone on the open unit interval.

theorem ProbabilityTheory.realQuantile_cdf_le (ν : MeasureTheory.Measure ℝ) {y : ℝ} (hy : 0 < ↑(cdf ν) y) : realQuantile ν (↑(cdf ν) y) ≤ y

The quantile never exceeds the point at which the CDF is evaluated.

theorem ProbabilityTheory.realQuantile_cdf_eq (ν : MeasureTheory.Measure ℝ) {y : ℝ} (hy : 0 < ↑(cdf ν) y) (hq : ∀ (q : ℚ), ↑(cdf ν) ↑q ≠ ↑(cdf ν) y) : realQuantile ν (↑(cdf ν) y) = y

The quantile inverts the CDF at every point that is not on the level of a rational point.

theorem ProbabilityTheory.ae_realQuantile_cdf (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous ↑(cdf ν)) : ∀ᵐ (y : ℝ) ∂ν, realQuantile ν (↑(cdf ν) y) = y

For a continuous CDF F, the quantile recovers y from F y almost surely.

theorem ProbabilityTheory.ae_cdf_mem_Ioo (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous ↑(cdf ν)) : ∀ᵐ (y : ℝ) ∂ν, ↑(cdf ν) y ∈ Set.Ioo 0 1

For a continuous CDF F, almost surely 0 < F y < 1.