# mathlib3documentation

probability.kernel.measurable_integral

# Measurability of the integral against a kernel #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
• measure_theory.strongly_measurable.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 probability_theory.kernel.measurable_kernel_prod_mk_left_of_finite {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {t : set × β)} (ht : measurable_set t) (hκs : (a : α), ) :
measurable (λ (a : α), (κ a) (prod.mk a ⁻¹' t))

This is an auxiliary lemma for measurable_kernel_prod_mk_left.

theorem probability_theory.kernel.measurable_kernel_prod_mk_left {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {t : set × β)} (ht : measurable_set t) :
measurable (λ (a : α), (κ a) (prod.mk a ⁻¹' t))
theorem probability_theory.kernel.measurable_kernel_prod_mk_left' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {η : (probability_theory.kernel × β) γ)} {s : set × γ)} (hs : measurable_set s) (a : α) :
measurable (λ (b : β), (η (a, b)) (prod.mk b ⁻¹' s))
theorem probability_theory.kernel.measurable_kernel_prod_mk_right {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {s : set × α)} (hs : measurable_set s) :
measurable (λ (y : α), (κ y) ((λ (x : β), (x, y)) ⁻¹' s))
theorem probability_theory.kernel.measurable_lintegral_indicator_const {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {t : set × β)} (ht : measurable_set t) (c : ennreal) :
measurable (λ (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α : measurable_space α} {mβ : measurable_space β} {κ : } {f : α } (hf : measurable ) :
measurable (λ (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α : measurable_space α} {mβ : measurable_space β} {κ : } {f : α × β ennreal} (hf : measurable f) :
measurable (λ (a : α), ∫⁻ (b : β), f (a, b) κ a)
theorem measurable.lintegral_kernel_prod_right'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {η : (probability_theory.kernel × β) γ)} {a : α} {f : β × γ ennreal} (hf : measurable f) :
measurable (λ (x : β), ∫⁻ (y : γ), f (x, y) η (a, x))
theorem measurable.set_lintegral_kernel_prod_right {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {f : α } (hf : measurable ) {s : set β} (hs : measurable_set s) :
measurable (λ (a : α), ∫⁻ (b : β) in s, f a b κ a)
theorem measurable.lintegral_kernel_prod_left' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {f : β × α ennreal} (hf : measurable f) :
measurable (λ (y : α), ∫⁻ (x : β), f (x, y) κ y)
theorem measurable.lintegral_kernel_prod_left {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {f : β } (hf : measurable ) :
measurable (λ (y : α), ∫⁻ (x : β), f x y κ y)
theorem measurable.set_lintegral_kernel_prod_left {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {f : β } (hf : measurable ) {s : set β} (hs : measurable_set s) :
measurable (λ (b : α), ∫⁻ (a : β) in s, f a b κ b)
theorem measurable.lintegral_kernel {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {f : β ennreal} (hf : measurable f) :
measurable (λ (a : α), ∫⁻ (b : β), f b κ a)
theorem measurable.set_lintegral_kernel {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {f : β ennreal} (hf : measurable f) {s : set β} (hs : measurable_set s) :
measurable (λ (a : α), ∫⁻ (b : β) in s, f b κ a)
theorem probability_theory.measurable_set_kernel_integrable {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {E : Type u_4} ⦃f : α β E  :
measurable_set {x : α | (κ x)}
theorem measure_theory.strongly_measurable.integral_kernel_prod_right {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {E : Type u_4} [ E] ⦃f : α β E  :
measure_theory.strongly_measurable (λ (x : α), (y : β), f x y κ x)
theorem measure_theory.strongly_measurable.integral_kernel_prod_right' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {E : Type u_4} [ E] ⦃f : α × β E⦄  :
measure_theory.strongly_measurable (λ (x : α), (y : β), f (x, y) κ x)
theorem measure_theory.strongly_measurable.integral_kernel_prod_right'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {η : (probability_theory.kernel × β) γ)} {a : α} {E : Type u_4} [ E] {f : β × γ E}  :
measure_theory.strongly_measurable (λ (x : β), (y : γ), f (x, y) η (a, x))
theorem measure_theory.strongly_measurable.integral_kernel_prod_left {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {E : Type u_4} [ E] ⦃f : β α E  :
measure_theory.strongly_measurable (λ (y : α), (x : β), f x y κ y)
theorem measure_theory.strongly_measurable.integral_kernel_prod_left' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {E : Type u_4} [ E] ⦃f : β × α E⦄  :
measure_theory.strongly_measurable (λ (y : α), (x : β), f (x, y) κ y)
theorem measure_theory.strongly_measurable.integral_kernel_prod_left'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {η : (probability_theory.kernel × β) γ)} {a : α} {E : Type u_4} [ E] {f : γ × β E}  :
measure_theory.strongly_measurable (λ (y : β), (x : γ), f (x, y) η (a, y))