Irreducibility of kernels #
A kernel κ : Kernel α α is φ-irreducible, for a given measure φ on α,
if for every measurable set A with positive measure under φ, and for every a : α,
there exists a positive integer n such that we have (κ ^ n) a A > 0.
When the kernel κ is the transition kernel of a Markov chain,
this precisely means that the Markov chain is φ-irreducible,
that is, there is a positive probability of reaching any
(φ-positive measure) set of states from any other state within a finite number of steps.
Main definitions #
ProbabilityTheory.Kernel.IsIrreducible: irreducibility of a given kernel with respect to a measureφ.
Main statements #
isIrreducible_of_le_measure: If a kernelκis irreducible with respect to a measureφ₂, then it is also irreducible with respect to any measureφ₁withφ₁ ≤ φ₂.
References #
class
ProbabilityTheory.Kernel.IsIrreducible
{α : Type u_1}
{mα : MeasurableSpace α}
(φ : MeasureTheory.Measure α)
(κ : Kernel α α)
:
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
Instances
theorem
ProbabilityTheory.Kernel.isIrreducible_iff
{α : Type u_1}
{mα : MeasurableSpace α}
(φ : MeasureTheory.Measure α)
(κ : Kernel α α)
:
IsIrreducible φ κ ↔ ∀ ⦃A : Set α⦄, MeasurableSet A → φ A > 0 → ∀ (a : α), ∃ (n : ℕ), ((κ ^ n) a) A > 0
instance
ProbabilityTheory.Kernel.instIsIrreducibleIdOfSubsingleton
{α : Type u_1}
{mα : MeasurableSpace α}
{φ : MeasureTheory.Measure α}
[Subsingleton α]
:
instance
ProbabilityTheory.Kernel.instIsIrreducibleHSMulENNRealMeasure
{α : Type u_1}
{mα : MeasurableSpace α}
{c : ENNReal}
{φ : MeasureTheory.Measure α}
{κ : Kernel α α}
[hκ : IsIrreducible φ κ]
:
IsIrreducible (c • φ) κ
theorem
ProbabilityTheory.Kernel.isIrreducible_of_le_measure
{α : Type u_1}
{mα : MeasurableSpace α}
{φ₁ φ₂ : MeasureTheory.Measure α}
(hφ : φ₁ ≤ φ₂)
{κ : Kernel α α}
[hκ : IsIrreducible φ₂ κ]
:
IsIrreducible φ₁ κ