Theorems · Theorem · probability

ProbabilityTheory.Kernel.isIrreducible_iff

∀ {α : Type u_1} {mα : MeasurableSpace α} (φ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α),
  ProbabilityTheory.Kernel.IsIrreducible φ κ ↔
    ∀ ⦃A : Set α⦄, MeasurableSet A → φ A > 0 → ∀ (a : α), ∃ n, ((κ ^ n) a) A > 0

Defined in

Mathlib.Probability.Kernel.Irreducible

Cited by

0 results in Mathlib

Foundations

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