# Documentation

Mathlib.Probability.Kernel.MeasurableIntegral

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

theorem ProbabilityTheory.kernel.measurable_kernel_prod_mk_left_of_finite {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : { x // }} {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β : } {κ : { x // }} {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γ : } {η : { x // x 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β : } {κ : { x // }} {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β : } {κ : { x // }} {t : Set (α × β)} (ht : ) (c : ENNReal) :
Measurable fun a => ∫⁻ (b : β), Set.indicator t (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β : } {κ : { x // }} {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β : } {κ : { x // }} {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γ : } {η : { x // x 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β : } {κ : { x // }} {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β : } {κ : { x // }} {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β : } {κ : { x // }} {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β : } {κ : { x // }} {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β : } {κ : { x // }} {f : βENNReal} (hf : ) :
Measurable fun a => ∫⁻ (b : β), f bκ a
theorem Measurable.set_lintegral_kernel {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : { x // }} {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β : } {κ : { x // }} {E : Type u_4} ⦃f : αβE :
theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_right {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : { x // }} {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β : } {κ : { x // }} {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γ : } {η : { x // x 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β : } {κ : { x // }} {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β : } {κ : { x // }} {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γ : } {η : { x // x ProbabilityTheory.kernel (α × β) γ }} {a : α} {E : Type u_4} [] [] {f : γ × βE} (hf : ) :
MeasureTheory.StronglyMeasurable fun y => ∫ (x : γ), f (x, y)η (a, y)