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

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 is monotone.

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.

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