mathlib3

3b92d54a - chore(probability/kernel/composition): redefine kernel.comp using measure.bind, remove kernel.map_measure (#19160)

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. Co-authored-by: RemyDegenne <remydegenne@gmail.com>