Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes