Commit 2023-05-31 12:41 00abe069

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.