Measurability of the integral against a kernel #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
The Lebesgue integral of a measurable function against a kernel is measurable. The Bochner integral
is strongly measurable.
Main statements #
This is an auxiliary lemma for
For an s-finite kernel
κ and a function
f : α → β → ℝ≥0∞ which is measurable when seen as a
α × β (hypothesis
measurable (uncurry f)), the integral
a ↦ ∫⁻ b, f a b ∂(κ a) is