20. Truncating memory without losing the prediction bound
On this page · Permalink · Source line 812
Section 8 bounded the omitted tail of the exact linear memory expression using the same resolved history. We now close the separate recursion argument.
Write the exact relation as
For negative indices set \(z_s=0\), solely as a convention for missing prehistory in this initialized formula. A length-\(H\) approximate model, with \(H\geq0\), is
An empty sum is zero. Let \(d_t\) be the exact right-hand side minus this truncated right-hand side evaluated on the true history.
Proposition 19: Uniform prediction bound for a stable finite-memory truncation
Suppose
Let \(E_0\) bound the initialization errors at indices \(-H,\ldots,0\). Then the recursively generated predictions satisfy
If \(\|z_t\|\leq Z\) for \(t\geq0\) and \(\|D\|\leq\rho<1\), a valid choice of defect bound is
The last term can be removed if the exact initialized forcing \(f_t\) is retained in the approximate recurrence.
Read proof · Recorded Lean scope · Visual guide: Memory is an exact elimination · Permalink · Source line 832
Proof
Subtract the two recurrences and bound every retained history error by the largest of the errors at indices \(t-H,\ldots,t\). This gives \(e_{t+1}\leq a\max_{t-H\leq s\leq t}e_s+\Delta\). The ball of radius \(E=\max(E_0,\Delta/(1-a))\) is invariant because \(aE+\Delta\leq E\). Induction proves the bound. The estimate for \(\Delta\) separates coefficient errors, the geometric kernel tail and the initialized forcing, using Proposition 10. \(\square\)
This norm-sum condition is sufficient, not necessary. A stable recurrence with cancellation can fail this test. Failure to find this certificate is not proof of instability.
For the scalar example with \(q_0=0\), take exact retained coefficients and \(z_0=1\). All outputs lie in \([0,1]\): the full nonnegative memory coefficients sum to at most \(7/8\), so induction bounds every new output by the previous maximum. Thus \(Z=1\) is valid. With
one obtains
The right-hand side is a theorem for every time in this initialized example. The figure compares it with a separately computed finite-horizon error. The computed maximum is not substituted for the uniform bound.
