Machine Learning

Motivation

Many arguments in high-dimensional geometry, statistics and computer science need to approximate a point of a convex set by an average of a handful of extreme points, rather than represent it exactly. The classical Carathéodory theorem (1907) answers the exact question: every point of the convex hull of a set $T \subseteq \mathbb{R}^n$ is a convex combination of at most $n+1$ points of $T$. That bound is tight and grows with the dimension $n$, which makes it useless whenever $n$ is large — exactly the regime of interest in high-dimensional probability.

B. Maurey's empirical method — an unpublished 1980–81 result reported by G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse Fonctionnelle 1980–1981 — and later applied by B. Carl to bound covering numbers of operators between Banach spaces (Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in Banach spaces, Ann. Inst. Fourier 35(3), 1985, 79–118), replaces the exact question with an approximate one and removes the dimension dependence entirely: to approximate $x$ to accuracy $\varepsilon$, the number of points needed depends only on $\varepsilon$, never on $n$. Vershynin's High-Dimensional Probability opens with this result as its "Appetizer," using it to illustrate the book's central theme — that randomness is a tool for constructing deterministic combinatorial objects — before any probabilistic machinery has been introduced.

Setting

A convex combination of finitely many points $z_1, \dots, z_m \in \mathbb{R}^n$ is a sum $\sum_{i=1}^m \lambda_i z_i$ with $\lambda_i \ge 0$ and $\sum_i \lambda_i = 1$. The convex hull $\operatorname{conv}(T)$ of a set $T \subseteq \mathbb{R}^n$ is the set of all convex combinations of all finite collections of points of $T$. The diameter of $T$ is $\operatorname{diam}(T) = \sup\{\|s-t\|_2 : s, t \in T\}$, the Euclidean norm throughout.

The classical Carathéodory theorem states that every $x \in \operatorname{conv}(T)$ is a convex combination of at most $n+1$ points of $T$ — with $n+1$ generally unavoidable, attained by a simplex. The question this mission answers is different: given that we are willing to approximate $x$ rather than represent it exactly, and willing to use only combinations with equal coefficients $1/k$ (an average of $k$ points, with repetition allowed), how large must $k$ be as a function of the desired accuracy?

Formalization targets

Goal — Theorem 0.0.2, Approximate Carathéodory's theorem

The quantifiers are exactly this order: for every bounded $T$, every point of its convex hull, and every target $k$, such an averaging set exists. This is the weakest stable statement carrying the theorem's content — the number of points $k$ does not depend on the dimension $n$, and the coefficients are forced to be uniform — and it is the form the corollary below invokes directly.

Milestone — Corollary 0.0.4, Covering polytopes by balls

This is a direct application of the goal to computational geometry's covering problem: how many balls of radius $\varepsilon$ are needed to cover a polytope, and where should they be centered.

Significance

The result itself. The approximate Carathéodory theorem is the prototype of a dimension-free approximation result: whenever a set is bounded, a fixed number of points (depending only on the target accuracy, not the ambient dimension) suffices to approximate any point of its convex hull. This is what makes possible dimension-independent covering-number bounds such as Corollary 0.0.4, which in turn are the starting point for the book's later treatment of entropy, packing and generic chaining (Chapters 4, 7–8). The technique generalizes far beyond $\mathbb{R}^n$: it underlies covering-number bounds for operators between Banach spaces (Carl's original application) and is a recurring device in learning theory for bounding the size of an $\varepsilon$-net of a hypothesis class.

Formalizing it. Both results are elementary and already fully proved in the literature; no open mathematical content remains. What this mission contributes is a machine-checked, faithful Lean statement of Maurey's construction and its corollary, phrased over Mathlib's existing convex-hull and metric-diameter machinery, so that later missions in this series (concentration inequalities, Johnson–Lindenstrauss, chaining) can build on a verified base case of "probability constructs a deterministic covering," and so that the empirical method itself becomes a reusable, linked component on the platform. The proof of the goal (via the probabilistic argument sketched by the book: interpret a convex combination as a probability distribution, average $k$ i.i.d. samples, and bound the variance) is left open for solvers.

Difficulty

The identity that makes the proof work — averaging $k$ independent copies of a random vector concentrates around its mean at rate $1/\sqrt{k}$ in mean-square — is a two-line computation once the convex combination is reinterpreted probabilistically. The step that is easy to miss is this reinterpretation itself: nothing in the statement mentions probability, so the "obvious" attack of manipulating the convex-combination weights directly, or trying to construct $x_1,\dots,x_k$ by some explicit combinatorial recipe, does not see a path to a bound independent of $n$. The probabilistic argument produces the points non-constructively, via an averaging/existence argument (the expected squared distance is small, so some realization achieves it) rather than an explicit formula — a solver has to introduce a probability space and a random vector that does not appear anywhere in the formal statement to be proved.

Formalization scope

Both results are stated over EuclideanSpace ℝ (Fin n) for an explicit dimension n : ℕ, so ‖·‖ is the Euclidean norm and Mathlib's Metric.diam is used directly for $\operatorname{diam}(T) = \sup\{\|s-t\|_2\}$. The convex hull is Mathlib's convexHull ℝ T; by Mathlib's convexHull_eq, this already coincides with the book's own definition of a convex combination of finitely many points of $T$, so no bespoke convex-combination definition is introduced — this mission needs no supporting definitions of its own. In the corollary, "a polytope $P$ with $N$ vertices" is formalized, following the book's own proof, as $P = \operatorname{conv}(T)$ for a finite vertex set $T$ with $\#T = N$, rather than via a separate Polytope structure (which Mathlib does not provide and the book's argument does not need). The covering bound $N^{\lceil 1/\varepsilon^2\rceil}$ is an exponent, not a product with $N$ — matching the book's own proof, which counts the $N^k$ ordered $k$-tuples of vertices with repetition, $k := \lceil 1/\varepsilon^2\rceil$; the typeset "$N\lceil 1/\varepsilon^2\rceil$" in the corollary statement is the same juxtaposition-as-exponent notation the proof uses for "$N^k$" one line earlier.

