The Markov chain CLT: six sufficient conditions (Jones Thm 9, mission goal)

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) A six-way disjunction — at least one of the following holds. Throughout: polynomially ergodic in the $L^1$ sense with exponent $m$ means there exists $M : X \to \mathbb R$, pointwise nonnegative and integrable with respect to $\pi$, with $d_{TV}(P^n(x,\cdot),\pi) \le M(x)\,n^{-m}$ for every $x$ and every $n \ge 1$ (real number $n$ raised to the real exponent $-m$; only $n \ge 1$ constrained); geometrically ergodic means 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$ 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$; uniformly ergodic means there exist reals $R \ge 0$ and $0 \le t < 1$ with $d_{TV}(P^n(x,\cdot),\pi) \le R\,t^n$ for every $x$ and every $n \ge 1$ (state-independent constant); $f \in L^2(\pi)$ (MemLp) means $f$ is $\pi$-a.e. strongly measurable with $\left(\int|f|^2\,d\pi\right)^{1/2} < \infty$; and integrability of a function means $\pi$-a.e. strong measurability with finite integral of its absolute value. The disjuncts: (A) there exists a real $m$ with $1 < m$ such that $P$ is polynomially ergodic in the $L^1$ sense with exponent $m$, and there exists a real $B$ (no positivity constraint stated) with $|f(x)| < B$ strictly for $\pi$-almost every $x$. (B) there exist reals $m, \delta$ with $0 < \delta$ and $2 + \delta < m\,\delta$, such that $P$ is polynomially ergodic in the $L^1$ sense with exponent $m$, and $x \mapsto |f(x)|^{2+\delta}$ is integrable with respect to $\pi$ (real-exponent power of the nonnegative base $|f(x)|$, with $0^{2+\delta}=0$). (C) $P$ is geometrically ergodic and there exists a real $\delta > 0$ such that $x \mapsto |f(x)|^{2+\delta}$ is integrable with respect to $\pi$. (D) $P$ is geometrically ergodic and $x \mapsto f(x)^2 \cdot \log^+|f(x)|$ is integrable with respect to $\pi$, where $f(x)^2$ is the ordinary square and $\log^+ s = \max(0,\log s)$ (Real.posLog) — this integrand vanishes wherever $|f(x)| \le 1$, including where $f(x) = 0$ (Lean's $\log 0 = 0$). (E) $P$ is geometrically ergodic, and $P$ is reversible with respect to $\pi$ (Kernel.IsReversible: the joint law of $(x,y)$ with $x \sim \pi$, $y \sim P(x,\cdot)$ — the measure $\pi \otimes P$ on $X \times X$ — is invariant under swapping the coordinates, i.e. detailed balance), and $f \in L^2(\pi)$. (F) $P$ is uniformly ergodic and $f \in L^2(\pi)$. 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$ is claimed to work for all $\lambda$; the existential over $v$ precedes the 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$, Lean's $0^{-1}=0$ and $\sqrt 0=0$ give $Z_0=0$); the centering constant is the $\pi$-mean $\int f\,d\pi$ for every initial law $\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 construction); 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)$ (gaussianReal 0 v) is the normal law of mean $0$ and variance $v$, equal to the Dirac point mass at $0$ when $v = 0$, so a degenerate limit is allowed.