mathlib3 documentation

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 #

theorem probability_theory.kernel.measurable_kernel_prod_mk_left_of_finite {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : (probability_theory.kernel α β)} {t : set × β)} (ht : measurable_set t) (hκs : (a : α), measure_theory.is_finite_measure (κ 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} {γ : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {η : (probability_theory.kernel × β) γ)} [probability_theory.is_s_finite_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 β} {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {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 β} {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {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 β} {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {f : α β ennreal} (hf : measurable (function.uncurry f)) :
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 β} {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {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 : α} [probability_theory.is_s_finite_kernel η] {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 β} {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {f : α β ennreal} (hf : measurable (function.uncurry f)) {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 β} {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {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 β} {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {f : β α ennreal} (hf : measurable (function.uncurry f)) :
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 β} {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {f : β α ennreal} (hf : measurable (function.uncurry f)) {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 β} {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {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 β} {κ : (probability_theory.kernel α β)} [probability_theory.is_s_finite_kernel κ] {f : β ennreal} (hf : measurable f) {s : set β} (hs : measurable_set s) :
measurable (λ (a : α), ∫⁻ (b : β) in s, f b κ a)