Theorems · Theorem · probability

ProbabilityTheory.Kernel.IsIrreducible.irreducible

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

Defined in

Mathlib.Probability.Kernel.Irreducible

Cited by

1 results in Mathlib

Foundations

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

Assumes

ProbabilityTheory.Kernel.IsIrreducible