# Documentation

Mathlib.Probability.Kernel.IntegralCompProd

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

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 ProbabilityTheory.kernel.lintegral_compProd 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 #

• ProbabilityTheory.integral_compProd: 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 Mathlib/MeasureTheory/Constructions/Prod/Basic.lean. 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 ProbabilityTheory.hasFiniteIntegral_prod_mk_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} (a : α) {s : Set (β × γ)} (h2s : ↑() s ) :
MeasureTheory.HasFiniteIntegral fun b => ENNReal.toReal (↑(η (a, b)) ( ⁻¹' s))
theorem ProbabilityTheory.integrable_kernel_prod_mk_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} (a : α) {s : Set (β × γ)} (hs : ) (h2s : ↑() s ) :
MeasureTheory.Integrable fun b => ENNReal.toReal (↑(η (a, b)) ( ⁻¹' s))
theorem MeasureTheory.AEStronglyMeasurable.integral_kernel_compProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} [] [] ⦃f : β × γE (hf : ) :
MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : γ), f (x, y)η (a, x)) (κ a)
theorem MeasureTheory.AEStronglyMeasurable.compProd_mk_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} {δ : Type u_5} [] {f : β × γδ} (hf : ) :
∀ᵐ (x : β) ∂κ a, MeasureTheory.AEStronglyMeasurable (fun y => f (x, y)) (η (a, x))

### Integrability #

theorem ProbabilityTheory.hasFiniteIntegral_compProd_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} ⦃f : β × γE (h1f : ) :
(∀ᵐ (x : β) ∂κ a, MeasureTheory.HasFiniteIntegral fun y => f (x, y)) MeasureTheory.HasFiniteIntegral fun x => ∫ (y : γ), f (x, y)η (a, x)
theorem ProbabilityTheory.hasFiniteIntegral_compProd_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} ⦃f : β × γE (h1f : ) :
(∀ᵐ (x : β) ∂κ a, MeasureTheory.HasFiniteIntegral fun y => f (x, y)) MeasureTheory.HasFiniteIntegral fun x => ∫ (y : γ), f (x, y)η (a, x)
theorem ProbabilityTheory.integrable_compProd_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} ⦃f : β × γE (hf : ) :
(∀ᵐ (x : β) ∂κ a, MeasureTheory.Integrable fun y => f (x, y)) MeasureTheory.Integrable fun x => ∫ (y : γ), f (x, y)η (a, x)
theorem MeasureTheory.Integrable.compProd_mk_left_ae {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} ⦃f : β × γE (hf : ) :
∀ᵐ (x : β) ∂κ a, MeasureTheory.Integrable fun y => f (x, y)
theorem MeasureTheory.Integrable.integral_norm_compProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} ⦃f : β × γE (hf : ) :
MeasureTheory.Integrable fun x => ∫ (y : γ), f (x, y)η (a, x)
theorem MeasureTheory.Integrable.integral_compProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} [] [] ⦃f : β × γE (hf : ) :
MeasureTheory.Integrable fun x => ∫ (y : γ), f (x, y)η (a, x)

### Bochner integral #

theorem ProbabilityTheory.kernel.integral_fn_integral_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} [] {E' : Type u_5} [] [] ⦃f : β × γE ⦃g : β × γE (F : EE') (hf : ) (hg : ) :
∫ (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 ProbabilityTheory.kernel.integral_fn_integral_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} [] {E' : Type u_5} [] [] ⦃f : β × γE ⦃g : β × γE (F : EE') (hf : ) (hg : ) :
∫ (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 ProbabilityTheory.kernel.lintegral_fn_integral_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} [] ⦃f : β × γE ⦃g : β × γE (F : EENNReal) (hf : ) (hg : ) :
∫⁻ (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 ProbabilityTheory.kernel.integral_integral_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} [] [] ⦃f : β × γE ⦃g : β × γE (hf : ) (hg : ) :
∫ (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 ProbabilityTheory.kernel.integral_integral_add' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} [] [] ⦃f : β × γE ⦃g : β × γE (hf : ) (hg : ) :
∫ (x : β), ∫ (y : γ), ((β × γE) + (β × γE)) (β × γE) instHAdd f g (x, y)η (a, x)κ a = ∫ (x : β), ∫ (y : γ), f (x, y)η (a, x)κ a + ∫ (x : β), ∫ (y : γ), g (x, y)η (a, x)κ a
theorem ProbabilityTheory.kernel.integral_integral_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} [] [] ⦃f : β × γE ⦃g : β × γE (hf : ) (hg : ) :
∫ (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 ProbabilityTheory.kernel.integral_integral_sub' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} [] [] ⦃f : β × γE ⦃g : β × γE (hf : ) (hg : ) :
∫ (x : β), ∫ (y : γ), ((β × γE) - (β × γE)) (β × γE) instHSub f g (x, y)η (a, x)κ a = ∫ (x : β), ∫ (y : γ), f (x, y)η (a, x)κ a - ∫ (x : β), ∫ (y : γ), g (x, y)η (a, x)κ a
theorem ProbabilityTheory.kernel.continuous_integral_integral {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} [] [] :
Continuous fun f => ∫ (x : β), ∫ (y : γ), f (x, y)η (a, x)κ a
theorem ProbabilityTheory.integral_compProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} [] [] {f : β × γE} :
∫ (z : β × γ), f z = ∫ (x : β), ∫ (y : γ), f (x, y)η (a, x)κ a
theorem ProbabilityTheory.set_integral_compProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} [] [] {f : β × γE} {s : Set β} {t : Set γ} (hs : ) (ht : ) (hf : MeasureTheory.IntegrableOn f (s ×ˢ t)) :
∫ (z : β × γ) in s ×ˢ t, f z = ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y)η (a, x)κ a
theorem ProbabilityTheory.set_integral_compProd_univ_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} [] [] (f : β × γE) {s : Set β} (hs : ) (hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ)) :
∫ (z : β × γ) in s ×ˢ Set.univ, f z = ∫ (x : β) in s, ∫ (y : γ), f (x, y)η (a, x)κ a
theorem ProbabilityTheory.set_integral_compProd_univ_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : } {mβ : } {mγ : } {κ : { x // }} {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} [] [] (f : β × γE) {t : Set γ} (ht : ) (hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t)) :
∫ (z : β × γ) in Set.univ ×ˢ t, f z = ∫ (x : β), ∫ (y : γ) in t, f (x, y)η (a, x)κ a