A trivializing formalization is ruled out explicitly: the goal must hold for every integer $k > 0$ and every $x \in \operatorname{conv}(T)$, not merely some convenient choice — e.g. $k = 1$ together with $x \in T$ trivially satisfies the inequality but proves nothing about the theorem's actual content, that a fixed, dimension-independent $k$ works uniformly over all points of the hull. The formal statement quantifies $T$, then $x$, then $k$, and only then asserts existence of the $x_1,\dots,x_k$, exactly in that order.

Classical Carathéodory (Theorem 0.0.1, stated for context in the source but not used by either formalized result's proof) is not drafted here: Mathlib already proves the corresponding statement via affine independence (Caratheodory.eq_pos_convex_span_of_mem_convexHull, Analysis/Convex/Caratheodory.lean), from which the book's "$n+1$ points" bound follows via AffineIndependent.card_le_finrank_succ. It is not added as a kind: reference milestone because no corresponding theorem is yet published on the Prove2Me platform to point at (checked 2026-09-17: GET /theorems?q=Caratheodory returns only unrelated tropical-convexity results), and re-drafting existing Mathlib content as a new platform theorem would duplicate rather than reuse it.

Selected references

• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, DOI 10.1017/9781108231596, Appetizer (pp. 1–5).
• G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse Fonctionnelle (Maurey–Schwartz), 1980–1981, exposé no. 5. numdam.org/item/SAF_1980-1981____A5_0
• B. Carl, "Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in Banach spaces," Annales de l'Institut Fourier, 35(3), 1985, 79–118. numdam.org/item/AIF_1985__35_3_79_0

Motivation

Online convex optimization (OCO) models a repeated decision process: at each round a learner picks a point in a convex set, an adversary (or the world) reveals a convex cost function, the learner pays that cost at its own point, and the process repeats. No statistical assumption on the sequence of costs is made. This model, introduced by Zinkevich [Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003], underlies most of modern online learning: portfolio selection, online routing, and — through its special case of stochastic optimization — the training of essentially every large machine-learning model in current use, since stochastic gradient descent (the subject of §3.4 of this chapter) is exactly an application of the regret bounds proved here.

The algorithm this chapter introduces, online gradient descent (OGD), is the field's default answer: take a gradient step against the most recently observed cost, project back onto the feasible set. It predates OCO itself as a heuristic, but Zinkevich's contribution — and this chapter's — is the regret analysis: a guarantee that holds against every sequence of costs, adversarially chosen, with an explicit, small constant. Precursors for less general settings appear in Kivinen and Warmuth [1997]; logarithmic-regret algorithms for OCO, the subject of §3.3 here, are due to Hazan, Agarwal and Kale [2007].

The online convex optimization protocol

Fix a convex set $K$ in a real inner product space, playing the role of the decision (or "action") space, and a sequence of cost functions $f_1, f_2, \dots : K \to \mathbb{R}$, each convex. At round $t$, the learner (not knowing $f_t$) plays a point $x_t \in K$, then observes $f_t$ and pays $f_t(x_t)$. Regret after $T$ rounds compares the learner's cumulative cost to that of the single best fixed decision made with hindsight of the whole sequence:

A learner with regret $o(T)$ is, on average, eventually as good as the best fixed point in $K$, even though it never knew the cost sequence in advance.

Two chapter-wide parameters bound how hard an instance can be: $D$, the diameter of $K$ ($\operatorname{dist}(x,y) \le D$ for all $x, y \in K$), and $G$, a common bound on the gradient norm of every $f_t$ over $K$ ($\|\nabla f_t(x)\| \le G$ for all $x \in K$), which implies but is strictly stronger than $G$-Lipschitzness on $K$. Online gradient descent (Algorithm 8) plays $x_1 \in K$ arbitrarily, then at every round sets $y_{t+1} = x_t - \eta_t \nabla f_t(x_t)$ and projects, $x_{t+1} = \Pi_K(y_{t+1})$, for a sequence of step sizes $\eta_t$ chosen in advance.

Formalization targets

Goal: Theorem 3.1 (online gradient descent regret)

using step sizes $\eta_t = D / (G\sqrt{t})$. This is the chapter's — and arguably the book's — central result: the simplest algorithm for the fully general OCO protocol already attains $O(\sqrt{T})$ regret, with an explicit small constant, against convex Lipschitz costs with no further structure.

Milestone: Theorem 3.2 (matching lower bound)

Any algorithm for OCO incurs $\Omega(DG\sqrt{T})$ regret in the worst case: no algorithm, however clever, can improve asymptotically on Theorem 3.1's rate. This is the weaker, worst-case-existence half of the theorem (see Formalization scope).

Milestone: Theorem 3.3 (logarithmic regret under strong convexity)

If every $f_t$ is additionally $\alpha$-strongly convex, the same algorithm — with only the step sizes changed to $\eta_t = 1/(\alpha t)$ — achieves

Strong convexity is a strictly stronger hypothesis than convexity, so this target does not subsume the goal; it sits alongside it as the chapter's second, sharper regime.

Significance

Theorem 3.1 is the reference point against which every later algorithm and every later chapter's improvement (Online Newton Step, RFTL, adaptive-regret methods) is measured: any new algorithm for OCO is judged first by whether it matches this $O(\sqrt{T})$ rate, then by what extra structure lets it do better. Theorem 3.2 closes the question for the general convex-Lipschitz class: $O(\sqrt{T})$ is not an artifact of a loose analysis, it is information-theoretically necessary. Theorem 3.3 identifies the one extra hypothesis (strong convexity) that buys an exponential improvement in the horizon dependence, from $\sqrt{T}$ to $\log T$, without any other change to the algorithm — the same phenomenon that in the book's Chapter 2 separated well-conditioned from general convex offline optimization, now transplanted to the online, adversarial setting.

None of these three statements has a machine-checked proof on the platform prior to this mission (see Formalization scope below for what was checked). Formalizing them establishes the regret protocol and the OGD algorithm as reusable definitions for the rest of this thirteen-chapter series, several chapters of which (Online Newton Step, RFTL, bandit convex optimization) build directly on Algorithm 8 or its regret guarantee.

Difficulty

The regret bound's proof (Theorem 3.1) is short but not naive: bounding $\nabla_t^\top(x_t - x^\star)$ by convexity alone gives no telescoping structure, so the argument instead bounds it using the projection step — the Pythagorean inequality $\|\Pi_K(z) - x^\star\| \le \|z - x^\star\|$ for $x^\star \in K$ — applied to the specific point $z = x_t - \eta_t \nabla_t$. This turns the per-round convexity bound into a telescoping sum in $\|x_t - x^\star\|^2$, and only the resulting sum, evaluated with the specific step-size schedule $\eta_t = D/(G\sqrt{t})$, produces the $\sqrt{T}$ rate; a constant or linearly growing step size does not. The same projection argument is reused for Theorem 3.3, where the strong-convexity inequality is engineered to make the $\|x^\star - x_t\|^2$ terms cancel exactly against the projection telescoping, leaving a harmonic sum. Theorem 3.2's difficulty is of a different kind: it is a lower bound over every algorithm, proved by exhibiting a randomized hard instance (the hypercube with $2^n$ sign-vector linear costs) on which no algorithm can do better than random guessing in expectation.

Formalization scope

$K$ is formalized as a subset of an arbitrary real, complete inner product space (not fixed to $\mathbb{R}^n$), since the chapter's argument uses only Hilbert-space structure. Rounds are 0-indexed (Finset.range T) rather than the book's 1-indexed rounds, so a step size stated here at round $t$ is the book's step size at round $t+1$. D and G are carried as shared section hypotheses (the chapter-wide diameter and gradient-norm bounds), not re-derived or re-stated per theorem; G is formalized exactly as the book defines it (p. 20: a bound on $\|\nabla f_t(x)\|$ over $K$, via Mathlib's HasGradientAt), not as the weaker two-point Lipschitz condition it implies — an earlier draft used the weaker Lipschitz hypothesis and was corrected during moderation, since it made the drafted theorems strictly stronger than the book's own (true by an added argument the book does not give, but not faithful to the stated proof). The projection step is formalized relationally (IsMetricProjection, an arbitrary closest point) rather than as a canonical function, since a general convex set need not come with one built into Mathlib.

For Theorem 3.2, this mission formalizes the theorem's main sentence — the worst-case existence claim — quantifying over "any algorithm" as a non-anticipating map from the full cost sequence to the play sequence, with the hard cost sequence existentially quantified after the algorithm and the horizon: for every algorithm and every horizon there is a cost sequence forcing $\Omega(DG\sqrt{T})$ regret against it. (An earlier draft quantified the cost sequence first — one fixed sequence defeating every algorithm — which is false: a constant algorithm playing a minimizer of that one sequence has zero regret against it; this was corrected during moderation.) It does not formalize the theorem's parenthetical strengthening, that the same $\Omega(DG\sqrt{T})$ bound holds even when costs are drawn from a fixed stationary distribution; that claim is about expected regret of a deterministic algorithm against a random cost sequence, and would need a probability-space formalization of the OCO protocol that this mission's definitions do not build. A formalization limited to the deterministic worst case does not trivialize the theorem: it is exactly the inequality "$O(\sqrt{T})$ cannot be improved," stated without the randomization machinery of its proof.

Theorem 3.4 (the stochastic gradient descent corollary, via a noisy gradient oracle with bounded second moment) is not included: it needs an expectation over a random oracle applied at a random, round-dependent point, which is a substantially heavier probabilistic object than the deterministic protocol built here, and is left for a future mission or an extension of this one.

Selected references

• Zinkevich, M. Online Convex Programming and Generalized Infinitesimal Gradient Ascent. ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf
• Kivinen, J. and Warmuth, M. K. Exponentiated Gradient Versus Gradient Descent for Linear Predictors. Information and Computation, 1997. https://doi.org/10.1006/inco.1996.2612
• Hazan, E., Agarwal, A. and Kale, S. Logarithmic Regret Algorithms for Online Convex Optimization. Machine Learning 69, 2007. https://doi.org/10.1007/s10994-007-5016-8
• Hazan, E. Introduction to Online Convex Optimization, 2nd ed. arXiv:1909.05207v3, Chapter 3. https://arxiv.org/abs/1909.05207

Motivation

Decision-making problems rarely present the same fixed choice twice. A doctor prescribing a treatment sees each patient's medical history and symptoms before deciding; a website choosing which article to show sees the visitor's profile first. The multi-armed bandit model — where the learner repeatedly picks from a fixed set of arms with no side information — cannot express this: it is blind to the covariates that any real decision-maker actually observes. The contextual bandit model closes this gap by letting the learner see a context before acting, and asks for a decision rule that generalizes across contexts rather than memorizing a policy per context. Foster and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making (arXiv:2312.16730v1, Section 3, pp. 38–53) develops this model and its algorithms as the bridge between supervised learning and sequential decision making, en route to general reinforcement learning. Contextual bandits with a learned reward-function class underlie production systems for content recommendation, online advertising, and adaptive clinical trial design (Li et al., A Contextual-Bandit Approach to Personalized News Article Recommendation, 2010, https://arxiv.org/abs/1003.0146; Agarwal et al., Making Contextual Decisions with Low Technical Debt, 2016, https://arxiv.org/abs/1606.03966).

The algorithmic history in this chapter runs through two distinct principles. The optimism principle (LinUCB, Section 3.2) generalizes the UCB algorithm to contexts under a linear reward model, but the chapter's own Example 3.1 (Section 3.3) shows optimism fails outside such structured classes, incurring regret linear in the size of the context space or the class. Foster and Rakhlin then present two "black-box" alternatives that use any function class $F$ through an abstract regression subroutine: the naive $\varepsilon$-Greedy method (Section 3.4), and the Inverse Gap Weighting (IGW) strategy underlying the SquareCB algorithm (Bietti, Agarwal & Langford, A Contextual Bandit Bake-off, 2018, https://arxiv.org/abs/1802.04064; Foster & Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles, 2020, https://arxiv.org/abs/2002.04926). SquareCB attains a regret rate that both generalizes across contexts (no dependence on the size of the context space) and matches the optimal $\sqrt{T}$ rate — improving on $\varepsilon$-Greedy's $T^{2/3}$ rate — while remaining agnostic to the internal structure of $F$.

Setting

Over $T$ rounds, a decision-maker faces the contextual bandit protocol: at each round $t$, it observes a context $x_t \in X$, selects a decision $\pi_t$ from a finite action set $\Pi = \{1,\dots,A\}$, and observes a reward $r_t \in \mathbb{R}$. Rewards are generated independently as $r_t \sim M^\star(\cdot \mid x_t, \pi_t)$ for a fixed, unknown conditional model $M^\star$; write $f^\star(x,\pi) := \mathbb{E}[r \mid x, \pi]$ for the mean reward function and $\pi^\star(x) := \arg\max_\pi f^\star(x,\pi)$ for the optimal, context-dependent policy. The context sequence $x_1,\dots,x_T$ is arbitrary — fixed in advance or adversarially chosen — while rewards remain stochastic. Performance is measured by regret against $\pi^\star$:

where $p_t$ is the learner's (possibly randomized) action distribution at round $t$.

To generalize across contexts, the learner is given a class $F \subseteq \{f : X\times\Pi \to \mathbb{R}\}$ with $f^\star \in F$, and aims for regret scaling with the statistical complexity $\log|F|$ rather than with $|X|$. Both algorithms in this mission access $F$ only through an online regression oracle (Definition 3, p. 47): given the history $(x_1,\pi_1,r_1),\dots,(x_{t-1},\pi_{t-1},r_{t-1})$, it returns an estimate $\hat f_t : X\times\Pi\to\mathbb{R}$ satisfying, with probability at least $1-\delta$, $\sum_{t=1}^T \mathbb{E}_{\pi_t\sim p_t}[(\hat f_t(x_t,\pi_t)-f^\star(x_t,\pi_t))^2] \le \mathrm{EstSq}(F,T,\delta)$ — for instance, exponential weights on a finite class $F$ achieves $\mathrm{EstSq}(F,T,\delta) = \log(|F|/\delta)$. SquareCB (p. 50–51) then samples its action from the Inverse Gap Weighting distribution (Definition 4, p. 50): given a vector of estimated values $\hat f \in \mathbb{R}^A$ with greedy action $\bar\pi = \arg\max_\pi \hat f(\pi)$, and an exploration parameter $\gamma \ge 0$, $p = \mathrm{IGW}_\gamma(\hat f)$ is $p(\pi) = 1/(\lambda + 2\gamma(\hat f(\bar\pi)-\hat f(\pi)))$ for the unique $\lambda \in [1,A]$ making $p$ a probability distribution.

Formalization targets

Milestone — Proposition 9 (IGW estimation-to-regret inequality)

This holds for any $\hat f, f^\star \in \mathbb{R}^A$ and any $\gamma>0$, with no reference to $F$ or to how $\hat f$ was produced — it is the purely algebraic core the goal theorem invokes at every round.

Goal — Proposition 10 (SquareCB regret bound)

with probability at least $1-\delta$, for SquareCB run with $\gamma = \sqrt{TA/\mathrm{EstSq}(F,T,\delta)}$, for any context sequence $x_1,\dots,x_T$. This is the weakest stable target level in the chapter's oracle-based development: it is stated for an arbitrary class $F$ and oracle, so it survives any future improvement to the oracle's own $\mathrm{EstSq}$ bound, unlike a version hard-coded to a specific class or oracle.

Significance

Proposition 10 shows that Inverse Gap Weighting converts any estimation-error guarantee into a regret guarantee with the same statistical rate, with no algorithm-side dependence on the structure of $F$ or the size of $X$: the same SquareCB template, driven by a plug-in regression oracle, is minimax optimal whenever the oracle itself is. When $F$ is finite, this yields $\mathrm{Reg} \lesssim \sqrt{AT\log(|F|/\delta)}$, matching the optimal rate for stochastic multi-armed bandits (Section 2) while generalizing across contexts — a guarantee that optimism (Proposition 7) provably cannot deliver outside linear classes (Example 3.1), and that the simpler $\varepsilon$-Greedy baseline (Proposition 8) only delivers at a slower $T^{2/3}$ rate. Foster and Rakhlin describe Proposition 9 itself as being "at the core of the development for the rest of the course": the same IGW mechanism reappears, generalized, in the book's treatment of general decision-making and the Decision-Estimation Coefficient.

Both propositions are proved results, not open questions; this mission's contribution is a machine-checked formalization of their exact statements and hypotheses — the precise OracleGuarantee hypothesis Proposition 10 requires, the exact constant ($2$, not a bare $\lesssim$) its proof yields at the stated optimal $\gamma$, and the universally-quantified form of the IGW inequality (Proposition 9) that makes it reusable independently of any particular oracle or class.

Difficulty

The obvious first idea for exploiting an estimator $\hat f_t$ is a UCB-style optimism approach: build a confidence set around $\hat f_t$ and act greedily on its upper envelope, as in LinUCB (Proposition 7). Example 3.1 shows this fails in general: a class $F$ can force the confidence set to remain wide on a fresh action at every new context, driving regret linear in $\min\{|F|,|X|\}$ — the confidence width in the regret bound does not shrink merely because the oracle's cumulative estimation error is small, since that error is not localized to the specific action the confidence-set approach tries next. Uniform exploration ($\varepsilon$-Greedy) sidesteps this but wastes exploration budget on actions already known to be far from optimal, which is what caps its rate at $T^{2/3}$ (Proposition 8). Inverse Gap Weighting instead ties the sampling probability itself to the estimated gap from the greedy action, so cheap-to-rule-out actions are down-weighted continuously rather than either fully explored (ε-Greedy) or trusted outright (optimism); the technical content of Proposition 9 is showing this specific reciprocal-gap form gives a bound with no hidden dependence on $F$ or $X$, for every pair $(\hat f, f^\star)$ simultaneously — a guarantee optimism cannot match because its confidence sets are class-dependent by construction.

Formalization scope

Contexts form an arbitrary type X; actions are Fin A for A : ℕ. A finite probability distribution over Fin A is represented directly as p : Fin A → ℝ with ∀ π, 0 ≤ p π and ∑ π, p π = 1, and $\mathbb{E}_{\pi\sim p}[g]$ as the finite sum ∑ π, p π * g π, rather than via Mathlib's PMF (which is ℝ≥0∞-valued) — an equivalent and lighter-weight representation of a distribution on a finite type. The normalizing constant $\lambda$ of Definition 4 and the optimal actions $\pi^\star$, $\bar\pi$ are each specified by their defining property (existence of $\lambda \in [1,A]$ realizing the IGW formula; $\forall\pi, f(\pi)\le f(\text{argmax})$) rather than constructed explicitly via an intermediate-value or Finset.argmax argument, avoiding committing to one choice function for a value the book itself leaves implicit. The class $F$ enters neither proposition's statement directly: it appears in the source only through the abstract bound $\mathrm{EstSq}(F,T,\delta)$, which is carried as an explicit real-valued parameter and hypothesis (OracleGuarantee) rather than as a literal subset of a function space, since no property of $F$ beyond producing this bound is ever used. The probability-$(1-\delta)$ qualifier attached to the online regression oracle's guarantee is likewise the explicit hypothesis OracleGuarantee ... EstSq on a fixed realized run, rather than a statement quantified over an underlying probability space of histories — every subsequent step in both propositions' proofs is deterministic given that this event holds, so this does not weaken either conclusion. A trivializing formalization would fix $A=1$ (a single ever-optimal action, making both Reg and the IGW inequality vacuous) or take EstSq as an unconstrained free variable with no positivity hypothesis (making $\gamma$ in Proposition 10 undefined); this mission's statements require 0 < EstSq and leave $A$, $T$, $X$, $F$-via-EstSq fully general.

This mission omits Proposition 7 (LinUCB): its proof rests on an entirely disjoint apparatus (finite linear parameter sets, least-squares confidence sets, the elliptic potential lemma) that neither Proposition 9 nor 10 requires, and Example 3.1 (the failure of optimism) is a worked example rather than a numbered, formalizable claim. It also omits Proposition 8 ($\varepsilon$-Greedy): the source leaves the optimal $\varepsilon$ unspecified ("choosing $\varepsilon$ appropriately"), and deriving its own optimal value and matching constant independently — rather than reusing the book's own explicit constant, as Rule 7 of this formalization effort requires — was judged too likely to introduce an unfaithful, invented constant within this mission's time budget; both are natural extensions for a follow-up mission or contribution. Reusable infrastructure: the Fin A-indexed finite-distribution convention and the OracleGuarantee/optimal-action-by-property pattern extend directly to any later chapter built on the same online-regression-oracle abstraction.

Selected references

• Foster, D. J. and Rakhlin, A. Foundations of Reinforcement Learning and Interactive Decision Making. 2023. https://arxiv.org/abs/2312.16730
• Foster, D. J. and Rakhlin, A. Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles. ICML 2020. https://arxiv.org/abs/2002.04926
• Bietti, A., Agarwal, A., and Langford, J. A Contextual Bandit Bake-off. JMLR 2021 (arXiv 2018). https://arxiv.org/abs/1802.04064
• Li, L., Chu, W., Langford, J., and Schapire, R. E. A Contextual-Bandit Approach to Personalized News Article Recommendation. WWW 2010. https://arxiv.org/abs/1003.0146
• Agarwal, A. et al. Making Contextual Decisions with Low Technical Debt. 2016. https://arxiv.org/abs/1606.03966

Motivation

The multi-armed bandit is the simplest model of sequential decision-making under partial feedback: a learner repeatedly picks one of finitely many options and observes a reward only for the option chosen, never for the alternatives. It formalizes problems ranging from clinical trial design (which treatment to offer a patient) to online advertising (which ad to show) and A/B testing more generally. The framework dates to Robbins' 1952 paper on sequential design, and the algorithm this mission's goal theorem concerns — the Upper Confidence Bound (UCB) algorithm of Lai and Robbins [1985] and Auer, Cesa-Bianchi and Fischer [2002] — is the canonical answer to how to explore efficiently: instead of exploring uniformly at random, act optimistically with respect to the current uncertainty about each option's value. This mission draws its formalization from Chapter 2 of Foster and Rakhlin's 2023 lecture notes, Foundations of Reinforcement Learning and Interactive Decision Making, which develops the bandit problem as the first rung of a ladder of increasingly general interactive decision-making settings (contextual bandits, structured bandits, reinforcement learning) that the book's later chapters build.

Setting

Fix a finite decision (action) space $\Pi = \{1,\dots,A\}$. In the multi-armed bandit protocol, for each round $t = 1,\dots,T$ the learner selects a decision $\pi_t \in \Pi$, possibly at random according to a distribution $p_t$ depending on the history $H_{t-1} = ((\pi_1,r_1),\dots,(\pi_{t-1},r_{t-1}))$ observed so far, and then observes a reward $r_t \in \mathbb{R}$ drawn independently from a fixed conditional distribution $M^\star(\cdot \mid \pi_t)$ (the stochastic rewards assumption). Writing $f^\star(\pi) := \mathbb{E}[r \mid \pi]$ for the mean reward function and $\pi^\star := \arg\max_\pi f^\star(\pi)$ for an optimal decision, the learner's performance is measured by the regret

Because the learner observes a reward only for the action played (bandit feedback), a purely greedy strategy that always plays the current empirical maximizer can commit to a suboptimal action forever, incurring linear regret; some form of deliberate exploration is necessary. The chapter's central construction is the confidence interval: a pair of functions $\underline{f}_t, \bar f_t : \Pi \to \mathbb{R}$ such that, with probability at least $1-\delta$, $f^\star(\pi) \in [\underline{f}_t(\pi), \bar f_t(\pi)]$ for every round $t$ and decision $\pi$ simultaneously. The UCB algorithm plays the optimistic action $\pi_t = \arg\max_\pi \bar f_t(\pi)$ at every round, using the confidence interval built from Hoeffding's inequality around the empirical mean $\hat f_t(\pi)$.

Formalization targets

Goal — Proposition 5 (UCB regret)

holding with probability at least $1-\delta$, for the UCB algorithm using the confidence radius $\sqrt{2\log(2T^2A/\delta)/n_t(\pi)}$ of Eq. (2.19). This is the weakest stable statement the chapter proves: it is optimal up to the log factor, and strengthening it (e.g. to the sharper instance-dependent bound of Remark 10) is explicitly left to later work by the book itself.

Milestones

• Proposition 4 (ε-Greedy regret): $\mathrm{Reg} \lesssim A^{1/3}T^{2/3}\log^{1/3}(AT/\delta)$ — the book's preceding, weaker result, establishing that naive forced exploration already gives sublinear regret, and motivating why an adaptive strategy (UCB) does better.
• Lemma 7 (Optimism): the per-round regret of the optimistic action is bounded by the confidence width at that action.
• Lemma 8 (Confidence width potential lemma): $\sum_{t=1}^T (1/\sqrt{n_t(\pi_t)} \wedge 1) \lesssim \sqrt{AT}$, a pigeonhole bound on how often any one action's confidence interval can still be wide.

Significance

UCB is the prototype of the "optimism in the face of uncertainty" principle that recurs, in increasingly abstract form, throughout the rest of the book: the same two-step argument (Lemma 7 + Lemma 8) reappears for linear bandits, structured bandits via the Decision-Estimation Coefficient, and UCB-VI for tabular reinforcement learning. Formalizing Chapter 2 in full therefore front-loads the proof pattern every later chapter in this series specializes. The result itself is also of standalone interest: the $\sqrt{AT}$ minimax rate is the benchmark every subsequent bandit algorithm in the literature is compared against, and the $A^{1/3}T^{2/3}$-vs-$\sqrt{AT}$ contrast between ε-Greedy and UCB is the standard illustration, in any course on the subject, of why adaptive exploration matters.

No formalization of this exact statement — realizability with respect to a function class $f^\star \in \mathcal{F} = \mathbb{R}^\Pi$ and a generic confidence interval, rather than a per-arm sub-Gaussian empirical mean — currently exists on the platform (see Formalization scope below); the mission both proves this specific regret bound and seeds the generic optimism/potential lemma pair (Lemma 7, Lemma 8) that the book's later, more structured settings specialize.

Difficulty

The natural first attempt — bound the regret of the empirical-mean-greedy algorithm directly — fails outright: on a two-armed instance where one arm is deterministic and the other only slightly better in expectation, the greedy algorithm can commit to the worse arm forever with constant probability, giving linear, not sublinear, regret (§2.1). The obvious fix, ε-Greedy, forces exploration uniformly across all actions regardless of how much is already known about each, so the exploration cost scales with $\varepsilon T$ even for actions whose value is already well determined — this is exactly what caps ε-Greedy at the $T^{2/3}$ rate. UCB's optimism principle resolves this by exploring an action only in proportion to how uncertain it still is; the technical core, isolated in Lemma 7 and Lemma 8, is disentangling "the algorithm made a mistake" from "the algorithm is still uncertain," which are conflated in the naive per-round regret decomposition used for ε-Greedy.

Formalization scope

Both the goal and the milestones fix a finite decision space Fin A, a mean reward function fStar : Fin A → ℝ with fStar π ∈ [0,1], and an optimal decision piStar. Regret is defined generically (Eq. (2.3)) via per-round decision weights p : ℕ → Fin A → ℝ, so it applies uniformly to a randomized algorithm (ε-Greedy) and a deterministic one (UCB, via the point mass at the played action). The book's "with probability at least $1-\delta$" qualifier on both Proposition 4 and Proposition 5 is formalized as the deterministic consequence of the underlying concentration event (Eq. (2.9) and Eq. (2.18) respectively) holding — exactly the move the book's own proofs make ("Let us condition on the event in (2.18) ... "). The concentration events themselves rest on Hoeffding's inequality for adaptive stopping times (Lemma 33) and Bernstein's inequality (Lemma 5), both stated in the book's technical appendix outside this chapter, and are not drafted here; a solver may either take them as a hypothesis (as this mission's statements do) or import/prove them separately. A trivializing formalization is ruled out explicitly: taking δ outside $(0,1)$, or dropping the fStar π ∈ [0,1] hypothesis, would make the stated constants vacuous or false, so both are retained as explicit hypotheses in every theorem. In every ≲ statement (Prop. 4, Lemma 8, Prop. 5) the witnessed constant C is quantified before the instance parameters (A, T, δ, and the realized sequences): ∃ C, 0 < C ∧ ∀ A T δ ..., Reg ≤ C * (rate), not the other order. This is deliberate, not stylistic: quantifying C after the instance lets it depend on A, T, δ, making the bound satisfiable by an arbitrarily large C chosen per instance and hence content-free, which is not what the book's ≲ means (a single constant working uniformly over all instances). Proposition 5's UCB decision rule is stated in the book's own two clauses, not collapsed into a single "maximize the upper confidence bound" rule: the confidence radius of Eq. (2.19) is $+\infty$ at $n_t(\pi)=0$ (an action never yet sampled), so the book's UCB always plays an unsampled action before ever comparing indices, and only compares finite upper confidence bounds once every action has been sampled at least once; the confidence event of Eq. (2.18) is correspondingly assumed only at sampled actions, since the book's own bound is vacuous otherwise. An earlier draft instead capped the radius at $1$ when $n_t(\pi)=0$, which is a true statement about a different algorithm (a sampled action can have index above the capped unsampled index), and was corrected to the book's own rule after moderation. Reuse from the platform's existing bandit library (BanditAlgorithm, Lattimore & Szepesvári) is deliberately avoided: that library's UCB (bandit_ucb_regret_bound, bandit_ucb_minimax_regret_bound) is stated for per-arm 1-sub-Gaussian rewards with $\delta = 1/n^2$ fixed by the horizon, whereas this chapter's UCB is stated for a free failure probability $\delta$ and a generic confidence-interval abstraction (the multi-armed case being $\mathcal{F} = \mathbb{R}^\Pi$ of the book's general realizability framework) — the two are related but not the same statement. Contributions extending the mission with the generic confidence-interval form of Lemma 7/8 applied to other chapters in this series (contextual and structured bandits) are welcome.

Selected references

• T. Lai and H. Robbins, Asymptotically Efficient Adaptive Allocation Rules, Advances in Applied Mathematics, 1985.
• P. Auer, N. Cesa-Bianchi, and P. Fischer, Finite-time Analysis of the Multiarmed Bandit Problem, Machine Learning, 2002.
• D. Foster and A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, arXiv:2312.16730, 2023. https://arxiv.org/abs/2312.16730
• T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020.

Motivation

An LLM agent acting in an environment spends most of its wall-clock time waiting. Each step — a model call, a tool or MCP request, a browser action, sometimes a human reply — must complete before the next can be issued, and the round trips dominate end-to-end latency: a chess game between two reasoning agents runs for hours, and an operating-system tuning task for tens of minutes. When a training or prompt-optimization loop repeats such a run thousands of times, the waiting is the cost.

Speculative actions (Ye, Ahuja, Liargkovas, Lu, Kaffes, Peng, ICLR 2026) transplants a classical systems idea — speculative execution in microprocessors, and speculative decoding for LLM inference — to the agent's environment loop. A cheap, fast speculator guesses the action a slow, authoritative actor is about to produce, the guess is used to launch the next environment call early, and the work is committed only when the actor's real action confirms the guess. The interface stays sequential and lossless; the internals run in parallel.

What makes this a formalization target rather than an engineering report is the paper's §5 cost–latency analysis. Speculating more branches buys hit probability but costs tokens, and the paper derives closed-form expressions for both sides of that trade — a self-contained piece of applied probability sitting underneath a systems paper. This mission asks for those expressions, machine-checked.

Setting

Fix a horizon $T$ and index steps $t = 0, 1, \dots, T-1$. At each step a policy maps the state to an API call; the actor executes it with latency $\mathrm{Exp}(\beta)$, while the speculator proposes candidate actions with latency $\mathrm{Exp}(\alpha)$, where $\beta < \alpha$ (the speculator is faster in expectation). A speculative branch hits when the action it guesses implies the same next call the actor's true action would have implied; branches hit independently across steps with probability $p$.

Two knobs define the two regimes analyzed. Breadth $k$: at each step, launch $k$ independent one-step speculations in parallel, each immediately followed by a real call. At least one of the $k$ succeeds with probability

Depth: follow a single branch, extending it whenever a speculative or real call returns and pruning subtrees the actor contradicts.

The quantity driving both results is $S_n$, the expected number of hits by round $n$. A hit consumes the following step's speculation window — after a correct guess the next call is already cached, so no new speculation is launched there — which yields the two-term recursion

Write $T_{\mathrm{seq}}, M_{\mathrm{seq}}$ for the latency and token cost of strictly sequential execution, and $T_{\mathrm{spec}}, M_{\mathrm{spec}}$ for their speculative counterparts. In the depth regime latencies are taken deterministic: $a$ for a real call, $b < a$ for a speculative one.

