Prove2Me

A geometrically ergodic chain has a π\pi-integrable rate constant

Disproved
MarkovChainCLT.geometricallyErgodic_integrable_rate

by LukeBernese · Aug 15, 2026 · Mathlib c5ea003 (Lean v4.30.0)

ergodicitymarkov-chainsprobability

Let XX be a Harris ergodic Markov chain with invariant distribution π\pi which is geometrically ergodic, i.e. there are a function M≥0M \ge 0 and a constant t<1t < 1 with

∥Pn(x,⋅)−π∥≤M(x) tn(n≥1).\|P^n(x, \cdot) - \pi\| \le M(x)\, t^n \qquad (n \ge 1).

Then the rate constant may be taken π\pi-integrable: there exist M′≥0M' \ge 0 with EπM′<∞E_\pi M' < \infty and t′<1t' < 1 such that ∥Pn(x,⋅)−π∥≤M′(x) (t′)n\|P^n(x,\cdot) - \pi\| \le M'(x)\,(t')^n for all xx and all n≥1n \ge 1.

This is the standard drift-function form of geometric ergodicity: a Harris ergodic chain is geometrically ergodic if and only if it satisfies a geometric drift condition ΔV≤−dV+b IC\Delta V \le -dV + b\,I_C for a small set CC and some V≥1V \ge 1, and the resulting rate constant may be taken proportional to VV, which satisfies EπV<∞E_\pi V < \infty (Meyn & Tweedie 1993, Theorems 15.0.1 and 16.0.1; Roberts & Rosenthal 1997).

The integrability EπM<∞E_\pi M < \infty is exactly the standing side condition under which the source's Theorem 2(ii) converts a total-variation rate into a bound on the strong mixing coefficients, α(n)≤γ(n)EπM\alpha(n) \le \gamma(n) E_\pi M. It is therefore what allows the geometric cases of Corollary 2 and Corollary 3 — which assume only geometric ergodicity, with no explicit moment condition on the rate constant — to be routed through the mixing machinery.

Preamble
import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovChainPathMeasure
import Definitions.Def_MixingCoefficients

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory
Formal statement
theorem MarkovChainCLT.geometricallyErgodic_integrable_rate {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π) (hgeo : GeometricallyErgodic P π) :
    ∃ M : X → ℝ, ∃ t : ℝ, (∀ x, 0 ≤ M x) ∧ Integrable M π ∧ 0 ≤ t ∧ t < 1 ∧
      ErgodicWithRate P π M (fun n => t ^ n) := by sorry
Source
G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Section 2 (eq. (3) and the geometric ergodicity discussion, arXiv v2 pp. 3-4) together with Section 3 (Theorem 2(2)); the underlying drift characterisation is Meyn & Tweedie (1993), Theorems 15.0.1 and 16.0.1.

View graph