Fading memory of a contracting reservoir (Prop. 3.1(ii))

Proved

ReservoirESN.fmp_of_contracting

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

echo-state-networkfading-memorymachine-learningreservoir-computing

Let $F$ be a reservoir map contracting with ratio $r < 1$ on the ball of radius $L$ , uniformly over inputs of norm at most $M$ , and let $w$ be a weighting sequence. Then the induced filter has the fading memory property with respect to $w$ : for every $\varepsilon > 0$ there is $\delta > 0$ such that any two admissible input sequences whose difference has weighted norm at most $\delta$ produce bounded solutions whose present states differ by less than $\varepsilon$ .

This is the second half of part (ii) of Proposition 3.1. The point of the source is that fading memory is not an extra hypothesis: it comes for free from the same contractivity condition that gives the echo state property. In the earlier literature the two were treated separately, contractivity being studied as a sufficient condition for the echo state property alone.

Fading memory is the continuity notion under which the approximation theory of Boyd and Chua, and the later universality results for reservoir systems, are stated; it is what licenses treating the input/output map as an operator that can be approximated.

Formalization Note Uniform continuity of the reservoir map in the input is an explicit hypothesis. It corresponds to the continuity assumption of Theorem 3.1 in the source, which is automatic on the compact balls of a finite-dimensional space; in a general normed space it must be required, since contractivity constrains only the dependence on the state. Continuity of the filter is stated in $\varepsilon$ - $\delta$ form against the weighted norm rather than the supremum norm, which is essential: a bound holding at each instant separately does not give continuity in the intended topology. The conclusion concerns the state at the present instant, which is the reservoir functional associated with the filter.

Preamble

import Mathlib
import Definitions.Def_ReservoirESN

open Matrix Metric ReservoirESN

Formal statement

namespace ReservoirESN

theorem fmp_of_contracting {E S : Type*} [NormedAddCommGroup E] [NormedAddCommGroup S]
    [CompleteSpace S] (F : S → E → S) (L M r : ℝ) (w : ℕ → ℝ)
    (hF : IsContracting F L M r) (hcont : UnifContInput F L M) (hw : IsWeighting w) :
    HasFadingMemory F L M w := 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. 11, Proposition 3.1, part (ii): the induced filter has the fading memory property.

Read-back

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

Fix two real normed vector spaces (more precisely, two normed additive commutative groups) $E$ and $S$ , of arbitrary dimension, and assume $S$ is complete. Fix a map

F : S \times E \to S,

three real numbers $L, M, r$ , and a sequence of real numbers $w : \mathbb{N} \to \mathbb{R}$ . All of $E$ , $S$ , $F$ , $L$ , $M$ , $r$ , $w$ are universally quantified; no finite-dimensionality, continuity, measurability or linearity is assumed of $F$ beyond what the three hypotheses below state, and $E$ is not assumed complete.

Throughout, sequences are indexed by $\mathbb{N}$ read as "steps into the past": index $k$ refers to the instant $k$ steps before the present, and $k = 0$ is the present.

Hypothesis 1 ( $F$ is contracting with data $L, M, r$ ). All six of the following hold: $0 \le r$ ; $r < 1$ ; $0 < L$ ; $0 < M$ ; for all $x \in S$ and $z \in E$ with $\|x\| \le L$ and $\|z\| \le M$ one has $\|F(x,z)\| \le L$ ; and for all $x, y \in S$ and $z \in E$ with $\|x\| \le L$ , $\|y\| \le L$ , $\|z\| \le M$ ,

\|F(x,z) - F(y,z)\| \le r\,\|x - y\|.

Since $L$ and $M$ are strictly positive, these conditions are not vacuous.

Hypothesis 2 (uniform continuity in the input on the balls of radii $L$ and $M$ ). For every $\varepsilon > 0$ there exists $\delta > 0$ such that for every state $x \in S$ with $\|x\| \le L$ and every pair of inputs $z, z' \in E$ with $\|z\| \le M$ , $\|z'\| \le M$ and $\|z - z'\| < \delta$ , one has $\|F(x,z) - F(x,z')\| < \varepsilon$ . The $\delta$ is uniform in $x$ as well as in $z, z'$ .

Hypothesis 3 ( $w$ is a weighting sequence). For every $k$ , $0 < w_k$ and $w_k \le 1$ ; $w$ is antitone ( $j \le k \Rightarrow w_k \le w_j$ ); and $w_k \to 0$ as $k \to \infty$ .

Conclusion (fading memory for $F$ with data $L, M, w$ ). 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 every $k$ ;
$\|x_k\| \le L$ and $\|x'_k\| \le L$ for every $k$ ;
the reservoir recursion holds for every $k \in \mathbb{N}$ (including $k = 0$ ):

x_k = F\bigl(x_{k+1},\, z_k\bigr), \qquad x'_k = F\bigl(x'_{k+1},\, z'_k\bigr);

and the weighted-difference bound holds termwise: for every $k$ ,

\|z_k - z'_k\|\, w_k \le \delta,

one has the strict estimate at the present instant

\|x_0 - x'_0\| < \varepsilon.

Several points are literal features of the statement. The parameter $r$ appears only in Hypothesis 1; it does not occur in the conclusion. The completeness of $S$ is assumed but appears nowhere in the conclusion's wording. The conclusion asserts nothing about the existence of solution sequences $x$ : it is a statement about arbitrary pairs of sequences that already satisfy the recursion and the uniform bounds, so for input pairs admitting no such bounded solution the inner claim is vacuously satisfied. The state bounds $\|x_k\| \le L$ and $\|x'_k\| \le L$ are hypotheses imposed on the sequences, not derived. The weighted condition is a bound on each individual term $\|z_k - z'_k\| w_k$ by $\delta$ (equivalently, $\delta$ bounds the supremum over $k$ ), stated with a non-strict $\le$ , while the conclusion $\|x_0 - x'_0\| < \varepsilon$ is strict. The order of quantifiers is: $\delta$ depends only on $\varepsilon$ (and on $F, L, M, w$ ), and is then uniform over all admissible quadruples $(z, z', x, x')$ . Only the present-time discrepancy $\|x_0 - x'_0\|$ is controlled; nothing is asserted about $\|x_k - x'_k\|$ for $k \ge 1$ .

View graph