mathlib3 documentation

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 #

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.

Integrability #

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 γ} [normed_add_comm_group E] {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {η : (probability_theory.kernel × β) γ)} [probability_theory.is_s_finite_kernel η] {a : α} ⦃f : β × γ E⦄ (hf : measure_theory.integrable f ((probability_theory.kernel.comp_prod κ η) 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 γ} [normed_add_comm_group E] {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {η : (probability_theory.kernel × β) γ)} [probability_theory.is_s_finite_kernel η] {a : α} ⦃f : β × γ E⦄ (hf : measure_theory.integrable f ((probability_theory.kernel.comp_prod κ η) 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 γ} [normed_add_comm_group E] {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {η : (probability_theory.kernel × β) γ)} [probability_theory.is_s_finite_kernel η] {a : α} [normed_space E] [complete_space E] {E' : Type u_5} [normed_add_comm_group E'] [complete_space E'] [normed_space E'] ⦃f g : β × γ E⦄ (F : E E') (hf : measure_theory.integrable f ((probability_theory.kernel.comp_prod κ η) a)) (hg : measure_theory.integrable g ((probability_theory.kernel.comp_prod κ η) 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 γ} [normed_add_comm_group E] {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {η : (probability_theory.kernel × β) γ)} [probability_theory.is_s_finite_kernel η] {a : α} [normed_space E] [complete_space E] {E' : Type u_5} [normed_add_comm_group E'] [complete_space E'] [normed_space E'] ⦃f g : β × γ E⦄ (F : E E') (hf : measure_theory.integrable f ((probability_theory.kernel.comp_prod κ η) a)) (hg : measure_theory.integrable g ((probability_theory.kernel.comp_prod κ η) 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 γ} [normed_add_comm_group E] {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {η : (probability_theory.kernel × β) γ)} [probability_theory.is_s_finite_kernel η] {a : α} [normed_space E] [complete_space E] ⦃f g : β × γ E⦄ (F : E ennreal) (hf : measure_theory.integrable f ((probability_theory.kernel.comp_prod κ η) a)) (hg : measure_theory.integrable g ((probability_theory.kernel.comp_prod κ η) 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 γ} [normed_add_comm_group E] {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {η : (probability_theory.kernel × β) γ)} [probability_theory.is_s_finite_kernel η] {a : α} [normed_space E] [complete_space E] ⦃f g : β × γ E⦄ (hf : measure_theory.integrable f ((probability_theory.kernel.comp_prod κ η) a)) (hg : measure_theory.integrable g ((probability_theory.kernel.comp_prod κ η) 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 γ} [normed_add_comm_group E] {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {η : (probability_theory.kernel × β) γ)} [probability_theory.is_s_finite_kernel η] {a : α} [normed_space E] [complete_space E] ⦃f g : β × γ E⦄ (hf : measure_theory.integrable f ((probability_theory.kernel.comp_prod κ η) a)) (hg : measure_theory.integrable g ((probability_theory.kernel.comp_prod κ η) 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 γ} [normed_add_comm_group E] {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {η : (probability_theory.kernel × β) γ)} [probability_theory.is_s_finite_kernel η] {a : α} [normed_space E] [complete_space E] ⦃f g : β × γ E⦄ (hf : measure_theory.integrable f ((probability_theory.kernel.comp_prod κ η) a)) (hg : measure_theory.integrable g ((probability_theory.kernel.comp_prod κ η) 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 γ} [normed_add_comm_group E] {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {η : (probability_theory.kernel × β) γ)} [probability_theory.is_s_finite_kernel η] {a : α} [normed_space E] [complete_space E] ⦃f g : β × γ E⦄ (hf : measure_theory.integrable f ((probability_theory.kernel.comp_prod κ η) a)) (hg : measure_theory.integrable g ((probability_theory.kernel.comp_prod κ η) 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.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 γ} [normed_add_comm_group E] {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {η : (probability_theory.kernel × β) γ)} [probability_theory.is_s_finite_kernel η] {a : α} [normed_space E] [complete_space E] {f : β × γ E} (hf : measure_theory.integrable f ((probability_theory.kernel.comp_prod κ η) a)) :
(z : β × γ), f z (probability_theory.kernel.comp_prod κ η) a = (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 γ} [normed_add_comm_group E] {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {η : (probability_theory.kernel × β) γ)} [probability_theory.is_s_finite_kernel η] {a : α} [normed_space E] [complete_space E] {f : β × γ E} {s : set β} {t : set γ} (hs : measurable_set s) (ht : measurable_set t) (hf : measure_theory.integrable_on f (s ×ˢ t) ((probability_theory.kernel.comp_prod κ η) a)) :
(z : β × γ) in s ×ˢ t, f z (probability_theory.kernel.comp_prod κ η) a = (x : β) in s, (y : γ) in t, f (x, y) η (a, x) κ a