Theorems · Theorem · probability

ProbabilityTheory.Kernel.condKernel_def

∀ {α : Type u_5} {β : Type u_6} {Ω : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] [inst_1 : Nonempty Ω]
  [h : MeasurableSpace.CountableOrCountablyGenerated α β] (κ : ProbabilityTheory.Kernel α (β × Ω))
  [inst_2 : ProbabilityTheory.IsFiniteKernel κ],
  κ.condKernel =
    if hα : Countable α then ProbabilityTheory.Kernel.condKernelCountable (fun a => (κ a).condKernel) ⋯
    else κ.condKernelBorel

Defined in

Mathlib.Probability.Kernel.Disintegration.StandardBorel

Cited by

0 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceNonemptyMeasurableSpace.CountableOrCountablyGeneratedProbabilityTheory.IsFiniteKernel