Cumulative distribution function

TheoremAtoms are the jumps of the cdf#✓fully proved

Let \(\mu\) be a probability measure on \(\mathbb{R}\) with cumulative distribution function \(F(y) = \mu((-\infty, y])\), and for \(x \in \mathbb{R}\) let \(F(x^-) = \lim_{y \to x^-} F(y)\) be its left limit at \(x\). Then \(\mu(\{x\})\) equals the jump \(F(x) - F(x^-)\), which is a nonnegative real number since \(F\) is nondecreasing.

theorem measure_singleton_eq_cdf_sub_leftLim
    (μ : Measure ℝ) [IsProbabilityMeasure μ] (x : ℝ) :
    μ {x} = ENNReal.ofReal (cdf μ x - Function.leftLim (cdf μ) x)

Used by 1

Used byThe cdf is continuous exactly at the non-atoms

TheoremThe cdf is continuous exactly at the non-atoms#✓fully proved

Let \(\mu\) be a probability measure on \(\mathbb{R}\) with cumulative distribution function \(F(y) = \mu((-\infty, y])\). For every \(x \in \mathbb{R}\), \(F\) is continuous at \(x\) if and only if \(\mu(\{x\}) = 0\).

theorem continuousAt_cdf_iff_measure_singleton_eq_zero
    (μ : Measure ℝ) [IsProbabilityMeasure μ] (x : ℝ) :
    ContinuousAt (cdf μ) x ↔ μ {x} = 0

Uses 1 · Used by 1

Proof usesAtoms are the jumps of the cdf

Used byNo atom at a continuity point of the cdf

TheoremNo atom at a continuity point of the cdf#✓fully proved

Let \(\mu\) be a probability measure on \(\mathbb{R}\) with cumulative distribution function \(F(y) = \mu((-\infty, y])\). If \(F\) is continuous at a point \(x \in \mathbb{R}\), then \(\mu(\{x\}) = 0\).

theorem cdf_continuousAt_singleton_null
    (μ : Measure ℝ) [IsProbabilityMeasure μ] (x : ℝ) (hx : ContinuousAt (cdf μ) x) :
    μ {x} = 0

Uses 1 · Used by 1

Proof usesThe cdf is continuous exactly at the non-atoms

Used byContinuity points of the cdf have null boundary

TheoremContinuity points of the cdf have null boundary#✓fully proved

Let \(\mu\) be a probability measure on \(\mathbb{R}\) with cumulative distribution function \(F(y) = \mu((-\infty, y])\). If \(F\) is continuous at a point \(x \in \mathbb{R}\), then the boundary of the half-line \((-\infty, x]\), which is \(\{x\}\), has \(\mu\)-measure zero.

theorem cdf_continuousAt_frontier_Iic_null
    (μ : Measure ℝ) [IsProbabilityMeasure μ] (x : ℝ) (hx : ContinuousAt (cdf μ) x) :
    μ (frontier (Iic x)) = 0

Uses 1

Proof usesNo atom at a continuity point of the cdf

TheoremMass of a half-open interval via the cdf#✓fully proved

Let \(\mu\) be a probability measure on \(\mathbb{R}\) with cumulative distribution function \(F(y) = \mu((-\infty, y])\). For all \(a, b \in \mathbb{R}\), the measure \(\mu((a, b])\) equals \(\max(F(b) - F(a), 0)\), as an extended nonnegative real.

theorem measure_Ioc_eq_ofReal_cdf
    (μ : Measure ℝ) [IsProbabilityMeasure μ] (a b : ℝ) :
    μ (Ioc a b) = ENNReal.ofReal (cdf μ b - cdf μ a)

TheoremThe continuity points of the cdf are dense#✓fully proved

Let \(\mu\) be a probability measure on \(\mathbb{R}\) with cumulative distribution function \(F(y) = \mu((-\infty, y])\). The set of points \(x \in \mathbb{R}\) at which \(F\) is continuous is dense in \(\mathbb{R}\).

This follows from the fact that a monotone function has only countably many discontinuities.

theorem dense_cdf_continuityPoints (μ : Measure ℝ) [IsProbabilityMeasure μ] :
    Dense {x : ℝ | ContinuousAt (cdf μ) x}

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.