mathlib

56f4cd1e - feat(measure_theory/kernel/basic): define kernels and classes of kernels (Markov, finite, s-finite) (#17976)

feat(measure_theory/kernel/basic): define kernels and classes of kernels (Markov, finite, s-finite) (#17976) We define kernels between measurable spaces as the `add_submonoid` of measurable functions `α → measure β`. That is, a kernel `κ` verifies that for all measurable sets `s` of `β`, `λ a, κ a s` is measurable. A kernel is said to be Markov if all measures its image are probability measures, finite if all measures are finite with a common bound, and s-finite if it can be written as a countable sum of finite kernels.