Target

The goal theorem is the finite-horizon latency ratio for breadth-focused speculation (Proposition 1), with $p(k)$ abbreviated $p_k$:

The supporting targets, ordered as the analysis builds them:

1. the closed form $S_n = \frac{p}{1+p}n + \frac{p^2}{(1+p)^2}\bigl(1 - (-p)^n\bigr)$ solving the recursion;
2. the per-hit saving $\mathbb{E}[(B-A)^+] = \frac{\alpha}{\beta(\alpha+\beta)}$ for independent $A \sim \mathrm{Exp}(\alpha)$, $B \sim \mathrm{Exp}(\beta)$;
3. the $T \to \infty$ limit $1 - \frac{p_k}{1+p_k}\cdot\frac{\alpha}{\alpha+\beta}$, and the resulting 50% ceiling: the latency reduction is strictly below $\tfrac12$ for every $p_k \le 1$;
4. the cost counterpart (Theorem 4), finite-horizon and in the limit, with $\tilde k$ the number of distinct actions across the $k$ branches;
5. the depth-focused time and cost identities (Theorem 6), whose latency coefficient is $p$ rather than $\frac{p}{1+p}$ — raising the speedup ceiling from $\tfrac12$ to $1$;
6. the structure of confidence-aware selective speculation (Theorem 3 and Corollary 5): with sorted per-branch confidences, the marginal hit-probability gain is non-increasing, so the optimal breadth is the greedy threshold rule "add a branch while $\Delta^\star \delta q(m) \ge c$".

Significance

The analysis is what turns speculation from a trick into a tunable system. Proposition 1 and Theorem 4 are governed by the same quantity $p_k$, so a practitioner who can estimate hit probability can choose $k$ offline against a latency/cost budget rather than by trial. The 50% ceiling is a genuine negative result — it says breadth alone cannot do better, and motivates the depth regime, where the ceiling becomes 1. Theorem 3 explains why confidence-based branch selection is cheap in practice: the whole dynamic program collapses to one scalar continuation value, so a runtime system sorts confidences and adds branches greedily in $O(k)$ per step.

The paper's proofs are pen-and-paper and, as far as we are aware, none of these results has a machine-checked proof. Three parts reward formalization specifically. The recursion's closed form is derived by a characteristic-equation argument with a particular solution that collides with the homogeneous part — routine but error-prone. The per-hit saving is an honest two-dimensional integral over independent exponentials. And Theorem 6's cost expression is stated in the paper with a floor function and then immediately replaced by an approximation, so formalizing it forces a decision about which claim is actually being asserted (see Formalization scope).

Difficulty

The obvious first move on the recursion — guess a constant particular solution — fails, because $r = 1$ is a root of the characteristic polynomial $r^2 - (1-p)r - p$ and a constant trial collides with the homogeneous family; the particular solution is linear in $n$, and the $\frac{p^2}{(1+p)^2}$ coefficient comes out of matching both initial conditions, not one.

