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 (μ : MeasureTheory.Measure ℝ) : StieltjesFunction

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

• ProbabilityTheory.cdf μ = ProbabilityTheory.condCDF (MeasureTheory.Measure.prod (MeasureTheory.Measure.dirac ()) μ) ()

theorem ProbabilityTheory.cdf_nonneg (μ : MeasureTheory.Measure ℝ) (x : ℝ) : 0 ≤ ↑(ProbabilityTheory.cdf μ) x

The cdf is non-negative.

theorem ProbabilityTheory.cdf_le_one (μ : MeasureTheory.Measure ℝ) (x : ℝ) : ↑(ProbabilityTheory.cdf μ) x ≤ 1

The cdf is lower or equal to 1.

theorem ProbabilityTheory.monotone_cdf (μ : MeasureTheory.Measure ℝ) : Monotone ↑(ProbabilityTheory.cdf μ)

The cdf is monotone.

theorem ProbabilityTheory.tendsto_cdf_atBot (μ : MeasureTheory.Measure ℝ) : Filter.Tendsto (↑(ProbabilityTheory.cdf μ)) Filter.atBot (nhds 0)

The cdf tends to 0 at -∞.

theorem ProbabilityTheory.tendsto_cdf_atTop (μ : MeasureTheory.Measure ℝ) : Filter.Tendsto (↑(ProbabilityTheory.cdf μ)) Filter.atTop (nhds 1)

The cdf tends to 1 at +∞.

theorem ProbabilityTheory.ofReal_cdf (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (x : ℝ) : ENNReal.ofReal (↑(ProbabilityTheory.cdf μ) x) = ↑↑μ (Set.Iic x)

theorem ProbabilityTheory.cdf_eq_toReal (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (x : ℝ) : ↑(ProbabilityTheory.cdf μ) x = ENNReal.toReal (↑↑μ (Set.Iic x))

instance ProbabilityTheory.instIsProbabilityMeasurecdf (μ : MeasureTheory.Measure ℝ) : MeasureTheory.IsProbabilityMeasure (StieltjesFunction.measure (ProbabilityTheory.cdf μ))

Equations

• (_ : MeasureTheory.IsProbabilityMeasure (StieltjesFunction.measure (ProbabilityTheory.cdf μ))) = (_ : MeasureTheory.IsProbabilityMeasure (StieltjesFunction.measure (ProbabilityTheory.cdf μ)))

theorem ProbabilityTheory.measure_cdf (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] : StieltjesFunction.measure (ProbabilityTheory.cdf μ) = μ

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)) : ProbabilityTheory.cdf (StieltjesFunction.measure f) = f

theorem MeasureTheory.Measure.eq_of_cdf (μ : MeasureTheory.Measure ℝ) (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (h : ProbabilityTheory.cdf μ = ProbabilityTheory.cdf ν) : μ = ν

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

@[simp]

theorem MeasureTheory.Measure.cdf_eq_iff (μ : MeasureTheory.Measure ℝ) (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : ProbabilityTheory.cdf μ = ProbabilityTheory.cdf ν ↔ μ = ν