Finite-order exponential mixing does not imply the central limit theorem
Bernat Bassols Cornudella, Matheus M Castro
math.DS
Oct 12, 2026 · v1
math.PR
TL;DR
The main Theorems A, B and C, plus the external results they rely on, are formalised in Lean 4 with Mathlib, using only the standard axioms.
Abstract
We show that finite-order exponential mixing does not imply the central limit theorem for smooth diffeomorphisms. For every integer $R\geq2$, we construct a $\mathcal{C}^{\infty}$ diffeomorphism $T:M\to M$ of a compact smooth manifold $M$ and a $T$-invariant probability measure $μ$ such that $(T,μ)$ is exponentially mixing of order $R$ for $\mathcal{C}^1(M)$ observables, but not of order $2R+2$. For some centred observable $f_0\in\mathcal{C}^{\infty}(M)$, no subsequence of the normalised sums $\frac{1}{\sqrt n}\sum_{i=0}^{n-1}f_0\circ T^i$ converges in distribution to a Gaussian law. In particular, exponential decay of two-point correlations implies neither exponential mixing of all orders nor the central limit theorem. We realise $(T,μ)$ in two ways. In the first, $T$ is a fixed linear Anosov diffeomorphism of $\mathbb T^2$ and $μ$ is singular with respect to Lebesgue measure. In the second, $M$ can be any compact smooth surface without boundary and $μ$ is a physical measure whose statistical basin contains a nonempty open set. The main theorems have been formalised in Lean 4.
Problem
Whether exponential mixing of finite order for smooth diffeomorphisms implies the central limit theorem for smooth observables. A related question is whether exponential decay of two-point correlations implies mixing of all orders.
Approach
The authors construct a stationary {-1,1}-valued process using nested random marker sets built from finitely dependent colourings. Block laws are defined recursively to preserve marginals on fewer than L=2R+2 children while creating negative L-point correlations. The resulting shift-invariant measure is realised smoothly in two ways: on a linear Anosov diffeomorphism of the 2-torus with a singular measure, and on any compact surface with a physical measure. The main theorems are formalised in Lean 4 with Mathlib.
Results
For every R≥2 there is a C^∞ diffeomorphism and invariant measure that is exponentially mixing of order R for C^1 observables but not of order 2R+2. For this system, the normalised Birkhoff sums of some smooth centred observable have no Gaussian subsequential limit. The Lean proofs are kernel-checked using only propext, Classical.choice and Quot.sound.
