Documentation

Mathlib.Probability.Kernel.Disintegration.Basic

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 #

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 α Ω) :

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

    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 (α × β) Ω) :

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

      Auxiliary definition for ProbabilityTheory.Kernel.condKernel.

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

      Equations
      Instances For
        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
        theorem 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) :
        theorem 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)