Doukhan–Massart–Rio CLT: $\alpha(n) = O(a^n)$, $E[Y^2\log^+|Y|] < \infty$ (Jones Thm 6)

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$). For $n \in \mathbb{N}$, the α-mixing coefficient used here is $\alpha(n) := \sup\{\, |P(A \cap B) - P(A)\,P(B)| \;:\; k \in \mathbb{N},\ A \in \mathcal{F}_{\le k},\ B \in \mathcal{F}_{\ge k+n} \,\}$, where $\mathcal{F}_{\le k}$ is the σ-algebra on $\Omega$ generated by the random variables $Y_i$ with $i \le k$ (the supremum of the pullback σ-algebras $\sigma(Y_i)$ over $i \le k$), $\mathcal{F}_{\ge k+n}$ is the σ-algebra generated by the $Y_i$ with $i \ge k+n$, and measure values are converted from extended nonnegative reals to reals ($\infty \mapsto 0$, irrelevant for a probability measure). The supremum ranges over the split point $k$ as well as over the event pair, and the index gap between the past block $\{0,\dots,k\}$ and the future block $\{k+n, k+n+1, \dots\}$ is exactly $n$ (so $\alpha(0)$ allows overlapping blocks at index $k$). It is the real-number $\sup$, which by Lean convention is $0$ for an empty or unbounded set; here the defining set contains $0$ (take $A = B = \emptyset$) and is bounded above by $1$, so $\alpha(n)$ is a genuine supremum lying in $[0,1]$. Further hypotheses: real numbers $c$ and $a$ with $0 \le a$ and $a < 1$ — note that no sign or size condition is imposed on $c$ — such that $\alpha(n) \le c \cdot a^{n}$ for every $n \in \mathbb{N}$, with $a^{n}$ the ordinary $n$-fold product ($a^{0} = 1$, so the $n = 0$ instance reads $\alpha(0) \le c$). Since each $\alpha(n) \ge 0$, this decay hypothesis is unsatisfiable when $c < 0$ (the theorem is then vacuous), and in the edge case $a = 0$ it forces $\alpha(n) = 0$ for every $n \ge 1$ (as $0^{n} = 0$ there). The moment hypothesis: the function $\omega \mapsto Y_0(\omega)^{2} \cdot \log^{+} |Y_0(\omega)|$ is integrable with respect to $P$, where $\log^{+} x = \max(\log x, 0)$ is Lean's Real.posLog — the positive part of the logarithm, equal to $0$ on $[0,1]$ (Lean's $\log$ is itself $0$ on nonpositive arguments, which does not matter here since the argument $|Y_0(\omega)|$ is nonnegative). 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$.