mathlib3

28b2a92f - feat(probability/kernel/measurable_integral): the integral against a kernel is strongly measurable (#18974)

feat(probability/kernel/measurable_integral): the integral against a kernel is strongly measurable (#18974) We also rename the measurability lemmas to use the same convention as in the file measure_theory/constructions/prod, which contains very similar lemmas for the integral against a measure (a particular case of what we are proving here).