# 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.lean` for a construction of disintegrating kernels.

### Disintegration of measures #

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

source
class MeasureTheory.Measure.IsCondKernel {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : 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 = ρ

Instances

source
theorem MeasureTheory.Measure.disintegrate {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : Measure (α × Ω)) (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] :
ρ.fst.compProd ρCond = ρ
source
theorem MeasureTheory.Measure.IsCondKernel.isSFiniteKernel {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : Measure (α × Ω)) (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] (hρ : ρ ≠ 0) :
ProbabilityTheory.IsSFiniteKernel ρCond
source
theorem MeasureTheory.Measure.IsCondKernel.apply_of_ne_zero {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : Measure (α × Ω)) (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] [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)` .

source
theorem MeasureTheory.Measure.IsCondKernel.isProbabilityMeasure {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : Measure (α × Ω)) (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] [IsFiniteMeasure ρ] [MeasurableSingletonClass α] {a : α} (ha : ρ.fst {a} ≠ 0) :
IsProbabilityMeasure (ρCond a)
source
theorem MeasureTheory.Measure.IsCondKernel.isMarkovKernel {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : Measure (α × Ω)) (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] [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 #

source
class ProbabilityTheory.Kernel.IsCondKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω} (κ : Kernel α (β × Ω)) (κCond : 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 = κ

Instances

source
instance ProbabilityTheory.Kernel.instIsCondKernel_zero {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω} (κCond : Kernel (α × β) Ω) :
IsCondKernel 0 κCond
source
theorem ProbabilityTheory.Kernel.disintegrate {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω} (κ : Kernel α (β × Ω)) (κCond : Kernel (α × β) Ω) [κ.IsCondKernel κCond] :
κ.fst.compProd κCond = κ
source
theorem ProbabilityTheory.Kernel.IsCondKernel.isProbabilityMeasure_ae {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω} (κ : Kernel α (β × Ω)) (κCond : Kernel (α × β) Ω) [IsFiniteKernel κ.fst] [κ.IsCondKernel κCond] (a : α) :
∀ᵐ (b : β) ∂κ.fst a, MeasureTheory.IsProbabilityMeasure (κCond (a, b))

A conditional kernel is almost everywhere a probability measure.

#### Existence of a disintegrating kernel in a countable space #

source
noncomputable def ProbabilityTheory.Kernel.condKernelCountable {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω} [Countable α] (κCond : α → Kernel β Ω) (h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y) :
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' := ⋯ }

Instances For

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