Machine Learning

Every time a streaming service guesses what you would rate a film you have never seen, it is solving a matrix completion problem: fill in the missing entries of a vast user-by-item table from the few that are observed. The question became famous during the Netflix Prize (2006-2009), and it looks hopeless - infinitely many matrices fit the observed entries - until one assumes the structure that makes recommendation possible: the table is essentially low rank, because tastes are governed by a few latent factors. In their landmark 2009 paper 'Exact Matrix Completion via Convex Optimization' (Foundations of Computational Mathematics), Emmanuel Candes and Benjamin Recht proved that an n-by-n matrix of rank r can be recovered exactly, with high probability, from only about n^1.2 * r * log n randomly observed entries - not by the NP-hard route of minimizing rank, but by minimizing the nuclear norm, a convex surrogate (the sum of the singular values) solvable efficiently. The proof, in the lineage of Candes-Romberg-Tao compressed sensing, turns on two ideas: an incoherence condition ensuring the singular vectors are spread out rather than spiky, and a dual certificate witnessing optimality, whose existence rests on delicate random-matrix concentration. It transformed a practical engineering puzzle into rigorous theory and seeded a decade of work across machine learning, signal processing, computer vision, and sensor localization. This mission formalizes the Candes-Recht exact-recovery theorem in Lean, decomposed into its dual-certificate construction and the probabilistic concentration reductions at its core.

The basic UCB regret bound of Mission II is logarithmic but not tight: its leading constant $16/\Delta_i$ is eight times the information-theoretic limit, and its worst-case rate carries a spurious $\sqrt{\log n}$. Chapters 8–9 of Lattimore–Szepesvári close both gaps. A refined confidence schedule $f(t) = 1 + t\log^2 t$ yields the asymptotically optimal $\limsup_{n\to\infty} R_n/\log n \le \sum_{i:\Delta_i>0} 2/\Delta_i$ — exactly matching the instance-dependent lower bound of Mission VII for Gaussian noise. The MOSS index $\hat\mu_i + \sqrt{\tfrac{4}{T_i}\log^+\!\big(\tfrac{n}{k T_i}\big)}$ achieves minimax regret $R_n \le 39\sqrt{kn} + \sum_i \Delta_i$, matching the $\Omega(\sqrt{kn})$ lower bound up to a constant. These two theorems are the gold standard for finite-armed stochastic bandits.

A learner repeatedly chooses one of $k$ slot machines, observes only the reward of the chosen arm, and wants to earn almost as much as the best arm in hindsight. This is the stochastic multi-armed bandit, the canonical model of the exploration–exploitation dilemma. This mission formalizes the model (environments, policies, regret, and the regret decomposition $R_n = \sum_i \Delta_i\,\mathbb{E}[T_i(n)]$) and the two classical algorithms of Chapters 6–7 of Lattimore–Szepesvári: Explore-Then-Commit and the Upper Confidence Bound algorithm built on the optimism principle. The goal theorem is the instance-dependent UCB regret bound $R_n \le 3\sum_i \Delta_i + \sum_{i:\Delta_i>0} 16\log(n)/\Delta_i$ — logarithmic regret with explicit constants, the single most cited result of bandit theory — together with its distribution-free companion $R_n \le 8\sqrt{nk\log n} + 3\sum_i \Delta_i$.

The oldest bandit algorithm (Thompson, 1933) is also the most modern: sample a parameter from the posterior and act greedily. Chapters 34–36 of Lattimore–Szepesvári develop the Bayesian view in two crowning results. The Gittins index theorem: for infinite-horizon discounted Markov bandits, the seemingly intractable dynamic program is solved exactly by an index policy — each arm gets a retirement-value index computable arm-by-arm, and playing the largest index is Bayesian optimal. And the frequentist analysis of Thompson sampling — the goal theorem: with Gaussian posteriors, Thompson sampling on 1-subgaussian bandits achieves $\lim_{n\to\infty} R_n/\log n = \sum_{i:\Delta_i>0} 2/\Delta_i$, exactly asymptotically optimal, alongside the minimax-grade $R_n \le C\sqrt{kn\log n}$. Together they explain why posterior sampling is both principled and practically dominant.

Is the $d\sqrt{n}$ regret of LinUCB (Mission X) an artifact of the algorithm or a law of nature? Chapters 24–25 of Lattimore–Szepesvári prove it is essentially unimprovable. On the unit ball there is a parameter $\theta$ with $\|\theta\|_2^2 = d^2/(48n)$ forcing $R_n \ge \frac{d\sqrt{n}}{16\sqrt{3}}$ — the goal theorem — and the hypercube gives the same $\Omega(d\sqrt{n})$ rate. The asymptotic chapter is more striking still: for fixed finite action sets, the instance-optimal constant $c(\mathcal{A},\theta)$ is characterized by an allocation program, and optimism itself is provably suboptimal — LinUCB and Thompson sampling cannot achieve it, because exploration must sometimes deliberately play actions optimism would never touch. These lower bounds define the targets for the entire linear-bandit literature.

What if the rewards are not random at all, but chosen by an adversary who knows your algorithm? Remarkably, a randomized learner can still compete with the best fixed arm in hindsight. Chapters 11–12 of Lattimore–Szepesvári develop the adversarial $k$-armed bandit: rewards $x_{ti} \in [0,1]$ are an arbitrary fixed matrix, the learner samples $A_t \sim P_t$, and regret is measured against $\max_i \sum_t x_{ti}$. The exponential-weights algorithm Exp3, fed by importance-weighted loss estimates $\hat X_{ti} = 1 - \mathbb{1}\{A_t = i\}(1 - X_t)/P_{ti}$, achieves $R_n \le \sqrt{2nk\log k}$ — the goal theorem. The companion Exp3-IX, which deliberately biases its estimator, upgrades this to a bound holding with high probability rather than only in expectation. These results are the foundation of all adversarial online learning with partial feedback.

Motivation

Demand, prices and click-through rates often follow seasonal cycles: weekly, monthly, yearly. A decision maker who repeatedly chooses among options whose expected payoffs repeat in time faces a non-stationary multi-armed bandit. Chen, Wang and Wang (arXiv:2005.08088v4, Operations Research, 2025) study the model in which each arm's mean reward is periodic with its own unknown period. They give a two-stage policy whose regret is $\tilde O(\sqrt{T\sum_k T_k})$, and a lower bound showing that no policy, even one told the periods, does better than $\Omega(\sqrt{T\max_k T_k})$. This mission formalizes that lower bound, Theorem 3 of the paper. A companion mission of the same series covers the upper bound.

Lower bounds of this kind fix what is achievable. For the stationary $K$-armed bandit, the minimax regret is of order $\sqrt{TK}$ (Auer, Cesa-Bianchi, Freund and Schapire, 2002; Lattimore and Szepesvári, Bandit Algorithms, 2020, Ch. 15). In the periodic model a learner effectively faces $\sum_k T_k$ "effective arms" (arm $k$ at each phase of its cycle), which suggests the rate $\sqrt{T\sum_k T_k}$. The paper proves the weaker but general bound $\sqrt{T\max_k T_k}/(32e)$, which matches the upper bound up to a factor $\sqrt K$ and logarithms.

