Machine Learning

Why moving comparators matter

In online learning, a learner chooses a point before seeing each round's loss. Ordinary regret compares the learner with one fixed point chosen after all rounds. That comparison can be too coarse when a useful action changes over time. A portfolio allocation, a prediction rule, or an operating point may need to move after the environment shifts. Dynamic regret compares the learner with a specified sequence of feasible points, one for each round. The sequence is allowed to move, but its movement appears explicitly in the bound. Chapter 14 of Orabona's Online Learning: A Modern Introduction Using Convex Optimization develops this comparison, then studies strongly adaptive and tracking regret. This mission isolates its first capstone, Theorem 14.2.

The result extends the book's earlier analysis of online mirror descent to changing comparators. As the chapter explains, a moving comparator can achieve a smaller cumulative loss than any single fixed point, so a dynamic bound answers a stricter performance question. The bound also makes its own limit clear: frequent or large comparator changes cost more. The chapter relates this framework to earlier work on drift in online learning; the formal target here is the precise statement in the pinned arXiv version, with its explicit constants and final Bregman term. Source, Chapter 14, pp. 227–229.

Setting and notation

Let $E$ be a finite-dimensional real normed space, $V\subseteq X\subseteq E$, and $V$ a nonempty closed convex feasible set. On round $t=1,\ldots,T$, the learner plays $x_t\in V$, receives a real-valued loss $\ell_t$, and selects a subgradient $g_t$ at $x_t$. A comparison sequence $u_1,\ldots,u_T$ consists of arbitrary points in $V$. The dynamic regret is

$$\operatorname{DRegret}_T(u_1,\ldots,u_T) =\sum_{t=1}^{T}\bigl(\ell_t(x_t)-\ell_t(u_t)\bigr).$$

The path length of the comparison sequence is the total distance between successive points:

$$P(u_1,\ldots,u_T)=\sum_{t=2}^{T}\lVert u_t-u_{t-1}\rVert.$$

It is zero for a constant sequence. The path starts at round two, so neither $u_0$ nor an artificial first movement enters the claim. The norm on $E$ is arbitrary. Its dual norm on continuous linear functionals is written $\lVert\cdot\rVert_*$.

Online mirror descent uses a differentiable regularizer $\psi$ and its Bregman divergence

$$B_\psi(a;b)=\psi(a)-\psi(b)-\langle\nabla\psi(b),a-b\rangle.$$

At each round, the next point minimizes $\langle g_t,z\rangle+B_\psi(z;x_t)/\eta$ over $z\in V$, with one constant step size $\eta>0$. The regularizer is closed and $\lambda$-strongly convex, with $\lambda>0$, on the stated domain. Its derivative must be evaluated at interior points of $X$. For a horizon $T\ge1$, the theorem measures the range of the gradients seen along the run by the finite maximum

$$Q=\max_{1\le t\le T}\lVert\nabla\psi(x_t)-\nabla\psi(x_1)\rVert_*.$$

The maximum includes $x_1$, at which the difference is zero, and stops at $x_T$. These conventions are the ones in Definition 14.1 and Theorem 14.2.

Formalization targets

One-step mirror descent estimate

The first milestone is the inequality part of Lemma 6.10. For each feasible comparator, one OMD update controls the loss difference by a decrease in Bregman divergence plus a quadratic dual-norm term. The milestone records the book's whole inequality chain, including the intermediate term that exposes the change in the iterate. It is the local estimate used at every round of Theorem 14.2. Lemma 6.10, p. 67.

Summed comparison with an extra endpoint

The second milestone is the display in the proof of Theorem 14.2 immediately before the final choice $u_{T+1}=u_T$. It keeps that additional comparator free and shows the gradient-difference sum explicitly. This intermediate statement is useful for inspecting the sign and time index of each comparator shift. Proof of Theorem 14.2, pp. 228–229.

Goal: dynamic regret of online mirror descent

The goal is the full bound of Theorem 14.2:

$$\operatorname{DRegret}_T(u_1,\ldots,u_T) \le \frac{B_\psi(u_T;x_1)+Q P(u_1,\ldots,u_T)}{\eta} +\frac{\eta}{2\lambda}\sum_{t=1}^{T}\lVert g_t\rVert_*^2 -\frac{B_\psi(u_T;x_{T+1})}{\eta}.$$

It applies to every feasible comparator sequence, including a constant one. The negative terminal divergence is part of the target. Retaining it makes the statement match the source and preserves information for later use. Theorem 14.2, p. 228.

What the result gives

The theorem quantifies how much a comparator may move before its performance becomes hard to match. The cost of movement is linear in the path length and scaled by the regularizer-gradient range $Q$. With a bounded dual norm for the observed subgradients and a suitable constant step size, the chapter derives a square-root dependence on the horizon for slowly moving sequences. A static comparator has path length zero and recovers the familiar mirror-descent setting. The bound also applies to arbitrary norms and regularizers, so it is not limited to Euclidean projection. Discussion after Theorem 14.2, p. 229.

The mathematical result is proved in the book. The remaining task is to give its exact assumptions, update rule, intermediate inequality, and final inequality machine-checked proofs. The already published Bregman definition supplies a reusable representation of $B_\psi$; the new run, path-length, and gradient-maximum definitions supply the chapter's missing interface. Those definitions can support later formalizations of tracking regret and other moving-comparator results. No proof of the present chapter result is claimed by these draft statements.

Difficulty

For a fixed comparator, the Bregman terms from successive rounds line up directly. With $u_t$ changing, they do not: each transition changes the first argument of $B_\psi$. The resulting correction depends on differences of regularizer gradients, and its time index must agree with the path-length sum. A simple replacement of the static comparator by $u_t$ in a static regret theorem therefore leaves an unaccounted term. The terminal point $x_{T+1}$ is also essential to the full telescoping statement. The mission asks for the book's exact constant and terminal term rather than only an asymptotic rate.

Formalization scope

The Lean model uses a finite-dimensional real normed space. Losses and the regularizer are real-valued on their evaluated domains; the feasible-set and domain predicates represent the book's extended-real convention outside those domains. Closedness of the regularizer is represented by a closed epigraph over $X$. Subgradients are continuous linear functionals, so their operator norm is the dual norm. The run predicate represents every admissible subgradient and argmin choice for Algorithm 6.1; it also carries the required membership of $x_1,\ldots,x_{T+1}$ in $V\cap\operatorname{int}X$. The run is a predicate on sequences, not a selected canonical sequence.

The book's round labels start at one. Index zero is unused. The horizon is at least one, and $\eta,\lambda$ are positive. These conditions keep the finite maximum nonempty and every denominator meaningful. The subgradient condition is relative to $V$, which is sufficient for the theorem's comparisons and slightly weaker than the book's full-space subgradient convention. This choice is disclosed in the item statements. The comparator sequence is universally quantified through its feasibility condition; it is never restricted to a constant sequence or assumed to satisfy the conclusion. The definitions and theorem statements invite proofs of the one-step inequality, the summed estimate, and the final bound, as well as reusable results about Bregman divergence on arbitrary normed spaces.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026. arXiv

Why estimate-then-optimize

Many operational decisions are linear programs whose cost vector is uncertain but predictable from side information: routing with travel times that depend on weather and time of day, procurement with prices that depend on market signals, assignment with costs that depend on observed features. Contextual linear optimization (CLO) formalizes this: observe features $X$, choose a decision $z$ in a polytope $\mathcal Z$, pay $Y^\top z$ for an unobserved random cost vector $Y$.

