mathlib3

00abe069 - feat(probability/kernel/cond_distrib): regular conditional probability distributions (#19090)

feat(probability/kernel/cond_distrib): regular conditional probability distributions (#19090) We define the regular conditional probability distribution `cond_distrib Y X μ` of `Y : α → Ω` given `X : α → β`, where `Ω` is a standard Borel space. This is a `kernel β Ω` such that for almost all `a`, for all measurable set `s`, `cond_distrib Y X μ (X a) s` is equal to the conditional expectation `μ⟦Y ⁻¹' s | mβ.comap X⟧` evaluated at `a`. Also define the above notation for the conditional expectation of the indicator of a set. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>