Machine Learning

Motivation

Lower bounds for stochastic multi-armed bandits are usually stated for a large horizon: Lai and Robbins (1985) and Burnetas and Katehakis (1996) show that a consistent strategy pulls a suboptimal arm at least about $\ln T / \mathcal{K}_{\inf}$ times. These bounds say nothing about the small-horizon regime, the first rounds in which a strategy has not yet had time to separate the arms. Garivier, Ménard and Stoltz (arXiv:1602.07182v3, Mathematics of Operations Research, 2019) describe that regime through one information-theoretic inequality, their (6), and derive several lower bounds from it. This mission formalizes their relative lower bound, Theorem 3 (p. 11): under a mild symmetry assumption on the strategy, a suboptimal arm is either pulled at the uniform rate $T/K$ or, on average, almost as often as an optimal arm. It is the statement behind the title's claim that bandit strategies must first explore.

Setting

There are $K$ arms. A bandit problem $\underline{\nu} = (\nu_1, \dots, \nu_K)$ assigns to each arm $a$ a probability distribution $\nu_a$ on $\mathbb{R}$ with expectation $\mu_a$. The optimal mean is $\mu^\star = \max_a \mu_a$, the gap of arm $a$ is $\Delta_a = \mu^\star - \mu_a$; arm $a$ is optimal if $\Delta_a = 0$ and suboptimal if $\Delta_a > 0$.

A model $\mathcal{D}$ is a set of distributions on $\mathbb{R}$, each with an expectation; a bandit problem is in $\mathcal{D}$ when every $\nu_a$ belongs to $\mathcal{D}$.

At each round $t$ a strategy $\psi$ picks an arm $A_t$, possibly at random, as a function of the past arms and rewards, and receives a reward $Y_t$ drawn from $\nu_{A_t}$. The number of pulls of arm $a$ in the first $T$ rounds is

$$N_{\psi,a}(T) = \sum_{t=1}^{T} \mathbb{1}\{A_t = a\},$$

and $\mathbb{E}_{\underline{\nu}}$ denotes expectation when $\psi$ plays against $\underline{\nu}$. Write $N^+_{\psi,a}(T) = \max\{N_{\psi,a}(T), 1\}$.

Kullback–Leibler divergence. $\mathrm{KL}(P, Q) \in [0, +\infty]$ is the Kullback–Leibler divergence between distributions, and $\mathrm{kl}(p, q)$ the divergence between Bernoulli laws of parameters $p$ and $q$.

Pairwise symmetry (Definition 3, p. 11). A strategy $\psi$ is pairwise symmetric for optimal arms on $\mathcal{D}$ if for every bandit problem $\underline{\nu}$ in $\mathcal{D}$, every pair of optimal arms $a^\star, a_\star$ with $\nu_{a^\star} = \nu_{a_\star}$ and every $T \ge 1$, the pairs $(N_{\psi,a^\star}(T), N_{\psi,a_\star}(T))$ and $(N_{\psi,a_\star}(T), N_{\psi,a^\star}(T))$ have the same distribution. A strategy that uses only the observed payoffs, and not the labels of the arms, has this property.

Formalization targets

Goal: Theorem 3 (p. 11)

For every model $\mathcal{D}$, every strategy $\psi$ pairwise symmetric for optimal arms on $\mathcal{D}$, every bandit problem $\underline{\nu}$ in $\mathcal{D}$, every suboptimal arm $a$, every optimal arm $a^\star$ with $\mathrm{KL}(\nu_a, \nu_{a^\star}) < \infty$ and every $T \ge 1$,

$$\mathbb{E}_{\underline{\nu}}\big[N_{\psi,a}(T)\big] \ge \frac{T}{K} \quad\text{or}\quad \mathbb{E}_{\underline{\nu}}\left[\frac{N^+_{\psi,a}(T)}{N^+_{\psi,a^\star}(T)}\right] \ge 1 - 2\sqrt{\frac{2T\,\mathrm{KL}(\nu_a, \nu_{a^\star})}{K}} .$$

Companion: the "in particular" clause

For $T \le K / (32\,\mathrm{KL}(\nu_a, \nu_{a^\star}))$ the second alternative becomes $\mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}(T)/N^+_{\psi,a^\star}(T)] \ge 1/2$.

Milestones (p. 12)

1. The symmetry identity: for the alternative problem $\underline{\nu}'$ obtained by replacing $\nu_a$ by $\nu_{a^\star}$, $\mathbb{E}_{\underline{\nu}'}[N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})] = 1/2$.
2. Inequality (12): $\mathbb{E}_{\underline{\nu}}[N_{\psi,a}(T)]\,\mathrm{KL}(\nu_a, \nu'_a) \ge \mathrm{kl}\big(\mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})], 1/2\big)$.
3. The Jensen display: $\mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})] \le r/(1+r)$ with $r = \mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}/N^+_{\psi,a^\star}]$.
4. The bound $r/(1+r) \ge 1/2 - \sqrt{T\,\mathrm{KL}(\nu_a,\nu'_a)/(2K)}$ in the case $\mathbb{E}_{\underline{\nu}}[N_{\psi,a}(T)] \le T/K$, $r \le 1$.

Significance

The theorem shows that in the initial phase a symmetric strategy cannot discard a suboptimal arm quickly: unless the arm is already sampled at the uniform rate, it is sampled, in ratio, nearly as often as an optimal arm, as long as $T$ is small compared with $K / \mathrm{KL}(\nu_a, \nu_{a^\star})$. Together with Theorem 2 (absolute lower bound) and Theorem 4 (collective lower bound) it describes the regret curve before the logarithmic regime: roughly linear growth, then a transition. It requires no assumption on the model beyond the existence of expectations, and it involves the divergence between the two arms themselves rather than the model-dependent quantity $\mathcal{K}_{\inf}$.

The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a Lean statement of Theorem 3 on the canonical bandit model already used on the platform (StochasticBandit, BanditPolicy), a formal version of the symmetry assumption that sibling missions reuse (mission V, the collective lower bound, uses the same Definition 3), and the four intermediate steps of the proof as separate targets.

Difficulty

The proof compares $\underline{\nu}$ with an alternative problem $\underline{\nu}'$ that differs from it only in arm $a$, and transfers information between them through the fundamental inequality (6) of §2, a data-processing argument on the law of the whole history. The step specific to Theorem 3 is the choice of the test variable: the expectation of $N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})$ is known exactly under $\underline{\nu}'$ only because the strategy is pairwise symmetric, and the symmetry is a statement about joint laws of pull counts, not about their expectations. A version of the assumption that only equates expected pull counts does not determine the expectation of this ratio. The ratio expectation then has to be extracted from a bound on $\mathbb{E}[x/(1+x)]$, which needs Jensen's inequality in the right direction and a case split on whether $r \le 1$.

Formalization scope

Arms are Fin K (0-based). The horizon $T$ is a natural number. A strategy is a published BanditPolicy: a family of Markov kernels from the observed history of (arm, reward) pairs to the next arm. Every strategy of the paper, which may use auxiliary uniform random variables, induces such a kernel with the same law of arms and rewards. The law of the history is the published banditMeasure, and $N_{\psi,a}(T)$ is the published armPullCount. The model is a set of measures on $\mathbb{R}$, and every statement assumes the paper's standing hypothesis (§1.1, p. 3) that each member is a probability measure with an integrable identity, together with $\underline{\nu}$ in $\mathcal{D}$.

Committed conventions:

• $\mathrm{KL}$ and $\mathrm{kl}$ take values in $[0, +\infty]$; the Bernoulli divergence is the Kullback–Leibler divergence of two Bernoulli laws on $\mathbb{R}$, not a real formula with finite values at $q \in \{0, 1\}$.
• Theorem 3 adds the hypothesis $\mathrm{KL}(\nu_a, \nu_{a^\star}) < \infty$. When the divergence is infinite the paper's bound reads $\ge -\infty$ and is empty; reading $+\infty$ as the real number $0$ would make the statement false.
• The "in particular" clause is stated as $32\,T\,\mathrm{KL}(\nu_a,\nu_{a^\star}) \le K$ in $[0, +\infty]$, which needs no finiteness assumption.
• Definition 3 is an equality of joint laws (push-forwards of the history law), for every $T \ge 1$, only for optimal arms of problems in $\mathcal{D}$ with equal distributions. Invariance under all permutations of the arms would strengthen the hypothesis and weaken the theorem.
• Ratios use $\max\{N, 1\}$ as real numbers, so no division by zero occurs; all integrands are bounded by $T$.

A formalization in which the symmetry assumption equates only expected pull counts, in which the divergence is a real number with junk value $0$ at $+\infty$, or in which the disjunction is replaced by its second alternative, is not this theorem.

The mission builds on the published definitions StochasticBandit and BanditPolicy. A complete development needs the fundamental inequality (6) for kernel policies (the divergence decomposition, published as BanditAlgorithm.bandit_divergence_decomposition, plus data processing for the Bernoulli test), Pinsker's inequality for Bernoulli laws (proved on the platform as BanditAlgorithm.bernoulli_relative_entropy_pinsker), Jensen's inequality for concave functions (Mathlib), and a lemma that the law of the history is unchanged in distribution when two identically distributed optimal arms are relabelled. The measurability of pull counts and the relation between the extended-real and real Bernoulli divergences are reusable beyond this mission. Proofs of any milestone, and of the general fundamental inequality, are welcome.

Selected references

• A. Garivier, P. Ménard, G. Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research 44(2), 2019. arXiv:1602.07182v3, doi:10.1287/moor.2017.0928
• T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6(1), 1985. doi:10.1016/0196-8858(85)90002-8
• A. N. Burnetas, M. N. Katehakis, Optimal adaptive policies for sequential allocation problems, Advances in Applied Mathematics 17(2), 1996. doi:10.1006/aama.1996.0007
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. doi:10.1017/9781108571401

Motivation

Reservoir computing learns an input/output system from data in two stages. A dynamical system, the reservoir, is driven by the input sequence and its state is recorded; then only a linear readout of that state is trained, by least squares. The echo state network (ESN) is the most widely used reservoir: its state evolves by $x_t = \sigma(Ax_{t-1} + Cz_t + \zeta)$, with the matrices $A, C$ and the vector $\zeta$ drawn at random and never trained. ESNs predict chaotic systems well in practice (Jaeger & Haas, Science 2004), and they are known to be universal: for every fading-memory input/output map some ESN approximates it (Grigoryeva & Ortega, Neural Netw. 2018). Universality does not explain the practice, where the reservoir weights are random and fixed in advance. Gonon, Grigoryeva & Ortega (Ann. Appl. Probab. 2023) prove that an ESN whose weights are drawn from an explicit distribution that does not depend on the target approximates every sufficiently regular target, with an explicit $L^2$ error bound. This mission formalizes that result, Theorem 2, and the chain of results its proof rests on.

Setting

Time runs over $\mathbb Z_- = \{0, -1, -2, \dots\}$. Inputs take values in a set $D_d$ with $0 \in D_d \subset B_M \subset \mathbb R^d$, where $B_M$ is the closed Euclidean ball of radius $M > 0$. The input $Z = (Z_t)_{t \in \mathbb Z_-}$ is a $D_d$-valued process with law $\mu_Z$. The target is a functional $H^* : (D_d)^{\mathbb Z_-} \to \mathbb R$, the present output as a function of the whole input history. All norms are Euclidean.

Regularity. Fix weights $w_{-i} > 0$ with $\sum_i i\, w_{-i} < \infty$. $H^*$ is $w$-Lipschitz with constant $L > 0$ if $|H^*(u) - H^*(v)| \le L\sum_{i \ge 0} w_{-i}\|u_{-i} - v_{-i}\|$. Assumption 1 asks, in addition, for every $T \ge 1$: with $q = d(T+1)$, the truncation $H^*_T(z_0, \dots, z_{-T}) = H^*(\dots, 0, z_{-T}, \dots, z_0)$ has a Fourier representation $H^*_T(u) = \int_{\mathbb R^q} e^{i\langle w, u\rangle} g_T(w)\,dw$ on $(D_d)^{T+1}$, with $g_T \in L^1$ and $\int \max(1, \|w\|^3)|g_T(w)|^2\,dw < \infty$.

The random ESN. Fix $T, N \ge 1$, $R > 0$, and a bound $M_T$ with $\|(Z_0, \dots, Z_{-T})\| \le M_T$ almost surely. Draw $A_1, \dots, A_N$ i.i.d. uniform on $B_R \subset \mathbb R^q$ and, independently, $\zeta_1, \dots, \zeta_N$ i.i.d. uniform on $[-\max(M_TR,1), \max(M_TR,1)]$. With $S$ the block shift on $\mathbb R^q$ and $c$ the embedding of $\mathbb R^d$ into the first block, and $a$ the matrix with rows $A_i^\top$, put

$$\bar A = \begin{pmatrix} S & 0\\ aS & 0\end{pmatrix},\quad \bar C = \begin{pmatrix} c\\ ac\end{pmatrix},\quad \bar\zeta = \begin{pmatrix} 0\\ \zeta\end{pmatrix},\quad A = \begin{pmatrix}\bar A & -\bar A\\ -\bar A & \bar A\end{pmatrix},\quad C = \begin{pmatrix}\bar C\\ -\bar C\end{pmatrix},\quad \zeta = \begin{pmatrix}\bar\zeta\\ -\bar\zeta\end{pmatrix}.$$

The ESN is $X_t = \sigma(AX_{t-1} + CZ_t + \zeta)$, $Y_t = WX_t$, with $\sigma(x) = \max(x, 0)$ and state space $\mathbb R^{2(N+d(T+1))}$.

Formalization targets

Goal: Theorem 2 (p. 54)

For every $H^*$ satisfying Assumption 1 there is a readout $W$, a function of the random weights alone, such that the ESN has the echo state property (a unique state sequence for every input) and

$$\mathbb E\big[|Y_0 - H^*(Z)|^2\big]^{1/2} \le \frac{\sqrt{C_{T,R}}}{\sqrt N} + \int_{\mathbb R^q \setminus B_R}|g_T(u)|\,du + LM\sum_{i > T} w_{-i},$$

with $C_{T,R} = 16\max(M_TR,1)\mathrm{Vol}_q(B_R)(M_T+1)^2(M_T^3+M_T+16)\int_{B_R}\max(1,\|u\|^3)|g_T(u)|^2\,du$.

Milestones

1. (8), p. 33: a scalar identity expressing $e^{iz} - iz - 1$ as an integral of ReLU ramps.
2. Proposition 2, pp. 31–32: under a Fourier condition, $f$ is an integral of ReLU ridge functions with a compactly supported, square-integrable weight $\pi$.
3. Proposition 3, pp. 41–42: a static ReLU network with uniformly sampled inner weights achieves mean-square error $C^*/N$.
4. Corollary 1, p. 43: the same with a dimension-free integrability condition and a truncation term.
5. Remark 10, p. 53: the shift reservoir is nilpotent, has $K = I$ and stores the last $T+1$ inputs.
6. Proposition 6, p. 51: a linear reservoir with a random ReLU readout satisfies the bound (54).
7. (64)–(66), pp. 55–56: every solution of the ESN reduces to the linear shift reservoir, which gives uniqueness.

Significance

Theorem 2 is the first approximation bound for echo state networks whose recurrent and input weights are sampled from a generic distribution rather than constructed from the target. The bound separates three error sources: a Monte Carlo term decaying like $N^{-1/2}$, a truncation term in the sampling radius $R$, and a memory term in the window length $T$. Because the readout can be taken to be the least-squares readout, the bound also controls the trained networks used in practice, and it is the input to the paper's rate and universality corollaries (Corollaries 4 and 5).

Status: the result is proved on paper. No part of it is formalized; the only reservoir-computing material on the platform is the published definition ReservoirESN (the state equation), which this mission reuses. A formal proof would supply the first machine-checked random-feature approximation bound with explicit constants.

Difficulty

The obvious argument fails in two places. First, the classical integral representations of Barron type place the inner weights on unbounded sets, which cannot be sampled uniformly; Proposition 2 needs a change of variables that makes the weight compactly supported while keeping it square integrable, and this costs the factor $R^{-(2q+2)}$ and the condition (5). Second, a ReLU network is not contractive, so the echo state property of the ESN cannot be taken from the standard contraction criterion; it has to be derived from the block structure of $A$, which makes the difference of the two state halves follow a nilpotent linear recursion.

Formalization scope

$\mathbb R^q$ is EuclideanSpace ℝ (Fin (T+1) × Fin d), block $k$ holding $z_{-k}$; input sequences are ℕ → EuclideanSpace ℝ (Fin d) with index $k = -t$, and $x_t = F(x_{t-1}, z_t)$ is the published ReservoirESN.IsSolution. Points of $\mathbb R^{q+1}$ are pairs with norm $(\|w\|^2 + u^2)^{1/2}$. The uniform laws are Lebesgue measure conditioned on the ball or interval; $N$ i.i.d. rows have the product law. The input is independent of the weights (§4.1) and $D_d$-valued with $0 \in D_d \subset B_M$ (§5.1): expectations are iterated lower Lebesgue integrals over $\mu_Z$ and the product law, and probability-$(1-\delta)$ statements bound the product measure of the bad set. The scalar output case $m = 1$ is used, as in the paper. Assumption 1 is required for every $T \ge 1$, as printed.

A readout allowed to depend on the input would make every bound trivial; in every statement the readout is a measurable function of the inner weights alone.

Departures from the print, each disclosed in the item: the last term of Proposition 6 is the $L^2(\mu_Z)$ norm of $\|K^{-1}S^{T+1}X_{-T-1}\|$, which the page prints outside the expectation; the state space of the linear reservoir (52) is a parameter $D_N$, as in §2.1, and its solution is assumed to be a random process; Proposition 3 omits "$C^* > 0$" (the explicit value (33) is used); measurability of the Fourier density $g$ is stated where the page leaves it implicit.

A complete development needs Fourier integrals on Euclidean spaces, change of variables under linear maps, product measures and Fubini–Tonelli, and an importance-sampling variance bound. The static results (Propositions 2, 3, Corollary 1) are reusable for random-feature models beyond reservoir computing. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

• L. Gonon, L. Grigoryeva, J.-P. Ortega, Approximation bounds for random neural networks and reservoir systems, Ann. Appl. Probab. 33(1), 28–69, 2023. https://doi.org/10.1214/22-AAP1806
• L. Grigoryeva, J.-P. Ortega, Echo state networks are universal, Neural Netw. 108, 495–508, 2018. https://doi.org/10.1016/j.neunet.2018.08.025
• H. Jaeger, H. Haas, Harnessing nonlinearity: predicting chaotic systems and saving energy in wireless communication, Science 304, 78–80, 2004. https://doi.org/10.1126/science.1091277
• A. R. Barron, Universal approximation bounds for superpositions of a sigmoidal function, IEEE Trans. Inf. Theory 39, 930–945, 1993. https://doi.org/10.1109/18.256500
• J. M. Klusowski, A. R. Barron, Approximation by combinations of ReLU and squared ReLU ridge functions with ℓ1 and ℓ0 controls, IEEE Trans. Inf. Theory 64, 7649–7656, 2018. https://doi.org/10.1109/tit.2018.2874447
• C. Cuchiero, L. Gonon, L. Grigoryeva, J.-P. Ortega, J. Teichmann, Discrete-time signatures and randomness in reservoir computing, IEEE Trans. Neural Netw. Learn. Syst., 2021. https://doi.org/10.1109/TNNLS.2021.3076777

Motivation

Bilevel optimization asks for an outer decision while an inner optimization problem responds to that decision. In hyperparameter selection, for example, the outer objective evaluates a model whose parameters are chosen by a training problem. A two-timescale algorithm updates both levels in one stochastic loop, so its outer step uses an inner solution that has not yet settled. The resulting error bound must account for both the outer decision and the inner tracking error. Hong, Wai, Wang and Yang study this setting and give finite-time bounds for their two-timescale stochastic approximation (TTSA) algorithm in the strongly convex outer case Hong et al., arXiv:2007.05170v4, §§1–3.

The paper states its main rates using $\lesssim$, with numerical constants omitted. Appendix A gives explicit bounds for the two errors. This mission targets those displayed bounds, retaining their constants and the actual stochastic update. The selected source is the arXiv v4 preprint: page numbers and theorem labels below refer to that version Hong et al., Theorem 1 and App. A.

Setting

Let $X\subseteq\mathbb R^{d_1}$ be closed and convex. For an outer point $x\in X$, the inner solution $y^\star(x)\in\mathbb R^{d_2}$ minimizes $g(x,\cdot)$. The outer objective is $\ell(x)=f(x,y^\star(x))$, and $x^\star\in X$ is an optimal outer point. The inner objective is strongly convex in $y$, which gives a unique inner minimizer. The paper’s derivative and Lipschitz assumptions control how that minimizer and the outer gradient change as $x$ and $y$ move Hong et al., Assumptions 1–2, pp. 5–6.

The algorithm keeps iterates $x^k\in X$ and $y^k\in\mathbb R^{d_2}$. With deterministic step sizes $\alpha_k,\beta_k$ and stochastic estimates $h_f^k,h_g^k$, it updates

$$y^{k+1}=y^k-\beta_k h_g^k,\qquad x^{k+1}=P_X(x^k-\alpha_k h_f^k),$$

where $P_X$ is the Euclidean nearest-point projection onto $X$. The inner estimate targets $\nabla_y g(x^k,y^k)$. The outer estimate targets the surrogate gradient

$$\bar\nabla_xf(x,y)=\nabla_xf(x,y)-\nabla^2_{xy}g(x,y) [\nabla^2_{yy}g(x,y)]^{-1}\nabla_yf(x,y),$$

with a bias bounded by $b_k$. Assumption 3 bounds the conditional variances given the histories $\mathcal F_k$ and $\mathcal F'_k$. The surrogate at $y^\star(x)$ is the paper’s $\nabla\ell(x)$ Hong et al., Algorithm 1, (5)–(7c), p. 6.

The two quantities being bounded are the outer error $\Delta_x^k=\mathbb E\|x^k-x^\star\|^2$ and inner tracking error $\Delta_y^k=\mathbb E\|y^k-y^\star(x^{k-1})\|^2$. At $k=0$, the convention is $x^{-1}=x^0$. The constants $L$ and $L_y$ are the exact functions of the derivative bounds in (13); $\widetilde\sigma_f^2=\sigma_f^2+3\sup_{x\in X}\|\nabla\ell(x)\|^2$ is finite by the paper’s standing assumption after (14). The products $G^{(1)}_{m:n}$ and $G^{(2)}_{m:n}$ are those of (48) Hong et al., pp. 8–9, 20.

Formalization targets

The first target is the explicit inner bound (55): for every $k\ge0$,

$$\Delta_y^{k+1}\le G^{(1)}_{0:k}\Delta_y^0+C_y^{(1)}\beta_k, \qquad C_y^{(1)}=\frac8{\mu_g}\left\{\sigma_g^2+ \frac{4c_0^2L_y^2}{\mu_g}(\widetilde\sigma_f^2+3b_0^2)\right\}.$$

The goal also includes the explicit outer bound displayed after (59):

$$\begin{aligned} \Delta_x^{k+1}\le{}&G^{(2)}_{0:k} \left\{\Delta_x^0+\left[\frac{2L^2}{\mu_\ell^2} +\frac{3\alpha_0L^2}{\mu_\ell}\right]\Delta_y^0\right\}\\ &+\frac2{\mu_\ell}\left[\frac{2\widetilde c_b}{\mu_\ell} +\widetilde\sigma_f^2+3b_0^2\right]\alpha_k\\ &+\frac{2c_1}{\mu_\ell}\left[\frac{2L^2}{\mu_\ell}+3\alpha_0L^2\right] C_y^{(1)}\alpha_k^{2/3}. \end{aligned}$$

These formulas use the paper’s step-size conditions (20a)–(20b), the bias condition $b_k^2\le\widetilde c_b\alpha_{k+1}$, and a positive outer modulus $\mu_\ell$. The milestones are the source’s Lemma 2 (12a), (14), (50), Lemma 10, (55), Lemma 11 and Lemma 4 (29). They supply independently stated targets for the two error quantities and the deterministic product estimates Hong et al., pp. 7–8, 13, 20–22, 34.

Significance

The bounds separate the effect of initialization from persistent stochastic error. Each $G$ product carries an initial-error term, while the remaining terms show how the current step sizes, variance and bias govern the residual error. This makes the dependencies on $L$, $L_y$, the strong convexity moduli and the estimator variances explicit, rather than hiding them in rate notation. The paper uses this strongly convex case as one part of its broader complexity analysis Hong et al., §3, Table 1.

The source proves the claimed rates on paper; this local development currently provides compiled Lean statements with open proofs. Completing it would add reusable formal interfaces for conditional stochastic-gradient assumptions, a moving strongly convex minimizer, and weighted products of varying contraction factors. The local mission does not claim a machine-checked proof of Theorem 1 yet.

Difficulty

The outer estimate depends on $y^{k+1}$, while the inner tracking error is measured against the minimizer at the preceding outer iterate. Treating the outer estimate as an ordinary unbiased gradient at $x^k$ loses both the surrogate-gradient discrepancy and the bias. A distance contraction for the inner step alone also does not settle the outer error, because the target $y^\star(x^k)$ moves with $x^k$. The assumptions must keep the two histories and their conditional estimates distinct Hong et al., (7a)–(7c), (17), App. A.

Formalization scope

Lean represents both spaces by EuclideanSpace ℝ (Fin d) with $d_1,d_2\ge1$, and Hessian blocks by continuous linear maps with operator norm. The mixed block maps inner directions to outer directions. The inner solution map is required to minimize $g(x,\cdot)$ on every $x\in X$; the projection is characterized as a nearest-point map on the closed convex set. These clauses prevent an arbitrary solution map or arbitrary outer update from satisfying the theorem. The $\nabla\ell$ used in (2) is defined by the displayed surrogate formula (5), so boundary points of $X$ have the same meaning as in the source.

The run starts at deterministic $(x^0,y^0)$ and uses measurable estimates with integrable squared norms. Conditional expectations are almost-sure statements relative to the sigma-algebras generated by the iterates, and $\Delta_x,\Delta_y$ are Bochner integrals. These regularity assumptions prevent totalized conditional expectation or integral operations from giving spurious zero values. The supremum defining $\widetilde\sigma_f^2$ is taken over $X$ and has an explicit bounded-above hypothesis; $X$ is nonempty because $x^0\in X$. The goal uses positive, nonincreasing step sizes, in line with the ratio conditions and the auxiliary lemmas. The paper prints $3/4$ in the $\alpha$ ratio of (20a), while its application of Lemma 10 with $q=2$ needs $1/2$; the stronger ratio is disclosed in the Lean hypotheses. The initial error uses $x^{-1}=x^0$, and real exponents use nonnegative bases.

The definition file and the seven milestone theorems are open for proof contributions. Theorem 1’s two explicit bounds are the mission goal. Lemma 3 (28) is excluded because its printed product uses a $1/2$ factor where (55) uses $1/4$; (55) is the selected inner target Hong et al., pp. 13, 21.

Selected references

• M. Hong, H.-T. Wai, Z. Wang and Z. Yang, A Two-Timescale Stochastic Algorithm Framework for Bilevel Optimization: Complexity Analysis and Application to Actor-Critic, SIAM Journal on Optimization, 2023; arXiv preprint v4, 2022. arXiv:2007.05170v4.

Why this lower bound matters

In a stochastic multi-armed bandit, a player repeatedly chooses one of finitely many arms and sees only the reward from the chosen arm. To earn a high reward, the player must favor arms that appear best. Yet an arm that currently appears inferior might be best under another plausible reward law. That uncertainty forces any strategy with uniformly strong long-run performance to keep testing apparently inferior arms. The asymptotic number of tests is a basic benchmark for comparing bandit algorithms: an algorithm that matches the bound uses no more exploration than the information in the model demands. Garivier, Ménard, and Stoltz restate this general benchmark as Theorem 1 and derive it within their analysis of the shape of regret Garivier–Ménard–Stoltz, §2.2.

The quantity controlling the benchmark comes from Burnetas and Katehakis. It measures the least information needed to replace one suboptimal arm by a plausible arm that is strictly better than the current best. The paper cites their quantity on page 4, and its Theorem 1 applies it to every suboptimal arm separately Garivier–Ménard–Stoltz, pp. 4, 9. This per-arm form matters when different arms have different reward laws and different amounts of information are needed to rule them out.

Bandit setting and notation

A bandit problem $\underline\nu=(\nu_a)_{a=1}^K$ has $K$ arms. Each $\nu_a$ is a probability distribution on real rewards with a finite expectation $\mu_a=\mathbb E_{\nu_a}X$. A strategy $\psi$ chooses an arm at each round using the preceding chosen arms and observed rewards, and it may randomize. Let $N_{\psi,a}(T)$ be the number of times arm $a$ is chosen in the first $T$ rounds. The optimal mean is $\mu^\star=\max_a\mu_a$, and the gap of arm $a$ is $\Delta_a=\mu^\star-\mu_a$. An arm is suboptimal when $\Delta_a>0$. These are the objects of §1.1 of the paper Garivier–Ménard–Stoltz, pp. 2–3.

A model $\mathcal D$ is a collection of possible real-valued reward distributions, each with a finite expectation. A bandit problem belongs to $\mathcal D$ when every one of its arm laws does. The Kullback–Leibler divergence $\mathrm{KL}(P,Q)$ measures the information discrepancy from one reward law $P$ to another $Q$; it may be infinite. For an arm law $P$ and a real threshold $x$, define the minimal information cost

$$\mathcal K_{\inf}(P,x,\mathcal D) =\inf\{\mathrm{KL}(P,Q):Q\in\mathcal D,\ \mathbb E_QX>x\}.$$

The infimum is $+\infty$ if there is no qualifying alternative. The strict inequality in the set matters: the replacement law must make the arm better than the original optimal mean, not merely tied with it Garivier–Ménard–Stoltz, p. 4.

Definition 1 calls $\psi$ uniformly fast convergent on $\mathcal D$ when, on every bandit problem in the model, the expected draw count of every suboptimal arm grows more slowly than $T^\alpha$ for each $0<\alpha\le1$:

$$\mathbb E_{\underline\nu}N_{\psi,a}(T)=o(T^\alpha).$$

Here $T$ tends to infinity through integer horizons. This condition is uniform in which problem and suboptimal arm are considered; it does not mean one numerical convergence rate is shared by all problems Garivier–Ménard–Stoltz, p. 9, Definition 1.

Formalization target

The goal is the paper's Theorem 1: for every model $\mathcal D$, every uniformly fast convergent strategy $\psi$, every bandit problem $\underline\nu$ in the model, and every suboptimal arm $a$,

$$\liminf_{T\to\infty} \frac{\mathbb E_{\underline\nu}N_{\psi,a}(T)}{\ln T} \ge\frac1{\mathcal K_{\inf}(\nu_a,\mu^\star,\mathcal D)}.$$

The bound states the minimum logarithmic exploration of each arm. It leaves the model and strategy arbitrary within the stated class. The milestones follow four statements from the proof on page 9: the Bernoulli entropy estimate in (11), the one-arm divergence chain in (10), the eventual bound on draws of the alternative's other arms, and the bound for one alternative law before taking the infimum. Their source text is recorded beside the local drafts Garivier–Ménard–Stoltz, p. 9.

What the result gives

If $\mathcal K_{\inf}$ is finite and positive, the theorem gives a concrete coefficient of $\ln T$ that any uniformly fast convergent strategy must spend on arm $a$. A small information cost means that the arm is hard to distinguish from a better alternative and must be sampled more often. If the cost is infinite because the model contains no better replacement, the reciprocal is zero and the bound makes no positive demand. If the cost is zero, the reciprocal is infinite: the normalized expected draw count must diverge. The extended-value convention is part of the target, not a choice of a finite stand-in Garivier–Ménard–Stoltz, pp. 4, 9.

The theorem is proved in the paper, while the Lean statements in this proposal are proof targets. A completed development would supply a machine-checked bridge from the canonical stochastic-bandit policy model through Bernoulli relative entropy and change of measure to the per-arm asymptotic claim. Its model and divergence definitions can also support lower bounds for other bandit classes. The existing Prove2Me StochasticBandit, BanditPolicy, and ConsistentBanditPolicy definitions provide the bandit law, policy, draw count, means, and $\mathcal K_{\inf}$ used here; Definition 1's exact strategy class is supplied locally.

Difficulty

The central issue is the quantification over every alternative law in an arbitrary model. A suboptimal arm may become uniquely optimal after changing only its law, while the strategy must remain uniformly fast on that new problem. The information cost is an infimum over such changes, including an empty set or costs arbitrarily close to zero. A statement that reasons about just one convenient alternative does not yield the coefficient in Theorem 1. The proof also passes from finite-horizon information inequalities to a liminf as $T$ grows, so endpoint values of Bernoulli divergence and the extended-value arithmetic must agree with the source Garivier–Ménard–Stoltz, pp. 6, 9.

Formalization scope

Lean indexes the paper's arms $1,\ldots,K$ by Fin K, starting at zero, and uses natural-number horizons. A strategy is a history-dependent Markov kernel, whose generated probability measure describes the sequence of chosen arms and rewards. The pull count is bounded by $T$, so its expectation is a genuine Bochner integral. The model explicitly requires probability laws with integrable identity; this ensures that each mean in $\mathcal K_{\inf}$ is genuine. Bernoulli relative entropy and arm-law KL take values in extended nonnegative reals. The goal's liminf is also in extended nonnegative reals, avoiding a default real liminf for an unbounded sequence. The first two horizons, where $\ln T\le0$, cannot affect an asymptotic liminf.

The theorem sentence on page 9 says “all bandit problems” without restricting the original problem to $\mathcal D$. Its proof applies Definition 1 to that problem, so the proposal states that its arms belong to $\mathcal D$. Without this condition a strategy can behave arbitrarily outside the model. The source's other standing conventions are kept: every reward law has an expectation, the improvement condition in $\mathcal K_{\inf}$ is strict, and uniform fast convergence ranges over all model problems, all suboptimal arms, and all $0<\alpha\le1$. These choices rule out an empty strategy class or a special hard-coded bandit as a trivial route to the target.

Useful contributions include the finite-horizon change-of-measure inequality, endpoint-correct Bernoulli KL estimates, identities for sums of expected pull counts, and asymptotic lemmas for reciprocal infima. The milestone drafts identify the paper statements those contributions must support.

Selected references

• Aurélien Garivier, Pierre Ménard, and Gilles Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research, 2019; cited here from arXiv:1602.07182v3, §§1–2.
• Apostolos N. Burnetas and Michael N. Katehakis, Optimal Adaptive Policies for Sequential Allocation Problems, Advances in Applied Mathematics, 1996. DOI:10.1006/aama.1996.0007.

Why a lower bound on the DEC for linear bandits

In a linear bandit a learner repeatedly chooses a decision $\pi$ from a set $\Pi \subseteq \mathbb{R}^d$ and observes a noisy reward whose mean is $\langle \theta^\star, \pi\rangle$ for an unknown parameter $\theta^\star$. It is the standard model for sequential decisions with many correlated actions, such as ad placement, routing and recommendation, and its minimax regret over $T$ rounds is known to scale as $d\sqrt{T}$ up to logarithmic factors (Dani, Hayes and Kakade, COLT 2008; see Lattimore and Szepesvári, 2020, Ch. 19–24).

Foster, Kakade, Qian and Rakhlin (2021) introduce the Decision-Estimation Coefficient (DEC), a single complexity measure that yields both upper and lower bounds on the regret of every interactive decision problem. A complexity measure of this kind is only useful if it is tight on the classical examples. Proposition 6.2 of that paper checks this for linear bandits on the Euclidean unit ball: the localized DEC is at least of order $d/\gamma$, which, through the paper's general lower bound (Theorem 3.2), gives the regret lower bound $\Omega(\sqrt{dT})$. Proposition 6.8 gives the analogous statement for linear bandits whose models have a fixed gap $\Delta$.

Setting

Let $\mathbb{B}^d = \{v \in \mathbb{R}^d : \|v\|_2 \le 1\}$ be the closed Euclidean unit ball. It is both the decision space $\Pi$ and the parameter set $\Theta$. A model with parameter $\theta \in \Theta$ returns, at decision $\pi$, an outcome in $\{-1, +1\}$ drawn from the Rademacher distribution $\mathrm{Rad}(\langle\theta,\pi\rangle)$, which puts mass $(1+\mu)/2$ on $+1$ and $(1-\mu)/2$ on $-1$ when its mean is $\mu$. The mean reward is $f^\theta(\pi) = \langle \theta, \pi\rangle$.

A maximizer selector $\theta \mapsto \pi_\theta$ picks a decision with $\langle\theta,\pi\rangle \le \langle\theta,\pi_\theta\rangle$ for all $\pi$. The regret of a decision is $g^\theta(\pi) = f^\theta(\pi_\theta) - f^\theta(\pi)$. Two outcome laws are compared by the squared Hellinger distance $D^2_{\mathrm{H}}(P,Q) = \sum_y (\sqrt{P(y)}-\sqrt{Q(y)})^2$.

Given a reference model $\overline{M}$, the $L_\infty$-localized class at radius $\varepsilon$ is

$$\mathcal{M}^\infty_\varepsilon(\overline{M}) = \{ M \in \mathcal{M} : |g^M(\pi) - g^{\overline{M}}(\pi)| \le \varepsilon \ \ \forall \pi \in \Pi \},$$

and the DEC at scale $\gamma > 0$ is

$$\mathsf{dec}_\gamma(\mathcal{M}', \overline{M}) = \inf_{p \in \Delta(\Pi)} \sup_{M \in \mathcal{M}'} \mathbb{E}_{\pi\sim p}\bigl[ g^M(\pi) - \gamma\, D^2_{\mathrm{H}}(M(\pi), \overline{M}(\pi)) \bigr],$$

the infimum running over all Borel probability measures $p$ on $\Pi$.

Formalization targets

Goal: Proposition 6.2

For all $d \ge 4$ and $\gamma \ge 2d/3$ there is $\overline{M} \in \mathcal{M}$ with

$$\mathsf{dec}_\gamma\bigl(\mathcal{M}^\infty_{\varepsilon_\gamma}(\overline{M}), \overline{M}\bigr) \ge \frac{d}{12\gamma}, \qquad \varepsilon_\gamma = \frac{2d}{3\gamma}.$$

The page prints $\varepsilon_\gamma = d/(3\gamma)$. The hard family of its proof has regret functions $\Delta(1-\pi_i)$, which reach $2\Delta$ at $\pi = -e_i$ while the reference regret is identically $0$, so the family lies in the class of radius $2\Delta$ and not in the class of radius $\Delta$. The goal is stated at the radius the proof supports.

Milestones

1. Lemma A.8: $D^2_{\mathrm{H}}(\mathrm{Rad}(\mu), \mathrm{Rad}(0)) \le \tfrac34\mu^2$ on $[-1,1]$, together with the two general bounds of the lemma.
2. Lemma 5.1: an $(\alpha,\beta,\delta)$-family forces $\mathsf{dec}_\gamma \ge \alpha/2 - \gamma(\beta/N + \delta)$, stated for a general measurable decision space.
3. The hard family $\theta_i = \Delta e_i$: regret $\Delta(1-\pi_i)$ and $D^2_{\mathrm{H}}(M_i(\pi), \mathrm{Rad}(0)) \le \tfrac34\Delta^2\pi_i^2$. With the coordinate bounds $\sum_i \pi_i \le \sqrt d \le d/2$ ($d \ge 4$) and $\sum_i \pi_i^2 \le 1$, stated as a separate item, this makes the family a $(\Delta, \tfrac34\Delta^2, 0)$-family.
4. Localization: the family lies in $\mathcal{M}^\infty_{2\Delta}(\mathrm{Rad}(0))$.

Companion: Proposition 6.8

For $\Delta \in (0, 1/4)$ and $d \ge 2$, an explicit class of linear bandit models on $\{e_1,\dots,e_d\}$, each with gap $\Delta$, satisfies $\mathsf{dec}_\gamma(\mathcal{M}^\infty_\Delta(\overline{M}),\overline{M}) \ge (\Delta/4)\,\mathbb{I}\{\gamma \le d/(12\Delta)\}$ for all $\gamma > 0$.

Significance

The bound shows that the DEC of linear bandits under Euclidean geometry is of order $d/\gamma$, which matches, up to constants, the upper bound $\mathsf{dec}^{\mathrm{Sq}}_\gamma \le d/(4\gamma)$ on the square-loss variant of the DEC certified by the strategy of Proposition 6.1. Through Theorem 3.2 it gives the regret lower bound $\Omega(\sqrt{dT})$ for every algorithm. Proposition 6.8 shows that the DEC gives meaningful lower bounds even for classes of models with a fixed gap.

All results are proved in the paper. None has a machine-checked proof. The mission produces a formal statement of the linear-bandit lower bound with its radius corrected, the hard-family lemma (Lemma 5.1) in a form that applies to infinite decision spaces and to range-free $u_i$, and the Rademacher Hellinger estimates that later DEC lower bounds reuse.

Difficulty

The arithmetic of the construction is short. The work is in the infrastructure.

• The infimum runs over all Borel probability measures on the ball, not over finitely supported ones. Lemma 5.1 must therefore be proved for Bochner integrals, with the integrability of the payoff established from its continuity on the compact ball.
• The bound $\sum_i \pi_i \le \sqrt d \le d/2$ is Cauchy–Schwarz on $\mathbb{R}^d$ and needs $d \ge 4$.
• The value $\langle\theta_i, \pi_{\theta_i}\rangle = \Delta$ must come from the selector hypothesis plus Cauchy–Schwarz, because the selector is not given explicitly.
• Lemma 5.1 cannot be applied in the form printed in Definition 5.1: there $u_i$ takes values in $[0,1]$, but the family's $u_i(\pi) = \pi_i$ can be negative. The lemma is needed without the range conditions.

Formalization scope

• Outcomes. They are finite: the $\pm1$ outcome is encoded on Bool, and models are the Rademacher laws $\mathrm{Rad}(\langle\theta,\pi\rangle)$, identified with their parameters $\theta \in \mathbb{B}^d$. The paper's class contains every reward law on $[-1,1]$ with linear mean. The Rademacher subclass has a smaller localized class, so a lower bound for it implies the paper's.
• Decisions. For the goal they range over the ball itself (an infinite space with its Borel $\sigma$-algebra), and decision distributions are arbitrary ProbabilityMeasures on it.
• The DEC is unfolded. For every $p$ some model of the localized class attains the bound. This is what the proof shows, and it implies the inf–sup inequality.
• Selectors. $\pi_M$ is a selector with a maximizer hypothesis, so statements hold for every choice of maximizer.
• Added hypotheses. Lemma 5.1 carries $\alpha, \beta \ge 0$ and integrability of its four functions. Proposition 6.8 carries $d \ge 2$.
• No trivializing reading. The integrals in the goal are genuine: the integrand is bounded and continuous, and a sanity file proves integrability, so the Bochner convention $\int f = 0$ for non-integrable $f$ never applies. The goal's quantifier over $p$ is not restricted. The radius $2d/(3\gamma)$ is the smallest the construction allows.
• Definitions and reuse. The mission defines the unit ball, $\mathrm{Rad}$, the linear model, the regret $g^\theta$, and the localized class over a measurable decision space. It references the published hellingerSq, fM and decGf. The general Lemma 5.1 and Lemma A.8 are reusable for every DEC lower bound in §§5–7.

Contributions welcome: proofs of the milestones, a version of the goal through an explicit inf–sup definition of the DEC over measures, and the general model class with arbitrary reward laws on $[-1,1]$.

Selected references

• D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, v3, 2023. https://arxiv.org/abs/2112.13487
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020 (linear bandits, Ch. 19–24). https://doi.org/10.1017/9781108571401
• D. J. Foster, C. Gentile, M. Mohri, J. Zimmert, Adapting to Misspecification in Contextual Bandits, NeurIPS 2020 (Proposition 6.1's strategy). https://arxiv.org/abs/2107.05745

Motivation

An echo state network with output feedback is a recurrent model whose previous output is fed back into its next hidden-state update. In reservoir computing only the linear output weights are trained, while the internal weights are fixed, typically after being drawn at random. This raises a quantitative question: if the internal rows are sampled from a fixed law, can a network with $N$ blocks of random rows and a suitable linear readout approximate a given input–output rule, and at what rate in $N$? Gonon, Grigoryeva and Ortega answer this for targets generated by contracting reservoir systems. Their Theorem 4 (p. 63) gives, with explicit constants, a probability bound and an excess-risk bound of order $1/\sqrt N$, plus a term decaying geometrically in the length $T$ of the observation window. The input set is not required to be bounded: the bound depends on the input process only through $\mathbb E[\max_{t}\|Z_t\|]$ over the window.

Setting

Inputs are vectors in a set $D_d\subseteq\mathbb R^d$ and an input history is $z=(z_t)_{t\in\mathbb Z_-}$, with $\mathbb Z_-=\{0,-1,-2,\dots\}$. A target reservoir is a map $F^*:\mathbb R^{N^*}\times D_d\to B_M$, with $B_M$ the closed Euclidean ball of radius $M$, such that $F^*(\cdot,v)$ is an $r$-contraction for every $v\in D_d$, with $r\in(0,1)$. Its reservoir functional is $H^*(z)=x^*_0$, where $x^*_t=F^*(x^*_{t-1},z_t)$ for all $t\in\mathbb Z_-$. The output dimension is $m=N^*$.

The approximating network has $N$ blocks of $N^*$ rows. Each row is a vector $\omega=(a,c,\zeta)\in\mathbb R^{N^*+d+1}$, and the $\bar N=NN^*$ rows $U_j^{(i)}$ of $[A,C,\zeta]$ are i.i.d. with law $\pi$. With an activation $\sigma$ and a readout matrix $W\in\mathbb M_{m,\bar N}$, the system is

$$x_t=\sigma(Ay_{t-1}+Cz_t+\zeta),\qquad y_t=Wx_t,\qquad t=-T,\dots,0,\qquad y_{-T-1}=\Xi,$$

with $T\ge1$ and $\|\Xi\|\le M$; its functional is $H^{A,C,\zeta}_W(z)=y_0$. For each $k\ge1$ and $j=1,\dots,N^*$ a signed measure $\pi_j^k\ll\pi$ defines the integral map

$$F_j^{*,N}(x,v)=\int\sigma((x,v,1)\cdot\omega)\,\pi_j^N(d\omega).$$

The constant $C_*=4\sqrt3L_\sigma\sup_{k}\sum_j(\int\|\omega\|^2(d\pi_j^k/d\pi)^2d\pi)^{1/2}$ measures the size of these densities, and $s_N=\mathbb E[\max_{t\in\{0,\dots,-T\}}\sup_{x\in B_{M+1}}\|F^{*,N}(x,Z_t)-F^*(x,Z_t)\|]$ is the approximation error of $F^{*,N}$. The input process $Z$ is independent of $(A,C,\zeta)$, $Y_0$ is an integrable target, and the loss $L\ge0$ is Lipschitz with constant $L_L$. The echo state event $\Omega_{\mathrm{ESP}}$ of (87) is the event that $\|WF^{A,C,\zeta}(x,Z_t)\|\le M+1$ for all $x\in B_{M+1}$ and $t\in\{0,\dots,-T\}$, where $F^{A,C,\zeta}(x,v)=\sigma(Ax+Cv+\zeta)$.

Formalization targets

Steps of the proof

The milestones are the displayed estimates of the proof, in attack order:

1. (89): one step of the error recursion on $\Omega_{\mathrm{ESP}}$, $\mathbb E[\|Y_t-X^*_t\|\mathbb 1_{\Omega_{\mathrm{ESP}}}]\le\mathbb E[\sup_{y}\|\cdots\|]+s_N+r\,\mathbb E[\|Y_{t-1}-X^*_{t-1}\|\mathbb 1_{\Omega_{\mathrm{ESP}}}]$;
2. (90): splitting into coordinates and symmetrization of the uniform error of the random map;
3. (91): a deterministic bound on Rademacher averages,

$$\mathbb E_\varepsilon\sup_{y\in B_{M+1}}\Big|\sum_{i=1}^N v_i\varepsilon_i\sigma((y,z,1)\cdot u_i)\Big|\le2L_\sigma\Big((M+1)\big(\textstyle\sum_iv_i^2\|a_i\|^2\big)^{1/2}+\|z\|\big(\sum_iv_i^2\|c_i\|^2\big)^{1/2}+\big(\sum_iv_i^2\zeta_i^2\big)^{1/2}\Big);$$

4. (92)–(93): for each fixed input $z\in D_d$,

$$\mathbb E\sup_{y\in B_{M+1}}\Big\|\frac1N\sum_{i=1}^NW_i\sigma(A^{(i)}y+C^{(i)}z+\zeta^{(i)})-F^{*,N}(y,z)\Big\|\le\frac{(M+2+\|z\|)C_*}{\sqrt N};$$

5. (96): $\mathbb P(\Omega\setminus\Omega_{\mathrm{ESP}})\le2(M+2+\mathbb E[\max_t\|Z_t\|])C_*/\sqrt N+2s_N$.

Goal: Theorem 4

There is a readout $W$, a function of $(A,C,\zeta)$ alone, such that for every $\delta\in(0,1)$ and every $\|\Xi\|\le M$, with probability at least $\max(1-\delta-2C_*(M+2+\mathbb E[\max_t\|Z_t\|])/\sqrt N-2s_N,0)$, the event $\Omega_{\mathrm{ESP}}$ holds and

$$|\mathcal R(H^{A,C,\zeta}_W)-\mathcal R(H^*)|\le \frac{L_L}{\delta}\Big[\frac{(M+2+\max_t\mathbb E\|Z_t\|)C_*}{(1-r)\sqrt N}+\frac{s_N}{1-r}+2(M+1)r^{T+1}\Big],$$

where $\mathcal R(H)=\mathbb E[L(H(Z),Y_0)]$ is evaluated at fixed network weights.

Significance

The bound separates three sources of error: sampling $N$ blocks of random rows (rate $1/\sqrt N$), the approximation of $F^*$ by the integral map $F^{*,N}$ ($s_N$), and the finite initialization of the feedback recursion ($r^{T+1}$). Only the readout depends on the target; the internal weights are generated without it. The theorem also bounds the probability that the random feedback map leaves the state ball on which the recursion is controlled, which is the form in which the echo state property enters. Via Theorem 3 (p. 62), which specializes the densities through the paper's Proposition 2, it gives approximation rates for ReLU output-feedback networks.

The paper proves the result on pp. 63–68. No part of it is formalized. A complete development would give machine-checked Rademacher symmetrization and contraction estimates for random features, uniform-over-a-ball bounds for sampled integral maps, and a treatment of finite feedback recursions on product probability spaces, all reusable outside reservoir computing.

Difficulty

A pointwise approximation of $F^*$ by the sampled map does not control the feedback system, because the next feedback value is itself the random output of the previous update. The comparison must hold uniformly over the state ball $B_{M+1}$ and over the whole input window, and the event that the recursion leaves the ball must be charged to an explicit probability. The uniform bound requires symmetrization and the Ledoux–Talagrand contraction principle for a supremum over a continuum of states, with per-index contractions; Lipschitz continuity of $\sigma$ alone does not supply the vanishing at zero that principle needs. The input is unbounded, so the input dependence must be tracked through $\|z\|$ and integrated at the end.

Formalization scope

States, inputs, outputs and rows are Euclidean spaces (EuclideanSpace); a row is indexed by $(\{1..N^*\}\sqcup\{1..d\})\sqcup\{\ast\}$ and the rows by $\{1..N\}\times\{1..N^*\}$. Time $t\in\mathbb Z_-$ is the index $-t\in\mathbb N$; the equation (78) is the published ReservoirESN.IsSolution. The rows have law $\pi^{\otimes NN^*}$ on their own space and $(Z,Y_0)$ lives on a separate probability space; the probability is under the product law, which encodes the independence of §6.1. Signed measures $\pi_j^k$ are their Radon–Nikodym densities with respect to $\pi$, with integrability and first-moment hypotheses. $C_*$, $s_N$ and $\mathbb E[\max_t\|Z_t\|]$ are extended nonnegative integrals and suprema, converted to reals only under their finiteness hypotheses; the risk integrals are finite under the loss Lipschitz bound, integrable target and input-moment assumption; the supremum in (87) is unfolded. $F^*$ is assumed jointly measurable, the standing convention that makes $s_N$ and $H^*(Z)$ random variables; the standing assumptions $d,N^*\ge1$ and $M>0$ (p. 30) and $T\ge1$ (§6.1) are hypotheses.

Trivialization ruled out. The readout is a measurable function of the rows only and is chosen before $\delta$ and $\Xi$. A readout allowed to look at the input $Z$ would make the claim a different and much weaker statement.

Correction of the print. The goal and milestones (91), (93), (96) assume $\sigma(0)=0$: the contraction principle cited at (91) needs contractions vanishing at zero, while the printed theorem states only that $\sigma$ is Lipschitz. ReLU, the paper's application, satisfies it. The goal retains the printed full risk difference. Its proof passes through (88), where an indicator depending on $Z$ is moved inside a risk integral; this step needs further justification. The milestone quotations keep the printed text.

Contributions are welcome on each milestone, on general Rademacher symmetrization and contraction lemmas for suprema over compact parameter sets, on measurability of suprema of continuous random fields, and on the printed form of the risk bound.

Selected references

• L. Gonon, L. Grigoryeva and J.-P. Ortega, Approximation bounds for random neural networks and reservoir systems, The Annals of Applied Probability 33(1), 2023, 28–69. https://doi.org/10.1214/22-AAP1806
• M. Ledoux and M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991 (Theorem 4.12, the contraction principle). https://doi.org/10.1007/978-3-642-20212-4