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 α β)}
[probability_theory.is_s_finite_kernel κ]
{η : ↥(probability_theory.kernel (α × β) γ)}
[probability_theory.is_s_finite_kernel η]
(a : α)
{s : set (β × γ)}
(h2s : ⇑(⇑(probability_theory.kernel.comp_prod κ η) a) s ≠ ⊤) :
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 α β)}
[probability_theory.is_s_finite_kernel κ]
{η : ↥(probability_theory.kernel (α × β) γ)}
[probability_theory.is_s_finite_kernel η]
(a : α)
{s : set (β × γ)}
(hs : measurable_set s)
(h2s : ⇑(⇑(probability_theory.kernel.comp_prod κ η) a) s ≠ ⊤) :
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 γ}
[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.ae_strongly_measurable f (⇑(probability_theory.kernel.comp_prod κ η) 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 α β)}
[probability_theory.is_s_finite_kernel κ]
{η : ↥(probability_theory.kernel (α × β) γ)}
[probability_theory.is_s_finite_kernel η]
{a : α}
{δ : Type u_4}
[topological_space δ]
{f : β × γ → δ}
(hf : measure_theory.ae_strongly_measurable f (⇑(probability_theory.kernel.comp_prod κ η) a)) :
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 γ}
[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⦄
(h1f : measure_theory.strongly_measurable f) :
measure_theory.has_finite_integral f (⇑(probability_theory.kernel.comp_prod κ η) 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.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 γ}
[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⦄
(h1f : measure_theory.ae_strongly_measurable f (⇑(probability_theory.kernel.comp_prod κ η) a)) :
measure_theory.has_finite_integral f (⇑(probability_theory.kernel.comp_prod κ η) 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 γ}
[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.ae_strongly_measurable f (⇑(probability_theory.kernel.comp_prod κ η) a)) :
measure_theory.integrable f (⇑(probability_theory.kernel.comp_prod κ η) a) ↔ (∀ᵐ (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 γ}
[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)) :
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)) :
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 γ}
[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)) :
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)) :
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)) :
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)) :
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)) :
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)) :
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)) :
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)) :
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 γ}
[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] :
continuous (λ (f : ↥(measure_theory.Lp E 1 (⇑(probability_theory.kernel.comp_prod κ η) 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 γ}
[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)) :
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)) :
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 γ}
[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 β}
(hs : measurable_set s)
(hf : measure_theory.integrable_on f (s ×ˢ set.univ) (⇑(probability_theory.kernel.comp_prod κ η) 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 γ}
[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)
{t : set γ}
(ht : measurable_set t)
(hf : measure_theory.integrable_on f (set.univ ×ˢ t) (⇑(probability_theory.kernel.comp_prod κ η) a)) :