Setting

There are $K \ge 2$ arms and epochs $t = 1, \dots, T$. An instance $\nu$ is a family of mean rewards $\mu_{k,t}$. If arm $k$ is pulled at epoch $t$, the reward is drawn from the Gaussian law $\mathcal N(\mu_{k,t}, 1)$, independently of the past given the arm.

A sequence $f$ has minimum period $p \ge 1$ if $f(t+p) = f(t)$ for all $t \ge 1$ and no smaller positive integer has this property.

A policy $\pi$ chooses the arm $\pi_t$ at epoch $t$ at random, from a distribution that depends on the previous arms and rewards. Its expected regret on $\nu$ is display (1) of the paper:

Three classes of instances appear, all with unit-variance Gaussian rewards and means in $[0,1]$ (Assumption 1):

1. $\mathcal E_1$: every arm is stationary;
2. $\mathcal E_2(T_1)$: the first arm's mean has minimum period $T_1$, the other arms are stationary;
3. $\mathcal E_3(T_1,\dots,T_K)$: arm $k$'s mean has minimum period $T_k$.

The proof compares instances through the metric (B-48),

The periods satisfy Assumption 3 with the parameters (7): with $n = \lfloor\sqrt{T/K}\rfloor$ and $g = \lceil\sqrt n\rceil$, $T > 4K$, $g \ge 2$ and $T_k < n/(2g)$ for every $k$.

Formalization targets

Goal: Theorem 3 (p. 24)

For every policy $\pi$ there is $\nu \in \mathcal E_3(T_1,\dots,T_K)$ with

Milestones

1. Lemma 12 (p. 23). Stationary Gaussian bandits whose arms other than the first have known mean $1/2$: every policy has regret at least $\sqrt T/(8\sqrt2 e)$ on some choice of $\mu_1 \in [0,1]$.
2. Lemma 13 (p. 23). One periodic arm: every policy has regret at least $\sqrt{TT_1}/(16e)$ on some instance of $\mathcal E_2(T_1)$ whose other arms have mean $1/2$.
3. Fact 1 (proof of Theorem 3, p. 48). $\mathcal E_3$ is dense in $\mathcal E_2 \cup \mathcal E_3$ under $\mathcal M$: an instance of $\mathcal E_2(T_1)$ can be perturbed on the arms other than the first into an instance of $\mathcal E_3(T_1,\dots,T_K)$ at $\mathcal M$-distance less than any $\delta > 0$.
4. Fact 2 (proof of Theorem 3, p. 48). The regret $f_\pi(\nu) = \mathbb E_\nu[R^\pi_T]$ is continuous in $\nu$ on $\mathcal E_2 \cup \mathcal E_3$ for $\mathcal M$, uniformly in $\pi$.

Significance

Theorem 3 shows that knowing the periods does not remove the cost of learning them phase by phase: the regret must grow like $\sqrt{T\max_k T_k}$, not like $\sqrt{TK}$. Together with the paper's upper bound $\tilde O(\sqrt{T\sum_k T_k})$ and the inequality $\sqrt{T\max_k T_k} \ge \sqrt{T\sum_k T_k}/\sqrt K$, it shows the two-stage policy is near-optimal when $K$ is fixed. The intermediate results are reusable: Lemma 12 is a clean two-point Gaussian lower bound, Lemma 13 is a phase-decomposition argument that applies to any bandit model with known cyclic structure, and facts 1 and 2 give a continuity framework for the regret as a function of the instance.

The result has a published proof. As far as the platform's records show, none of it has been machine-checked. The stationary minimax lower bound of Lattimore and Szepesvári (a different family and constant) exists on the platform, together with the Bretagnolle–Huber inequality, the Gaussian KL divergence and the divergence decomposition, which this mission lists as tools.

Difficulty

The two-point argument of Lemma 12 is standard, but its constant needs $\Delta = \sqrt{1/(2T)} < 1/2$, so small horizons must be handled separately. Lemma 13 decomposes the problem into $T_1$ phase problems; making this rigorous means showing that a policy on the periodic problem induces, on each phase, a policy on a stationary problem of horizon $\lfloor T/T_1\rfloor$, with a history law that factorizes accordingly. The phase-wise instances produced by the decomposition need not have minimum period exactly $T_1$ (all phases may coincide), so a perturbation is needed to land in $\mathcal E_2(T_1)$; the constant has slack for it. Fact 2 asks for continuity of an integral against the law of a $T$-round adaptive process, uniformly over all policies, which needs a domination argument that does not depend on the policy's kernels.

Formalization scope

• Arms are Fin K, 0-based: the paper's first arm is index $0$. Epochs are 1-based natural numbers; history coordinate $i$ is epoch $i+1$. Values of the means at $t = 0$ are ignored.
• A policy is the platform's BanditAlgorithm.BanditPolicy K: one Markov kernel per round from the history to the next arm. The history law periodicMeasure reuses the platform's step kernel with the Gaussian bandit of the current epoch's means; with constant means it is BanditAlgorithm.banditMeasure of BanditAlgorithm.gaussianBandit. Lemma 12 is stated with the platform's banditRegret, $T\mu^* - \mathbb E[\sum_t X_t]$, which equals (1) for Gaussian arms; the other statements use (1) directly.
• Assumption 1 is stated on epochs $1,\dots,T$. Minimum periods are exact.
• Every lower bound has the order "for every policy there is an instance", with the instance in the class, so the policy may depend on $K$, $T$ and the periods; this is the paper's "policy that knows $T_k$". The supremum over the class is replaced by an attained instance, which is the stronger form.
• Added hypotheses, all disclosed: $K \ge 2$ (with one arm the regret is $0$); $T_k \ge 1$ (the paper's $T_k \in \mathbb N^+$); in Lemmas 12 and 13, the means of the arms other than the first are $1/2$, which is how "a policy that knows $\mu_k$ for $k \ge 2$" is read (with arbitrary known values the printed lemmas fail). Assumption 3 with (7) is the standing assumption of Appendix B.4.
• A statement with the quantifiers in the order "there is an instance for every policy", without the $[0,1]$ clause, or without exact minimum periods, would be false or trivial; none of these is the target.

Welcome contributions: the bridge between periodicMeasure with constant means and banditMeasure, the phase decomposition of the history law, and the uniform continuity of the regret in the means.

Selected references

• N. Chen, C. Wang, L. Wang, Learning and Optimization with Seasonal Patterns, Operations Research, 2025; arXiv:2005.08088v4, 2021. https://arxiv.org/abs/2005.08088v4
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375

Motivation

In a linear stochastic bandit, a learner repeatedly chooses an action from a set of vectors and receives a noisy reward whose mean is linear in the action. The model underlies contextual recommendation, adaptive routing and dynamic pricing, where each option is described by features and the payoff of a feature vector must be learned while it is exploited. The quality of a strategy is measured by its regret: the reward lost, relative to always playing the best action, over the first $n$ rounds.

The optimism-in-the-face-of-uncertainty principle (play as if the most favourable parameter consistent with the data were true) was introduced for linear bandits by Auer (2002), and developed by Dani, Hayes and Kakade (2008) (ConfidenceBall, regret $O(d\sqrt n\log^{3/2} n)$ with confidence sets from a union bound over time) and Rusmevichientong and Tsitsiklis (2010). Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) replaced the union bound by a self-normalized martingale inequality that holds uniformly in time. It gives smaller confidence ellipsoids and, through them, a high-probability regret bound for the resulting algorithm, OFUL, that improves the earlier ones by logarithmic factors. The inequality became the standard tool for linear and kernelized bandits and for linear reinforcement learning.

Setting

Fix a dimension $d \ge 1$ and an unknown parameter $\theta_* \in \mathbb R^d$. In round $t = 1, 2, \dots$ the learner is given a nonempty decision set $D_t \subseteq \mathbb R^d$, chooses $X_t \in D_t$, and observes the reward

There is a filtration $\{F_t\}_{t \ge 0}$ such that $X_t$ is $F_{t-1}$-measurable and $\eta_t$ is $F_t$-measurable and conditionally $R$-sub-Gaussian: $\mathbf E[e^{\lambda\eta_t} \mid F_{t-1}] \le \exp(\lambda^2R^2/2)$ for all $\lambda \in \mathbb R$, with $R \ge 0$ fixed.

For a regularization parameter $\lambda > 0$ let $\overline V_t = \lambda I + \sum_{s=1}^t X_sX_s^\top$ and let $\widehat\theta_t = \overline V_t^{-1}\sum_{s=1}^t Y_sX_s$ be the regularized least-squares estimate. With $\|v\|_A = \sqrt{v^\top A v}$ and a known bound $\|\theta_*\|_2 \le S$, the confidence ellipsoid is

The OFUL algorithm chooses, in round $t$, a pair $(X_t, \widetilde\theta_t)$ maximizing $\langle x, \theta \rangle$ over $D_t \times C_{t-1}$. The pseudo-regret is $R_n = \sum_{t=1}^n \langle x^*_t - X_t, \theta_* \rangle$, where $\langle x^*_t, \theta_*\rangle = \max_{x\in D_t}\langle x,\theta_*\rangle$.

Formalization targets

Goal: Theorem 3, the regret of OFUL

If $\|X_t\|_2 \le L$, $\langle x, \theta_*\rangle \in [-1,1]$ for all $x \in D_t$, and $\lambda \ge \max(1, L^2)$, then for every $\delta > 0$, with probability at least $1 - \delta$,

Milestone: Theorem 1, the self-normalized bound

For any positive definite $V$, $\overline V_t = V + \sum_{s\le t}X_sX_s^\top$ and $S_t = \sum_{s \le t}\eta_sX_s$: with probability at least $1-\delta$, for all $t \ge 0$,

Milestones: Theorem 2, the confidence ellipsoids

With probability at least $1 - \delta$, $\theta_* \in C_t$ for all $t \ge 0$ (first claim). If $\|X_t\|_2 \le L$, then with probability at least $1-\delta$, for all $t$, $\|\widehat\theta_t - \theta_*\|_{\overline V_t} \le R\sqrt{d\log((1 + tL^2/\lambda)/\delta)} + \lambda^{1/2}S$ (second claim, stated here for $d \ge 2$).

Significance

Theorem 3 bounds the regret of OFUL by $O(d\sqrt n\log n)$ with high probability, uniformly over the horizon, so it holds for an unknown horizon without restarting. The bound applies to arbitrary, even adversarially changing, decision sets. Theorem 1 is the ingredient that makes this possible: a deviation bound for a vector-valued martingale, normalized by its own random covariance, that holds for all times simultaneously and whose logarithmic term is a determinant rather than a union-bound count. The same inequality underlies regret analyses of generalized linear bandits, kernelized bandits, linear Markov decision processes and many confidence-sequence constructions.

All three results are proved in the paper's appendices (not included in the source file used here). None of them is formalized in the stated generality. Prove2Me holds the special cases $V = \lambda I$, $R = 1$, $\delta < 1$ of Theorems 1 and 2 (from the Bandit Algorithms textbook series), a pathwise LinUCB regret lemma that assumes the confidence event, and the elliptical potential lemma. A formal proof of Theorem 3 would be the first machine-checked high-probability regret bound for OFUL with the paper's confidence sets.

Difficulty

The actions are chosen adaptively, by an argmax over a data-dependent set, so the sequence $X_t$ has no independence structure and the least-squares estimate is not a sum of independent terms. A fixed-design concentration bound followed by a union bound over time and over a covering of the sphere loses logarithmic factors and does not produce the determinant in the radius; that is the route of the earlier work that Theorem 1 improves. Theorem 1 must hold for all times at once for a quantity normalized by the random matrix $\overline V_t$, which is itself built from the adaptively chosen actions; a bound for each fixed $t$ does not give it.

Formalization scope

Vectors are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and $\|x\|_A$ is Real.sqrt (x ⬝ᵥ A *ᵥ x). Rounds are indexed $t+1$ for $t : ℕ$, so sums over $s \le t$ are sums over Finset.range t at index s + 1, and the time-0 objects are empty sums. The probability space is standard Borel, as Mathlib's conditional sub-Gaussianity (HasCondSubgaussianMGF, variance proxy $R^2$) requires; this is an added hypothesis. Every "with probability at least $1-\delta$, for all $t$" is stated as an outer-measure bound $\le \delta$ on the failure event, with the time quantifier inside the event. $\det(\cdot)^{1/2}$ is the real square root of the determinant; the matrices inverted are positive definite, so Lean's junk inverse never occurs.

OFUL is a predicate on the whole process: in every round the chosen pair maximizes $\langle x,\theta\rangle$ over $D_t \times C_{t-1}$, with any tie-breaking. Runs exist whenever the decision sets are nonempty and compact. The measurability of the actions is assumed, as in Theorem 1. The optimal reward $\langle x^*_t, \theta_*\rangle$ is the supremum over $D_t$, finite because of the reward bound.

Two corrections to the printed Theorem 3 are made and disclosed. The printed $nL/d$ is replaced by $nL^2/d$, which is what the determinant–trace bound $\det\overline V_n \le (\lambda + nL^2/d)^d$ gives; for $L \le 1$ the corrected bound implies the printed one. The hypothesis $\lambda \ge \max(1, L^2)$ is added: for $\lambda < 1$ the printed logarithm can be negative, and the printed bound would then assert $R_n \le 0$. In the second claim of Theorem 2, $d \ge 2$ is added, because at $d = 1$ the claim does not follow from the first claim and the paper's proof is not available.

The goal is a probability bound over the noise, not the pathwise statement "if $\theta_* \in C_{t-1}$ for all $t$ then $R_n \le \dots$". The pathwise statement assumes the confidence event instead of proving it, and is already on the platform. The confidence sets inside the OFUL predicate use the same $\delta$ as the conclusion.

Needed infrastructure: maximal inequalities for nonnegative supermartingales, Gaussian integrals of quadratic forms on $\mathbb R^d$, log-determinant bounds for sums of rank-one updates, and the determinant–trace inequality. The platform rows BanditAlgorithm.self_normalized_martingale_bound, BanditAlgorithm.least_squares_confidence_ellipsoid and BanditAlgorithm.elliptical_potential_lemma are referenced as tools. Proofs of the milestones, generalizations of the existing special cases to general $V$ and $R$, and reusable determinant lemmas are all welcome.

Selected references

• Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, Advances in Neural Information Processing Systems 24 (NIPS), 2011. https://proceedings.neurips.cc/paper/2011
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• V. Dani, T. P. Hayes, S. M. Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT, 2008. http://colt2008.cs.helsinki.fi/papers/80-Dani.pdf
• P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1100.0446
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapters 19–20. https://doi.org/10.1017/9781108571401

Motivation

A recurring question in high-dimensional statistics is how tightly a scalar quantity built from many random inputs concentrates around its mean, even as the number of inputs grows without bound. Two classical answers organize the whole toolkit: martingale methods, which control a sum of dependent increments one conditional step at a time, and Gaussian-specific isoperimetry, which shows that essentially any regular (Lipschitz) function of a high-dimensional Gaussian vector concentrates as tightly as a single Gaussian coordinate, regardless of dimension. This mission formalizes one representative theorem from each line: the general martingale Bernstein bound (Wainwright, High-Dimensional Statistics, 2019, Theorem 2.19) and the Gaussian concentration of Lipschitz functions (Theorem 2.26), following Chapter 2 of the same book.

Setting

A random variable $X$ with mean $\mu=\mathbb E[X]$ is sub-Gaussian with parameter $\sigma$ (Definition 2.2) if $\mathbb E[e^{\lambda(X-\mu)}]\le e^{\sigma^2\lambda^2/2}$ for all $\lambda\in\mathbb R$; it is sub-exponential with parameters $(\nu,\alpha)$ (Definition 2.7, a strictly milder condition) if the same bound holds only for $|\lambda|<1/\alpha$, with the convention $1/0=+\infty$ so that $\alpha=0$ recovers the sub-Gaussian case exactly.

A sequence $\{D_k\}_{k\ge1}$, adapted to a filtration $\{\mathcal F_k\}$, is a martingale difference sequence if each $D_k$ is $\mathcal F_k$-measurable and $\mathbb E[D_k\mid\mathcal F_{k-1}]=0$. Such sequences arise throughout statistics via the Doob martingale construction: given a function $f$ of independent variables $X_1,\dots,X_n$, setting $D_k:=\mathbb E[f(X)\mid X_1,\dots,X_k]-\mathbb E[f(X)\mid X_1,\dots,X_{k-1}]$ telescopes to $f(X)-\mathbb E[f(X)]=\sum_k D_k$, converting a deviation question about $f(X)$ into a martingale concentration question.

A function $f:\mathbb R^n\to\mathbb R$ is $L$-Lipschitz with respect to the Euclidean norm if $|f(x)-f(y)|\le L\|x-y\|_2$ for all $x,y$ (Eq. (2.38)).

Formalization targets

Goal — Theorem 2.26 (Gaussian concentration of Lipschitz functions)

Let $(X_1,\dots,X_n)$ be i.i.d. standard Gaussian and $f$ be $L$-Lipschitz with respect to the Euclidean norm. Then $f(X)-\mathbb E[f(X)]$ is sub-Gaussian with parameter at most $L$, and hence

The bound is dimension-free: it depends on $n$ only through $f$'s Lipschitz constant, not the ambient dimension itself.

Milestone — Lemma 2.27 (Gaussian interpolation identity)

For any differentiable $f$ and convex $\varphi$, $\mathbb E[\varphi(f(X)-\mathbb E[f(X)])] \le \mathbb E[\varphi(\tfrac\pi2\langle\nabla f(X),Y\rangle)]$ for $X,Y\sim N(0,I_n)$ independent — the interpolation identity Theorem 2.26's proof is built on.

Milestone — Theorem 2.19 (martingale Bernstein bound)

Given a martingale difference sequence with a per-index sub-exponential conditional moment-generating-function bound $\mathbb E[e^{\lambda D_k}\mid\mathcal F_{k-1}]\le e^{\lambda^2\nu_k^2/2}$ for $|\lambda|<1/\alpha_k$, the sum $\sum_k D_k$ is itself sub-exponential with parameters $\big(\sqrt{\sum_k\nu_k^2},\ \max_k\alpha_k\big)$, and satisfies the two-regime concentration inequality of Eq. (2.28): sub-Gaussian for small deviations, sub-exponential for large ones. This is the chapter's central general-purpose martingale concentration tool.

Significance

Theorem 2.19 is the source of two of the most-cited concentration inequalities in the field — the Azuma–Hoeffding inequality (Corollary 2.20) and the bounded-differences/McDiarmid inequality (Corollary 2.21), both already faithfully covered elsewhere on the platform (azuma_hoeffding_two_sided, bounded_diff_martingale_two_sided) and included here as kind: reference milestones rather than redrafted. Theorem 2.26's Gaussian Lipschitz concentration is separately significant: it is the tool behind dimension-free operator-norm bounds for random matrices, concentration of the empirical spectral distribution, and much of the machinery of Chapters 5 and 6 of the same book.

