Damping: closeness over a finite horizon forces closeness in weighted norm
ProvedBoydChua.weighted_of_finite_horizonOn the ball of radius M, agreement over a finite horizon already controls the whole weighted distance: given a tolerance, there is a horizon n₀, depending on the weight and the radius but not on the signals, such that any two signals of the ball agreeing to within that tolerance at every index up to n₀ are within the same tolerance in weighted norm.
This is the quantitative form of the discrete Lemma A1 of the source, and the only place where the assumption that the weight tends to zero is used. Its consequence is that on the ball the weighted topology and the topology of pointwise convergence coincide, which is what lets Tychonoff's theorem supply the compactness the approximation argument needs.
import Mathlib import Definitions.Def_BoydChua open Filter Topology MeasureTheory ReservoirESN BoydChua
namespace BoydChua
theorem weighted_of_finite_horizon {E : Type*} [NormedAddCommGroup E]
(M : ℝ) (hM : 0 < M) (w : ℕ → ℝ) (hw : IsWeighting w) (ε : ℝ) (hε : 0 < ε) :
∃ n₀ : ℕ, ∀ u v : ℕ → E, UnifBdd M u → UnifBdd M v →
(∀ k ≤ n₀, ‖u k - v k‖ ≤ ε) → WeightedBound w (fun k => u k - v k) ε := by sorry
end BoydChuaRead-back
What the Lean code literally says, in plain math · claude-opus-5
For every normed space, every positive radius M, every weighting w and every positive tolerance e, there exists one horizon n0, depending only on M, w, e and chosen before the inputs, such that: whenever two sequences both have all norms at most M, and they agree to within e at every index up to n0, then they satisfy the global weighted bound e at every index, including far beyond the horizon.
In words: on the M-ball, agreement to within e on a fixed finite initial window already forces agreement to within e in the weighted sup-seminorm. The same e serves as both the finite-horizon tolerance and the weighted conclusion; this is consistent because the weight being at most one handles the indices inside the window, while the weight tending to zero combined with the uniform bound 2M handles those outside. The hypothesis that the weight tends to zero is used here and nowhere else.
Confirmed by the mission captain (proposal self-audit).