Theorems · Theorem · probability

ProbabilityTheory.eq_condKernel_of_kernel_eq_compProd

∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] {ρ : ProbabilityTheory.Kernel α (β × Ω)}
  [inst_4 : ProbabilityTheory.IsFiniteKernel ρ] {κ : ProbabilityTheory.Kernel (α × β) Ω}
  [ProbabilityTheory.IsFiniteKernel κ],
  ρ.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.

Defined in

Mathlib.Probability.Kernel.Disintegration.Unique

Cited by

0 results in Mathlib

Foundations

Depth 339 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceStandardBorelSpaceNonemptyMeasurableSpace.CountableOrCountablyGeneratedProbabilityTheory.IsFiniteKernelProbabilityTheory.IsFiniteKernel