Poisson equation has an $L^2(\pi)$ solution under the geometric drift condition with $f^2 \le V$

Proved

MarkovChainCLT.poissonEquation_ae_of_geometricDrift

by Cody Wang · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmartingalemcmcpoisson-equationprobability

Let $X = \{X_n\}_{n \ge 0}$ be a Markov chain with transition kernel $P$ on a state space $\mathsf{X}$ , Harris ergodic with invariant probability distribution $\pi$ , and let $f : \mathsf{X} \to \mathbb{R}$ be measurable. Suppose $V : \mathsf{X} \to [1,\infty)$ is measurable, $C \subseteq \mathsf{X}$ is a measurable small set, $d > 0$ and $b$ are constants, the geometric drift condition

(PV)(x) - V(x) \;\le\; -d\,V(x) + b\,\mathbb{1}_C(x) \qquad (x \in \mathsf{X})

holds with $V$ integrable under every $P(x,\cdot)$ , and $f^2 \le V$ pointwise. Write $(Pg)(x) = \int g(y)\,P(x,\mathrm{d}y)$ and $E_\pi f = \int f\,\mathrm{d}\pi$ .

Then the Poisson equation for $f$ has a square-integrable solution: there exists a measurable $g : \mathsf{X} \to \mathbb{R}$ such that

$g \in L^2(\pi)$ ;
$Pg$ is measurable and $Pg \in L^2(\pi)$ ;
$g(x) - (Pg)(x) = f(x) - E_\pi f$ for $\pi$ -almost every $x$ .

The role of this statement is to supply the martingale approximation on which the drift route to the Markov chain central limit theorem rests. Given such a $g$ , the increments $D_i = g(X_{i+1}) - (Pg)(X_i)$ form a stationary, square-integrable martingale difference sequence for the natural filtration of the chain, and the telescoping identity

\sqrt{n}\,\bigl(\bar f_n - E_\pi f\bigr) \;=\; \frac{1}{\sqrt n}\sum_{i=0}^{n-1} D_i \;+\; \frac{1}{\sqrt n}\bigl((Pg)(X_0) - (Pg)(X_n)\bigr)

reduces the central limit theorem for the sample averages $\bar f_n$ to the martingale central limit theorem plus a remainder that vanishes in probability. The hypotheses are exactly those of Theorem 1, condition 1 of the source survey, so the statement isolates the one genuinely Markov-theoretic ingredient of that theorem: the drift condition must be converted into an $L^2(\pi)$ solution of the Poisson equation, everything after that being general martingale theory.

Formalization Note "Harris ergodic" is encoded by its total-variation characterization: $\pi$ is invariant for $P$ and $\|P^n(x,\cdot) - \pi\| \to 0$ for every starting point $x$ . GeoDriftCondition P V d b C carries the integrability of $V$ under every $P(x,\cdot)$ as a conjunct, and IsSmallSet P C is the minorization condition $P^{n_0}(x,A) \ge \varepsilon\,Q(A)$ for $x \in C$ . The $\sigma$ -algebra of the state space is assumed countably generated, the standard general-state-space setting of Meyn and Tweedie, matching the parent theorem. The conclusion asserts the Poisson identity only $\pi$ -almost everywhere, which is all the martingale approximation consumes; the classical construction in fact gives it at every $x$ . The conclusion's shape deliberately matches the existing platform theorem MarkovChainCLT.poissonEquation_ae_of_uniformlyErgodic, so the two are interchangeable in downstream martingale-approximation arguments.

Preamble

import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovDriftMinorization
import Definitions.Def_MarkovChainPathMeasure

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory

Formal statement

theorem MarkovChainCLT.poissonEquation_ae_of_geometricDrift {X : Type*} [MeasurableSpace X]
    [MeasurableSpace.CountablyGenerated X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π) (f : X → ℝ) (hf : Measurable f)
    (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)
    (hfV : ∀ x, f x ^ 2 ≤ V x) :
    ∃ g : X → ℝ, Measurable g ∧ MemLp g 2 π ∧
      Measurable (fun x => ∫ y, g y ∂(P x)) ∧
      MemLp (fun x => ∫ y, g y ∂(P x)) 2 π ∧
      ∀ᵐ x ∂π, g x - ∫ y, g y ∂(P x) = f x - ∫ x, f x ∂π := by sorry

Source

G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Theorem 1 condition 1 (drift eq. (5), f^2 <= V) and Remark 2, which attributes that condition to Meyn & Tweedie 1993. This theorem isolates the Poisson-equation (martingale-approximation) step of that proof. Original sources: S. P. Meyn & R. L. Tweedie, Markov Chains and Stochastic Stability (Springer 1993; 2nd ed. Cambridge Univ. Press 2009), Chapter 16 'V-Uniform Ergodicity' (Theorem 16.0.1: the geometric drift condition towards a small set is equivalent to V-uniform ergodicity) and Chapter 17, Section 17.4, where the CLT of Theorem 17.0.1 is proved via a square-integrable solution of the Poisson equation; and P. W. Glynn & S. P. Meyn, "A Liapounov bound for solutions of the Poisson equation", Annals of Probability 24 (1996) 916-931, which gives the Lyapunov bound g^2 <= cV on the solution under a drift condition for V with f^2 <= V.

View graph

Poisson equation has an L2(π)L^2(\pi)L2(π) solution under the geometric drift condition with f2≤Vf^2 \le Vf2≤V

Poisson equation has an $L^2(\pi)$ solution under the geometric drift condition with $f^2 \le V$