# mathlib3documentation

probability.kernel.integral_comp_prod

# Bochner integral of a function against the composition-product of two kernels #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We prove properties of the composition-product of two kernels. If κ is an s-finite kernel from α to β and η is an s-finite kernel from α × β to γ, we can form their composition-product κ ⊗ₖ η : kernel α (β × γ). We proved in probability.kernel.lintegral_comp_prod that it verifies ∫⁻ bc, f bc ∂((κ ⊗ₖ η) a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a). In this file, we prove the same equality for the Bochner integral.

## Main statements #

• probability_theory.integral_comp_prod: the integral against the composition-product is ∫ z, f z ∂((κ ⊗ₖ η) a) = ∫ x, ∫ y, f (x, y) ∂(η (a, x)) ∂(κ a)

## Implementation details #

This file is to a large extent a copy of part of measure_theory.constructions.prod. The product of two measures is a particular case of composition-product of kernels and it turns out that once the measurablity of the Lebesgue integral of a kernel is proved, almost all proofs about integrals against products of measures extend with minimal modifications to the composition-product of two kernels.

theorem probability_theory.has_finite_integral_prod_mk_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} (a : α) {s : set × γ)} (h2s : a) s ) :
measure_theory.has_finite_integral (λ (b : β), ((η (a, b)) (prod.mk b ⁻¹' s)).to_real) (κ a)
theorem probability_theory.integrable_kernel_prod_mk_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} (a : α) {s : set × γ)} (hs : measurable_set s) (h2s : a) s ) :
measure_theory.integrable (λ (b : β), ((η (a, b)) (prod.mk b ⁻¹' s)).to_real) (κ a)
theorem measure_theory.ae_strongly_measurable.integral_kernel_comp_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} [ E] ⦃f : β × γ E⦄  :
measure_theory.ae_strongly_measurable (λ (x : β), (y : γ), f (x, y) η (a, x)) (κ a)
theorem measure_theory.ae_strongly_measurable.comp_prod_mk_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} {δ : Type u_4} {f : β × γ δ}  :
∀ᵐ (x : β) κ a, measure_theory.ae_strongly_measurable (λ (y : γ), f (x, y)) (η (a, x))

### Integrability #

theorem probability_theory.has_finite_integral_comp_prod_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} ⦃f : β × γ E⦄  :
(∀ᵐ (x : β) κ a, measure_theory.has_finite_integral (λ (y : γ), f (x, y)) (η (a, x))) measure_theory.has_finite_integral (λ (x : β), (y : γ), f (x, y) η (a, x)) (κ a)
theorem probability_theory.has_finite_integral_comp_prod_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} ⦃f : β × γ E⦄ (h1f : a)) :
(∀ᵐ (x : β) κ a, measure_theory.has_finite_integral (λ (y : γ), f (x, y)) (η (a, x))) measure_theory.has_finite_integral (λ (x : β), (y : γ), f (x, y) η (a, x)) (κ a)
theorem probability_theory.integrable_comp_prod_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} ⦃f : β × γ E⦄  :
(∀ᵐ (x : β) κ a, measure_theory.integrable (λ (y : γ), f (x, y)) (η (a, x))) measure_theory.integrable (λ (x : β), (y : γ), f (x, y) η (a, x)) (κ a)
theorem measure_theory.integrable.comp_prod_mk_left_ae {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} ⦃f : β × γ E⦄ (hf : a)) :
∀ᵐ (x : β) κ a, measure_theory.integrable (λ (y : γ), f (x, y)) (η (a, x))
theorem measure_theory.integrable.integral_norm_comp_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} ⦃f : β × γ E⦄ (hf : a)) :
measure_theory.integrable (λ (x : β), (y : γ), f (x, y) η (a, x)) (κ a)
theorem measure_theory.integrable.integral_comp_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} [ E] ⦃f : β × γ E⦄ (hf : a)) :
measure_theory.integrable (λ (x : β), (y : γ), f (x, y) η (a, x)) (κ a)

### Bochner integral #

