Echo state property under the spectral condition $\lVert A\rVert_2 L_\sigma < 1$ (Cor. 3.2(ii))

Proved

ReservoirESN.esn_esp_of_spectral_condition

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

echo-state-networkmachine-learningneural-networkreservoir-computing

Consider the echo state network

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

where $A$ is the $N \times N$ reservoir matrix, $C$ the $N \times n$ input matrix, $\zeta$ a bias vector, and $\sigma$ is applied componentwise. Assume $\sigma$ takes values in $[-1,1]$ and is Lipschitz with constant $L_\sigma$ , and that $A$ satisfies the operator bound $\lVert A v \rVert \le n_A \lVert v \rVert$ for all $v$ . If

n_A \, L_\sigma < 1 ,

then for every input sequence uniformly bounded by $M$ the network has exactly one state sequence with all components in $[-1,1]$ satisfying the displayed equation.

This is part (ii) of Corollary 3.2 of the source, specialized to the echo state property. Taking $n_A$ to be the spectral norm $\lVert A \rVert_2$ recovers the condition $\lVert A \rVert_2 L_\sigma < 1$ stated there, which is the sufficient condition that has circulated in the reservoir computing literature since Jaeger. The source notes that this condition is far from sharp and that sharper ones are known; the statement here is the classical one.

Formalization Note The bound on $A$ is stated as an operator inequality with an explicit constant $n_A$ rather than through a named matrix norm, so that any valid bound may be supplied and the spectral norm is one admissible choice. States and inputs are Euclidean, so that the operator bound refers to the Euclidean norm as in the source. The confinement of the state to $[-1,1]^N$ is expressed componentwise, matching the codomain of the squashing function; it is what plays the role of the invariant ball. Uniqueness is asserted among sequences with components in $[-1,1]$ .

Preamble

import Mathlib
import Definitions.Def_ReservoirESN

open Matrix Metric ReservoirESN

Formal statement

namespace ReservoirESN

theorem esn_esp_of_spectral_condition {n N : ℕ}
    (A : Matrix (Fin N) (Fin N) ℝ) (Cin : Matrix (Fin N) (Fin n) ℝ)
    (ζ : EuclideanSpace ℝ (Fin N)) (σ : ℝ → ℝ) (Lσ nA M : ℝ)
    (hσ : IsSquashing σ Lσ) (hnA : 0 ≤ nA)
    (hA : ∀ v : EuclideanSpace ℝ (Fin N),
      ‖(EuclideanSpace.equiv (Fin N) ℝ).symm (A *ᵥ (EuclideanSpace.equiv (Fin N) ℝ v))‖
        ≤ nA * ‖v‖)
    (hspec : nA * Lσ < 1) (hM : 0 < M) (hN : 0 < N)
    (z : ℕ → EuclideanSpace ℝ (Fin n)) (hz : UnifBdd M z) :
    ∃! x : ℕ → EuclideanSpace ℝ (Fin N),
      (∀ k i, x k i ∈ Set.Icc (-1 : ℝ) 1) ∧ IsESNSolution A Cin ζ σ 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. 13, Corollary 3.2, part (ii): a squashing function with Lipschitz constant L_sigma and a reservoir matrix with spectral norm satisfying ||A||_2 * L_sigma < 1 give the echo state and fading memory properties. The statement here is the echo state half.

Read-back

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

Read-back — `esn_esp_of_spectral_condition`

Fix two natural numbers $n$ and $N$ (both implicit; $n$ is unconstrained and may be $0$ , while $N$ is required to satisfy $N > 0$ ). The statement takes as data:

a square real matrix $A \in \mathbb{R}^{N \times N}$ and a real matrix $C^{\mathrm{in}} \in \mathbb{R}^{N \times n}$ ;
a vector $\zeta \in \mathbb{R}^{N}$ , where $\mathbb{R}^{N}$ carries the Euclidean ( $\ell^2$ ) norm;
a function $\sigma : \mathbb{R} \to \mathbb{R}$ and three real numbers $L_\sigma$ , $n_A$ , $M$ ;
a sequence $z : \mathbb{N} \to \mathbb{R}^{n}$ of inputs, again with the Euclidean norm.

