Theorems · Theorem · probability

MeasureTheory.Measure.IsCondKernel.isMarkovKernel

∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω))
  (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] [MeasureTheory.IsFiniteMeasure ρ]
  [MeasurableSingletonClass α], (∀ (a : α), ρ.fst {a} ≠ 0) → ProbabilityTheory.IsMarkovKernel ρCond

Defined in

Mathlib.Probability.Kernel.Disintegration.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.Measure.IsCondKernelMeasureTheory.IsFiniteMeasureMeasurableSingletonClass