Markov chain CLT with autocovariance-series variance (Lemma EC.4, scalar form)

Let $X = \{X_n\}$ be a Harris ergodic, uniformly ergodic Markov chain with kernel $P$ and stationary distribution $\pi$, and let $f$ be measurable with $E_\pi f^2 < \infty$. Then: (i) the autocovariance series $\sum_{k \ge 1} \mathrm{Cov}_\pi(f(X_0), f(X_k))$ is summable; (ii) the asymptotic variance $\sigma^2(f) = \mathrm{Var}_\pi(f) + 2\sum_{k\ge 1}\mathrm{Cov}_\pi(f(X_0), f(X_k))$ is nonnegative; and (iii) for every initial distribution, $\sqrt{n}\,(\bar f_n - E_\pi f) \xrightarrow{d} N(0, \sigma^2(f))$ where $\bar f_n = n^{-1}\sum_{i=1}^n f(X_i)$. This sharpens the platform's uniformly ergodic CLT (MarkovChainCLT.clt_of_uniformly_ergodic, which asserts existence of some asymptotic variance) by identifying the variance as the autocovariance series — the scalar form of the multivariate Markov chain CLT quoted as Lemma EC.4 of arXiv:2407.19618 (Vats 2017); the multivariate statement follows coordinatewise/directionally since the identified variance is a quadratic form in the observable.