Quantile function and inverse transform sampling

DefinitionQuantile function of a real measure#✓fully proved

Let \(\mu\) be a measure on \(\mathbb{R}\) with cumulative distribution function \(F_\mu\) (for a probability measure, \(F_\mu(x) = \mu((-\infty, x])\)). The quantile function of \(\mu\), the generalized inverse of \(F_\mu\), is the function \(Q_\mu : \mathbb{R} \to \mathbb{R}\) given by \(Q_\mu(u) = \inf \lbrace x \in \mathbb{R} : u \le F_\mu(x) \rbrace\) for \(u \in (0, 1)\) and \(Q_\mu(u) = 0\) for \(u \notin (0, 1)\).

noncomputable def cdfQuantile (μ : Measure ℝ) (u : ℝ) : ℝ :=
  if u ∈ Ioo (0 : ℝ) 1 then sInf {x : ℝ | u ≤ cdf μ x} else 0

Used by 6

Used bySkorokhod representation theorem · The quantile function as a generalized inverse of the cdf · The cdf at the quantile is at least the level · Monotonicity of the quantile function · Inverse transform sampling · Measurability of the quantile function

TheoremThe cdf at the quantile is at least the level#✓fully proved

Let \(\mu\) be a measure on \(\mathbb{R}\) with cumulative distribution function \(F_\mu\) and quantile function \(Q_\mu\). For every \(u \in (0, 1)\), \(u \le F_\mu(Q_\mu(u))\).

theorem cdfQuantile_mem (μ : Measure ℝ) {u : ℝ} (hu : u ∈ Ioo (0 : ℝ) 1) :
    u ≤ cdf μ (cdfQuantile μ u)

Uses 1 · Used by 1

Statement usesQuantile function of a real measure

Used byThe quantile function as a generalized inverse of the cdf

TheoremThe quantile function as a generalized inverse of the cdf#✓fully proved

Let \(\mu\) be a measure on \(\mathbb{R}\) with cumulative distribution function \(F_\mu\) and quantile function \(Q_\mu\). For every \(u \in (0, 1)\) and every real \(x\), \(Q_\mu(u) \le x\) if and only if \(u \le F_\mu(x)\).

theorem cdfQuantile_le_iff (μ : Measure ℝ) {u : ℝ} (hu : u ∈ Ioo (0 : ℝ) 1)
    {x : ℝ} : cdfQuantile μ u ≤ x ↔ u ≤ cdf μ x

Uses 2 · Used by 4

Statement usesQuantile function of a real measure

Proof usesThe cdf at the quantile is at least the level

Used bySkorokhod representation theorem · Monotonicity of the quantile function · Inverse transform sampling · Measurability of the quantile function

TheoremMonotonicity of the quantile function#✓fully proved

For every measure \(\mu\) on \(\mathbb{R}\), the quantile function \(Q_\mu\) is monotone on \((0, 1)\): if \(0 < u \le v < 1\), then \(Q_\mu(u) \le Q_\mu(v)\).

theorem cdfQuantile_monoOn (μ : Measure ℝ) : MonotoneOn (cdfQuantile μ) (Ioo 0 1)

Uses 2 · Used by 1

Statement usesQuantile function of a real measure

Proof usesThe quantile function as a generalized inverse of the cdf

Used bySkorokhod representation theorem

TheoremMeasurability of the quantile function#✓fully proved

For every measure \(\mu\) on \(\mathbb{R}\), the quantile function \(Q_\mu : \mathbb{R} \to \mathbb{R}\) is measurable.

theorem measurable_cdfQuantile (μ : Measure ℝ) : Measurable (cdfQuantile μ)

Uses 2 · Used by 2

Statement usesQuantile function of a real measure

Proof usesThe quantile function as a generalized inverse of the cdf

Used bySkorokhod representation theorem · Inverse transform sampling

TheoremInverse transform sampling#✓fully proved

Let \(\mu\) be a probability measure on \(\mathbb{R}\) with quantile function \(Q_\mu\). The pushforward under \(Q_\mu\) of Lebesgue measure restricted to \([0, 1]\) is \(\mu\).

theorem map_cdfQuantile_restrict_Icc (μ : Measure ℝ) [IsProbabilityMeasure μ] :
    Measure.map (cdfQuantile μ) (volume.restrict (Icc (0 : ℝ) 1)) = μ

Uses 3 · Used by 1

Statement usesQuantile function of a real measure

Proof usesThe quantile function as a generalized inverse of the cdf · Measurability of the quantile function

Used bySkorokhod representation theorem

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.