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 #

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 : ((κ.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 γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.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 : MeasureTheory.AEStronglyMeasurable f ((κ.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 ((κ.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 ((κ.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] {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.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] {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.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 : MeasureTheory.Integrable f ((κ.compProd η) a)) :
∀ᵐ (x : β) ∂κ a, MeasureTheory.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 : MeasureTheory.Integrable f ((κ.compProd η) a)) :
MeasureTheory.Integrable (fun (x : β) => ∫ (y : γ), f (x, y)η (a, x)) (κ 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 : MeasureTheory.Integrable f ((κ.compProd η) a)) :
MeasureTheory.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] {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {a : α} [NormedSpace E] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace E'] ⦃f : β × γE ⦃g : β × γE (F : EE') (hf : MeasureTheory.Integrable f ((κ.compProd η) a)) (hg : MeasureTheory.Integrable g ((κ.compProd η) 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 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 : EE') (hf : MeasureTheory.Integrable f ((κ.compProd η) a)) (hg : MeasureTheory.Integrable g ((κ.compProd η) 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 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 : EENNReal) (hf : MeasureTheory.Integrable f ((κ.compProd η) a)) (hg : MeasureTheory.Integrable g ((κ.compProd η) 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 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] ⦃f : β × γE ⦃g : β × γE (hf : MeasureTheory.Integrable f ((κ.compProd η) a)) (hg : MeasureTheory.Integrable g ((κ.compProd η) 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 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] ⦃f : β × γE ⦃g : β × γE (hf : MeasureTheory.Integrable f ((κ.compProd η) a)) (hg : MeasureTheory.Integrable g ((κ.compProd η) 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 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] ⦃f : β × γE ⦃g : β × γE (hf : MeasureTheory.Integrable f ((κ.compProd η) a)) (hg : MeasureTheory.Integrable g ((κ.compProd η) 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 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] ⦃f : β × γE ⦃g : β × γE (hf : MeasureTheory.Integrable f ((κ.compProd η) a)) (hg : MeasureTheory.Integrable g ((κ.compProd η) 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 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] :
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] {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {a : α} [NormedSpace E] {f : β × γE} :
MeasureTheory.Integrable f ((κ.compProd η) a)∫ (z : β × γ), f z(κ.compProd η) a = ∫ (x : β), ∫ (y : γ), f (x, y)η (a, x)κ a
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] {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {a : α} [NormedSpace E] {f : β × γE} {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) (hf : MeasureTheory.IntegrableOn f (s ×ˢ t) ((κ.compProd η) a)) :
∫ (z : β × γ) in s ×ˢ t, f z(κ.compProd η) a = ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y)η (a, x)κ a
@[deprecated ProbabilityTheory.setIntegral_compProd]
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] {f : β × γE} {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) (hf : MeasureTheory.IntegrableOn f (s ×ˢ t) ((κ.compProd η) a)) :
∫ (z : β × γ) in s ×ˢ t, f z(κ.compProd η) a = ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y)η (a, x)κ 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] {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {a : α} [NormedSpace E] (f : β × γE) {s : Set β} (hs : MeasurableSet s) (hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ((κ.compProd η) a)) :
∫ (z : β × γ) in s ×ˢ Set.univ, f z(κ.compProd η) a = ∫ (x : β) in s, ∫ (y : γ), f (x, y)η (a, x)κ a
@[deprecated ProbabilityTheory.setIntegral_compProd_univ_right]
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] (f : β × γE) {s : Set β} (hs : MeasurableSet s) (hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ((κ.compProd η) a)) :
∫ (z : β × γ) in s ×ˢ Set.univ, f z(κ.compProd η) a = ∫ (x : β) in s, ∫ (y : γ), f (x, y)η (a, x)κ a

Alias of ProbabilityTheory.setIntegral_compProd_univ_right.

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] {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {a : α} [NormedSpace E] (f : β × γE) {t : Set γ} (ht : MeasurableSet t) (hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ((κ.compProd η) a)) :
∫ (z : β × γ) in Set.univ ×ˢ t, f z(κ.compProd η) a = ∫ (x : β), ∫ (y : γ) in t, f (x, y)η (a, x)κ a
@[deprecated ProbabilityTheory.setIntegral_compProd_univ_left]
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] (f : β × γE) {t : Set γ} (ht : MeasurableSet t) (hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ((κ.compProd η) a)) :
∫ (z : β × γ) in Set.univ ×ˢ t, f z(κ.compProd η) a = ∫ (x : β), ∫ (y : γ) in t, f (x, y)η (a, x)κ a

Alias of ProbabilityTheory.setIntegral_compProd_univ_left.