Lemma 1: the bounded slew-limited class is compact in weighted norm
ProvedBoydChua.slewBdd_tendsto_subseqLemma 1 of the source. The class of signals bounded in amplitude by M₁ and in slew rate by M₂ is sequentially compact for the weighted supremum norm: every sequence of such signals has a subsequence converging, in weighted norm, to a signal of the same class.
The source proves this by applying Arzela-Ascoli on each interval [-n, 0], where the amplitude bound gives uniform boundedness and the slew bound gives equicontinuity, then extracting a diagonal subsequence and using the decay of the weight to upgrade uniform convergence on compacts to convergence in weighted norm.
The slew bound cannot be dropped. In discrete time no analogue is needed — the source remarks on this explicitly — but in continuous time it is the equicontinuity that makes the class compact, and without it the approximation theorem fails.
import Mathlib import Definitions.Def_BoydChua open Filter Topology MeasureTheory ReservoirESN BoydChua
namespace BoydChua
theorem slewBdd_tendsto_subseq (M₁ M₂ : ℝ) (hM₁ : 0 < M₁) (hM₂ : 0 < M₂)
(w : ℝ → ℝ) (hw : IsWeightingC w)
(u : ℕ → ℝ → ℝ) (hu : ∀ n, SlewBdd M₁ M₂ (u n)) :
∃ (φ : ℕ → ℕ) (u₀ : ℝ → ℝ), StrictMono φ ∧ SlewBdd M₁ M₂ u₀ ∧
∀ ε > 0, ∀ᶠ k in atTop, WeightedBoundC w (fun t => u (φ k) t - u₀ t) ε := by sorry
end BoydChuaRead-back
What the Lean code literally says, in plain math · claude-opus-5
Given positive M1, M2, a weighting w, and a sequence of functions each bounded by M1 and Lipschitz with constant M2 on the non-negative half-line, there exist a strictly increasing extraction and a limit function, itself bounded by M1 and Lipschitz with constant M2 on that half-line, such that the extracted subsequence converges to the limit in the weighted seminorm: for every positive e, for all sufficiently large indices, the weighted bound e holds on the difference at every non-negative time.
The single extraction is required to work for all tolerances at once - it is quantified before the tolerance. This is sequential compactness of the slew-bounded class for the half-line weighted seminorm.
Nothing is asserted about any function at negative times, and the limit is unconstrained there; this was verified to be harmless, since both fields of the class and the weighted bound read only the non-negative half-line, so the limit may be set to zero on the negative one. The construction is Arzela-Ascoli on each bounded interval followed by a diagonal extraction; the non-strict bound and the Lipschitz constant pass to the pointwise limit, and the junction between the interval and its complement uses the weight being at most one on one side and tending to zero on the other.
Confirmed by the mission captain (proposal self-audit).