Geometric ergodicity CLT under $E_\pi[f^2 \log^+|f|] < \infty$ (Jones Cor 3)

Open

MarkovChainCLT.clt_of_geometric_of_log_moment

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

markov-chainsmcmcprobability

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. Write $\bar f_n = n^{-1} \sum_{i=1}^{n} f(X_i)$ for the sample average and $E_\pi f = \int f \, d\pi$ . Suppose the chain is geometrically ergodic and

E_\pi\bigl[f^2 \, \log^+ |f|\bigr] < \infty, \qquad \log^+ t = \max(0, \log t).

Then the chain satisfies the central limit theorem for $f$ : there is a single asymptotic variance $\sigma_f^2 \ge 0$ such that for every initial distribution of the chain,

\sqrt{n}\,\bigl(\bar f_n - E_\pi f\bigr) \xrightarrow{d} N(0, \sigma_f^2) \qquad (n \to \infty).

This refines the Chan–Geyer condition: for geometrically ergodic chains a logarithmic sliver above square-integrability suffices (and, by the counterexamples cited in the source, a bare second moment does not).

Formalization Note The stated moment already implies $E_\pi f^2 < \infty$ , so it is not assumed separately. "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$ (equivalent to the classical aperiodic, $\psi$ -irreducible, positive Harris recurrent definition; the "every $x$ " quantifier is exactly the Harris property). Convergence in distribution is weak convergence of laws, and $N(0, 0)$ is read as the point mass at $0$ , which absorbs the source's " $\sigma_f^2 > 0$ " caveat.

Preamble

import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovChainPathMeasure
import Mathlib.Analysis.SpecialFunctions.Log.PosLog

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory

/-- **Corollary 3**: a geometrically ergodic Harris chain with
`E_π[f² log⁺|f|] < ∞` satisfies the CLT for every initial distribution. -/

Formal statement

theorem MarkovChainCLT.clt_of_geometric_of_log_moment {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π) (f : X → ℝ) (hf : Measurable f)
    (hgeo : GeometricallyErgodic P π)
    (hmom : Integrable (fun x => f x ^ 2 * Real.posLog |f x|) π) :
    SatisfiesCLT P π f := by sorry

Source

G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Corollary 3 (arXiv v2 p. 11; proved there from Theorem 6 via Theorem 2(ii))

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Setting. $X$ is an arbitrary type with a measurable-space structure; $P$ is a kernel from $X$ to $X$ assumed (typeclass) to be a Markov kernel ( $P(x,\cdot)$ a probability measure for every $x$ ); $\pi$ is a measure on $X$ assumed (typeclass) to be a probability measure. Hypotheses. (1) Harris ergodicity: $\pi$ is invariant for $P$ ( $A \mapsto \int_X P(x,A)\,d\pi(x)$ equals $\pi$ ) and for every $x \in X$ , $d_{TV}(P^n(x,\cdot),\pi) \to 0$ as $n \to \infty$ , where $P^n$ is the $n$ -fold iterate ( $P^0 =$ identity kernel, $P^{n+1} = P \circ P^n$ ) and $d_{TV}(\mu,\nu) = \sup\{\,|\mu(A)-\nu(A)| : A \text{ measurable}\,\}$ (no factor $\tfrac12$ ; measure values sent to reals with $\infty \mapsto 0$ ; real supremum with junk value $0$ if unbounded, set contains $0$ via $A=\varnothing$ ). (2) $f : X \to \mathbb R$ is measurable. (3) Geometric ergodicity: there exist $M : X \to \mathbb R$ and $t \in \mathbb R$ with $M(x) \ge 0$ for all $x$ (no measurability or integrability of $M$ is required), $0 \le t < 1$ , and $d_{TV}(P^n(x,\cdot),\pi) \le M(x)\,t^n$ for every $x$ and every $n \ge 1$ (ordinary power $t^n$ ; nothing asserted at $n=0$ ). (4) $L^2 \log L$ -type moment: the function $x \mapsto f(x)^2 \cdot \log^+ |f(x)|$ is integrable with respect to $\pi$ ( $\pi$ -a.e. strongly measurable with finite integral of its absolute value), where $f(x)^2$ is the ordinary square and $\log^+ s = \max(0, \log s)$ is the positive part of the natural logarithm (Real.posLog); consequently the integrand vanishes wherever $|f(x)| \le 1$ — in particular where $f(x)=0$ (Lean's $\log 0 = 0$ ) — so this hypothesis constrains $f$ only where $|f| > 1$ . No other moment or $L^2$ hypothesis on $f$ appears. Conclusion ( $f$ satisfies the CLT for $(P,\pi)$ , unfolded): there exists a nonnegative real $v$ such that for every probability measure $\lambda$ on $X$ — a single $v$ for all $\lambda$ ; existential over $v$ before universal over $\lambda$ — the functions $Z_n(\omega) = \sqrt{n}\,\left(\bar f_n(\omega) - \int_X f\,d\pi\right)$ converge in distribution to $\mathcal N(0,v)$ as $n \to \infty$ under the path measure $\mu_\lambda$ , where: $\bar f_n(\omega) = n^{-1}\sum_{i=0}^{n-1} f(\omega_{i+1})$ averages $f$ over the chain states at times $1,\dots,n$ (the time- $0$ state is never used; at $n=0$ , $0^{-1}=0$ and $\sqrt 0=0$ give $Z_0=0$ ); the centering constant is the $\pi$ -mean for every $\lambda$ ; $\mu_\lambda$ is the law on $\mathbb N \to X$ of the time-homogeneous Markov chain with transition kernel $P$ started with $\omega_0 \sim \lambda$ ( $\omega_{n+1} \sim P(\omega_n,\cdot)$ , Ionescu–Tulcea); convergence in distribution means $\int g(Z_n)\,d\mu_\lambda \to \int_{\mathbb R} g\,d\mathcal N(0,v)$ for every bounded continuous $g : \mathbb R \to \mathbb R$ ; and $\mathcal N(0,v)$ is the normal law of mean $0$ and variance $v$ , equal to the Dirac point mass at $0$ when $v=0$ (degenerate limit allowed).

Human review

Endorsed by Community (Bot) · Aug 15, 2026
Endorsed by Shuze Chen · Aug 15, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Geometric ergodicity CLT under Eπ[f2log⁡+∣f∣]<∞E_\pi[f^2 \log^+|f|] < \inftyEπ​[f2log+∣f∣]<∞ (Jones Cor 3)

Geometric ergodicity CLT under $E_\pi[f^2 \log^+|f|] < \infty$ (Jones Cor 3)