Machine Learning

Why sequential portfolios matter

A portfolio manager chooses fractions of current wealth to place in several stocks before seeing that day’s market gains. The gains need not follow a statistical model: a sequence may be selected adversarially, with some stocks losing all value on a given day. A useful benchmark is the best constantly rebalanced portfolio, which holds the same fractions each day but trades at the end of every round to restore them. Its fixed allocation is an active strategy, and it can grow even when buying and holding each individual stock does not. Chapter 10 of Orabona’s online learning text studies guarantees against this benchmark without imposing a positive lower bound or a finite upper bound on nonzero market gains.

The chapter presents a universal portfolio: an allocation determined by a prior distribution over all fixed portfolios and reweighted according to their wealth so far. The mission focuses on the uniform-prior part of Theorem 10.1. It asks for a worst-case logarithmic regret guarantee against every fixed comparator and every admissible market sequence. This is a deterministic guarantee; no distributional assumption about the market enters its statement.

Market and strategy

There are $d\ge2$ stocks and $T\ge1$ rounds. In round $t$, the market supplies a vector $w_t\in\mathbb R_{≥0}^d\setminus\{0\}$ of nonnegative gains. A portfolio is $u\in\Delta^{d-1}$, the simplex of vectors with nonnegative coordinates summing to one. If one unit is invested initially and the allocation stays fixed, its wealth after $T$ rounds is

A sequential strategy chooses $x_t\in\Delta^{d-1}$ before seeing $w_t$, and has wealth $W_T=\prod_{t=1}^{T}\langle w_t,x_t\rangle$. The quantity of interest is the difference between the logarithms of benchmark wealth and sequential wealth. A fixed portfolio can have zero wealth when all the stocks it holds have a zero gain on some day; its log wealth is then $-\infty$ in the mathematical convention of the book.

Algorithm 10.1 begins with a prior $F$ on the simplex. Before round $t$, it gives each fixed portfolio $u$ weight proportional to its wealth $W_{t-1}(u)$, and chooses the resulting mean allocation:

For this mission, $F$ is the uniform probability measure on the simplex. It is represented by Lebesgue measure in the first $d-1$ coordinates, scaled by $(d-1)!$; the final coordinate is one minus their sum. This explicit density fixes what “uniform” means and prevents the prior from being chosen to suit a particular market sequence.

Formalization targets

The goal is the uniform-prior case of Theorem 10.1. With the notation above, for every fixed portfolio of positive wealth,

The goal also asserts $W_T>0$, so the algorithm’s logarithmic wealth is defined. The first inequality gives an exact finite-horizon combinatorial bound; the second displays its logarithmic dependence on $T$ for fixed $d$. The book also states a Dirichlet$(1/2,\ldots,1/2)$ prior bound in the same theorem. That companion branch is not among this proposal’s draft items; its gamma-function normalization and integral identities would require a separate audited definition layer. The fixed series title follows the chapter plan, while the goal and milestone list specify the precise scope delivered here.

The attack path records four source statements. Lemma 10.5 bounds a ratio of nonnegative sums by the largest component ratio. Lemma 10.6 reduces a universal portfolio’s wealth ratio to a maximum over sequences of single-stock choices. Theorem 10.4 bounds the size of a type class, the set of sequences with the same empirical fractions of symbols. Equation (10.5) computes the monomial integral under the uniform simplex prior. These statements are from the chapter’s proof of Theorem 10.1; the equation is referred to as an exercise in Problem 10.3.

What the result provides

The theorem ensures that the uniform-prior strategy keeps its log wealth within $O(d\log(1+T/d))$ of the best constantly rebalanced portfolio, while making no bounded-gain assumption. In particular, a stock may have gain zero on one day or a very large gain on another. The guarantee is pathwise: it applies to the realized market vectors, regardless of how they were chosen. For a fixed number of stocks, dividing regret by $T$ therefore gives a vanishing average shortfall in log wealth.

The mathematical result is already proved in the cited text. This mission’s work is to give its exact algorithm, prior measure, combinatorial objects, and finite-horizon constants machine-checked statements and then proofs. The density-based prior, finite type classes, and simplex monomial integrals can also be reused in online aggregation and universal coding developments. The draft statements currently have Lean placeholders for proofs; a successful submission will still require solvers to close them.

Main difficulty

Applying a generic online convex optimization bound to the loss $-\log\langle w_t,x\rangle$ runs into unbounded gradients when a chosen portfolio has small gain. A bound based on one global Lipschitz constant cannot cover the market sequences allowed here. The integral strategy creates a different obstacle: its denominator must be positive at every round, including histories with zero gains for many fixed portfolios. Its uniform prior is a measure on a $(d-1)$-dimensional simplex embedded in $\mathbb R^d$, so ambient $d$-dimensional volume would give it mass zero. A proof must work with the intrinsic coordinate measure and its normalization. The exact binomial coefficient also depends on counting all sequences of one type without losing the boundary cases where some symbol occurs zero times.

Formalization scope

Lean represents a portfolio as a function Fin d → ℝ in Mathlib’s stdSimplex; a market is a one-based sequence of vectors of the same type. The coordinate chart maps $\mathbb R^{d-1}$ into the simplex, and a scaled restricted Lebesgue measure is pushed forward to define the uniform prior. The chart’s measurability is proved in the definition file. Algorithm 10.1 is a componentwise ratio of real integrals, and the main theorem asserts positive realized wealth. All market vectors on rounds $1,\ldots,T$ are nonnegative and nonzero. The parameter restrictions $d\ge2$ and $T\ge1$ make the dimension and printed denominators meaningful.

For Lemma 10.5, quotients use extended nonnegative reals, with $a/0=+\infty$ when $a>0$ and $0/0=0$ as printed. Lemma 10.6 is stated for a generic prior concentrated on the simplex, with its ratios in extended nonnegative reals under the same conventions, and with the hypothesis that the normalizing integral of Algorithm 10.1 is positive in every round, which is what makes the algorithm's prediction defined. A comparator with zero wealth is omitted only from the real-log statement, corresponding to log wealth $-\infty$ in the source. The prior cannot be replaced by an arbitrary point mass: the theorem names the chart-based uniform measure, and the prediction is the exact integral ratio. Contributions proving normalization, support, the integral identity, and the final regret bound are all within scope.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 10 and Appendix A.2.2. arXiv

Motivation

The proximal stochastic subgradient method is the workhorse of large-scale learning: to minimize a regularized population risk $\varphi(x) = f(x) + r(x)$ with $f(x) = \mathbb E_{\xi \sim P}[f(x,\xi)]$, it samples a data point, takes a step against a sampled subgradient of $f$, and applies the proximal map of the regularizer $r$. Its sample complexity is classical for convex problems ($O(\varepsilon^{-2})$ samples for function accuracy $\varepsilon$) and for smooth nonconvex problems ($O(\varepsilon^{-4})$ samples for gradient norm $\varepsilon$, Ghadimi–Lan 2013). For problems that are both nonsmooth and nonconvex, however, no complexity bound was known for any reasonably broad class before Davis–Drusvyatskiy 2019.

Many such problems — robust phase retrieval, nonlinear least squares with an $\ell_1$ loss, conditional value-at-risk minimization with smooth losses, covariance estimation — are weakly convex: they become convex after adding a quadratic $\frac{\rho}{2}\|x\|^2$. This mission formalizes the complexity guarantee of Davis and Drusvyatskiy for the proximal stochastic subgradient method on weakly convex problems.

Timeline. Nurminskii (1973) showed that for weakly convex $f(\cdot,\xi)$ and $r = 0$ the stochastic subgradient method has limit points that are stationary, without a rate. Ghadimi and Lan (2013) proved the $O(\varepsilon^{-4})$ rate for smooth $f$. Davis and Drusvyatskiy (arXiv 2018, SIAM J. Optim. 2019) proved the first rate for the proximal stochastic subgradient method under weak convexity, measured by the gradient of the Moreau envelope; this is Theorem 3.4 of their paper.

