Pipeline-generated

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.

✓ 2 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 2 also cleared it.

Stationary means and sample autocovariance

1 · Prerequisites

2 · Summary

For an integer-indexed real process, strict stationarity concerns all finite-dimensional laws, while weak stationarity requires finite second moments, a constant mean and lag-dependent covariance. Under weak stationarity, the sample-mean variance is a triangularly weighted covariance sum; absolute covariance summability gives an $O (n^{- 1})$ variance bound and $L^{2}$ consistency, without a mixing or central limit conclusion. The zero-extended biased sample ACVF has nonnegative Toeplitz quadratic forms; the pair-count-normalized rescaling need not. Ergodicity gives a separate almost-sure and $L^{1}$ mean limit only with strict stationarity, integrability and the Axiom of Choice required by the Birkhoff supplier. These are consequences of the specified probability law; neither a model contract nor these theorems establish that a scientific model adequately describes its application.

Model contract for this pair

For horizon $n \geq 1$ , the observed record is the finite coordinate tuple $D_{n} = (X_{1}, \dots, X_{n})$ in $R^{n}$ with the finite product Borel sigma-algebra; its law is the pushforward of the process law under the coordinate map (Stochastic processes and their finite-dimensional distributions, Law or distribution of a random element, The product sigma-algebra and its finite iterates, The Borel sigma-algebra of a topological space). One record is one real coordinate at an integer time index. The index set and origin for the displayed sample are fixed; a physical time scale, sampling frame and scientific unit are application fields, not supplied by this abstract pair. The coordinates are random and $D_{n}$ is observed; no predictors, latent quantities, treatment assignment or missingness mechanism is specified. The target is the common law mean $μ$ , and the analysis uses the joint process law without conditioning on a design. No support restriction beyond that law is imposed. This model-record convention is the observation/index/quantity-status/law context of Scientific statistical model contracts.

Stationarity and finite moments are empirically assessable assumptions: data can challenge their implications but cannot prove them. Absolute covariance summability and ergodicity are global law hypotheses that a finite record does not verify. Whether the specified law describes a scientific population requires application-level evidence and is not a consequence of the mathematics here.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Strict and weak stationarity for integer-indexed time series

Definition

Let $X = (X_{t})_{t \in Z}$ be a real-valued stochastic process on one probability space, so each $X_{t}$ is a real random variable and each finite tuple has its pushforward law (Stochastic processes and their finite-dimensional distributions, Random elements and real random variables, Law or distribution of a random element). We call $X$ a time series here because its index set is $Z$ .

The process is strictly stationary when for every integer $r \geq 1$ , every $t_{1}, \dots, t_{r} \in Z$ , and every shift $m \in Z$ , $L (X_{t_{1} + m}, \dots, X_{t_{r} + m}) = L (X_{t_{1}}, \dots, X_{t_{r}}) .$ This condition concerns the full finite-dimensional laws and imposes no moment condition by itself.

The process is weakly stationary when $E [∣ X_{t} ∣^{2}] < \infty$ for every $t \in Z$ , its mean $μ : = E [X_{t}]$ is independent of $t$ , and for every $h \in Z$ the covariance $γ (h) : = Cov (X_{t + h}, X_{t})$ is independent of $t$ . Expectation, variance, and covariance have the meanings in Expectation of a nonnegative or integrable random variable and Moments, variance, and covariance on a probability space. Strict stationarity alone therefore does not supply the moment hypotheses needed for covariance or sample-mean claims.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Autocovariance and sample autocovariance

Definition

For a weakly stationary real process $X = (X_{t})_{t \in Z}$ , its autocovariance function (ACVF) is $γ (h) : = Cov (X_{t + h}, X_{t}), h \in Z,$ which is independent of $t$ by Strict and weak stationarity for integer-indexed time series.

For a finite data vector $x_{1}, \dots, x_{n} \in R$ , where $n \geq 1$ , let ${\overset{ˉ}{x}}_{n} : = \frac{1}{n} \sum_{t = 1}^{n} x_{t} .$ Its biased sample ACVF is the zero-extended sequence on $Z$ given by ${\hat{γ}}_{n} (h) : = \frac{1}{n} \sum_{t = 1}^{n - ∣ h ∣} (x_{t + ∣ h ∣} - {\overset{ˉ}{x}}_{n}) (x_{t} - {\overset{ˉ}{x}}_{n}), ∣ h ∣ < n,$ and ${\hat{γ}}_{n} (h) : = 0$ for $∣ h ∣ \geq n$ . The absolute lag makes ${\hat{γ}}_{n} (- h) = {\hat{γ}}_{n} (h)$ .

