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.

Durbin–Levinson solves the successive prediction equations

Statement

Let X be weakly stationary with mean μ and ACVF γ, and suppose Γk=(γ(i−j))i,j=1k is positive definite for 1≤k≤m. For each k≤m, let ϕk,νk be the outputs of Durbin–Levinson forecast recursion and put rk=(γ(1),…,γ(k))T. Then ϕk is the unique solution of Γkϕk=rk, and νk=Var⁡(Xt+1−μ−∑j=1kϕk,j(Xt+1−j−μ))=γ(0)−rkTϕk.

Facts & Assumptions

Given: A weakly stationary real process X, its mean μ and ACVF γ, an integer m≥1, and positive-definite matrices Γk for 1≤k≤m.

[F1]

The procedure takes ACVF lags, requires positive-definite leading covariance blocks, and defines κk, ϕk and νk by its stated initialization and updates. Durbin–Levinson forecast recursion

[F2]

When a finite stationary history covariance matrix is nonsingular, the forecast coefficients solve the covariance normal equations and its error variance is γ(0)−rkTϕk. Finite-history forecast equations and error variance

[F3]

The population ACVF is γ(r)=Cov⁡(Xt+r,Xt) for every integer lag. Autocovariance and sample autocovariance

[F4]

Covariance is symmetric and bilinear on finite linear combinations. Variance and covariance identities for random variables

Proof

1.1givenF1F2

For k=1, positive definiteness of Γ1=[γ(0)] gives γ(0)>0. The algorithm sets ϕ1,1=γ(1)/γ(0), so Γ1ϕ1=r1, and [F2] gives error variance γ(0)−γ(1)2/γ(0)=ν1, including the zero-error case.

1.2givenF1

For the induction step fix 2≤k≤m and assume the claim at order k−1. Write r=(γ(1),…,γ(k−1))T; covariance symmetry gives Γk=(γ(0)rTrΓk−1). The induction hypothesis gives ϕk−1=Γk−1−1r and νk−1=γ(0)−rTΓk−1−1r. The positive quadratic form of Γk at (1,−Γk−1−1r)T equals this value, so νk−1>0 and the order-k division is valid.

2.1F1F3F4step 1.2

Set T=∑j=1k−1ϕk−1,jγ(k−j) and κk=(γ(k)−T)/νk−1. For i<k, the new coefficient rule gives (Γkϕk)i=∑j=1k−1γ(i−j)ϕk−1,j−κk∑j=1k−1γ(i−j)ϕk−1,k−j+κkγ(i−k). The first sum is γ(i) by the old system; reindexing the second by ℓ=k−j gives its row k−i, namely γ(k−i). Since γ(i−k)=γ(k−i), these last terms cancel and (Γkϕk)i=γ(i).

3.1F1step 1.2step 2.1algebra

Let S=rTϕk−1=γ(0)−νk−1. Reindexing the last row gives ∑j=1k−1γ(k−j)ϕk−1,j−κk∑j=1k−1γ(k−j)ϕk−1,k−j+κkγ(0)=T+κk(γ(0)−S)=T+κkνk−1=γ(k). Thus Γkϕk=rk, and positive definiteness makes the solution unique.

4.1F1F2step 1.2step 3.1algebra∎

Reindexing the new vector gives rkTϕk=S−κkT+κkγ(k)=S+κk2νk−1 by the definition of κk. Therefore γ(0)−rkTϕk=νk−1(1−κk2)=νk. The forecast theorem [F2] identifies this with the one-step projection-error variance, completing the induction through k=m.

Depends on

Used by

Cited to discharge well-definedness by Durbin–Levinson forecast recursion.

Dependency tree · two levels

17 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