Setting

Work in $\mathbb R^d$ with the Euclidean norm. Let $r : \mathbb R^d \to \mathbb R \cup \{+\infty\}$ be closed (its epigraph is closed) and convex, with nonempty domain $D = \operatorname{dom} r$, and let $f : \mathbb R^d \to \mathbb R$ be $\rho$-weakly convex: $x \mapsto f(x) + \frac{\rho}{2}\|x\|^2$ is convex. Set $\varphi = f + r$.

The subdifferential $\partial\psi(x)$ of a function $\psi$ at a point $x$ of its domain is the set of vectors $v$ with $\psi(y) \ge \psi(x) + \langle v, y - x\rangle + o(\|y - x\|)$ as $y \to x$; it is empty off the domain. For $\lambda > 0$ the Moreau envelope and the proximal map are

Assumption A (stochastic subgradient oracle): on a probability space $(\Omega, \mathcal F, P)$ one can draw i.i.d. samples $\xi_0, \xi_1, \dots \sim P$ (A1); there are an open set $U \supseteq D$ and a measurable map $G$ with $\mathbb E_\xi[G(x,\xi)] \in \partial f(x)$ for all $x \in U$ (A2); and $\mathbb E_\xi\|G(x,\xi)\|^2 \le L^2$ for all $x \in D$ (A3).

Algorithm 3.1 starts at $x_0 \in D$ and, for $t = 0, \dots, T$, samples $\xi_t$ and sets $x_{t+1} = \operatorname{prox}_{\alpha_t r}(x_t - \alpha_t G(x_t, \xi_t))$. It returns $x_{t^*}$ with $t^*$ drawn from $\{0, \dots, T\}$ with probability $\alpha_t / \sum_i \alpha_i$.

Formalization targets

Goal: Theorem 3.4, (3.15) and (3.16)

For $\bar\rho \in (\rho, 2\rho]$ and stepsizes $\alpha_t \in (0, 1/\bar\rho]$,

and with $\alpha_t = \gamma/\sqrt{T+1}$, $\gamma \in (0, \frac{1}{2\rho}]$,

Milestones

In the order the proof uses them: Lemma 2.1 (subdifferential characterization of weak convexity), the existence of $\hat v_t \in \partial f(\hat x_t)$ with $\bar\rho(x_t - \hat x_t) \in \partial r(\hat x_t) + \hat v_t$ (§3.2), Lemma 3.2 ($\hat x_t$ is a proximal point of $r$), Lemma 3.3 (one-step contraction towards $\hat x_t$), Lemma 2.2 (the envelope is $C^1$ with $\nabla\varphi_\lambda(x) = \lambda^{-1}(x - \operatorname{prox}_{\lambda\varphi}(x))$), and the one-step descent estimate (3.14).

Significance

The result. A small $\|\nabla\varphi_\lambda(x)\|$ certifies that $x$ is within $\lambda\|\nabla\varphi_\lambda(x)\|$ of a point $\hat x$ with $\varphi(\hat x) \le \varphi(x)$ and $\operatorname{dist}(0, \partial\varphi(\hat x)) \le \|\nabla\varphi_\lambda(x)\|$. Theorem 3.4 therefore gives a sample complexity of $O(\varepsilon^{-4})$ for reaching an $\varepsilon$-nearly stationary point, matching the smooth rate, for a method that is run in practice without modification. The underlying observation — the method is an approximate descent method on the Moreau envelope — is reused in the paper's model-based analysis (Theorem 4.3) and in subsequent work on stochastic nonsmooth nonconvex optimization.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A complete development produces reusable infrastructure: the Fréchet subdifferential of extended-valued functions, weak convexity and its subgradient characterization, Moreau envelopes of weakly convex functions and their differentiability, nonexpansiveness of convex proximal maps, and the bookkeeping of iterates driven by i.i.d. samples under a product measure.

