Ibragimov–Linnik CLT, bounded case: $|Y| < B$ a.s., $\sum \alpha(n) < \infty$ (Jones Thm 5(i))

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$). Further hypotheses: there is a fixed real number $B$ (no sign condition is imposed on $B$) such that for each $n$, $|Y_n(\omega)| < B$ for $P$-almost every $\omega$ — a strict inequality, with the almost-everywhere quantifier taken separately for each $n$; since $|Y_n(\omega)| \ge 0$ and $P$ is a probability measure, this hypothesis is unsatisfiable when $B \le 0$, making the theorem vacuously true for such $B$. 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]$. The mixing hypothesis is that the family $n \mapsto \alpha(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$.