Machine Learning

Motivation

A learning algorithm picks a predictor $f$ from a class $F$ after looking at $n$ training examples, and the quantity of interest is its expected loss on a fresh example. Since $f$ depends on the data, its training error is a biased estimate of that loss, and a risk bound quantifies the bias uniformly over the class: with high probability, every $f \in F$ has expected loss at most an observable sample average plus a complexity penalty. Classical penalties (VC dimension, covering numbers, fat-shattering dimension) are fixed in advance; data-dependent penalties such as the Rademacher complexity can be estimated from the sample itself and adapt to the distribution, which matters for model selection by complexity regularization.

Bartlett and Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results (JMLR 3, 2002, jmlr.org), state such a bound in a general decision-theoretic setting (Theorem 8, p. 467): the loss is any $[0,1]$-valued function of an outcome and an action, and the sample average is taken of a dominating cost $\phi \ge \mathcal L$, which may be Lipschitz and hence amenable to the structural results of the paper's §3 even when $\mathcal L$ is a discontinuous $0$–$1$ loss. Multiclass classification with error-correcting output codes is the paper's example. The ingredients — McDiarmid's inequality (McDiarmid, 1989) and symmetrization — are standard; the paper combines them for this setting with a centred cost class. The source is the published JMLR article (pp. 463–482); all page numbers below are its printed pages.

Setting

Let $\mathcal X$ be an input space, $\mathcal Y$ an output space and $\mathcal A$ an action space with a distinguished action $0 \in \mathcal A$, each a measurable space. A probability measure $P$ on $\mathcal X \times \mathcal Y$ generates independent examples $(X_1, Y_1), \dots, (X_n, Y_n)$, and $(X, Y)$ is a fresh draw from $P$.

• A loss is $\mathcal L : \mathcal Y \times \mathcal A \to [0,1]$; a cost $\phi : \mathcal Y \times \mathcal A \to [0,1]$ dominates it if $\phi(y,a) \ge \mathcal L(y,a)$ for all $y, a$.
• $F$ is a class of maps $\mathcal X \to \mathcal A$; the expected loss of $f$ is $\mathbf E\mathcal L(Y, f(X)) = \int \mathcal L(y, f(x))\, dP(x,y)$.
• The empirical mean of $h : \mathcal X \times \mathcal Y \to \mathbb R$ is $\hat{\mathbf E}_n h = \frac1n\sum_{i=1}^n h(X_i, Y_i)$.
• The centred cost class is $\tilde\phi\circ F = \{(x,y) \mapsto \phi(y, f(x)) - \phi(y, 0) : f \in F\}$.
• For a class $G$ of real functions on a space $\mathcal Z$ and a sample $z_1, \dots, z_n$, the empirical Rademacher complexity is

$$\hat R_n(G) = \mathbf E_\sigma \sup_{g \in G}\Bigl|\frac2n\sum_{i=1}^n \sigma_i g(z_i)\Bigr|,$$

with $\sigma_1, \dots, \sigma_n$ independent uniform signs, and the Rademacher complexity is $R_n(G) = \mathbf E\hat R_n(G)$, the expectation over an i.i.d. sample (Definition 2, p. 464). The factor is $2/n$ and the absolute value is inside the supremum.

In Lean these are RadGauss.RiskBound.empiricalRademacher, rademacherComplexity, empMean, supDev (the uniform deviation $\sup_{h \in G}(\mathbf Eh - \hat{\mathbf E}_nh)$), doubleSupDev and phiTildeComp.

Formalization targets

Goal: Theorem 8 (p. 467)

For every integer $n \ge 1$ and every $0 < \delta < 1$, with probability at least $1-\delta$ over the sample, every $f \in F$ satisfies

$$\mathbf E\mathcal L(Y, f(X)) \le \hat{\mathbf E}_n\phi(Y, f(X)) + R_n(\tilde\phi\circ F) + \sqrt{\frac{8\ln(2/\delta)}{n}} .$$

The event is uniform over $F$. The constant $\sqrt 8$ is the printed one.

Milestones (the steps of the paper's proof)

1. Theorem 9 (McDiarmid's inequality), p. 467: for independent, not necessarily identically distributed $X_i$ and $f$ with bounded differences $c_i$,

$$P\{f(X_1,\dots,X_n) - \mathbf Ef(X_1,\dots,X_n) \ge t\} \le e^{-2t^2/\sum_i c_i^2}.$$

2. Bounded differences, p. 467: replacing one example changes $\sup_{h \in \tilde\phi\circ F}(\mathbf Eh - \hat{\mathbf E}_nh)$ by at most $2/n$.
3. Concentration, p. 467: with probability at least $1 - \delta/2$,

$$\sup_{h}(\mathbf Eh - \hat{\mathbf E}_nh) \le \mathbf E\sup_{h}(\mathbf Eh - \hat{\mathbf E}_nh) + \sqrt{2\ln(2/\delta)/n}.$$

4. Combined bound, p. 468: with probability at least $1-\delta$, for all $f \in F$,

$$\mathbf E\mathcal L(Y, f(X)) \le \hat{\mathbf E}_n\phi(Y, f(X)) + \mathbf E\sup_{h \in \tilde\phi\circ F}(\mathbf Eh - \hat{\mathbf E}_nh) + \sqrt{8\ln(2/\delta)/n}.$$

5. Symmetrization, p. 468:

$$\mathbf E\sup_{h \in \tilde\phi\circ F}(\mathbf Eh - \hat{\mathbf E}_nh) \le R_n(\tilde\phi\circ F).$$

The platform's Proved UnderstandingML.representativeness_le_rademacher (Shalev-Shwartz and Ben-David, Lemma 26.2) is included as a supporting reference: it is the middle inequality of milestone 5 in the $1/n$, absolute-value-free normalization.

Significance

Theorem 8 bounds the expected loss of any predictor in the class, including one selected by the data, by quantities the learner can compute or estimate: the empirical cost and the Rademacher complexity of the centred cost class, which concentrates around its empirical version. Combined with the paper's structural results (§3: contraction by Lipschitz maps, convex hulls, sums), it yields margin bounds for voting methods, neural networks and kernel machines (§4) from complexities of simple base classes. Centring by $\phi(y,0)$ matters: with the absolute value inside the supremum, $R_n(\phi\circ F)$ can exceed $R_n(\tilde\phi\circ F)$ by order $1/\sqrt n$ even for a single function.

The result is proved in the paper. As far as the platform's catalog shows, it has no machine-checked proof in this normalization; McDiarmid's inequality in the non-identically distributed form, the $2/n$ bounded-difference step and the absolute-value Rademacher symmetrization with factor $2/n$ are not on the platform. A Lean proof would give a reusable risk-bound template for any loss dominated by a bounded cost.

Difficulty

The obvious argument — bound $\mathbf E\phi(Y,f(X)) - \hat{\mathbf E}_n\phi(Y,f(X))$ for a fixed $f$ by Hoeffding's inequality — does not survive the choice of $f$ after seeing the data: the deviation must be controlled uniformly over $F$, and $F$ is typically infinite. The supremum over $F$ is a single random variable, but its expectation is not obviously small, and relating it to the Rademacher complexity requires a ghost sample and a sign-swap symmetry of the product measure. In a formal development, the supremum of an uncountable family is not automatically measurable; the expectations the argument manipulates must be genuine, not lower integrals, which is why the statements carry explicit measurability hypotheses. McDiarmid's inequality itself, for independent but not identically distributed coordinates, is a martingale-difference concentration argument that is not in Mathlib in this form.

Formalization scope

• Sample and law. A sample is S : Fin n → X × Y, its law the product Measure.pi (fun _ => P). "With probability at least $1-\delta$, every $f \in F$ satisfies …" is encoded by bounding the (outer) measure of $\{S \mid \exists f \in F,\ \neg\,\text{bound}\}$ by $\delta$, with $0 < \delta < 1$.
• Complexities in $[0,\infty]$. $\hat R_n$ is an average over all $2^n$ sign vectors (Fin n → Bool, true $= +1$) of $[0,\infty]$-valued suprema; $R_n$ is its Lebesgue integral. The goal is stated in $[0,\infty]$, with the real terms embedded by ENNReal.ofReal (all are nonnegative). A real supremum or a Bochner integral would silently return $0$ on an unbounded class or a non-integrable integrand, making the bound trivially false or vacuous; this is ruled out by the choice of codomain.
• Added hypotheses, all implicit in the paper. $n \ge 1$ (at $n = 0$ Lean's $1/0 = 0$ makes the bound read $\mathbf E\mathcal L \le 0$, which is false); measurability of $\mathcal L$, $\phi$ and every $f \in F$; a distinguished action $0$ ([Zero A]).
• Measurability guard. The goal and milestones 3–5 assume measurability of exactly the random variables the proof integrates: the uniform deviation $S \mapsto \sup_{h \in \tilde\phi\circ F}(\mathbf Eh - \hat{\mathbf E}_nh)$, the empirical Rademacher complexity $S \mapsto \hat R_n(\tilde\phi\circ F)$, and the double-sample deviation $(S,S') \mapsto \sup_h(\frac1n\sum_i h(S'_i) - \hat{\mathbf E}_nh)$. These hold, for example, for countable $F$; the same guard is used by UnderstandingML.representativeness_le_rademacher.
• No printed slip was found in the statements formalized here. In Theorem 9, if every $c_i = 0$ the printed exponent has a zero denominator; Lean reads it as $0$ and the bound as $1$, which is true.
• Not formalized: the paper's Theorem 10 and the applications; this mission covers Definition 2 and §2 up to the end of the proof of Theorem 8.

Contributions welcome: a proof of McDiarmid's inequality for Measure.pi (reusable well beyond this mission), the ghost-sample symmetrization with the sign-swap invariance of $P^n \otimes P^n$, and the final assembly.

Selected references

• P. L. Bartlett and S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002), 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics 1989, London Math. Soc. Lecture Note Series 141, Cambridge University Press, 148–188. https://doi.org/10.1017/CBO9781107359949.008
• S. Shalev-Shwartz and S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 26. https://doi.org/10.1017/CBO9781107298019
• V. Koltchinskii and D. Panchenko, Empirical margin distributions and bounding the generalization error of combined classifiers, Annals of Statistics 30 (2002), 1–50. https://doi.org/10.1214/aos/1015362183

Motivation

In best arm identification with fixed confidence, a learner samples $K$ unknown distributions (arms) sequentially and must, as early as possible, name the arm with the largest mean, while being wrong with probability at most a prescribed risk $\delta$. The problem models adaptive A/B/n testing, clinical and simulation-based selection among alternatives, and the "ranking and selection" problem of operations research and simulation optimization. The quantity of interest is the sample complexity $\mathbb E_{\boldsymbol\mu}[\tau_\delta]$, the expected number of samples a strategy takes before stopping.

Timeline of the question this mission formalizes:

• Chernoff (1959) introduced sequential tests based on generalized likelihood ratios for adaptive design of experiments, with a finite set of hypotheses (doi:10.1214/aoms/1177706205).
• Kaufmann, Cappé and Garivier (2016, JMLR) proved a change-of-measure lower bound on the sample complexity of every $\delta$-PAC strategy (arXiv:1407.4443).
• Garivier and Kaufmann (COLT 2016) identified the exact constant $T^*(\boldsymbol\mu)$ in that lower bound and gave the first strategy, Track-and-Stop, whose sample complexity matches it asymptotically as $\delta\to0$ (arXiv:1602.04589). This mission covers the upper-bound half of that paper.

Setting

A canonical one-parameter exponential family is a family of laws $\nu_\theta$, $\theta\in\Theta$, on $\mathbb R$ with density $\exp(\theta x-b(\theta))$ with respect to a reference measure $\xi$; $b$ is twice differentiable and strictly convex, and $\nu_\theta$ has mean $\dot b(\theta)$. Bernoulli, Poisson and Gaussian laws with known variance are examples. The divergence $d(\mu,\mu')$ is the Kullback–Leibler divergence between the members with means $\mu$ and $\mu'$.

A bandit model $\boldsymbol\mu=(\mu_1,\dots,\mu_K)$ assigns a member of the family to each arm. The class $\mathcal S$ consists of models with a unique optimal arm $a^*(\boldsymbol\mu)$. At each round $t=1,2,\dots$ the learner picks an arm $A_t$ as a function of past observations, observes a reward drawn from that arm's law, and at a stopping time $\tau_\delta$ recommends an arm. $N_a(t)$ is the number of draws of arm $a$ in the first $t$ rounds and $\hat\mu_a(t)$ its empirical mean.

With $\mathrm{Alt}(\boldsymbol\mu)=\{\boldsymbol\lambda\in\mathcal S: a^*(\boldsymbol\lambda)\ne a^*(\boldsymbol\mu)\}$ and $\Sigma_K$ the probability simplex, the characteristic time is

$$T^*(\boldsymbol\mu)^{-1}=\sup_{w\in\Sigma_K}\ \inf_{\boldsymbol\lambda\in\mathrm{Alt}(\boldsymbol\mu)}\ \sum_{a=1}^K w_a\,d(\mu_a,\lambda_a),$$

and the maximizer $w^*(\boldsymbol\mu)$ are the optimal proportions of arm draws.

Track-and-Stop combines two ingredients:

• a sampling rule that tracks the plug-in proportions $w^*(\hat{\boldsymbol\mu}(t))$ while forcing each arm to be drawn about $\sqrt t$ times: C-Tracking tracks the cumulated sum of projections of $w^*(\hat{\boldsymbol\mu}(s))$ onto $\Sigma^{\epsilon_s}_K=\{w\in\Sigma_K: w_a\ge\epsilon_s\}$, $\epsilon_s=(K^2+s)^{-1/2}/2$; D-Tracking draws an under-sampled arm when some $N_a(t)<\sqrt t-K/2$, and otherwise the arm maximizing $t\,w^*_a(\hat{\boldsymbol\mu}(t))-N_a(t)$;
• Chernoff's stopping rule, which stops at the first $t$ at which some arm $a$ beats every other arm $b$ in a generalized likelihood ratio test, $Z_{a,b}(t)>\beta(t,\delta)$, here with $\beta(t,\delta)=\log(r(t)/\delta)$.

Formalization targets

Goal: Theorem 14 (p. 13)

For $\alpha\in[1,e/2]$ and $r(t)=O(t^\alpha)$, Chernoff's stopping rule with $\beta(t,\delta)=\log(r(t)/\delta)$ combined with C-Tracking or D-Tracking satisfies

$$\limsup_{\delta\to0}\frac{\mathbb E_{\boldsymbol\mu}[\tau_\delta]}{\log(1/\delta)}\le\alpha\,T^*(\boldsymbol\mu)$$

for every $\boldsymbol\mu\in\mathcal S$.

Milestones

• Lemma 15 (p. 20): greedy tracking of cumulated proportions $P(k)$ keeps $\max_i|N_i(n)-P_i(n)|\le K-1$.
• Lemma 7 (p. 7): C-Tracking ensures $N_a(t)\ge\sqrt{t+K^2}-2K$ and $\max_a|N_a(t)-\sum_{s<t}w^*_a(\hat{\boldsymbol\mu}(s))|\le K(1+\sqrt t)$.
• Lemma 8 (p. 7): D-Tracking ensures $N_a(t)\ge(\sqrt t-K/2)_+-1$, and proportions within $3(K-1)\epsilon$ of $w^*(\boldsymbol\mu)$ after a time $t_\epsilon$ that does not depend on the trajectory, once the plug-in targets are within $\epsilon$.
• Proposition 9 (p. 8): under either rule, $N_a(t)/t\to w^*_a(\boldsymbol\mu)$ almost surely.
• Lemma 18 (p. 27): an explicit $x$ with $c_1x\ge\log(c_2x^\alpha)$ for $\alpha\in[1,e/2]$.
• Proposition 13 (p. 11): with any sampling rule whose proportions converge almost surely to $w^*$, $\tau_\delta<\infty$ almost surely and $\limsup_{\delta\to0}\tau_\delta/\log(1/\delta)\le\alpha T^*(\boldsymbol\mu)$ almost surely.

Significance

Theorem 1 of the same paper shows $\mathbb E_{\boldsymbol\mu}[\tau_\delta]\ge T^*(\boldsymbol\mu)\,\mathrm{kl}(\delta,1-\delta)$ for every $\delta$-PAC strategy, and $\mathrm{kl}(\delta,1-\delta)\sim\log(1/\delta)$. Theorem 14 with $\alpha=1$ therefore shows that the lower bound is attained: $T^*(\boldsymbol\mu)$ is the exact asymptotic sample complexity of best arm identification in exponential family models, and Track-and-Stop is asymptotically optimal.

The result is proved in the paper. What is not available is a machine-checked proof for exponential families. The platform already holds a Lean development of the Gaussian case following Lattimore and Szepesvári, Bandit Algorithms, Ch. 33, stated for one existentially chosen policy with a different threshold. This mission asks for the universal statement: every run of either tracking rule, for every exponential family, with the paper's thresholds. The tracking lemmas (Lemmas 15, 7, 8) are deterministic combinatorics and reusable by any tracking-based algorithm.

Difficulty

The obvious argument plugs the almost-sure behaviour of Proposition 13 into an expectation. That step fails: almost-sure convergence of $\tau_\delta/\log(1/\delta)$ does not control $\mathbb E[\tau_\delta]$, because on the rare events where the empirical means are far from $\boldsymbol\mu$ the stopping time may be very large. Theorem 14 needs a quantitative concentration of $\hat{\boldsymbol\mu}(t)$ on events whose complements have summable probability, which in turn relies on the forced exploration guaranteed by the $\sqrt t$ lower bounds on $N_a(t)$ (the concentration step of App. D, Lemmas 19–20).

A second obstacle is the regularity of $w^*$: the tracking lemmas only transfer convergence of $\hat{\boldsymbol\mu}(t)$ to convergence of $N_a(t)/t$ through the continuity of $\boldsymbol\mu\mapsto w^*(\boldsymbol\mu)$ on $\mathcal S$, proved from the characterization of $w^*$ in §2.2 (Proposition 6). The GLR statistic also needs its closed form (7) near $\boldsymbol\mu$, which requires the empirical means to lie in the interior of the mean space.

Formalization scope

• Model. The exponential family is a structure $(\xi,\Theta,b)$ with $\Theta$ a nonempty open interval, each $\nu_\theta$ normalized, $b$ twice continuously differentiable and $\ddot b>0$ on $\Theta$. Openness and $\ddot b>0$ are added to the paper's "convex, twice differentiable"; strict convexity is what makes $\nu^\mu$ unique. Bandit models are parameter vectors $\theta\in\Theta^K$ with $K\ge2$; arms are indexed $0,\dots,K-1$. $\mathcal S$ is the set of parameter vectors with a unique arm of largest mean $\dot b(\theta_a)$.
• Protocol. Policies, the trajectory law $\mathbb P_{\boldsymbol\mu}$, pull counts, empirical means and $T^*(\boldsymbol\mu)$ are the platform's published definitions (BanditPolicy, BanditTrajectory, TrackAndStop). $T^*$ uses Kullback–Leibler divergences of the arm laws over the class $\mathcal S$ and takes values in $[0,\infty]$. Trajectory coordinate $t$ is round $t+1$. An arm never drawn has empirical mean $0$.
• Target map. $w^*(\hat{\boldsymbol\mu}(t))$ is undefined in the paper when $\hat{\boldsymbol\mu}(t)\notin\mathcal S$ (an unsampled arm, ties, a mean outside $\dot b(\Theta)$). Every tracking statement quantifies over every target map with values in $\Sigma_K$ that returns optimal proportions on $\mathcal S$, over every choice of $L^\infty$ projections, and over every tie-breaking, including randomized ones.
• Stopping rule. The two maxima in $Z_{a,b}(t)$ are suprema over $\Theta$ in the extended reals. $Z_{a,b}(t)>\beta$ is written without subtracting infinities. The stopping time is the first $t\ge1$ at which the test succeeds, $+\infty$ if none. "$r(t)=O(t^\alpha)$" is $r(t)\le Dt^\alpha$ for $t\ge1$; $r>0$ is added so that $\log(r(t)/\delta)$ is defined.
• Values in $[0,\infty]$. Expectations of $\tau_\delta$, the ratios and $T^*$ live in $[0,\infty]$. No statement converts them to reals, so an infinite expected stopping time is never read as $0$.
• Corrections, disclosed. Proposition 9's printed $\mathbb P_w$ is $\mathbb P_{\boldsymbol\mu}$. Lemma 18 adds $c_2/c_1^\alpha>1$ and $x>0$, without which its expressions are undefined.
• Ruled out. Specializing to Gaussian arms, or asserting that some sampling policy achieves the bound, would restate existing platform results and is not this theorem: the goal is about every C-Tracking or D-Tracking run in every exponential family.
• Welcome contributions. Exponential-family facts ($\dot b$ is the mean, the KL formula, concentration of empirical means); the continuity of $w^*$ (Proposition 6, App. A.3); Lemma 17 (App. B.2), from which Lemma 8 follows; the closed form (7) of the GLR statistic.

Selected references

• A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016, JMLR W&CP 49. arXiv:1602.04589v2
• E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, JMLR 17, 2016. arXiv:1407.4443
• H. Chernoff, Sequential Design of Experiments, Ann. Math. Statist. 30(3), 1959. doi:10.1214/aoms/1177706205
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Ch. 33. doi:10.1017/9781108571401

Motivation

Best arm identification with fixed confidence is the pure-exploration counterpart of the multi-armed bandit problem. A learner faces $K$ unknown reward distributions ("arms"), samples them sequentially, and must stop and name the arm with the largest mean, being wrong with probability at most a prescribed $\delta$. The question is how many samples this requires. It arises in adaptive A/B testing, in the selection of the best of several simulated systems (ranking and selection in simulation optimization), and in clinical trials that must declare the best treatment with a guaranteed error rate.

Lower bounds for this problem were first stated in terms of the gaps between means (Mannor and Tsitsiklis, 2004). Kaufmann, Cappé and Garivier (2016) replaced ad hoc changes of measure by a single "transportation" lemma relating expected sample counts, Kullback–Leibler divergences and the error probability. Garivier and Kaufmann (COLT 2016, arXiv:1602.04589v2) combine this lemma over all alternative models at once, in the spirit of Graves and Lai (1997), and obtain a lower bound whose constant $T^*(\boldsymbol\mu)$ is exactly matched, as $\delta \to 0$, by their Track-and-Stop strategy. This mission formalizes that lower bound (Theorem 1 of the paper, p. 3).

Setting

A canonical one-parameter exponential family is given by a reference measure $\xi$ on $\mathbb R$, an open interval $\Theta \subset \mathbb R$ and a function $b$, twice continuously differentiable on $\Theta$ with $\ddot b > 0$, such that the laws $\nu_\theta$ with density $\exp(\theta x - b(\theta))$ with respect to $\xi$ are probability measures for $\theta \in \Theta$. The mean of $\nu_\theta$ is $\dot b(\theta)$. Bernoulli laws and Gaussian laws of known variance are examples.

A bandit model is a vector $\theta = (\theta_1, \dots, \theta_K) \in \Theta^K$; arm $a$ returns i.i.d. rewards with law $\nu_{\theta_a}$ and mean $\mu_a = \dot b(\theta_a)$. Arm $a^*(\boldsymbol\mu)$ is the unique optimal arm if $\mu_{a^*} > \mu_a$ for every $a \ne a^*$. Let $\mathcal S$ be any set of bandit models of the family each having a unique optimal arm, and put $\mathrm{Alt}(\boldsymbol\mu) = \{\boldsymbol\lambda \in \mathcal S : a^*(\boldsymbol\lambda) \ne a^*(\boldsymbol\mu)\}$.

A strategy consists of a sampling rule $\pi$ (the arm $A_t$ drawn at round $t$ depends, possibly with extra randomization, on the first $t - 1$ observations), a stopping time $\tau$ of the natural filtration $\mathcal F_t = \sigma(A_1, X_1, \dots, A_t, X_t)$, and an $\mathcal F_\tau$-measurable decision $\hat a_\tau$. It is $\delta$-PAC on $\mathcal S$ if for every $\boldsymbol\mu \in \mathcal S$, $\mathbb P_{\boldsymbol\mu}(\tau < \infty) = 1$ and $\mathbb P_{\boldsymbol\mu}(\hat a_\tau \ne a^*(\boldsymbol\mu)) \le \delta$. $N_a(t)$ is the number of draws of arm $a$ among the first $t$ rounds.

Write $d(\mu_a, \lambda_a) = \mathrm{KL}(\nu_{\theta_a}, \nu_{\lambda_a})$ for the divergence between two arm laws, $\mathrm{kl}(x, y) = x\log\frac{x}{y} + (1 - x)\log\frac{1 - x}{1 - y}$, and $\Sigma_K$ for the probability simplex on the $K$ arms. The characteristic time is defined by eq. (1):

$$T^*(\boldsymbol\mu)^{-1} = \sup_{w \in \Sigma_K}\ \inf_{\boldsymbol\lambda \in \mathrm{Alt}(\boldsymbol\mu)} \sum_{a=1}^K w_a\, d(\mu_a, \lambda_a).$$

Formalization targets

Goal: Theorem 1 (p. 3)

For $\delta \in (0, 1/2]$, every $\delta$-PAC strategy on $\mathcal S$ and every $\boldsymbol\mu \in \mathcal S$,

$$\mathbb E_{\boldsymbol\mu}[\tau] \ \ge\ T^*(\boldsymbol\mu)\,\mathrm{kl}(\delta, 1 - \delta).$$

The statement fixes no constant beyond those of the paper, and it holds for every $\delta$, not only in the limit.

Milestone: eq. (2) (p. 4)

For every $\boldsymbol\lambda \in \mathcal S$ with $a^*(\boldsymbol\lambda) \ne a^*(\boldsymbol\mu)$,

$$\sum_{a=1}^K d(\mu_a, \lambda_a)\, \mathbb E_{\boldsymbol\mu}[N_a(\tau)] \ \ge\ \mathrm{kl}(\delta, 1 - \delta).$$

This is Lemma 1 of Kaufmann et al. (2016), which the paper quotes without proof; Theorem 1 follows from it for every alternative simultaneously.

Significance

Theorem 1 identifies $T^*(\boldsymbol\mu)$ as the exact problem-dependent complexity of fixed-confidence best arm identification: since $\mathrm{kl}(\delta, 1 - \delta) \sim \log(1/\delta)$, it gives $\liminf_{\delta \to 0} \mathbb E_{\boldsymbol\mu}[\tau_\delta]/\log(1/\delta) \ge T^*(\boldsymbol\mu)$, and the paper's Track-and-Stop strategy attains this rate (the subject of mission IV of this series). The bound also explains which proportions of draws an optimal strategy must use: the maximizer $w^*(\boldsymbol\mu)$ of eq. (1) (mission II).

Both results are proved in the literature. Neither is formalized in the paper's generality. The platform holds the textbook form of Lattimore and Szepesvári (Theorem 33.5), which is stated for an arbitrary class with the weaker constant $\log(1/(4\delta))$; for $\delta \le 1/2$, $\mathrm{kl}(\delta, 1 - \delta) \ge \log(1/(2.4\delta)) > \log(1/(4\delta))$, so Theorem 1 is strictly stronger. A formal proof here yields the transportation lemma for exponential families on the platform's infinite-horizon bandit model, which later missions (II–IV, and any lower bound by change of measure) can reuse.

Difficulty

The obvious proof applies the finite-horizon divergence decomposition $\mathrm{KL}(\mathbb P^n_{\boldsymbol\mu}, \mathbb P^n_{\boldsymbol\lambda}) = \sum_a \mathbb E_{\boldsymbol\mu}[N_a(n)]\,d(\mu_a, \lambda_a)$ at a deterministic horizon $n$. That fails here: $\tau$ is random and unbounded, the decision is $\mathcal F_\tau$-measurable, and the relevant divergence is between the laws of the stopped observations. The step from a fixed horizon to a stopping time, together with the data-processing inequality that turns the error guarantees under two models into $\mathrm{kl}(\delta, 1 - \delta)$, is the central difficulty. A second, smaller difficulty is to identify the paper's divergence $d$ and its means $\dot b(\theta)$ with the measure-theoretic KL divergence and mean of the arm laws of the exponential family.

Formalization scope

Lean namespace OptimalBAI.LowerBound. The bandit protocol is the platform's (BanditAlgorithm.BanditPolicy, banditTrajMeasure, IsBanditStoppingTime, IsSoundBAI, baiComplexity); $\mathrm{kl}$ is the platform's bernoulliRelativeEntropy and $N_a(t)$ is trajPullCount. Conventions:

• arms are Fin K, 0-based (the paper's arm $a$ is index $a - 1$); trajectory coordinate $t$ is round $t + 1$;
• $\Theta$ is a nonempty open interval and $\ddot b > 0$ on $\Theta$ (added: the paper says $b$ is convex and twice differentiable; strict convexity is what makes "the unique distribution with mean $\mu$" meaningful); the paper's $d$ is written as the KL divergence of the arm laws (its first equality on p. 3), and the unique optimal arm is defined through the parameter means $\dot b(\theta_a)$;
• $\mathcal S$ is an arbitrary set of models with a unique optimal arm, not the specific set the paper fixes from p. 4 on;
• $\delta$-PAC keeps both halves of the paper's definition (almost-sure stopping and error at most $\delta$);
• $T^*(\boldsymbol\mu)$, divergences and expectations of $\tau$ take values in $[0, \infty]$, never truncated to reals; $T^* = 0$ when $\mathrm{Alt}(\boldsymbol\mu) = \emptyset$ and $T^* = \infty$ when the supremum in eq. (1) is $0$;
• $\delta \le 1/2$ is added. The paper states $\delta \in (0, 1)$, but the theorem and eq. (2) are false for $\delta \in (1/2, 1)$: with two unit-variance Gaussian arms, drawing arm 1 once and naming arm 1 exactly when the fractional part of the reward is below $1/2$ is $0.9$-PAC, while $T^*(\boldsymbol\mu) \to \infty$ as the two means merge. At $\delta = 1/2$ the bound is $0$.

A statement with $\log(1/(4\delta))$ in place of $\mathrm{kl}(\delta, 1 - \delta)$, or restricted to Gaussian arms, is the platform's existing textbook theorem and does not count as this mission's goal; nor does any version that drops the almost-sure stopping clause or truncates $\mathbb E[\tau]$ or $T^*$ to real numbers.

Needed infrastructure: the transportation lemma at a stopping time (data processing for KL through an $\mathcal F_\tau$-measurable event, Wald-type identity for the stopped log-likelihood ratio), the identities "mean of $\nu_\theta$ $= \dot b(\theta)$" and "KL of two family members $= b(\theta') - b(\theta) - \dot b(\theta)(\theta' - \theta)$", and $\mathbb E[\tau] = \sum_a \mathbb E[N_a(\tau)]$. All are reusable beyond this mission. Contributions of any of these lemmas, of eq. (2) alone, or of the Gaussian and Bernoulli special cases as stepping stones are welcome.

Selected references

• A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2. https://arxiv.org/abs/1602.04589
• E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, Journal of Machine Learning Research 17(1), 2016. https://arxiv.org/abs/1407.4443
• T. L. Graves, T. L. Lai, Asymptotically Efficient Adaptive Choice of Control Laws in Controlled Markov Chains, SIAM Journal on Control and Optimization 35(3), 1997. https://doi.org/10.1137/S0363012994275440
• S. Mannor, J. N. Tsitsiklis, The Sample Complexity of Exploration in the Multi-Armed Bandit Problem, Journal of Machine Learning Research 5, 2004. https://www.jmlr.org/papers/v5/mannor04b.html
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 33. https://doi.org/10.1017/9781108571401

Motivation

The stochastic multi-armed bandit is the basic model of sequential decision making under uncertainty: a learner repeatedly chooses one of $d$ actions, observes a noisy reward for the chosen action only, and must balance exploring poorly known actions against exploiting the one that currently looks best. It underlies adaptive clinical trials, online advertising, recommendation, dynamic pricing and many simulation-optimization procedures in operations research.

The standard algorithm is UCB (Auer, Cesa-Bianchi and Fischer, 2002, doi:10.1023/A:1013689704352), which plays the arm with the largest upper confidence bound on its mean. Its confidence widths grow with the current time $t$ (or with a horizon $n$ fixed in advance), and its guarantee is on the expected regret, which grows like $\log n$. Lai and Robbins (1985, doi:10.1016/0196-8858(85)90002-8) showed that logarithmic growth of the expected regret cannot be avoided by a consistent algorithm.

Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) proved a self-normalized concentration inequality for vector-valued martingales that holds uniformly over time. Section 6 of their paper applies it to the $d$-armed bandit. The resulting confidence intervals depend on neither the horizon nor the current time. The UCB variant built on them, UCB($\delta$), has pseudo-regret bounded by a constant, independent of the horizon, on a single event of probability at least $1-\delta$. This mission formalizes that section.

Setting

There are $d \ge 1$ arms with unknown means $\mu_1, \dots, \mu_d \in \mathbb R$. Write $\mu_* = \max_{1 \le i \le d} \mu_i$ for the best mean and $\Delta_i = \mu_* - \mu_i \ge 0$ for the gap of arm $i$.

Randomness lives on a probability space $(\Omega, \mathcal F, P)$ with a filtration $(\mathcal F_t)_{t \ge 0}$. In round $t = 1, 2, \dots$ the learner plays an arm $I_t$ that is $\mathcal F_{t-1}$-measurable and receives the reward $\mu_{I_t} + \eta_t$. The noise $\eta_t$ is $\mathcal F_t$-measurable and conditionally 1-sub-Gaussian:

$$\mathbf E\left[e^{\lambda\eta_t} \mid \mathcal F_{t-1}\right] \le e^{\lambda^2/2} \qquad \text{for all } \lambda \in \mathbb R .$$

The noise need not be independent or identically distributed across rounds, and the rewards need not be bounded.

After $t$ rounds, $N_{i,t}$ is the number of plays of arm $i$ and $\overline X_{i,t}$ is the average reward received from it. For a confidence level $\delta > 0$ the confidence width is

$$c_{i,t} = \sqrt{\frac{1 + N_{i,t}}{N_{i,t}^2}\left(1 + 2\log\frac{d\,(1 + N_{i,t})^{1/2}}{\delta}\right)} \qquad (3)$$

with $c_{i,t} = +\infty$ when $N_{i,t} = 0$. UCB($\delta$) plays, in round $t$, an arm that maximizes $\overline X_{i,t-1} + c_{i,t-1}$; in particular every arm is played once before any comparison is made. The pseudo-regret after $n$ rounds is

$$R_n = \sum_{t=1}^n \left(\mu_* - \mu_{I_t}\right).$$

This is the linear bandit of the paper with the standard basis of $\mathbb R^d$ as decision set and $\theta_* = \mu$.

Formalization targets

Goal: Theorem 7 (constant regret of UCB($\delta$))

For every $\delta > 0$, with probability at least $1-\delta$, for all $n \ge 0$ simultaneously,

$$R_n \le \sum_{i : \Delta_i > 0}\left(3\Delta_i + \frac{16}{\Delta_i}\log\frac{2d}{\Delta_i\delta}\right).$$

The right-hand side depends only on the gaps, $d$ and $\delta$.

Milestone: Lemma 6 (confidence intervals)

For any adapted choice of arms (not only UCB($\delta$)) and every $\delta > 0$, with probability at least $1-\delta$,

$$|\overline X_{i,t} - \mu_i| \le c_{i,t} \qquad \text{for all arms } i \text{ and all } t \ge 0 .$$

Significance

The result. Theorem 7 shows that, once a confidence level is fixed, a UCB-type algorithm can stop paying for exploration after finitely many rounds: with probability $1-\delta$ the total regret over an infinite horizon is bounded. The paper notes that this does not contradict the Lai–Robbins lower bound, which concerns expected regret; on the failure event of probability $\delta$ the regret may grow linearly. Lemma 6 is the practical content behind this: anytime-valid confidence intervals for adaptively sampled means under martingale noise, usable for stopping rules, best-arm identification and any sequential procedure that inspects its estimates at data-dependent times.

Formalizing it. Both results are proved in the paper's appendices (F and G). No machine-checked proof of either is known to exist. The platform already has the self-normalized martingale bound for $V = \lambda I$ and unit sub-Gaussian noise (BanditAlgorithm.self_normalized_martingale_bound, listed here as a reference item), and UCB bounds with horizon-dependent widths and in-expectation or pathwise conclusions. Neither is Theorem 7. The mission produces a formal account of time-uniform confidence intervals for adaptively sampled arm means, and of a regret bound that is uniform in the horizon.

Difficulty

Two points separate this from textbook UCB analyses. First, the number of samples $N_{i,t}$ of an arm is itself random and depends on past noise, so a fixed-sample concentration inequality with a union bound over times does not give widths that are free of $t$: a union bound over all $t$ costs a factor that diverges. The time-uniform event must come from a maximal (self-normalized) inequality applied to the martingale $\sum_s \eta_s \mathbf 1\{I_s = i\}$. Second, the regret statement is uniform in $n$ with constants depending on the gaps; converting a condition of the form "$c(N) \ge \Delta_i/2$" into an explicit bound on $N$ requires solving an inequality in which $N$ appears both polynomially and inside a logarithm, and the explicit constants $3$ and $16$ must come out of that step.

Formalization scope

The Lean development lives in the namespace ImprovedLinBandits.UCBDelta.

• Arms are Fin d with 0 < d in the goal; means are μ : Fin d → ℝ, $\mu_*$ is ⨆ i, μ i (the maximum over a nonempty finite type).
• Rounds are indexed t + 1 for t : ℕ: the arm I (t + 1) is ℱ t-measurable, the noise η (t + 1) is ℱ (t + 1)-measurable and satisfies Mathlib's HasCondSubgaussianMGF (ℱ t) … (η (t + 1)) 1 P. Values at index $0$ are unused.
• The sample space is assumed to be a standard Borel space, which Mathlib's conditional sub-Gaussianity requires; this hypothesis is not in the paper.
• "With probability at least $1-\delta$, for all …" is stated as: the outer probability of the failure event, with the quantifiers over arms and times inside it, is at most $\delta$. For $\delta \ge 1$ the statements are trivially true, as in the paper.
• The rule (4) is read with the statistics of rounds $1, \dots, t-1$, because the printed $\overline X_{i,t}$, $c_{i,t}$ already count round $t$. An unplayed arm, whose width is $+\infty$ in the paper, is played before the indices are compared. Every tie-breaking rule is allowed, and measurability of the chosen arm is assumed rather than derived.
• The printed Theorem 7 has no quantifier on $n$; it is formalized in the uniform-in-$n$ form, matching the section's claim of constant regret and the time-uniform event of Lemma 6.
• Lean's division by zero makes $\overline X_{i,t}$ and $c_{i,t}$ equal to $0$ when $N_{i,t} = 0$. Lemma 6 therefore excludes $N_{i,t} = 0$ explicitly (where the paper's inequality is vacuous), and the run predicate handles unplayed arms separately. The regret bound sums over arms with $\Delta_i > 0$, so its divisions are well defined.

A trivializing formalization is ruled out: the confidence event is not assumed as a hypothesis of Theorem 7, the i.i.d. bandit model is not substituted for the martingale noise model, and no bound on the means or rewards is imposed.

Useful infrastructure for solvers: the self-normalized bound of Theorem 1 in the scalar case ($d = 1$, $\lambda = 1$, $A_s = \mathbf 1\{I_s = i\}$, $\overline V_t = 1 + N_{i,t}$), a union bound over arms, and elementary inequalities inverting $N \mapsto \frac{1+N}{N^2}(1 + 2\log(d\sqrt{1+N}/\delta))$. Lemmas about pull counts and empirical means under adaptive sampling are reusable beyond this mission and are welcome as contributions.

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://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
• P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time Analysis of the Multiarmed Bandit Problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• T. L. Lai, H. Robbins, Asymptotically Efficient Adaptive Allocation Rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• J.-Y. Audibert, R. Munos, Cs. Szepesvári, Exploration–exploitation tradeoff using variance estimates in multi-armed bandits, Theoretical Computer Science 410, 2009. https://doi.org/10.1016/j.tcs.2009.01.016

Motivation

Online convex optimization is a repeated game between a learner and an adversary. In each round $t=1,\dots,T$ the learner commits to a point $x_t$ of a convex set $\mathcal P\subseteq\mathbb R^n$; only then is a convex cost function $f_t$ revealed, and the learner pays $f_t(x_t)$. The learner is judged by its regret: its total cost minus the total cost of the best fixed point chosen in hindsight. The model covers online portfolio selection, online regression, prediction with expert advice and the analysis of stochastic gradient methods, and it is the standard language of online learning theory.

Zinkevich (ICML 2003) showed that projected gradient descent with step sizes of order $1/\sqrt t$ has regret $O(GD\sqrt T)$ for any convex costs with gradients bounded by $G$ on a set of diameter $D$, and this rate cannot be improved for linear costs. Hazan, Agarwal and Kale (Machine Learning 69, 2007) asked what curvature buys. Their first result, the subject of this mission, is that the same algorithm with the faster step sizes $1/(Ht)$ has regret only logarithmic in $T$ once every cost function is $H$-strongly convex. The paper's other three results (the Online Newton Step, Follow the Approximate Leader and Exponentially Weighted Online Optimization, for exp-concave costs) are the subject of the other missions of this series.

Setting

Fix $n\in\mathbb N$ and a nonempty, closed, bounded, convex set $\mathcal P\subseteq\mathbb R^n$, with the Euclidean norm $\|\cdot\|_2$ (§2.1, p. 171).

• Cost functions. A sequence $f_1,f_2,\dots:\mathbb R^n\to\mathbb R$. Write $\nabla f_t(x)$ for the gradient and $\nabla^2 f_t(x)$ for the Hessian.
• Gradient bound. A number $G$ with $\|\nabla f_t(x)\|_2\le G$ for all $x\in\mathcal P$ and all rounds $t$ (p. 172).
• $H$-strong convexity (p. 172). For $H>0$, $f$ is $H$-strongly convex on $\mathcal P$ when it is twice differentiable and $\nabla^2 f(x)\succeq H I_n$ for every $x\in\mathcal P$, i.e. $v^\top\nabla^2 f(x)v\ge H\|v\|_2^2$ for all $v$.
• Euclidean projection. $\Pi_{\mathcal P}(y)$ is the point of $\mathcal P$ nearest to $y$, $\Pi_{\mathcal P}(y)=\arg\min_{x\in\mathcal P}\|x-y\|_2$ (IsProj P y z).
• Online Gradient Descent (Fig. 1, p. 174), with step sizes $\eta_1,\eta_2,\dots$: $x_1\in\mathcal P$ is arbitrary, and in iteration $t>1$

$$x_t=\Pi_{\mathcal P}\bigl(x_{t-1}-\eta_t\nabla f_{t-1}(x_{t-1})\bigr)$$

(IsOGDRun P η f x).

• Regret (p. 171): $\mathrm{Regret}_T=\sum_{t=1}^T f_t(x_t)-\min_{x\in\mathcal P}\sum_{t=1}^T f_t(x)$, and $\mathrm{Regret}_T(\mathrm{OGD})$ is its supremum over all cost sequences.

Formalization targets

Goal: Theorem 1 (p. 175)

For $H>0$, cost functions that are $H$-strongly convex on $\mathcal P$ with gradients bounded by $G$ on $\mathcal P$, and any run of Online Gradient Descent whose step after round $t$ is $\eta_{t+1}=1/(Ht)$, for every $T\ge1$ and every $u\in\mathcal P$:

$$\sum_{t=1}^{T}\bigl(f_t(x_t)-f_t(u)\bigr)\ \le\ \frac{G^2}{2H}\,\bigl(1+\log T\bigr).$$

This is LogRegretOCO.OGD.ogd_regret_bound. The constant is the paper's, and at $T=1$ the bound reads $G^2/(2H)$.

Milestones

1. Eq. (1), the strong-convexity inequality: for $x,y\in\mathcal P$, $2(f(x)-f(y))\le 2\nabla f(x)^\top(x-y)-H\|y-x\|_2^2$.
2. Lemma 8 with $A=I_n$: for a convex $\mathcal P$, $z=\Pi_{\mathcal P}(y)$ and $a\in\mathcal P$, $\|y-a\|_2^2\ge\|z-a\|_2^2$. This is already on the platform, proved, as UnderstandingML.projection_lemma, and is reused as a reference item.
3. Eq. (2), the one-step inequality: for $z=\Pi_{\mathcal P}(x-\eta g)$, $\eta>0$, $\|g\|_2\le G$ and $u\in\mathcal P$, $2g^\top(x-u)\le(\|x-u\|_2^2-\|z-u\|_2^2)/\eta+\eta G^2$.

The last step of the argument is the harmonic-sum bound $\sum_{t=1}^T 1/t\le 1+\log T$, which Mathlib already provides (harmonic_le_one_add_log).

Significance

The result. Theorem 1 separates two regimes of online convex optimization: $\Theta(\sqrt T)$ regret for general convex costs and $O(\log T)$ for strongly convex ones, with an algorithm that costs one gradient and one projection per round. Through the online-to-batch conversion, the same step-size schedule gives the $O(\log T/T)$ rate of stochastic gradient descent on strongly convex objectives. The theorem is also the reference point for the paper's weaker exp-concavity assumption, under which the other three algorithms obtain $O(n\log T)$ regret.

Formalizing it. The result is proved and well known; what this mission adds is a machine-checked proof with the paper's exact constant. The Prove2Me platform holds a statement of the textbook version of this theorem (Hazan, Introduction to Online Convex Optimization, Theorem 3.3), OnlineConvexOpt.FirstOrder.online_gradient_descent_strongly_convex_regret, but it is Disproved: its regret is written with a real infimum over the decision set, which Lean evaluates to a junk value. No proved version of the logarithmic bound is on the platform. The strong-convexity inequality, the one-step projected-gradient inequality and the telescoping argument are reusable by every later formalization of gradient methods on the platform.

Difficulty

The argument is short, and its difficulty lies in the bookkeeping. The telescoping sum of squared distances cancels exactly only with the right step-size indexing: the step taken after round $t$ must be $1/(Ht)$. Reading Fig. 1 literally with $\eta_t=1/(Ht)$ makes the step after round $t$ equal to $1/(H(t+1))$, and the sum then leaves an uncancelled term $\frac H2\|x_1-x^*\|_2^2$ that the printed bound does not contain. Strong convexity is a statement about the Hessian, so the curvature inequality (1) needs a second-order Taylor expansion along a segment of $\mathcal P$; convexity of $\mathcal P$ keeps the segment inside the set where the Hessian bound holds. The projection step needs the obtuse-angle property of Euclidean projection onto a convex set.

Formalization scope

Points are EuclideanSpace ℝ (Fin n), so $\|\cdot\|$ is the Euclidean norm (the sup norm of Fin n → ℝ would change the gradient bound). Cost functions are functions on all of $\mathbb R^n$, as the paper's use of gradients and Hessians presupposes; the gradient is Mathlib's gradient, and the Hessian quadratic form is the second Fréchet derivative applied to $(v,v)$. Rounds are 1-based: x 0, f 0 and η 1 are never read, and sums run over Finset.Icc 1 T. The run of the algorithm is a predicate on the whole trajectory, required at every round; the projection is a predicate (nearest point of $\mathcal P$), which is unique for nonempty closed convex $\mathcal P$.

Choices and corrections relative to the printed text:

• Step-size index. Theorem 1 prints "step sizes $\eta_t=\frac1{Ht}$", while its proof sets $\eta_{t+1}=1/(Ht)$ for the step after round $t$. The goal uses the proof's indexing, as a hypothesis η (t + 1) = 1 / (H * t) for $t\ge1$ on the step sizes of Fig. 1.
• Eq. (2). The paper prints "$5\nabla_t^\top(x_t-x^*)$"; the $5$ is a typo for $2$, and the milestone states $2$. The verbatim milestone text keeps the printed $5$.
• Regret. Regret is stated against every comparator $u\in\mathcal P$; the minimum over the compact set $\mathcal P$ is attained, so this is the paper's statement. The expectation in the paper's regret is vacuous for this deterministic algorithm, and the supremum over cost sequences is the universal quantifier over $f$.
• Hypotheses. Strong convexity and the gradient bound are required for the rounds $1,\dots,T$ only. Convexity of each $f_t$, a standing assumption of §2.2, follows from $H$-strong convexity on the convex set $\mathcal P$ and is not added. No diameter bound enters Theorem 1.

A regret bound written with a real ⨅/sInf over $\mathcal P$, or a bound for an arbitrary sequence satisfying Eq. (2) instead of a run of the paper's algorithm, would not be Theorem 1; the goal quantifies over every comparator in $\mathcal P$ and carries the run predicate, the Hessian hypothesis and the gradient bound. The hypotheses are jointly satisfiable: on the closed unit ball, $f_t(x)=\frac H2\|x\|_2^2$ with $G=H$ meets all of them.

Contributions welcome: proofs of the two inequalities and of the goal; a general projection lemma for positive semidefinite $A$ (Lemma 8 in full, needed by the Online Newton Step mission) is reusable beyond this mission.

Selected references

• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., MIT Press 2022 (Theorem 3.3). https://arxiv.org/abs/1909.05207
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014 (Lemma 14.9, the projection lemma). https://doi.org/10.1017/CBO9781107298019

Motivation

In many operational problems (shortest paths, assignment, planning) the decision solves a linear program whose cost vector is unknown at decision time and is predicted from contextual features. The predict-then-optimize pipeline fits a model $f$ that maps a feature vector $x$ to a predicted cost vector $\hat c=f(x)$, and then acts on the decision that is optimal for $\hat c$. Elmachtoub and Grigas (Smart "Predict, then Optimize", Management Science 2022) proposed to measure the quality of such a model not by the prediction error but by the SPO loss (Smart Predict-then-Optimize loss): the excess true cost of the decision induced by the prediction over the best decision in hindsight.

The question is whether a small SPO loss on the training sample implies a small SPO loss on new data, uniformly over the models a training procedure may return. The SPO loss is neither convex nor continuous in the prediction, so the standard Lipschitz-based bounds for regression do not apply. El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3, Mathematics of Operations Research 2023; a preliminary version appeared at NeurIPS 2019) give the first such generalization bounds. This mission formalizes their first one, for polyhedral feasible regions, which treats every vertex of the feasible region as a class label of a multiclass classification problem. The bound has since been used by later work, e.g. Hu, Kallus and Mao (Fast rates for contextual linear optimization, Management Science 2022), who sharpen it by a $\sqrt{\log n}$ factor (as noted on p. 4 of the paper).

Setting

A feasible region $S\subseteq\mathbb R^d$ is nonempty, compact and convex. For a cost vector $c\in\mathbb R^d$ the nominal problem is $\min_{w\in S}c^\top w$. An optimization oracle is a fixed map $w^*:\mathbb R^d\to S$ with $w^*(c)\in\arg\min_{w\in S}c^\top w$ for every $c$; nothing is assumed about how it breaks ties. The SPO loss of a prediction $\hat c$ when the realized cost is $c$ is

$$\ell_{\rm SPO}(\hat c,c)=c^\top w^*(\hat c)-c^\top w^*(c)\ \ge 0 .$$

The linear optimization gap is $\omega_S(c)=\max_{w\in S}c^\top w-\min_{w\in S}c^\top w$, and for a set $\mathcal C$ of cost vectors $\omega_S(\mathcal C)=\sup_{c\in\mathcal C}\omega_S(c)$; the SPO loss of a cost in $\mathcal C$ lies in $[0,\omega_S(\mathcal C)]$.

Data are pairs $(x,c)$ drawn from a distribution $\mathcal D$ on $\mathcal X\times\mathcal C$. A hypothesis class $\mathcal H$ is a family of predictors $f:\mathcal X\to\mathbb R^d$. The SPO risk is $R_{\rm SPO}(f)=\mathbb E_{\mathcal D}[\ell_{\rm SPO}(f(x),c)]$, and on an i.i.d. sample $(x_1,c_1),\dots,(x_n,c_n)$ the empirical SPO risk is $\hat R_{\rm SPO}(f)=\frac1n\sum_i\ell_{\rm SPO}(f(x_i),c_i)$. The empirical Rademacher complexity with respect to the SPO loss is

$$\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)=\mathbb E_\sigma\Big[\sup_{f\in\mathcal H}\frac1n\sum_{i=1}^n\sigma_i\,\ell_{\rm SPO}(f(x_i),c_i)\Big]$$

with independent uniform signs $\sigma_i\in\{\pm1\}$, and $\mathfrak R^n_{\rm SPO}(\mathcal H)$ is its expectation over the sample.

The decisions induced by $\mathcal H$ form the class $w^*(\mathcal H)=\{x\mapsto w^*(f(x)):f\in\mathcal H\}$. A class $\mathcal F$ N-shatters a finite set $\mathbb X\subseteq\mathcal X$ if there are two labelings $g_1,g_2$ that differ at every point of $\mathbb X$ such that every mixture of them (follow $g_1$ on a subset $T$, $g_2$ on the rest) is realized by some member of $\mathcal F$. The Natarajan dimension $d_N(\mathcal F)$ is the largest size of an N-shattered set. When $S$ is a polyhedron, $\mathfrak S$ denotes its finite set of extreme points.

Formalization targets

Goal: Theorem 2, second display (p. 11)

For a polyhedral $S$ and every $\delta>0$, with probability at least $1-\delta$ over an i.i.d. sample of size $n$, every $f\in\mathcal H$ satisfies

$$R_{\rm SPO}(f)\le\hat R_{\rm SPO}(f)+2\,\omega_S(\mathcal C)\sqrt{\frac{2d_N(w^*(\mathcal H))\log(n|\mathfrak S|^2)}{n}}+\omega_S(\mathcal C)\sqrt{\frac{\log(1/\delta)}{2n}} .$$

Milestones, in attack order

1. Theorem 1 (p. 9): with probability $1-\delta$, $R_{\rm SPO}(f)\le\hat R_{\rm SPO}(f)+2\mathfrak R^n_{\rm SPO}(\mathcal H)+\omega_S(\mathcal C)\sqrt{\log(1/\delta)/(2n)}$ for all $f\in\mathcal H$.
2. Massart step (Appendix B.1, p. 31): for a fixed sample with costs in $\mathcal C$, $\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)\le\omega_S(\mathcal C)\sqrt{2\log|\mathfrak F_{|\mathbb X}|/n}$, where $\mathfrak F_{|\mathbb X}$ is the set of decision vectors $(w^*(f(x_1)),\dots,w^*(f(x_n)))$.
3. Natarajan lemma (cited on p. 31; proved on the platform as UnderstandingML.natarajan_lemma): a class from an $m$-point set to $k$ labels with Natarajan dimension $d$ has at most $m^d k^{2d}$ members.
4. Empirical bound (Appendix B.1, p. 31): for a fixed sample, $\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)\le\omega_S(\mathcal C)\sqrt{2d_N(w^*(\mathcal H))\log(n|\mathfrak S|^2)/n}$.
5. Theorem 2, first display (p. 11): the same bound for the expected complexity $\mathfrak R^n_{\rm SPO}(\mathcal H)$.

Significance

The bound controls the out-of-sample decision cost of every predictor in the class, not only of an empirical risk minimizer, so it applies to any training procedure (SPO+ surrogate minimization, decision trees, heuristics) that returns a member of $\mathcal H$. Its dependence on the feasible region is only through $\omega_S(\mathcal C)$ and $\log|\mathfrak S|$: the number of vertices of a combinatorial polytope is typically exponential in $d$, and enters only logarithmically. For linear predictors $x\mapsto Bx$ the paper's Corollary 2 bounds $d_N(w^*(\mathcal H_{\rm lin}))$ by $dp$, giving a rate of order $\sqrt{dp\log(n|\mathfrak S|)/n}$.

The results are proved in the paper; this mission formalizes them. No statement about predict-then-optimize or the SPO loss is known to have a machine-checked proof. The platform already has the Natarajan lemma (proved) and several Massart-type lemmas for generic classes; this mission connects that multiclass machinery to decision losses, and its Theorem 1 is a reusable Rademacher generalization bound for a loss with range $[0,\omega]$.

Difficulty

The obvious route through Lipschitz contraction fails: the SPO loss jumps when the prediction crosses a point where the optimum is not unique, so the Rademacher complexity of the composed class cannot be bounded by that of $\mathcal H$ times a Lipschitz constant. Any argument through the finitely many vertices of $S$ needs the decisions $w^*(f(x_i))$ to take finitely many values on a sample, i.e. the oracle to return vertices; for an oracle that returns a non-vertex optimal point under ties, $w^*(\mathcal H)$ may take infinitely many values on a sample. On the probabilistic side, the passage from the empirical to the expected complexity and the McDiarmid concentration step (Theorem 1) require the suprema over an uncountable class to be measurable, which the paper does not discuss.

Formalization scope

Lean works in $\mathbb R^d$ = EuclideanSpace ℝ (Fin d); cost vectors and decisions live in the same space and $c^\top w$ is the inner product. The standing assumptions of §2 are hypotheses of every theorem: $S$ nonempty, compact and convex; $w^*$ an arbitrary oracle (a hypothesis IsOracle S w, never a specific selection); $\mathcal C$ nonempty and bounded, with the cost component of $\mathcal D$ in $\mathcal C$ almost surely (or, for fixed-sample statements, every $c_i\in\mathcal C$); $n\ge1$. "Polyhedron" means the solution set of finitely many linear inequalities; with compactness it is a polytope, and $|\mathfrak S|$ is the cardinality of Set.extremePoints ℝ S. The expectation over signs is the exact average over the $2^n$ sign vectors; $R_{\rm SPO}$ and $\mathfrak R^n_{\rm SPO}$ are Bochner integrals. "With probability at least $1-\delta$" is stated as: the product measure of the set of samples on which some $f\in\mathcal H$ violates the bound is at most $\delta$.

The formalization commits to the following disclosed additions:

• In the empirical bound, Theorem 2 and its first display, the oracle returns extreme points of $S$. This is the proof's own "w.l.o.g." (p. 31), made explicit because p. 10 allows non-vertex outputs under ties. The hypothesis is needed: on the unit square, an oracle that returns distinct interior points of an edge under ties can have $d_N(w^*(\mathcal H))=1$ and empirical complexity near $\frac12$, which exceeds the printed bound for large $n$.
• The Natarajan dimension is not defined as a number (a supremum in $\mathbb N$ would silently be $0$ for unboundedly large shattered sets). Statements carry a natural number $k$ bounding the size of every N-shattered set, in place of $d_N(w^*(\mathcal H))$. This is equivalent when $d_N$ is finite; the printed bound is vacuous otherwise.
• Theorem 1 and the goal carry three measurability hypotheses: each loss function $z\mapsto\ell_{\rm SPO}(f(z_1),z_2)$ is measurable; the uniform deviation $\sup_f(R_{\rm SPO}(f)-\hat R_{\rm SPO}(f))$ and, for each sign vector, the signed supremum $\sup_f\frac1n\sum_i\sigma_i\ell_{\rm SPO}(f(x_i),c_i)$ are almost-everywhere measurable functions of the sample. Without them the integral defining $\mathfrak R^n_{\rm SPO}$ could default to $0$.
• The Massart step assumes $\mathfrak F_{|\mathbb X}$ finite, the case in which its printed right-hand side is finite.

A formalization that let $d_N$ be an sSup in $\mathbb N$, or chose a specific tie-breaking oracle inside the definitions, would prove a different and in part trivial statement; both are excluded.

Infrastructure needed: McDiarmid's bounded-differences inequality and symmetrization for the product measure; Massart's finite-class lemma (a proved version is on the platform as RademacherMassart.rad_le_massart, with its own normalization); the Natarajan lemma (proved, UnderstandingML.natarajan_lemma, stated with its own but identical notion of N-shattering over finite types); finiteness and nonemptiness of the extreme points of a nonempty polytope. Theorem 1 and the Massart step do not use polyhedrality and are reusable for any bounded decision loss. Contributions of these infrastructure lemmas are welcome.

Selected references

• O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, arXiv:1905.11488v3, 2022; Mathematics of Operations Research, 2023. https://arxiv.org/abs/1905.11488
• A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 9–26, 2022. https://arxiv.org/abs/1710.08005
• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian complexities: risk bounds and structural results, Journal of Machine Learning Research 3, 463–482, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
• B. K. Natarajan, On learning sets and functions, Machine Learning 4(1), 67–97, 1989. https://doi.org/10.1007/BF00114804
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014 (Lemma 29.4). https://doi.org/10.1017/CBO9781107298019
• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018 (Theorem 3.3, Corollary 3.8). https://cs.nyu.edu/~mohri/mlbook/