Bochner integral of a function against the composition and the composition-products of two kernels #
We prove properties of the composition and the composition-product of two kernels.
If κ is a kernel from α to β and η is a kernel from β to γ, we can form their
composition η ∘ₖ κ : Kernel α γ. We proved in ProbabilityTheory.Kernel.lintegral_comp that it
verifies ∫⁻ c, f c ∂((η ∘ₖ κ) a) = ∫⁻ b, ∫⁻ c, f c ∂(η b) ∂(κ a). In this file, we
prove the same equality for the Bochner integral.
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).ProbabilityTheory.integral_comp: the integral against the composition is∫⁻ z, f z ∂((η ∘ₖ κ) a) = ∫⁻ x, ∫⁻ y, f y ∂(η x) ∂(κ a).
Implementation details #
This file is to a large extent a copy of part of Mathlib/MeasureTheory/Integral/Prod.lean.
The product of two measures is a particular case of composition-product of kernels and
it turns out that once the measurability 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.
The composition of kernels can also be expressed easily with the composition-product and therefore the proofs about the composition are only simplified versions of the ones for the composition-product. However it is necessary to do all the proofs once again because the composition-product requires s-finiteness while the composition does not.
theorem
ProbabilityTheory.hasFiniteIntegral_prodMk_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 ≠ ⊤)
:
@[deprecated ProbabilityTheory.hasFiniteIntegral_prodMk_left (since := "2025-03-05")]
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 ≠ ⊤)
:
theorem
ProbabilityTheory.integrable_kernel_prodMk_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 ≠ ⊤)
:
@[deprecated ProbabilityTheory.integrable_kernel_prodMk_left (since := "2025-03-05")]
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 ≠ ⊤)
:
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]
{a : α}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsSFiniteKernel η]
[NormedSpace ℝ E]
⦃f : β × γ → E⦄
(hf : AEStronglyMeasurable f ((κ.compProd η) a))
:
theorem
MeasureTheory.AEStronglyMeasurable.compProd_mk_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{a : α}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsSFiniteKernel η]
{δ : Type u_5}
[TopologicalSpace δ]
{f : β × γ → δ}
(hf : AEStronglyMeasurable f ((κ.compProd η) a))
:
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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
⦃f : β × γ → E⦄
(h1f : MeasureTheory.StronglyMeasurable f)
:
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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
⦃f : β × γ → E⦄
(h1f : MeasureTheory.AEStronglyMeasurable f ((κ.compProd η) 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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
⦃f : β × γ → E⦄
(hf : MeasureTheory.AEStronglyMeasurable f ((κ.compProd η) a))
:
theorem
MeasureTheory.Integrable.ae_of_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsSFiniteKernel η]
⦃f : β × γ → E⦄
(hf : Integrable f ((κ.compProd η) a))
:
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]
{a : α}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsSFiniteKernel η]
⦃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]
{a : α}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsSFiniteKernel η]
[NormedSpace ℝ E]
⦃f : β × γ → E⦄
(hf : Integrable f ((κ.compProd η) 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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
[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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
[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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
[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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
[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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
[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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
[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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
[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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
[NormedSpace ℝ E]
:
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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
[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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
[NormedSpace ℝ E]
{f : β × γ → E}
{s : Set β}
{t : Set γ}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ t) ((κ.compProd η) a))
:
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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
[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]
{a : α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
[NormedSpace ℝ E]
(f : β × γ → E)
{t : Set γ}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ((κ.compProd η) a))
:
theorem
MeasureTheory.AEStronglyMeasurable.integral_kernel_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel β γ}
[NormedSpace ℝ E]
⦃f : γ → E⦄
(hf : AEStronglyMeasurable f ((η.comp κ) a))
:
AEStronglyMeasurable (fun (x : β) => ∫ (y : γ), f y ∂η x) (κ a)
theorem
MeasureTheory.AEStronglyMeasurable.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{a : α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel β γ}
{δ : Type u_5}
[TopologicalSpace δ]
{f : γ → δ}
(hf : AEStronglyMeasurable f ((η.comp κ) a))
:
∀ᵐ (x : β) ∂κ a, AEStronglyMeasurable f (η x)
Integrability with respect to composition #
theorem
ProbabilityTheory.hasFiniteIntegral_comp_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : Kernel α β}
{η : Kernel β γ}
⦃f : γ → E⦄
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.HasFiniteIntegral f ((η.comp κ) a) ↔ (∀ᵐ (x : β) ∂κ a, MeasureTheory.HasFiniteIntegral f (η x)) ∧ MeasureTheory.HasFiniteIntegral (fun (x : β) => ∫ (y : γ), ‖f y‖ ∂η x) (κ a)
theorem
ProbabilityTheory.hasFiniteIntegral_comp_iff'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : Kernel α β}
{η : Kernel β γ}
⦃f : γ → E⦄
(hf : MeasureTheory.AEStronglyMeasurable f ((η.comp κ) a))
:
MeasureTheory.HasFiniteIntegral f ((η.comp κ) a) ↔ (∀ᵐ (x : β) ∂κ a, MeasureTheory.HasFiniteIntegral f (η x)) ∧ MeasureTheory.HasFiniteIntegral (fun (x : β) => ∫ (y : γ), ‖f y‖ ∂η x) (κ a)
theorem
ProbabilityTheory.integrable_comp_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : Kernel α β}
{η : Kernel β γ}
⦃f : γ → E⦄
(hf : MeasureTheory.AEStronglyMeasurable f ((η.comp κ) a))
:
MeasureTheory.Integrable f ((η.comp κ) a) ↔ (∀ᵐ (y : β) ∂κ a, MeasureTheory.Integrable f (η y)) ∧ MeasureTheory.Integrable (fun (y : β) => ∫ (z : γ), ‖f z‖ ∂η y) (κ a)
theorem
MeasureTheory.Integrable.ae_of_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel β γ}
⦃f : γ → E⦄
(hf : Integrable f ((η.comp κ) a))
:
∀ᵐ (x : β) ∂κ a, Integrable f (η x)
theorem
MeasureTheory.Integrable.integral_norm_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel β γ}
⦃f : γ → E⦄
(hf : Integrable f ((η.comp κ) a))
:
theorem
MeasureTheory.Integrable.integral_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel β γ}
[NormedSpace ℝ E]
⦃f : γ → E⦄
(hf : Integrable f ((η.comp κ) a))
:
Integrable (fun (x : β) => ∫ (y : γ), f y ∂η x) (κ a)
Bochner integral with respect to the composition #
theorem
ProbabilityTheory.Kernel.integral_fn_integral_add_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : Kernel α β}
{η : Kernel β γ}
[NormedSpace ℝ E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
⦃f g : γ → E⦄
(F : E → E')
(hf : MeasureTheory.Integrable f ((η.comp κ) a))
(hg : MeasureTheory.Integrable g ((η.comp κ) a))
:
theorem
ProbabilityTheory.Kernel.integral_fn_integral_sub_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : Kernel α β}
{η : Kernel β γ}
[NormedSpace ℝ E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
⦃f g : γ → E⦄
(F : E → E')
(hf : MeasureTheory.Integrable f ((η.comp κ) a))
(hg : MeasureTheory.Integrable g ((η.comp κ) a))
:
theorem
ProbabilityTheory.Kernel.lintegral_fn_integral_sub_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : Kernel α β}
{η : Kernel β γ}
[NormedSpace ℝ E]
⦃f g : γ → E⦄
(F : E → ENNReal)
(hf : MeasureTheory.Integrable f ((η.comp κ) a))
(hg : MeasureTheory.Integrable g ((η.comp κ) a))
:
theorem
ProbabilityTheory.Kernel.integral_integral_add_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : Kernel α β}
{η : Kernel β γ}
[NormedSpace ℝ E]
⦃f g : γ → E⦄
(hf : MeasureTheory.Integrable f ((η.comp κ) a))
(hg : MeasureTheory.Integrable g ((η.comp κ) a))
:
theorem
ProbabilityTheory.Kernel.integral_integral_add'_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : Kernel α β}
{η : Kernel β γ}
[NormedSpace ℝ E]
⦃f g : γ → E⦄
(hf : MeasureTheory.Integrable f ((η.comp κ) a))
(hg : MeasureTheory.Integrable g ((η.comp κ) a))
:
theorem
ProbabilityTheory.Kernel.integral_integral_sub_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : Kernel α β}
{η : Kernel β γ}
[NormedSpace ℝ E]
⦃f g : γ → E⦄
(hf : MeasureTheory.Integrable f ((η.comp κ) a))
(hg : MeasureTheory.Integrable g ((η.comp κ) a))
:
theorem
ProbabilityTheory.Kernel.integral_integral_sub'_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : Kernel α β}
{η : Kernel β γ}
[NormedSpace ℝ E]
⦃f g : γ → E⦄
(hf : MeasureTheory.Integrable f ((η.comp κ) a))
(hg : MeasureTheory.Integrable g ((η.comp κ) a))
:
theorem
ProbabilityTheory.Kernel.continuous_integral_integral_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : Kernel α β}
{η : Kernel β γ}
[NormedSpace ℝ E]
:
Continuous fun (f : ↥(MeasureTheory.Lp E 1 ((η.comp κ) a))) => ∫ (x : β), ∫ (y : γ), ↑↑f y ∂η x ∂κ a
theorem
ProbabilityTheory.Kernel.integral_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : Kernel α β}
{η : Kernel β γ}
[NormedSpace ℝ E]
{f : γ → E}
:
theorem
ProbabilityTheory.Kernel.setIntegral_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{E : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[NormedAddCommGroup E]
{a : α}
{κ : Kernel α β}
{η : Kernel β γ}
[NormedSpace ℝ E]
{f : γ → E}
{s : Set γ}
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f s ((η.comp κ) a))
:
theorem
MeasureTheory.AEStronglyMeasurable.ae_of_compProd
{α : Type u_5}
{β : Type u_6}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{μ : Measure α}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{E : Type u_8}
[NormedAddCommGroup E]
{f : α → β → E}
(hf : AEStronglyMeasurable (Function.uncurry f) (μ.compProd κ))
:
∀ᵐ (x : α) ∂μ, AEStronglyMeasurable (f x) (κ x)
theorem
MeasureTheory.Measure.integrable_compProd_iff
{α : Type u_5}
{β : Type u_6}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{μ : Measure α}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{E : Type u_8}
[NormedAddCommGroup E]
{f : α × β → E}
(hf : AEStronglyMeasurable f (μ.compProd κ))
:
theorem
MeasureTheory.Measure.integral_compProd
{α : Type u_5}
{β : Type u_6}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{μ : Measure α}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{E : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α × β → E}
(hf : Integrable f (μ.compProd κ))
:
theorem
MeasureTheory.Measure.setIntegral_compProd
{α : Type u_5}
{β : Type u_6}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{μ : Measure α}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{E : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set α}
(hs : MeasurableSet s)
{t : Set β}
(ht : MeasurableSet t)
{f : α × β → E}
(hf : IntegrableOn f (s ×ˢ t) (μ.compProd κ))
:
theorem
MeasureTheory.Measure.integrable_compProd_snd_iff
{α : Type u_5}
{β : Type u_6}
{E : Type u_7}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[NormedAddCommGroup E]
{κ : ProbabilityTheory.Kernel α β}
{μ : Measure α}
{f : β → E}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
(hf : AEStronglyMeasurable f (μ.bind ⇑κ))
:
theorem
MeasureTheory.Measure.ae_integrable_of_integrable_comp
{α : Type u_5}
{β : Type u_6}
{E : Type u_7}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[NormedAddCommGroup E]
{κ : ProbabilityTheory.Kernel α β}
{μ : Measure α}
{f : β → E}
(h_int : Integrable f (μ.bind ⇑κ))
:
∀ᵐ (x : α) ∂μ, Integrable f (κ x)
theorem
MeasureTheory.Measure.integrable_integral_norm_of_integrable_comp
{α : Type u_5}
{β : Type u_6}
{E : Type u_7}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[NormedAddCommGroup E]
{κ : ProbabilityTheory.Kernel α β}
{μ : Measure α}
{f : β → E}
(h_int : Integrable f (μ.bind ⇑κ))
: