The generating series of a bounded input separates inputs

Proved

PowerSep.exists_ne_zero_of_ne_zero

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

analysispower-seriesreservoir-computingseparation

Let $z$ be a real input sequence uniformly bounded by $M$ , indexed so that $j$ counts steps into the past, and form its generating series

f_z(x) \;=\; \sum_{j\ge 0} z_j\, x^j .

The series converges for $|x| < 1$ , since its terms are dominated by $M|x|^j$ . The theorem asserts that if $z$ is not the zero sequence, then $f_z$ does not vanish identically: there is a point $x$ with $|x| < 1$ at which $f_z(x) \ne 0$ .

Why this is the separation property. Two distinct bounded inputs have a nonzero difference, so their generating series differ at some point of the open unit interval. The map $z \mapsto f_z$ is therefore injective on uniformly bounded sequences, which is what "separating points" means for the family of functionals built from such series. Separation is one of the two hypotheses of the Stone-Weierstrass theorem, the other being that the family is an algebra containing the constants; it is what prevents a dense family from collapsing distinct inputs.

Formalization Note The source proves this through real analyticity, invoking the uniqueness of the Taylor expansion of a function represented by a convergent power series. The statement here is the same, but its proof is elementary: one isolates the first index at which $z$ does not vanish, factors that power of $x$ out, and chooses the evaluation point small enough that the remaining tail — bounded by $M|x|/(1-|x|)$ — stays below the first coefficient in absolute value. No analyticity, no differentiation, and no uniqueness theorem for power series is needed; only the geometric bound. The uniform bound is the platform predicate UnifBdd. The conclusion is an existence statement over the open interval, with no claim about where the nonvanishing point lies beyond $|x| < 1$ .

A further point on the Lean rendering: the sum is Lean's unconditional tsum, which takes the junk value $0$ on a non-summable family; the nonvanishing conclusion therefore carries summability at the witness implicitly. The hypothesis $z \ne 0$ is inequality in the function space, so it means that some coefficient is nonzero, not that all are. The bound $M$ appears only in the hypothesis and contributes nothing quantitative to the conclusion, which amounts to requiring that $z$ be bounded.

Preamble

import Mathlib
import Definitions.Def_ReservoirESN

open Filter ReservoirESN

Formal statement

namespace PowerSep

theorem exists_ne_zero_of_ne_zero {M : ℝ} {z : ℕ → ℝ} (hz : UnifBdd M z) (hne : z ≠ 0) :
    ∃ x : ℝ, |x| < 1 ∧ (∑' j, z j * x ^ j) ≠ 0 := by sorry

end PowerSep

Source

L. Grigoryeva, J.-P. Ortega, Universal discrete-time reservoir computers with stochastic inputs and linear readouts using non-homogeneous state-affine systems, Journal of Machine Learning Research 19(24) (2018), 1-40, https://arxiv.org/abs/1712.00754, Appendix, Lemma 6.2: the generating function of a bounded input is real analytic on (-1,1) and, when the input is nonzero, takes a nonzero value there.

View graph