Difficulty

The obvious argument — show that $\varphi(x_t)$ decreases in expectation — fails: neither $\varphi(x_t) - \min\varphi$ nor $\operatorname{dist}(0, \partial\varphi(x_t))$ need tend to zero, and the latter is discontinuous in $x$. Progress must be measured on the Moreau envelope, which requires comparing the iterate $x_{t+1}$ with the proximal point $\hat x_t$ of $\varphi$, not of $r$. In Lean, the heaviest single ingredient is Lemma 2.2 (differentiability of the envelope of an extended-valued weakly convex function), and the direction $4 \Rightarrow 1$ of Lemma 2.1, which in the paper rests on Rockafellar–Wets' characterization of convexity by monotonicity of the subdifferential.

Formalization scope

• Carrier. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d). An extended-valued function is a pair (domain $D$, real values on $D$); closedness is closedness of $\{(x,t) : x \in D,\ \psi(x) \le t\}$. The subdifferential is the published regular subgradient NonconvexSplitting.Shared.IsRegularSubgrad of the $+\infty$-extended lift.
• Proximal map. prox a z is a function constrained, for every $a > 0$, to return a minimizer over $D$ of $r(y) + \frac{1}{2a}\|y - z\|^2$; this determines it uniquely.
• Randomness. The samples $\xi_0, \dots, \xi_T$ form a point of $\Omega^{T+1}$ under the product measure $P^{\otimes(T+1)}$; $\mathbb E$ is the Bochner integral, and every bounded expectation is accompanied by a conclusion that its integrand is integrable. The conditional expectation $\mathbb E_t$ in Lemma 3.3 is the integral over one sample with the iterate held fixed.
• Output index. Because $t^*$ is independent of the samples, $\mathbb E\|\nabla\varphi_{1/\bar\rho}(x_{t^*})\|^2$ is the $\alpha$-weighted average of $\mathbb E\|\nabla\varphi_{1/\bar\rho}(x_t)\|^2$, as in the paper's (3.17).
• $\min\varphi$ is an arbitrary real lower bound $\varphi^*$ of $\varphi$ on $D$.
• Corrected constant in (3.14). The paper prints the last term of (3.14) as $\alpha_t^2\bar\rho L^2$; its proof, and the unfolded sum leading to (3.15), give $2\alpha_t^2\bar\rho L^2$, and that is what is stated. (3.15) and (3.16) are stated as printed.
• Lemma 2.1 is stated for items 1–4; the clause for $C^2$-smooth functions is not stated. Lemma 2.2 adds the implicit hypotheses that $\varphi$ is closed and proper, and includes existence and uniqueness of the proximal point.
• Ruling out trivializations. The proximal map is tied to $r$, $G$ is tied to $\partial f$ by (A2), $\min\varphi$ is not a real infimum, and integrability is concluded, so neither a junk value nor an unconstrained selection can make the statements hold vacuously; the hypotheses are satisfied by $r = f = 0$, $G = 0$.
• Contributions welcome: proofs of the milestones, general lemmas on Moreau envelopes of weakly convex functions, and the nonexpansiveness of convex proximal maps on a closed convex domain.

Selected references

• D. Davis and D. Drusvyatskiy, Stochastic Model-Based Minimization of Weakly Convex Functions, SIAM J. Optim. 29(1), 2019; arXiv:1803.06523v3, 2018. https://arxiv.org/abs/1803.06523
• S. Ghadimi and G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM J. Optim. 23(4), 2013. https://doi.org/10.1137/120880811
• R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• H. Robbins and S. Monro, A Stochastic Approximation Method, Ann. Math. Statist. 22(3), 1951. https://doi.org/10.1214/aoms/1177729586

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

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$,

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

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

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

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

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$,

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

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

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$:

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$,

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.