The hypotheses are:

$\sigma$ is a squashing function with constant $L_\sigma$ , meaning all six of: $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$ ; $\sigma(t) \to 1$ as $t \to +\infty$ ; and $|\sigma(s) - \sigma(t)| \le L_\sigma\,|s-t|$ for all real $s,t$ .
$0 \le n_A$ .
$n_A$ bounds $A$ in operator $\ell^2$ -norm: for every $v \in \mathbb{R}^{N}$ , $\;\|A v\| \le n_A \|v\|$ , the norms being Euclidean. ( $n_A$ is not defined to be the operator norm or the spectral radius; it is any real number for which this bound is assumed.)
Spectral-type condition: $n_A \, L_\sigma < 1$ , strictly.
$M > 0$ and $N > 0$ .
The input is uniformly bounded by $M$ : $\|z_k\| \le M$ for every $k \in \mathbb{N}$ .

The conclusion asserts the existence of a unique sequence $x : \mathbb{N} \to \mathbb{R}^{N}$ satisfying the conjunction of two properties:

(a) Range constraint. For every index $k \in \mathbb{N}$ and every coordinate $i \in \{1,\dots,N\}$ , the real number $x_k(i)$ lies in the closed interval $[-1,1]$ .
(b) Echo-state equation. For every $k \in \mathbb{N}$ and every coordinate $i$ ,

x_k(i) \;=\; \sigma\!\Big( \big(A\,x_{k+1} + C^{\mathrm{in}} z_k\big)_i \;+\; \zeta_i \Big),

i.e. componentwise application of $\sigma$ to $A x_{k+1} + C^{\mathrm{in}} z_k + \zeta$ .

Several features of this formulation deserve to be stated explicitly.

The recursion runs backwards in the index: $x_k$ is expressed in terms of $x_{k+1}$ , the later index, not the earlier one. There is no initial condition at $k = 0$ ; the equation is imposed at every $k \in \mathbb{N}$ simultaneously, and uniqueness is uniqueness of the whole two-sided-in-spirit sequence as a function $\mathbb{N} \to \mathbb{R}^{N}$ .

Uniqueness is asserted only within the class of sequences satisfying both (a) and (b); nothing is claimed about sequences satisfying (b) alone. Note, however, that hypothesis 1 already forces $\sigma$ to take values in $[-1,1]$ , so any sequence satisfying (b) automatically satisfies (a); condition (a) therefore constrains nothing beyond (b).

The parameters $M$ and the bound $\|z_k\| \le M$ enter only as hypotheses; $M$ appears nowhere in the conclusion, and no quantitative bound, contraction rate, or continuous dependence on $z$ is claimed. Likewise $\zeta$ , $n_A$ and $L_\sigma$ are arbitrary subject to the stated constraints.

Edge cases the quantifiers silently admit: $n = 0$ is allowed, in which case $\mathbb{R}^{n}$ is the zero space, $C^{\mathrm{in}}$ is empty, $z$ is identically $0$ and hypothesis 6 is automatic. $n_A = 0$ is allowed (forcing $A v = 0$ for all $v$ ), and then hypothesis 4 holds for any $L_\sigma \ge 0$ . The case $L_\sigma = 0$ cannot occur, since a $0$ -Lipschitz $\sigma$ is constant and cannot have limits $-1$ and $+1$ at $\mp\infty$ ; so hypothesis 1 is never satisfied with $L_\sigma = 0$ . No continuity, boundedness or measurability is assumed of $\sigma$ beyond what hypothesis 1 lists, and no assumption whatever is made on $C^{\mathrm{in}}$ .

View graph

Echo state property under the spectral condition ∥A∥2Lσ<1\lVert A\rVert_2 L_\sigma < 1∥A∥2​Lσ​<1 (Cor. 3.2(ii))

Read-back — esn_esp_of_spectral_condition

Echo state property under the spectral condition $\lVert A\rVert_2 L_\sigma < 1$ (Cor. 3.2(ii))

Read-back — `esn_esp_of_spectral_condition`