Lebesgue and Bochner integrals of conditional kernels

Integrals of ProbabilityTheory.Kernel.condKernel and MeasureTheory.Measure.condKernel.

Main statements

• ProbabilityTheory.setIntegral_condKernel: the integral ∫ b in s, ∫ ω in t, f (b, ω) ∂(Kernel.condKernel κ (a, b)) ∂(Kernel.fst κ a) is equal to ∫ x in s ×ˢ t, f x ∂(κ a).
• MeasureTheory.Measure.setIntegral_condKernel: ∫ b in s, ∫ ω in t, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst = ∫ x in s ×ˢ t, f x ∂ρ

Corresponding statements for the Lebesgue integral and/or without the sets s and t are also provided.

theorem ProbabilityTheory.lintegral_condKernel_mem {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated α β] {κ : Kernel α (β × Ω)} [IsFiniteKernel κ] (a : α) {s : Set (β × Ω)} (hs : MeasurableSet s) : ∫⁻ (x : β), (κ.condKernel (a, x)) {y : Ω | (x, y) ∈ s} ∂κ.fst a = (κ a) s

theorem ProbabilityTheory.setLIntegral_condKernel_eq_measure_prod {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated α β] {κ : Kernel α (β × Ω)} [IsFiniteKernel κ] (a : α) {s : Set β} (hs : MeasurableSet s) {t : Set Ω} (ht : MeasurableSet t) : ∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = (κ a) (s ×ˢ t)

theorem ProbabilityTheory.lintegral_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated α β] {κ : Kernel α (β × Ω)} [IsFiniteKernel κ] {f : β × Ω → ENNReal} (hf : Measurable f) (a : α) : ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω), f x ∂κ a

theorem ProbabilityTheory.setLIntegral_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated α β] {κ : Kernel α (β × Ω)} [IsFiniteKernel κ] {f : β × Ω → ENNReal} (hf : Measurable f) (a : α) {s : Set β} (hs : MeasurableSet s) {t : Set Ω} (ht : MeasurableSet t) : ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂κ a

theorem ProbabilityTheory.setLIntegral_condKernel_univ_right {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated α β] {κ : Kernel α (β × Ω)} [IsFiniteKernel κ] {f : β × Ω → ENNReal} (hf : Measurable f) (a : α) {s : Set β} (hs : MeasurableSet s) : ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ a

theorem ProbabilityTheory.setLIntegral_condKernel_univ_left {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated α β] {κ : Kernel α (β × Ω)} [IsFiniteKernel κ] {f : β × Ω → ENNReal} (hf : Measurable f) (a : α) {t : Set Ω} (ht : MeasurableSet t) : ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f x ∂κ a

theorem MeasureTheory.AEStronglyMeasurable.integral_kernel_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated α β] {κ : ProbabilityTheory.Kernel α (β × Ω)} [ProbabilityTheory.IsFiniteKernel κ] {E : Type u_4} {f : β × Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : α) (hf : AEStronglyMeasurable f (κ a)) : AEStronglyMeasurable (fun (x : β) => ∫ (y : Ω), f (x, y) ∂κ.condKernel (a, x)) (κ.fst a)

theorem ProbabilityTheory.integral_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated α β] {κ : Kernel α (β × Ω)} [IsFiniteKernel κ] {E : Type u_4} {f : β × Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : α) (hf : MeasureTheory.Integrable f (κ a)) : ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω), f x ∂κ a

theorem ProbabilityTheory.setIntegral_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated α β] {κ : Kernel α (β × Ω)} [IsFiniteKernel κ] {E : Type u_4} {f : β × Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : α) {s : Set β} (hs : MeasurableSet s) {t : Set Ω} (ht : MeasurableSet t) (hf : MeasureTheory.IntegrableOn f (s ×ˢ t) (κ a)) : ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in s ×ˢ t, f x ∂κ a

theorem ProbabilityTheory.setIntegral_condKernel_univ_right {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated α β] {κ : Kernel α (β × Ω)} [IsFiniteKernel κ] {E : Type u_4} {f : β × Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : α) {s : Set β} (hs : MeasurableSet s) (hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) (κ a)) : ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ a

theorem ProbabilityTheory.setIntegral_condKernel_univ_left {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated α β] {κ : Kernel α (β × Ω)} [IsFiniteKernel κ] {E : Type u_4} {f : β × Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : α) {t : Set Ω} (ht : MeasurableSet t) (hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) (κ a)) : ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂κ a

