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:

• Build a measurable function f : (α × β) → ℚ → ℝ such that for all measurable sets s and all q : ℚ, ∫ x in s, f (a, x) q ∂(Kernel.fst κ a) = (κ a).real (s ×ˢ Iic (q : ℝ)). We restrict to ℚ here to be able to prove the measurability.
• Extend that function to (α × β) → StieltjesFunction. See the file MeasurableStieltjes.lean.
• Finally obtain from the measurable Stieltjes function a measure on ℝ for each element of α × β in a measurable way: we have obtained a Kernel (α × β) ℝ. See the file CDFToKernel.lean for that step.

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

• If α is countable, we can provide for each a : α a function f : β → ℚ → ℝ and proceed as above to obtain a Kernel β ℝ. Since α is countable, measurability is not an issue and we can put those together into a Kernel (α × β) ℝ. The construction of that f is done in the CondCDF.lean file.
• If α is not countable, we can't proceed separately for each a : α and have to build a function f : α × β → ℚ → ℝ which is measurable on the product. We are able to do so if β has a countably generated σ-algebra (this is the case in particular for standard Borel spaces). See the file Density.lean.

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

• ProbabilityTheory.Kernel.condKernel κ : Kernel (α × β) Ω: conditional kernel described above.
• MeasureTheory.Measure.condKernel ρ : Kernel β Ω: conditional kernel of a measure.

Main statements

• ProbabilityTheory.Kernel.compProd_fst_condKernel: fst κ ⊗ₖ condKernel κ = κ
• MeasureTheory.Measure.compProd_fst_condKernel: ρ.fst ⊗ₘ ρ.condKernel = ρ

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

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

theorem ProbabilityTheory.Kernel.isRatCondKernelCDF_density_Iic {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] : 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.

noncomputable def ProbabilityTheory.Kernel.condKernelCDF {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] : α × γ → StieltjesFunction

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

Equations

• κ.condKernelCDF = ProbabilityTheory.stieltjesOfMeasurableRat (fun (p : α × γ) (q : ℚ) => κ.density κ.fst p.1 p.2 (Set.Iic ↑q)) ⋯

theorem ProbabilityTheory.Kernel.isCondKernelCDF_condKernelCDF {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] : IsCondKernelCDF κ.condKernelCDF κ κ.fst

noncomputable def ProbabilityTheory.Kernel.condKernelReal {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] : Kernel (α × γ) ℝ

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

Equations

• κ.condKernelReal = ProbabilityTheory.IsCondKernelCDF.toKernel κ.condKernelCDF ⋯

instance ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelReal {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] : IsMarkovKernel κ.condKernelReal

theorem ProbabilityTheory.Kernel.compProd_fst_condKernelReal {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] : κ.fst.compProd κ.condKernelReal = κ

noncomputable def ProbabilityTheory.Kernel.condKernelUnitReal {α : Type u_1} {mα : MeasurableSpace α} (κ : Kernel Unit (α × ℝ)) [IsFiniteKernel κ] : Kernel (Unit × α) ℝ

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

Equations

• κ.condKernelUnitReal = ProbabilityTheory.IsCondKernelCDF.toKernel (fun (p : Unit × α) => ProbabilityTheory.condCDF (κ ()) p.2) ⋯

instance ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelUnitReal {α : Type u_1} {mα : MeasurableSpace α} (κ : Kernel Unit (α × ℝ)) [IsFiniteKernel κ] : IsMarkovKernel κ.condKernelUnitReal

instance ProbabilityTheory.Kernel.condKernelUnitReal.instIsCondKernel {α : Type u_1} {mα : MeasurableSpace α} (κ : Kernel Unit (α × ℝ)) [IsFiniteKernel κ] : κ.IsCondKernel κ.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.

noncomputable def ProbabilityTheory.Kernel.borelMarkovFromReal {α : Type u_1} {mα : MeasurableSpace α} (Ω : Type u_5) [Nonempty Ω] [MeasurableSpace Ω] [StandardBorelSpace Ω] (η : Kernel α ℝ) : Kernel α Ω

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

• ProbabilityTheory.Kernel.borelMarkovFromReal Ω η = (ProbabilityTheory.Kernel.piecewise ⋯ η (ProbabilityTheory.Kernel.deterministic (fun (x : α) => Exists.choose ⋯) ⋯)).comapRight ⋯

theorem ProbabilityTheory.Kernel.borelMarkovFromReal_apply {α : Type u_1} {mα : MeasurableSpace α} (Ω : Type u_5) [Nonempty Ω] [MeasurableSpace Ω] [StandardBorelSpace Ω] (η : Kernel α ℝ) (a : α) : (borelMarkovFromReal Ω η) a = if (η a) (Set.range (MeasureTheory.embeddingReal Ω))ᶜ = 0 then MeasureTheory.Measure.comap (MeasureTheory.embeddingReal Ω) (η a) else MeasureTheory.Measure.comap (MeasureTheory.embeddingReal Ω) (MeasureTheory.Measure.dirac (Exists.choose ⋯))

theorem ProbabilityTheory.Kernel.borelMarkovFromReal_apply' {α : Type u_1} {mα : MeasurableSpace α} (Ω : Type u_5) [Nonempty Ω] [MeasurableSpace Ω] [StandardBorelSpace Ω] (η : Kernel α ℝ) (a : α) {s : Set Ω} (hs : MeasurableSet s) : ((borelMarkovFromReal Ω η) a) s = if (η a) (Set.range (MeasureTheory.embeddingReal Ω))ᶜ = 0 then (η a) (MeasureTheory.embeddingReal Ω '' s) else (MeasureTheory.embeddingReal Ω '' s).indicator 1 (Exists.choose ⋯)

instance ProbabilityTheory.Kernel.instIsSFiniteKernelBorelMarkovFromReal {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (η : Kernel α ℝ) [IsSFiniteKernel η] : IsSFiniteKernel (borelMarkovFromReal Ω η)

When η is an s-finite kernel, borelMarkovFromReal Ω η is an s-finite kernel.

instance ProbabilityTheory.Kernel.instIsFiniteKernelBorelMarkovFromReal {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (η : Kernel α ℝ) [IsFiniteKernel η] : IsFiniteKernel (borelMarkovFromReal Ω η)

When η is a finite kernel, borelMarkovFromReal Ω η is a finite kernel.

instance ProbabilityTheory.Kernel.instIsMarkovKernelBorelMarkovFromReal {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (η : Kernel α ℝ) [IsMarkovKernel η] : IsMarkovKernel (borelMarkovFromReal Ω η)

When η is a Markov kernel, borelMarkovFromReal Ω η is a Markov kernel.

theorem ProbabilityTheory.Kernel.compProd_fst_borelMarkovFromReal_eq_comapRight_compProd {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel α (β × Ω)) [IsSFiniteKernel κ] (η : Kernel (α × β) ℝ) [IsSFiniteKernel η] (hη : (κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))).fst.compProd η = κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))) : κ.fst.compProd (borelMarkovFromReal Ω η) = ((κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))).fst.compProd η).comapRight ⋯

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

theorem ProbabilityTheory.Kernel.compProd_fst_borelMarkovFromReal {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel α (β × Ω)) [IsSFiniteKernel κ] (η : Kernel (α × β) ℝ) [IsSFiniteKernel η] (hη : (κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))).fst.compProd η = κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))) : κ.fst.compProd (borelMarkovFromReal Ω η) = κ

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

noncomputable def ProbabilityTheory.Kernel.condKernelBorel {α : Type u_1} {γ : Type u_3} {Ω : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel α (γ × Ω)) [IsFiniteKernel κ] : Kernel (α × γ) Ω

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

Equations

• κ.condKernelBorel = ProbabilityTheory.Kernel.borelMarkovFromReal Ω (κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))).condKernelReal

