Theorems · Inductive type · probability

ProbabilityTheory.Kernel.IsIrreducible

{α : Type u_1} → {mα : MeasurableSpace α} → MeasureTheory.Measure α → ProbabilityTheory.Kernel α α → Prop

A kernel κ : Kernel α α is φ-irreducible (w.r.t. a given measure φ on α), if for every measurable set A with positive measure under φ, and for every a : α, there exists an integer n such that (κ ^ n) a A > 0. Ref. Meyn-Tweedie Proposition 4.2.1(ii), page 89

Defined in

Mathlib.Probability.Kernel.Irreducible

Cited by

3 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms