Prove2Me

A geometric drift function is π\pi-integrable (Meyn-Tweedie Thm 14.3.7)

Proved
MarkovChainCLT.integrable_of_geoDriftCondition

by BrunoDCDO · Sep 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

ergodicitymarkov-chainsprobability

Let XX be a Harris ergodic Markov chain with transition kernel PP and invariant probability distribution π\pi. Suppose a measurable function V:X→[1,∞)V : \mathsf{X} \to [1,\infty) satisfies the geometric drift condition towards a measurable small set CC: VV is integrable under every P(x,⋅)P(x,\cdot) and, for some d>0d > 0 and some bb,

ΔV(x)=PV(x)−V(x)≤−d V(x)+b 1C(x)(x∈X).\Delta V(x) = PV(x) - V(x) \le -d\,V(x) + b\,\mathbb{1}_C(x) \qquad (x \in \mathsf{X}).

Then VV is π\pi-integrable:

EπV=∫V dπ<∞.E_\pi V = \int V \, d\pi < \infty.

This is Theorem 14.3.7 of Meyn and Tweedie (1993), quoted in the source's Remark 1 as "if (5) holds then EπV<∞E_\pi V < \infty". It is the step that turns the drift function of a geometrically ergodic chain into a π\pi-integrable rate constant, which is the standing side condition EπM<∞E_\pi M < \infty under which the source's Theorem 2(ii) bounds the strong mixing coefficients by the total-variation rate.

Formalization Note Harris ergodicity is the mission's total-variation encoding (HarrisErgodic), which gives the invariance of π\pi and the ψ\psi-irreducibility that Meyn and Tweedie assume; the drift condition is the platform's GeoDriftCondition, whose integrability conjunct rules out the vacuous reading of a non-integrable VV. The σ\sigma-algebra of the state space is assumed countably generated (MeasurableSpace.CountablyGenerated X), the standing assumption of Meyn and Tweedie (1993, Section 3.1) on which the existence of small sets (their Theorem 5.2.2) rests; the mission's Theorem 1(i) milestone carries the same hypothesis.

Preamble
import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovDriftMinorization

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory
Formal statement
theorem MarkovChainCLT.integrable_of_geoDriftCondition {X : Type*} [MeasurableSpace X]
    [MeasurableSpace.CountablyGenerated X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π)
    (V : X → ℝ) (hV : Measurable V) (hV1 : ∀ x, 1 ≤ V x)
    (C : Set X) (hC : MeasurableSet C) (hsmall : IsSmallSet P C)
    (d b : ℝ) (hd : 0 < d) (hdrift : GeoDriftCondition P V d b C) :
    Integrable V π := by sorry
Source
G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Section 2, Remark 1 (arXiv v2 pp. 3-4); original: S. P. Meyn & R. L. Tweedie, Markov Chains and Stochastic Stability (1993), Theorem 14.3.7; standing assumption: Meyn & Tweedie (1993), Section 3.1 (countably generated sigma-field) and Theorem 5.2.2 (existence of small sets)

View graph