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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
(a : α)
{s : Set (β × γ)}
(h2s : ↑↑((ProbabilityTheory.kernel.compProd κ η) a) s ≠ ⊤)
:
MeasureTheory.HasFiniteIntegral fun (b : β) => ENNReal.toReal (↑↑(η (a, b)) (Prod.mk b ⁻¹' s))
theorem
ProbabilityTheory.integrable_kernel_prod_mk_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
(a : α)
{s : Set (β × γ)}
(hs : MeasurableSet s)
(h2s : ↑↑((ProbabilityTheory.kernel.compProd κ η) a) s ≠ ⊤)
:
MeasureTheory.Integrable fun (b : β) => ENNReal.toReal (↑↑(η (a, b)) (Prod.mk b ⁻¹' s))
theorem
MeasureTheory.AEStronglyMeasurable.integral_kernel_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
[CompleteSpace E]
⦃f : β × γ → E⦄
(hf : MeasureTheory.AEStronglyMeasurable f ((ProbabilityTheory.kernel.compProd κ η) a))
:
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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
{δ : Type u_5}
[TopologicalSpace δ]
{f : β × γ → δ}
(hf : MeasureTheory.AEStronglyMeasurable f ((ProbabilityTheory.kernel.compProd κ η) a))
:
∀ᵐ (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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
⦃f : β × γ → E⦄
(h1f : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.HasFiniteIntegral f ↔ (∀ᵐ (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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
⦃f : β × γ → E⦄
(h1f : MeasureTheory.AEStronglyMeasurable f ((ProbabilityTheory.kernel.compProd κ η) a))
:
MeasureTheory.HasFiniteIntegral f ↔ (∀ᵐ (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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
⦃f : β × γ → E⦄
(hf : MeasureTheory.AEStronglyMeasurable f ((ProbabilityTheory.kernel.compProd κ η) a))
:
MeasureTheory.Integrable f ↔ (∀ᵐ (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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
⦃f : β × γ → E⦄
(hf : MeasureTheory.Integrable f)
:
∀ᵐ (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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
⦃f : β × γ → E⦄
(hf : MeasureTheory.Integrable f)
:
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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
[CompleteSpace E]
⦃f : β × γ → E⦄
(hf : MeasureTheory.Integrable f)
:
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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
⦃f : β × γ → E⦄
⦃g : β × γ → E⦄
(F : E → E')
(hf : MeasureTheory.Integrable f)
(hg : MeasureTheory.Integrable g)
:
theorem
ProbabilityTheory.kernel.integral_fn_integral_sub
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
⦃f : β × γ → E⦄
⦃g : β × γ → E⦄
(F : E → E')
(hf : MeasureTheory.Integrable f)
(hg : MeasureTheory.Integrable g)
:
theorem
ProbabilityTheory.kernel.lintegral_fn_integral_sub
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
⦃f : β × γ → E⦄
⦃g : β × γ → E⦄
(F : E → ENNReal)
(hf : MeasureTheory.Integrable f)
(hg : MeasureTheory.Integrable g)
:
theorem
ProbabilityTheory.kernel.integral_integral_add
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
[CompleteSpace E]
⦃f : β × γ → E⦄
⦃g : β × γ → E⦄
(hf : MeasureTheory.Integrable f)
(hg : MeasureTheory.Integrable g)
:
theorem
ProbabilityTheory.kernel.integral_integral_add'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
[CompleteSpace E]
⦃f : β × γ → E⦄
⦃g : β × γ → E⦄
(hf : MeasureTheory.Integrable f)
(hg : MeasureTheory.Integrable g)
:
theorem
ProbabilityTheory.kernel.integral_integral_sub
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
[CompleteSpace E]
⦃f : β × γ → E⦄
⦃g : β × γ → E⦄
(hf : MeasureTheory.Integrable f)
(hg : MeasureTheory.Integrable g)
:
theorem
ProbabilityTheory.kernel.integral_integral_sub'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
[CompleteSpace E]
⦃f : β × γ → E⦄
⦃g : β × γ → E⦄
(hf : MeasureTheory.Integrable f)
(hg : MeasureTheory.Integrable g)
:
theorem
ProbabilityTheory.kernel.continuous_integral_integral
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
[CompleteSpace E]
:
Continuous fun (f : ↥(MeasureTheory.Lp E 1)) => ∫ (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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
[CompleteSpace E]
{f : β × γ → E}
:
MeasureTheory.Integrable f →
∫ (z : β × γ), f z ∂(ProbabilityTheory.kernel.compProd κ η) a = ∫ (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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
[CompleteSpace E]
{f : β × γ → E}
{s : Set β}
{t : Set γ}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ t))
:
∫ (z : β × γ) in s ×ˢ t, f z ∂(ProbabilityTheory.kernel.compProd κ η) a = ∫ (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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
[CompleteSpace E]
(f : β × γ → E)
{s : Set β}
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ))
:
∫ (z : β × γ) in s ×ˢ Set.univ, f z ∂(ProbabilityTheory.kernel.compProd κ η) a = ∫ (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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
[CompleteSpace E]
(f : β × γ → E)
{t : Set γ}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t))
:
∫ (z : β × γ) in Set.univ ×ˢ t, f z ∂(ProbabilityTheory.kernel.compProd κ η) a = ∫ (x : β), ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a