Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass
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.

Zero covariance long-run variance gives a degenerate CLT under absolute summability

Statement

Let (Yk)k≥0 be a centered, strictly stationary, square-integrable real process (The space Lp(μ) as the quotient by null functions), and put γk=Cov⁡(Y0,Yk). If ∑k≥1∣γk∣<∞ and γ0+2∑k=1∞γk=0, then n−1/2∑k=1nYk→0 in L2 and hence in distribution to N(0,0).

Facts & Assumptions

Given: A centered strictly stationary real process with finite second moment and the stated covariance hypotheses.

[F1]

Variance is the centered second moment and covariance is the centered product expectation. (Moments, variance, and covariance on a probability space)

[F2]

Strict stationarity makes every covariance depend only on the lag. (Strong, uniform, and maximal-correlation mixing coefficients)

[F3]

Convergence in L2 implies convergence in probability. (Lp convergence implies convergence in probability)

[F4]

Convergence in probability to a constant implies convergence in distribution to its point-mass law. (Convergence in probability implies convergence in distribution)

[F5]

Dominated convergence applies to a series indexed by counting measure when its terms have a summable majorant. (Dominated convergence)

Proof

1.1F1F2F5given

Expanding the finite square of Sn:=∑k=1nYk and using centering and [F2] gives 1nVar⁡(Sn)=γ0+2∑k=1n−1(1−kn)γk. For each fixed k, the weight tends to 1 and its absolute value is at most 1. The summable sequence ∣γk∣ dominates the summands, so [F5] gives n−1Var⁡(Sn)→γ0+2∑k≥1γk=0.

2.1F1F3F4step 1.1∎

Since E[Sn]=0, step 1.1 gives E[(Sn/n)2]=n−1Var⁡(Sn)→0. This is convergence to zero in L2; [F3] gives convergence in probability, and [F4] gives convergence in distribution to the point mass at zero, namely N(0,0).

Depends on

Used by

Dependency tree · two levels

25 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