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

• Meyn, S.P. and Tweedie, R.L., Markov Chains and Stochastic Stability
• C Robert, G Casella, Monte Carlo Statistical Methods

class ProbabilityTheory.Kernel.IsIrreducible {α : Type u_1} {mα : MeasurableSpace α} (φ : MeasureTheory.Measure α) (κ : 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

• irreducible ⦃A : Set α⦄ (hA : MeasurableSet A) (hφA : φ A > 0) (a : α) : ∃ (n : ℕ), ((κ ^ n) a) A > 0

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 α] : IsIrreducible φ Kernel.id

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 φ₁ κ