Alphabeta Math
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.

Finite-history forecast equations and error variance

Statement

Let X=(Xt)t∈Z be a weakly stationary real process with mean μ and autocovariance γ, and let n,h≥1. Define Yi:=Xn+1−i, Γij:=γ(i−j), and γh:=(γ(h),γ(h+1),…,γ(h+n−1))T. If Γ is nonsingular, the unique forecast coefficients satisfy a=Γ−1γh, the best linear forecast is X^n+h=μ+∑i=1nai(Yi−μ), and its error variance is Var⁡(Xn+h−X^n+h)=γ(0)−aTγh.

Facts & Assumptions

Given: A weakly stationary real process X on Z, its common mean μ, its autocovariance γ, and integers n,h≥1.

[F1]

The finite-history affine minimization has a unique almost-sure class for every weakly stationary process, including singular history covariance. Existence and uniqueness of the finite-history predictor class

[F2]

The affine L2 projection theorem gives an affine representative whose coefficients satisfy the intercept and covariance normal equations. Normal equations for best affine L2 prediction

[F3]

Weak stationarity means finite second moments, a time-independent mean, and covariance depending only on the lag. Strict and weak stationarity for integer-indexed time series

[F4]

The ACVF convention is γ(k)=Cov⁡(Xt+k,Xt) for integer k. Autocovariance and sample autocovariance

[F5]

Covariance is symmetric and bilinear on finite linear combinations of square-integrable real random variables. Variance and covariance identities for random variables

[F6]

Variance is the expectation of the centered square, so a mean-zero forecast error has variance equal to its mean-square error. Moments, variance, and covariance on a probability space

Proof

1.1givenF1F2F3

Since weak stationarity gives Xn+h,Y1,…,Yn∈L2, [F1] supplies a unique minimizing class and [F2] an affine representative with coefficients satisfying the normal equations. Every variable has mean μ by [F3], so the intercept is a0=μ(1−∑iai) and the representative is μ+∑iai(Yi−μ).

2.1givenF3F4F5step 1.1

For each i,j, the lag difference between Yi and Yj is j−i; covariance symmetry in [F5] gives γ(j−i)=γ(i−j), so Cov⁡(Yi,Yj)=Γij. The lag from Yi=Xn+1−i to Xn+h is h+i−1, so Cov⁡(Xn+h,Yi)=γ(h+i−1). Rewriting step 1.1's equations gives Γa=γh.

3.1givenstep 2.1algebra

Under the statement's nonsingularity hypothesis, Γa=γh has the unique solution a=Γ−1γh.

4.1F2F3F4F5F6step 1.1step 2.1step 3.1algebra∎

Put U=Xn+h−μ and Zi=Yi−μ; the intercept equation makes the error mean zero, and stationarity gives E[UZi]=γ(h+i−1) and E[ZiZj]=Γij. Expanding gives E[(U−aTZ)2]=γ(0)−2aTγh+aTΓa=γ(0)−aTγh because Γa=γh. By [F6] this is the error variance.

Depends on

Used by

Dependency tree · two levels

21 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