Two families of data-driven methods compete. Estimate-then-optimize (ETO) fits a regression $\hat f(x) \approx \mathbb E[Y \mid X = x]$ and then solves the linear program with the estimated costs. Integrated methods (for example the SPO+ approach of Elmachtoub and Grigas, 2022) choose a decision rule by minimizing the empirical decision cost directly over a policy class, on the argument that a regression fit ignores how its errors affect decisions. Hu, Kallus and Mao (arXiv:2011.03030v3, Management Science 2022) show that, under a margin condition on the problem, the comparison goes the other way: ETO attains faster regret rates than any method that only uses a policy class.

This mission formalizes their ETO upper bound, Theorem 8. It is the third of a three-mission series on the paper; the first formalizes the upper bound for empirical risk minimization over a policy class (Theorem 6) and the second the matching lower bound for policy-class methods (Theorem 7).

Setting

Write $\mathbb R^k$ for Euclidean space with inner product $u^\top v$ and norm $\|\cdot\|$.

• Decisions. The polytope $\mathcal Z = \{z \in \mathbb R^d : Az \le b\}$ is nonempty and satisfies $\|z\| \le B$ for all $z \in \mathcal Z$, with $B > 0$. Its set of extreme points is $\mathcal Z^\angle$, a finite set.
• Data. Features $X \in \mathbb R^p$ have law $\mathbb P_X$; costs $Y \in \mathbb R^d$ satisfy $\|Y\| \le 1$. The regression function is $f^*(x) = \mathbb E[Y \mid X = x]$. The data $\mathcal D$ are $n$ i.i.d. copies of $(X, Y)$.
• Optimal decisions. $\mathcal Z^*(x) = \arg\min_{z \in \mathcal Z} f^*(x)^\top z$.
• Gap. If $\mathcal Z^*(x) \ne \mathcal Z$, the gap is

$$\Delta(x) = \min_{z \in \mathcal Z^\angle \setminus \mathcal Z^*(x)} f^*(x)^\top z - \min_{z \in \mathcal Z} f^*(x)^\top z,$$

the extra cost of the best suboptimal vertex; otherwise $\Delta(x) = 0$.

• Noise condition (Assumption 2). For some $\alpha, \gamma \ge 0$,

$$\mathbb P_X\bigl(0 < \Delta(X) \le \delta\bigr) \le (\gamma\delta/B)^\alpha \quad \text{for all } \delta > 0.$$

It always holds with $\alpha = 0$; larger $\alpha$ means less mass near dual degeneracy.

• Plug-in policy. For an estimate $f$, a plug-$f$-in policy $\pi_f$ chooses at every $x$ an extreme point in $\arg\min_{z \in \mathcal Z} f(x)^\top z$. The ETO policy is $\pi_{\hat f}$, where $\hat f = \hat f_{\mathcal D}$ is computed from the data.
• Regret. $\mathrm{Regret}(\hat\pi) = \mathbb E_{\mathcal D}\mathbb E_X\bigl[f^*(X)^\top \hat\pi_{\mathcal D}(X) - \min_{z \in \mathcal Z} f^*(X)^\top z\bigr]$.

In Lean the polytope is FastCLO.ETO.Polytope, the distribution is FastCLO.ETO.Instance (the law $\mu$ of $X$ and the conditional law $\kappa$ of $Y$ given $X$), and optVal, Zstar, gap, NoiseCond, IsPlugIn and regret are the objects above.

Formalization targets

Goal: Theorem 8

Fix $\alpha, \gamma \ge 0$ and $C_1, C_2 > 0$. There is a constant $C$ depending only on these such that, for every instance satisfying the noise condition, every $n$, every $a_n > 0$ and every estimator $\hat f$ with

$$\mathbb P_{\mathcal D}\bigl(\|\hat f(x) - f^*(x)\| \ge \delta\bigr) \le C_1 \exp(-C_2 a_n \delta^2) \quad \text{for every } \delta > 0 \text{ and almost every } x,$$

the plug-in policy satisfies

$$\mathrm{Regret}(\pi_{\hat f}) \le C\,B\,a_n^{-(1+\alpha)/2}.$$

The constant is existential, as on the page; the proof gives an explicit value, but the goal does not commit to it.

Milestones

The milestones are the displayed steps of the paper's proof (Appendix A.5, p. 30), in order:

1. Pointwise bound. The plug-in decision's excess cost at a point is at most $2B\|f^*(x) - \hat f(x)\|$.
2. Implication display. If the plug-in decision is strictly suboptimal at $x$ and $\|f^*(x) - \hat f(x)\| \le \varepsilon$, then $0 < \Delta(x) \le 2B\varepsilon$.
3. Peeled bound. For every $\delta > 0$,

$$\mathrm{Regret}(\pi_{\hat f}) \le 2B\delta\,\mathbb P(0 < \Delta(X) \le 2B\delta) + B\delta\sum_{r \ge 1} 2^{r+1}\,\mathbb P\bigl(\|f^*(X) - \hat f(X)\| > 2^{r-1}\delta,\ 0 < \Delta(X) \le 2^{r+1}B\delta\bigr).$$

4. Bound after iterating expectations. Under the hypotheses of Theorem 8, for every $\delta > 0$,

$$\mathrm{Regret}(\pi_{\hat f}) \le B\gamma^\alpha(2\delta)^{\alpha+1} + B\gamma^\alpha C_1\delta^{\alpha+1}\sum_{r \ge 1} 2^{(r+1)(\alpha+1)} e^{-C_2 a_n (2^{r-1}\delta)^2}.$$

Significance

For well-specified least squares regression, $a_n$ is of order $n$ up to a logarithmic factor (Corollary 4 of the paper), and Theorem 8 gives regret of order $n^{-(1+\alpha)/2}$ up to logarithms. Theorem 7 of the same paper shows that no algorithm that only uses a policy class of Natarajan dimension $\eta$ can beat $n^{-(1+\alpha)/(2+\alpha)}$ in the worst case over such instances. Since $(1+\alpha)/2 > (1+\alpha)/(2+\alpha)$ for every $\alpha \ge 0$, the two results separate ETO from integrated methods when the regression model is well specified. This runs against the common intuition behind end-to-end learning. The noise condition is the CLO analogue of the Tsybakov margin condition in classification (Tsybakov, 2004): the gap $\Delta$ plays the role of the distance of the regression function from the decision boundary.

The result is proved in the paper; as far as is known it has not been machine-checked. Formalizing it fixes the exact hypotheses (which quantifiers the tail condition carries, what "universal" means for $C_1, C_2$, and the measurability the regret integral needs) and yields reusable pieces: the extreme-point argument behind the implication display and the peeling bound in $[0, \infty]$.

Difficulty

The obvious argument bounds regret by $2B\,\mathbb E\|f^*(X) - \hat f(X)\|$, which gives only the rate $a_n^{-1/2}$ and ignores the noise condition (this is Theorem 4 of the paper). The faster rate needs two things the naive bound does not use. First, a wrong decision at $x$ is possible only where the gap $\Delta(x)$ is positive and at most a multiple of the estimation error. This uses that plug-in decisions are extreme points, so a strictly suboptimal decision is at least $\Delta(x)$ worse than optimal; it requires finiteness of $\mathcal Z^\angle$, which must be proved for an H-polytope. Second, the error must be controlled pointwise in $x$, with sub-Gaussian tails over the data, and combined with the noise condition shell by shell, through a Fubini exchange between the data and the feature.

Formalization scope

