Documentation

Mathlib.Probability.Kernel.MeasurableIntegral

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 #

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 : β), Set.indicator t (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 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] [CompleteSpace 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] [CompleteSpace 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] [CompleteSpace 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] [CompleteSpace 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] [CompleteSpace 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] [CompleteSpace E] [ProbabilityTheory.IsSFiniteKernel η] {f : γ × βE} (hf : MeasureTheory.StronglyMeasurable f) :
MeasureTheory.StronglyMeasurable fun (y : β) => ∫ (x : γ), f (x, y)η (a, y)