Uniform polynomial approximation of fading-memory functionals on bounded histories

Proved

ReservoirSAS.fmp_polynomial_approximation

by con · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

fading-memoryfunctional-analysispolynomial-approximationreservoir-computing

Let $w:\mathbb N\to\mathbb R$ be a weighting sequence and let $H:(\mathbb N\to\mathbb R)\to\mathbb R$ have the fading-memory property on histories bounded by one, relative to $w$ . For every $\eta>0$ there exists a real polynomial $f$ in finitely many of the history coordinates such that

|H(z)-f(z_0,z_1,\ldots)|<\eta

for every history $z$ with $z_k\in[-1,1]$ at every index.

This isolates the approximation-theoretic part of SAS universality. The index set of polynomial variables is $\mathbb N$ , but each multivariate polynomial contains only finitely many monomials and variables; the approximant therefore uses a finite history. The SAS realization of that polynomial is a separate finite-dimensional construction.

The result is a Stone–Weierstrass consequence of the compact-history and fading-memory framework in the source, presented here as a separate reusable lemma. It uses exactly the mission's existing FunctionalFMP convention. No assertion is made about inputs outside the cube.

Preamble

import Definitions.Def_ReservoirESN
import Definitions.Def_ReservoirSAS
import Mathlib.Algebra.MvPolynomial.Eval

open ReservoirESN ReservoirSAS

Formal statement

namespace ReservoirSAS
theorem fmp_polynomial_approximation (w : ℕ → ℝ) (hw : IsWeighting w)
    (H : (ℕ → ℝ) → ℝ) (hH : FunctionalFMP H 1 w)
    (η : ℝ) (hη : 0 < η) :
    ∃ f : MvPolynomial ℕ ℝ, ∀ z : ℕ → ℝ,
      (∀ k, z k ∈ Set.Icc (-1 : ℝ) 1) → |H z - MvPolynomial.eval z f| < η := by sorry
end ReservoirSAS

Source

L. Grigoryeva and J.-P. Ortega, Universal discrete-time reservoir computers with stochastic inputs and linear readouts using non-homogeneous state-affine systems, JMLR 19(24) (2018), https://jmlr.org/papers/volume19/18-020/18-020.pdf. Lemma 2 (compactness of bounded histories), Theorem 8 (Stone–Weierstrass framework), and Theorem 19 / Appendix 6.10, pp. 12–13 and 30–31. This is the coordinate-polynomial specialization of that approximation mechanism, not a verbatim separately numbered assertion. The proof establishes continuity for the product topology directly from the published weighting/FMP definitions, then uses Mathlib Stone–Weierstrass.

View graph