Integrating against measurable families of measures

A measurable family of measures need not be an s-finite kernel. When its slices have finite mass almost everywhere for an outer measure, integrating a jointly measurable function gives an almost everywhere measurable function of the parameter. The Bochner version applies to jointly strongly measurable functions with values in any normed real vector space.

The outer measure is arbitrary, and the finite-mass hypothesis is only almost everywhere: exceptional slices may have infinite mass. In particular, no uniform mass bound or integrability of the total mass is required. These results apply to spatial integrals of measure-valued curves without requiring a continuity equation.

Main results

• Measurable.aemeasurable_lintegral_measure: measurability of nonnegative integrals against a measurable family with almost everywhere finite slices.
• MeasureTheory.StronglyMeasurable.aestronglyMeasurable_integral_measure: strong measurability of Bochner integrals against such a family.

theorem Measurable.aemeasurable_lintegral_measure {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : α → MeasureTheory.Measure β} {ν : MeasureTheory.Measure α} {f : α → β → ENNReal} (hf : Measurable (Function.uncurry f)) (hμ : Measurable μ) (hμfin : ∀ᵐ (a : α) ∂ν, (μ a) Set.univ ≠ ⊤) : AEMeasurable (fun (a : α) => ∫⁻ (x : β), f a x ∂μ a) ν

Integrating a jointly measurable nonnegative function against a measurable family of measures with almost everywhere finite slices gives an almost everywhere measurable function.

theorem MeasureTheory.StronglyMeasurable.aestronglyMeasurable_integral_measure {α : Type u_1} {β : Type u_2} {F : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : α → Measure β} {ν : Measure α} {f : α → β → F} (hf : StronglyMeasurable (Function.uncurry f)) (hμ : Measurable μ) (hμfin : ∀ᵐ (a : α) ∂ν, (μ a) Set.univ ≠ ⊤) : AEStronglyMeasurable (fun (a : α) => ∫ (x : β), f a x ∂μ a) ν

Integrating a jointly strongly measurable function against a measurable family of measures with almost everywhere finite slices gives an almost everywhere strongly measurable function. The codomain needs no measurable-space, separability or completeness assumptions.