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_integrable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : Kernel α β}
{E : Type u_4}
[NormedAddCommGroup E]
⦃f : β → E⦄
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasurableSet {a : α | MeasureTheory.Integrable f (κ a)}
theorem
ProbabilityTheory.measurableSet_kernel_integrable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : Kernel α β}
{E : Type u_4}
[NormedAddCommGroup E]
[IsSFiniteKernel κ]
⦃f : α → β → E⦄
(hf : MeasureTheory.StronglyMeasurable (Function.uncurry f))
:
MeasurableSet {x : α | MeasureTheory.Integrable (f x) (κ x)}
theorem
MeasureTheory.StronglyMeasurable.integral_kernel
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
⦃f : β → E⦄
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (x : α) => ∫ (y : β), f 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 : StronglyMeasurable (Function.uncurry f))
:
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 : StronglyMeasurable f)
:
theorem
MeasureTheory.StronglyMeasurable.integral_kernel_prod_right''
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{a : α}
{E : Type u_4}
[NormedAddCommGroup E]
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsSFiniteKernel η]
[NormedSpace ℝ E]
{f : β × γ → E}
(hf : StronglyMeasurable f)
:
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 : StronglyMeasurable (Function.uncurry f))
:
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 : StronglyMeasurable f)
:
theorem
MeasureTheory.StronglyMeasurable.integral_kernel_prod_left''
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{a : α}
{E : Type u_4}
[NormedAddCommGroup E]
{η : ProbabilityTheory.Kernel (α × β) γ}
[ProbabilityTheory.IsSFiniteKernel η]
[NormedSpace ℝ E]
{f : γ × β → E}
(hf : StronglyMeasurable f)
: