Reservoir systems: solutions, uniform bounds, contraction, weighting sequences, fading memory

Definition

ReservoirESN

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

dynamical-systemsecho-state-networkmachine-learningreservoir-computing

This module fixes the objects of discrete-time reservoir computing, following Section 2 of Grigoryeva-Ortega.

Time convention. The source indexes time by the nonpositive integers, writing the reservoir equation as $x_t = F(x_{t-1}, z_t)$ for $t \in \mathbb{Z}_-$ . Here time is indexed by $\mathbb{N}$ instead, with index $k$ denoting the instant $k$ steps into the past and $k = 0$ the present. Setting $X_k = x_{-k}$ and $Z_k = z_{-k}$ turns the equation into

X_k = F(X_{k+1}, Z_k),

which is the same constraint under a relabelling of the index set.

Reservoir equation. Given a reservoir map $F$ sending a state and an input to a new state, a state sequence is a solution for the input sequence $z$ when it satisfies the displayed equation at every instant.

Uniform bounds. A sequence is uniformly bounded by $M$ when every one of its terms has norm at most $M$ . This is the set written $K_M$ in the source, equation (2.14).

Contracting reservoir maps. A reservoir map is contracting with ratio $r$ on the balls of radii $L$ and $M$ when it maps the state ball into itself and satisfies

\lVert F(x,z) - F(y,z) \rVert \le r \lVert x - y \rVert

for all states of norm at most $L$ and inputs of norm at most $M$ , with $0 \le r < 1$ and both radii strictly positive, as in the source. The contraction is uniform in the input.

Weighting sequences and fading memory. A weighting sequence is a map $w : \mathbb{N} \to (0,1]$ , decreasing to zero, discounting the past: $w_k$ weights the instant $k$ steps before the present. The weighted norm of Definition 2.5 is $\lVert z \rVert_w = \sup_k \lVert z_k \rVert w_k$ ; the predicate recorded here is the statement that a given real number is an upper bound for that supremum. The fading memory property is then expressed in $\varepsilon$ - $\delta$ form: inputs that are close in weighted norm produce present states that are close.

Formalization Note States and inputs live in arbitrary normed additive groups, so the definitions apply beyond the Euclidean setting; completeness is required only where a limit is taken, and is therefore an assumption of the theorems rather than of the definitions. The weighted norm is recorded through the bound predicate rather than as a supremum, which avoids assuming beforehand that the supremum exists.

Squashing functions. The definition follows the source: nondecreasing, with values in $[-1,1]$ and limits $-1$ and $+1$ at $\mp\infty$ , plus a Lipschitz constant. The two limits matter: without them a constant map would qualify.

Uniform continuity in the input. The source assumes the reservoir map to be continuous and works in finite dimension, where continuity on a closed ball is automatically uniform. Since the development here allows arbitrary normed spaces, uniform continuity in the input on the relevant balls is recorded as a separate predicate. It is not decorative: contractivity alone constrains only the dependence on the state, and a reservoir map that is contracting but wildly discontinuous in the input fails the fading memory property.

Definition code

import Mathlib

set_option autoImplicit false

open Metric Matrix

namespace ReservoirESN

/-- **Equation de reservoir, indexee par le passe.** L'article ecrit
`x_t = F(x_{t-1}, z_t)` pour `t ∈ ℤ_-`. En posant `X k := x_{-k}` et `Z k := z_{-k}`,
cela devient `X k = F (X (k+1)) (Z k)` : l'indice `k` compte les pas dans le passe,
`k = 0` etant le present. -/
def IsSolution {E S : Type*} [NormedAddCommGroup E] [NormedAddCommGroup S]
    (F : S → E → S) (z : ℕ → E) (x : ℕ → S) : Prop :=
  ∀ k, x k = F (x (k + 1)) (z k)

/-- Suites uniformement bornees par `M` : le `K_M` de l'article, eq. (2.14). -/
def UnifBdd {E : Type*} [NormedAddCommGroup E] (M : ℝ) (z : ℕ → E) : Prop :=
  ∀ k, ‖z k‖ ≤ M

/-- Une application de reservoir est **contractante** de rapport `r` sur les boules
`B(0,L) × B(0,M)` lorsqu'elle y laisse `B(0,L)` invariante et contracte l'etat
uniformement en l'entree. Les rayons sont strictement positifs, comme dans la
source (« Let M > 0 »), ce qui empeche que les hypotheses soient vides. -/
structure IsContracting {E S : Type*} [NormedAddCommGroup E] [NormedAddCommGroup S]
    (F : S → E → S) (L M r : ℝ) : Prop where
  nonneg : 0 ≤ r
  lt_one : r < 1
  state_radius_pos : 0 < L
  input_radius_pos : 0 < M
  maps_to : ∀ x w, ‖x‖ ≤ L → ‖w‖ ≤ M → ‖F x w‖ ≤ L
  contract : ∀ x y w, ‖x‖ ≤ L → ‖y‖ ≤ L → ‖w‖ ≤ M → ‖F x w - F y w‖ ≤ r * ‖x - y‖

/-- Une **suite de ponderation** au sens de la Definition 2.5 : `w : ℕ → (0,1]`,
decroissante et tendant vers zero. `w k` pondere l'instant situe `k` pas dans le passe. -/
structure IsWeighting (w : ℕ → ℝ) : Prop where
  pos : ∀ k, 0 < w k
  le_one : ∀ k, w k ≤ 1
  antitone : Antitone w
  tendsto_zero : Filter.Tendsto w Filter.atTop (nhds 0)

/-- Norme ponderee `‖z‖_w = sup_k ‖z k‖ * w k` de la Definition 2.5, sous la forme
« majorant » : `WeightedBound w z c` dit que `c` majore cette borne superieure. -/
def WeightedBound {E : Type*} [NormedAddCommGroup E] (w : ℕ → ℝ) (z : ℕ → E) (c : ℝ) : Prop :=
  ∀ k, ‖z k‖ * w k ≤ c

/-- **Propriete de memoire evanescente** (Definition 2.5) pour l'application
entree ↦ etat present, exprimee en `ε`-`δ` avec la norme ponderee. -/
def HasFadingMemory {E S : Type*} [NormedAddCommGroup E] [NormedAddCommGroup S]
    (F : S → E → S) (L M : ℝ) (w : ℕ → ℝ) : Prop :=
  ∀ ε > 0, ∃ δ > 0, ∀ z z' : ℕ → E, ∀ x x' : ℕ → S,
    UnifBdd M z → UnifBdd M z' → UnifBdd L x → UnifBdd L x' →
    IsSolution F z x → IsSolution F z' x' →
    WeightedBound w (fun k => z k - z' k) δ →
    ‖x 0 - x' 0‖ < ε

/-- **Continuite uniforme en l'entree** sur les boules `B(0,L) × B(0,M)`.
La source suppose l'application de reservoir continue (Theoreme 3.1) et travaille en
dimension finie, ou la continuite sur un compact est automatiquement uniforme. En
dimension quelconque cette uniformite doit etre demandee : sans elle deux entrees
arbitrairement proches peuvent produire des etats eloignes, et la memoire evanescente
est en defaut. -/
def UnifContInput {E S : Type*} [NormedAddCommGroup E] [NormedAddCommGroup S]
    (F : S → E → S) (L M : ℝ) : Prop :=
  ∀ ε > 0, ∃ δ > 0, ∀ x : S, ∀ z z' : E,
    ‖x‖ ≤ L → ‖z‖ ≤ M → ‖z'‖ ≤ M → ‖z - z'‖ < δ → ‖F x z - F x z'‖ < ε

/-- **Memoire evanescente d'une fonctionnelle.** Une fonctionnelle envoie une suite
d'entrees sur la valeur presente de la sortie. Par la Proposition 2.12 de la source,
filtres causaux invariants et fonctionnelles se correspondent bijectivement, la FMP
d'un cote equivalant a celle de l'autre ; travailler avec la fonctionnelle est donc
fidele et evite d'avoir a formaliser separement causalite et invariance temporelle. -/
def FunctionalFMP {E S : Type*} [NormedAddCommGroup E] [NormedAddCommGroup S]
    (H : (ℕ → E) → S) (M : ℝ) (w : ℕ → ℝ) : Prop :=
  ∀ ε > 0, ∃ δ > 0, ∀ z z' : ℕ → E,
    UnifBdd M z → UnifBdd M z' → WeightedBound w (fun k => z k - z' k) δ →
    ‖H z - H z'‖ < ε

