$\rho$-mixing CLT: $E Y^2 < \infty$, $\sum \rho(n) < \infty$ (Jones Thm 7)

Let $\Omega$ be a type carrying a σ-algebra, $P$ a measure on $\Omega$ assumed to be a probability measure ($P(\Omega)=1$), and $Y_0, Y_1, Y_2, \dots : \Omega \to \mathbb{R}$ a sequence of functions. Standing hypotheses: each $Y_n$ is measurable; the sequence is strictly stationary, meaning that for every $k \in \mathbb{N}$ the pushforward of $P$ under $\omega \mapsto (Y_{n+k}(\omega))_{n \in \mathbb{N}}$ equals the pushforward of $P$ under $\omega \mapsto (Y_n(\omega))_{n \in \mathbb{N}}$, as measures on the sequence space $\mathbb{R}^{\mathbb{N}}$ with the product σ-algebra (the whole shifted sequence has the same joint law as the original; Lean's pushforward returns the zero measure for a non-a.e.-measurable map, but measurability of each $Y_n$ makes these sequence maps measurable); and $\int Y_0 \, dP = 0$, where $\int$ is Lean's Bochner integral, equal to $0$ by convention when the integrand is not integrable (so this centering hypothesis is automatically satisfied by a non-integrable $Y_0$). In addition $Y_0$ belongs to $L^2(P)$ (Mathlib's MemLp at exponent $2$): it is almost-everywhere strongly measurable and $\int |Y_0|^2 \, dP < \infty$. For $n \in \mathbb{N}$, the ρ-mixing coefficient used here is $\rho(n) := \sup\left\{\, \dfrac{|\mathrm{Cov}_P(U,V)|}{\sqrt{\mathrm{Var}_P(U)}\,\sqrt{\mathrm{Var}_P(V)}} \,\right\}$, the supremum ranging over all $k \in \mathbb{N}$ and all pairs of functions $U, V : \Omega \to \mathbb{R}$ such that $U$ is measurable with respect to $\mathcal{F}_{\le k}$ (the σ-algebra generated by the $Y_i$ with $i \le k$, i.e. the supremum of the pullback σ-algebras), $V$ is measurable with respect to $\mathcal{F}_{\ge k+n}$ (generated by the $Y_i$ with $i \ge k+n$), and both $U$ and $V$ lie in $L^2(P)$; $\mathrm{Cov}$ and $\mathrm{Var}$ are Mathlib's covariance and variance under $P$. Division by zero yields $0$ in Lean, so pairs in which either variance vanishes are not excluded — they contribute the value $0$. The supremum is the real $\sup$ (junk value $0$ on an empty or unbounded set); the defining set contains $0$ (e.g. $U = V = 0$) and, by Cauchy–Schwarz together with the division-by-zero convention, is bounded above by $1$, so $\rho(n)$ is a genuine supremum in $[0,1]$. As with the other coefficients, the split point $k$ is also quantified inside the supremum and the index gap between the two blocks is $n$. The mixing hypothesis is that the family $n \mapsto \rho(n)$ is summable in $\mathbb{R}$ (its finite partial sums converge along the net of finite subsets — unconditional, equivalently absolute, summability). The conclusion is the conjunction of two statements. (1) The real-valued family $k \mapsto \int Y_0\, Y_{k+1} \, dP$ (indexed by $k \in \mathbb{N}$, so it comprises the lag-$1, 2, 3, \dots$ covariance integrals but not the lag-$0$ one; each integral is $0$ by convention if $Y_0 Y_{k+1}$ fails to be integrable) is summable in $\mathbb{R}$, i.e. its finite partial sums converge to some real limit along the net of finite subsets — on the reals this is unconditional summability, equivalent to absolute convergence. (2) A guarded implication: set $\sigma^2 := \int Y_0^2 \, dP + 2 \sum_{k=0}^{\infty} \int Y_0\, Y_{k+1}\, dP$, where the infinite sum is Lean's tsum, equal to $0$ by convention if the family is not summable (a degeneracy ruled out whenever conjunct (1) holds). If $0 < \sigma^2$, then the random variables $X_n(\omega) := (\sqrt{n})^{-1} \sum_{i=0}^{n-1} Y_i(\omega)$ converge in distribution along $n \to \infty$ to the Gaussian law with mean $0$ and variance $\max(\sigma^2, 0)$: the variance parameter is $\sigma^2$ truncated at $0$ (Real.toNNReal), which under the guard $0 < \sigma^2$ is just $\sigma^2$; gaussianReal 0 v is the normal law $\mathcal{N}(0, v)$ on $\mathbb{R}$, degenerating to the point mass at $0$ when $v = 0$ (excluded by the guard). Convergence in distribution (TendstoInDistribution, with the limit presented as the identity map on $\mathbb{R}$ carrying the Gaussian measure, whose law is that Gaussian itself) means the laws $P \circ X_n^{-1}$ converge weakly to $\mathcal{N}(0, \sigma^2)$: $\int f(X_n)\, dP \to \int f \, d\mathcal{N}(0,\sigma^2)$ for every bounded continuous $f : \mathbb{R} \to \mathbb{R}$. Degenerate index: $(\sqrt{0})^{-1} = 0$ in Lean, so $X_0 \equiv 0$.