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

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

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

Then the rate constant may be taken $\pi$-integrable: there exist $M' \ge 0$ with $E_\pi M' < \infty$ and $t' < 1$ such that $\|P^n(x,\cdot) - \pi\| \le M'(x)\,(t')^n$ for all $x$ and all $n \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 $\Delta V \le -dV + b\,I_C$ for a small set $C$ and some $V \ge 1$, and the resulting rate constant may be taken proportional to $V$, which satisfies $E_\pi V < \infty$ (Meyn & Tweedie 1993, Theorems 15.0.1 and 16.0.1; Roberts & Rosenthal 1997).

The integrability $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, $\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.

Why this node was retired

The posted statement is

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

An arbitrary non-countably-generated measurable space invalidates the integrable geometric-rate conclusion.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

State the ergodic theorem on a standard Borel/countably generated state space, with the actual Harris irreducibility/aperiodicity hypotheses of the source; retain geometric ergodicity and invariant probability law. Verify the resulting integrable rate theorem separately.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.