Documentation

Mathlib.Probability.Kernel.Integral

Bochner integrals of kernels #

source
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) s).toReal) μ
source
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) s).toReal) μ
source
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 ∂μ
source
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)
source
@[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)
source
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
source
@[deprecated ProbabilityTheory.Kernel.setIntegral_deterministic' (since := "2024-04-17")]
theorem ProbabilityTheory.Kernel.set_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) {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

Alias of ProbabilityTheory.Kernel.setIntegral_deterministic'.

source
@[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
source
@[deprecated ProbabilityTheory.Kernel.setIntegral_deterministic (since := "2024-04-17")]
theorem ProbabilityTheory.Kernel.set_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) (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

Alias of ProbabilityTheory.Kernel.setIntegral_deterministic.

source
@[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 ∂μ
source
@[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 ∂μ
source
@[deprecated ProbabilityTheory.Kernel.setIntegral_const (since := "2024-04-17")]
theorem ProbabilityTheory.Kernel.set_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 β} {s : Set β} :
∫ (x : β) in s, f x ∂(const α μ) a = ∫ (x : β) in s, f x ∂μ

Alias of ProbabilityTheory.Kernel.setIntegral_const.

source
@[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
source
@[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
source
@[deprecated ProbabilityTheory.Kernel.setIntegral_restrict (since := "2024-04-17")]
theorem ProbabilityTheory.Kernel.set_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) (t : Set β) :
∫ (x : β) in t, f x ∂(κ.restrict hs) a = ∫ (x : β) in t ∩ s, f x ∂κ a

Alias of ProbabilityTheory.Kernel.setIntegral_restrict.

source
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
source
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
source
@[deprecated ProbabilityTheory.Kernel.setIntegral_piecewise (since := "2024-04-17")]
theorem ProbabilityTheory.Kernel.set_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) (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

Alias of ProbabilityTheory.Kernel.setIntegral_piecewise.