Measurability of the integral against a kernel

The Lebesgue integral of a measurable function against a kernel is measurable.

Main statements

• Measurable.lintegral_kernel_prod_right: the function a ↦ ∫⁻ b, f a b ∂(κ a) is measurable, for an s-finite kernel κ : Kernel α β and a function f : α → β → ℝ≥0∞ such that uncurry f is measurable.

theorem ProbabilityTheory.Kernel.measurable_kernel_prodMk_left_of_finite {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} {t : Set (α × β)} (ht : MeasurableSet t) (hκs : ∀ (a : α), MeasureTheory.IsFiniteMeasure (κ a)) : Measurable fun (a : α) => (κ a) (Prod.mk a ⁻¹' t)

This is an auxiliary lemma for measurable_kernel_prodMk_left.

theorem ProbabilityTheory.Kernel.measurable_kernel_prodMk_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} [IsSFiniteKernel κ] {t : Set (α × β)} (ht : MeasurableSet t) : Measurable fun (a : α) => (κ a) (Prod.mk a ⁻¹' t)

theorem ProbabilityTheory.Kernel.measurable_kernel_prodMk_left' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {η : Kernel (α × β) γ} [IsSFiniteKernel η] {s : Set (β × γ)} (hs : MeasurableSet s) (a : α) : Measurable fun (b : β) => (η (a, b)) (Prod.mk b ⁻¹' s)

theorem ProbabilityTheory.Kernel.measurable_kernel_prodMk_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} [IsSFiniteKernel κ] {s : Set (β × α)} (hs : MeasurableSet s) : Measurable fun (y : α) => (κ y) ((fun (x : β) => (x, y)) ⁻¹' s)

theorem ProbabilityTheory.Kernel.measurable_lintegral_indicator_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} [IsSFiniteKernel κ] {t : Set (α × β)} (ht : MeasurableSet t) (c : ENNReal) : Measurable fun (a : α) => ∫⁻ (b : β), t.indicator (Function.const (α × β) c) (a, b) ∂κ a

Auxiliary lemma for Measurable.lintegral_kernel_prod_right.

theorem Measurable.lintegral_kernel_prod_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {f : α → β → ENNReal} (hf : Measurable (Function.uncurry f)) : Measurable fun (a : α) => ∫⁻ (b : β), f a b ∂κ a

For an s-finite kernel κ and a function f : α → β → ℝ≥0∞ which is measurable when seen as a map from α × β (hypothesis Measurable (uncurry f)), the integral a ↦ ∫⁻ b, f a b ∂(κ a) is measurable.

theorem Measurable.lintegral_kernel_prod_right' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {f : α × β → ENNReal} (hf : Measurable f) : Measurable fun (a : α) => ∫⁻ (b : β), f (a, b) ∂κ a

theorem Measurable.lintegral_kernel_prod_right'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {η : ProbabilityTheory.Kernel (α × β) γ} {a : α} [ProbabilityTheory.IsSFiniteKernel η] {f : β × γ → ENNReal} (hf : Measurable f) : Measurable fun (x : β) => ∫⁻ (y : γ), f (x, y) ∂η (a, x)

theorem Measurable.setLIntegral_kernel_prod_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {f : α → β → ENNReal} (hf : Measurable (Function.uncurry f)) {s : Set β} (hs : MeasurableSet s) : Measurable fun (a : α) => ∫⁻ (b : β) in s, f a b ∂κ a

theorem Measurable.lintegral_kernel_prod_left' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {f : β × α → ENNReal} (hf : Measurable f) : Measurable fun (y : α) => ∫⁻ (x : β), f (x, y) ∂κ y

theorem Measurable.lintegral_kernel_prod_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {f : β → α → ENNReal} (hf : Measurable (Function.uncurry f)) : Measurable fun (y : α) => ∫⁻ (x : β), f x y ∂κ y

theorem Measurable.setLIntegral_kernel_prod_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {f : β → α → ENNReal} (hf : Measurable (Function.uncurry f)) {s : Set β} (hs : MeasurableSet s) : Measurable fun (b : α) => ∫⁻ (a : β) in s, f a b ∂κ b

theorem Measurable.lintegral_kernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {f : β → ENNReal} (hf : Measurable f) : Measurable fun (a : α) => ∫⁻ (b : β), f b ∂κ a

theorem Measurable.setLIntegral_kernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {f : β → ENNReal} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) : Measurable fun (a : α) => ∫⁻ (b : β) in s, f b ∂κ a