mathlib

2bb0d084 - feat(probability/kernel/basic): measurability of the integral against a kernel (#18061)

feat(probability/kernel/basic): measurability of the integral against a kernel (#18061) The main result is ```lean theorem measurable_lintegral (κ : kernel α β) [is_s_finite_kernel κ] {f : α → β → ℝ≥0∞} (hf : measurable (function.uncurry f)) : measurable (λ a, ∫⁻ b, f a b ∂(κ a)) ```