# 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α : } {mβ : } [] [] {κ : (ProbabilityTheory.kernel α (β × Ω))} (a : α) {s : Set (β × Ω)} (hs : ) :
∫⁻ (x : β), ( (a, x)) {y : Ω | (x, y) s} = (κ a) s
theorem ProbabilityTheory.set_lintegral_condKernel_eq_measure_prod {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] {κ : (ProbabilityTheory.kernel α (β × Ω))} (a : α) {s : Set β} (hs : ) {t : Set Ω} (ht : ) :
∫⁻ (b : β) in s, ( (a, b)) t = (κ a) (s ×ˢ t)
theorem ProbabilityTheory.lintegral_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] {κ : (ProbabilityTheory.kernel α (β × Ω))} {f : β × ΩENNReal} (hf : ) (a : α) :
∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) (a, b) = ∫⁻ (x : β × Ω), f xκ a
theorem ProbabilityTheory.set_lintegral_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] {κ : (ProbabilityTheory.kernel α (β × Ω))} {f : β × ΩENNReal} (hf : ) (a : α) {s : Set β} (hs : ) {t : Set Ω} (ht : ) :
∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) (a, b) = ∫⁻ (x : β × Ω) in s ×ˢ t, f xκ a
theorem ProbabilityTheory.set_lintegral_condKernel_univ_right {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] {κ : (ProbabilityTheory.kernel α (β × Ω))} {f : β × ΩENNReal} (hf : ) (a : α) {s : Set β} (hs : ) :
∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) (a, b) = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f xκ a
theorem ProbabilityTheory.set_lintegral_condKernel_univ_left {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] {κ : (ProbabilityTheory.kernel α (β × Ω))} {f : β × ΩENNReal} (hf : ) (a : α) {t : Set Ω} (ht : ) :
∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) (a, b) = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f xκ a
theorem MeasureTheory.AEStronglyMeasurable.integral_kernel_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] {κ : (ProbabilityTheory.kernel α (β × Ω))} {E : Type u_4} {f : β × ΩE} [] (a : α) (hf : ) :
MeasureTheory.AEStronglyMeasurable (fun (x : β) => ∫ (y : Ω), f (x, y) (a, x)) ()
theorem ProbabilityTheory.integral_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] {κ : (ProbabilityTheory.kernel α (β × Ω))} {E : Type u_4} {f : β × ΩE} [] (a : α) (hf : MeasureTheory.Integrable f (κ a)) :
∫ (b : β), ∫ (ω : Ω), f (b, ω) (a, b) = ∫ (x : β × Ω), f xκ a
theorem ProbabilityTheory.setIntegral_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] {κ : (ProbabilityTheory.kernel α (β × Ω))} {E : Type u_4} {f : β × ΩE} [] (a : α) {s : Set β} (hs : ) {t : Set Ω} (ht : ) (hf : MeasureTheory.IntegrableOn f (s ×ˢ t) (κ a)) :
∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) (a, b) = ∫ (x : β × Ω) in s ×ˢ t, f xκ a
@[deprecated ProbabilityTheory.setIntegral_condKernel]
theorem ProbabilityTheory.set_integral_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] {κ : (ProbabilityTheory.kernel α (β × Ω))} {E : Type u_4} {f : β × ΩE} [] (a : α) {s : Set β} (hs : ) {t : Set Ω} (ht : ) (hf : MeasureTheory.IntegrableOn f (s ×ˢ t) (κ a)) :
∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) (a, b) = ∫ (x : β × Ω) in s ×ˢ t, f xκ a

Alias of ProbabilityTheory.setIntegral_condKernel.

theorem ProbabilityTheory.setIntegral_condKernel_univ_right {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] {κ : (ProbabilityTheory.kernel α (β × Ω))} {E : Type u_4} {f : β × ΩE} [] (a : α) {s : Set β} (hs : ) (hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) (κ a)) :
∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) (a, b) = ∫ (x : β × Ω) in s ×ˢ Set.univ, f xκ a
@[deprecated ProbabilityTheory.setIntegral_condKernel_univ_right]
theorem ProbabilityTheory.set_integral_condKernel_univ_right {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] {κ : (ProbabilityTheory.kernel α (β × Ω))} {E : Type u_4} {f : β × ΩE} [] (a : α) {s : Set β} (hs : ) (hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) (κ a)) :
∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) (a, b) = ∫ (x : β × Ω) in s ×ˢ Set.univ, f xκ a

