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

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

Instances For

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

Instances For

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

Instances For

source
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' := ⋯ }

source
theorem ProbabilityTheory.Kernel.measurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) :
Measurable ⇑κ
source
theorem ProbabilityTheory.Kernel.aemeasurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) {μ : MeasureTheory.Measure α} :
AEMeasurable (⇑κ) μ
source
@[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
source
instance ProbabilityTheory.Kernel.instZero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
Zero (Kernel α β)
Equations

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

source
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' := ⋯ } }

source
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' := ⋯ } }

source
@[simp]
theorem ProbabilityTheory.Kernel.coe_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
⇑0 = 0
source
@[simp]
theorem ProbabilityTheory.Kernel.coe_add {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ η : Kernel α β) :
⇑(κ + η) = ⇑κ + ⇑η
source
@[simp]
theorem ProbabilityTheory.Kernel.coe_nsmul {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (n : ℕ) (κ : Kernel α β) :
⇑(n • κ) = n • ⇑κ
source
@[simp]
theorem ProbabilityTheory.Kernel.zero_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (a : α) :
0 a = 0
source
@[simp]
theorem ProbabilityTheory.Kernel.add_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ η : Kernel α β) (a : α) :
(κ + η) a = κ a + η a
source
@[simp]
theorem ProbabilityTheory.Kernel.nsmul_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (n : ℕ) (κ : Kernel α β) (a : α) :
(n • κ) a = n • κ a
source
noncomputable instance ProbabilityTheory.Kernel.instAddCommMonoid {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
AddCommMonoid (Kernel α β)
Equations

- ProbabilityTheory.Kernel.instAddCommMonoid = Function.Injective.addCommMonoid (fun (f : ProbabilityTheory.Kernel α β) => ⇑f) ⋯ ⋯ ⋯ ⋯

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

- ProbabilityTheory.Kernel.instPartialOrder = PartialOrder.lift (fun (f : ProbabilityTheory.Kernel α β) => ⇑f) ⋯

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

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

source
noncomputable def ProbabilityTheory.Kernel.coeAddHom (α : Type u_4) (β : Type u_5) [MeasurableSpace α] [MeasurableSpace β] :
Kernel α β →+ α → MeasureTheory.Measure β

Coercion to a function as an additive monoid homomorphism.

Equations

- ProbabilityTheory.Kernel.coeAddHom α β = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem ProbabilityTheory.Kernel.coeAddHom_apply (α : Type u_4) (β : Type u_5) [MeasurableSpace α] [MeasurableSpace β] (κ : Kernel α β) :
(coeAddHom α β) κ = ⇑κ
source
@[simp]
theorem ProbabilityTheory.Kernel.coe_finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (I : Finset ι) (κ : ι → Kernel α β) :
⇑(∑ i ∈ I, κ i) = ∑ i ∈ I, ⇑(κ i)
source
theorem ProbabilityTheory.Kernel.finset_sum_apply {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (I : Finset ι) (κ : ι → Kernel α β) (a : α) :
(∑ i ∈ I, κ i) a = ∑ i ∈ I, (κ i) a
source
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
source
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)

Instances

source
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 κ

Instances

source
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

Instances

source
theorem ProbabilityTheory.eq_zero_or_isMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [h : IsZeroOrMarkovKernel κ] :
κ = 0 ∨ IsMarkovKernel κ
source
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

Instances For

source
@[deprecated ProbabilityTheory.Kernel.bound (since := "2025-09-13")]
def ProbabilityTheory.IsFiniteKernel.bound {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) :
ENNReal

Alias of `ProbabilityTheory.Kernel.bound`.

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

- @ProbabilityTheory.IsFiniteKernel.bound = @ProbabilityTheory.Kernel.bound

Instances For

source
theorem ProbabilityTheory.Kernel.bound_lt_top {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [h : IsFiniteKernel κ] :
κ.bound < ⊤
source
@[deprecated ProbabilityTheory.Kernel.bound_lt_top (since := "2025-09-13")]
theorem ProbabilityTheory.IsFiniteKernel.bound_lt_top {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [h : IsFiniteKernel κ] :
κ.bound < ⊤

Alias of `ProbabilityTheory.Kernel.bound_lt_top`.

source
theorem ProbabilityTheory.Kernel.bound_ne_top {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [IsFiniteKernel κ] :
κ.bound ≠ ⊤
source
@[deprecated ProbabilityTheory.Kernel.bound_ne_top (since := "2025-09-13")]
theorem ProbabilityTheory.IsFiniteKernel.bound_ne_top {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [IsFiniteKernel κ] :
κ.bound ≠ ⊤

Alias of `ProbabilityTheory.Kernel.bound_ne_top`.

source
theorem ProbabilityTheory.Kernel.measure_le_bound {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) (a : α) (s : Set β) :
(κ a) s ≤ κ.bound
source
@[simp]
theorem ProbabilityTheory.Kernel.bound_eq_zero_of_isEmpty {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty α] (κ : Kernel α β) :
κ.bound = 0
source
@[deprecated ProbabilityTheory.Kernel.bound_eq_zero_of_isEmpty (since := "2025-09-13")]
theorem ProbabilityTheory.IsFiniteKernel.bound_eq_zero_of_isEmpty {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty α] (κ : Kernel α β) :
κ.bound = 0

Alias of `ProbabilityTheory.Kernel.bound_eq_zero_of_isEmpty`.

source
@[simp]
theorem ProbabilityTheory.Kernel.bound_eq_zero_of_isEmpty' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty β] (κ : Kernel α β) :
κ.bound = 0
source
@[deprecated ProbabilityTheory.Kernel.bound_eq_zero_of_isEmpty' (since := "2025-09-13")]
theorem ProbabilityTheory.IsFiniteKernel.bound_eq_zero_of_isEmpty' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty β] (κ : Kernel α β) :
κ.bound = 0

Alias of `ProbabilityTheory.Kernel.bound_eq_zero_of_isEmpty'`.

source
@[simp]
theorem ProbabilityTheory.Kernel.bound_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
bound 0 = 0
source
@[deprecated ProbabilityTheory.Kernel.bound_zero (since := "2025-09-13")]
theorem ProbabilityTheory.IsFiniteKernel.bound_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
Kernel.bound 0 = 0

Alias of `ProbabilityTheory.Kernel.bound_zero`.

source
instance ProbabilityTheory.isFiniteKernel_zero (α : Type u_4) (β : Type u_5) {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} :
IsFiniteKernel 0
source
instance ProbabilityTheory.IsFiniteKernel.add {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
IsFiniteKernel (κ + η)
source
theorem ProbabilityTheory.isFiniteKernel_of_le {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ ν : Kernel α β} [hν : IsFiniteKernel ν] (hκν : κ ≤ ν) :
IsFiniteKernel κ
source
instance ProbabilityTheory.IsMarkovKernel.is_probability_measure' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} [IsMarkovKernel κ] (a : α) :
MeasureTheory.IsProbabilityMeasure (κ a)
source
instance ProbabilityTheory.instIsZeroOrMarkovKernelOfNatKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
IsZeroOrMarkovKernel 0
source
@[instance 100]
instance ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} [h : IsMarkovKernel κ] :
ProbabilityTheory.IsZeroOrMarkovKernel κ
source
@[instance 100]
instance ProbabilityTheory.IsZeroOrMarkovKernel.isZeroOrProbabilityMeasure {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} [IsZeroOrMarkovKernel κ] (a : α) :
MeasureTheory.IsZeroOrProbabilityMeasure (κ a)
source
instance ProbabilityTheory.IsFiniteKernel.isFiniteMeasure {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} [IsFiniteKernel κ] (a : α) :
MeasureTheory.IsFiniteMeasure (κ a)
source
@[instance 100]
instance ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} [h : IsZeroOrMarkovKernel κ] :
IsFiniteKernel κ
source
@[simp]
theorem ProbabilityTheory.Kernel.bound_eq_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Nonempty α] (κ : Kernel α β) [IsMarkovKernel κ] :
κ.bound = 1
source
@[deprecated ProbabilityTheory.Kernel.bound_eq_one (since := "2025-09-13")]
theorem ProbabilityTheory.IsMarkovKernel.bound_eq_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Nonempty α] (κ : Kernel α β) [IsMarkovKernel κ] :
κ.bound = 1

Alias of `ProbabilityTheory.Kernel.bound_eq_one`.

source
@[simp]
theorem ProbabilityTheory.Kernel.bound_le_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] :
κ.bound ≤ 1
source
@[deprecated ProbabilityTheory.Kernel.bound_le_one (since := "2025-09-13")]
theorem ProbabilityTheory.IsZeroOrMarkovKernel.bound_le_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] :
κ.bound ≤ 1

Alias of `ProbabilityTheory.Kernel.bound_le_one`.

source
theorem ProbabilityTheory.Kernel.ext {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : Kernel α β} (h : ∀ (a : α), κ a = η a) :
κ = η
source
theorem ProbabilityTheory.Kernel.ext_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : Kernel α β} :
κ = η ↔ ∀ (a : α), κ a = η a
source
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
source
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) :
κ = η
source
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
source
instance ProbabilityTheory.Kernel.instSubsingletonOfIsEmpty {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty β] :
Subsingleton (Kernel α β)
source
instance ProbabilityTheory.Kernel.instIsMarkovKernelOfIsEmpty {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty α] (κ : Kernel α β) :
IsMarkovKernel κ
source
instance ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelOfIsEmpty {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty β] (κ : Kernel α β) :
IsZeroOrMarkovKernel κ
source
theorem ProbabilityTheory.Kernel.not_isMarkovKernel_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Nonempty α] :
¬IsMarkovKernel 0
source
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
source
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
source
theorem ProbabilityTheory.Kernel.eq_zero_of_isEmpty_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [h : IsEmpty α] :
κ = 0
source
theorem ProbabilityTheory.Kernel.eq_zero_of_isEmpty_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [IsEmpty β] :
κ = 0
source
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' := ⋯ }

Instances For

source
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
source
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
source
@[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
source
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
source
@[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
source
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 η
source
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

Instances

source
@[instance 100]
instance ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} [h : IsFiniteKernel κ] :
IsSFiniteKernel κ
source
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

Instances For

source
theorem ProbabilityTheory.Kernel.kernel_sum_seq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [h : IsSFiniteKernel κ] :
Kernel.sum κ.seq = κ
source
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
source
instance ProbabilityTheory.Kernel.isFiniteKernel_seq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [h : IsSFiniteKernel κ] (n : ℕ) :
IsFiniteKernel (κ.seq n)
source
instance ProbabilityTheory.IsSFiniteKernel.sFinite {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} [IsSFiniteKernel κ] (a : α) :
MeasureTheory.SFinite (κ a)
source
instance ProbabilityTheory.Kernel.IsSFiniteKernel.add {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ η : Kernel α β) [IsSFiniteKernel κ] [IsSFiniteKernel η] :
IsSFiniteKernel (κ + η)
source
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)
source
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)
source
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)