Uniqueness of the conditional kernel #

We prove that the conditional kernels ProbabilityTheory.Kernel.condKernel and MeasureTheory.Measure.condKernel are almost everywhere unique.

Main statements #

ProbabilityTheory.eq_condKernel_of_kernel_eq_compProd: a.e. uniqueness of ProbabilityTheory.Kernel.condKernel
ProbabilityTheory.eq_condKernel_of_measure_eq_compProd: a.e. uniqueness of MeasureTheory.Measure.condKernel
ProbabilityTheory.Kernel.condKernel_apply_eq_condKernel: the kernel condKernel is almost everywhere equal to the measure condKernel.

Uniqueness of `Measure.condKernel` #

The conditional kernel of a measure is unique almost everywhere.

source

theorem ProbabilityTheory.eq_condKernel_of_measure_eq_compProd' {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : MeasureTheory.Measure (α × Ω)} [MeasureTheory.IsFiniteMeasure ρ] (κ : Kernel α Ω) [IsSFiniteKernel κ] (hκ : ρ = ρ.fst.compProd κ) {s : Set Ω} (hs : MeasurableSet s) :

∀ᵐ (x : α) ∂ρ.fst, (κ x) s = (ρ.condKernel x) s

A s-finite kernel which satisfy the disintegration property of the given measure ρ is almost everywhere equal to the disintegration kernel of ρ when evaluated on a measurable set.

This theorem in the case of finite kernels is weaker than eq_condKernel_of_measure_eq_compProd which asserts that the kernels are equal almost everywhere and not just on a given measurable set.

source

theorem ProbabilityTheory.eq_condKernel_of_measure_eq_compProd_real {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × ℝ)} [MeasureTheory.IsFiniteMeasure ρ] (κ : Kernel α ℝ) [IsFiniteKernel κ] (hκ : ρ = ρ.fst.compProd κ) :

∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x

Auxiliary lemma for eq_condKernel_of_measure_eq_compProd. Uniqueness of the disintegration kernel on ℝ.

source

theorem ProbabilityTheory.eq_condKernel_of_measure_eq_compProd {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : MeasureTheory.Measure (α × Ω)} [MeasureTheory.IsFiniteMeasure ρ] (κ : Kernel α Ω) [IsFiniteKernel κ] (hκ : ρ = ρ.fst.compProd κ) :

∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x

A finite kernel which satisfies the disintegration property is almost everywhere equal to the disintegration kernel.

source

theorem ProbabilityTheory.condKernel_compProd {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (κ : Kernel α Ω) [IsMarkovKernel κ] :

⇑(μ.compProd κ).condKernel =ᵐ[μ] ⇑κ

source

theorem ProbabilityTheory.Kernel.apply_eq_measure_condKernel_of_compProd_eq {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : Kernel α (β × Ω)} [IsFiniteKernel ρ] {κ : Kernel (α × β) Ω} [IsFiniteKernel κ] (hκ : ρ.fst.compProd κ = ρ) (a : α) :

(fun (b : β) => κ (a, b)) =ᵐ[ρ.fst a] ⇑(ρ a).condKernel

source

theorem ProbabilityTheory.Kernel.condKernel_apply_eq_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated α β] (κ : Kernel α (β × Ω)) [IsFiniteKernel κ] (a : α) :

(fun (b : β) => κ.condKernel (a, b)) =ᵐ[κ.fst a] ⇑(κ a).condKernel

For fst κ a-almost all b, the conditional kernel Kernel.condKernel κ applied to (a, b) is equal to the conditional kernel of the measure κ a applied to b.

source