English
CDF of a real-valued measure on ℝ is defined as the distribution function; for probability measures, F(x) = μ((−∞, x]).
Русский
CDF меры на ℝ — это функция распределения; для вероятностной меры F(x) = μ((−∞, x]).
LaTeX
$$$$\text{CDF: } \mathsf{cdf}(\mu): \mathbb{R} \to \text{StieltjesFunction}, \quad F(x)=\mu((-\infty,x])\text{ for probability measures } \mu.$$$$
Lean4
/-- Cumulative distribution function of a real measure. The definition currently makes sense only
for probability measures. In that case, it satisfies `cdf μ x = μ.real (Iic x)` (see
`ProbabilityTheory.cdf_eq_real`). -/
noncomputable def cdf (μ : Measure ℝ) : StieltjesFunction :=
condCDF ((dirac Unit.unit).prod μ) Unit.unit
