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 ρ] (κ : ↥(ProbabilityTheory.kernel α Ω)) [ProbabilityTheory.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 ρ] (κ : ↥(ProbabilityTheory.kernel α ℝ)) [ProbabilityTheory.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 ρ] (κ : ↥(ProbabilityTheory.kernel α Ω)) [ProbabilityTheory.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.kernel.apply_eq_measure_condKernel_of_compProd_eq {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {ρ : ↥(ProbabilityTheory.kernel α (β × Ω))} [ProbabilityTheory.IsFiniteKernel ρ] {κ : ↥(ProbabilityTheory.kernel (α × β) Ω)} [ProbabilityTheory.IsFiniteKernel κ] (hκ : ProbabilityTheory.kernel.compProd (ProbabilityTheory.kernel.fst ρ) κ = ρ) (a : α) :

((ProbabilityTheory.kernel.fst ρ) a).ae.EventuallyEq (fun (b : β) => κ (a, b)) ⇑(ρ 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 α β] (κ : ↥(ProbabilityTheory.kernel α (β × Ω))) [ProbabilityTheory.IsFiniteKernel κ] (a : α) :

((ProbabilityTheory.kernel.fst κ) a).ae.EventuallyEq (fun (b : β) => (ProbabilityTheory.kernel.condKernel κ) (a, b)) ⇑(κ 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