Markov Kernels

A kernel from a measurable space α to another measurable space β is a measurable map α → MeasureTheory.Measure β, where the measurable space instance on measure β is the one defined in MeasureTheory.Measure.instMeasurableSpace. That is, a kernel κ verifies that for all measurable sets s of β, a ↦ κ a s is measurable.

Main definitions

Classes of kernels:

• ProbabilityTheory.kernel α β: kernels from α to β, defined as the AddSubmonoid of the measurable functions in α → Measure β.
• ProbabilityTheory.IsMarkovKernel κ: a kernel from α to β is said to be a Markov kernel if for all a : α, k a is a probability measure.
• ProbabilityTheory.IsFiniteKernel κ: a kernel from α to β is said to be finite if there exists C : ℝ≥0∞ such that C < ∞ and for all a : α, κ a univ ≤ C. This implies in particular that all measures in the image of κ are finite, but is stronger since it requires a uniform bound. This stronger condition is necessary to ensure that the composition of two finite kernels is finite.
• ProbabilityTheory.IsSFiniteKernel κ: a kernel is called s-finite if it is a countable sum of finite kernels.

Particular kernels:

• ProbabilityTheory.kernel.deterministic (f : α → β) (hf : Measurable f): kernel a ↦ Measure.dirac (f a).
• ProbabilityTheory.kernel.const α (μβ : measure β): constant kernel a ↦ μβ.
• ProbabilityTheory.kernel.restrict κ (hs : MeasurableSet s): kernel for which the image of a : α is (κ a).restrict s. Integral: ∫⁻ b, f b ∂(kernel.restrict κ hs a) = ∫⁻ b in s, f b ∂(κ a)

Main statements

• ProbabilityTheory.kernel.ext_fun: if ∫⁻ b, f b ∂(κ a) = ∫⁻ b, f b ∂(η a) for all measurable functions f and all a, then the two kernels κ and η are equal.

noncomputable def ProbabilityTheory.kernel (α : Type u_1) (β : Type u_2) [MeasurableSpace α] [MeasurableSpace β] : AddSubmonoid (α → MeasureTheory.Measure β)

A kernel from a measurable space α to another measurable space β is a measurable function κ : α → Measure β. The measurable space structure on MeasureTheory.Measure β is given by MeasureTheory.Measure.instMeasurableSpace. A map κ : α → MeasureTheory.Measure β is measurable iff ∀ s : Set β, MeasurableSet s → Measurable (fun a ↦ κ a s).

Equations

• ProbabilityTheory.kernel α β = { toAddSubsemigroup := { carrier := Measurable, add_mem' := ⋯ }, zero_mem' := ⋯ }

instance ProbabilityTheory.instFunLikeSubtypeForAllMeasureMemAddSubmonoidAddZeroClassToAddZeroClassToAddMonoidInstAddCommMonoidInstMembershipInstSetLikeAddSubmonoidKernel {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] : FunLike (↥(ProbabilityTheory.kernel α β)) α (MeasureTheory.Measure β)

Equations

• One or more equations did not get rendered due to their size.

instance ProbabilityTheory.kernel.instCovariantAddLE {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] : CovariantClass (↥(ProbabilityTheory.kernel α β)) (↥(ProbabilityTheory.kernel α β)) (fun (x x_1 : ↥(ProbabilityTheory.kernel α β)) => x + x_1) fun (x x_1 : ↥(ProbabilityTheory.kernel α β)) => x ≤ x_1

Equations

• ⋯ = ⋯

noncomputable instance ProbabilityTheory.kernel.instOrderBot {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] : OrderBot ↥(ProbabilityTheory.kernel α β)

Equations

• ProbabilityTheory.kernel.instOrderBot = OrderBot.mk ⋯

@[simp]

theorem ProbabilityTheory.kernel.coeFn_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : ⇑0 = 0

@[simp]

theorem ProbabilityTheory.kernel.coeFn_add {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) (η : ↥(ProbabilityTheory.kernel α β)) : ⇑(κ + η) = ⇑κ + ⇑η

def ProbabilityTheory.kernel.coeAddHom (α : Type u_4) (β : Type u_5) [MeasurableSpace α] [MeasurableSpace β] : ↥(ProbabilityTheory.kernel α β) →+ α → MeasureTheory.Measure β

Coercion to a function as an additive monoid homomorphism.

Equations

• ProbabilityTheory.kernel.coeAddHom α β = AddSubmonoid.subtype (ProbabilityTheory.kernel α β)

@[simp]

theorem ProbabilityTheory.kernel.zero_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (a : α) : 0 a = 0

@[simp]

theorem ProbabilityTheory.kernel.coe_finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (I : Finset ι) (κ : ι → ↥(ProbabilityTheory.kernel α β)) : ⇑(Finset.sum I fun (i : ι) => κ i) = Finset.sum I fun (i : ι) => ⇑(κ i)

theorem ProbabilityTheory.kernel.finset_sum_apply {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (I : Finset ι) (κ : ι → ↥(ProbabilityTheory.kernel α β)) (a : α) : (Finset.sum I fun (i : ι) => κ i) a = Finset.sum I fun (i : ι) => (κ i) a

theorem ProbabilityTheory.kernel.finset_sum_apply' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (I : Finset ι) (κ : ι → ↥(ProbabilityTheory.kernel α β)) (a : α) (s : Set β) : ↑↑((Finset.sum I fun (i : ι) => κ i) a) s = Finset.sum I fun (i : ι) => ↑↑((κ i) a) s

class ProbabilityTheory.IsMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) : Prop

A kernel is a Markov kernel if every measure in its image is a probability measure.

• isProbabilityMeasure : ∀ (a : α), MeasureTheory.IsProbabilityMeasure (κ a)

class ProbabilityTheory.IsFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) : Prop

A kernel is finite if every measure in its image is finite, with a uniform bound.

• exists_univ_le : ∃ C < ⊤, ∀ (a : α), ↑↑(κ a) Set.univ ≤ C

noncomputable def ProbabilityTheory.IsFiniteKernel.bound {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) [h : ProbabilityTheory.IsFiniteKernel κ] : ENNReal

A constant C : ℝ≥0∞ such that C < ∞ (ProbabilityTheory.IsFiniteKernel.bound_lt_top κ) and for all a : α and s : Set β, κ a s ≤ C (ProbabilityTheory.kernel.measure_le_bound κ a s).

