TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Sample-mean variance and positive semidefinite sample ACVF

Statement

Let $X = (X_{t})_{t \in Z}$ be weakly stationary, with mean $μ$ and autocovariance $γ$ , and define ${\overset{ˉ}{X}}_{n} : = n^{- 1} \sum_{t = 1}^{n} X_{t}$ for $n \geq 1$ . Then $Var ({\overset{ˉ}{X}}_{n}) = \frac{1}{n^{2}} \sum_{∣ h ∣ < n} (n - ∣ h ∣) γ (h) .$ If $\sum_{h \in Z} ∣ γ (h) ∣ < \infty$ , then $0 \leq Var ({\overset{ˉ}{X}}_{n}) \leq \frac{1}{n} \sum_{h \in Z} ∣ γ (h) ∣,$ so $E [({\overset{ˉ}{X}}_{n} - μ)^{2}] \to 0$ : the sample mean is consistent in $L^{2}$ . No mixing property or central limit theorem is asserted here. For every finite real data vector, the zero-extended biased sample ACVF ${\hat{γ}}_{n}$ of Autocovariance and sample autocovariance has nonnegative Toeplitz quadratic forms.

Facts & Assumptions

Given: A weakly stationary real process $X = (X_{t})_{t \in Z}$ with mean $μ$ and autocovariance $γ$ , an integer $n \geq 1$ , and (for the consistency conclusion) $\sum_{h \in Z} ∣ γ (h) ∣ < \infty$ . The sample ACVF conclusion applies to every finite real data vector of length $n$ .

[F1]

Strict and weak stationarity for integer-indexed time series: each $X_{t}$ has finite second moment, $E [X_{t}] = μ$ is constant, and $γ (h) = Cov (X_{t + h}, X_{t})$ is independent of $t$ .

[F2]

Moments, variance, and covariance on a probability space defines variance and covariance from centered squares and products; Variance and covariance identities for random variables gives covariance bilinearity on finite linear combinations.

[F3]

Linearity, monotonicity, and the modulus bound for expectation: expectation is linear on integrable random variables.

[F4]

Autocovariance and sample autocovariance: after centering a data vector by its sample mean, ${\hat{γ}}_{n} (h)$ is the $1 / n$ lagged product sum, with zero extension for $∣ h ∣ \geq n$ .

Proof

Proof technique: count pairs by their lag, bound the resulting covariance sum, and write the sample Toeplitz form as a sum of squares.

1.1F1F2F3givenalgebra

Each $X_{t}$ is integrable because $2 ∣ X_{t} ∣ \leq 1 + X_{t}^{2}$ and the probability space has total mass one. Repeated application of [F3] gives $E [{\overset{ˉ}{X}}_{n}] = μ$ . By [F2] and its cited covariance-bilinearity supplier, $Var ({\overset{ˉ}{X}}_{n}) = n^{- 2} \sum_{s = 1}^{n} \sum_{t = 1}^{n} Cov (X_{s}, X_{t})$ .

1.2F4givenalgebra

Fix a data vector $x_{1}, \dots, x_{n}$ , let $y_{t} = x_{t} - {\overset{ˉ}{x}}_{n}$ for $1 \leq t \leq n$ , and set $y_{t} = 0$ otherwise. By [F4], for every $h \in Z$ , ${\hat{γ}}_{n} (h) = n^{- 1} \sum_{t \in Z} y_{t} y_{t + h}$ . The sum is finite because $y$ has finite support. Replacing $t$ by $t - h$ and commuting the real factors shows ${\hat{γ}}_{n} (- h) = {\hat{γ}}_{n} (h)$ .

2.1F1step 1.1algebra

For $s, t \in {1, \dots, n}$ , [F1] gives $Cov (X_{s}, X_{t}) = γ (s - t)$ . For each integer $h$ with $∣ h ∣ < n$ , exactly $n - ∣ h ∣$ ordered pairs $(s, t)$ satisfy $s - t = h$ , and no ordered pair has $∣ s - t ∣ \geq n$ . Grouping the finite sum in step 1.1 by $h = s - t$ proves the variance identity.

3.1step 2.1givenalgebra

Under absolute covariance summability, every weight $n - ∣ h ∣$ in the identity is between $0$ and $n$ , so $0 \leq Var ({\overset{ˉ}{X}}_{n}) \leq n^{- 2} \sum_{∣ h ∣ < n} (n - ∣ h ∣) ∣ γ (h) ∣ \leq n^{- 1} \sum_{h \in Z} ∣ γ (h) ∣$ .

4.1step 1.1step 3.1algebra

Step 1.1 gives $E [{\overset{ˉ}{X}}_{n}] = μ$ . Therefore $E [({\overset{ˉ}{X}}_{n} - μ)^{2}] = Var ({\overset{ˉ}{X}}_{n})$ , and the bound in step 3.1 tends to zero as $n \to \infty$ . This is precisely $L^{2}$ consistency for the mean.

5.1step 1.2givenalgebra∎

Let $(a_{j})_{j \in J}$ be any finitely supported real coefficient family indexed by integers. Expanding the finite sums and using the evenness from step 1.2 gives $\sum_{j, k \in J} a_{j} a_{k} {\hat{γ}}_{n} (j - k) = n^{- 1} \sum_{u \in Z} (\sum_{j \in J} a_{j} y_{u + j})^{2} \geq 0$ . Only finitely many terms on the right are nonzero, and every summand is a square. Thus every finite Toeplitz quadratic form of ${\hat{γ}}_{n}$ is nonnegative.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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

Nicolai Meinshausen, Time Series Analysis: Notes for the course HS 2022, complete 57-page lecture notes (standard reference, not scraped)
STAT 720 Time Series Analysis, South Carolina course notes by Wang, focused Sections 2.1–2.2 and Lemma 2.3 (standard reference, not scraped)