Harris ergodic chains are strongly mixing: $\alpha(n) \to 0$ (Jones Thm 2(i))

Let $X$ be a type with a countably generated σ-algebra (MeasurableSpace.CountablyGenerated: generated by countably many sets), $P$ a Markov kernel from $X$ to itself (each $P(x,\cdot)$ a probability measure), and $\pi$ a probability measure on $X$. The single substantive hypothesis is Harris ergodicity: $\pi$ is invariant for $P$, and for every starting point $x\in X$, $\operatorname{tv}(P^n(x,\cdot),\pi)\to 0$ as $n\to\infty$, where $P^n$ is the $n$-fold kernel iterate ($P^0$ = identity) and $\operatorname{tv}(\mu,\nu)=\sup\{|\mu(A)-\nu(A)|:A\text{ measurable}\}$ (a real supremum, values of measures converted to reals, no factor $\tfrac12$). The conclusion is a pure limit statement with no rate: $\alpha(n)\to 0$ as $n\to\infty$, where $\alpha(n)$ is the bundle's α-mixing coefficient of the coordinate process $\omega\mapsto\omega_i$ under the stationary path measure — the Ionescu–Tulcea measure $\mathbb P$ on $\mathbb{N}\to X$ of the chain started from the invariant law itself ($\omega_0\sim\pi$, $\omega_{n+1}\sim P(\omega_n,\cdot)$). Unfolded, $\alpha(n)$ is the supremum (real sSup) of the set of numbers $\big|\mathbb P(A\cap B)-\mathbb P(A)\,\mathbb P(B)\big|$ taken over all split points $k\in\mathbb{N}$, all events $A$ measurable with respect to the σ-algebra generated by the coordinates $\{0,1,\dots,k\}$, and all events $B$ measurable with respect to the σ-algebra generated by the coordinates $\{k+n,k+n+1,\dots\}$ (measure values converted to reals; the supremum over $k$ is built into the definition, so the coefficient is uniform over the split point). This set always contains $0$ (take $A=B=\emptyset$), and for a probability measure it is bounded, so the real supremum is the honest one; by Lean's convention sSup of an empty or unbounded set of reals would be $0$.