Porting note (#11215): TODO: does it make sense to -- make ProbabilityTheory.IsFiniteKernel.bound the least possible bound? -- Should it be an NNReal number?

Equations

• ProbabilityTheory.IsFiniteKernel.bound κ = Exists.choose ⋯

theorem ProbabilityTheory.IsFiniteKernel.bound_lt_top {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) [h : ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsFiniteKernel.bound κ < ⊤

theorem ProbabilityTheory.IsFiniteKernel.bound_ne_top {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsFiniteKernel.bound κ ≠ ⊤

theorem ProbabilityTheory.kernel.measure_le_bound {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) [h : ProbabilityTheory.IsFiniteKernel κ] (a : α) (s : Set β) : ↑↑(κ a) s ≤ ProbabilityTheory.IsFiniteKernel.bound κ

instance ProbabilityTheory.isFiniteKernel_zero (α : Type u_4) (β : Type u_5) {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : ProbabilityTheory.IsFiniteKernel 0

Equations

• ⋯ = ⋯

instance ProbabilityTheory.IsFiniteKernel.add {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) (η : ↥(ProbabilityTheory.kernel α β)) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.IsFiniteKernel (κ + η)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.isFiniteKernel_of_le {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} {ν : ↥(ProbabilityTheory.kernel α β)} [hν : ProbabilityTheory.IsFiniteKernel ν] (hκν : κ ≤ ν) : ProbabilityTheory.IsFiniteKernel κ

instance ProbabilityTheory.IsMarkovKernel.is_probability_measure' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} [ProbabilityTheory.IsMarkovKernel κ] (a : α) : MeasureTheory.IsProbabilityMeasure (κ a)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.IsFiniteKernel.isFiniteMeasure {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} [ProbabilityTheory.IsFiniteKernel κ] (a : α) : MeasureTheory.IsFiniteMeasure (κ a)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.IsMarkovKernel.isFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.IsFiniteKernel κ

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.kernel.ext {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} {η : ↥(ProbabilityTheory.kernel α β)} (h : ∀ (a : α), κ a = η a) : κ = η

theorem ProbabilityTheory.kernel.ext_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} {η : ↥(ProbabilityTheory.kernel α β)} : κ = η ↔ ∀ (a : α), κ a = η a

theorem ProbabilityTheory.kernel.ext_iff' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} {η : ↥(ProbabilityTheory.kernel α β)} : κ = η ↔ ∀ (a : α) (s : Set β), MeasurableSet s → ↑↑(κ a) s = ↑↑(η a) s

theorem ProbabilityTheory.kernel.ext_fun {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} {η : ↥(ProbabilityTheory.kernel α β)} (h : ∀ (a : α) (f : β → ENNReal), Measurable f → ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a) : κ = η

theorem ProbabilityTheory.kernel.ext_fun_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} {η : ↥(ProbabilityTheory.kernel α β)} : κ = η ↔ ∀ (a : α) (f : β → ENNReal), Measurable f → ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a

theorem ProbabilityTheory.kernel.measurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) : Measurable ⇑κ

theorem ProbabilityTheory.kernel.measurable_coe {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) {s : Set β} (hs : MeasurableSet s) : Measurable fun (a : α) => ↑↑(κ a) s

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) μ

noncomputable def ProbabilityTheory.kernel.sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (κ : ι → ↥(ProbabilityTheory.kernel α β)) : ↥(ProbabilityTheory.kernel α β)

Sum of an indexed family of kernels.

Equations

• ProbabilityTheory.kernel.sum κ = { val := fun (a : α) => MeasureTheory.Measure.sum fun (n : ι) => (κ n) a, property := ⋯ }

theorem ProbabilityTheory.kernel.sum_apply {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (κ : ι → ↥(ProbabilityTheory.kernel α β)) (a : α) : (ProbabilityTheory.kernel.sum κ) a = MeasureTheory.Measure.sum fun (n : ι) => (κ n) a

theorem ProbabilityTheory.kernel.sum_apply' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (κ : ι → ↥(ProbabilityTheory.kernel α β)) (a : α) {s : Set β} (hs : MeasurableSet s) : ↑↑((ProbabilityTheory.kernel.sum κ) a) s = ∑' (n : ι), ↑↑((κ n) a) s

@[simp]

theorem ProbabilityTheory.kernel.sum_zero {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] : (ProbabilityTheory.kernel.sum fun (x : ι) => 0) = 0

theorem ProbabilityTheory.kernel.sum_comm {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (κ : ι → ι → ↥(ProbabilityTheory.kernel α β)) : (ProbabilityTheory.kernel.sum fun (n : ι) => ProbabilityTheory.kernel.sum (κ n)) = ProbabilityTheory.kernel.sum fun (m : ι) => ProbabilityTheory.kernel.sum fun (n : ι) => κ n m

@[simp]

theorem ProbabilityTheory.kernel.sum_fintype {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Fintype ι] (κ : ι → ↥(ProbabilityTheory.kernel α β)) : ProbabilityTheory.kernel.sum κ = Finset.sum Finset.univ fun (i : ι) => κ i

theorem ProbabilityTheory.kernel.sum_add {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (κ : ι → ↥(ProbabilityTheory.kernel α β)) (η : ι → ↥(ProbabilityTheory.kernel α β)) : (ProbabilityTheory.kernel.sum fun (n : ι) => κ n + η n) = ProbabilityTheory.kernel.sum κ + ProbabilityTheory.kernel.sum η

class ProbabilityTheory.IsSFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) : Prop

A kernel is s-finite if it can be written as the sum of countably many finite kernels.

• tsum_finite : ∃ (κs : ℕ → ↥(ProbabilityTheory.kernel α β)), (∀ (n : ℕ), ProbabilityTheory.IsFiniteKernel (κs n)) ∧ κ = ProbabilityTheory.kernel.sum κs

instance ProbabilityTheory.kernel.IsFiniteKernel.isSFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} [h : ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsSFiniteKernel κ

Equations

• ⋯ = ⋯

noncomputable def ProbabilityTheory.kernel.seq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) [h : ProbabilityTheory.IsSFiniteKernel κ] : ℕ → ↥(ProbabilityTheory.kernel α β)

A sequence of finite kernels such that κ = ProbabilityTheory.kernel.sum (seq κ). See ProbabilityTheory.kernel.isFiniteKernel_seq and ProbabilityTheory.kernel.kernel_sum_seq.

Equations

• ProbabilityTheory.kernel.seq κ = Exists.choose ⋯

theorem ProbabilityTheory.kernel.kernel_sum_seq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) [h : ProbabilityTheory.IsSFiniteKernel κ] : ProbabilityTheory.kernel.sum (ProbabilityTheory.kernel.seq κ) = κ

theorem ProbabilityTheory.kernel.measure_sum_seq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) [h : ProbabilityTheory.IsSFiniteKernel κ] (a : α) : (MeasureTheory.Measure.sum fun (n : ℕ) => (ProbabilityTheory.kernel.seq κ n) a) = κ a

instance ProbabilityTheory.kernel.isFiniteKernel_seq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) [h : ProbabilityTheory.IsSFiniteKernel κ] (n : ℕ) : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.seq κ n)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.kernel.IsSFiniteKernel.sFinite {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} [ProbabilityTheory.IsSFiniteKernel κ] (a : α) : MeasureTheory.SFinite (κ a)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.kernel.IsSFiniteKernel.add {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) (η : ↥(ProbabilityTheory.kernel α β)) [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η] : ProbabilityTheory.IsSFiniteKernel (κ + η)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.kernel.IsSFiniteKernel.finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κs : ι → ↥(ProbabilityTheory.kernel α β)} (I : Finset ι) (h : ∀ i ∈ I, ProbabilityTheory.IsSFiniteKernel (κs i)) : ProbabilityTheory.IsSFiniteKernel (Finset.sum I fun (i : ι) => κs i)

theorem ProbabilityTheory.kernel.isSFiniteKernel_sum_of_denumerable {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Denumerable ι] {κs : ι → ↥(ProbabilityTheory.kernel α β)} (hκs : ∀ (n : ι), ProbabilityTheory.IsSFiniteKernel (κs n)) : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.sum κs)

theorem ProbabilityTheory.kernel.isSFiniteKernel_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] {κs : ι → ↥(ProbabilityTheory.kernel α β)} (hκs : ∀ (n : ι), ProbabilityTheory.IsSFiniteKernel (κs n)) : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.sum κs)

noncomputable def ProbabilityTheory.kernel.deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β) (hf : Measurable f) : ↥(ProbabilityTheory.kernel α β)

Kernel which to a associates the dirac measure at f a. This is a Markov kernel.

Equations

• ProbabilityTheory.kernel.deterministic f hf = { val := fun (a : α) => MeasureTheory.Measure.dirac (f a), property := ⋯ }

theorem ProbabilityTheory.kernel.deterministic_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) (a : α) : (ProbabilityTheory.kernel.deterministic f hf) a = MeasureTheory.Measure.dirac (f a)

theorem ProbabilityTheory.kernel.deterministic_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) (a : α) {s : Set β} (hs : MeasurableSet s) : ↑↑((ProbabilityTheory.kernel.deterministic f hf) a) s = Set.indicator s (fun (x : β) => 1) (f a)

instance ProbabilityTheory.kernel.isMarkovKernel_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.deterministic f hf)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.kernel.lintegral_deterministic' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} {a : α} (hg : Measurable g) (hf : Measurable f) : ∫⁻ (x : β), f x ∂(ProbabilityTheory.kernel.deterministic g hg) a = f (g a)

@[simp]

theorem ProbabilityTheory.kernel.lintegral_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} {a : α} (hg : Measurable g) [MeasurableSingletonClass β] : ∫⁻ (x : β), f x ∂(ProbabilityTheory.kernel.deterministic g hg) a = f (g a)

theorem ProbabilityTheory.kernel.set_lintegral_deterministic' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} {a : α} (hg : Measurable g) (hf : Measurable 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

@[simp]

theorem ProbabilityTheory.kernel.set_lintegral_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} {a : α} (hg : Measurable g) [MeasurableSingletonClass β] (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

theorem ProbabilityTheory.kernel.integral_deterministic' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : β → E} {g : α → β} {a : α} (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_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : β → E} {g : α → β} {a : α} (hg : Measurable g) [MeasurableSingletonClass β] : ∫ (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_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : β → E} {g : α → β} {a : α} (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_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : β → E} {g : α → β} {a : α} (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_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : β → E} {g : α → β} {a : α} (hg : Measurable g) [MeasurableSingletonClass β] (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_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : β → E} {g : α → β} {a : α} (hg : Measurable g) [MeasurableSingletonClass β] (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.

def ProbabilityTheory.kernel.const (α : Type u_4) {β : Type u_5} [MeasurableSpace α] : {x : MeasurableSpace β} → MeasureTheory.Measure β → ↥(ProbabilityTheory.kernel α β)

Constant kernel, which always returns the same measure.

Equations

• ProbabilityTheory.kernel.const α μβ = { val := fun (x : α) => μβ, property := ⋯ }

@[simp]

theorem ProbabilityTheory.kernel.const_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μβ : MeasureTheory.Measure β) (a : α) : (ProbabilityTheory.kernel.const α μβ) a = μβ

@[simp]

theorem ProbabilityTheory.kernel.const_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : ProbabilityTheory.kernel.const α 0 = 0

theorem ProbabilityTheory.kernel.const_add {α : Type u_1} {mα : MeasurableSpace α} (β : Type u_4) [MeasurableSpace β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : ProbabilityTheory.kernel.const β (μ + ν) = ProbabilityTheory.kernel.const β μ + ProbabilityTheory.kernel.const β ν

theorem ProbabilityTheory.kernel.sum_const {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (μ : ι → MeasureTheory.Measure β) : (ProbabilityTheory.kernel.sum fun (n : ι) => ProbabilityTheory.kernel.const α (μ n)) = ProbabilityTheory.kernel.const α (MeasureTheory.Measure.sum μ)

instance ProbabilityTheory.kernel.isFiniteKernel_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β} [MeasureTheory.IsFiniteMeasure μβ] : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.const α μβ)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.kernel.isSFiniteKernel_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β} [MeasureTheory.SFinite μβ] : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.const α μβ)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.kernel.isMarkovKernel_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β} [hμβ : MeasureTheory.IsProbabilityMeasure μβ] : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.const α μβ)

Equations

• ⋯ = ⋯

@[simp]

theorem ProbabilityTheory.kernel.lintegral_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {μ : MeasureTheory.Measure β} {a : α} : ∫⁻ (x : β), f x ∂(ProbabilityTheory.kernel.const α μ) a = ∫⁻ (x : β), f x ∂μ

@[simp]

theorem ProbabilityTheory.kernel.set_lintegral_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {μ : MeasureTheory.Measure β} {a : α} {s : Set β} : ∫⁻ (x : β) in s, f x ∂(ProbabilityTheory.kernel.const α μ) a = ∫⁻ (x : β) in s, f x ∂μ

@[simp]

theorem ProbabilityTheory.kernel.integral_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : β → E} {μ : MeasureTheory.Measure β} {a : α} : ∫ (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_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : β → E} {μ : MeasureTheory.Measure β} {a : α} {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_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : β → E} {μ : MeasureTheory.Measure β} {a : α} {s : Set β} : ∫ (x : β) in s, f x ∂(ProbabilityTheory.kernel.const α μ) a = ∫ (x : β) in s, f x ∂μ

