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

source
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`.

source
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)
source
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)
source
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)
source
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`.

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

source
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
source
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)
source
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
source
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
source
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
source
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
source
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
source
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