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 β.
• ProbabilityTheory.IsMarkovKernel κ: a kernel from α to β is said to be a Markov kernel if for all a : α, k a is a probability measure.
• ProbabilityTheory.IsZeroOrMarkovKernel κ: a kernel from α to β which is zero or a Markov kernel.
• 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.

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.

structure ProbabilityTheory.Kernel (α : Type u_1) (β : Type u_2) [MeasurableSpace α] [MeasurableSpace β] : Type (max u_1 u_2)

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

• toFun : α → MeasureTheory.Measure β

  The underlying function of a kernel.

  Do not use this function directly. Instead use the coercion coming from the DFunLike instance.

• measurable' : Measurable self.toFun

  A kernel is a measurable map.

  Do not use this lemma directly. Use Kernel.measurable instead.

def ProbabilityTheory.«termKernel[_]__» : Lean.ParserDescr

Notation for Kernel with respect to a non-standard σ-algebra in the domain.

Equations

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

def ProbabilityTheory.«termKernel[_,_]__» : Lean.ParserDescr

Notation for Kernel with respect to a non-standard σ-algebra in the domain and codomain.

Equations

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

@[instance_reducible]

instance ProbabilityTheory.Kernel.instFunLike {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : FunLike (Kernel α β) α (MeasureTheory.Measure β)

Equations

• ProbabilityTheory.Kernel.instFunLike = { coe := ProbabilityTheory.Kernel.toFun, coe_injective := ⋯ }

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

theorem ProbabilityTheory.Kernel.aemeasurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) {μ : MeasureTheory.Measure α} : AEMeasurable (⇑κ) μ

@[simp]