Alias of ProbabilityTheory.kernel.setIntegral_const.

def ProbabilityTheory.kernel.ofFunOfCountable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] : {x : MeasurableSpace β} → [inst : Countable α] → [inst : MeasurableSingletonClass α] → (α → MeasureTheory.Measure β) → ↥(ProbabilityTheory.kernel α β)

In a countable space with measurable singletons, every function α → MeasureTheory.Measure β defines a kernel.

Equations

• ProbabilityTheory.kernel.ofFunOfCountable f = { val := f, property := ⋯ }

noncomputable def ProbabilityTheory.kernel.restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : ↥(ProbabilityTheory.kernel α β)) (hs : MeasurableSet s) : ↥(ProbabilityTheory.kernel α β)

Kernel given by the restriction of the measures in the image of a kernel to a set.

Equations

• ProbabilityTheory.kernel.restrict κ hs = { val := fun (a : α) => (κ a).restrict s, property := ⋯ }

theorem ProbabilityTheory.kernel.restrict_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : ↥(ProbabilityTheory.kernel α β)) (hs : MeasurableSet s) (a : α) : (ProbabilityTheory.kernel.restrict κ hs) a = (κ a).restrict s

theorem ProbabilityTheory.kernel.restrict_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} {t : Set β} (κ : ↥(ProbabilityTheory.kernel α β)) (hs : MeasurableSet s) (a : α) (ht : MeasurableSet t) : ↑↑((ProbabilityTheory.kernel.restrict κ hs) a) t = ↑↑(κ a) (t ∩ s)

@[simp]

theorem ProbabilityTheory.kernel.restrict_univ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} : ProbabilityTheory.kernel.restrict κ ⋯ = κ

@[simp]

theorem ProbabilityTheory.kernel.lintegral_restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : ↥(ProbabilityTheory.kernel α β)) (hs : MeasurableSet s) (a : α) (f : β → ENNReal) : ∫⁻ (b : β), f b ∂(ProbabilityTheory.kernel.restrict κ hs) a = ∫⁻ (b : β) in s, f b ∂κ a

@[simp]

theorem ProbabilityTheory.kernel.set_lintegral_restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : ↥(ProbabilityTheory.kernel α β)) (hs : MeasurableSet s) (a : α) (f : β → ENNReal) (t : Set β) : ∫⁻ (b : β) in t, f b ∂(ProbabilityTheory.kernel.restrict κ hs) a = ∫⁻ (b : β) in t ∩ s, f b ∂κ a

@[simp]

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

@[deprecated ProbabilityTheory.kernel.setIntegral_restrict]

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

Alias of ProbabilityTheory.kernel.setIntegral_restrict.

instance ProbabilityTheory.kernel.IsFiniteKernel.restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : ↥(ProbabilityTheory.kernel α β)) [ProbabilityTheory.IsFiniteKernel κ] (hs : MeasurableSet s) : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.restrict κ hs)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.kernel.IsSFiniteKernel.restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : ↥(ProbabilityTheory.kernel α β)) [ProbabilityTheory.IsSFiniteKernel κ] (hs : MeasurableSet s) : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.restrict κ hs)

Equations

• ⋯ = ⋯

noncomputable def ProbabilityTheory.kernel.comapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γ → β} (κ : ↥(ProbabilityTheory.kernel α β)) (hf : MeasurableEmbedding f) : ↥(ProbabilityTheory.kernel α γ)

Kernel with value (κ a).comap f, for a measurable embedding f. That is, for a measurable set t : Set β, ProbabilityTheory.kernel.comapRight κ hf a t = κ a (f '' t).

Equations

• ProbabilityTheory.kernel.comapRight κ hf = { val := fun (a : α) => MeasureTheory.Measure.comap f (κ a), property := ⋯ }

