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 γ}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
(a : α)
{s : Set (β × γ)}
(h2s : ((κ.compProd η) a) s ≠ ⊤)
:
MeasureTheory.HasFiniteIntegral (fun (b : β) => ((η (a, b)) (Prod.mk b ⁻¹' s)).toReal) (κ a)
theorem
ProbabilityTheory.integrable_kernel_prod_mk_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
(a : α)
{s : Set (β × γ)}
(hs : MeasurableSet s)
(h2s : ((κ.compProd η) a) s ≠ ⊤)
:
MeasureTheory.Integrable (fun (b : β) => ((η (a, b)) (Prod.mk b ⁻¹' s)).toReal) (κ a)
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]
⦃f : β × γ → E⦄
(hf : AEStronglyMeasurable f ((κ.compProd η) a))
:
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 : AEStronglyMeasurable f ((κ.compProd η) a))
:
∀ᵐ (x : β) ∂κ a, 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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
⦃f : β × γ → E⦄
(h1f : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.HasFiniteIntegral f ((κ.compProd η) a) ↔ (∀ᵐ (x : β) ∂κ a, MeasureTheory.HasFiniteIntegral (fun (y : γ) => f (x, y)) (η (a, x))) ∧ MeasureTheory.HasFiniteIntegral (fun (x : β) => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)
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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
⦃f : β × γ → E⦄
(h1f : MeasureTheory.AEStronglyMeasurable f ((κ.compProd η) a))
:
MeasureTheory.HasFiniteIntegral f ((κ.compProd η) a) ↔ (∀ᵐ (x : β) ∂κ a, MeasureTheory.HasFiniteIntegral (fun (y : γ) => f (x, y)) (η (a, x))) ∧ MeasureTheory.HasFiniteIntegral (fun (x : β) => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)
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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
⦃f : β × γ → E⦄
(hf : MeasureTheory.AEStronglyMeasurable f ((κ.compProd η) a))
:
MeasureTheory.Integrable f ((κ.compProd η) a) ↔ (∀ᵐ (x : β) ∂κ a, MeasureTheory.Integrable (fun (y : γ) => f (x, y)) (η (a, x))) ∧ MeasureTheory.Integrable (fun (x : β) => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)
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 : Integrable f ((κ.compProd η) a))
:
∀ᵐ (x : β) ∂κ a, Integrable (fun (y : γ) => f (x, y)) (η (a, x))
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 : Integrable f ((κ.compProd η) a))
:
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]
⦃f : β × γ → E⦄
(hf : Integrable f ((κ.compProd η) a))
:
Integrable (fun (x : β) => ∫ (y : γ), f (x, y) ∂η (a, x)) (κ a)
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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
⦃f g : β × γ → E⦄
(F : E → E')
(hf : MeasureTheory.Integrable f ((κ.compProd η) a))
(hg : MeasureTheory.Integrable g ((κ.compProd η) a))
:
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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
⦃f g : β × γ → E⦄
(F : E → E')
(hf : MeasureTheory.Integrable f ((κ.compProd η) a))
(hg : MeasureTheory.Integrable g ((κ.compProd η) a))
:
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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
⦃f g : β × γ → E⦄
(F : E → ENNReal)
(hf : MeasureTheory.Integrable f ((κ.compProd η) a))
(hg : MeasureTheory.Integrable g ((κ.compProd η) a))
:
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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
⦃f g : β × γ → E⦄
(hf : MeasureTheory.Integrable f ((κ.compProd η) a))
(hg : MeasureTheory.Integrable g ((κ.compProd η) a))
:
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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
⦃f g : β × γ → E⦄
(hf : MeasureTheory.Integrable f ((κ.compProd η) a))
(hg : MeasureTheory.Integrable g ((κ.compProd η) a))
:
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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
⦃f g : β × γ → E⦄
(hf : MeasureTheory.Integrable f ((κ.compProd η) a))
(hg : MeasureTheory.Integrable g ((κ.compProd η) a))
:
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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
⦃f g : β × γ → E⦄
(hf : MeasureTheory.Integrable f ((κ.compProd η) a))
(hg : MeasureTheory.Integrable g ((κ.compProd η) a))
:
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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
:
Continuous fun (f : ↥(MeasureTheory.Lp E 1 ((κ.compProd η) a))) => ∫ (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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
{f : β × γ → E}
:
theorem
ProbabilityTheory.setIntegral_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
{f : β × γ → E}
{s : Set β}
{t : Set γ}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ t) ((κ.compProd η) a))
:
@[deprecated ProbabilityTheory.setIntegral_compProd (since := "2024-04-17")]
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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
{f : β × γ → E}
{s : Set β}
{t : Set γ}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ t) ((κ.compProd η) a))
:
Alias of ProbabilityTheory.setIntegral_compProd.
theorem
ProbabilityTheory.setIntegral_compProd_univ_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
(f : β × γ → E)
{s : Set β}
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ((κ.compProd η) a))
:
@[deprecated ProbabilityTheory.setIntegral_compProd_univ_right (since := "2024-04-17")]
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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
(f : β × γ → E)
{s : Set β}
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ((κ.compProd η) a))
:
theorem
ProbabilityTheory.setIntegral_compProd_univ_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
(f : β × γ → E)
{t : Set γ}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ((κ.compProd η) a))
:
@[deprecated ProbabilityTheory.setIntegral_compProd_univ_left (since := "2024-04-17")]
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]
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
[NormedSpace ℝ E]
(f : β × γ → E)
{t : Set γ}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ((κ.compProd η) a))
: