Measurability of the integral against a kernel #
The Bochner integral of a strongly measurable function against a kernel is strongly measurable.
Main statements #
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.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]
[ProbabilityTheory.IsSFiniteKernel κ]
[NormedSpace ℝ E]
⦃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]
[ProbabilityTheory.IsSFiniteKernel κ]
[NormedSpace ℝ E]
⦃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]
[ProbabilityTheory.IsSFiniteKernel η]
[NormedSpace ℝ E]
{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]
[ProbabilityTheory.IsSFiniteKernel κ]
[NormedSpace ℝ E]
⦃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]
[ProbabilityTheory.IsSFiniteKernel κ]
[NormedSpace ℝ E]
⦃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]
[ProbabilityTheory.IsSFiniteKernel η]
[NormedSpace ℝ E]
{f : γ × β → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.StronglyMeasurable fun (y : β) => ∫ (x : γ), f (x, y) ∂η (a, y)