/-- **Equation d'un reseau a etats d'echo** : `x_k = σ(A x_{k+1} + C z_k + ζ)`,
`σ` etant appliquee composante par composante. Indexation par le passe, comme partout. -/
def IsESNSolution {n N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ) (Cin : Matrix (Fin N) (Fin n) ℝ)
    (ζ : EuclideanSpace ℝ (Fin N)) (σ : ℝ → ℝ)
    (z : ℕ → EuclideanSpace ℝ (Fin n)) (x : ℕ → EuclideanSpace ℝ (Fin N)) : Prop :=
  ∀ k i, x k i = σ ((A *ᵥ (EuclideanSpace.equiv (Fin N) ℝ (x (k + 1)))
      + Cin *ᵥ (EuclideanSpace.equiv (Fin n) ℝ (z k))) i + ζ i)

/-- **Fonction d'ecrasement** au sens de la source : croissante, de limites `-1` et `1`,
a valeurs dans `[-1,1]`, de limites `-1` en `-∞` et `1` en `+∞`, et lipschitzienne de
rapport `Lσ`. Les deux limites sont dans la definition de la source ; sans elles une
fonction constante passerait pour une fonction d'ecrasement. -/
structure IsSquashing (σ : ℝ → ℝ) (Lσ : ℝ) : Prop where
  lipschitz_nonneg : 0 ≤ Lσ
  range_mem : ∀ t : ℝ, σ t ∈ Set.Icc (-1 : ℝ) 1
  monotone : Monotone σ
  tendsto_atBot : Filter.Tendsto σ Filter.atBot (nhds (-1))
  tendsto_atTop : Filter.Tendsto σ Filter.atTop (nhds 1)
  lipschitz : ∀ s t : ℝ, |σ s - σ t| ≤ Lσ * |s - t|

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, Section 2 (Definitions 2.3 and 2.5, equation (2.14)) and Section 3 (contraction hypothesis of Theorem 3.1(ii)).

Read-back

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

The file contains ten declarations and no theorem; nothing below is proved, and no declaration is stated to depend on any other except where noted. Throughout, $E$ and $S$ are arbitrary types carrying a normed additive commutative group structure (no completeness, no finite dimension, no inner product, no vector-space structure over $\mathbb{R}$ beyond what a normed additive group gives), and all index sets are $\mathbb{N}$ .

Reservoir equation. For a map $F : S \times E \to S$ , an input sequence $z : \mathbb{N} \to E$ and a state sequence $x : \mathbb{N} \to S$ , the predicate $\mathrm{IsSolution}(F, z, x)$ asserts

\forall k \in \mathbb{N},\quad x_k = F(x_{k+1},\, z_k).

Note the index shift: the state at index $k$ is determined by the state at the larger index $k+1$ . The condition is imposed for every $k \in \mathbb{N}$ , so the recursion never terminates and there is no initial condition; nothing asserts existence or uniqueness of such an $x$ .

Uniform bound. $\mathrm{UnifBdd}(M, z)$ , for $M \in \mathbb{R}$ and $z : \mathbb{N} \to E$ , asserts $\|z_k\| \le M$ for every $k$ . $M$ is unconstrained in sign: for $M < 0$ the predicate holds for no sequence, and for $M = 0$ only for the zero sequence.

Contraction. $\mathrm{IsContracting}(F, L, M, r)$ is a conjunction of six conditions on real numbers $L, M, r$ : $0 \le r$ ; $r < 1$ (strict); $0 < L$ ; $0 < M$ ; the invariance condition $\|F(x,w)\| \le L$ whenever $\|x\| \le L$ and $\|w\| \le M$ ; and the contraction condition

\|F(x,w) - F(y,w)\| \le r\,\|x-y\| \quad\text{whenever } \|x\|\le L,\ \|y\|\le L,\ \|w\|\le M.