The interesting hypothesis is the one the recursion's shape encodes and the prose states only in passing: a hit at round $t$ removes the speculation window at round $t+1$. Drop it and the recursion becomes one-term and the answer changes.

For the per-hit saving, the difficulty is analytic rather than algebraic: the inner antiderivative of $(b-a)\alpha e^{-\alpha a}$ must be handled, and the outer integral runs over an unbounded interval, so integrability has to be established rather than assumed.

The asymptotic statements need the oscillating term $(-p_k)^{T-1}$ controlled uniformly — it is bounded, not vanishing termwise in an obvious way — before the $\tfrac1T$ prefactor can be taken to zero.

Formalization scope

Everything is over $\mathbb{R}$. The model lives in one definition bundle, Def_SpecActions_model, in namespace SpecActions; the mission's Lean names match the prose symbols ($S_n$ is hits, $p(k)$ is phit, $\tilde k$ is kt).

The model is formalized at the level the paper's own proofs use: $\mathbb{E}[T]$ and $\mathbb{E}[M]$ are defined by the expressions Appendix A derives for them (specTime, specCost, and their depth analogues), and the theorems assert the algebraic and asymptotic identities relating those quantities. Deriving those expressions from a measure-theoretic model of the execution trace is deliberately not in scope — with one exception: milestone 2 states the per-hit saving as a genuine iterated integral against the exponential densities, so the one probabilistic step the paper actually computes is formalized as an integral rather than assumed.

Conventions a solver should know before starting:

• Statements are quantified over $\alpha, \beta > 0$ and $0 \le p_k \le 1$; the standing assumption $\beta < \alpha$ is not imposed, since none of the identities need it.
• Finite-horizon statements carry $1 \le T$, and $T-1$ is natural-number subtraction — the $T = 0$ case is excluded rather than silently truncated.
• hits takes $p_k$ (the per-step hit probability $p(k)$), not the per-branch $p$; phit relates the two, and Thm_SpecActions_phit_bounds supplies the $0 \le p(k) \le 1$ range facts the other statements assume.
• Theorem 6's cost is stated as the exact identity, not the paper's approximation. The paper gives an exact expression involving $\lfloor a/b \rfloor$ and then an $\approx$ form with $\frac{a}{2b} - \frac12$; these coincide only when $a/b$ is an integer. The milestone asserts the exact floor version, which is what the proof establishes.
• The 50% ceiling is stated as the strict bound $\frac{p_k}{1+p_k}\cdot\frac{\alpha}{\alpha+\beta} < \frac12$, which holds for all admissible parameters; the paper's "upper bound of 50%, occurring when $p=1$ and $\alpha = \infty$" describes an unattained supremum.
• Theorem 3's dynamic program is formalized as the two facts that carry its content — diminishing marginal returns, and optimality of the greedy threshold breadth — rather than as a Bellman recursion over a mode process, which would require a full MDP development.

Reusable beyond this mission: the two-term linear recursion solved in milestone 1, and the $\mathbb{E}[(B-A)^+]$ computation for independent exponentials, which is a standard fact absent from Mathlib. Contributions extending the model toward an actual measure on execution traces — deriving specTime rather than defining it — are welcome as follow-on work.

Selected references

• Naimeng Ye, Arnav Ahuja, Georgios Liargkovas, Yunan Lu, Kostis Kaffes, Tianyi Peng. Speculative Actions: A Lossless Framework for Faster Agentic Systems. ICLR 2026. arXiv:2510.04371 — Proposition 1 (p. 4), Appendix A (pp. 13–14), Theorem 3 (p. 10), Theorem 4 (p. 19), Corollary 5 (p. 22), Theorem 6 (p. 23).
• Yaniv Leviathan, Matan Kalman, Yossi Matias. Fast Inference from Transformers via Speculative Decoding. ICML 2023. arXiv:2211.17192 — the speculate-verify pattern at token level.
• Wenyue Hua, Mengting Wan, Shashank Vadrevu, Ryan Nadel, Yongfeng Zhang, Chi Wang. Interactive Speculative Planning. 2024. arXiv:2410.00079 — depth-oriented speculation on a single planning branch.
• Yilin Guan et al. Dynamic Speculative Agent Planning. 2025. arXiv:2509.01920 — online RL for choosing speculation depth under a cost-latency trade-off.
• Robert M. Tomasulo. An Efficient Algorithm for Exploiting Multiple Arithmetic Units. IBM Journal of Research and Development, 1967. DOI:10.1147/rd.111.0025 — speculative execution in hardware.

Beneath Exp3, Exp4 and their relatives lies one algorithm: minimize past losses plus a convex regularizer. Chapters 26–28 of Lattimore–Szepesvári develop this unifying view. For a Legendre potential $F$ with Bregman divergence $D_F$, both mirror descent and follow-the-regularised-leader satisfy the master bound $R_n(a) \le \frac{F(a) - F(a_1)}{\eta} + \frac{1}{\eta}\sum_t D_F(a_t, \tilde a_{t+1})$; the negentropy potential on the simplex recovers Exp3 exactly. The goal theorem is the payoff for adversarial linear bandits: FTRL on the unit ball with the self-concordant-flavoured potential $F(a) = -\log(1-\|a\|) - \|a\|$ achieves $R_n \le 2\sqrt{3nd\log n}$ — improving the $\sqrt{d}$ factor over the Exp3-style approach of Chapter 27 and matching the $\Omega(d\sqrt{n})$ lower bound of Mission XI up to logarithms.

Real decisions come with context: a news site chooses an article for a particular user. Competing with the single best arm is then meaningless; the right benchmark is the best mapping from contexts to arms, or more generally the best of $M$ expert policies. Chapter 18 of Lattimore–Szepesvári formalizes this via Exp4 — exponential weighting over experts, fed by the importance-weighted estimator of Mission V. The goal theorem: with learning rate $\eta = \sqrt{2\log(M)/(nk)}$, Exp4 satisfies $R_n \le \sqrt{2nk\log M}$ against the best of $M$ experts. Since $M$ enters only logarithmically, the learner can compete with exponentially large policy classes — the conceptual gateway from bandits to reinforcement learning with function approximation.