# 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α : } [] [] {ρ : MeasureTheory.Measure (α × Ω)} (κ : ()) (hκ : ρ = ρ.fst.compProd κ) {s : Set Ω} (hs : ) :
∀ᵐ (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α : } {ρ : } (κ : ) (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α : } [] [] {ρ : MeasureTheory.Measure (α × Ω)} (κ : ()) (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α : } {mβ : } [] [] {ρ : (ProbabilityTheory.kernel α (β × Ω))} {κ : (ProbabilityTheory.kernel (α × β) Ω)} (hκ : ) (a : α) :
().ae.EventuallyEq (fun (b : β) => κ (a, b)) (ρ a).condKernel
theorem ProbabilityTheory.kernel.condKernel_apply_eq_condKernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] (κ : (ProbabilityTheory.kernel α (β × Ω))) (a : α) :
().ae.EventuallyEq (fun (b : β) => (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.

theorem ProbabilityTheory.condKernel_const {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : } {mβ : } [] [] (ρ : MeasureTheory.Measure (β × Ω)) (a : α) :
ρ.fst.ae.EventuallyEq (fun (b : β) => ) ρ.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α : } {mβ : } [] [] {ρ : (ProbabilityTheory.kernel α (β × Ω))} {κ : (ProbabilityTheory.kernel (α × β) Ω)} (hκ : ) (a : α) :
∀ᵐ (x : β) ∂, κ (a, x) = (a, x)

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