# Documentation

Mathlib.Probability.Kernel.CondCdf

# Conditional cumulative distribution function #

Given ρ : measure (α × ℝ), we define the conditional cumulative distribution function (conditional cdf) of ρ. It is a function cond_cdf ρ : α → ℝ → ℝ such that if ρ is a finite measure, then for all a : α cond_cdf ρ a is monotone and right-continuous with limit 0 at -∞ and limit 1 at +∞, and such that for all x : ℝ, a ↦ cond_cdf ρ a x is measurable. For all x : ℝ and measurable set s, that function satisfies ∫⁻ a in s, ennreal.of_real (cond_cdf ρ a x) ∂ρ.fst = ρ (s ×ˢ Iic x).

## Main definitions #

• probability_theory.cond_cdf ρ : α → stieltjes_function: the conditional cdf of ρ : measure (α × ℝ). A stieltjes_function is a function ℝ → ℝ which is monotone and right-continuous.

## Main statements #

• probability_theory.set_lintegral_cond_cdf: for all a : α and x : ℝ, all measurable set s, ∫⁻ a in s, ennreal.of_real (cond_cdf ρ a x) ∂ρ.fst = ρ (s ×ˢ Iic x).

The construction of the conditional cdf in this file follows the proof of Theorem 3.4 in [O. Kallenberg, Foundations of modern probability][kallenberg2021].

## TODO #

• The conditional cdf can be used to define the cdf of a real measure by using the conditional cdf of (measure.dirac unit.star).prod μ : measure (unit × ℝ).