An $L^2(\pi)$ Poisson solution under polynomial drift

Proved

MarkovChainCLT.poissonEquation_ae_of_polynomialDrift

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

markov-chainsmartingalepoisson-equationprobability

Let $P$ be a Harris ergodic Markov kernel on a countably generated measurable state space, with invariant probability measure $\pi$ . Let $V\ge1$ and $f$ be measurable, let $C$ be a measurable small set, and assume $V$ is integrable under $P(x,\cdot)$ for every $x$ . Suppose $d>0$ , $b\in\mathbb R$ , and $0\le\tau<1$ satisfy

PV(x)-V(x)\le-dV(x)^\tau+b\mathbf1_C(x).

For a real $\eta$ satisfying $1-\tau\le\eta\le1$ , assume

\int V^{2\eta}\,d\pi<\infty, \qquad |f(x)|\le V(x)^{\tau+\eta-1}\quad\text{for every }x.

Then there is a measurable solution $g$ of the centered Poisson equation such that

g\in L^2(\pi),\qquad Pg\text{ is measurable},\qquad Pg\in L^2(\pi), \qquad g-Pg=f-\pi(f)\quad\pi\text{-almost everywhere}.

Here $Pg(x)=\int g(y)\,P(x,dy)$ and $\pi(f)=\int f\,d\pi$ .

This isolates the Poisson-equation ingredient of the polynomial-drift central limit theorem. Its conclusion also supports martingale approximations and bounds for additive functionals, independently of a central limit theorem.

Formalization Note. Harris ergodicity and smallness use the existing mission definitions. The Poisson identity is required only almost everywhere under the invariant measure. The case $\tau=0$ forces $\eta=1$ and is included.

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_polynomialDrift {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) (hτ0 : 0 ≤ τ) (hτ1 : τ < 1)
    (hdrift : PolyDriftCondition P V d b τ C)
    (η : ℝ) (hη0 : 1 - τ ≤ η) (hη1 : η ≤ 1)
    (hVint : Integrable (fun x => V x ^ (2 * η)) π)
    (hfV : ∀ x, |f x| ≤ V x ^ (τ + η - 1)) :
    ∃ 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), arXiv math/0409112v2, p. 4, Theorem 1(2), equation (6), and Remark 2: https://arxiv.org/pdf/math/0409112. Poisson-equation formulation derived from P. W. Glynn and S. P. Meyn, A Liapounov Bound for Solutions of the Poisson Equation, Annals of Probability 24 (1996), 916–931, equation (8) p. 919 and Theorem 2.3 p. 921: https://web.stanford.edu/~glynn/papers/1996/GM96.pdf. Apply that weighted Poisson theorem after the concave-power drift transformation W=V^eta and F=V^(tau+eta-1); the bound |g| <= const*(W+1) and pi(V^(2*eta))<infinity give L2. The source of the parent CLT is Jarner–Roberts (2002), Theorem 4.2.

View graph

An L2(π)L^2(\pi)L2(π) Poisson solution under polynomial drift

An $L^2(\pi)$ Poisson solution under polynomial drift