Bochner integrals of kernels #
theorem
ProbabilityTheory.Kernel.IsFiniteKernel.integrable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
{s : Set β}
(hs : MeasurableSet s)
:
MeasureTheory.Integrable (fun (x : α) => ((κ x) s).toReal) μ
theorem
ProbabilityTheory.Kernel.IsMarkovKernel.integrable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
{s : Set β}
(hs : MeasurableSet s)
:
MeasureTheory.Integrable (fun (x : α) => ((κ x) s).toReal) μ
theorem
ProbabilityTheory.Kernel.integral_congr_ae₂
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → β → E}
{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_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 ∂(ProbabilityTheory.Kernel.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 ∂(ProbabilityTheory.Kernel.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 ∂(ProbabilityTheory.Kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
@[deprecated ProbabilityTheory.Kernel.setIntegral_deterministic']
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 ∂(ProbabilityTheory.Kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
Alias of ProbabilityTheory.Kernel.setIntegral_deterministic'.
@[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 ∂(ProbabilityTheory.Kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
@[deprecated ProbabilityTheory.Kernel.setIntegral_deterministic]
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 ∂(ProbabilityTheory.Kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
Alias of ProbabilityTheory.Kernel.setIntegral_deterministic.
@[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 ∂(ProbabilityTheory.Kernel.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 ∂(ProbabilityTheory.Kernel.const α μ) a = ∫ (x : β) in s, f x ∂μ
@[deprecated ProbabilityTheory.Kernel.setIntegral_const]
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 ∂(ProbabilityTheory.Kernel.const α μ) a = ∫ (x : β) in s, f x ∂μ
@[simp]
theorem
ProbabilityTheory.Kernel.integral_restrict
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.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 β}
{κ : ProbabilityTheory.Kernel α β}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : β → E}
{a : α}
{s : Set β}
(hs : MeasurableSet s)
(t : Set β)
:
@[deprecated ProbabilityTheory.Kernel.setIntegral_restrict]
theorem
ProbabilityTheory.Kernel.set_integral_restrict
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : β → E}
{a : α}
{s : Set β}
(hs : MeasurableSet s)
(t : Set β)
:
theorem
ProbabilityTheory.Kernel.integral_piecewise
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{η : ProbabilityTheory.Kernel α β}
{s : Set α}
{hs : MeasurableSet s}
[DecidablePred fun (x : α) => x ∈ s]
(a : α)
(g : β → E)
:
∫ (b : β), g b ∂(ProbabilityTheory.Kernel.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 β}
{κ : ProbabilityTheory.Kernel α β}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{η : ProbabilityTheory.Kernel α β}
{s : Set α}
{hs : MeasurableSet s}
[DecidablePred fun (x : α) => x ∈ s]
(a : α)
(g : β → E)
(t : Set β)
:
∫ (b : β) in t, g b ∂(ProbabilityTheory.Kernel.piecewise hs κ η) a = if a ∈ s then ∫ (b : β) in t, g b ∂κ a else ∫ (b : β) in t, g b ∂η a
@[deprecated ProbabilityTheory.Kernel.setIntegral_piecewise]
theorem
ProbabilityTheory.Kernel.set_integral_piecewise
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{η : ProbabilityTheory.Kernel α β}
{s : Set α}
{hs : MeasurableSet s}
[DecidablePred fun (x : α) => x ∈ s]
(a : α)
(g : β → E)
(t : Set β)
:
∫ (b : β) in t, g b ∂(ProbabilityTheory.Kernel.piecewise hs κ η) a = if a ∈ s then ∫ (b : β) in t, g b ∂κ a else ∫ (b : β) in t, g b ∂η a