Bochner integration against mixtures

The Bochner integral against Measure.bind is the iterated integral against its components. Integrability is characterized by almost-everywhere component integrability and integrability of the component absolute moments. The second-moment version supports covariance calculations for probability mixtures. The real mass of a measurable set is the integral of its component real masses when those component masses are finite almost everywhere.

These results use Mathlib's integration theory for kernel composition, with the mixing measure viewed as a constant kernel. No finiteness assumptions on the measures are needed.

theorem MeasureTheory.Measure.integrable_bind_iff {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : Measure α} {K : α → Measure β} {f : β → E} (hK : Measurable K) (hf : AEStronglyMeasurable f (μ.bind K)) : Integrable f (μ.bind K) ↔ (∀ᵐ (a : α) ∂μ, Integrable f (K a)) ∧ Integrable (fun (a : α) => ∫ (x : β), ‖f x‖ ∂K a) μ

Integrability against a mixture is equivalent to component integrability almost everywhere and integrability of the component absolute moments.

theorem MeasureTheory.Measure.integral_bind {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : Measure α} {K : α → Measure β} {f : β → E} [NormedSpace ℝ E] (hK : AEMeasurable K μ) (hf : Integrable f (μ.bind K)) : ∫ (x : β), f x ∂μ.bind K = ∫ (a : α), ∫ (x : β), f x ∂K a ∂μ

The integral against an almost-everywhere measurable mixture equals the iterated component integral.

theorem MeasureTheory.Measure.bind_apply_real {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {K : α → Measure β} (hK : AEMeasurable K μ) {s : Set β} (hs : MeasurableSet s) (hKs : ∀ᵐ (a : α) ∂μ, (K a) s ≠ ⊤) : (μ.bind K).real s = ∫ (a : α), (K a).real s ∂μ

The real mass of a measurable set under a mixture is the integral of its component real masses. Only finiteness on the set is required of each component.

theorem MeasureTheory.Measure.integrable_integral_bind {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : Measure α} {K : α → Measure β} {f : β → E} [NormedSpace ℝ E] (hK : Measurable K) (hf : Integrable f (μ.bind K)) : Integrable (fun (a : α) => ∫ (x : β), f x ∂K a) μ

Component expectations of an integrable observable are integrable under the mixing law.

theorem MeasureTheory.Measure.memLp_two_bind_iff {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : Measure α} {K : α → Measure β} {f : β → E} (hK : Measurable K) (hf : AEStronglyMeasurable f (μ.bind K)) : MemLp f 2 (μ.bind K) ↔ (∀ᵐ (a : α) ∂μ, MemLp f 2 (K a)) ∧ Integrable (fun (a : α) => ∫ (x : β), ‖f x‖ ^ 2 ∂K a) μ

A mixture has a finite second moment exactly when its components do almost everywhere and their second moments are integrable under the mixing law.