TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A uniform-mixing CLT for square-integrable stationary sequences

Statement

Assume AC. Let $(Y_{k})_{k \geq 0}$ be a centered strictly stationary real sequence with $E [Y_{0}^{2}] < \infty$ . If $\sum_{n = 1}^{\infty} \sqrt{ϕ_{Y} (n)} < \infty,$ then the covariance series $σ_{Y}^{2} : = E [Y_{0}^{2}] + 2 \sum_{k = 1}^{\infty} Cov (Y_{0}, Y_{k})$ converges absolutely and is nonnegative. If $σ_{Y}^{2} > 0$ , then for $S_{n} = \sum_{k = 1}^{n} Y_{k}$ , $n^{- 1 / 2} S_{n} \Rightarrow N (0, σ_{Y}^{2}) .$ If $σ_{Y}^{2} = 0$ , Zero covariance long-run variance gives a degenerate CLT under absolute summability gives the degenerate normal limit.

Facts & Assumptions

Given: AC, the centered strictly stationary real sequence $Y$ , finite second moment, and $\sum_{n \geq 1} \sqrt{ϕ_{Y} (n)} < \infty$ .

[A1]

AC is inherited through the rho-mixing CLT. (The Axiom of Choice)

[F1]

The coefficient $ϕ_{Y} (n)$ bounds $∣ P (B ∣ A) - P (B) ∣$ for a positive-probability past event $A$ and an event $B$ in the separated future; $ρ_{Y} (n)$ is the supremum of their square-integrable variable correlations. (Strong, uniform, and maximal-correlation mixing coefficients)

[F2]

Real square-integrable random variables satisfy Cauchy–Schwarz. (Cauchy-Schwarz for random variables)

[F3]

Simple functions are dense in real $L^{2}$ on a probability space. (Simple functions with finite-measure support are dense in $L^{p} (μ)$ for $1 \leq p < \infty$ )

[F4]

For a centered stationary real sequence of finite second moment, $\sum_{n \geq 1} ρ_{Y} (n) < \infty$ gives absolute convergence and nonnegativity of the covariance variance, and the normal CLT with that variance, including zero. (A rho-mixing CLT for square-integrable stationary sequences)

[F5]

Variance and covariance are centered second and product moments. (Moments, variance, and covariance on a probability space)

Proof

1.1F1givenconstructalgebra

Fix a gap $n \geq 1$ and a split $k \geq 0$ , put $A = σ (Y_{0}, \dots, Y_{k})$ and $B = σ (Y_{k + n}, Y_{k + n + 1}, \dots)$ , and put $ϕ = ϕ_{Y} (n)$ . Take finite partitions $(A_{i})$ in $A$ and $(B_{j})$ in $B$ . Write $a_{i} = P (A_{i})$ , $b_{j} = P (B_{j})$ , $p_{i j} = P (A_{i} \cap B_{j})$ , and $d_{i j} = p_{i j} - a_{i} b_{j}$ . For each fixed $i$ the $d_{i j}$ sum to zero. If $a_{i} > 0$ , their positive sum is $P (A_{i} \cap B) - a_{i} P (B) \leq ϕ a_{i}$ for $B = ⋃_{j : d_{i j} > 0} B_{j}$ , by [F1]. Hence $\sum_{j} ∣ d_{i j} ∣ \leq 2 ϕ a_{i}$ ; when $a_{i} = 0$ , every $d_{i j} = 0$ and the same bound holds. For each $j$ , $∣ p_{i j} - a_{i} b_{j} ∣ \leq p_{i j} + a_{i} b_{j}$ gives $\sum_{i} ∣ d_{i j} ∣ \leq 2 b_{j}$ .

2.1F2F5step 1.1algebra

For simple $U = \sum_{i} u_{i} 1_{A_{i}}$ and $V = \sum_{j} v_{j} 1_{B_{j}}$ , [F5] and finite Cauchy–Schwarz with weights $∣ d_{i j} ∣$ give $∣ Cov (U, V) ∣ = ∣ \sum_{i, j} d_{i j} u_{i} v_{j} ∣ \leq (\sum_{i, j} ∣ d_{i j} ∣ u_{i}^{2})^{1 / 2} (\sum_{i, j} ∣ d_{i j} ∣ v_{j}^{2})^{1 / 2} \leq 2 \sqrt{ϕ} ∥ U ∥_{2} ∥ V ∥_{2}$ , using step 1.1's row and column bounds. The finite Cauchy–Schwarz inequality here is also the probability-space inequality [F2] on a finite set, after normalizing the total weight; if all weights vanish the conclusion is immediate.

3.1F1F2F3F5step 2.1

For arbitrary real square-integrable $A$ -measurable $U$ and $B$ -measurable $V$ , choose simple approximants in their respective $L^{2}$ spaces using [F3]. Their means, norms and product expectations converge by [F2]; therefore step 2.1's inequality passes to the limit. Apply it to $U - E U$ and $V - E V$ to get $∣ Cov (U, V) ∣ \leq 2 \sqrt{ϕ} \sqrt{Var (U) Var (V)}$ . Taking the supremum over positive-variance variables and then splits in [F1] proves $ρ_{Y} (n) \leq 2 \sqrt{ϕ_{Y} (n)}$ . No reversal of the conditioning direction of $ϕ$ has been used.

4.1A1F4step 3.1given∎

Summation of step 3.1 gives $\sum_{n \geq 1} ρ_{Y} (n) \leq 2 \sum_{n \geq 1} \sqrt{ϕ_{Y} (n)} < \infty$ . The given stationarity, centering, and second-moment assumptions are exactly those of [F4], so that theorem proves absolute convergence and nonnegativity of the displayed covariance series and $S_{n} / \sqrt{n} \Rightarrow N (0, σ_{Y}^{2})$ for positive or zero $σ_{Y}^{2}$ . Thus every claimed conclusion holds.

Source notes

The phi-to-rho bound is proved directly by finite partitions and $L^{2}$ approximation. The normal limit is supplied by the locally proved rho-mixing CLT, rather than an external uniform-mixing limit theorem.

Depends on

Used by

Sufficient MCMC CLT regimes Theorem

Dependency tree · two levels

20 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Galin L. Jones, On the Markov Chain Central Limit Theorem, Theorem 8 (standard reference, not scraped)
Mikhail Gordin and Magda Peligrad, On the functional central limit theorem via martingale approximation, §§1–2 and §3.3; finite-partition phi-to-rho bound proved locally (standard reference, not scraped)