# Measurability of the integral against a kernel #

The Lebesgue integral of a measurable function against a kernel is measurable. The Bochner integral is strongly 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.
• 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.kernel.measurable_kernel_prod_mk_left_of_finite {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {t : Set (α × β)} (ht : ) (hκs : ∀ (a : α), ) :
Measurable fun (a : α) => (κ a) ( ⁻¹' t)

This is an auxiliary lemma for measurable_kernel_prod_mk_left.

theorem ProbabilityTheory.kernel.measurable_kernel_prod_mk_left {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {t : Set (α × β)} (ht : ) :
Measurable fun (a : α) => (κ a) ( ⁻¹' t)
theorem ProbabilityTheory.kernel.measurable_kernel_prod_mk_left' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {η : (ProbabilityTheory.kernel (α × β) γ)} {s : Set (β × γ)} (hs : ) (a : α) :
Measurable fun (b : β) => (η (a, b)) ( ⁻¹' s)
theorem ProbabilityTheory.kernel.measurable_kernel_prod_mk_right {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {s : Set (β × α)} (hs : ) :
Measurable fun (y : α) => (κ y) ((fun (x : β) => (x, y)) ⁻¹' s)
theorem ProbabilityTheory.kernel.measurable_lintegral_indicator_const {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {t : Set (α × β)} (ht : ) (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α : } {mβ : } {κ : ()} {f : αβENNReal} (hf : ) :
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α : } {mβ : } {κ : ()} {f : α × βENNReal} (hf : ) :
Measurable fun (a : α) => ∫⁻ (b : β), f (a, b)κ a
theorem Measurable.lintegral_kernel_prod_right'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {η : (ProbabilityTheory.kernel (α × β) γ)} {a : α} {f : β × γENNReal} (hf : ) :
Measurable fun (x : β) => ∫⁻ (y : γ), f (x, y)η (a, x)
theorem Measurable.set_lintegral_kernel_prod_right {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {f : αβENNReal} (hf : ) {s : Set β} (hs : ) :
Measurable fun (a : α) => ∫⁻ (b : β) in s, f a bκ a
theorem Measurable.lintegral_kernel_prod_left' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {f : β × αENNReal} (hf : ) :
Measurable fun (y : α) => ∫⁻ (x : β), f (x, y)κ y
theorem Measurable.lintegral_kernel_prod_left {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {f : βαENNReal} (hf : ) :
Measurable fun (y : α) => ∫⁻ (x : β), f x yκ y
theorem Measurable.set_lintegral_kernel_prod_left {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {f : βαENNReal} (hf : ) {s : Set β} (hs : ) :
Measurable fun (b : α) => ∫⁻ (a : β) in s, f a bκ b
theorem Measurable.lintegral_kernel {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {f : βENNReal} (hf : ) :
Measurable fun (a : α) => ∫⁻ (b : β), f bκ a
theorem Measurable.set_lintegral_kernel {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {f : βENNReal} (hf : ) {s : Set β} (hs : ) :
Measurable fun (a : α) => ∫⁻ (b : β) in s, f bκ a
theorem ProbabilityTheory.measurableSet_kernel_integrable {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {E : Type u_4} ⦃f : αβE :
MeasurableSet {x : α | MeasureTheory.Integrable (f x) (κ x)}
theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_right {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {E : Type u_4} [] ⦃f : αβE :
MeasureTheory.StronglyMeasurable fun (x : α) => ∫ (y : β), f x yκ x
theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_right' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {E : Type u_4} [] ⦃f : α × βE (hf : ) :
MeasureTheory.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α : } {mβ : } {mγ : } {η : (ProbabilityTheory.kernel (α × β) γ)} {a : α} {E : Type u_4} [] {f : β × γE} (hf : ) :
MeasureTheory.StronglyMeasurable fun (x : β) => ∫ (y : γ), f (x, y)η (a, x)
theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_left {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {E : Type u_4} [] ⦃f : βαE :
MeasureTheory.StronglyMeasurable fun (y : α) => ∫ (x : β), f x yκ y
theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_left' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {E : Type u_4} [] ⦃f : β × αE (hf : ) :
MeasureTheory.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α : } {mβ : } {mγ : } {η : (ProbabilityTheory.kernel (α × β) γ)} {a : α} {E : Type u_4} [] {f : γ × βE} (hf : ) :
MeasureTheory.StronglyMeasurable fun (y : β) => ∫ (x : γ), f (x, y)η (a, y)