For comparison, define the pair-count-normalized rescaling ${\tilde{γ}}_{n} (h) : = \frac{1}{n - ∣ h ∣} \sum_{t = 1}^{n - ∣ h ∣} (x_{t + ∣ h ∣} - {\overset{ˉ}{x}}_{n}) (x_{t} - {\overset{ˉ}{x}}_{n}), ∣ h ∣ < n,$ and set it to zero for $∣ h ∣ \geq n$ . Its denominator is positive on the stated domain. The names specify the denominator convention; they assert no unbiasedness formula.

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Ergodic time-series sample means converge almost surely and in L1

Statement

Assume the Axiom of Choice. Let $X = (X_{t})_{t \in Z}$ be a real strictly stationary process with $E ∣ X_{0} ∣ < \infty$ . Put $Y_{k} : = X_{k + 1}$ for $k \geq 0$ . If the canonical shift of the one-sided path law of $Y$ is ergodic, then ${\overset{ˉ}{X}}_{n} : = \frac{1}{n} \sum_{t = 1}^{n} X_{t} ⟶ E [X_{0}]$ almost surely and in $L^{1}$ . Here strict stationarity on $Z$ means invariance of every finite-dimensional law under every common integer shift; the one-sided ergodicity convention is that of Stationary process and canonical path shift and Ergodicity relative to an invariant measure.

Facts & Assumptions

Given: AC, a real process $X = (X_{t})_{t \in Z}$ whose finite-dimensional laws are invariant under all common integer shifts, $E ∣ X_{0} ∣ < \infty$ , and ergodicity of the canonical shift on the path law of $Y_{k} = X_{k + 1}$ , $k \geq 0$ .

[A1]

The Axiom of Choice (AC) asserts that every family of nonempty sets has a choice function (The Axiom of Choice).

[F1]

Strict and weak stationarity for integer-indexed time series: strict stationarity on $Z$ is invariance of all finite-dimensional laws under common integer shifts.

[F2]

Stationary process and canonical path shift: a one-sided strictly stationary process has a canonical path law and left shift.

[F3]

Ergodicity relative to an invariant measure: ergodicity means every strictly invariant event is null or conull for the invariant path law.

[F4]

Birkhoff limit for a stationary integrable process: assuming AC, a real strictly stationary integrable process has almost-sure and $L^{1}$ convergence of its averages to the conditional-expectation limit; if its canonical shift is ergodic, that limit is its mean.

Proof

Proof technique: restrict the integer-indexed process to positive times and apply the established one-sided Birkhoff result.

1.1F1F2given

Define $Y_{k} = X_{k + 1}$ for $k \geq 0$ . For any finite indices $0 \leq k_{1} < \dots < k_{r}$ and shift $m \geq 0$ , [F1] applied to the times $k_{1} + 1, \dots, k_{r} + 1$ gives $L (Y_{k_{1} + m}, \dots, Y_{k_{r} + m}) = L (Y_{k_{1}}, \dots, Y_{k_{r}})$ . Thus $Y$ is strictly stationary in the one-sided convention of [F2]. Taking $r = 1$ shows $Y_{0} = X_{1}$ has the same law as $X_{0}$ , so it is integrable; the canonical shift is ergodic by the given assumption.

2.1A1F3F4step 1.1given∎

By [F3] the assumed ergodicity is exactly ergodicity of the canonical path shift required by [F4]. AC [A1], integrability from step 1.1, strict stationarity from step 1.1, and that ergodic shift satisfy the hypotheses of [F4]. Hence $n^{- 1} \sum_{k = 0}^{n - 1} Y_{k}$ converges almost surely and in $L^{1}$ to $E [Y_{0}] = E [X_{0}]$ . Since this average is exactly $n^{- 1} \sum_{t = 1}^{n} X_{t} = {\overset{ˉ}{X}}_{n}$ , the asserted convergence follows. The choice assumption is inherited through [F4]'s conditional-expectation identification; this proof adds no other choice use.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

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.

5 · Examples, counterexamples and false statements

None yet.

Stationary means and sample autocovariance

1 · Prerequisites

2 · Summary

Model contract for this pair

3 · Logical flowchart

4 · Definitions, theorems and proofs

Strict and weak stationarity for integer-indexed time series

Definition

Autocovariance and sample autocovariance

Definition

Ergodic time-series sample means converge almost surely and in L1

Statement

Facts & Assumptions

Proof

Sample-mean variance and positive semidefinite sample ACVF

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources