Echo state networks are universal (Thm. 4.1)

Open

ReservoirESN.esn_universal

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

echo-state-networkmachine-learningreservoir-computinguniversal-approximation

Let $H$ be a functional on uniformly bounded input sequences with the fading memory property: it sends an input history to the present value of an output, continuously for the weighted norm. The theorem asserts that for every accuracy $\varepsilon > 0$ there is an echo state network

x_k = \sigma\!\left(A x_{k+1} + C z_k + \zeta\right), \qquad y = W x_0 ,

with a squashing function $\sigma$ and a reservoir matrix satisfying the contraction condition, whose linear readout approximates $H$ uniformly over all admissible inputs:

\sup_{z} \; \lVert H(z) - W x_0(z) \rVert < \varepsilon .

In words: any fading memory input/output system in discrete time is realized, to arbitrary accuracy, by a finite-dimensional network whose recurrent part is fixed and whose only trained component is a linear readout. This is the theorem that justifies reservoir computing as a method: it says the architecture is not merely convenient but expressive enough in principle, and that the training problem may legitimately be reduced to a linear regression.

The result is proved in the source. Its proof is not self-contained: the target functional is first approximated by a non-homogeneous state-affine system, using a density theorem established in a companion paper, and only then is that system replaced by an echo state network.

Formalization Note The statement is phrased for the functional rather than the filter. By Proposition 2.12 of the source the two are in linear bijection, with the fading memory property on one side equivalent to it on the other, so nothing is lost; this avoids formalizing causality and time-invariance separately. The approximating network is required to satisfy the contraction condition $n_A L_\sigma < 1$ , which by the supporting target gives it the echo state property, so the state sequence it is evaluated at is the unique bounded one; the conclusion is stated for any such state sequence rather than presupposing a choice. The bound on the reservoir matrix is an operator inequality with an explicit constant, of which the spectral norm is one admissible value. The supremum over inputs is expressed as a universally quantified strict inequality.

Preamble

import Mathlib
import Definitions.Def_ReservoirESN

open Matrix Metric ReservoirESN

Formal statement

namespace ReservoirESN

theorem esn_universal {n d : ℕ} (hd : 0 < d)
    (M : ℝ) (hM : 0 < M) (w : ℕ → ℝ) (hw : IsWeighting w)
    (H : (ℕ → EuclideanSpace ℝ (Fin n)) → EuclideanSpace ℝ (Fin d))
    (hH : FunctionalFMP H M w) (ε : ℝ) (hε : 0 < ε) :
    ∃ (N : ℕ) (A : Matrix (Fin N) (Fin N) ℝ) (Cin : Matrix (Fin N) (Fin n) ℝ)
      (ζ : EuclideanSpace ℝ (Fin N)) (W : Matrix (Fin d) (Fin N) ℝ)
      (σ : ℝ → ℝ) (Lσ nA : ℝ),
      IsSquashing σ Lσ ∧ 0 ≤ nA ∧
      (∀ v : EuclideanSpace ℝ (Fin N),
        ‖(EuclideanSpace.equiv (Fin N) ℝ).symm (A *ᵥ (EuclideanSpace.equiv (Fin N) ℝ v))‖
          ≤ nA * ‖v‖) ∧
      nA * Lσ < 1 ∧
      ∀ z : ℕ → EuclideanSpace ℝ (Fin n), UnifBdd M z →
        ∀ x : ℕ → EuclideanSpace ℝ (Fin N), IsESNSolution A Cin ζ σ z x →
          (∀ k i, x k i ∈ Set.Icc (-1 : ℝ) 1) →
          ‖H z - (EuclideanSpace.equiv (Fin d) ℝ).symm
              (W *ᵥ (EuclideanSpace.equiv (Fin N) ℝ (x 0)))‖ < ε := by sorry

end ReservoirESN

Source

L. Grigoryeva, J.-P. Ortega, Echo state networks are universal, Neural Networks 108 (2018), 495-508, https://arxiv.org/abs/1806.00797, p. 14, Theorem 4.1: every causal, time-invariant filter with the fading memory property on uniformly bounded inputs is uniformly approximated by an echo state network with a linear readout.

Read-back

What the Lean code literally says, in plain math · claude-opus-5

Read-back — `esn_universal`

The statement fixes two natural numbers $n$ and $d$ (implicit arguments, so $n$ is unconstrained and may be $0$ ; $d$ is assumed to satisfy $0 < d$ ), a real $M$ with $0 < M$ , a sequence $w : \mathbb{N} \to \mathbb{R}$ , a map

H : (\mathbb{N} \to \mathbb{R}^n) \longrightarrow \mathbb{R}^d,

where $\mathbb{R}^n$ and $\mathbb{R}^d$ carry the Euclidean ( $\ell^2$ ) norm, and a real $\varepsilon$ with $0 < \varepsilon$ .

Three hypotheses are assumed.

$w$ is a weighting sequence: $w_k > 0$ for every $k$ , $w_k \le 1$ for every $k$ , $w$ is antitone (non-increasing), and $w_k \to 0$ as $k \to \infty$ .
$H$ has the functional fading-memory property with radius $M$ and weight $w$ : for every $\varepsilon' > 0$ there exists $\delta > 0$ such that for all input sequences $z, z' : \mathbb{N} \to \mathbb{R}^n$ satisfying $\|z_k\| \le M$ and $\|z'_k\| \le M$ for every $k$ , if the pointwise weighted bound $\|z_k - z'_k\| \cdot w_k \le \delta$ holds for every $k$ , then $\|H(z) - H(z')\| < \varepsilon'$ . (The weighted condition is a pointwise bound by $\delta$ , non-strict, not a statement about an actual supremum.)
$0 < d$ , $0 < M$ , $0 < \varepsilon$ .

Under these hypotheses the conclusion asserts the existence of: a natural number $N$ ; a real matrix $A \in \mathbb{R}^{N \times N}$ ; a real matrix $C_{\mathrm{in}} \in \mathbb{R}^{N \times n}$ ; a vector $\zeta \in \mathbb{R}^N$ ; a real matrix $W \in \mathbb{R}^{d \times N}$ ; a function $\sigma : \mathbb{R} \to \mathbb{R}$ ; and two reals $L_\sigma$ and $n_A$ , such that all of the following hold simultaneously.

$\sigma$ is a squashing function with Lipschitz constant $L_\sigma$ : $0 \le L_\sigma$ ; $\sigma(t) \in [-1,1]$ for every real $t$ ; $\sigma$ is monotone non-decreasing; $\sigma(t) \to -1$ as $t \to -\infty$ and $\sigma(t) \to 1$ as $t \to +\infty$ ; and $|\sigma(s) - \sigma(t)| \le L_\sigma\,|s-t|$ for all reals $s,t$ .
$0 \le n_A$ .
$n_A$ bounds $A$ in $\ell^2$ operator norm: for every $v \in \mathbb{R}^N$ , $\|Av\| \le n_A \|v\|$ , the norms being Euclidean.
$n_A \cdot L_\sigma < 1$ , strictly.
For every input sequence $z : \mathbb{N} \to \mathbb{R}^n$ with $\|z_k\| \le M$ for every $k$ , and for every sequence $x : \mathbb{N} \to \mathbb{R}^N$ such that

x_k(i) \;=\; \sigma\!\Big( \big(A\,x_{k+1} + C_{\mathrm{in}}\,z_k\big)(i) + \zeta(i) \Big) \quad \text{for all } k \in \mathbb{N},\ i \in \{1,\dots,N\},

and such that additionally $x_k(i) \in [-1,1]$ for all $k$ and $i$ , one has

\big\| H(z) \;-\; W\,x_0 \big\| \;<\; \varepsilon .

Several features of the quantifier structure are worth stating explicitly. The objects $N, A, C_{\mathrm{in}}, \zeta, W, \sigma, L_\sigma, n_A$ are chosen before $z$ and $x$ , hence uniformly over all inputs bounded by $M$ and over all state sequences. The indexing convention is that $k$ increases into the past: the recursion expresses $x_k$ in terms of $x_{k+1}$ , and the approximation is asserted only at index $0$ .

The final clause is a conditional statement about state sequences $x$ ; the statement does not assert that such an $x$ exists for a given $z$ , nor that it is unique. If for some bounded $z$ no sequence satisfies the recursion, the requirement is vacuously met for that $z$ . The extra requirement $x_k(i) \in [-1,1]$ is an additional hypothesis narrowing the sequences quantified over (it is already entailed by the recursion together with the range condition on $\sigma$ ). The readout is purely linear: $W x_0$ , with no bias term. Nothing constrains $N$ to be positive, and $n$ may be $0$ . The constant $n_A$ is any number satisfying the operator bound, not necessarily the operator norm itself; likewise $L_\sigma$ is any admissible Lipschitz constant. The hypothesis $0 < d$ and the weighting hypothesis on $w$ enter the statement only as stated assumptions; $w$ itself appears in the conclusion nowhere.

The declaration is stated without a proof (its proof term is a placeholder).

Human review

Flagged by Shuze Chen · Sep 11, 2026
The following problem is reported by Fable 5. It seems this theorem is a stronger version of the one in the original paper. If that's intended, please ignore the report and submit again.

Theorem 4.1 does not give an approximant with nA * Lσ < 1: its conclusion is about generalized filters and the echo state property is only conditional (the authors confirm this in Gonon and Ortega, "Fading memory echo state networks are universal", Neural Networks 2021, arXiv:2010.12047, whose own construction is a nilpotent shift register with no bound on ‖A‖₂·Lσ). So the goal as stated is not the cited theorem. Either replace nA * Lσ < 1 by "for every admissible input the bounded state sequence exists and is unique" and cite the 2021 paper, or keep it and state in the source field and NL that this strengthening is not proved in either paper.

View graph

Echo state networks are universal (Thm. 4.1)

Read-back — esn_universal

Read-back — `esn_universal`