mathlib

20d57630 - feat(probability/kernel/cond_cdf): conditional cumulative distribution function (#18988)

feat(probability/kernel/cond_cdf): conditional cumulative distribution function (#18988) We define `cond_cdf ρ : α → stieltjes_function`, the conditional cdf of `ρ : measure (α × ℝ)`, and prove its main properties: it is monotone and right-continuous with limit 0 at -∞ and limit 1 at +∞; for all `x : ℝ`, `a ↦ cond_cdf ρ a x` is measurable; for all `x : ℝ` and measurable set `s`, it satisfies `∫⁻ a in s, ennreal.of_real (cond_cdf ρ a x) ∂ρ.fst = ρ (s ×ˢ Iic x)`