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 functiona ↦ ∫⁻ b, f a b ∂(κ a)is measurable, for an s-finite kernelκ : kernel α βand a functionf : α → β → ℝ≥0∞such thatuncurry fis measurable.MeasureTheory.StronglyMeasurable.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
ProbabilityTheory.kernel.measurable_kernel_prod_mk_left_of_finite
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{t : Set (α × β)}
(ht : MeasurableSet t)
(hκs : ∀ (a : α), MeasureTheory.IsFiniteMeasure (κ a))
:
Measurable fun (a : α) => ↑↑(κ a) (Prod.mk 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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{t : Set (α × β)}
(ht : MeasurableSet t)
:
Measurable fun (a : α) => ↑↑(κ a) (Prod.mk a ⁻¹' t)
theorem
ProbabilityTheory.kernel.measurable_kernel_prod_mk_left'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{s : Set (β × γ)}
(hs : MeasurableSet s)
(a : α)
:
Measurable fun (b : β) => ↑↑(η (a, b)) (Prod.mk b ⁻¹' s)
theorem
ProbabilityTheory.kernel.measurable_kernel_prod_mk_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{s : Set (β × α)}
(hs : MeasurableSet s)
:
Measurable fun (y : α) => ↑↑(κ y) ((fun (x : β) => (x, y)) ⁻¹' s)
theorem
ProbabilityTheory.kernel.measurable_lintegral_indicator_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{t : Set (α × β)}
(ht : MeasurableSet t)
(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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{f : α → β → ENNReal}
(hf : Measurable (Function.uncurry f))
:
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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{f : α × β → ENNReal}
(hf : Measurable f)
:
Measurable fun (a : α) => ∫⁻ (b : β), f (a, b) ∂κ a
theorem
Measurable.lintegral_kernel_prod_right''
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
{a : α}
[ProbabilityTheory.IsSFiniteKernel η]
{f : β × γ → ENNReal}
(hf : Measurable f)
:
Measurable fun (x : β) => ∫⁻ (y : γ), f (x, y) ∂η (a, x)
theorem
Measurable.set_lintegral_kernel_prod_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{f : α → β → ENNReal}
(hf : Measurable (Function.uncurry f))
{s : Set β}
(hs : MeasurableSet s)
:
Measurable fun (a : α) => ∫⁻ (b : β) in s, f a b ∂κ a
theorem
Measurable.lintegral_kernel_prod_left'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{f : β × α → ENNReal}
(hf : Measurable f)
:
Measurable fun (y : α) => ∫⁻ (x : β), f (x, y) ∂κ y
theorem
Measurable.lintegral_kernel_prod_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{f : β → α → ENNReal}
(hf : Measurable (Function.uncurry f))
:
Measurable fun (y : α) => ∫⁻ (x : β), f x y ∂κ y
theorem
Measurable.set_lintegral_kernel_prod_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{f : β → α → ENNReal}
(hf : Measurable (Function.uncurry f))
{s : Set β}
(hs : MeasurableSet s)
:
Measurable fun (b : α) => ∫⁻ (a : β) in s, f a b ∂κ b
theorem
Measurable.lintegral_kernel
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{f : β → ENNReal}
(hf : Measurable f)
:
Measurable fun (a : α) => ∫⁻ (b : β), f b ∂κ a
theorem
Measurable.set_lintegral_kernel
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{f : β → ENNReal}
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
:
Measurable fun (a : α) => ∫⁻ (b : β) in s, f b ∂κ a
theorem
ProbabilityTheory.measurableSet_kernel_integrable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{E : Type u_4}
[NormedAddCommGroup E]
[ProbabilityTheory.IsSFiniteKernel κ]
⦃f : α → β → E⦄
(hf : MeasureTheory.StronglyMeasurable (Function.uncurry f))
:
MeasurableSet {x : α | MeasureTheory.Integrable (f x) (κ x)}
theorem
MeasureTheory.StronglyMeasurable.integral_kernel_prod_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[ProbabilityTheory.IsSFiniteKernel κ]
⦃f : α → β → E⦄
(hf : MeasureTheory.StronglyMeasurable (Function.uncurry f))
:
MeasureTheory.StronglyMeasurable fun (x : α) => ∫ (y : β), f x y ∂κ x
theorem
MeasureTheory.StronglyMeasurable.integral_kernel_prod_right'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[ProbabilityTheory.IsSFiniteKernel κ]
⦃f : α × β → E⦄
(hf : MeasureTheory.StronglyMeasurable f)
:
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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
{a : α}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[ProbabilityTheory.IsSFiniteKernel η]
{f : β × γ → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.StronglyMeasurable fun (x : β) => ∫ (y : γ), f (x, y) ∂η (a, x)
theorem
MeasureTheory.StronglyMeasurable.integral_kernel_prod_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[ProbabilityTheory.IsSFiniteKernel κ]
⦃f : β → α → E⦄
(hf : MeasureTheory.StronglyMeasurable (Function.uncurry f))
:
MeasureTheory.StronglyMeasurable fun (y : α) => ∫ (x : β), f x y ∂κ y
theorem
MeasureTheory.StronglyMeasurable.integral_kernel_prod_left'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[ProbabilityTheory.IsSFiniteKernel κ]
⦃f : β × α → E⦄
(hf : MeasureTheory.StronglyMeasurable f)
:
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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
{a : α}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[ProbabilityTheory.IsSFiniteKernel η]
{f : γ × β → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.StronglyMeasurable fun (y : β) => ∫ (x : γ), f (x, y) ∂η (a, y)