$\varphi$-mixing CLT: $E Y^2 < \infty$, $\sum \sqrt{\varphi(n)} < \infty$ (Jones Thm 8)

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 $\varphi(n) := \sup\left\{\, \left|\dfrac{P(A \cap B)}{P(A)} - P(B)\right| \;:\; k \in \mathbb{N},\ A \in \mathcal{F}_{\le k} \text{ with } P(A) \neq 0,\ B \in \mathcal{F}_{\ge k+n} \,\right\}$, where $\mathcal{F}_{\le k}$ is the σ-algebra on $\Omega$ generated by the $Y_i$ with $i \le k$ (supremum of the pullback σ-algebras) and $\mathcal{F}_{\ge k+n}$ is generated by the $Y_i$ with $i \ge k+n$; the constraint $P(A) \neq 0$ is on the measure value itself, and the quotient and difference are taken between the real conversions of the measure values ($\infty \mapsto 0$, irrelevant here), so under the constraint no division by zero occurs. The split point $k$ is quantified inside the supremum; the index gap between the blocks is $n$. The supremum is the real $\sup$ (junk value $0$ for an empty or unbounded set); the set contains $0$ (take $A = \Omega$, which has $P(A) = 1 \neq 0$, and $B = \emptyset$) and is bounded above by $1$, so $\varphi(n)$ is a genuine supremum in $[0,1]$. The mixing hypothesis is that the family $n \mapsto \sqrt{\varphi(n)}$ is summable in $\mathbb{R}$ (unconditional/absolute summability); the square root is Lean's real square root, which maps negative arguments to $0$, though $\varphi(n) \ge 0$ here as noted. 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$.