Disintegration of measures and kernels

This file defines predicates for a kernel to "disintegrate" a measure or a kernel. This kernel is also called the "conditional kernel" of the measure or kernel.

A measure ρ : Measure (α × Ω) is disintegrated by a kernel ρCond : Kernel α Ω if ρ.fst ⊗ₘ ρCond = ρ.

A kernel ρ : Kernel α (β × Ω) is disintegrated by a kernel κCond : Kernel (α × β) Ω if κ.fst ⊗ₖ κCond = κ.

Main definitions

• MeasureTheory.Measure.IsCondKernel ρ ρCond: Predicate for the kernel ρCond to disintegrate the measure ρ.
• ProbabilityTheory.Kernel.IsCondKernel κ κCond: Predicate for the kernel κ Cond to disintegrate the kernel κ.

Further, if κ is an s-finite kernel from a countable α such that each measure κ a is disintegrated by some kernel, then κ itself is disintegrated by a kernel, namely ProbabilityTheory.Kernel.condKernelCountable.

See also

Mathlib.Probability.Kernel.Disintegration.StandardBorel for a construction of disintegrating kernels.

Disintegration of measures

This section provides a predicate for a kernel to disintegrate a measure.

class MeasureTheory.Measure.IsCondKernel {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω)) (ρCond : ProbabilityTheory.Kernel α Ω) : Prop

A kernel ρCond is a conditional kernel for a measure ρ if it disintegrates it in the sense that ρ.fst ⊗ₘ ρCond = ρ.

• disintegrate : ρ.fst.compProd ρCond = ρ

theorem MeasureTheory.Measure.disintegrate {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω)) (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] : ρ.fst.compProd ρCond = ρ

theorem MeasureTheory.Measure.IsCondKernel.isSFiniteKernel {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω)) (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] (hρ : ρ ≠ 0) : ProbabilityTheory.IsSFiniteKernel ρCond

theorem MeasureTheory.Measure.IsCondKernel.apply_of_ne_zero {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω)) (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] [MeasureTheory.IsFiniteMeasure ρ] [MeasurableSingletonClass α] {x : α} (hx : ρ.fst {x} ≠ 0) (s : Set Ω) : (ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

If the singleton {x} has non-zero mass for ρ.fst, then for all s : Set Ω, ρCond x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s) .

theorem MeasureTheory.Measure.IsCondKernel.isProbabilityMeasure {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω)) (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] [MeasureTheory.IsFiniteMeasure ρ] [MeasurableSingletonClass α] {a : α} (ha : ρ.fst {a} ≠ 0) : MeasureTheory.IsProbabilityMeasure (ρCond a)

theorem MeasureTheory.Measure.IsCondKernel.isMarkovKernel {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω)) (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] [MeasureTheory.IsFiniteMeasure ρ] [MeasurableSingletonClass α] (hρ : ∀ (a : α), ρ.fst {a} ≠ 0) : ProbabilityTheory.IsMarkovKernel ρCond

Disintegration of kernels

This section provides a predicate for a kernel to disintegrate a kernel. It also proves that if κ is an s-finite kernel from a countable α such that each measure κ a is disintegrated by some kernel, then κ itself is disintegrated by a kernel, namely ProbabilityTheory.Kernel.condKernelCountable..

Predicate for a kernel to disintegrate a kernel

class ProbabilityTheory.Kernel.IsCondKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω} (κ : ProbabilityTheory.Kernel α (β × Ω)) (κCond : ProbabilityTheory.Kernel (α × β) Ω) : Prop

A kernel κCond is a conditional kernel for a kernel κ if it disintegrates it in the sense that κ.fst ⊗ₖ κCond = κ.

• disintegrate : κ.fst.compProd κCond = κ

instance ProbabilityTheory.Kernel.instIsCondKernel_zero {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω} (κCond : ProbabilityTheory.Kernel (α × β) Ω) : ProbabilityTheory.Kernel.IsCondKernel 0 κCond

theorem ProbabilityTheory.Kernel.disintegrate {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω} (κ : ProbabilityTheory.Kernel α (β × Ω)) (κCond : ProbabilityTheory.Kernel (α × β) Ω) [κ.IsCondKernel κCond] : κ.fst.compProd κCond = κ

Existence of a disintegrating kernel in a countable space

noncomputable def ProbabilityTheory.Kernel.condKernelCountable {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω} [Countable α] (κCond : α → ProbabilityTheory.Kernel β Ω) (h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y) : ProbabilityTheory.Kernel (α × β) Ω

Auxiliary definition for ProbabilityTheory.Kernel.condKernel.

A conditional kernel for κ : Kernel α (β × Ω) where α is countable and Ω is a measurable space.

Equations

• ProbabilityTheory.Kernel.condKernelCountable κCond h_atom = { toFun := fun (p : α × β) => (κCond p.1) p.2, measurable' := ⋯ }

theorem ProbabilityTheory.Kernel.condKernelCountable_apply {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω} [Countable α] (κCond : α → ProbabilityTheory.Kernel β Ω) (h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y) (p : α × β) : (ProbabilityTheory.Kernel.condKernelCountable κCond h_atom) p = (κCond p.1) p.2

instance ProbabilityTheory.Kernel.condKernelCountable.instIsMarkovKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω} [Countable α] (κCond : α → ProbabilityTheory.Kernel β Ω) [∀ (a : α), ProbabilityTheory.IsMarkovKernel (κCond a)] (h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y) : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.condKernelCountable κCond h_atom)

instance ProbabilityTheory.Kernel.condKernelCountable.instIsCondKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω} [Countable α] (κCond : α → ProbabilityTheory.Kernel β Ω) [∀ (a : α), ProbabilityTheory.IsMarkovKernel (κCond a)] (h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y) (κ : ProbabilityTheory.Kernel α (β × Ω)) [ProbabilityTheory.IsSFiniteKernel κ] [∀ (a : α), (κ a).IsCondKernel (κCond a)] : κ.IsCondKernel (ProbabilityTheory.Kernel.condKernelCountable κCond h_atom)