theorem probability_theory.kernel.integral_fn_integral_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} [ E] {E' : Type u_5} [complete_space E'] [ E'] ⦃f g : β × γ E⦄ (F : E E') (hf : a)) (hg : a)) :
(x : β), F ( (y : γ), f (x, y) + g (x, y) η (a, x)) κ a = (x : β), F ( (y : γ), f (x, y) η (a, x) + (y : γ), g (x, y) η (a, x)) κ a
theorem probability_theory.kernel.integral_fn_integral_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} [ E] {E' : Type u_5} [complete_space E'] [ E'] ⦃f g : β × γ E⦄ (F : E E') (hf : a)) (hg : a)) :
(x : β), F ( (y : γ), f (x, y) - g (x, y) η (a, x)) κ a = (x : β), F ( (y : γ), f (x, y) η (a, x) - (y : γ), g (x, y) η (a, x)) κ a
theorem probability_theory.kernel.lintegral_fn_integral_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} [ E] ⦃f g : β × γ E⦄ (F : E ennreal) (hf : a)) (hg : a)) :
∫⁻ (x : β), F ( (y : γ), f (x, y) - g (x, y) η (a, x)) κ a = ∫⁻ (x : β), F ( (y : γ), f (x, y) η (a, x) - (y : γ), g (x, y) η (a, x)) κ a
theorem probability_theory.kernel.integral_integral_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} [ E] ⦃f g : β × γ E⦄ (hf : a)) (hg : a)) :
(x : β), (y : γ), f (x, y) + g (x, y) η (a, x) κ a = (x : β), (y : γ), f (x, y) η (a, x) κ a + (x : β), (y : γ), g (x, y) η (a, x) κ a
theorem probability_theory.kernel.integral_integral_add' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} [ E] ⦃f g : β × γ E⦄ (hf : a)) (hg : a)) :
(x : β), (y : γ), (f + g) (x, y) η (a, x) κ a = (x : β), (y : γ), f (x, y) η (a, x) κ a + (x : β), (y : γ), g (x, y) η (a, x) κ a
theorem probability_theory.kernel.integral_integral_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} [ E] ⦃f g : β × γ E⦄ (hf : a)) (hg : a)) :
(x : β), (y : γ), f (x, y) - g (x, y) η (a, x) κ a = (x : β), (y : γ), f (x, y) η (a, x) κ a - (x : β), (y : γ), g (x, y) η (a, x) κ a
theorem probability_theory.kernel.integral_integral_sub' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} [ E] ⦃f g : β × γ E⦄ (hf : a)) (hg : a)) :
(x : β), (y : γ), (f - g) (x, y) η (a, x) κ a = (x : β), (y : γ), f (x, y) η (a, x) κ a - (x : β), (y : γ), g (x, y) η (a, x) κ a
theorem probability_theory.kernel.continuous_integral_integral {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} [ E]  :
continuous (λ (f : a))), (x : β), (y : γ), f (x, y) η (a, x) κ a)
theorem probability_theory.integral_comp_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} [ E] {f : β × γ E} (hf : a)) :
(z : β × γ), f z = (x : β), (y : γ), f (x, y) η (a, x) κ a
theorem probability_theory.set_integral_comp_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} [ E] {f : β × γ E} {s : set β} {t : set γ} (hs : measurable_set s) (ht : measurable_set t) (hf : (s ×ˢ t) a)) :
(z : β × γ) in s ×ˢ t, f z = (x : β) in s, (y : γ) in t, f (x, y) η (a, x) κ a
theorem probability_theory.set_integral_comp_prod_univ_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} [ E] (f : β × γ E) {s : set β} (hs : measurable_set s) (hf : a)) :
(z : β × γ) in , f z = (x : β) in s, (y : γ), f (x, y) η (a, x) κ a
theorem probability_theory.set_integral_comp_prod_univ_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {κ : } {η : (probability_theory.kernel × β) γ)} {a : α} [ E] (f : β × γ E) {t : set γ} (ht : measurable_set t) (hf : a)) :
(z : β × γ) in , f z = (x : β), (y : γ) in t, f (x, y) η (a, x) κ a