Documentation

Mathlib.Probability.Kernel.Disintegration.Unique

Uniqueness of the conditional kernel #

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

Main statements #

Uniqueness of Measure.condKernel #

The conditional kernel of a measure is unique almost everywhere.

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.

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

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

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 : α) :

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.

Uniqueness of Kernel.condKernel #

The conditional kernel is unique almost everywhere.

theorem ProbabilityTheory.eq_condKernel_of_kernel_eq_compProd {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated α β] {ρ : Kernel α (β × Ω)} [IsFiniteKernel ρ] {κ : Kernel (α × β) Ω} [IsFiniteKernel κ] (hκ : ρ.fst.compProd κ = ρ) (a : α) :
∀ᵐ (x : β) ρ.fst a, κ (a, x) = ρ.condKernel (a, x)

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