Theorem 4: discrete-time approximation by a nonlinear moving average
ProvedBoydChua.nlma_approximationTheorem 4 of the source (NLMA Approximation Theorem). Let a tolerance be given, let K be the ball of radius M in bounded scalar signals, and let N be any time-invariant operator with fading memory on K. Then there is a window length m and a polynomial p in m variables such that the nonlinear moving average reading p from the last m samples approximates N to within that tolerance — simultaneously for every signal of the ball and at every instant.
Two points deserve emphasis. The approximation is uniform over all of K at once and over the whole infinite time horizon at once, not on a finite window and not on a compact subset; and K is not compact for the supremum norm, so the result is not a disguised Stone-Weierstrass on a compact input set. Fading memory is precisely what makes K behave as though it were compact.
The source notes that this statement implies its Theorem 3, approximation by a finite Volterra series, since a moving average with polynomial nonlinearity is itself a finite Volterra series operator.
import Mathlib import Definitions.Def_BoydChua open Filter Topology MeasureTheory ReservoirESN BoydChua
namespace BoydChua
theorem nlma_approximation (M : ℝ) (hM : 0 < M) (w : ℕ → ℝ) (hw : IsWeighting w)
(N : (ℕ → ℝ) → (ℕ → ℝ)) (hTI : IsTimeInvariant N) (hFM : OperatorFMP N M w)
(ε : ℝ) (hε : 0 < ε) :
∃ (m : ℕ) (p : MvPolynomial (Fin m) ℝ), ∀ u : ℕ → ℝ, UnifBdd M u →
∀ k, |N u k - NLMA p u k| ≤ ε := by sorry
end BoydChuaRead-back
What the Lean code literally says, in plain math · claude-opus-5
Fix a positive radius M, a weighting w, an operator N on real sequences that is time-invariant and has the operator fading-memory property at radius M for w, and a positive tolerance e. Then there exist an integer m and a polynomial p in m variables - chosen once, uniformly in the input and in the time - such that for every input bounded by M, and for every index k, the output N u k differs from p(u k, ..., u(k+m-1)) by at most e.
So a time-invariant fading-memory operator on the M-ball is uniformly approximated, over all inputs and all times simultaneously, by a single finite-order polynomial moving average.
Two points were checked independently. The fading-memory hypothesis is imposed at index zero only, yet it suffices for every index: the shift preserves the ball, and the approximant satisfies the same time-invariance identity as N, so a uniform approximation of the instant-zero functional on the ball covers all instants. And the positivity of M is not decorative: without it the ball can be empty and the statement, while true, asserts nothing.
Confirmed by the mission captain (proposal self-audit).