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 (s ×ˢ Iic (q : ℝ))).toReal. 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 γ] (κ : ProbabilityTheory.Kernel α (γ × ℝ)) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.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 γ] (κ : 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.

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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.

noncomputable def ProbabilityTheory.Kernel.borelMarkovFromReal {α : Type u_1} {mα : MeasurableSpace α} (Ω : Type u_5) [Nonempty Ω] [MeasurableSpace Ω] [StandardBorelSpace Ω] (η : ProbabilityTheory.Kernel α ℝ) : ProbabilityTheory.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 Ω] (η : ProbabilityTheory.Kernel α ℝ) (a : α) : (ProbabilityTheory.Kernel.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 Ω] (η : ProbabilityTheory.Kernel α ℝ) (a : α) {s : Set Ω} (hs : MeasurableSet s) : ((ProbabilityTheory.Kernel.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 Ω] (η : ProbabilityTheory.Kernel α ℝ) [ProbabilityTheory.IsSFiniteKernel η] : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.borelMarkovFromReal Ω η)

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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 Ω] (κ : ProbabilityTheory.Kernel α (β × Ω)) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) ℝ) [ProbabilityTheory.IsSFiniteKernel η] (hη : (κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))).fst.compProd η = κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))) : κ.fst.compProd (ProbabilityTheory.Kernel.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 Ω] (κ : ProbabilityTheory.Kernel α (β × Ω)) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) ℝ) [ProbabilityTheory.IsSFiniteKernel η] (hη : (κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))).fst.compProd η = κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))) : κ.fst.compProd (ProbabilityTheory.Kernel.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 Ω] (κ : ProbabilityTheory.Kernel α (γ × Ω)) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.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 Ω] (κ : ProbabilityTheory.Kernel α (γ × Ω)) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsMarkovKernel κ.condKernelBorel

Equations

• ⋯ = ⋯

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 = κ

noncomputable def ProbabilityTheory.Kernel.condKernelUnitBorel {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (κ : ProbabilityTheory.Kernel Unit (α × Ω)) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.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 Ω] (κ : ProbabilityTheory.Kernel Unit (α × Ω)) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsMarkovKernel κ.condKernelUnitBorel

Equations

• ⋯ = ⋯

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]

noncomputable def MeasureTheory.Measure.condKernel {α : Type u_5} {Ω : Type u_6} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (ρ : MeasureTheory.Measure (α × Ω)) [MeasureTheory.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

• @MeasureTheory.Measure.condKernel = ProbabilityTheory.Kernel.wrapped✝.1

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

• ⋯ = ⋯

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

noncomputable def ProbabilityTheory.Kernel.condKernel {α : Type u_5} {β : Type u_6} {Ω : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [h : MeasurableSpace.CountableOrCountablyGenerated α β] (κ : ProbabilityTheory.Kernel α (β × Ω)) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.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

• @ProbabilityTheory.Kernel.condKernel = ProbabilityTheory.Kernel.wrapped✝.1

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

condKernel κ is a Markov kernel.

Equations

• ⋯ = ⋯

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

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 κ.