Documentation

Mathlib.Probability.Kernel.Disintegration.StandardBorel

Existence of disintegration of measures and kernels for standard Borel spaces #

Let κ : Kernel α (β × Ω) be a finite kernel, where Ω is a standard Borel space. Then if α is countable or β has a countably generated σ-algebra (for example if it is standard Borel), then there exists a Kernel (α × β) Ω called conditional kernel and denoted by condKernel κ such that κ = fst κ ⊗ₖ condKernel κ. We also define a conditional kernel for a measure ρ : Measure (β × Ω), where Ω is a standard Borel space. This is a Kernel β Ω denoted by ρ.condKernel such that ρ = ρ.fst ⊗ₘ ρ.condKernel.

In order to obtain a disintegration for any standard Borel space Ω, we use that these spaces embed measurably into : it then suffices to define a suitable kernel for Ω = ℝ.

For κ : Kernel α (β × ℝ), the construction of the conditional kernel proceeds as follows:

The first step (building the measurable function on ) is done differently depending on whether α is countable or not.

The conditional kernel is defined under the typeclass assumption CountableOrCountablyGenerated α β, which encodes the property Countable α ∨ CountablyGenerated β.

Properties of integrals involving condKernel are collated in the file Integral.lean. The conditional kernel is unique (almost everywhere w.r.t. fst κ): this is proved in the file Unique.lean.

Main definitions #

Main statements #

Disintegration of kernels from α to γ × ℝ for countably generated γ #

theorem ProbabilityTheory.Kernel.isRatCondKernelCDF_density_Iic {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × )) [ProbabilityTheory.IsFiniteKernel κ] :
ProbabilityTheory.IsRatCondKernelCDF (fun (p : α × γ) (q : ) => κ.density κ.fst p.1 p.2 (Set.Iic q)) κ κ.fst

Taking the kernel density of intervals Iic q for q : ℚ gives a function with the property isRatCondKernelCDF.

The conditional kernel CDF of a kernel κ : Kernel α (γ × ℝ), where γ is countably generated.

