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 (setOf fun (a : α) => MeasureTheory.Integrable f (DFunLike.coe κ 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 (setOf fun (x : α) => MeasureTheory.Integrable (f x) (DFunLike.coe κ 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 Real E]
⦃f : β → E⦄
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (x : α) => integral (DFunLike.coe κ x) fun (y : β) => f y
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 Real E]
⦃f : α → β → E⦄
(hf : StronglyMeasurable (Function.uncurry f))
:
StronglyMeasurable fun (x : α) => integral (DFunLike.coe κ x) fun (y : β) => f x y
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 Real E]
⦃f : Prod α β → E⦄
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (x : α) => integral (DFunLike.coe κ x) fun (y : β) => f { fst := x, snd := y }
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 (Prod α β) γ}
[ProbabilityTheory.IsSFiniteKernel η]
[NormedSpace Real E]
{f : Prod β γ → E}
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (x : β) =>
integral (DFunLike.coe η { fst := a, snd := x }) fun (y : γ) => f { fst := x, snd := 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 Real E]
⦃f : β → α → E⦄
(hf : StronglyMeasurable (Function.uncurry f))
:
StronglyMeasurable fun (y : α) => integral (DFunLike.coe κ y) fun (x : β) => f x 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 Real E]
⦃f : Prod β α → E⦄
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (y : α) => integral (DFunLike.coe κ y) fun (x : β) => f { fst := x, snd := y }
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 (Prod α β) γ}
[ProbabilityTheory.IsSFiniteKernel η]
[NormedSpace Real E]
{f : Prod γ β → E}
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (y : β) =>
integral (DFunLike.coe η { fst := a, snd := y }) fun (x : γ) => f { fst := x, snd := y }