Disintegration of kernels and measures #
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 γ #
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
- One or more equations did not get rendered due to their size.
Instances For
Auxiliary definition for ProbabilityTheory.kernel.condKernel.
A conditional kernel for κ : kernel α (γ × ℝ) where γ is countably generated.
Equations
Instances For
Equations
- ⋯ = ⋯
Auxiliary definition for MeasureTheory.Measure.condKernel and
ProbabilityTheory.kernel.condKernel.
A conditional kernel for κ : kernel Unit (α × ℝ).
Equations
- ProbabilityTheory.kernel.condKernelUnitReal κ = ProbabilityTheory.IsCondKernelCDF.toKernel (fun (p : Unit × α) => ProbabilityTheory.condCDF (κ ()) p.2) ⋯
Instances For
Equations
- ⋯ = ⋯
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
- One or more equations did not get rendered due to their size.
Instances For
When η is an s-finite kernel, borelMarkovFromReal Ω η is an s-finite kernel.
Equations
- ⋯ = ⋯
When η is a finite kernel, borelMarkovFromReal Ω η is a finite kernel.
Equations
- ⋯ = ⋯
When η is a Markov kernel, borelMarkovFromReal Ω η is a Markov kernel.
Equations
- ⋯ = ⋯
For κ' := map κ (Prod.map (id : β → β) e) (measurable_id.prod_map he.measurable), the
hypothesis hη is fst κ' ⊗ₖ η = κ'. The conclusion of the lemma is
fst κ ⊗ₖ borelMarkovFromReal Ω η = comapRight (fst κ' ⊗ₖ η) _.
For κ' := map κ (Prod.map (id : β → β) e) (measurable_id.prod_map he.measurable), the
hypothesis hη 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
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Auxiliary definition for MeasureTheory.Measure.condKernel and
ProbabilityTheory.kernel.condKernel.
A conditional kernel for κ : kernel Unit (α × Ω) where Ω is standard Borel.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Conditional kernel of a measure on a product space: a Markov kernel such that
ρ = ρ.fst ⊗ₘ ρ.condKernel (see MeasureTheory.Measure.compProd_fst_condKernel).
Instances For
Equations
- ⋯ = ⋯
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.
Auxiliary lemma for condKernel_apply_of_ne_zero.
If the singleton {x} has non-zero mass for ρ.fst, then for all s : Set Ω,
ρ.condKernel x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s) .
Auxiliary definition for ProbabilityTheory.kernel.condKernel.
A conditional kernel for κ : kernel α (β × Ω) where α is countable and Ω is standard Borel.
Equations
- ProbabilityTheory.kernel.condKernelCountable κ = { val := fun (p : α × β) => (MeasureTheory.Measure.condKernel (κ p.1)) p.2, property := ⋯ }
Instances For
Equations
- ⋯ = ⋯
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.
Instances For
condKernel κ is a Markov kernel.
Equations
- ⋯ = ⋯
Disintegration of finite kernels.
The composition-product of fst κ and condKernel κ is equal to κ.