• Representation. Vectors live in EuclideanSpace ℝ (Fin k). The polytope bundles $A$, $b$, $B > 0$, nonemptiness and the bound $\|z\| \le B$. The distribution is a probability measure $\mu$ on features and a Markov kernel $\kappa$ with $\kappa(x)\{\|y\| > 1\} = 0$; $f^*(x) = \int y\,\kappa(x)(dy)$, and the data law is the $n$-fold product of $\mu \otimes \kappa$.
• Conventions. Optimal values and gaps are real infima, taken over nonempty bounded (indeed finite or compact) sets. The regret is measured against the optimal value, which equals the paper's $f^*(X)^\top\pi^*(X)$. Probabilities are $[0, \infty]$-valued measures; $(\gamma\delta/B)^\alpha$ is a real power with $0^0 = 1$.
• Disclosed additions. Plug-in policies are any selection from the argmin with values in $\mathcal Z^\angle$ (the paper's consistent tie-breaking is dropped, which strengthens the upper bound). The estimator and the policy are jointly measurable in the data and the feature. $C_1, C_2 > 0$ and $a_n > 0$. The constant $C$ is chosen after $\alpha, \gamma, C_1, C_2$ and before the instance, the sample size, the estimator and $a_n$.
• Ruled out. The tail hypothesis bounds the probability over the data for each fixed $x$, for every $\delta > 0$; it is not a probability over $X$ and not a single $\delta$. The conclusion is uniform: one constant for all instances, estimators and $a_n$. The peeled bound is stated in $[0, \infty]$, because a divergent real series would sum to $0$.
• Infrastructure needed. Finiteness of the extreme points of a bounded H-polytope and attainment of linear minima at extreme points; measurability of $x \mapsto \Delta(x)$; Fubini–Tonelli on the product of the data law and $\mu$; summability of $\sum_r 2^{(r+1)(\alpha+1)} e^{-c\,4^r}$. The polytope facts are reusable well beyond this mission.

Selected references

• Y. Hu, N. Kallus, X. Mao, Fast Rates for Contextual Linear Optimization, arXiv:2011.03030v3, 2021; Management Science, 2022. https://arxiv.org/abs/2011.03030v3
• A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 2022. https://doi.org/10.1287/mnsc.2020.3922
• A. B. Tsybakov, Optimal aggregation of classifiers in statistical learning, Annals of Statistics 32(1), 2004. https://doi.org/10.1214/aos/1079120131
• P. Massart, É. Nédélec, Risk bounds for statistical learning, Annals of Statistics 34(5), 2006. https://doi.org/10.1214/009053606000000786

Motivation

Online learning studies repeated decisions made before their losses are known. A learner chooses a point, observes a loss function, and then uses that observation to choose the next point. The natural performance measure is regret: the learner's cumulative loss minus the cumulative loss of one fixed competitor chosen after the sequence is known. A regret bound makes a claim for every loss sequence, including a sequence adapted to the learner's earlier decisions. Orabona's Chapter 6 develops online mirror descent as a way to obtain such bounds in geometries other than Euclidean distance Orabona, Chapter 6.

The geometry matters because the decision set and its loss gradients can have very different scales under different norms. On a simplex, for example, a Euclidean description treats coordinate changes differently from an entropy-based description. Theorem 6.11 expresses the guarantee in a primal norm chosen for the regularizer and the corresponding dual norm for the observed subgradients. It is the chapter's general regret statement for the basic mirror-descent algorithm Orabona, Theorem 6.11, p. 67.

Setting

Let $E$ be a finite-dimensional real normed space, representing the book's $\mathbb R^d$ with a chosen norm $\|\cdot\|$. The learner chooses from a nonempty closed convex set $V\subseteq E$. A regularizer $\psi$ has domain $X\supseteq V$; it is strictly convex on $X$ and differentiable on the interior of $X$. Its Bregman divergence is

$$B_\psi(y;x)=\psi(y)-\psi(x)-\langle\nabla\psi(x),y-x\rangle,$$

defined when $y\in X$ and $x\in\operatorname{int}X$. It need not be symmetric or satisfy the triangle inequality. The regularizer is $\lambda$-strongly convex on $V$ with respect to the chosen norm, where $\lambda>0$. The norm of a gradient $g$, written $\|g\|_*$, is the norm dual to $\|\cdot\|$. These are the conventions of Definition 6.4 and Lemma 6.10 Orabona, pp. 63–67.

At round $t$, beginning with $t=1$, the learner has $x_t\in V$, then observes a loss $\ell_t$ and a selected subgradient $g_t$ at $x_t$. With step size $\eta_t>0$, Algorithm 6.1 chooses any minimizer

$$x_{t+1}\in\arg\min_{y\in V}\left\{\langle g_t,y\rangle+\frac{1}{\eta_t}B_\psi(y;x_t)\right\}.$$

The book gives two ways to keep each update in the interior of $X$. The statements assume either of them, (6.5) or (6.6), $V\subseteq\operatorname{int}X$, so every iterate is a valid reference point for the next Bregman divergence Orabona, Algorithm 6.1 and (6.6), p. 65. Regret is measured against one fixed $u\in V$:

$$R_T(u)=\sum_{t=1}^{T}\bigl(\ell_t(x_t)-\ell_t(u)\bigr).$$

Formalization targets

For $T\ge1$ and nonincreasing positive step sizes, Theorem 6.11 gives the chapter's general bound

$$R_T(u)\le\frac{\max_{1\le t\le T}B_\psi(u;x_t)}{\eta_T} +\frac{1}{2\lambda}\sum_{t=1}^{T}\eta_t\|g_t\|_*^2\qquad(u\in V).$$

When every step equals the same $\eta>0$, it also gives the more specific bound

$$R_T(u)\le\frac{B_\psi(u;x_1)}{\eta} +\frac{\eta}{2\lambda}\sum_{t=1}^{T}\|g_t\|_*^2.$$

The decreasing-step bound is the goal; the constant-step conclusion is a companion theorem. The milestone list records the book's three-point identity (Lemma 6.7), the unique-minimizer theorem for a closed strongly convex function (Theorem 6.9), and the existence and full three-part inequality of the one-step mirror-descent lemma (Lemma 6.10). Theorem 6.11 follows these results in the source Orabona, pp. 64–67.

Significance

The first bound makes the cost of the update explicit: one term measures the divergence from the competitor to the iterates, and the other accumulates squared dual norms of the selected subgradients. The constant-step form depends only on the initial divergence, which can be substantially easier to estimate. These forms let a later analysis choose a regularizer and norm pair suited to its feasible set and gradients, as the chapter does in its subsequent examples Orabona, §§6.6–6.7.

The theorem and its proof are known mathematically from the textbook. The work here is to express the algorithm, its admissible oracle choices, and the exact bounds as Lean statements and then prove them. A formal proof of the one-step inequality would also be reusable for later dynamic-regret and optimistic mirror-descent results. The published Bregman-divergence definition is reused, but the statements in this mission remain proof targets; a related published three-point identity assumes continuous differentiability, stronger than the book's hypothesis.

Difficulty

The usual squared Euclidean distance has a symmetric algebraic expansion. Bregman divergence is asymmetric and its second argument must lie where the regularizer is differentiable. Thus a direct replacement of squared distance by $B_\psi$ does not by itself establish that every update is defined or that the terms in a regret sum have the right orientation. Theorem 6.11 also allows changing step sizes, so the divergence terms carry different denominators from one round to the next. The one-step lemma packages the exact inequality needed to make those issues precise Orabona, Lemma 6.10 and Theorem 6.11, p. 67.

Formalization scope

The Lean development uses an arbitrary finite-dimensional real normed space; continuous linear functionals represent subgradients, and their operator norm is $\|\cdot\|_*$. The regularizer is a total real-valued Lean function, but only its values on $X$ represent the book's function. Closedness is expressed by the closed epigraph of the extension equal to $+\infty$ outside $X$. Bregman divergence uses the published definition with the derivative at the second argument. The run predicate records the initial point, a selected subgradient, and a minimizer over $V$ on each round; it imposes no tie-breaking rule. The loss functions are real valued on $V$, and subgradient inequalities are stated relative to $V$, the only points compared in the regret result.

All sums use rounds $1,\ldots,T$; index zero carries no data. The maximum is a finite maximum with the explicit condition $T\ge1$. Positive $\eta_t$ and $\lambda$ protect every division in the displayed bounds. Every drafted statement assumes the book's "(6.5) or (6.6)", with (6.5) read as a one-sided limit $r\to0^+$. The update is required to minimize over $V$ itself, and $u$ ranges over $V$; allowing points outside that set would change the theorem. The minimizer result, the full one-step chain, and both regret bounds are welcome proof targets. The domain-restricted closed-function representation and the finite-round run predicate can be reused in related online convex optimization developments.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv preprint arXiv:1912.13213v10, 2026. arXiv

Motivation

Classifiers trained to be robust against small, adversarially chosen input perturbations routinely lose standard accuracy. Adversarial training (Madry et al., 2018) improves worst-case accuracy under an $\ell_p$-bounded attack, but on MNIST, CIFAR-10 and ImageNet the resulting models are measurably less accurate on unperturbed inputs, and the loss grows with the attack radius. A natural reading is that this is an artefact of training procedures or of finite data.

Tsipras, Santurkar, Engstrom, Turner and Mądry (ICLR 2019) argue otherwise: they exhibit a simple distribution on which every classifier faces the trade-off, so that the tension is a property of the data distribution itself and survives infinite data, including for the Bayes-optimal classifier. The argument isolates a distinction that has since been influential: robust features, moderately correlated with the label and stable under small perturbations, versus non-robust features, individually weak but jointly highly predictive and easily flipped. This mission formalizes the paper's first theorem, Theorem 2.1, and its proof in Appendix C.

Setting

Fix $d \in \mathbb N$, a probability $p$ with $\tfrac12 \le p < 1$, and $\eta \ge 0$. The distribution $\mathcal D$ of an input-label pair $(x, y)$, $x = (x_1, x_2, \dots, x_{d+1}) \in \mathbb R^{d+1}$, is the data model (3):

$$y \sim \mathrm{Unif}\{-1,+1\}, \qquad x_1 = \begin{cases} +y & \text{w.p. } p\\ -y & \text{w.p. } 1-p\end{cases}, \qquad x_2, \dots, x_{d+1} \overset{\text{i.i.d.}}{\sim} \mathcal N(\eta y, 1),$$

with $x_1$ and $(x_2, \dots, x_{d+1})$ independent given $y$. Write $G_+$ and $G_-$ for the law $\mathcal N(\pm\eta, 1)^{\otimes d}$ of the weak features given $y = +1$ and $y = -1$.

A classifier is a measurable map $f : \mathbb R^{d+1} \to \{-1, +1\}$. Its standard accuracy is $\Pr_{(x,y)\sim\mathcal D}[f(x) = y]$, the objective (1) of the paper with the 0–1 loss. Its $\ell_\infty$ robust accuracy at radius $\varepsilon$ is

$$\mathrm{acc}_\varepsilon(f) = \Pr_{(x,y)\sim\mathcal D}\big[f(x + \delta) = y \text{ for every } \delta \in \mathbb R^{d+1} \text{ with } \|\delta\|_\infty \le \varepsilon\big],$$

the objective (2) with the 0–1 loss and perturbation set $\Delta = \{\|\delta\|_\infty \le \varepsilon\}$. In Lean these are stdAcc d p η f and robustAcc d p η f ε, each an average with weight $\tfrac12$ of the two class-conditional probabilities. The proof also uses $p_{ij}$, the probability that $f$ predicts $+1$ when $x_1 = i$ and the weak features follow $G_j$ (pij), and the shift adversary $x_i \mapsto x_i - 2\eta y$ for $i \ge 2$ (shiftAdv, accuracy shiftAcc).

Formalization targets

Goal: Theorem 2.1 (p. 5)

For every measurable classifier $f$ and every $\delta \in \mathbb R$,

$$\Pr[f(x) = y] \ge 1 - \delta \ \Longrightarrow\ \mathrm{acc}_\varepsilon(f) \le \frac{p}{1-p}\,\delta \qquad \text{for every } \varepsilon \ge 2\eta.$$

The statement quantifies over all classifiers, not a parametric family, and over every radius $\varepsilon \ge 2\eta$.

Milestones (App. C, pp. 14–16)

1. The shift $z_i \mapsto z_i - 2\eta y$ pushes $\mathcal N(\eta y, 1)^{\otimes d}$ forward to $\mathcal N(-\eta y, 1)^{\otimes d}$: it changes $G_+$ to $G_-$ and vice versa.
2. For $\varepsilon \ge 2\eta \ge 0$, robust accuracy is at most the accuracy against the shift adversary.
3. $\Pr[f(x) = y] = \tfrac12\big(p(1 + p_{++} - p_{--}) + (1-p)(1 + p_{-+} - p_{+-})\big)$.
4. $\Pr[f(x_{\mathrm{adv}}) = y] = \tfrac12\big(p(1 + p_{+-} - p_{-+}) + (1-p)(1 + p_{--} - p_{++})\big)$.
5. With $a = 1 - p_{++} + p_{--} \ge 0$ and $b = 1 - p_{-+} + p_{+-}$: $1 - \tfrac12(pa + (1-p)b) \ge 1 - \delta$ implies $\tfrac12((1-p)a + pb) \le \tfrac{p}{1-p}\delta$.

Companion statements (§2.1, pp. 4–5)

• Tightness. $\mathrm{sign}(x_1)$ has standard accuracy $p$ and robust accuracy $p$ for $0 \le \varepsilon < 1$; at $\delta = 1-p$ the bound of Theorem 2.1 is attained.
• Standard classification is easy. For $f_{\mathrm{avg}}(x) = \mathrm{sign}(\tfrac1d\sum_{i\ge2} x_i)$, $\Pr[f_{\mathrm{avg}}(x) = y] = \Pr[\mathcal N(\eta, 1/d) > 0]$, which exceeds $99\%$ when $\eta \ge 3/\sqrt d$.

Significance

Theorem 2.1 converts the empirical observation into a statement about a distribution: on $\mathcal D$, standard accuracy $1 - \delta$ caps robust accuracy at $\frac{p}{1-p}\delta$, so as $\delta \to 0$ robust accuracy falls to $0$, while the adversary's budget $\varepsilon = 2\eta = \Theta(1/\sqrt d)$ is small compared with the feature scale $\pm 1$. Together with the companion statements it shows that the model admits a classifier with accuracy above $99\%$ and a classifier with robust accuracy $p$, but no classifier with both. It underlies the paper's conclusion that robust training must give up non-robust features, and the later line of work on robust versus non-robust features.

The result is proved in the paper, with an elementary argument. As far as the platform record and a search of the literature show, it has not been machine-checked. The formalization adds an exact, convention-explicit version of the model and of robust accuracy (worst case over a closed $\ell_\infty$ ball, outer measure of a possibly non-measurable event), a Lean statement of the shift-invariance property of Gaussian products that the argument rests on, and a reusable template for 0–1-loss adversarial objectives that later missions on robustness in Gaussian models can follow.

Difficulty

The obvious attempt is to bound robust accuracy for a specific classifier, or for linear classifiers, where the adversary's best response is explicit. That does not reach the theorem: the claim is about every measurable $f$, for which no best response is computable and the robust event need not even be measurable. On the formal side, the statements involve the pushforward of a product of Gaussians under a coordinatewise shift, the decomposition of the class-conditional law into the two-point law of $x_1$ and the product $G_\pm$, and a measure applied to a possibly non-measurable robust event; none of these is available as a ready-made lemma for this model.

Formalization scope

Inputs live in Fin (d + 1) → ℝ; coordinate 0 is $x_1$ and coordinate i.succ is $x_{i+2}$. The Mathlib norm on this type is the sup norm, so ‖δ‖ ≤ ε is exactly the $\ell_\infty$ ball. Labels and predictions are the reals $\pm1$. The class-conditional law is ((x1Law p y).prod (weakLaw d η y)).map (Matrix.vecCons ·.1 ·.2) with weakLaw d η y = Measure.pi (fun _ => gaussianReal (y * η) 1). Accuracies are real numbers in $[0,1]$ computed with toReal. The robust event is measured by its outer measure, i.e. under the completion of $\mathcal D$; no measurability of that event is assumed.

The standing assumption $p \ge \tfrac12$ of model (3) is a hypothesis of every statement. Four hypotheses implicit on the page are explicit: $p < 1$ in the goal (the bound divides by $1-p$, and Lean's $p/0 = 0$ would make the statement false at $p = 1$); $\eta \ge 0$ (the page takes $\eta$ large, $\Theta(1/\sqrt d)$; with $\eta < 0$ the case $\varepsilon = 0$ has no adversary and the statement fails); measurability of $f$; and $f(x) \in \{\pm1\}$ for every $x$.

A trivializing formalization is ruled out: the goal is stated for every measurable $\{\pm1\}$-valued classifier and for the worst case over the full $\ell_\infty$ ball of every radius $\varepsilon \ge 2\eta$, not for linear classifiers, not for the fixed shift adversary, and not with the $p_{ij}$ among its hypotheses; those appear only in milestones.

The development needs Mathlib's gaussianReal, Measure.pi, product measures and pushforwards. Welcome contributions: the Gaussian shift identity (reusable for any Gaussian location model), the disintegration of condLaw along $x_1$, and the two accuracy formulas.

Selected references

• D. Tsipras, S. Santurkar, L. Engstrom, A. Turner, A. Mądry, Robustness May Be at Odds with Accuracy, ICLR 2019; arXiv:1805.12152v5 (2019). https://arxiv.org/abs/1805.12152
• A. Madry, A. Makelov, L. Schmidt, D. Tsipras, A. Vladu, Towards Deep Learning Models Resistant to Adversarial Attacks, ICLR 2018. https://arxiv.org/abs/1706.06083
• L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, NeurIPS 2018. https://arxiv.org/abs/1804.11285

Motivation

In a game, each participant chooses a strategy while the cost of that choice depends on what everyone else does. A network user may choose a route, for example, but its travel time depends on the routes chosen by other users. The price of anarchy compares the cost of self-interested outcomes with the best joint outcome. A guarantee restricted to a Nash equilibrium leaves open what happens when players repeatedly adapt their choices without settling on any equilibrium. Roughgarden's extension theorem addresses sequences produced by players whose accumulated costs are asymptotically competitive with fixed alternatives. Its bound depends on a property of the game, rather than on a particular learning algorithm or on convergence of play. Roughgarden, §§1 and 3.2.

Setting

There is a finite set of players $i$, and player $i$ has a strategy set $S_i$. These sets may be infinite. An outcome $s$ specifies one strategy $s_i\in S_i$ for every player. The real number $C_i(s)$ is player $i$'s cost, and the joint cost is $C(s)=\sum_i C_i(s)$. The paper treats this objective as nonnegative. If player $i$ alone changes to the strategy $s'_i$ of another outcome $s'$, its cost is written $C_i(s'_i,s_{-i})$; every other player's strategy stays as in $s$. Roughgarden, §2.1.

A game is $(\lambda,\mu)$-smooth if every pair $s,s'$ satisfies $\sum_i C_i(s'_i,s_{-i})\leq\lambda C(s')+\mu C(s)$. The robust price of anarchy $\rho(G)$ is the infimum of $\lambda/(1-\mu)$ over all such smoothness pairs with $\mu<1$. This number packages every bound obtainable from the same smoothness condition. It is taken in the extended reals, with value $+\infty$ when no pair exists; the mission assumes an admissible pair exists, so it is below $+\infty$. Roughgarden, Definitions 2.1–2.2.

For a played outcome $s^t$ at time $t$ and a comparison outcome $s'$, define the hypothetical improvement $\delta_i(s^t;s')=C_i(s^t)-C_i(s'_i,s^t_{-i})$. A player has vanishing average external regret when its average cost, up to an error tending to zero, is no greater than the average cost it would have paid by using any one fixed strategy throughout the first $T$ rounds. The comparison strategy is held fixed across time, while the other players' strategies may change on every round. Each player may have its own error function. Roughgarden, (22), (24).

Formalization targets

Additive bound

The paragraph following equation (25) asserts a bound with a vanishing additive error. For any comparison outcome $s'$ and every horizon $T\geq1$, there is a function $\eta(T)\to0$ with

$$\frac1T\sum_{t=1}^{T}C(s^t)\leq\rho(G)C(s')+\eta(T).$$

This target includes the case $C(s')=0$. The paper states the conclusion for an optimal outcome; the same displayed relations also apply to any comparison outcome. Relations (23) and (25) are separate milestones: the former bounds one outcome using the players' hypothetical improvements, and the latter averages that bound over time. Roughgarden, §3.2, pp. 13–14.

Multiplicative repeated-play bound

The mission goal is Theorem 3.3's multiplicative presentation. For a comparison outcome with $C(s')>0$, there is a function $\eta(T)\to0$ such that

$$\frac1T\sum_{t=1}^{T}C(s^t)\leq\bigl(\rho(G)+\eta(T)\bigr)C(s')\qquad(T\geq1).$$

The positive-cost condition is needed to make the printed statement true. Consider one player with strategies of costs $1$ and $0$, playing the costly strategy once and the zero-cost strategy thereafter. Its average regret tends to zero, but its average cost is $1/T>0$ at every finite horizon. Taking the zero-cost strategy as $s'$ makes the right-hand side of the printed multiplicative bound zero for any $\eta$. The additive milestone preserves the valid zero-cost case. Roughgarden, Theorem 3.3 and the paragraph preceding it.

Significance

The result transfers a bound defined by the game's smoothness condition to repeated play even when the sequence does not converge. It therefore gives a welfare guarantee for the behavior captured by vanishing external regret without identifying which learning rule generated the sequence. The additive statement also records exactly what remains true when an optimal outcome has zero cost. Roughgarden, §3.2.

Formalizing the result makes the quantifiers behind $o(1)$ explicit: for each fixed game, sequence, and comparison outcome, one error sequence works across all positive horizons and tends to zero. The development also distinguishes the paper's valid additive consequence from its multiplicative display at zero cost. The paper proves the result mathematically; the Lean files in this mission are theorem statements for solvers and do not yet contain machine-checked proofs.

Difficulty

For a fixed smoothness pair, a finite-time inequality controls average joint cost by the comparison cost and players' average hypothetical improvements. Regret controls those improvements asymptotically, but the robust price of anarchy takes an infimum over all admissible pairs. Passing from bounds for individual pairs to that infimum requires the sign and boundedness conditions on the joint cost to be tracked correctly. A direct replacement of the fixed pair's ratio by $\rho(G)$ does not itself justify the limit. The zero-cost example also shows why an additive error cannot simply be displayed as a multiplicative $o(1)$ term in every case. Roughgarden, (23)–(25) and Theorem 3.3.

Formalization scope

Lean uses a finite type of players, arbitrary strategy types, and real-valued player costs. It defines the joint objective by the finite sum $\sum_i C_i(s)$; it does not assume that each individual cost is nonnegative. The goal and additive milestone assume that the joint objective is nonnegative at every outcome, matching the paper's standing convention. They also assume at least one smoothness pair with $\mu<1$, the case in which $\rho(G)=+\infty$ and the page's bound is vacuous. $\rho(G)$ is an extended-real infimum and the inequalities are compared in the extended reals. For a nonnegative game with an admissible pair, $\rho(G)$ is a real number at least 1 when some outcome has positive cost; if all outcomes cost zero, the target cost bounds are zero. Roughgarden, §§1, 2.1, 3.2.

Time indices are $1,\ldots,T$, with $T\geq1$. The Lean sequence is infinite so that the asymptotic assertion concerns prefixes of one sequence; its value at index zero is unused. The regret definition quantifies over every fixed alternative strategy rather than assuming a minimum is attained when a strategy set is infinite. A separate vanishing error sequence may be chosen for each player. The conclusion chooses one vanishing error sequence after the game, play sequence, and comparison outcome, and uses it at every horizon. These choices make the $o(1)$ terms genuine limits, rather than unconstrained values chosen separately for each $T$. Roughgarden, (24), Theorem 3.3.

The game objective, smoothness predicate, robust price of anarchy, deviation improvement, and regret predicate are the reusable definitions. Solvers can contribute proofs of the one-step bound, its averaged form, the additive conclusion, and the main theorem. Mixed-outcome sequences from Remark 3.4 are outside this mission's core; their probability and integrability conventions would require another definition layer.

Selected references

• Tim Roughgarden, Intrinsic Robustness of the Price of Anarchy, Journal of the ACM 62(5), Article 32, 2015. DOI: 10.1145/2806883. Statements and page numbers follow the author's final version dated July 14, 2015.

Why random signs matter in learning

Learning theory asks whether a rule that fits an observed sample will also perform well on future observations. A class with many functions can fit accidental patterns in the sample, so its size and geometry affect the reliability of empirical risk estimates. Empirical Rademacher complexity measures this ability to fit noise: attach an independent random sign to each observed point, let the class choose its best function after seeing all signs, and average the resulting signed score. A smaller value supports tighter uniform generalization bounds. Orabona, §16.1, pp. 270–271

Online learning studies a different protocol. A learner chooses a prediction before each round's loss is revealed, and its regret compares its cumulative loss with that of a fixed competitor chosen in hindsight. Chapter 16 of Orabona's book connects these two quantities. The connection matters because an online algorithm's regret estimate can be used to control the statistical complexity of a class of predictors, even though the online game and the random-sign experiment are defined differently. Orabona, Theorem 16.4, p. 272

Setting and notation

Fix a horizon $T\ge1$ and vectors $z_1,\ldots,z_T\in\mathbb R^d$. For each $t$, let $\varepsilon_t$ be an independent Rademacher sign, equal to $1$ or $-1$ with probability one half each. Given a nonempty bounded set $V\subseteq\mathbb R^d$, define its linear class by

$$H_{\mathrm{lin}}=\{z\mapsto\langle x,z\rangle:x\in V\}.$$

The empirical complexity on the fixed sample $S=(z_1,\ldots,z_T)$ is

$$\widehat{\mathfrak R}_S(H_{\mathrm{lin}}) =\frac1T\mathbb E_\varepsilon\left[ \sup_{x\in V}\sum_{t=1}^T\varepsilon_t\langle x,z_t\rangle \right].$$

This is a finite expectation over the $2^T$ possible sign assignments. The supremum is over the same comparison set $V$ for every assignment; the chosen $x$ may depend on the signs. The book's general Definition 16.1 allows an arbitrary class of real-valued functions, while this mission uses its linear specialization from the discussion immediately preceding Theorem 16.4. Orabona, Definition 16.1 and §16.1, pp. 270–272

For the final bound, $V$ is the probability simplex $\Delta^{d-1}=\{x\in\mathbb R^d:x_i\ge0,\ \sum_i x_i=1\}$. The supremum of a linear score over this simplex is the maximum of its $d$ coordinate scores. Write $G_\infty$ for a common bound on the infinity norm of the sample vectors, so $|z_{t,i}|\le G_\infty$ for every round and coordinate. Orabona, Corollary 16.7, p. 273

Formalization targets

The central target is Corollary 16.7, called Massart's Lemma in the book:

$$\frac1T\mathbb E_\varepsilon\left[ \max_{1\le i\le d}\sum_{t=1}^T\varepsilon_tz_{t,i} \right] \le \frac{G_\infty\sqrt{2\ln d}}{\sqrt T}.$$

Its constant and dependence on $d$ and $T$ are part of the target. The result includes $d=1$: in that case the expectation and the bound are both zero. Orabona, Corollary 16.7, p. 273

Two statements supply the chapter's route to this target. Theorem 16.4 says that if a nonanticipating online linear algorithm has worst-case regret at most $R(T)$ for all loss vectors in a symmetric set $Z$, then $\widehat{\mathfrak R}_S(H_{\mathrm{lin}})\le R(T)/T$ for any sample in $Z$. The Exponentiated Gradient regret bound of §6.6 gives, on the simplex, $\sum_t(\ell_t(x_t)-\ell_t(u))\le(\ln d)/\eta+(\eta/2)\sum_t\|g_t\|_\infty^2$ for every simplex competitor $u$. The milestone list quotes both source statements. Orabona, Theorem 16.4, p. 272; §6.6, p. 81

What the result provides

The goal supplies a sample-dependent complexity bound using only a coordinate bound, the number of coordinates, and the sample size. Its square-root dependence on $\ln d$ explains why a simplex-indexed class can have much smaller complexity than a crude bound that scales directly with $d$. In applications where a generalization estimate contains empirical Rademacher complexity, this result gives a concrete quantity to insert for a finite coordinate class. Orabona, §16.1, pp. 271–273

The mathematical statements are proved in the book. This mission asks for machine-checked proofs of the exact finite-sign formulation of the goal, the regret-to-complexity reduction, and the source's Exponentiated Gradient regret estimate. The local proposal currently contains statements with proof placeholders; it does not claim that these three items have already been proved in Lean. The resulting finite-sign and bounded-supremum definitions can also support other empirical-process arguments.

Where the work is difficult

The reduction has to respect the order of the online game. A bound for a learner allowed to inspect the current random sign would not imply the same complexity estimate: it could choose its round-$t$ point using information that a genuine online learner lacks. The algorithm therefore needs a precise causality condition, as well as a regret guarantee that holds for every admissible gradient sequence. Orabona, proof of Theorem 16.4, p. 272

The simplex result also depends on the exact regret coefficient. A generic $O(\sqrt T)$ estimate does not recover the displayed $\sqrt{2\ln d}$ constant. At the boundaries, real division and logarithms in Lean are total, so the statements must say when $T$ and $d$ are positive. The one-dimensional case is meaningful and must stay in the theorem.

Formalization scope

Vectors are functions Fin d → ℝ, representing $\mathbb R^d$ with its coordinate pairing. Samples, predictions and gradients use rounds $1,\ldots,T$; index zero is unused. The random-sign expectation is an exact average over Boolean assignments, with no measure-theoretic integrability convention. Both Rademacher averages require $T\ge1$. The signed linear supremum is real-valued and receives evidence that $V$ is nonempty and bounded. Theorem 16.4 also records the book's closedness hypothesis.

Theorem 16.4 formalizes deterministic online algorithms. The source permits internal randomization as well; that extension requires an independent probability model for the algorithm's random choices. The Exponentiated Gradient item represents losses by real-valued functions and requires the subgradient inequality on the simplex, where the book evaluates them. Its run predicate requires $\eta>0$ and includes the uniform initial point and coordinate update of Algorithm 6.2. The goal itself has no algorithm hypothesis. Its infinity-norm assumption is expressed as coordinate absolute-value bounds.

The definitions exclude an empty comparison class or an unbounded real supremum being silently assigned a default Lean value. A complete development needs finite-sign averaging identities, properties of real suprema over bounded sets, simplex geometry, and the regret analysis of Exponentiated Gradient. Contributions to these reusable components, to the two milestones, and to the goal are in scope. The PAC-Bayes and time-uniform concentration parts of Chapter 16 are reserved for separate work because they need different probability and measure-theory objects.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 16 and §6.6. arXiv

Motivation

Online prediction compares the losses of a sequence of decisions with the losses of one fixed decision chosen after the sequence is known. A learner would like a regret guarantee that remains valid for every such competitor, even when the losses arrive in an arbitrary order. Exponentially weighted averaging is a way to make each decision from all feasible points rather than committing to one candidate early. The method gives the Weighted Average Algorithm (WAA) in Chapter 11 of Orabona's text. It is particularly effective when the exponential of each negative loss is concave, a condition called exp-concavity.

The chapter first compares WAA with a competing probability distribution. Theorem 11.5 turns that guarantee into a bound against an individual feasible point. That distinction matters when the benchmark is a concrete portfolio, parameter vector, or other fixed decision, rather than a distribution over decisions. The same chapter later extends the weighted-average viewpoint to mixable losses through the Aggregating Algorithm; this mission focuses on the earlier deterministic-comparator result.

Setting

The feasible set $V$ is a closed, bounded, convex, full-dimensional subset of $\mathbb R^d$, with $d\geq1$. Its uniform distribution assigns a measurable subset probability equal to its Euclidean volume divided by $\operatorname{Vol}(V)$. Because $V$ is bounded and full-dimensional, its volume is finite and positive. Rounds are $t=1,\ldots,T$, with $T\geq1$. In round $t$, the learner predicts $x_t$, then observes a loss $\ell_t$ and pays $\ell_t(x_t)$. A competitor $u\in V$ is fixed across all rounds. Its regret is

$$R_T(u)=\sum_{t=1}^{T}\bigl(\ell_t(x_t)-\ell_t(u)\bigr).$$

For a parameter $\alpha>0$, a real-valued loss $\ell_t$ is $\alpha$-exp-concave on $V$ if $x\mapsto e^{-\alpha\ell_t(x)}$ is concave on $V$. Definition 7.31 in the source also permits a loss value of $+\infty$, with $e^{-\alpha(+\infty)}=0$. The mission defines that extended-valued concept for Proposition 7.34 and uses real-valued losses in its WAA target. The weighted average in round $t$ is

$$x_t=\frac{\int_V x\,\exp\!\left(-\alpha\sum_{s=1}^{t-1}\ell_s(x)\right)\,dx}{\int_V\exp\!\left(-\alpha\sum_{s=1}^{t-1}\ell_s(x)\right)\,dx}.$$

Thus $x_1$ is the centroid of $V$. This formula is Algorithm 11.1 with the uniform initial distribution and $1/\lambda_t=\alpha$. The existing published EWOO point definition uses precisely this one-based formula, so the mission imports that object. The integrals are with respect to Euclidean Lebesgue measure.

Formalization targets

The main target is Theorem 11.5, equation (11.6): for every $u\in V$,

$$R_T(u)\leq\frac d\alpha\left(1+\ln\left(\frac Td+1\right)\right).$$

The target fixes the exact dimension, horizon, and exp-concavity dependence from the source. It applies to each fixed competitor, with no distribution chosen in the statement. The milestone list records three source claims in reading order. Proposition 7.34 says that exp-concavity implies convexity, including the book's extended-real convention. Two displays in the proof of Theorem 11.5 describe the translated, contracted set $V'=\{\frac{T/d}{T/d+1}u+\frac{1}{T/d+1}w:w\in V\}$: the exponential losses there are bounded against those at $u$, and its uniform-prior mass is $1/(T/d+1)^d$. These are the chapter's explicit geometric and loss-comparison targets.

Significance

The theorem converts a distributional WAA guarantee into a bound for each deterministic competitor. Its dimension factor is $d$, and its logarithm contains $T/d+1$. This exact expression is sharper than replacing that logarithm by $\ln(T+1)$ for $d>1$; the distinction is visible in the target statement. A related EWOO result with the weaker $(d/\alpha)(1+\ln(T+1))$ form is already represented in the platform's library, but it does not establish the bound selected here. The source theorem is proved in the book; the remaining work is a machine-checked proof of this statement and the geometric milestones, with the source's constants intact.

The formal development can also support later results on exponentially weighted prediction. Its reusable pieces are the definition of exp-concavity, the extended-real epigraph convention, and the volume identity for a translated scaling of a convex body. The WAA prediction itself is represented by a previously published definition, giving future results a common algorithmic object rather than another copy of the same integral formula.

Difficulty

The general WAA statement compares the algorithm with a probability distribution, whereas Theorem 11.5 compares it with a point $u$. A point mass at $u$ is unsuitable as a comparator to a uniform continuous prior: it has no density with respect to that prior, so its relative entropy is infinite. The finite bound depends on identifying a region around $u$ that has positive uniform mass while retaining control of every exp-concave loss on that region. A formal treatment must also ensure that the weighted vector integral denotes an actual mean and that the normalization denominator is positive, rather than inheriting a default value from a total integral or division operator.

Formalization scope

The state space is EuclideanSpace ℝ (Fin d), and a loss is indexed from round one; index zero is unused. The prior is uniform on $V$, and the point played is the published one-based EWOO weighted mean. The hypotheses $d,T\geq1$ make the printed ratios meaningful. Closedness, boundedness, convexity, and positive volume express the source's full-dimensional convex-body setting. The theorem additionally records almost-everywhere measurability of each loss on $V$, and integrability of each exponential weight and its vector moment; these are explicit analytic conditions for the real and Bochner integrals in Lean. They are not algorithmic restrictions or assumptions of the regret inequality's conclusion. Positive volume and integrability rule out a vacuous zero denominator or Lean's zero value for a non-integrable integral.

The source allows extended-real losses, but the goal uses real-valued losses on $V$. Proposition 7.34 separately retains the full extended-real statement through WithTop ℝ: $+\infty$ maps to zero under the exponential, and convexity is expressed by a convex epigraph. A complete proof needs the exp-concavity and Jensen facts, the weighted-mean properties on convex $V$, the measure and volume properties of $V'$, and the distributional WAA inequality from the chapter. Contributions that supply these lemmas under the stated conventions are within scope. The prediction cannot be replaced by an arbitrary point of $V$: the exact uniform-prior weighted mean is part of the goal.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026. Chapter 11 and Proposition 7.34.

Motivation

A saddle-point problem asks one player to choose a decision that keeps a payoff small while another chooses a decision that makes it large. Such problems include two-player zero-sum games and constrained optimization written through a Lagrangian. Online convex optimization supplies a way to construct approximate saddle points from repeated play: each player responds to losses generated by the other's current decision. Chapter 15 of Orabona's textbook develops this connection and studies the resulting averages. The chapter's earlier online-to-saddle-point result gives a duality-gap certificate from the two players' regrets; §15.5 asks how the certificate improves when the payoff is smooth and both players use predictions of their next gradients.

The minimax equality for continuous convex-concave payoffs on compact convex sets is already a known mathematical result. Theorem 15.11 in the book is a case of Sion's minimax theorem, and a proved Sion theorem already exists in the platform library. This mission centers on the algorithmic rate in Theorem 15.26, which has a separate statement and a different role.

Setting

Let $X$ and $Y$ be nonempty closed convex sets in finite-dimensional real normed spaces, with norms $\|\cdot\|_X$ and $\|\cdot\|_Y$. The payoff $f(x,y)$ is real-valued, convex as a function of $x$ for fixed $y$, and concave as a function of $y$ for fixed $x$. The $X$-player tries to minimize it; the $Y$-player tries to maximize it. A saddle point would be a pair whose $X$ coordinate minimizes the payoff against its $Y$ coordinate and whose $Y$ coordinate maximizes it against its $X$ coordinate.

The duality gap of a pair $(x,y)$, when the extrema are attained, is $\max_{v\in Y}f(x,v)-\min_{u\in X}f(u,y)$. It is nonnegative and measures how far the pair is from the simultaneous best-response condition. For iterates indexed from $1$ through $T$, the book evaluates this gap at the averages $\bar x_T=T^{-1}\sum_{t=1}^{T}x_t$ and $\bar y_T=T^{-1}\sum_{t=1}^{T}y_t$.

Optimistic follow-the-regularized-leader, or optimistic FTRL, chooses each point by minimizing a regularizer plus all earlier linearized losses and a hint for the next loss. Algorithm 15.6 sets the hint equal to the previous observed partial gradient, starting with zero at round $0$. The $X$-player's observed linear functional is $g_{X,t}=\nabla_x f(x_t,y_t)$; the $Y$-player's is $g_{Y,t}=-\nabla_y f(x_t,y_t)$. Their regularizers $\psi_X$ and $\psi_Y$ have strong-convexity parameters $\lambda_X$ and $\lambda_Y$ with respect to their respective norms. The norm of each partial gradient is the corresponding dual norm.

Smoothness here means that the partial gradients exist on an open neighborhood of $X\times Y$ and satisfy four Lipschitz inequalities. Changes in the $X$ coordinate affect the $X$ gradient by at most $L_{XX}$ times the $X$ distance; changes in the $Y$ coordinate affect it by at most $L_{XY}$ times the $Y$ distance. For the $Y$ gradient the cross constant is again $L_{XY}$, and the own-coordinate constant is $L_{YY}$, exactly as in equations (15.7)–(15.10) of the textbook.

Formalization targets

The goal is the exact finite-horizon inequality of Theorem 15.26. Fix $\alpha>0$ and parameters satisfying $\lambda_X\ge2\sqrt2(L_{XX}+L_{XY}\alpha)$ and $\lambda_Y\ge2\sqrt2(L_{YY}+L_{XY}/\alpha)$. For any minimizer $x'_T$ of $f(\cdot,\bar y_T)$ and maximizer $y'_T$ of $f(\bar x_T,\cdot)$, the target is

$$\max_{v\in Y}f(\bar x_T,v)-\min_{u\in X}f(u,\bar y_T) \le \frac{\psi_X(x'_T)-\psi_X(x_1)+\psi_Y(y'_T)-\psi_Y(y_1)+\|g_{X,1}\|_{X,*}^{2}/\lambda_X+\|g_{Y,1}\|_{Y,*}^{2}/\lambda_Y}{T}.$$

The milestones are the linear-loss, fixed-regularizer instance of Theorem 7.47 used in the chapter, Theorem 15.12 relating player regrets to the averaged duality gap, and the explicit summed-regret inequality on page 262. Together they specify the algorithmic input, the conversion to a saddle-point certificate, and the exact stability coefficients in the goal.

Significance

The bound certifies the quality of the averaged pair after a specified number of rounds. When the regularizers are bounded on the feasible sets, its numerator is uniformly bounded and the gap is $O(1/T)$, as stated in the paragraph before Theorem 15.26. Without that further boundedness, the displayed inequality remains the theorem's finite-horizon statement, but its numerator can depend on $T$ through $x'_T$ and $y'_T$. The mission name's “constant over $T$” describes the bounded-regularizer setting; the formal goal preserves the more general printed bound.

The book proves the theorem mathematically. The work here is a machine-checked representation of Algorithm 15.6, its smoothness assumptions, the exact parameter thresholds, and the finite-horizon inequality. The run and smoothness definitions can be reused for other optimistic methods in the chapter, including Theorem 15.28. Existing library results about minimax equality address existence and equality of optimal values; they do not supply the quantitative guarantee for this run.

Difficulty

A standard regret bound for each player leaves variation terms involving successive iterates. With two players, each player's gradient variation depends on both players' movement and on different norms. A bound that discards this coupling loses the displayed coefficients and the rate in Theorem 15.26. The formal statement therefore keeps both sequences, both dual norms, and all four smoothness inequalities visible. It also has to treat the first round separately: the previous-gradient hint is zero there, while later rounds compare two observed gradients.

Formalization scope

The Lean development uses finite-dimensional real normed spaces; a partial gradient is a continuous linear functional and its operator norm is the book's dual norm. The payoff and regularizers are represented by real-valued functions on the ambient spaces, restricted to $X$ and $Y$ when optimized. Smoothness includes an open set containing the feasible product. Strong convexity uses Mathlib's set-relative StrongConvexOn. The run predicate enforces both argmin updates, and index $0$ is used only for the zero hint. It constrains exactly the rounds $1,\ldots,T$. In the optimistic FTRL milestone, the look-ahead point $x_{T+1}$ is the minimizer of the regularized loss sum with a zero hint. The book's proof uses the hint of round $T$ there instead, which makes that milestone's first inequality false.

The goal assumes $T\ge1$, positive $\alpha,\lambda_X,\lambda_Y$, and nonnegative smoothness constants. These record the book's parameter conventions and keep every denominator meaningful. The extrema in the conclusion are represented by arbitrary attained minimizer and maximizer witnesses, matching the theorem's nonempty-argmin and nonempty-argmax hypotheses. No boundedness or compactness of $X$ or $Y$ is imposed. An arbitrary sequence of feasible points cannot satisfy the goal: the optimistic FTRL argmin updates are part of the run hypothesis. Contributions that establish the two-player regret estimate, the regret-to-gap step, or the final inequality against this run model directly support the mission.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 15, pp. 244–269; Theorem 7.47, pp. 129–130. arXiv
• Maurice Sion, On general minimax theorems, Pacific Journal of Mathematics 8 (1958), pp. 171–176. DOI