Formalizing it. No faithful prior art exists on the platform for either the martingale Bernstein bound or Lipschitz-Gaussian concentration itself (a fresh search for "martingale Bernstein," "sub-exponential martingale," "Gaussian interpolation," and "Lipschitz concentration" returned no hits; the existing Vershynin-book item HighDimProb.Isoperimetry.lipschitz_concentration_sphere concentrates a Lipschitz function on the sphere, a different underlying space and a different proof from Theorem 2.26's Gaussian vector). Both goal-adjacent theorems and the Gaussian interpolation lemma are drafted here as open goals (:= by sorry); the two Azuma–Hoeffding/bounded-differences corollaries are reused from the platform's existing, already-proved formalizations.

Difficulty

The naive approach to Theorem 2.26 — try to bound $f(X)-\mathbb E[f(X)]$ directly via a Lipschitz-type argument in $\mathbb R^n$ — has no obvious route to a dimension-free bound, since a union bound over coordinates (or over an $\varepsilon$-net of the domain) picks up a factor that grows with $n$. The resolution, Lemma 2.27's interpolation identity, instead exploits a special structural fact about the Gaussian distribution — its rotation invariance — to replace the nonlinear quantity $f(X)-\mathbb E[f(X)]$ with the linear, and hence exactly computable, Gaussian quantity $\langle\nabla f(X),Y\rangle$, at the mild cost of a non-optimal constant. Theorem 2.19's difficulty is bookkeeping rather than a conceptual obstruction: the recursive conditioning step (Eq. (2.29)) must be iterated exactly $n$ times while keeping track of the interplay between the two parameters $\nu_k,\alpha_k$ per difference, and Proposition 2.9's two-regime tail bound (small-deviation sub-Gaussian behavior, large-deviation sub-exponential behavior) must be carried through unchanged into the final statement — dropping either regime understates what the theorem proves.

Formalization scope

Expectations are Bochner integrals against an explicit probability measure, with integrability required as an explicit hypothesis in IsSubGaussian and IsSubExponential (Mathlib's Bochner integral silently returns $0$ for a non-integrable function, which this mission's definitions rule out as a trivializing formalization). The sub-exponential condition's domain restriction |λ| < 1/α is realized as the disjunction α = 0 ∨ |λ| < 1/α, since Lean's real division convention 1/0 = 0 is exactly backwards from the book's own stated 1/0 = +\infty convention for the degenerate sub-Gaussian case.

"$X,Y\sim N(0,I_n)$ independent" (Lemma 2.27, Theorem 2.26) is formalized via Mathlib's HasGaussianLaw predicate together with explicit coordinatewise mean-zero and identity-covariance hypotheses, which together pin down the standard multivariate normal law, plus IndepFun. The inner product $\langle\nabla f(X),Y\rangle$ is realized as fderiv ℝ f (X ω) (Y ω), the Fréchet derivative applied to $Y(\omega)$ — equal to $\langle\nabla f(X(\omega)),Y(\omega)\rangle$ by the Riesz representation of the gradient on a Hilbert space, avoiding the need to separately construct a gradient vector field.

Theorem 2.19's printed parameter pair for part (a), "$(\sum_k\nu_k^2,\alpha_*)$," is formalized as $(\sqrt{\sum_k\nu_k^2},\alpha_*)$: Definition 2.7 parametrizes the sub-exponential MGF bound by $\nu$ (with $\nu^2$ appearing in the exponent), so a literal transcription of the printed pair's first entry would silently square the effective parameter and make part (a), read literally, inconsistent with part (b)'s own tail-bound formula (which the book derives from part (a) via the general sub-exponential tail bound, Proposition 2.9). The corrected pairing is the one the book's own proof actually establishes; see MODERATION_NOTES.md for the full derivation.

Out of scope for this mission: Proposition 2.5 (plain Hoeffding for a sum of independent sub-Gaussians), used in the book only as background for Theorem 2.26's proof and not redrafted, since the goal theorem's own statement does not depend on it once Lemma 2.27 is in hand.

Selected references

• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019. DOI: 10.1017/9781108627771. Chapter 2.
• K. Azuma, "Weighted sums of certain dependent random variables," Tôhoku Mathematical Journal, 19:357–367, 1967.
• W. Hoeffding, "Probability inequalities for sums of bounded random variables," Journal of the American Statistical Association, 58:13–30, 1963.

Motivation

Every algorithm in the first three chapters of Foster and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making — ε-Greedy and UCB for the multi-armed bandit, Inverse Gap Weighting and SquareCB for contextual bandits — is a special case of the same two-step recipe: estimate a model of the world with an online regression oracle, then convert the estimate into a decision that trades exploration against exploitation. Chapter 4 asks whether this recipe can be made generic: given any structured decision-making problem, specified only by a function class $F$ and a decision space $\Pi$, is there a single quantity that governs the best achievable regret, the way $\sqrt{A/\gamma}$ governs the multi-armed bandit and $\sqrt{d/\gamma}$ governs the linear bandit? The chapter's answer is the Decision-Estimation Coefficient (DEC), introduced by Foster, Kakade, Qian, and Rakhlin [40] as a complexity measure that both upper- and lower-bounds achievable regret for a general decision-making protocol, unifying results that were previously proved from scratch, case by case, for each structured setting. This mission formalizes the chapter's central upper bound (Proposition 13) together with the machinery that makes it computable in two concrete cases — the multi-armed bandit (Proposition 14) and the linear bandit (Propositions 16–17).

Setting

Fix a finite decision space $\Pi$ and a class $F \subseteq \mathbb{R}^\Pi$ of candidate mean-reward functions, with a ground-truth $f^\star \in F$ (realizability). Over $T$ rounds, at each round $t$ the learner observes an estimate $\hat f_t$ produced by an online regression oracle, plays a decision distribution $p_t \in \Delta(\Pi)$ (possibly depending on $\hat f_t$ and the history), and the regret is

where $\pi^\star = \arg\max_\pi f^\star(\pi)$. The oracle's cumulative estimation error is assumed bounded: $\sum_{t=1}^T \mathbb{E}_{\pi \sim p_t}[(\hat f_t(\pi) - f^\star(\pi))^2] \le \mathrm{EstSq}(F,T,\delta)$ with probability at least $1-\delta$ (Definition 7). Writing $\pi_f := \arg\max_\pi f(\pi)$, the DEC game value at a reference model $\hat f$ and scale $\gamma > 0$ is the min-max quantity

and the DEC of $F$ itself is $\mathrm{dec}_\gamma(F) := \sup_{\hat f \in \mathrm{co}(F)} \mathrm{dec}_\gamma(F, \hat f)$. The Estimation-to-Decisions (E2D) algorithm plays, at each round, a $p_t$ certifying (i.e. attaining or beating) the value of this min-max game at $\hat f_t$.

Formalization targets

Goal — Proposition 13 (E2D regret bound)

with probability at least $1-\delta$, for any exploration parameter $\gamma > 0$. This is the weakest stable statement the chapter proves about E2D: it holds for an arbitrary function class and an arbitrary regression oracle, with no structural assumption on $F$ beyond realizability, and the chapter's later sections instantiate it rather than strengthen it.

Milestones

• Lemma 9 (Decoupling), general form: for any distribution $\nu$ over a finite model class and any $\bar f$, $\mathbb{E}_{f\sim\nu}[f(\pi_f) - \bar f(\pi_f)] \le \sqrt{A \cdot \mathbb{E}_{f\sim\nu}\mathbb{E}_{\pi\sim p}[(f(\pi)-\bar f(\pi))^2]}$ — the estimation-to-decisions bridge the whole chapter's approach rests on, decoupling the model index from the played decision.
• Proposition 14 (IGW minimizes the DEC): for the multi-armed bandit ($\Pi=[A]$, $F=\mathbb{R}^A$), Inverse Gap Weighting is the exact minimizer of the DEC game, giving $\mathrm{dec}_\gamma(F) = (A-1)/(4\gamma)$ — the first concrete computation of an abstract quantity, recovering Chapter 3's rate from Proposition 13 alone.
• Proposition 16 (G-optimal design): existence, for any compact full-dimensional-span set $Z \subseteq \mathbb{R}^d$, of a distribution $p$ with $\sup_{z\in Z}\langle \Sigma_p^{-1}z,z\rangle \le d$ — the classical convex-analysis primitive Proposition 17 needs.
• Proposition 17 (DEC for linear bandits): combining the G-optimal design with inverse gap weighting gives $\mathrm{dec}_\gamma(F) \lesssim d/\gamma$ for the linear bandit function class, leading via Proposition 13 to a $\sqrt{dT}$ regret bound.

Significance

The Decision-Estimation Coefficient is, in the book's own words, "the main result" of this line of work: Foster, Kakade, Qian, and Rakhlin [40] show it is not merely an upper bound but (in a suitable localized form, developed further in Chapter 6) a tight characterization of the minimax regret for structured bandits and, more generally, for the interactive decision-making protocol the rest of the book studies. Proposition 13 is the mechanism that makes this useful in practice: it reduces regret analysis for a new structured problem to a single, purely convex-analytic computation of $\mathrm{dec}_\gamma(F)$, in place of a bespoke exploration argument. Propositions 14–17 are the demonstration that this reduction is not vacuous — they recompute, via the DEC alone, the two rates (multi-armed and linear bandit) that earlier chapters of the book derived by direct, setting-specific arguments, and the match is exact. Formalizing this chapter therefore captures the book's unifying abstraction itself, not just one more instance of it. No formalization of the Decision-Estimation Coefficient, in any form, currently exists on the platform (see Formalization scope).

Difficulty

The obvious formalization mistake is to state Proposition 13's conclusion with $\mathrm{dec}_\gamma(F)$ left as an unconstrained free real-number parameter satisfying only the inequality the theorem asserts — a formalization under which the "theorem" would be a triviality about an arbitrary real number, since nothing about the actual min-max game would ever be checked. The chapter's content is precisely the opposite: that this specific minimax quantity can be computed (Proposition 14) or bounded via a concrete strategy (Proposition 17), and — as Chapter 6 shows for a lower bound outside this chunk's scope — that no smaller quantity would do. A second difficulty is proof-theoretic rather than notational: the book's own proof of Proposition 13 bounds regret by an unconstrained supremum over all reference functions $\hat f : \Pi \to \mathbb{R}$, and only identifies this with the official, $\mathrm{co}(F)$-restricted $\mathrm{dec}_\gamma(F)$ of Eq. (4.16) via Proposition 24 — a fact stated on p. 80, outside this chapter's numbered range, whose own proof the book defers to an exercise. A formalization that quietly imports Proposition 24 to close this gap would rest the goal theorem on an unverified fact; this mission instead states the hypothesis the book's own text uses to motivate restricting to $\mathrm{co}(F)$ in the first place (online estimation algorithms produce $\hat f_t \in \mathrm{co}(F)$), so the goal is faithful to what is actually established within the chapter's own pages.

Formalization scope

Every item fixes a finite decision space (Fin A, Fin n, or a generic Fintype S) and states the DEC as the literal sInf-of-sSup transcription of the min-max game (Eqs. (4.15)–(4.16)), never as an opaque bound — this is the trivializing formalization the chunk's own reading of the chapter rules out (see Difficulty). piStar : (S → ℝ) → S is a hypothesized global maximizer selector throughout, constrained to be a genuine argmax only on the function class in scope (F or Set.univ), matching how the book treats $\pi_f$ as a fixed but arbitrary tie-breaking choice. The goal theorem (Proposition 13) adds the explicit hypothesis hfhat : ∀ t, fhat t ∈ convexHull ℝ F, replacing an appeal to the out-of-range Proposition 24 (see Difficulty); this is the one place this mission's statement is not a line-by-line transcription of the book's own displayed proof steps, and it is recorded here and in MODERATION_NOTES.md. Proposition 14's and Proposition 17's $\lesssim$ are replaced by the explicit constants the book's own proofs establish ($(A-1)/(4\gamma)$ exactly, and $(4d+1)/(2\gamma)$ respectively — the latter obtained by summing the three terms the proof of Proposition 17 isolates). Proposition 14's Lean statement splits the book's single equality $\mathrm{dec}_\gamma(F,\hat f) = (A-1)/(4\gamma)$ into an upper bound on the literal decGf, a lower bound restricted to full-support distributions, and IGW's own exact game value, because the book's min over the whole simplex is not provable as a literal Lean equality: a distribution with a zero-weight arm makes the inner supremum genuinely unbounded, and Lean's total Real.sSup returns a junk value smaller than $(A-1)/(4\gamma)$ there (caught in moderation, MODERATION_NOTES.md); the three-conjunct statement recovers exactly the book's real content without asserting that false literal equality. Lemma 9 is restated inside FoundationsRL.Structured rather than imported from the Chapter 2 mission, since draft items across chunks cannot import one another; its source citation still points to its original location (p. 32). Proposition 16 is not drafted: the platform's existing BanditAlgorithm.kiefer_wolfowitz_equivalence (Lattimore & Szepesvári, Theorem 21.1) states the identical existence claim — compact set with full-dimensional span, a design with G-value at most $d$ — as one clause of a larger equivalence, and is reused as a reference item rather than redrafted. Proposition 22 (primal/dual DEC equivalence, §4.4) is deliberately excluded: the book states it "under mild regularity conditions" it does not pin down in the statement itself, which is exactly the kind of unquantified hypothesis this series' faithfulness standard excludes from a goal or milestone. Contributions extending this mission with Chapter 6's lower bound (matching $\mathrm{dec}_\gamma(F)$ from below, establishing tightness) or with a formalization of Proposition 24 itself (removing this mission's hfhat hypothesis) are welcome.