theorem ProbabilityTheory.Kernel.coe_mk {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → MeasureTheory.Measure β) (hf : Measurable f) : ⇑{ toFun := f, measurable' := hf } = f

@[instance_reducible]

instance ProbabilityTheory.Kernel.instZero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : Zero (Kernel α β)

Equations

• ProbabilityTheory.Kernel.instZero = { zero := { toFun := 0, measurable' := ⋯ } }

@[instance_reducible]

noncomputable instance ProbabilityTheory.Kernel.instAdd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : Add (Kernel α β)

Equations

• ProbabilityTheory.Kernel.instAdd = { add := fun (κ η : ProbabilityTheory.Kernel α β) => { toFun := ⇑κ + ⇑η, measurable' := ⋯ } }

@[instance_reducible]

noncomputable instance ProbabilityTheory.Kernel.instSMulNat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : SMul ℕ (Kernel α β)

Equations

• ProbabilityTheory.Kernel.instSMulNat = { smul := fun (n : ℕ) (κ : ProbabilityTheory.Kernel α β) => { toFun := n • ⇑κ, measurable' := ⋯ } }

instance ProbabilityTheory.Kernel.instIsZeroApplyMeasure {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : IsZeroApply (Kernel α β) α (MeasureTheory.Measure β)

instance ProbabilityTheory.Kernel.instIsAddApplyMeasure {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : IsAddApply (Kernel α β) α (MeasureTheory.Measure β)

instance ProbabilityTheory.Kernel.instIsSMulApplyNatMeasure {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : IsSMulApply ℕ (Kernel α β) α (MeasureTheory.Measure β)

@[deprecated FunLike.coe_zero (since := "2026-06-30")]

theorem ProbabilityTheory.Kernel.coe_zero {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [Zero F] [Zero β] [IsZeroApply F α β] : ⇑0 = 0

Alias of FunLike.coe_zero.

@[deprecated FunLike.coe_add (since := "2026-06-30")]

theorem ProbabilityTheory.Kernel.coe_add {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [Add F] [Add β] [IsAddApply F α β] (f g : F) : ⇑(f + g) = ⇑f + ⇑g

Alias of FunLike.coe_add.

@[deprecated FunLike.coe_smul (since := "2026-06-30")]

theorem ProbabilityTheory.Kernel.coe_nsmul {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [SMul M F] [SMul M β] [IsSMulApply M F α β] (n : M) (f : F) : ⇑(n • f) = n • ⇑f

Alias of FunLike.coe_smul.

@[deprecated zero_apply (since := "2026-06-30")]

theorem ProbabilityTheory.Kernel.zero_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Zero β} {inst✝² : Zero F} [self : IsZeroApply F α β] (x : α) : 0 x = 0

Alias of zero_apply.

@[deprecated add_apply (since := "2026-06-30")]

theorem ProbabilityTheory.Kernel.add_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Add β} {inst✝² : Add F} [self : IsAddApply F α β] (f g : F) (x : α) : (f + g) x = f x + g x

Alias of add_apply.

@[deprecated smul_apply (since := "2026-06-30")]

theorem ProbabilityTheory.Kernel.nsmul_apply {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst✝ : FunLike F α β} {inst✝¹ : SMul M β} {inst✝² : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α) : (r • f) x = r • f x

Alias of smul_apply.

@[instance_reducible]

noncomputable instance ProbabilityTheory.Kernel.instAddCommMonoid {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : AddCommMonoid (Kernel α β)

Equations

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

@[instance_reducible]

instance ProbabilityTheory.Kernel.instPartialOrder {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : PartialOrder (Kernel α β)

Equations

• ProbabilityTheory.Kernel.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯

instance ProbabilityTheory.Kernel.instAddLeftMono {α : Type u_4} {β : Type u_5} [MeasurableSpace α] [MeasurableSpace β] : AddLeftMono (Kernel α β)

@[instance_reducible]

noncomputable instance ProbabilityTheory.Kernel.instOrderBot {α : Type u_4} {β : Type u_5} [MeasurableSpace α] [MeasurableSpace β] : OrderBot (Kernel α β)

Equations

• ProbabilityTheory.Kernel.instOrderBot = { bot := 0, bot_le := ⋯ }

@[deprecated FunLike.coe_coeAddMonoidHom (since := "2026-06-30")]

theorem ProbabilityTheory.Kernel.coeAddHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddZero F] [AddZeroClass β] [IsZeroApply F α β] [IsAddApply F α β] : ⇑(FunLike.coeAddMonoidHom F α β) = DFunLike.coe

Alias of FunLike.coe_coeAddMonoidHom.

@[deprecated FunLike.coeAddMonoidHom_apply (since := "2026-06-30")]

theorem ProbabilityTheory.Kernel.coeAddHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddZero F] [AddZeroClass β] [IsZeroApply F α β] [IsAddApply F α β] (f : F) : (FunLike.coeAddMonoidHom F α β) f = ⇑f

Alias of FunLike.coeAddMonoidHom_apply.

@[deprecated FunLike.coe_sum (since := "2026-06-30")]

theorem ProbabilityTheory.Kernel.coe_finsetSum {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [FunLike F α β] [AddCommMonoid β] [AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F) : ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)

Alias of FunLike.coe_sum.

@[deprecated FunLike.coe_sum (since := "2026-04-08")]

theorem ProbabilityTheory.Kernel.coe_finset_sum {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [FunLike F α β] [AddCommMonoid β] [AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F) : ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)

Alias of FunLike.coe_sum.

@[deprecated sum_apply (since := "2026-06-30")]

theorem ProbabilityTheory.Kernel.finsetSum_apply {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [FunLike F α β] [AddCommMonoid β] [AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F) (x : α) : (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x

Alias of sum_apply.

@[deprecated sum_apply (since := "2026-04-08")]

theorem ProbabilityTheory.Kernel.finset_sum_apply {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [FunLike F α β] [AddCommMonoid β] [AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F) (x : α) : (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x

Alias of sum_apply.

theorem ProbabilityTheory.Kernel.finsetSum_apply' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (I : Finset ι) (κ : ι → Kernel α β) (a : α) (s : Set β) : ((∑ i ∈ I, κ i) a) s = ∑ i ∈ I, ((κ i) a) s

@[deprecated ProbabilityTheory.Kernel.finsetSum_apply' (since := "2026-04-08")]

theorem ProbabilityTheory.Kernel.finset_sum_apply' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (I : Finset ι) (κ : ι → Kernel α β) (a : α) (s : Set β) : ((∑ i ∈ I, κ i) a) s = ∑ i ∈ I, ((κ i) a) s

Alias of ProbabilityTheory.Kernel.finsetSum_apply'.

class ProbabilityTheory.IsMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : 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.IsZeroOrMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : Prop

A class for kernels which are zero or a Markov kernel.

• eq_zero_or_isMarkovKernel' : κ = 0 ∨ IsMarkovKernel κ

class ProbabilityTheory.IsFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : 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

theorem ProbabilityTheory.eq_zero_or_isMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [h : IsZeroOrMarkovKernel κ] : κ = 0 ∨ IsMarkovKernel κ

noncomputable def ProbabilityTheory.Kernel.bound {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : ENNReal

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

Equations

• κ.bound = ⨆ (a : α), (κ a) Set.univ

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

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

theorem ProbabilityTheory.Kernel.measure_le_bound {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) (a : α) (s : Set β) : (κ a) s ≤ κ.bound

@[simp]

theorem ProbabilityTheory.Kernel.bound_eq_zero_of_isEmpty {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty α] (κ : Kernel α β) : κ.bound = 0

@[simp]

theorem ProbabilityTheory.Kernel.bound_eq_zero_of_isEmpty' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty β] (κ : Kernel α β) : κ.bound = 0

@[simp]

theorem ProbabilityTheory.Kernel.bound_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : bound 0 = 0

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

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

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

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

instance ProbabilityTheory.instIsZeroOrMarkovKernelOfNatKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : IsZeroOrMarkovKernel 0

@[instance 100]

instance ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} [h : IsMarkovKernel κ] : ProbabilityTheory.IsZeroOrMarkovKernel κ

@[instance 100]

instance ProbabilityTheory.IsZeroOrMarkovKernel.isZeroOrProbabilityMeasure {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} [IsZeroOrMarkovKernel κ] (a : α) : MeasureTheory.IsZeroOrProbabilityMeasure (κ a)

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

@[instance 100]

instance ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} [h : IsZeroOrMarkovKernel κ] : IsFiniteKernel κ

@[simp]

theorem ProbabilityTheory.Kernel.bound_eq_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Nonempty α] (κ : Kernel α β) [IsMarkovKernel κ] : κ.bound = 1

@[simp]

theorem ProbabilityTheory.Kernel.bound_le_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] : κ.bound ≤ 1

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

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

theorem ProbabilityTheory.Kernel.ext_iff' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : 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 β} {κ η : 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 β} {κ η : Kernel α β} : κ = η ↔ ∀ (a : α) (f : β → ENNReal), Measurable f → ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a

instance ProbabilityTheory.Kernel.instSubsingletonOfIsEmpty {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty β] : Subsingleton (Kernel α β)

instance ProbabilityTheory.Kernel.instIsMarkovKernelOfIsEmpty {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty α] (κ : Kernel α β) : IsMarkovKernel κ

instance ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelOfIsEmpty {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty β] (κ : Kernel α β) : IsZeroOrMarkovKernel κ

theorem ProbabilityTheory.Kernel.not_isMarkovKernel_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Nonempty α] : ¬IsMarkovKernel 0

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

theorem ProbabilityTheory.Kernel.apply_congr_of_mem_measurableAtom {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) {y' y : α} (hy' : y' ∈ measurableAtom y) : κ y' = κ y

theorem ProbabilityTheory.Kernel.eq_zero_of_isEmpty_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [h : IsEmpty α] : κ = 0

theorem ProbabilityTheory.Kernel.eq_zero_of_isEmpty_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [IsEmpty β] : κ = 0

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

Sum of an indexed family of kernels.

Equations

• ProbabilityTheory.Kernel.sum κ = { toFun := fun (a : α) => MeasureTheory.Measure.sum fun (n : ι) => (κ n) a, measurable' := ⋯ }

theorem ProbabilityTheory.Kernel.sum_apply {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (κ : ι → Kernel α β) (a : α) : (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 ι] (κ : ι → Kernel α β) (a : α) {s : Set β} (hs : MeasurableSet s) : ((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 ι] : (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 ι] (κ : ι → ι → Kernel α β) : (Kernel.sum fun (n : ι) => Kernel.sum (κ n)) = Kernel.sum fun (m : ι) => 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 ι] (κ : ι → Kernel α β) : Kernel.sum κ = ∑ i : ι, κ i

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

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

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

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

@[instance 100]

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

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

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

Equations

• κ.seq = ⋯.choose

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

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

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

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

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

theorem ProbabilityTheory.Kernel.IsSFiniteKernel.finsetSum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κs : ι → Kernel α β} (I : Finset ι) (h : ∀ i ∈ I, IsSFiniteKernel (κs i)) : IsSFiniteKernel (∑ i ∈ I, κs i)

@[deprecated ProbabilityTheory.Kernel.IsSFiniteKernel.finsetSum (since := "2026-04-08")]

theorem ProbabilityTheory.Kernel.IsSFiniteKernel.finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κs : ι → Kernel α β} (I : Finset ι) (h : ∀ i ∈ I, IsSFiniteKernel (κs i)) : IsSFiniteKernel (∑ i ∈ I, κs i)

Alias of ProbabilityTheory.Kernel.IsSFiniteKernel.finsetSum.

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

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