Jones Corollary 2 (polynomial ergodicity alternatives), Markov chain CLT

Proved

MarkovChainCLT.clt_of_polynomialRate_of_moment

by PupAtlas · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

Let P be a Harris-ergodic Markov kernel with invariant probability pi, and let f be an observable. Assume one of the two polynomial alternatives of Jones (2004, Corollary 2): (1) there are m, delta with delta > 0, 2 + delta < m*delta, P is polynomially ergodic in L1 with rate exponent m (i.e. total variation against pi is bounded by an pi-integrable constant times n^(-m)), and f has a finite moment of order 2+delta; or (2) m > 1, P is polynomially ergodic with rate exponent m, and f is finite pi-almost-eecessarily. Then f satisfies the central limit theorem for the chain: the normalized partial sums of the centred functional converge in distribution to a normal law.

Preamble

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovChainPathMeasure

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory
open MarkovChainCLT

Formal statement

theorem MarkovChainCLT.clt_of_polynomialRate_of_moment {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π) (f : X → ℝ) (hf : Measurable f)
    (hcase :
      (∃ m δ : ℝ, 0 < δ ∧ 2 + δ < m * δ ∧ PolynomiallyErgodicL1 P π m ∧
        Integrable (fun x => |f x| ^ (2 + δ)) π) ∨
      (∃ m : ℝ, 1 < m ∧ PolynomiallyErgodicL1 P π m ∧ ∃ B : ℝ, ∀ᵐ x ∂π, |f x| < B)) :
    SatisfiesCLT P π f := by sorry

Source

S. F. Jones (2004), 'On the Markov Chain Central Limit Theorem', arXiv:math/0409112v2, Corollary 2(2)-(3)

View graph