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.

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.

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 ℝ.

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.

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.

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