Bochner integrals of kernels

theorem ProbabilityTheory.Kernel.IsFiniteKernel.integrable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (κ : Kernel α β) [IsFiniteKernel κ] {s : Set β} (hs : MeasurableSet s) : MeasureTheory.Integrable (fun (x : α) => (κ x).real s) μ

theorem ProbabilityTheory.Kernel.IsMarkovKernel.integrable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (κ : Kernel α β) [IsMarkovKernel κ] {s : Set β} (hs : MeasurableSet s) : MeasureTheory.Integrable (fun (x : α) => (κ x).real s) μ

theorem ProbabilityTheory.Kernel.integral_congr_ae₂ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : α → β → E} {μ : MeasureTheory.Measure α} (h : ∀ᵐ (a : α) ∂μ, f a =ᵐ[κ a] g a) : ∫ (a : α), ∫ (b : β), f a b ∂κ a ∂μ = ∫ (a : α), ∫ (b : β), g a b ∂κ a ∂μ

theorem ProbabilityTheory.Kernel.integral_indicator₂ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : α → β → E) (s : Set α) (a : α) : ∫ (y : β), s.indicator (fun (x : α) => f x y) a ∂κ a = s.indicator (fun (x : α) => ∫ (y : β), f x y ∂κ x) a

theorem ProbabilityTheory.Kernel.integral_deterministic' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : β → E} {a : α} [CompleteSpace E] {g : α → β} (hg : Measurable g) (hf : MeasureTheory.StronglyMeasurable f) : ∫ (x : β), f x ∂(deterministic g hg) a = f (g a)

@[simp]

theorem ProbabilityTheory.Kernel.integral_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : β → E} {a : α} [CompleteSpace E] {g : α → β} [MeasurableSingletonClass β] (hg : Measurable g) : ∫ (x : β), f x ∂(deterministic g hg) a = f (g a)

theorem ProbabilityTheory.Kernel.setIntegral_deterministic' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : β → E} {a : α} [CompleteSpace E] {g : α → β} (hg : Measurable g) (hf : MeasureTheory.StronglyMeasurable f) {s : Set β} (hs : MeasurableSet s) [Decidable (g a ∈ s)] : ∫ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0

@[simp]

theorem ProbabilityTheory.Kernel.setIntegral_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : β → E} {a : α} [CompleteSpace E] {g : α → β} [MeasurableSingletonClass β] (hg : Measurable g) (s : Set β) [Decidable (g a ∈ s)] : ∫ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0

@[simp]

theorem ProbabilityTheory.Kernel.integral_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : β → E} {a : α} {μ : MeasureTheory.Measure β} : ∫ (x : β), f x ∂(const α μ) a = ∫ (x : β), f x ∂μ

@[simp]

theorem ProbabilityTheory.Kernel.setIntegral_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : β → E} {a : α} {μ : MeasureTheory.Measure β} {s : Set β} : ∫ (x : β) in s, f x ∂(const α μ) a = ∫ (x : β) in s, f x ∂μ

@[simp]

theorem ProbabilityTheory.Kernel.integral_restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : β → E} {a : α} {s : Set β} (hs : MeasurableSet s) : ∫ (x : β), f x ∂(κ.restrict hs) a = ∫ (x : β) in s, f x ∂κ a

@[simp]

theorem ProbabilityTheory.Kernel.setIntegral_restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : β → E} {a : α} {s : Set β} (hs : MeasurableSet s) (t : Set β) : ∫ (x : β) in t, f x ∂(κ.restrict hs) a = ∫ (x : β) in t ∩ s, f x ∂κ a

theorem ProbabilityTheory.Kernel.integral_piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {η : Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] (a : α) (g : β → E) : ∫ (b : β), g b ∂(piecewise hs κ η) a = if a ∈ s then ∫ (b : β), g b ∂κ a else ∫ (b : β), g b ∂η a

theorem ProbabilityTheory.Kernel.setIntegral_piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {η : Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] (a : α) (g : β → E) (t : Set β) : ∫ (b : β) in t, g b ∂(piecewise hs κ η) a = if a ∈ s then ∫ (b : β) in t, g b ∂κ a else ∫ (b : β) in t, g b ∂η a