Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Sequential compactness of uniformly bounded input sequences for a weighted norm

Proved
WeightedCompact.unifBdd_tendsto_subseq

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

compactnessfading-memoryfunctional-analysisreservoir-computing

Let w:N→(0,1]w : \mathbb{N} \to (0,1]w:N→(0,1] be a weighting sequence — positive, bounded by one, nonincreasing, and tending to zero — and let MMM be a bound. Consider the set of input sequences uniformly bounded by MMM, indexed so that kkk denotes the instant kkk steps into the past. Then from every sequence of such inputs one may extract a subsequence converging to another uniformly bounded input, uniformly in time once weighted:

∀ε>0, ∃I, ∀i≥I, ∀k:∣Zφ(i),k−zk∣ wk<ε.\forall \varepsilon > 0,\ \exists I,\ \forall i \ge I,\ \forall k : \quad \bigl| Z_{\varphi(i),k} - z_k \bigr| \, w_k < \varepsilon .∀ε>0, ∃I, ∀i≥I, ∀k:​Zφ(i),k​−zk​​wk​<ε.

This is sequential compactness of the space of uniformly bounded sequences for the weighted norm ∥z∥w=sup⁡k∣zk∣wk\lVert z \rVert_w = \sup_k |z_k| w_k∥z∥w​=supk​∣zk​∣wk​.

Why the weighting is essential. The same statement is false for the supremum norm: the space of uniformly bounded sequences is not compact for it, as the shifted unit vectors show. The weighting is what makes compactness available, by damping the tail: beyond a rank determined by www alone, the bound ∣Z−z∣≤2M|Z - z| \le 2M∣Z−z∣≤2M already forces the weighted difference below ε\varepsilonε, whatever the sequences do there. Only finitely many coordinates then remain, each converging pointwise.

Reuse value. Compactness of the input space for a weighted norm is the hypothesis under which approximation theorems for input/output systems are stated — it is what makes a Stone-Weierstrass argument available on a space of infinite input histories. It is used in the approximation theory of fading memory filters, and in the universality results for reservoir computing that rest on it.

Formalization Note The statement is the sequential form of compactness, expressed with an explicit extraction rather than through a metric space structure on the set of bounded sequences; this avoids having to equip that set with a norm before the result can be stated. Inputs are scalar. The uniform bound is the platform predicate UnifBdd, and the weighting sequence the platform predicate IsWeighting, both already published. The conclusion quantifies the rank III before the time index kkk, so the convergence is uniform in time, which is the content of convergence in the weighted norm rather than merely coordinatewise. Because the strict bound is asserted at each kkk with III chosen first, what follows for the supremum is sup⁡k∣Zφ(i),k−zk∣wk≤ε\sup_k |Z_{\varphi(i),k} - z_k| w_k \le \varepsilonsupk​∣Zφ(i),k​−zk​∣wk​≤ε, non-strictly; since ε\varepsilonε is arbitrary this is equivalent to convergence in the weighted norm. No positivity is assumed of MMM: for M<0M < 0M<0 the hypothesis is unsatisfiable and the statement vacuous.

Preamble
import Mathlib
import Definitions.Def_ReservoirESN

open Filter Topology Set ReservoirESN
Formal statement
namespace WeightedCompact

theorem unifBdd_tendsto_subseq
    (M : ℝ) (w : ℕ → ℝ) (hw : IsWeighting w)
    (Z : ℕ → ℕ → ℝ) (hZ : ∀ i, UnifBdd M (Z i)) :
    ∃ (z : ℕ → ℝ) (φ : ℕ → ℕ), UnifBdd M z ∧ StrictMono φ ∧
      ∀ ε > 0, ∃ I, ∀ i ≥ I, ∀ k, |Z (φ i) k - z k| * w k < ε := by sorry

end WeightedCompact
Source
L. Grigoryeva, J.-P. Ortega, Echo state networks are universal, Neural Networks 108 (2018), 495-508, https://arxiv.org/abs/1806.00797, p. 8, Corollary 2.8 (compactness of K_M for the weighted norm); see also Universal discrete-time reservoir computers ... non-homogeneous state-affine systems, JMLR 19(24) (2018), https://arxiv.org/abs/1712.00754, p. 6, Lemma 2.2.

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me