Commit 2023-05-31 12:41 00abe069
View on Github →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.