The contraction is required only for the same input $w$ on both sides; nothing is asserted about $F(x,w)$ versus $F(x,w')$ . The balls are closed.

Weighting sequence. $\mathrm{IsWeighting}(w)$ , for $w : \mathbb{N} \to \mathbb{R}$ , asserts: $w_k > 0$ for all $k$ ; $w_k \le 1$ for all $k$ ; $w$ is antitone (non-increasing, $j \le k \Rightarrow w_k \le w_j$ ); and $w_k \to 0$ as $k \to \infty$ .

Weighted bound. $\mathrm{WeightedBound}(w, z, c)$ asserts the pointwise inequality $\|z_k\|\,w_k \le c$ for every $k$ . It says $c$ is an upper bound for each term, not that $c$ equals the supremum; $c$ and $w$ are arbitrary reals/real sequences here, with no positivity or weighting hypothesis.

Fading memory for a reservoir map. $\mathrm{HasFadingMemory}(F, L, M, w)$ asserts: for every $\varepsilon > 0$ there exists $\delta > 0$ such that for all input sequences $z, z' : \mathbb{N} \to E$ and all state sequences $x, x' : \mathbb{N} \to S$ satisfying

$\|z_k\| \le M$ and $\|z'_k\| \le M$ for all $k$ ,
$\|x_k\| \le L$ and $\|x'_k\| \le L$ for all $k$ ,
$x_k = F(x_{k+1}, z_k)$ and $x'_k = F(x'_{k+1}, z'_k)$ for all $k$ ,
$\|z_k - z'_k\|\,w_k \le \delta$ for all $k$ (non-strict),

one has $\|x_0 - x'_0\| < \varepsilon$ (strict). Only the value at index $0$ is compared. No hypothesis requires $w$ to be a weighting sequence, or $F$ to be contracting or continuous; if no pair of bounded solutions exists, the statement holds vacuously.

Uniform continuity in the input. $\mathrm{UnifContInput}(F, L, M)$ asserts: for every $\varepsilon>0$ there is $\delta>0$ such that for every state $x$ with $\|x\| \le L$ and all inputs $z, z'$ with $\|z\| \le M$ , $\|z'\| \le M$ and $\|z - z'\| < \delta$ , one has $\|F(x,z) - F(x,z')\| < \varepsilon$ . The same $x$ appears on both sides; this is uniformity in $x$ and in the pair $(z,z')$ .

Fading memory for a functional. For $H : (\mathbb{N} \to E) \to S$ , $\mathrm{FunctionalFMP}(H, M, w)$ asserts: for every $\varepsilon>0$ there is $\delta>0$ such that for all $z, z'$ with $\|z_k\| \le M$ , $\|z'_k\| \le M$ for all $k$ and $\|z_k - z'_k\|\,w_k \le \delta$ for all $k$ , one has $\|H(z) - H(z')\| < \varepsilon$ . Again $w$ is an arbitrary real sequence, unconstrained.

Echo state network equation. For natural numbers $n, N$ , a matrix $A \in \mathbb{R}^{N\times N}$ , a matrix $C_{\mathrm{in}} \in \mathbb{R}^{N\times n}$ , a vector $\zeta \in \mathbb{R}^N$ , a scalar function $\sigma : \mathbb{R}\to\mathbb{R}$ , inputs $z : \mathbb{N} \to \mathbb{R}^n$ and states $x : \mathbb{N} \to \mathbb{R}^N$ (Euclidean spaces), $\mathrm{IsESNSolution}$ asserts that for every $k \in \mathbb{N}$ and every coordinate $i \in \{0,\dots,N-1\}$ ,

x_k(i) = \sigma\!\big((A\,x_{k+1} + C_{\mathrm{in}}\,z_k)(i) + \zeta(i)\big),

with $\sigma$ applied coordinatewise and the same backward index shift as above. The dimensions $n$ and $N$ are implicit arguments and may be $0$ , in which case the coordinate quantifier is empty and the condition is vacuous.

Squashing function. $\mathrm{IsSquashing}(\sigma, L_\sigma)$ asserts: $0 \le L_\sigma$ ; $\sigma(t) \in [-1,1]$ for every real $t$ ; $\sigma$ is monotone (non-decreasing, not strictly); $\sigma(t) \to -1$ as $t \to -\infty$ ; $\sigma(t) \to 1$ as $t \to +\infty$ ; and $|\sigma(s)-\sigma(t)| \le L_\sigma\,|s-t|$ for all reals $s,t$ .

Human review

Endorsed by Shuze Chen · Sep 11, 2026
Endorsed by olivier · Sep 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph