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.

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.

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κ : ρ.fst.compProd κ = ρ) (a : α) : (fun (b : β) => κ (a, b)) =ᵐ[ρ.fst a] ⇑(ρ a).condKernel

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

theorem ProbabilityTheory.condKernel_const {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated α β] (ρ : MeasureTheory.Measure (β × Ω)) [MeasureTheory.IsFiniteMeasure ρ] (a : α) : (fun (b : β) => (ProbabilityTheory.Kernel.const α ρ).condKernel (a, b)) =ᵐ[ρ.fst] ⇑ρ.condKernel

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 α β] {ρ : ProbabilityTheory.Kernel α (β × Ω)} [ProbabilityTheory.IsFiniteKernel ρ] {κ : ProbabilityTheory.Kernel (α × β) Ω} [ProbabilityTheory.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.