# Cumulative distribution function of a real probability measure #

The cumulative distribution function (cdf) of a probability measure over ℝ is a monotone, right continuous function with limit 0 at -∞ and 1 at +∞, such that cdf μ x = μ (Iic x) for all x : ℝ. Two probability measures are equal if and only if they have the same cdf.

## Main definitions #

• ProbabilityTheory.cdf μ: cumulative distribution function of μ : Measure ℝ, defined as the conditional cdf (ProbabilityTheory.condCDF) of the product measure (Measure.dirac Unit.unit).prod μ evaluated at Unit.unit.

The definition could be replaced by the more elementary cdf μ x = (μ (Iic x)).toReal, but using condCDF gives us access to its API, from which most properties of the cdf follow directly.

## Main statements #

• ProbabilityTheory.ofReal_cdf: for a probability measure μ and x : ℝ, ENNReal.ofReal (cdf μ x) = μ (Iic x).
• MeasureTheory.Measure.ext_of_cdf: two probability measures are equal if and only if they have the same cdf.

## TODO #

The definition could be extended to a finite measure by rescaling condCDF, but it would be nice to have more structure on Stieltjes functions first. Right now, if f is a Stieltjes function, 2 • f makes no sense. We could define Stieltjes functions as a submodule.

The definition could be extended to ℝⁿ, either by extending the definition of condCDF, or by using another construction here.

noncomputable def ProbabilityTheory.cdf (μ : ) :

Cumulative distribution function of a real measure. The definition currently makes sense only for probability measures. In that case, it satisfies cdf μ x = (μ (Iic x)).toReal (see ProbabilityTheory.cdf_eq_toReal).

Equations
Instances For
theorem ProbabilityTheory.cdf_nonneg (μ : ) (x : ) :
0 x

The cdf is non-negative.

theorem ProbabilityTheory.cdf_le_one (μ : ) (x : ) :
x 1

The cdf is lower or equal to 1.

The cdf is monotone.

theorem ProbabilityTheory.tendsto_cdf_atBot (μ : ) :
Filter.Tendsto () Filter.atBot (nhds 0)

The cdf tends to 0 at -∞.

theorem ProbabilityTheory.tendsto_cdf_atTop (μ : ) :
Filter.Tendsto () Filter.atTop (nhds 1)

The cdf tends to 1 at +∞.

theorem ProbabilityTheory.ofReal_cdf (μ : ) (x : ) :
ENNReal.ofReal ( x) = μ ()
theorem ProbabilityTheory.cdf_eq_toReal (μ : ) (x : ) :
x = (μ ()).toReal
Equations
• =
theorem ProbabilityTheory.measure_cdf (μ : ) :
.measure = μ

The measure associated to the cdf of a probability measure is the same probability measure.

theorem ProbabilityTheory.cdf_measure_stieltjesFunction (f : StieltjesFunction) (hf0 : Filter.Tendsto (f) Filter.atBot (nhds 0)) (hf1 : Filter.Tendsto (f) Filter.atTop (nhds 1)) :

If two real probability distributions have the same cdf, they are equal.

@[simp]