Cumulative distribution functions

This file records basic properties of cumulative distribution functions. In particular, the cdf of an atomless real probability measure is continuous.

A probability measure μ on ℕ becomes a real law by pushing it forward along the cast ℕ → ℝ. The resulting cumulative distribution function is determined by the cumulative masses of μ itself: it vanishes below the origin, where the pushforward has no mass at all, and at a nonnegative point x it is the mass μ gives to the initial segment below the natural floor of x. Every discrete law on ℕ therefore reads its real cdf off its own cumulative masses.

Main results

• MeasureTheory.Measure.continuous_cdf_of_noAtoms proves continuity for atomless real laws;
• MeasureTheory.Measure.cdf_sublevel_measure evaluates the measure of a CDF sublevel set for an atomless real law;
• MeasureTheory.Measure.cdf_map_natCast evaluates the cdf at a nonnegative point;
• MeasureTheory.Measure.cdf_map_natCast_of_neg evaluates it below the origin.

Adapted from

continuous_cdf_of_noAtoms and cdf_sublevel_measure are adapted from Cameron Freer's independent implementation in Graphon/MeasureIso.lean at commit 9f7be59fa754d260a544b4cfd83d6a5b94f7552e: https://github.com/cameronfreer/graphon/commit/9f7be59fa754d260a544b4cfd83d6a5b94f7552e, under the same names; the graphon-specific packaging was removed. The original work is copyright Cameron Freer and licensed under Apache 2.0.

These two results are the input to the probability integral transform MeasureTheory.Measure.cdf_map_eq_volume_restrict in TauCeti.Probability.Quantile, which is adapted from the same source, and they realize the measure-preserving equivalence of an atomless standard-Borel space with 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).

theorem MeasureTheory.Measure.cdf_map_natCast (μ : Measure ℕ) [IsProbabilityMeasure μ] {x : ℝ} (hx : 0 ≤ x) : ↑(ProbabilityTheory.cdf (map Nat.cast μ)) x = μ.real (Set.Iic ⌊x⌋₊)

At a nonnegative point, the cdf of a natural-valued law cast to the reals is the cumulative mass of the initial segment below the natural floor of that point.

theorem MeasureTheory.Measure.cdf_map_natCast_of_neg (μ : Measure ℕ) [IsProbabilityMeasure μ] {x : ℝ} (hx : x < 0) : ↑(ProbabilityTheory.cdf (map Nat.cast μ)) x = 0

Below the origin, the cdf of a natural-valued law cast to the reals vanishes: the law is carried by the natural numbers.

theorem MeasureTheory.Measure.continuous_cdf_of_noAtoms (ν : Measure ℝ) [IsProbabilityMeasure ν] [NullSingletonClass ν] : Continuous ↑(ProbabilityTheory.cdf ν)

CDF continuity from null singletons. The cumulative distribution function of a probability measure on ℝ is continuous when every singleton has measure zero.

theorem MeasureTheory.Measure.measureReal_Ioc_eq_cdf_sub (ν : Measure ℝ) [IsProbabilityMeasure ν] {a b : ℝ} (hab : a ≤ b) : ν.real (Set.Ioc a b) = ↑(ProbabilityTheory.cdf ν) b - ↑(ProbabilityTheory.cdf ν) a

The mass of a bounded interval Ioc a b is the increment of the cumulative distribution function between its endpoints.

theorem MeasureTheory.Measure.cdf_sublevel_measure (ν : Measure ℝ) [IsProbabilityMeasure ν] [NullSingletonClass ν] (y : ℝ) (hy1 : y < 1) : ν {x : ℝ | ↑(ProbabilityTheory.cdf ν) x ≤ y} = ENNReal.ofReal y

The measure of the sublevel set {x | cdf ν x ≤ y} is ENNReal.ofReal y when y < 1.