Measurability of the integral against a kernel

The Bochner integral of a strongly measurable function against a kernel is strongly measurable.

Main statements

• MeasureTheory.StronglyMeasurable.integral_kernel_prod_right: the function a ↦ ∫ b, f a b ∂(κ a) is measurable, for an s-finite kernel κ : Kernel α β and a function f : α → β → E such that uncurry f is measurable.

theorem ProbabilityTheory.measurableSet_integrable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} {E : Type u_4} [NormedAddCommGroup E] ⦃f : β → E⦄ (hf : MeasureTheory.StronglyMeasurable f) : MeasurableSet {a : α | MeasureTheory.Integrable f (κ a)}

theorem ProbabilityTheory.measurableSet_kernel_integrable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} {E : Type u_4} [NormedAddCommGroup E] [IsSFiniteKernel κ] ⦃f : α → β → E⦄ (hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)) : MeasurableSet {x : α | MeasureTheory.Integrable (f x) (κ x)}

theorem MeasureTheory.StronglyMeasurable.integral_kernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] ⦃f : β → E⦄ (hf : StronglyMeasurable f) : StronglyMeasurable fun (x : α) => ∫ (y : β), f y ∂κ x

theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {E : Type u_4} [NormedAddCommGroup E] [ProbabilityTheory.IsSFiniteKernel κ] [NormedSpace ℝ E] ⦃f : α → β → E⦄ (hf : StronglyMeasurable (Function.uncurry f)) : StronglyMeasurable fun (x : α) => ∫ (y : β), f x y ∂κ x

theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_right' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {E : Type u_4} [NormedAddCommGroup E] [ProbabilityTheory.IsSFiniteKernel κ] [NormedSpace ℝ E] ⦃f : α × β → E⦄ (hf : StronglyMeasurable f) : StronglyMeasurable fun (x : α) => ∫ (y : β), f (x, y) ∂κ x

theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_right'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {a : α} {E : Type u_4} [NormedAddCommGroup E] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] [NormedSpace ℝ E] {f : β × γ → E} (hf : StronglyMeasurable f) : StronglyMeasurable fun (x : β) => ∫ (y : γ), f (x, y) ∂η (a, x)

theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {E : Type u_4} [NormedAddCommGroup E] [ProbabilityTheory.IsSFiniteKernel κ] [NormedSpace ℝ E] ⦃f : β → α → E⦄ (hf : StronglyMeasurable (Function.uncurry f)) : StronglyMeasurable fun (y : α) => ∫ (x : β), f x y ∂κ y

theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_left' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {E : Type u_4} [NormedAddCommGroup E] [ProbabilityTheory.IsSFiniteKernel κ] [NormedSpace ℝ E] ⦃f : β × α → E⦄ (hf : StronglyMeasurable f) : StronglyMeasurable fun (y : α) => ∫ (x : β), f (x, y) ∂κ y

theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_left'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {a : α} {E : Type u_4} [NormedAddCommGroup E] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] [NormedSpace ℝ E] {f : γ × β → E} (hf : StronglyMeasurable f) : StronglyMeasurable fun (y : β) => ∫ (x : γ), f (x, y) ∂η (a, y)