Alias of ProbabilityTheory.setIntegral_condKernel_univ_right.

theorem ProbabilityTheory.setIntegral_condKernel_univ_left {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] {κ : (ProbabilityTheory.kernel α (β × Ω))} {E : Type u_4} {f : β × ΩE} [] (a : α) {t : Set Ω} (ht : ) (hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) (κ a)) :
∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) (a, b) = ∫ (x : β × Ω) in Set.univ ×ˢ t, f xκ a
@[deprecated ProbabilityTheory.setIntegral_condKernel_univ_left]
theorem ProbabilityTheory.set_integral_condKernel_univ_left {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] {κ : (ProbabilityTheory.kernel α (β × Ω))} {E : Type u_4} {f : β × ΩE} [] (a : α) {t : Set Ω} (ht : ) (hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) (κ a)) :
∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) (a, b) = ∫ (x : β × Ω) in Set.univ ×ˢ t, f xκ a

Alias of ProbabilityTheory.setIntegral_condKernel_univ_left.

theorem MeasureTheory.Measure.lintegral_condKernel_mem {β : Type u_2} {Ω : Type u_3} {mβ : } [] [] {ρ : MeasureTheory.Measure (β × Ω)} {s : Set (β × Ω)} (hs : ) :
∫⁻ (x : β), (ρ.condKernel x) {y : Ω | (x, y) s}ρ.fst = ρ s
theorem MeasureTheory.Measure.set_lintegral_condKernel_eq_measure_prod {β : Type u_2} {Ω : Type u_3} {mβ : } [] [] {ρ : MeasureTheory.Measure (β × Ω)} {s : Set β} (hs : ) {t : Set Ω} (ht : ) :
∫⁻ (b : β) in s, (ρ.condKernel b) tρ.fst = ρ (s ×ˢ t)
theorem MeasureTheory.Measure.lintegral_condKernel {β : Type u_2} {Ω : Type u_3} {mβ : } [] [] {ρ : MeasureTheory.Measure (β × Ω)} {f : β × ΩENNReal} (hf : ) :
∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω)ρ.condKernel bρ.fst = ∫⁻ (x : β × Ω), f xρ
theorem MeasureTheory.Measure.set_lintegral_condKernel {β : Type u_2} {Ω : Type u_3} {mβ : } [] [] {ρ : MeasureTheory.Measure (β × Ω)} {f : β × ΩENNReal} (hf : ) {s : Set β} (hs : ) {t : Set Ω} (ht : ) :
∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω)ρ.condKernel bρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ t, f xρ
theorem MeasureTheory.Measure.set_lintegral_condKernel_univ_right {β : Type u_2} {Ω : Type u_3} {mβ : } [] [] {ρ : MeasureTheory.Measure (β × Ω)} {f : β × ΩENNReal} (hf : ) {s : Set β} (hs : ) :
∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω)ρ.condKernel bρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f xρ
theorem MeasureTheory.Measure.set_lintegral_condKernel_univ_left {β : Type u_2} {Ω : Type u_3} {mβ : } [] [] {ρ : MeasureTheory.Measure (β × Ω)} {f : β × ΩENNReal} (hf : ) {t : Set Ω} (ht : ) :
∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω)ρ.condKernel bρ.fst = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f xρ
theorem MeasureTheory.AEStronglyMeasurable.integral_condKernel {β : Type u_2} {Ω : Type u_3} {mβ : } [] [] {ρ : MeasureTheory.Measure (β × Ω)} {E : Type u_4} {f : β × ΩE} [] (hf : ) :
MeasureTheory.AEStronglyMeasurable (fun (x : β) => ∫ (y : Ω), f (x, y)ρ.condKernel x) ρ.fst
theorem MeasureTheory.Measure.integral_condKernel {β : Type u_2} {Ω : Type u_3} {mβ : } [] [] {ρ : MeasureTheory.Measure (β × Ω)} {E : Type u_4} {f : β × ΩE} [] (hf : ) :
∫ (b : β), ∫ (ω : Ω), f (b, ω)ρ.condKernel bρ.fst = ∫ (x : β × Ω), f xρ
theorem MeasureTheory.Measure.setIntegral_condKernel {β : Type u_2} {Ω : Type u_3} {mβ : } [] [] {ρ : MeasureTheory.Measure (β × Ω)} {E : Type u_4} {f : β × ΩE} [] {s : Set β} (hs : ) {t : Set Ω} (ht : ) (hf : MeasureTheory.IntegrableOn f (s ×ˢ t) ρ) :
∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω)ρ.condKernel bρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f xρ
@[deprecated MeasureTheory.Measure.setIntegral_condKernel]
theorem MeasureTheory.Measure.set_integral_condKernel {β : Type u_2} {Ω : Type u_3} {mβ : } [] [] {ρ : MeasureTheory.Measure (β × Ω)} {E : Type u_4} {f : β × ΩE} [] {s : Set β} (hs : ) {t : Set Ω} (ht : ) (hf : MeasureTheory.IntegrableOn f (s ×ˢ t) ρ) :
∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω)ρ.condKernel bρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f xρ

