Chen characterization: CLT $\iff$$\sqrt{n}\bar f_n$ bounded in probability (Jones Thm 4)

Setting. $X$ is an arbitrary type with a measurable-space structure, together with the typeclass assumption that its $\sigma$-algebra is countably generated (generated by some countable family of sets); $P$ is a kernel from $X$ to $X$ assumed (typeclass) to be a Markov kernel, i.e. $P(x,\cdot)$ is a probability measure for every $x$; $\pi$ is a measure on $X$ assumed (typeclass) to be a probability measure. Hypotheses. (1) Harris ergodicity of $(P,\pi)$, which in this bundle means the conjunction of: $\pi$ is invariant for $P$ (the measure $A \mapsto \int_X P(x,A)\,d\pi(x)$ equals $\pi$), and for every starting point $x \in X$, $d_{TV}(P^n(x,\cdot),\pi) \to 0$ as $n \to \infty$; here $P^n$ is the $n$-fold iterate of $P$ defined by $P^0 =$ the identity kernel and $P^{n+1} = P \circ P^n$, and $d_{TV}(\mu,\nu)$ is this bundle's total-variation distance $\sup\{\, |\mu(A) - \nu(A)| : A \text{ measurable}\,\}$ — with no factor $\tfrac12$, measure values converted to reals by a convention sending $\infty$ to $0$ (immaterial for probability measures), and the supremum taken as a real-number supremum whose junk value is $0$ if the set were unbounded (the set always contains $0$, via $A = \varnothing$). (2) $f : X \to \mathbb{R}$ is measurable. (3) $\int_X f\,d\pi = 0$. (4) $f \in L^2(\pi)$ in the MemLp sense: $f$ is $\pi$-almost-everywhere strongly measurable and $\left(\int |f|^2\,d\pi\right)^{1/2} < \infty$. Conclusion — an exact if-and-only-if. Left side: there exists a nonnegative real $v$ such that the functions $Z_n(\omega) = \sqrt{n}\; \bar f_n(\omega)$ converge in distribution to $\mathcal N(0,v)$ as $n \to \infty$, under the path measure $\mu_\pi$. Here $\bar f_n(\omega) = n^{-1} \sum_{i=0}^{n-1} f(\omega_{i+1})$ is the average of $f$ over the chain states at times $1,\dots,n$ — the time-$0$ state $\omega_0$ is never used, and at $n = 0$ Lean's convention $0^{-1} = 0$ together with $\sqrt 0 = 0$ gives $Z_0 = 0$. No centering term is subtracted inside $Z_n$ — centering is supplied only by hypothesis (3). $\mu_\pi$ (chainMeasure P \pi) is the probability law on trajectory space $\mathbb N \to X$ of the time-homogeneous Markov chain with one-step transition kernel $P$ whose initial state $\omega_0$ is drawn from $\pi$ itself (the stationary start; no other initial distribution appears anywhere in this statement), each $\omega_{n+1}$ being drawn from $P(\omega_n,\cdot)$ via the Ionescu–Tulcea trajectory construction. TendstoInDistribution (against the identity map on the probability space $(\mathbb R, \mathcal N(0,v))$) means $\int g(Z_n)\,d\mu_\pi \to \int_{\mathbb R} g\,d\mathcal N(0,v)$ for every bounded continuous $g : \mathbb R \to \mathbb R$; gaussianReal 0 v is the normal law of mean $0$ and variance $v$, which is the Dirac point mass at $0$ when $v = 0$ — so a degenerate limit satisfies the left side. Right side: the same sequence $(Z_n)$ is bounded in probability under $\mu_\pi$, which in this bundle means: for every real $\varepsilon > 0$ there exists a real $K$ (not required to be positive) such that for every $n \in \mathbb N$ simultaneously, $\mu_\pi\{\omega : K < |Z_n(\omega)|\} \le \varepsilon$ (the measure value converted to a real, with $\infty \mapsto 0$ — immaterial since $\mu_\pi$ is a probability measure); the case $n = 0$ is included, where $Z_0 = 0$.