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 functiona ↦ ∫⁻ b, f a b ∂(κ a)is measurable, for an s-finite kernelκ : kernel α βand a functionf : α → β → ℝ≥0∞such thatuncurry fis measurable.measure_theory.strongly_measurable.integral_kernel_prod_right: the functiona ↦ ∫ b, f a b ∂(κ a)is measurable, for an s-finite kernelκ : kernel α βand a functionf : α → β → Esuch thatuncurry fis measurable.
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}
{mα : measurable_space α}
{mβ : measurable_space β}
{κ : ↥(probability_theory.kernel α β)}
[probability_theory.is_s_finite_kernel κ]
{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 (α × β) γ)}
[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) :
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) :
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) :
theorem
probability_theory.measurable_set_kernel_integrable
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{κ : ↥(probability_theory.kernel α β)}
{E : Type u_4}
[normed_add_comm_group E]
[probability_theory.is_s_finite_kernel κ]
⦃f : α → β → E⦄
(hf : measure_theory.strongly_measurable (function.uncurry f)) :
measurable_set {x : α | measure_theory.integrable (f x) (⇑κ x)}
theorem
measure_theory.strongly_measurable.integral_kernel_prod_right
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{κ : ↥(probability_theory.kernel α β)}
{E : Type u_4}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
[probability_theory.is_s_finite_kernel κ]
⦃f : α → β → E⦄
(hf : measure_theory.strongly_measurable (function.uncurry f)) :
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 β}
{κ : ↥(probability_theory.kernel α β)}
{E : Type u_4}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
[probability_theory.is_s_finite_kernel κ]
⦃f : α × β → E⦄
(hf : measure_theory.strongly_measurable f) :
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}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
[probability_theory.is_s_finite_kernel η]
{f : β × γ → E}
(hf : measure_theory.strongly_measurable f) :
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 β}
{κ : ↥(probability_theory.kernel α β)}
{E : Type u_4}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
[probability_theory.is_s_finite_kernel κ]
⦃f : β → α → E⦄
(hf : measure_theory.strongly_measurable (function.uncurry f)) :
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 β}
{κ : ↥(probability_theory.kernel α β)}
{E : Type u_4}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
[probability_theory.is_s_finite_kernel κ]
⦃f : β × α → E⦄
(hf : measure_theory.strongly_measurable f) :
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}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
[probability_theory.is_s_finite_kernel η]
{f : γ × β → E}
(hf : measure_theory.strongly_measurable f) :
measure_theory.strongly_measurable (λ (y : β), ∫ (x : γ), f (x, y) ∂⇑η (a, y))