theorem ProbabilityTheory.kernel.comapRight_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γ → β} (κ : ↥(ProbabilityTheory.kernel α β)) (hf : MeasurableEmbedding f) (a : α) : (ProbabilityTheory.kernel.comapRight κ hf) a = MeasureTheory.Measure.comap f (κ a)

theorem ProbabilityTheory.kernel.comapRight_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γ → β} (κ : ↥(ProbabilityTheory.kernel α β)) (hf : MeasurableEmbedding f) (a : α) {t : Set γ} (ht : MeasurableSet t) : ↑↑((ProbabilityTheory.kernel.comapRight κ hf) a) t = ↑↑(κ a) (f '' t)

@[simp]

theorem ProbabilityTheory.kernel.comapRight_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ↥(ProbabilityTheory.kernel α β)) : ProbabilityTheory.kernel.comapRight κ ⋯ = κ

theorem ProbabilityTheory.kernel.IsMarkovKernel.comapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γ → β} (κ : ↥(ProbabilityTheory.kernel α β)) (hf : MeasurableEmbedding f) (hκ : ∀ (a : α), ↑↑(κ a) (Set.range f) = 1) : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.comapRight κ hf)

instance ProbabilityTheory.kernel.IsFiniteKernel.comapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γ → β} (κ : ↥(ProbabilityTheory.kernel α β)) [ProbabilityTheory.IsFiniteKernel κ] (hf : MeasurableEmbedding f) : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.comapRight κ hf)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.kernel.IsSFiniteKernel.comapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γ → β} (κ : ↥(ProbabilityTheory.kernel α β)) [ProbabilityTheory.IsSFiniteKernel κ] (hf : MeasurableEmbedding f) : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.comapRight κ hf)

Equations

• ⋯ = ⋯

def ProbabilityTheory.kernel.piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (hs : MeasurableSet s) (κ : ↥(ProbabilityTheory.kernel α β)) (η : ↥(ProbabilityTheory.kernel α β)) : ↥(ProbabilityTheory.kernel α β)

ProbabilityTheory.kernel.piecewise hs κ η is the kernel equal to κ on the measurable set s and to η on its complement.

Equations

• ProbabilityTheory.kernel.piecewise hs κ η = { val := fun (a : α) => if a ∈ s then κ a else η a, property := ⋯ }

theorem ProbabilityTheory.kernel.piecewise_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} {η : ↥(ProbabilityTheory.kernel α β)} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] (a : α) : (ProbabilityTheory.kernel.piecewise hs κ η) a = if a ∈ s then κ a else η a

theorem ProbabilityTheory.kernel.piecewise_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} {η : ↥(ProbabilityTheory.kernel α β)} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] (a : α) (t : Set β) : ↑↑((ProbabilityTheory.kernel.piecewise hs κ η) a) t = if a ∈ s then ↑↑(κ a) t else ↑↑(η a) t

instance ProbabilityTheory.kernel.IsMarkovKernel.piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} {η : ↥(ProbabilityTheory.kernel α β)} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.piecewise hs κ η)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.kernel.IsFiniteKernel.piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} {η : ↥(ProbabilityTheory.kernel α β)} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.piecewise hs κ η)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.kernel.IsSFiniteKernel.piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} {η : ↥(ProbabilityTheory.kernel α β)} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η] : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.piecewise hs κ η)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.kernel.lintegral_piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} {η : ↥(ProbabilityTheory.kernel α β)} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] (a : α) (g : β → ENNReal) : ∫⁻ (b : β), g b ∂(ProbabilityTheory.kernel.piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η a

theorem ProbabilityTheory.kernel.set_lintegral_piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} {η : ↥(ProbabilityTheory.kernel α β)} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] (a : α) (g : β → ENNReal) (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

theorem ProbabilityTheory.kernel.integral_piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α β)} {η : ↥(ProbabilityTheory.kernel α β)} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] (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 α β)} {η : ↥(ProbabilityTheory.kernel α β)} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] (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 α β)} {η : ↥(ProbabilityTheory.kernel α β)} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] (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

Alias of ProbabilityTheory.kernel.setIntegral_piecewise.