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 #

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 #


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.

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).

Instances For

    The cdf is non-negative.

    The cdf is lower or equal to 1.

    The cdf tends to 0 at -∞.

    The cdf tends to 1 at +∞.

    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.