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 setssand allq : ℚ,∫ 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 fileMeasurableStieltjes.lean. - Finally obtain from the measurable Stieltjes function a measure on
ℝfor each element ofα × βin a measurable way: we have obtained aKernel (α × β) ℝ. See the fileCDFToKernel.leanfor 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 eacha : αa functionf : β → ℚ → ℝand proceed as above to obtain aKernel β ℝ. Sinceαis countable, measurability is not an issue and we can put those together into aKernel (α × β) ℝ. The construction of thatfis done in theCondCDF.leanfile. - If
αis not countable, we can't proceed separately for eacha : αand have to build a functionf : α × β → ℚ → ℝ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 fileDensity.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)) ⋯
Instances For
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 ⋯
Instances For
instance
ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelReal
{α : Type u_1}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
[MeasurableSpace.CountablyGenerated γ]
(κ : ProbabilityTheory.Kernel α (γ × ℝ))
[ProbabilityTheory.IsFiniteKernel κ]
:
ProbabilityTheory.IsMarkovKernel κ.condKernelReal
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 κ]
:
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) ⋯
Instances For
instance
ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelUnitReal
{α : Type u_1}
{mα : MeasurableSpace α}
(κ : ProbabilityTheory.Kernel Unit (α × ℝ))
[ProbabilityTheory.IsFiniteKernel κ]
:
ProbabilityTheory.IsMarkovKernel κ.condKernelUnitReal
instance
ProbabilityTheory.Kernel.condKernelUnitReal.instIsCondKernel
{α : Type u_1}
{mα : MeasurableSpace α}
(κ : ProbabilityTheory.Kernel Unit (α × ℝ))
[ProbabilityTheory.IsFiniteKernel κ]
:
κ.IsCondKernel κ.condKernelUnitReal
@[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 α ℝ)
:
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 ⋯
Instances For
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 η]
:
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 Ω]
(η : ProbabilityTheory.Kernel α ℝ)
[ProbabilityTheory.IsFiniteKernel η]
:
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 Ω]
(η : ProbabilityTheory.Kernel α ℝ)
[ProbabilityTheory.IsMarkovKernel η]
:
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 Ω]
(κ : 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
Instances For
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
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
@[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
Instances For
instance
ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelUnitBorel
{α : Type u_1}
{Ω : Type u_4}
{mα : MeasurableSpace α}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(κ : ProbabilityTheory.Kernel Unit (α × Ω))
[ProbabilityTheory.IsFiniteKernel κ]
:
ProbabilityTheory.IsMarkovKernel κ.condKernelUnitBorel
instance
ProbabilityTheory.Kernel.condKernelUnitBorel.instIsCondKernel
{α : Type u_1}
{Ω : Type u_4}
{mα : MeasurableSpace α}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(κ : ProbabilityTheory.Kernel Unit (α × Ω))
[ProbabilityTheory.IsFiniteKernel κ]
:
κ.IsCondKernel κ.condKernelUnitBorel
@[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 ρ]
:
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)) ⋯
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
instance
MeasureTheory.Measure.instIsMarkovKernelCondKernel
{α : Type u_1}
{Ω : Type u_4}
{mα : MeasurableSpace α}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
:
ProbabilityTheory.IsMarkovKernel ρ.condKernel
@[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)
:
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 Ω)
:
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
- κ.condKernel = if hα : Countable α then ProbabilityTheory.Kernel.condKernelCountable (fun (a : α) => (κ a).condKernel) ⋯ else κ.condKernelBorel
Instances For
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.
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
@[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 κ.