Read-back: MarkovChainCLT.clt_asymptotic_variance_of_uniformly_ergodic

Setting. Let $X$ be an arbitrary type equipped with a measurable-space structure (no topological or countability assumptions). Let $P$ be a Markov transition kernel on $X$ (each $P(x,\cdot)$ is a probability measure), and let $\pi$ be a probability measure on $X$. Write $P^n$ for the $n$-step kernel defined by iteration: $P^0(x,\cdot) = \delta_x$ (the Dirac/identity kernel) and $P^{n+1} = P \circ P^n$.

Custom notions used, unfolded.

• Total variation distance (custom normalization): for measures $\mu,\nu$,

$$d_{TV}(\mu,\nu) \;=\; \sup\big\{\, |\mu(A) - \nu(A)| \;:\; A \subseteq X \text{ measurable} \,\big\},$$

where the measure values are converted from extended nonnegative reals to reals before subtracting (an infinite-measure value is converted to the junk value $0$; for probability measures this has no effect).

• Harris ergodicity (custom): the conjunction of (i) $\pi$ is invariant for $P$ (the pushforward of $\pi$ through $P$ is $\pi$), and (ii) for every starting point $x \in X$, $\;d_{TV}\big(P^n(x,\cdot),\, \pi\big) \to 0$ as $n \to \infty$.

• Uniform ergodicity (custom): there exist real numbers $R \ge 0$ and $t$ with $0 \le t < 1$ such that for every $x \in X$ and every $n \ge 1$,

$$d_{TV}\big(P^n(x,\cdot),\, \pi\big) \;\le\; R\, t^n.$$

• Lag-$k$ covariance (custom): for $f,g : X \to \mathbb{R}$ and $k \in \mathbb{N}$,

$$\gamma_k(f,g) \;=\; \int_X \Big( f(x) - \textstyle\int f\, d\pi \Big) \cdot \Big( \textstyle\int g \; dP^k(x,\cdot) \;-\; \int g\, d\pi \Big) \, d\pi(x),$$

a Bochner integral (if any integrand fails to be integrable, the corresponding integral takes the junk value $0$). Write $\gamma_k = \gamma_k(f,f)$.

• Asymptotic variance (custom):

$$\sigma^2(f) \;=\; \gamma_0 \;+\; \sum_{k=0}^{\infty} \gamma_{k+1} \;+\; \sum_{k=0}^{\infty} \gamma_{k+1},$$

i.e. $\gamma_0$ plus twice the sum $\sum_{k \ge 1}\gamma_k$ (the same infinite sum appears as two separate summands, which coincide here since both arguments are $f$). Each infinite sum is a Lean tsum: if the family is not summable it takes the junk value $0$.

• Chain law (custom): for an initial distribution $\lambda$ on $X$, $\mathbb{P}_\lambda$ denotes the measure on the path space $\mathbb{N} \to X$ given by composing $\lambda$ with the trajectory kernel of $P$ (an Ionescu–Tulcea construction from an imported platform definition, BanditAlgorithm.markovChainKernel, sending a starting point to the law of the trajectory $(X_0, X_1, X_2, \dots)$ with $X_0$ having law $\lambda$ and transitions governed by $P$).

• Sample average (custom): for a path $\omega : \mathbb{N} \to X$,

$$\bar f_n(\omega) \;=\; \frac{1}{n} \sum_{i=1}^{n} f(\omega_i),$$

which excludes the initial coordinate $\omega_0$. For $n = 0$ the factor $1/n$ is Lean's junk value $0^{-1} = 0$, so $\bar f_0(\omega) = 0$.

Hypotheses. Given, in addition to the setting above:

• $\pi$ and $P$ satisfy Harris ergodicity as unfolded above ($h_P$);
• $\pi$ and $P$ satisfy uniform ergodicity as unfolded above ($h_{\mathrm{uni}}$);
• $f : X \to \mathbb{R}$ is measurable ($h_f$);
• $f \in L^2(\pi)$, i.e. $f$ is a.e.-strongly measurable with $\int |f|^2 \, d\pi < \infty$ ($h_{L^2}$).

Assertion. The theorem claims the conjunction of three statements:

1. Summability. The family $(\gamma_{k+1})_{k \in \mathbb{N}}$, i.e. the lag covariances $\gamma_1, \gamma_2, \gamma_3, \dots$, is summable in Lean's sense: the net of finite partial sums converges (unconditional convergence in $\mathbb{R}$, equivalent here to absolute convergence). Note this concerns only lags $k \ge 1$; $\gamma_0$ is not part of this family.

2. Nonnegativity. $\;0 \le \sigma^2(f)$, with $\sigma^2(f)$ as unfolded above (a weak inequality, allowing $\sigma^2(f) = 0$).

3. Central limit theorem for every initial distribution. For every probability measure $\lambda$ on $X$: the sequence of functions on path space

$$\omega \;\longmapsto\; \sqrt{n}\,\Big( \bar f_n(\omega) - \textstyle\int f \, d\pi \Big), \qquad n \to \infty,$$

each considered as a random variable under the fixed law $\mathbb{P}_\lambda$, converges in distribution to the real Gaussian law

$$\mathcal{N}\!\big(0,\; \max(\sigma^2(f),\, 0)\big),$$

realized as the identity random variable on $\mathbb{R}$ carrying that Gaussian measure. (Convergence in distribution here is Mathlib's TendstoInDistribution: weak convergence of the pushforward laws, i.e. convergence of integrals of bounded continuous test functions.)

On the $\mathbb{R}_{\ge 0}$ coercion. The variance fed to the Gaussian is not $\sigma^2(f)$ itself but its coercion .toNNReal into the nonnegative reals, which maps a real $v$ to $\max(v, 0)$. Thus if $\sigma^2(f)$ were negative, the limit law asserted in conjunct 3 would silently become $\mathcal{N}(0,0)$, which is the Dirac point mass at $0$ — the clamping to $0$ happens without any hypothesis forcing it, though conjunct 2 of the same conjunction separately asserts $\sigma^2(f) \ge 0$, so within this theorem's claim the clamp is only ever the identity. Likewise, if $\sigma^2(f) = 0$ (permitted by the weak inequality), the asserted limit is the point mass at $0$. A further degenerate case: since the summability claim of conjunct 1 is stated separately, the tsums inside $\sigma^2(f)$ are well-defined regardless, but would equal $0$ (junk) if summability failed — conjunct 1 rules this out as part of the same conjunction.