instance ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelBorel {α : Type u_1} {γ : Type u_3} {Ω : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel α (γ × Ω)) [IsFiniteKernel κ] : IsMarkovKernel κ.condKernelBorel

instance ProbabilityTheory.Kernel.condKernelBorel.instIsCondKernel {α : Type u_1} {γ : Type u_3} {Ω : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel α (γ × Ω)) [IsFiniteKernel κ] : κ.IsCondKernel κ.condKernelBorel

noncomputable def ProbabilityTheory.Kernel.condKernelUnitBorel {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Unit (α × Ω)) [IsFiniteKernel κ] : Kernel (Unit × α) Ω

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

Equations

• κ.condKernelUnitBorel = ProbabilityTheory.Kernel.borelMarkovFromReal Ω (κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))).condKernelUnitReal

instance ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelUnitBorel {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Unit (α × Ω)) [IsFiniteKernel κ] : IsMarkovKernel κ.condKernelUnitBorel

instance ProbabilityTheory.Kernel.condKernelUnitBorel.instIsCondKernel {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Unit (α × Ω)) [IsFiniteKernel κ] : κ.IsCondKernel κ.condKernelUnitBorel

theorem MeasureTheory.Measure.condKernel_def {α : Type u_5} {Ω : Type u_6} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (ρ : Measure (α × Ω)) [IsFiniteMeasure ρ] : ρ.condKernel = (ProbabilityTheory.Kernel.const Unit ρ).condKernelUnitBorel.comap (fun (a : α) => ((), a)) ⋯

@[irreducible]

noncomputable def MeasureTheory.Measure.condKernel {α : Type u_5} {Ω : Type u_6} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (ρ : Measure (α × Ω)) [IsFiniteMeasure ρ] : ProbabilityTheory.Kernel α Ω

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

Equations

• ρ.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 Ω] (ρ : Measure (α × Ω)) [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 Ω] (ρ : Measure (α × Ω)) [IsFiniteMeasure ρ] : ρ.IsCondKernel ρ.condKernel

instance MeasureTheory.Measure.instIsMarkovKernelCondKernel {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (ρ : Measure (α × Ω)) [IsFiniteMeasure ρ] : ProbabilityTheory.IsMarkovKernel ρ.condKernel

theorem MeasureTheory.Measure.condKernel_apply_of_ne_zero {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : Measure (α × Ω)} [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) .

theorem ProbabilityTheory.Kernel.condKernel_def {α : Type u_5} {β : Type u_6} {Ω : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [h : MeasurableSpace.CountableOrCountablyGenerated α β] (κ : Kernel α (β × Ω)) [IsFiniteKernel κ] : κ.condKernel = if hα : Countable α then condKernelCountable (fun (a : α) => (κ a).condKernel) ⋯ else κ.condKernelBorel

@[irreducible]

noncomputable def ProbabilityTheory.Kernel.condKernel {α : Type u_5} {β : Type u_6} {Ω : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [h : MeasurableSpace.CountableOrCountablyGenerated α β] (κ : Kernel α (β × Ω)) [IsFiniteKernel κ] : Kernel (α × β) Ω

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

• κ.condKernel = if hα : Countable α then ProbabilityTheory.Kernel.condKernelCountable (fun (a : α) => (κ a).condKernel) ⋯ else κ.condKernelBorel

instance ProbabilityTheory.Kernel.instIsMarkovKernelCondKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [h : MeasurableSpace.CountableOrCountablyGenerated α β] (κ : Kernel α (β × Ω)) [IsFiniteKernel κ] : IsMarkovKernel κ.condKernel

condKernel κ is a Markov kernel.

instance ProbabilityTheory.Kernel.condKernel.instIsCondKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [h : MeasurableSpace.CountableOrCountablyGenerated α β] (κ : Kernel α (β × Ω)) [IsFiniteKernel κ] : κ.IsCondKernel κ.condKernel