theorem MeasureTheory.Measure.lintegral_condKernel_mem {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] {s : Set (β × Ω)} (hs : MeasurableSet s) : ∫⁻ (x : β), (ρ.condKernel x) {y : Ω | (x, y) ∈ s} ∂ρ.fst = ρ s

theorem MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] {s : Set β} (hs : MeasurableSet s) {t : Set Ω} (ht : MeasurableSet t) : ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ρ (s ×ˢ t)

theorem MeasureTheory.Measure.lintegral_condKernel {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] {f : β × Ω → ENNReal} (hf : Measurable f) : ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω), f x ∂ρ

theorem MeasureTheory.Measure.setLIntegral_condKernel {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] {f : β × Ω → ENNReal} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) {t : Set Ω} (ht : MeasurableSet t) : ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ

theorem MeasureTheory.Measure.setLIntegral_condKernel_univ_right {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] {f : β × Ω → ENNReal} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) : ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ

theorem MeasureTheory.Measure.setLIntegral_condKernel_univ_left {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] {f : β × Ω → ENNReal} (hf : Measurable f) {t : Set Ω} (ht : MeasurableSet t) : ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ

theorem MeasureTheory.AEStronglyMeasurable.integral_condKernel {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] {E : Type u_3} {f : β × Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] (hf : AEStronglyMeasurable f ρ) : AEStronglyMeasurable (fun (x : β) => ∫ (y : Ω), f (x, y) ∂ρ.condKernel x) ρ.fst

theorem MeasureTheory.Measure.integral_condKernel {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] {E : Type u_3} {f : β × Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] (hf : Integrable f ρ) : ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ

theorem MeasureTheory.Measure.setIntegral_condKernel {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] {E : Type u_3} {f : β × Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set β} (hs : MeasurableSet s) {t : Set Ω} (ht : MeasurableSet t) (hf : IntegrableOn f (s ×ˢ t) ρ) : ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ

theorem MeasureTheory.Measure.setIntegral_condKernel_univ_right {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] {E : Type u_3} {f : β × Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set β} (hs : MeasurableSet s) (hf : IntegrableOn f (s ×ˢ Set.univ) ρ) : ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ

theorem MeasureTheory.Measure.setIntegral_condKernel_univ_left {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : Measure (β × Ω)} [IsFiniteMeasure ρ] {E : Type u_3} {f : β × Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] {t : Set Ω} (ht : MeasurableSet t) (hf : IntegrableOn f (Set.univ ×ˢ t) ρ) : ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ

Integrability

We place these lemmas in the MeasureTheory namespace to enable dot notation.

theorem MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff {α : Type u_1} {Ω : Type u_2} {F : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] {f : α × Ω → F} (hf : AEStronglyMeasurable f ρ) : (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun (ω : Ω) => f (a, ω)) (ρ.condKernel a)) ∧ Integrable (fun (a : α) => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔ Integrable f ρ

theorem MeasureTheory.Integrable.condKernel_ae {α : Type u_1} {Ω : Type u_2} {F : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] {f : α × Ω → F} (hf_int : Integrable f ρ) : ∀ᵐ (a : α) ∂ρ.fst, Integrable (fun (ω : Ω) => f (a, ω)) (ρ.condKernel a)

theorem MeasureTheory.Integrable.integral_norm_condKernel {α : Type u_1} {Ω : Type u_2} {F : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] {f : α × Ω → F} (hf_int : Integrable f ρ) : Integrable (fun (x : α) => ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst

theorem MeasureTheory.Integrable.norm_integral_condKernel {α : Type u_1} {Ω : Type u_2} {E : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup E] [NormedSpace ℝ E] {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] {f : α × Ω → E} (hf_int : Integrable f ρ) : Integrable (fun (x : α) => ‖∫ (y : Ω), f (x, y) ∂ρ.condKernel x‖) ρ.fst

theorem MeasureTheory.Integrable.integral_condKernel {α : Type u_1} {Ω : Type u_2} {E : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup E] [NormedSpace ℝ E] {ρ : Measure (α × Ω)} [IsFiniteMeasure ρ] {f : α × Ω → E} (hf_int : Integrable f ρ) : Integrable (fun (x : α) => ∫ (y : Ω), f (x, y) ∂ρ.condKernel x) ρ.fst