Commit 2023-06-07 11:35 3b92d54a
View on Github →chore(probability/kernel/composition): redefine kernel.comp using measure.bind, remove kernel.map_measure (#19160)
We replace the definition of kernel.comp
with a new one using measure.bind
: it removes the need for is_s_finite_kernel
hypotheses in the definition and most lemmas. When the kernels are s-finite, the new definition coincides with the old one.
We remove kernel.map_measure
because it is exactly the same as measure.bind
applied to a kernel.