Alias of MeasureTheory.Measure.setIntegral_condKernel.

theorem MeasureTheory.Measure.setIntegral_condKernel_univ_right {β : Type u_2} {Ω : Type u_3} {mβ : } [] [] {ρ : MeasureTheory.Measure (β × Ω)} {E : Type u_4} {f : β × ΩE} [] {s : Set β} (hs : ) (hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ρ) :
∫ (b : β) in s, ∫ (ω : Ω), f (b, ω)ρ.condKernel bρ.fst = ∫ (x : β × Ω) in s ×ˢ Set.univ, f xρ
@[deprecated MeasureTheory.Measure.setIntegral_condKernel_univ_right]
theorem MeasureTheory.Measure.set_integral_condKernel_univ_right {β : Type u_2} {Ω : Type u_3} {mβ : } [] [] {ρ : MeasureTheory.Measure (β × Ω)} {E : Type u_4} {f : β × ΩE} [] {s : Set β} (hs : ) (hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ρ) :
∫ (b : β) in s, ∫ (ω : Ω), f (b, ω)ρ.condKernel bρ.fst = ∫ (x : β × Ω) in s ×ˢ Set.univ, f xρ

Alias of MeasureTheory.Measure.setIntegral_condKernel_univ_right.

theorem MeasureTheory.Measure.setIntegral_condKernel_univ_left {β : Type u_2} {Ω : Type u_3} {mβ : } [] [] {ρ : MeasureTheory.Measure (β × Ω)} {E : Type u_4} {f : β × ΩE} [] {t : Set Ω} (ht : ) (hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ρ) :
∫ (b : β), ∫ (ω : Ω) in t, f (b, ω)ρ.condKernel bρ.fst = ∫ (x : β × Ω) in Set.univ ×ˢ t, f xρ
@[deprecated MeasureTheory.Measure.setIntegral_condKernel_univ_left]
theorem MeasureTheory.Measure.set_integral_condKernel_univ_left {β : Type u_2} {Ω : Type u_3} {mβ : } [] [] {ρ : MeasureTheory.Measure (β × Ω)} {E : Type u_4} {f : β × ΩE} [] {t : Set Ω} (ht : ) (hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ρ) :
∫ (b : β), ∫ (ω : Ω) in t, f (b, ω)ρ.condKernel bρ.fst = ∫ (x : β × Ω) in Set.univ ×ˢ t, f xρ

Alias of MeasureTheory.Measure.setIntegral_condKernel_univ_left.

### 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α : } [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩF} (hf : ) :
(∀ᵐ (a : α) ∂ρ.fst, MeasureTheory.Integrable (fun (ω : Ω) => f (a, ω)) (ρ.condKernel a)) MeasureTheory.Integrable (fun (a : α) => ∫ (ω : Ω), f (a, ω)ρ.condKernel a) ρ.fst
theorem MeasureTheory.Integrable.condKernel_ae {α : Type u_1} {Ω : Type u_2} {F : Type u_4} {mα : } [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩF} (hf_int : ) :
∀ᵐ (a : α) ∂ρ.fst, MeasureTheory.Integrable (fun (ω : Ω) => f (a, ω)) (ρ.condKernel a)
theorem MeasureTheory.Integrable.integral_norm_condKernel {α : Type u_1} {Ω : Type u_2} {F : Type u_4} {mα : } [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩF} (hf_int : ) :
MeasureTheory.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α : } [] [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩE} (hf_int : ) :
MeasureTheory.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α : } [] [] [] {ρ : MeasureTheory.Measure (α × Ω)} {f : α × ΩE} (hf_int : ) :
MeasureTheory.Integrable (fun (x : α) => ∫ (y : Ω), f (x, y)ρ.condKernel x) ρ.fst