Equations
Instances For

    Auxiliary definition for ProbabilityTheory.Kernel.condKernel. A conditional kernel for κ : Kernel α (γ × ℝ) where γ is countably generated.

    Equations
    Instances For

      Auxiliary definition for MeasureTheory.Measure.condKernel and ProbabilityTheory.Kernel.condKernel. A conditional kernel for κ : Kernel Unit (α × ℝ).

      Equations
      Instances For
        Equations
        • =
        @[deprecated ProbabilityTheory.Kernel.disintegrate]
        theorem ProbabilityTheory.Kernel.compProd_fst_condKernelUnitReal {α : Type u_1} {mα : MeasurableSpace α} (κ : ProbabilityTheory.Kernel Unit (α × )) [ProbabilityTheory.IsFiniteKernel κ] :
        κ.fst.compProd κ.condKernelUnitReal = κ

        Disintegration of kernels on standard Borel spaces #

        Since every standard Borel space embeds measurably into , we can generalize a disintegration property on to all these spaces.

        Auxiliary definition for ProbabilityTheory.Kernel.condKernel. A Borel space Ω embeds measurably into (with embedding e), hence we can get a Kernel α Ω from a Kernel α ℝ by taking the comap by e. Here we take the comap of a modification of η : Kernel α ℝ, useful when η a is a probability measure with all its mass on range e almost everywhere with respect to some measure and we want to ensure that the comap is a Markov kernel. We thus take the comap by e of a kernel defined piecewise: η when η a (range (embeddingReal Ω))ᶜ = 0, and an arbitrary deterministic kernel otherwise.

        Equations
        Instances For

          For κ' := map κ (Prod.map (id : β → β) e), the hypothesis is fst κ' ⊗ₖ η = κ'. The conclusion of the lemma is fst κ ⊗ₖ borelMarkovFromReal Ω η = comapRight (fst κ' ⊗ₖ η) _.

          For κ' := map κ (Prod.map (id : β → β) e), the hypothesis is fst κ' ⊗ₖ η = κ'. With that hypothesis, fst κ ⊗ₖ borelMarkovFromReal κ η = κ.

          Auxiliary definition for ProbabilityTheory.Kernel.condKernel. A conditional kernel for κ : Kernel α (γ × Ω) where γ is countably generated and Ω is standard Borel.

          Equations
          Instances For
            instance ProbabilityTheory.Kernel.condKernelBorel.instIsCondKernel {α : Type u_1} {γ : Type u_3} {Ω : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (κ : ProbabilityTheory.Kernel α (γ × Ω)) [ProbabilityTheory.IsFiniteKernel κ] :
            κ.IsCondKernel κ.condKernelBorel
            Equations
            • =
            @[deprecated ProbabilityTheory.Kernel.disintegrate]
            theorem ProbabilityTheory.Kernel.compProd_fst_condKernelBorel {α : Type u_1} {γ : Type u_3} {Ω : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (κ : ProbabilityTheory.Kernel α (γ × Ω)) [ProbabilityTheory.IsFiniteKernel κ] :
            κ.fst.compProd κ.condKernelBorel = κ

            Auxiliary definition for MeasureTheory.Measure.condKernel and ProbabilityTheory.Kernel.condKernel. A conditional kernel for κ : Kernel Unit (α × Ω) where Ω is standard Borel.

            Equations
            Instances For
              instance ProbabilityTheory.Kernel.condKernelUnitBorel.instIsCondKernel {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (κ : ProbabilityTheory.Kernel Unit (α × Ω)) [ProbabilityTheory.IsFiniteKernel κ] :
              κ.IsCondKernel κ.condKernelUnitBorel
              Equations
              • =
              @[deprecated ProbabilityTheory.Kernel.disintegrate]
              theorem ProbabilityTheory.Kernel.compProd_fst_condKernelUnitBorel {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (κ : ProbabilityTheory.Kernel Unit (α × Ω)) [ProbabilityTheory.IsFiniteKernel κ] :
              κ.fst.compProd κ.condKernelUnitBorel = κ
              @[irreducible]

              Conditional kernel of a measure on a product space: a Markov kernel such that ρ = ρ.fst ⊗ₘ ρ.condKernel (see MeasureTheory.Measure.compProd_fst_condKernel).

              Equations
              Instances For
                theorem MeasureTheory.Measure.condKernel_def {α : Type u_5} {Ω : Type u_6} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (ρ : MeasureTheory.Measure (α × Ω)) [MeasureTheory.IsFiniteMeasure ρ] :
                ρ.condKernel = (ProbabilityTheory.Kernel.const Unit ρ).condKernelUnitBorel.comap (fun (a : α) => ((), a))
                theorem MeasureTheory.Measure.condKernel_apply {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (ρ : MeasureTheory.Measure (α × Ω)) [MeasureTheory.IsFiniteMeasure ρ] (a : α) :
                ρ.condKernel a = (ProbabilityTheory.Kernel.const Unit ρ).condKernelUnitBorel ((), a)
                instance MeasureTheory.Measure.condKernel.instIsCondKernel {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (ρ : MeasureTheory.Measure (α × Ω)) [MeasureTheory.IsFiniteMeasure ρ] :
                ρ.IsCondKernel ρ.condKernel
                Equations
                • =
                @[deprecated MeasureTheory.Measure.disintegrate]
                theorem MeasureTheory.Measure.compProd_fst_condKernel {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (ρ : MeasureTheory.Measure (α × Ω)) [MeasureTheory.IsFiniteMeasure ρ] :
                ρ.fst.compProd ρ.condKernel = ρ

                Disintegration of finite product measures on α × Ω, where Ω is standard Borel. Such a measure can be written as the composition-product of ρ.fst (marginal measure over α) and a Markov kernel from α to Ω. We call that Markov kernel ρ.condKernel.

                @[deprecated MeasureTheory.Measure.IsCondKernel.apply_of_ne_zero]
                theorem MeasureTheory.Measure.condKernel_apply_of_ne_zero_of_measurableSet {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : MeasureTheory.Measure (α × Ω)} [MeasureTheory.IsFiniteMeasure ρ] [MeasurableSingletonClass α] {x : α} (hx : ρ.fst {x} 0) {s : Set Ω} (hs : MeasurableSet s) :
                (ρ.condKernel x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

                Auxiliary lemma for condKernel_apply_of_ne_zero.

                theorem MeasureTheory.Measure.condKernel_apply_of_ne_zero {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : MeasureTheory.Measure (α × Ω)} [MeasureTheory.IsFiniteMeasure ρ] [MeasurableSingletonClass α] {x : α} (hx : ρ.fst {x} 0) (s : Set Ω) :
                (ρ.condKernel x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

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

                @[deprecated ProbabilityTheory.Kernel.disintegrate]
                theorem ProbabilityTheory.Kernel.compProd_fst_condKernelCountable {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [Countable α] (κ : ProbabilityTheory.Kernel α (β × Ω)) [ProbabilityTheory.IsFiniteKernel κ] :
                κ.fst.compProd (ProbabilityTheory.Kernel.condKernelCountable (fun (a : α) => (κ a).condKernel) ) = κ
                theorem ProbabilityTheory.Kernel.condKernel_def {α : Type u_5} {β : Type u_6} {Ω : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [h : MeasurableSpace.CountableOrCountablyGenerated α β] (κ : ProbabilityTheory.Kernel α (β × Ω)) [ProbabilityTheory.IsFiniteKernel κ] :
                κ.condKernel = if hα : Countable α then ProbabilityTheory.Kernel.condKernelCountable (fun (a : α) => (κ a).condKernel) else κ.condKernelBorel
                @[irreducible]

                Conditional kernel of a kernel κ : Kernel α (β × Ω): a Markov kernel such that fst κ ⊗ₖ condKernel κ = κ (see MeasureTheory.Measure.compProd_fst_condKernel). It exists whenever Ω is standard Borel and either α is countable or β is countably generated.

                Equations
                Instances For
                  Equations
                  • =
                  @[deprecated ProbabilityTheory.Kernel.disintegrate]
                  theorem ProbabilityTheory.Kernel.compProd_fst_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [h : MeasurableSpace.CountableOrCountablyGenerated α β] (κ : ProbabilityTheory.Kernel α (β × Ω)) [ProbabilityTheory.IsFiniteKernel κ] :
                  κ.fst.compProd κ.condKernel = κ

                  Disintegration of finite kernels. The composition-product of fst κ and condKernel κ is equal to κ.