Strongly mixing stationary sequences: CLT $\iff$$\{S_n^2/\sigma_n^2\}$ uniformly integrable (Jones Thm 3)

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 $\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]$. Two further hypotheses: $\alpha(n) \to 0$ as $n \to \infty$, and, writing $S_n(\omega) := \sum_{i=0}^{n-1} Y_i(\omega)$ and $s_n^2 := \int S_n^2 \, dP$ (a Bochner integral, $0$ by convention if $S_n^2$ is not integrable), the sequence $s_n^2$ tends to $+\infty$ (eventually exceeds every real bound). The conclusion is an equivalence (if and only if) between the following two statements. (A) The random variables $\omega \mapsto S_n(\omega) / \sqrt{s_n^2}$ converge in distribution along $n \to \infty$ to the standard Gaussian: gaussianReal 0 1 is the normal law of mean $0$ and variance $1$ (it would be the point mass at $0$ only if the variance were $0$, which $1$ is not), and TendstoInDistribution — with the limit presented as the identity map on $\mathbb{R}$ carrying that Gaussian measure, whose law is the Gaussian itself — asserts weak convergence of the laws: $\int f(S_n/\sqrt{s_n^2})\, dP \to \int f\, d\mathcal{N}(0,1)$ for every bounded continuous $f : \mathbb{R} \to \mathbb{R}$. (B) The family $g_n(\omega) := S_n(\omega)^2 / s_n^2$ (indexed by $n \in \mathbb{N}$) is uniformly integrable at exponent $1$ over $P$ in Mathlib's sense (UniformIntegrable), which is the conjunction of three conditions: (i) each $g_n$ is almost-everywhere strongly measurable; (ii) uniform absolute continuity: for every $\varepsilon > 0$ there exists $\delta > 0$ such that for every $n$ and every measurable set $S \subseteq \Omega$ with $P(S) \le \delta$ one has $\int_S |g_n| \, dP \le \varepsilon$ (the $L^1$ norm of $g_n$ cut off to $S$); and (iii) uniform $L^1$ boundedness: there is a finite constant $C \ge 0$ with $\|g_n\|_{L^1(P)} \le C$ for all $n$. Degenerate cases: real division by zero yields $0$ in Lean, so whenever $s_n^2 = 0$ — in particular at $n = 0$, where $S_0 \equiv 0$, hence $s_0^2 = 0$ and $\sqrt{s_0^2} = 0$ — both the normalized variable $S_n/\sqrt{s_n^2}$ and the ratio $g_n$ are identically $0$; also $\sqrt{\cdot}$ is Lean's real square root, which sends negative arguments to $0$ (here $s_n^2 \ge 0$ in all cases).