Uniform ergodicity $\iff$ uniform ( $\varphi$ -) mixing, with exponential rate (Jones Thm 2(iv))

Disproved

MarkovChainCLT.uniformly_ergodic_iff_phi_mixing

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

markov-chainsmcmcmixing-processesprobability

Let $X$ be a Markov chain with transition kernel $P$ , Harris ergodic with invariant probability $\pi$ . Then the chain is uniformly ergodic if and only if its stationary version is uniformly mixing ( $\varphi(n) \to 0$ ); and if it is uniformly ergodic, the mixing is exponentially fast: there exist $c \ge 0$ and $\theta > 0$ with

\varphi(n) \;\le\; c\, e^{-\theta n} \qquad (n \ge 1).

This equivalence (Ibragimov–Linnik) identifies the strongest classical mixing condition with the strongest ergodicity condition, and feeds the uniformly ergodic CLT (Corollary 5).

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$ (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. The $\sigma$ -algebra of the state space is additionally assumed countably generated, the standard general-state-space setting of Meyn and Tweedie.

Preamble

import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovChainPathMeasure
import Definitions.Def_MixingCoefficients

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory

/-- **Theorem 2, part 4** (Ibragimov–Linnik 1971, pp. 367–368; Bradley 1986):
a Harris ergodic chain is uniformly ergodic if and only if its stationary version is
uniformly (φ-) mixing, in which case the φ-mixing is exponentially fast. -/

Formal statement

theorem MarkovChainCLT.uniformly_ergodic_iff_phi_mixing {X : Type*} [MeasurableSpace X]
    [MeasurableSpace.CountablyGenerated X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π) :
    (UniformlyErgodic P π ↔
      Tendsto (fun n => phiMixingCoef (chainMeasure P π) (fun i ω => ω i) n)
        atTop (𝓝 0)) ∧
    (UniformlyErgodic P π → ∃ c θ : ℝ, 0 ≤ c ∧ 0 < θ ∧ ∀ n : ℕ, 1 ≤ n →
      phiMixingCoef (chainMeasure P π) (fun i ω => ω i) n ≤ c * Real.exp (-θ * n)) := by sorry

Source

G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Theorem 2, part 4 (arXiv v2 p. 8); original: I. A. Ibragimov & Y. V. Linnik, Independent and Stationary Sequences of Random Variables (1971), pp. 367-368, plus R. C. Bradley (1986), Theorem 4.2

Read-back

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

Let $X$ be a type with a countably generated σ-algebra (MeasurableSpace.CountablyGenerated: generated by some countable family of sets), $P$ a Markov kernel from $X$ to itself (each $P(x,\cdot)$ a probability measure), and $\pi$ a probability measure on $X$ , assumed Harris ergodic: $\pi$ is invariant for $P$ and for every $x\in X$ , $\operatorname{tv}(P^n(x,\cdot),\pi)\to0$ , with $P^n$ the $n$ -fold iterate ( $P^0$ = identity) and $\operatorname{tv}(\mu,\nu)=\sup\{|\mu(A)-\nu(A)|:A\text{ measurable}\}$ (real supremum, no factor $\tfrac12$ ). Write $\varphi(n)$ for the bundle's φ-mixing coefficient of the coordinate process $\omega\mapsto\omega_i$ under the stationary path measure $\mathbb P$ — the Ionescu–Tulcea measure on $\mathbb{N}\to X$ of the chain started from $\pi$ ( $\omega_0\sim\pi$ , $\omega_{n+1}\sim P(\omega_n,\cdot)$ ): unfolded, $\varphi(n)$ is the real supremum (sSup) of the set of values $\big|\mathbb P(A\cap B)/\mathbb P(A)\ -\ \mathbb P(B)\big|$ over all $k\in\mathbb{N}$ , all events $A$ measurable for the σ-algebra generated by coordinates $\{0,\dots,k\}$ with $\mathbb P(A)\ne 0$ , and all events $B$ measurable for the σ-algebra generated by coordinates $\{k+n,k+n+1,\dots\}$ (measure values converted to reals before dividing and subtracting; the set contains $0$ , e.g. $A$ = whole space, $B=\emptyset$ ; a real sSup of an empty or unbounded set would be $0$ by convention). Uniform ergodicity unfolds as: there exist reals $R\ge 0$ and $0\le t<1$ such that $\operatorname{tv}(P^n(x,\cdot),\pi)\le R\,t^{\,n}$ for every $x\in X$ and every $n\ge1$ (a state-independent geometric bound; nothing claimed at $n=0$ ). The conclusion is the conjunction of two claims: (a) a genuine equivalence — $P$ is uniformly ergodic for $\pi$ if and only if $\varphi(n)\to0$ as $n\to\infty$ (the forward direction gives only the limit, with no rate); and (b) a one-way implication — if $P$ is uniformly ergodic for $\pi$ then there exist reals $c\ge 0$ (zero allowed) and $\theta>0$ such that $\varphi(n)\le c\,e^{-\theta n}$ for every $n\ge1$ ( $n=0$ excluded; one pair $(c,\theta)$ for all such $n$ ). No converse of (b) is asserted: an exponential φ-mixing rate is not claimed to imply uniform ergodicity, except insofar as (a) already converts $\varphi(n)\to0$ back into uniform ergodicity.

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

Uniform ergodicity ⟺ \iff⟺ uniform (φ\varphiφ-) mixing, with exponential rate (Jones Thm 2(iv))

Uniform ergodicity $\iff$ uniform ( $\varphi$ -) mixing, with exponential rate (Jones Thm 2(iv))