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
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
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.
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
If two real probability distributions have the same cdf, they are equal.