Sequential compactness of uniformly bounded input sequences for a weighted norm
ProvedWeightedCompact.unifBdd_tendsto_subseqLet be a weighting sequence — positive, bounded by one, nonincreasing, and tending to zero — and let be a bound. Consider the set of input sequences uniformly bounded by , indexed so that denotes the instant 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:
This is sequential compactness of the space of uniformly bounded sequences for the weighted norm .
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 alone, the bound already forces the weighted difference below , 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 before the time index , 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 with chosen first, what follows for the supremum is , non-strictly; since is arbitrary this is equivalent to convergence in the weighted norm. No positivity is assumed of : for the hypothesis is unsatisfiable and the statement vacuous.
import Mathlib import Definitions.Def_ReservoirESN open Filter Topology Set ReservoirESN
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