Echo state property of a contracting reservoir (Prop. 3.1(ii))

Proved

ReservoirESN.esp_of_contracting

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

echo-state-networkfixed-pointmachine-learningreservoir-computing

Let $F$ be a reservoir map that is contracting with ratio $r < 1$ on the ball of radius $L$ , uniformly over inputs of norm at most $M$ , and let the state space be complete. Then for every input sequence $z$ uniformly bounded by $M$ there is exactly one state sequence $x$ , uniformly bounded by $L$ , satisfying

x_k = F(x_{k+1}, z_k) \qquad \text{for every } k .

This is the echo state property of Jaeger, in the form proved as part (ii) of Proposition 3.1 of the source. Uniqueness is what makes the assignment $z \mapsto x$ a well-defined map — the filter induced by $F$ — and existence is what makes that map total.

Both halves are genuine assertions. Since time runs from the infinite past there is no initial condition to iterate from, so the equation constrains an entire sequence rather than generating one; existence cannot be read off from the recursion. Uniqueness fails without contractivity: a reservoir map may admit a whole family of bounded solutions for the same input, in which case the state at the present instant retains a memory of an initialization infinitely far back.

Formalization Note The statement is $\exists!$ over sequences satisfying the conjunction of the boundedness and the equation, so uniqueness is asserted within the bounded solutions only, exactly as in the source; nothing is claimed about unbounded ones. Completeness of the state space is assumed because the solution is obtained as a limit.

Preamble

import Mathlib
import Definitions.Def_ReservoirESN

open Matrix Metric ReservoirESN

Formal statement

namespace ReservoirESN

theorem esp_of_contracting {E S : Type*} [NormedAddCommGroup E] [NormedAddCommGroup S]
    [CompleteSpace S] (F : S → E → S) (L M r : ℝ)
    (hF : IsContracting F L M r) (z : ℕ → E) (hz : UnifBdd M z) :
    ∃! x : ℕ → S, UnifBdd L x ∧ IsSolution F z x := 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): existence and uniqueness of the bounded solution (echo state property).

Read-back

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

`ReservoirESN.esp_of_contracting`

Let $E$ and $S$ be two arbitrary types, each carrying the structure of a normed additive commutative group (so each has a zero, subtraction, and a norm $\|\cdot\|$ satisfying the usual axioms; in particular neither is empty, and neither is assumed finite-dimensional). Assume in addition that $S$ is a complete normed group. No completeness, separability, continuity or dimension assumption is placed on $E$ .

Let

F : S \to E \to S

be an arbitrary function of two arguments — a state in $S$ and an input in $E$ — with no continuity or measurability assumed, and let $L$ , $M$ , $r$ be three real numbers. The statement assumes $F$ is contracting with ratio $r$ on the closed balls of radii $L$ and $M$ , which unfolds into exactly six conditions:

$0 \le r$ ;
$r < 1$ (strictly);
$0 < L$ (strictly);
$0 < M$ (strictly);
invariance: for all $x \in S$ and $w \in E$ , if $\|x\| \le L$ and $\|w\| \le M$ then $\|F(x,w)\| \le L$ ;
contraction, uniform in the input: for all $x, y \in S$ and $w \in E$ , if $\|x\| \le L$ , $\|y\| \le L$ and $\|w\| \le M$ , then

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

All the ball conditions are non-strict ( $\le$ ), i.e. closed balls centred at the origin. The contraction is asserted only in the state argument; nothing whatsoever is assumed about how $F$ varies with its input argument $w$ .

Finally, let $z : \mathbb{N} \to E$ be an arbitrary sequence indexed by the natural numbers, assumed uniformly bounded by $M$ , which means exactly

\|z_k\| \le M \quad \text{for every } k \in \mathbb{N}.

Under these hypotheses the theorem asserts: there exists exactly one sequence $x : \mathbb{N} \to S$ such that both of the following hold:

$\|x_k\| \le L$ for every $k \in \mathbb{N}$ ; and
$x_k = F\!\left(x_{k+1},\, z_k\right)$ for every $k \in \mathbb{N}$ .

Several features of this conclusion are worth spelling out. The recursion runs backwards in the index: the term at index $k$ is determined by the term at index $k+1$ together with $z_k$ . There is no initial condition, no anchoring value at $k = 0$ , and no limiting condition as $k \to \infty$ ; the displayed equation is required at every $k$ including $k = 0$ .

The uniqueness is relative to the conjunction: it says that any sequence $y : \mathbb{N} \to S$ that is both bounded in norm by $L$ at every index and satisfies the same recursion at every index is equal to $x$ — equal as a function, i.e. $y_k = x_k$ for all $k$ . It says nothing about sequences that satisfy the recursion but violate the bound $\|y_k\| \le L$ ; such sequences may exist without contradicting the statement. The quantifier is unique existence, not mere existence and not "unique up to" anything.

The bound $L$ used for the solution is the same $L$ appearing in the invariance and contraction hypotheses, and the bound $M$ used for $z$ is the same $M$ appearing there. The parameter $r$ occurs nowhere in the conclusion; it is only constrained to lie in $[0,1)$ and to bound the contraction in hypothesis 6. Because $L > 0$ and $M > 0$ are explicitly required, the closed balls involved are non-degenerate; the hypotheses are satisfiable (for instance by $F$ constantly $0$ with $z$ constantly $0$ ), so the statement is not vacuous.

No claim is made about continuity of $x$ in $z$ , about dependence of $x$ on $z$ , or about any weighted norm, fading-memory, echo-state-network or squashing-function notion: none of those auxiliary definitions from the accompanying file occurs in this statement.

View graph