Selected references

• D. Foster, S. Kakade, J. Qian, and A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv:2112.13487, 2021. https://arxiv.org/abs/2112.13487
• 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.
• J. Kiefer and J. Wolfowitz, The Equivalence of Two Extremum Problems, Canadian Journal of Mathematics, 1960.

The final step from bandits to reinforcement learning: actions now change the state of the world. Chapter 38 of Lattimore–Szepesvári studies online learning in an unknown Markov decision process with $S$ states, $A$ actions and rewards in $[0,1]$. The optimism principle of Mission II scales up: UCRL2 maintains confidence sets over transition kernels, solves an extended MDP by extended value iteration, and recomputes only when a state-action count doubles. The goal theorem: with probability $1-\delta$, $\hat R_n < C\,D(M)\,S\sqrt{An\log(nSA/\delta)}$, where $D(M)$ is the diameter of the MDP — sublinear regret with no prior knowledge of the dynamics. The matching lower bound $\mathbb{E}[\hat R_n] \ge C'\sqrt{DSAn}$ brackets the true complexity of tabular reinforcement learning up to $\sqrt{DS}$.

How well can any algorithm possibly do? Chapters 13–17 of Lattimore–Szepesvári answer with three matching impossibility results. The divergence decomposition identifies the information a policy collects: $D(\mathbb{P}_{\nu\pi}, \mathbb{P}_{\nu'\pi}) = \sum_i \mathbb{E}[T_i(n)] D(P_i, P_i')$. Feeding it into the Bretagnolle–Huber inequality of Mission VI yields the goal theorem — the minimax lower bound $R_n \ge \frac{1}{27}\sqrt{(k-1)n}$ over Gaussian bandits, showing MOSS (Mission III) is optimal up to a constant. The same machinery gives the instance-dependent bound of Lai–Robbins type: every consistent policy suffers $\liminf_n R_n/\log n \ge \sum_{i:\Delta_i>0} \Delta_i / d_{\inf}(P_i, \mu^*, \mathcal{M}_i)$, certifying the asymptotic optimality of the UCB of Mission III and KL-UCB of Mission IV, and a high-probability lower bound showing the Exp3-IX guarantees of Mission V cannot be improved.

Motivation

In inverse optimization one observes the decisions of an expert who solves an optimization problem and tries to recover the expert's objective. The contextual version of Besbes, Fonseca and Lobel (arXiv:2106.14015; Operations Research, 2025) asks a sharper question: not how well the cost can be estimated, but how well a decision-maker who imitates the expert performs, measured by regret against the expert. Settings of this kind arise whenever a firm wants to reproduce the routine choices of an experienced planner, for example routing, assortment or scheduling decisions, without being told the planner's cost trade-offs.

The online setting is adversarial. Nature fixes an unknown cost vector and then presents a sequence of problems; after each decision it reveals the expert's optimal action, which cuts the set of costs still consistent with the observations. A companion mission of this series shows that the natural greedy policy, which plays the center of this consistent set, can incur regret linear in the horizon. This mission formalizes the paper's first positive answer: an algorithm, EllipsoidalCones, with regret logarithmic in the horizon when the initial set of costs lies inside a pointed cone.

Setting

Costs lie on the unit sphere $S^d$ of $\mathbb R^d$, $d=m+1\ge2$. In period $t$ nature presents a feasible set $\mathcal X_t\subseteq\mathbb R^n$, compact, nonempty and of diameter at most $1$, and a $1$-Lipschitz context $f_t:\mathbb R^n\to\mathbb R^d$. The forward problem with cost $c$ has solution set $\psi(c,\mathcal X_t,f_t)=\operatorname{argmin}_{x\in\mathcal X_t}f_t(x)'c$. The decision-maker plays some $x^\pi_t$, nature reveals an expert action $x^\star_t\in\psi(c^\star,\mathcal X_t,f_t)$ for the true cost $c^\star$, and the regret over $T$ periods is

The knowledge set $C(\mathcal I_t)$ is the set of costs in the initial set $C_0\subseteq S^d$ under which every expert action seen so far was optimal.

The angle between nonzero vectors is $\theta(c,\hat c)=\arccos(c'\hat c/\|c\|\|\hat c\|)$, and the uncertainty angle of a set $C$ is $\alpha(C)=\inf_{\hat c\in S^d}\sup_{c\in C}\theta(c,\hat c)$; a minimizing $\hat c$ is a circumcenter. The initial set is pointed when $\alpha(C_0)<\pi/2$.

For a positive diagonal $W=\operatorname{diag}(w_1,\dots,w_m)$ and an orthonormal $U$, the ellipsoidal cone is

a cone with axis $Ue_1$ and elliptical cross-section. The effective difference of period $t$ is $\delta^\pi_t=(f_t(x^\pi_t)-f_t(x^\star_t))/\|f_t(x^\pi_t)-f_t(x^\star_t)\|$ (and $0$ if the difference vanishes).

EllipsoidalCones with parameter $\epsilon$ starts from the circular cone $W_1=\tan^2\alpha(C_0)I$, $U_1e_1$ a circumcenter of $C_0$, and plays the axis $U_te_1$ as proxy cost. With $\bar\delta=U_t^{-1}\delta^\pi_t$ it keeps the cone if

and otherwise replaces it by the output of ConeUpdate, which performs one central-cut step of the ellipsoid method on the cone's cross-section and re-centres the result by a spectral decomposition.

Formalization targets

Goal: Theorem 3 (p. 20)

With $\epsilon=d/T$ there is an absolute constant $K$ such that for every $d\ge2$, $T\ge1$, closed pointed $C_0$ with $\alpha(C_0)>0$, $c^\star\in C_0$, admissible instances and run,

The constant is left unfixed: the shape $d^2\ln(T\tan\alpha(C_0))$ is the claim, and the proof's explicit constant rests on a step that fails at $d=2$.

Milestones

1. Proposition 1: $\alpha(E(W,U))=\arctan\sqrt{\lambda_{\max}(W)}$.
2. Lemma 4: if $C(\mathcal I_t)\subseteq E(W_t,U_t)$ and (12) holds, the period's regret is at most $\epsilon$.
3. Lemma B-1 ($\eta=0$): ConeUpdate's output contains $E(W,U)\cap\{\delta'c\ge0\}$ and $\prod\lambda_i$ shrinks by $e^{-1/(2(d-1))}$.
4. Lemma 3: $C(\mathcal I_{t+1})\subseteq E(W_t,U_t)\cap\{\delta^{\pi\prime}_tc\ge0\}\subseteq E(W_{t+1},U_{t+1})$, and for $d\ge3$ $\prod\lambda_i$ shrinks by $e^{-1/(d-1)}$.
5. Cohen et al. (2020), Lemmas 3 and 4 (already posed on the platform, referenced): an ellipsoid-method step shrinks the smallest eigenvalue by at most $(d-1)^2/d^2$, and does not shrink it at all below the threshold $(\epsilon/(10(d-1)))^2$ when the cut is long.
6. Lemma 5: for $d\ge3$, $\lambda_{\max}(W_t)\le(10d/\epsilon)^{2(d-2)}\lambda_{\max}(W_1)^{d-1}e^{-I^\pi_t/(d-1)}$, or no update ever happens.

Significance

The theorem shows that in contextual inverse optimization the decision-maker can force nature to reveal information: a cone update happens only after a large mistake, and each such mistake shrinks the cone geometrically, so large mistakes are logarithmically rare. It is the building block of the paper's general-case algorithm, which restarts the same construction in growing subspaces, and it isolates why the greedy policy fails: it never trades instantaneous regret for information.

The paper proves the result; nothing in it is machine-checked. The mission produces a checked version of the pointed-case analysis, an ellipsoidal-cone layer on top of the platform's ellipsoid-method definitions, and corrected statements where the printed ones are imprecise: the dimension restriction $d\ge3$ for the rate of Lemma 3 and the first part of Lemma 5, the column order of the spectral decomposition in ConeUpdate, and the $\eta=0$ case of Lemma B-1.

Difficulty

Two steps resist the obvious argument. First, ConeUpdate is not the ellipsoid method: the minimum-volume ellipsoid of the cut cross-section has the right volume but its cone is no longer centred, and the new cone's axis is an eigenvector of an indefinite bordered matrix. Showing that this re-centred cone still contains the cut cone requires matching the eigenvalues of the bordered matrix with those of the ellipsoid matrix in the right order. Second, a volume decrease alone does not bound the regret: by Proposition 1 the uncertainty angle is governed by the largest eigenvalue, and the ellipsoid method can make that eigenvalue grow. The lazy test (12) and the smallest-eigenvalue lemmas of Cohen et al. are what keep the cones from becoming long and thin; without them the product of eigenvalues falls while the angle does not.

Formalization scope

Costs live in EuclideanSpace ℝ (Fin (m+1)) with $d=m+1$, actions in EuclideanSpace ℝ (Fin n), so all norms are Euclidean. $W$ is stored as its diagonal $w$, $U$ as a real orthogonal matrix, and $U^{-1}$ is written $U^\top$. Lean periods are $0$-based: Lean period $t$ is the paper's period $t+1$. This text is the arXiv v3 preprint (1 July 2023), not the published 2025 article; all numbering is the preprint's.

Standing assumptions carried by the statements: $d\ge2$, $n\ge1$, feasible sets nonempty, compact and of diameter at most $1$, contexts $1$-Lipschitz, $C_0$ a closed subset of $S^d$, $\epsilon>0$. Pinned and disclosed choices:

• ConeUpdate is a relation, not a function. The printed $U^{-1}B\delta_{[2:p]}$ is read as $(U^{-1}\delta)_{[2:p]}$. The first column of $V$ is the eigenvector of the positive eigenvalue of $M$ with positive first entry, and larger $|\mu|$ is paired with larger eigenvalues of $N$. The page leaves this order open, and Algorithm 1 and Lemma B-1 disagree on it.
• The printed "$U_1\leftarrow I_{d-1}$" is read as: $U_1$ orthonormal with a circumcenter of $C_0$ as its first column.
• $\alpha(C_0)>0$ on the goal. At $\alpha(C_0)=0$ the algorithm's $W_1=0$ is not positive definite.
• The rate of Lemma 3 and the first part of Lemma 5 are stated for $d\ge3$ only; the rest of both lemmas for every $d\ge2$. At $d=2$ ConeUpdate halves $W$, and $1/2>e^{-1}$.
• Lemma B-1 is stated only for $\eta=0$. Its $\eta>0$ inclusion is false as printed.
• The worst-case regret is stated as a bound for every true cost, every adaptive instance sequence and every run, not as a real supremum. The polynomial running-time claim is not formalized.

The run predicate is satisfiable: a circumcenter of a closed nonempty $C_0$ exists, the bordered matrix has exactly one positive eigenvalue, and a cone update is required only when the tail of $\bar\delta$ is nonzero. A formalization in which no run exists, or in which $K$ may depend on $d$ or $T$, does not state Theorem 3.

A complete development needs the angle and uncertainty-angle layer, ellipsoidal cones and their cross-sections, the published ellipsoid-method update (LinearOptimization_EllipsoidMethod) with its volume and eigenvalue facts, Cauchy–Schwarz over ellipsoids, and eigenvalue interlacing for bordered matrices. The ellipsoidal-cone layer and the cone-update lemma can be reused in the paper's general case and in other cone-based learning algorithms. Proofs of any milestone, and of the referenced Cohen et al. lemmas, are welcome.

Selected references

• O. Besbes, Y. Fonseca, I. Lobel, Contextual Inverse Optimization: Offline and Online Learning, arXiv:2106.14015v3, 2023; Operations Research, 2025. https://arxiv.org/abs/2106.14015
• M. C. Cohen, I. Lobel, R. Paes Leme, Feature-Based Dynamic Pricing, Management Science 66(11), 2020. https://doi.org/10.1287/mnsc.2019.3485
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, 2nd ed., Springer, 1993. https://doi.org/10.1007/978-3-642-78240-4
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 8.

Motivation

When every participant in a repeated game runs a no-regret learning algorithm, the time-averaged play converges to a coarse correlated equilibrium, and in smooth games the average welfare approaches the price-of-anarchy guarantee. These facts are a standard justification for equilibrium predictions in auctions, routing and markets, where agents learn rather than solve for equilibria. Against an adversary, the regret of any learning algorithm can grow like $\sqrt T$, which gives average regret of order $T^{-1/2}$. Syrgkanis, Agarwal, Luo and Schapire (arXiv:1507.00407, NIPS 2015) asked whether learning is faster when the opponents are themselves learning, and so their play changes slowly.

Timeline. Daskalakis, Deckelbaum and Kim (2011) gave a decentralized algorithm with $O(\log T)$ regret in two-player zero-sum games. Rakhlin and Sridharan (2013) obtained the same rate in zero-sum games with optimistic mirror descent, which uses the last observed utility as a prediction of the next one. Syrgkanis et al. (2015) extended recency-biased learning to general multi-player normal-form games. They isolated the RVU property, proved that it gives constant total regret (Theorem 4, Corollary 8), and proved that each individual player's regret is $O(T^{1/4})$ (Theorem 11, Corollary 12). This mission formalizes the second result. Later work by Chen and Peng (2020) and by Daskalakis, Fishelson and Golowich (2021) improved the individual rate to polylogarithmic in $T$.

Setting

A static game has $n$ players. Each player $i$ has a finite strategy set $S_i$ with $|S_i|=d$, and a utility function $u_i:S_1\times\cdots\times S_n\to[0,1]$. A mixed strategy is a point $w_i$ of the probability simplex $\Delta(S_i)\subset\mathbb R^d$, and the players randomize independently. The game is played at times $t=1,\dots,T$. At time $t$ each player picks $w_i^t\in\Delta(S_i)$ and then observes its utility vector

so its expected utility is $\langle w_i^t,u_i^t\rangle$. The regret of player $i$ after $T$ steps is

Strategies are measured in the norm $\|\cdot\|=\|\cdot\|_1$. Utilities are measured in its dual, $\|v\|_*=\|v\|_\infty$. A regularizer $\mathcal R$ is 1-strongly convex if $\mathcal R(\frac{a+b}2)\le\frac{\mathcal R(a)+\mathcal R(b)}2-\frac{\|a-b\|_1^2}8$. The range $R$ is $\max_i(\sup_{\Delta}\mathcal R_i-\inf_\Delta\mathcal R_i)$.

Optimistic follow the regularized leader (OFTRL) with step size $\eta>0$ and predictor sequence $M_i^t$ plays $w_i^0=\operatorname{argmin}_\Delta\mathcal R$ and

With one-step recency bias, $M_i^T=u_i^{T-1}$. An algorithm has the RVU property (Regret bounded by Variation in Utilities) with parameters $\alpha,\beta,\gamma$ if its regret against every $w^*$ is at most $\alpha+\beta\sum_t\|u^t-u^{t-1}\|_*^2-\gamma\sum_t\|w^t-w^{t-1}\|^2$. It has the stability property with constant $\kappa$ if $\|w_i^t-w_i^{t+1}\|\le\kappa$.

Formalization targets

Goal: Corollary 12 (p. 5)

If $n\ge2$, every player runs OFTRL with $M_i^t=u_i^{t-1}$ and $\eta=(n-1)^{-1/2}T^{-1/4}$, then for every player $i$ and every $w_i^*\in\Delta(S_i)$,

Milestones

1. Lemma 20 (supp. p. 4): $\|w^t-g^t\|\le\eta\|M^t-u^t\|_*$ and $\|g^t-w^{t+1}\|\le\eta\|M^{t+1}\|_*$, where $g^T=\operatorname{argmax}_\Delta\langle g,\sum_{t\le T}u^t\rangle-\mathcal R(g)/\eta$ is the leader sequence.
2. Stability with $\kappa=2\eta$ (p. 5, before Corollary 12): OFTRL with $M^t=u^{t-1}$ and utilities in $[0,1]$ moves by at most $2\eta$ per step.
3. Proposition 7 (p. 5): OFTRL with $M^t=u^{t-1}$ has the RVU property with $\alpha=R/\eta$, $\beta=\eta$, $\gamma=1/(4\eta)$.
4. The display in the proof of Theorem 11 (p. 5): $\|u_i^t-u_i^{t-1}\|_*^2\le(n-1)\sum_{j\ne i}\|w_j^t-w_j^{t-1}\|^2\le(n-1)^2\kappa^2$.
5. Theorem 11 (p. 5): RVU with $\alpha>0,\beta>0,\gamma\ge0$ plus stability $\kappa$ give each player regret at most $\alpha+\beta\kappa^2(n-1)^2T$.