# 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.

source
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 ≠ ⊤) :
MeasureTheory.HasFiniteIntegral (fun (b : β) => (η (a, b)).real (Prod.mk b ⁻¹' s)) (κ a)
source
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 ≠ ⊤) :
MeasureTheory.Integrable (fun (b : β) => (η (a, b)).real (Prod.mk b ⁻¹' s)) (κ a)
source
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)) :
AEStronglyMeasurable (fun (x : β) => ∫ (y : γ), f (x, y) ∂η (a, x)) (κ a)
source
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)) :
∀ᵐ (x : β) ∂κ a, AEStronglyMeasurable (fun (y : γ) => f (x, y)) (η (a, x))

### Integrability #

source
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) :
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)
source
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)) :
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)
source
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)) :
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)
source
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)) :
∀ᵐ (x : β) ∂κ a, Integrable (fun (y : γ) => f (x, y)) (η (a, x))
source
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)) :
Integrable (fun (x : β) => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)
source
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)) :
Integrable (fun (x : β) => ∫ (y : γ), f (x, y) ∂η (a, x)) (κ a)

### Bochner integral #

source
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)) :
∫ (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
source
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)) :
∫ (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
source
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)) :
∫⁻ (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
source
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)) :
∫ (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
source
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)) :
∫ (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
source
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)) :
∫ (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
source
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)) :
∫ (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
source
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] :
Continuous fun (f : ↥(MeasureTheory.Lp E 1 ((κ.compProd η) a))) => ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a
source
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} :
MeasureTheory.Integrable f ((κ.compProd η) a) → ∫ (z : β × γ), f z ∂(κ.compProd η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
source
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)) :
∫ (z : β × γ) in s ×ˢ t, f z ∂(κ.compProd η) a = ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
source
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)) :
∫ (z : β × γ) in s ×ˢ Set.univ, f z ∂(κ.compProd η) a = ∫ (x : β) in s, ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
source
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)) :
∫ (z : β × γ) in Set.univ ×ˢ t, f z ∂(κ.compProd η) a = ∫ (x : β), ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
source
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)
source
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 #

source
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)
source
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)
source
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)
source
theorem MeasureTheory.Measure.integrable_comp_iff {α : Type u_1} {β : Type u_2} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [NormedAddCommGroup E] {κ : ProbabilityTheory.Kernel α β} {μ : Measure α} {f : β → E} (hf : AEStronglyMeasurable f (μ.bind ⇑κ)) :
Integrable f (μ.bind ⇑κ) ↔ (∀ᵐ (x : α) ∂μ, Integrable f (κ x)) ∧ Integrable (fun (x : α) => ∫ (y : β), ‖f y‖ ∂κ x) μ
source
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)
source
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)) :
Integrable (fun (x : β) => ∫ (y : γ), ‖f y‖ ∂η x) (κ a)
source
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 #

source
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)) :
∫ (x : β), F (∫ (y : γ), f y + g y ∂η x) ∂κ a = ∫ (x : β), F (∫ (y : γ), f y ∂η x + ∫ (y : γ), g y ∂η x) ∂κ a
source
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)) :
∫ (x : β), F (∫ (y : γ), f y - g y ∂η x) ∂κ a = ∫ (x : β), F (∫ (y : γ), f y ∂η x - ∫ (y : γ), g y ∂η x) ∂κ a
source
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)) :
∫⁻ (x : β), F (∫ (y : γ), f y - g y ∂η x) ∂κ a = ∫⁻ (x : β), F (∫ (y : γ), f y ∂η x - ∫ (y : γ), g y ∂η x) ∂κ a
source
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)) :
∫ (x : β), ∫ (y : γ), f y + g y ∂η x ∂κ a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a + ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a
source
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)) :
∫ (x : β), ∫ (y : γ), (f + g) y ∂η x ∂κ a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a + ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a
source
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)) :
∫ (x : β), ∫ (y : γ), f y - g y ∂η x ∂κ a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a - ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a
source
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)) :
∫ (x : β), ∫ (y : γ), (f - g) y ∂η x ∂κ a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a - ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a
source
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
source
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} :
MeasureTheory.Integrable f ((η.comp κ) a) → ∫ (z : γ), f z ∂(η.comp κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
source
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)) :
∫ (z : γ) in s, f z ∂(η.comp κ) a = ∫ (x : β), ∫ (y : γ) in s, f y ∂η x ∂κ a
source
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)
source
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 κ)) :
Integrable f (μ.compProd κ) ↔ (∀ᵐ (x : α) ∂μ, Integrable (fun (y : β) => f (x, y)) (κ x)) ∧ Integrable (fun (x : α) => ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ
source
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 κ)) :
∫ (x : α × β), f x ∂μ.compProd κ = ∫ (a : α), ∫ (b : β), f (a, b) ∂κ a ∂μ
source
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 κ)) :
∫ (x : α × β) in s ×ˢ t, f x ∂μ.compProd κ = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ
source
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 ⇑κ)) :
Integrable (fun (p : α × β) => f p.2) (μ.compProd κ) ↔ Integrable f (μ.bind ⇑κ)
source
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)
source
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 ⇑κ)) :
Integrable (fun (x : α) => ∫ (y : β), ‖f y‖ ∂κ x) μ