Mixtures of measures

This file identifies a mixture of jointly measurable densities with the measure whose density is their pointwise integral. The result allows s-finite mixing and reference measures, so it applies to probability mixtures and unnormalised integral representations.

Main results

• MeasureTheory.Measure.bind_withDensity writes a mixture of withDensity measures as a single withDensity measure.
• MeasureTheory.Measure.bind_eq_withDensity_of_ae_eq allows the component-density presentation to hold only almost everywhere with respect to the mixing measure.
• MeasureTheory.Measure.rnDeriv_bind_withDensity identifies the Radon--Nikodym derivative of a mixture of densities.

theorem MeasureTheory.Measure.bind_withDensity {A : Type u_1} {B : Type u_2} [MeasurableSpace A] [MeasurableSpace B] (rho : Measure A) (nu : Measure B) [SFinite rho] [SFinite nu] {f : A → B → ENNReal} (hf : Measurable (Function.uncurry f)) : (rho.bind fun (a : A) => nu.withDensity (f a)) = nu.withDensity fun (b : B) => ∫⁻ (a : A), f a b ∂rho

A mixture of measures with jointly measurable densities has density equal to the pointwise integral of the component densities.

theorem MeasureTheory.Measure.bind_eq_withDensity_of_ae_eq {A : Type u_1} {B : Type u_2} [MeasurableSpace A] [MeasurableSpace B] (rho : Measure A) (nu : Measure B) [SFinite rho] [SFinite nu] {K : A → Measure B} {f : A → B → ENNReal} (hf : Measurable (Function.uncurry f)) (hKf : K =ᵐ[rho] fun (a : A) => nu.withDensity (f a)) : rho.bind K = nu.withDensity fun (b : B) => ∫⁻ (a : A), f a b ∂rho

If almost every component of a measurable family has a density with respect to the same reference measure, then its mixture has the integrated density.

theorem MeasureTheory.Measure.rnDeriv_bind_withDensity {A : Type u_1} {B : Type u_2} [MeasurableSpace A] [MeasurableSpace B] {rho : Measure A} {nu : Measure B} {K : A → Measure B} {f : A → B → ENNReal} [SFinite rho] [SigmaFinite nu] (hf : Measurable (Function.uncurry f)) (hKf : K =ᵐ[rho] fun (a : A) => nu.withDensity (f a)) : (rho.bind K).rnDeriv nu =ᵐ[nu] fun (b : B) => ∫⁻ (a : A), f a b ∂rho

The Radon--Nikodym derivative of a mixture of densities is the pointwise integral of the component densities.