Convex Optimization

Motivation

Resource-constrained project scheduling asks for start times of the activities of a project that respect precedence-type time lags and the capacities of renewable resources (machines, crews, equipment). Classical project scheduling minimizes the project duration, a regular objective: delaying an activity never helps. Many objectives met in practice are not regular. The resource investment problem minimizes the cost of the resource capacities that must be procured; resource levelling problems minimize fluctuations of resource usage over time; the resource renting problem trades fixed procurement against time-dependent renting costs; net present value and earliness–tardiness objectives reward late as well as early starts. For such objectives the familiar fact that "some active schedule is optimal" fails, and algorithms need another finite set of candidate schedules that is guaranteed to contain an optimum.

Chapter 3 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2), organizes the objective functions of project scheduling into seven classes and pairs each class with a class of schedules that contains an optimal schedule. This mission formalizes §3.3 of that chapter. The classification goes back to Neumann, Nübel and Schwindt (2000) and Zimmermann (2001); the two locally defined classes, and the matching schedule classes of quasiactive and quasistable schedules, are the book's device for covering discontinuous resource-based objectives.

Setting

A project consists of activities $V=\{0,1,\dots,n+1\}$, $n\ge 1$, where $0$ and $n+1$ are fictitious activities marking the project beginning and completion. Activity $i$ has an integer duration $p_i$ ($p_0=p_{n+1}=0$, $p_i>0$ otherwise). The project network has an arc set $E$ with integer weights $\delta_{ij}$; a schedule is a vector $S=(S_0,\dots,S_{n+1})$ of real start times with $S_0=0$, $S\ge 0$, and it is time-feasible if $S_j-S_i\ge\delta_{ij}$ for all $\langle i,j\rangle\in E$. A maximum project duration $\bar d\in\mathbb N$ is prescribed through a backward arc $\langle n+1,0\rangle$ of weight $-\bar d$, so $S_{n+1}\le\bar d$. Each renewable resource $k$ has capacity $R_k$, activity $i$ uses $r_{ik}$ units while in progress, and $r_k(S,t)$ is the total usage at time $t$. The feasible region $\mathcal S$ consists of the time-feasible schedules with $r_k(S,t)\le R_k$ for all $k$ and $t$.

For an objective function $f:\mathbb R^{n+2}_{\ge 0}\to\mathbb R$, problem $PS|temp,\bar d|f$ asks for an optimal schedule: some $S\in\mathcal S$ with $f(S)\le f(S')$ for all $S'\in\mathcal S$.

A schedule induces the strict order $O(S)=\{(i,j)\mid i\ne j,\ S_j\ge S_i+p_i\}$ of precedences it realizes. The equal-order set of $S$ is

$$\mathcal S_T^{=}(O(S))=\{S'\text{ time-feasible}\mid S'_j\ge S'_i+p_i\ \forall (i,j)\in O(S),\ O(S')=O(S)\},$$

a polytope with part of its boundary removed. The distinct equal-order sets partition $\mathcal S$ into finitely many pieces.

Schedule classes are defined through shifts. A shift from a feasible $S$ to a feasible $S'\ne S$ is order-preserving if $O(S)\subseteq O(S')$; it is a left-shift if $S'\le S$. Two shifts from $S$ to $S'$ and $S''$ are opposite if $S''-S=\lambda(S'-S)$ with $\lambda<0$. A feasible schedule is active if no feasible left-shift exists, quasiactive if no order-preserving left-shift exists, stable if no pair of opposite shifts to feasible schedules exists, and quasistable if no pair of opposite order-preserving shifts exists.

Objective classes: $f$ is regular if $S\le S'$ implies $f(S)\le f(S')$; quasiconcave on a set $M$ if $f(\lambda S+(1-\lambda)S')\ge\min[f(S),f(S')]$ for $S,S'\in M$, $\lambda\in[0,1]$; lower semicontinuous if $f(S)\le\liminf_{S'\to S}f(S')$ on $\mathbb R^{n+2}_{\ge 0}$. Then $f$ is locally regular (class 6) if it is lower semicontinuous and regular on every equal-order set $\mathcal S_T^{=}(O(S))$, $S\in\mathcal S$, and locally quasiconcave (class 7) if it is lower semicontinuous and quasiconcave on every such set.

Formalization targets

Goal: Theorem 3.3.13

For every locally quasiconcave $f$,

$$\mathcal S\ne\emptyset\ \Longrightarrow\ \exists\,S\ \text{quasistable with}\ f(S)=\min_{S'\in\mathcal S}f(S').$$

Milestones

• Class 1 (§3.3.2): every regular $f$ has an active optimal schedule when $\mathcal S\ne\emptyset$.
• Class 5 (§3.3.6): every quasiconcave $f$ has a stable optimal schedule when $\mathcal S\ne\emptyset$.
• Eq. (3.3.11): the equal-order sets form a finite partition of $\mathcal S$.
• Propositions 3.3.5 and 3.3.6: the resource investment objective $\sum_k c_k\max_t r_k(S,t)$ with $c_k\ge 0$ is constant on each equal-order set and lower semicontinuous, hence locally regular.
• Theorem 3.3.9: every locally regular $f$ has a quasiactive optimal schedule when $\mathcal S\ne\emptyset$.

Significance

Quasiactive and quasistable schedules are finite in number: they are the minimal points and the vertices of the finitely many schedule polytopes. Theorem 3.3.13 therefore turns the minimization of any locally quasiconcave objective over a disconnected, non-convex feasible region into a finite search. Class 7 contains the resource levelling objectives $\sum c_k\sum r_{kt}^2$ and $\sum c_k\sum o_{kt}$, the total variation of the resource profiles, and the resource renting objective (Propositions 3.3.10 and 3.3.12, and Nübel 2001). The enumeration schemes and decision sets of §3.5–3.7 rest on this result, and Theorem 3.3.9 plays the same role for class 6 (resource investment, changeover times).

The results are proved in the book and the cited papers. As far as a search of the platform shows, none of them, and none of the schedule classes, has a machine-checked formalization; Mathlib supplies lower semicontinuity and quasiconcavity but nothing about schedules. The mission produces a checked version of the classification theorems in the book's exact generality: general time lags (cycles in the network allowed), real start times, and arbitrary objectives given only by their class.

Difficulty

The optimum need not exist a priori: objectives of classes 6 and 7 are discontinuous, and the feasible region is a finite union of polytopes that is in general disconnected. Existence of a minimizer needs compactness of $\mathcal S$ (which depends on the deadline arc and the network's path structure) together with lower semicontinuity.

The main obstacle is that the objective is only controlled piecewise. Quasiconcavity holds on each equal-order set separately, and an equal-order set is not closed: a schedule polytope $\mathcal S_T(O(S))$ also contains schedules inducing strictly larger orders, where the hypothesis on $f$ says nothing about its relation to the values on $\mathcal S_T^{=}(O(S))$. The obvious argument, taking an optimal schedule and invoking quasiconcavity along the segment of a pair of opposite order-preserving shifts, only relates $f$ at points of one equal-order set, and it does not by itself produce a schedule that admits no such pair at all. The same issue arises for Theorem 3.3.9 with order-preserving left-shifts, which may cross from one equal-order set into another.

Formalization scope

Activities are Fin (n + 2), with 0 and Fin.last (n + 1) fictitious. Start times are real; objective functions are total functions (Fin (n + 2) → ℝ) → ℝ whose regularity, quasiconcavity and lower semicontinuity are required only on the nonnegative orthant (lower semicontinuity is Mathlib's LowerSemicontinuousOn on the orthant). The deadline $S_{n+1}\le\bar d$ is the network's backward arc, as in §3.1. The project structure records the book's standing property (p. 8) that from each node $i$ there is a path to $n+1$ of length at least $p_i$; this bounds every activity by $\bar d$. The resource constraints are imposed for all $t\ge 0$, which under that property is the book's $0\le t\le\bar d$. The peak $\max_t r_k(S,t)$ in the resource investment objective is a supremum in $\mathbb N$ over $t\ge 0$ of a nonempty finite set, hence attained.

"Optimal" always means minimizing $f$ over the whole feasible region $\mathcal S$, and the theorems quantify over every function in the class; a formalization with a fixed objective, or with optimality over a single polytope or a single equal-order set, would be a different and weaker statement. The schedule classes are defined through shifts, never as minimal or extreme points, so no statement is true by definition. The only hypothesis besides the class of $f$ is $\mathcal S\ne\emptyset$.

The mission restates locally the project model, the induced orders and the shift classes also drafted by the companion missions on schedule classes of this series. Useful contributions beyond the milestones: compactness of $\mathcal S$ and closedness of the schedule polytopes, the representation of $\mathcal S$ as a finite union of feasible order polytopes, and the finiteness of the sets of quasiactive and quasistable schedules.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §3.3. doi:10.1007/978-3-540-24800-2
• K. Neumann, H. Nübel, C. Schwindt, Active and stable project scheduling, Mathematical Methods of Operations Research 52 (2000), cited in the book as Neumann et al. (2000).
• J. Zimmermann, Ablauforientiertes Projektmanagement: Modelle, Verfahren und Anwendungen, Gabler, 2001.

Motivation

In bandit convex optimization a forecaster repeatedly picks a point $x_t$ of a convex set $\mathcal K\subseteq\mathbb R^d$, and an adversary picks a convex loss $\ell_t$. The forecaster pays $\ell_t(x_t)$ and observes only that number: it never sees the function, its gradient, or its value elsewhere. This is the model of online optimization with only function-value access, as in tuning a system online from measured costs, dynamic pricing with an unknown convex demand-cost curve, or routing with path costs observed only on the route taken. The question is how fast the forecaster can approach the best fixed point in hindsight.

Chapter 6 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2, Foundations and Trends in Machine Learning 5(1), 2012) treats the problem through spherical gradient estimates fed to projected gradient descent. The one-point method is due to Flaxman, Kalai and McMahan (SODA 2005, arXiv:cs/0408007), who obtained an $\mathcal O(n^{3/4})$ regret bound. Agarwal, Dekel and Xiao (COLT 2010) showed that two function evaluations per round allow $\mathcal O(\sqrt n)$. Whether one-point feedback admits $\sqrt n$ regret was open when the monograph was written (p. 94); Bubeck, Eldan and Lee (STOC 2017, arXiv:1607.03084) later obtained $\sqrt n$ regret up to logarithmic and polynomial-in-$d$ factors for convex losses, with a different and much more involved algorithm.

Setting

Let $\mathbb B=\{x\in\mathbb R^d:\|x\|\le1\}$ be the closed Euclidean unit ball and $\mathbb S=\{x:\|x\|=1\}$ the unit sphere, with unnormalized spherical measure $\sigma$, so that $\sigma(\mathbb S)=d\,\mathrm{Vol}(\mathbb B)$. Fix $\delta>0$. For a loss $\ell$, the smoothed loss is $\widetilde\ell(x)=\mathbb E\,\ell(x+\delta B)$ with $B$ uniform on $\mathbb B$.

The set $\mathcal K$ is closed and convex with $r\mathbb B\subseteq\mathcal K\subseteq R\mathbb B$. The losses $\ell_1,\ell_2,\dots:\mathbb R^d\to\mathbb R$ are $G$-Lipschitz, differentiable and convex, and are fixed before the game (an oblivious adversary).

OSGD (Online Stochastic Gradient Descent) on a set $\mathcal K'$ with learning rate $\eta$ starts at $x_1=0$ and sets $x_{t+1}=\operatorname{argmin}_{y\in\mathcal K'}\|y-(x_t-\eta\widetilde g_t(x_t))\|$, where $\widetilde g_t$ is a gradient estimate. With $S_1,S_2,\dots$ independent and uniform on $\mathbb S$:

• the two-point estimate (6.1) is $\widetilde g_t(x_t)=\frac d{2\delta}\big(\ell_t(X_t^+)-\ell_t(X_t^-)\big)S_t$ with $X_t^\pm=x_t\pm\delta S_t$; the played point is $X_t^+$ or $X_t^-$ by a fair coin;
• the one-point estimate (6.3) is $\widetilde g_t(x_t)=\frac d\delta\,\ell_t(\widetilde X_t)S_t$ with played point $\widetilde X_t=x_t+\delta S_t$.

OSGD runs on the shrunken set $\mathcal K'=(1-\delta/r)\mathcal K$, so that the perturbed points stay in $\mathcal K$. The pseudo-regret is

$$\overline R_n=\mathbb E\sum_{t=1}^n\ell_t(\widetilde X_t)-\min_{x\in\mathcal K}\sum_{t=1}^n\ell_t(x).$$

Formalization targets

Goal: Theorem 6.2, tuned

If in addition $|\ell_t|\le L$ on $\mathcal K$, and $\delta=(2n)^{-1/4}\sqrt{RdL/((3+R/r)G)}$, $\eta=(2n)^{-3/4}\sqrt{R^3/(dL(3+R/r)G)}$, then one-point OSGD satisfies

$$\overline R_n\le 4n^{3/4}\sqrt{RdL\,(3+R/r)\,G}.$$

Milestones

1. Lemma 6.1: $\nabla\int_{\mathbb B}\ell(x+\delta b)\,db=\frac1\delta\int_{\mathbb S}\ell(x+\delta s)s\,d\sigma(s)$.
2. Lemma 6.2: $\frac d\delta\mathbb E[\ell(x+\delta S)S]=\nabla\mathbb E\,\ell(x+\delta B)$.
3. Eq. (6.2): $|\ell(x)-\widetilde\ell(x)|\le\delta G$.
4. Lemma 6.3: the queried points' regret against $x$ is at most the smoothed regret of the iterates against $(1-\xi)x$, plus $3\delta Gn+\xi GRn$.
5. Theorem 6.1: two-point OSGD has $\overline R_n\le R^2/\eta+\eta(Gd)^2n+\delta(3+R/r)Gn$, and $\overline R_n\le 2RGd\sqrt n+\delta(3+R/r)Gn$ for $\eta=R/(Gd\sqrt n)$.
6. Theorem 6.2, first display: one-point OSGD has $\overline R_n\le R^2/\eta+\frac{(dL)^2}{\delta^2}\eta n+\delta(3+R/r)Gn$ for every $0<\delta\le r$ and $\eta>0$.

Significance

The $n^{3/4}$ bound shows that a single function value per round suffices for sublinear regret against any oblivious sequence of Lipschitz convex losses, with a forecaster whose only operations are a random perturbation and a Euclidean projection. The smoothing identity of Lemmas 6.1–6.2 is the basic tool of zeroth-order (derivative-free) optimization, used well beyond bandits, and Theorem 6.1 is the $\sqrt n$ benchmark for two-point methods.

All results are proved in the source. To the best of current knowledge none is formalized: the related items of the Introduction to Online Convex Optimization series on Prove2Me (Hazan's Lemma 6.7 and Theorem 6.9) were formalized with missing hypotheses and are recorded as disproved. This mission produces machine-checked statements with every hypothesis explicit, and the formal infrastructure (sphere measure calculus, a projected stochastic gradient analysis) for later zeroth-order results.

Difficulty

Two steps resist a direct formal treatment. First, Lemma 6.1 is a divergence-theorem identity on the ball; Mathlib has the sphere measure and polar coordinates, but its divergence theorem covers boxes rather than balls, so differentiating the ball average in $x$ requires either such a theorem or a direct argument about translates of the ball. Second, the regret analysis takes expectations of quantities that depend on the whole past: the iterate $x_t$ is a function of $S_1,\dots,S_{t-1}$, and unbiasedness $\mathbb E[\widetilde g_t\mid x_t]=\nabla\widetilde\ell_t(x_t)$ holds only conditionally, via independence of $S_t$ from the past. A pathwise gradient-descent inequality must be combined with this conditional expectation round by round, with measurability of the projected iterates established along the way. The naive approach of treating the estimate as the true gradient of $\ell_t$ fails: it is a gradient of $\widetilde\ell_t$, and the gap is handled only by Eq. (6.2) and Lemma 6.3.

Formalization scope

Points are in EuclideanSpace ℝ (Fin d) with $d\ge1$; rounds are $t=1,2,\dots$, sums run over Finset.Icc 1 n. $\sigma$ is Mathlib's Measure.toSphere of Lebesgue measure; the uniform laws are normalized restrictions. Randomness lives on an arbitrary probability space; the directions $S_t$ are measurable, mutually independent (iIndepFun) and uniform on $\mathbb S$, and in Theorem 6.1 the pairs $(S_t,C_t)$ are independent with $C_t$ a fair sign independent of $S_t$. A run of OSGD is a predicate (start at $0$, each iterate a Euclidean projection onto $(1-\delta/r)\mathcal K$), which determines the run uniquely, so the forecaster uses only observed values and its own randomness. The losses are Lipschitz, differentiable and convex on all of $\mathbb R^d$; the bound $|\ell_t|\le L$ is on $\mathcal K$, because a convex function bounded on $\mathbb R^d$ is constant. The minimum over $\mathcal K$ is an infimum over the subtype $\mathcal K$, attained in every theorem.

Conventions and corrections, each stated in the item's Formalization Note:

• Lemma 6.1 carries the factor $1/\delta$ that the printed statement omits and the proof contains (corrected misprint).
• Theorem 6.1's second display prints $\eta=R/(GD\sqrt n)$ and a limit "for $\delta\to0$"; the item states $\overline R_n\le 2RGd\sqrt n+\delta(3+R/r)Gn$ for $\eta=R/(Gd\sqrt n)$ and every admissible $\delta$, which implies the limit (corrected misprint).
• Theorems 6.1 and 6.2 add $0<\delta\le r$, which the proofs need for $X_t^\pm,\widetilde X_t\in\mathcal K$; for the tuned $\delta$ of the goal it is a condition on $n$.
• The goal adds $G,L>0$ and $n\ge1$, which its formulas for $\delta,\eta$ need; the constant $4$ is the book's rounding of $2\cdot2^{3/4}$ and is kept, as is the form $R^2/\eta$.

The statements cannot be satisfied trivially: the run is pinned by its recursion, the losses are fixed before the randomness, the expectations are of bounded measurable functions (no zero-valued Bochner integrals), and the minimum is over the nonempty compact $\mathcal K$. Section 6.3 (Lemma 6.4, Theorem 6.3) is not included, because its algorithm box and proof use different stage lengths and its unimodality condition is stated on a smaller set than the proof uses.

Needed infrastructure: calculus of ball averages and sphere integrals, symmetry of the uniform sphere law, nonexpansiveness of projections onto closed convex sets, and conditional-expectation bookkeeping for adapted iterates. Each is reusable for zeroth-order optimization; contributions of any of them as separate lemmas are welcome.

Selected references

• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721v2, doi:10.1561/2200000024
• A. Flaxman, A. Kalai, H. B. McMahan, Online convex optimization in the bandit setting: gradient descent without a gradient, SODA 2005. arXiv:cs/0408007
• A. Agarwal, O. Dekel, L. Xiao, Optimal algorithms for online convex optimization with multi-point bandit feedback, COLT 2010. link
• S. Bubeck, R. Eldan, Y. T. Lee, Kernel-based methods for bandit convex optimization, STOC 2017. arXiv:1607.03084

Motivation

Learning from a finite sample is useful only if changing the sample has a controlled effect on the learned predictor. Uniform stability asks for a bound on the change in loss at every test point when one training example is removed. Bousquet and Elisseeff use this property to obtain generalization bounds for learning algorithms, and identify regularization as a source of stability in methods built from reproducing kernels. The present mission isolates their result for a squared norm penalty in a reproducing kernel Hilbert space (RKHS). It concerns the sensitivity of the optimizer itself, before any probability bound on a random training sample is applied. The result is Theorem 22 of Bousquet and Elisseeff (2002).

Setting

Let $X$ be an input space, $Y$ a label space, and $H$ a real reproducing kernel Hilbert space of real-valued predictors on $X$. A kernel $K:X\times X\to\mathbb R$ and a feature representative $\Phi(x)\in H$ express the reproducing identity $f(x)=\langle f,\Phi(x)\rangle_H$ and $K(x,x')=\langle\Phi(x),\Phi(x')\rangle_H$. Thus $K(x,x)=\|\Phi(x)\|_H^2$. The source assumes that all diagonal kernel values satisfy $K(x,x)\le\kappa^2$.

A labeled example is $z=(x,y)\in X\times Y$. Its loss under $f$ is $\ell(f,z)=c(f(x),y)$, where $c$ is a real-valued cost. Let $D_H$ be the set of predictions that some element of $H$ can produce at some input. The loss is $\sigma$-admissible when $c(\cdot,y)$ is convex for every label $y$ and $|c(a,y)-c(b,y)|\le\sigma|a-b|$ for all $a,b\in D_H$ and $y\in Y$. Here $\sigma$ is a nonnegative Lipschitz constant. The definition compares any two attainable predictions, even when they arise at different inputs.

Fix a sample $S=(z_1,\ldots,z_m)$, a deleted index $i$, and a regularization weight $\lambda>0$. The paper's full and truncated objectives, with squared RKHS norm regularization, are

$$R_r(g)=\frac1m\sum_{j=1}^{m}\ell(g,z_j)+\lambda\|g\|_H^2, \qquad R_r^{\setminus i}(g)=\frac1m\sum_{j\ne i}\ell(g,z_j)+\lambda\|g\|_H^2.$$

The factor in both objectives is $1/m$. Let $f$ and $f^{\setminus i}$ be minimizers of these respective objectives over all of $H$. The statements allow any minimizer satisfying the relevant global optimality condition; they do not choose one by an arbitrary fallback rule.

Formalization targets

The central target is the explicit deletion stability estimate of Theorem 22. For every test point $z\in X\times Y$,

$$|\ell(f,z)-\ell(f^{\setminus i},z)| \le \frac{\sigma^2\kappa^2}{2\lambda m}.$$

Its four milestones follow the paper's route through Lemma 20, the point-evaluation inequality (25), and the two quantitative inequalities displayed in the proof of Theorem 22. In particular, the intermediate RKHS distance bound is $\|f^{\setminus i}-f\|_H\le\kappa\sigma/(2\lambda m)$ when $\kappa\ge0$. The main theorem uses $\kappa^2$, so it does not need a choice of sign for $\kappa$. These numerical constants are part of the target, rather than placeholders for unspecified bounds.

Significance

The theorem supplies a deterministic, uniform sensitivity estimate for kernel methods trained by squared norm regularization. The bound applies simultaneously to every test example and decreases as either the sample size or the regularization weight increases. It is one of the ingredients that lets the paper apply its earlier stability-to-generalization results to concrete learning procedures. The loss need not be bounded for this theorem; bounding it is a separate question addressed later in the paper.

The result is proved in the source article. This mission asks for a machine-checked version of its exact pairwise claim and the reusable infrastructure around it: the paper's admissibility condition, the two objectives, the general regularizer inequality, and the RKHS evaluation bound. The existing Prove2Me library already has definitions for loss, empirical error, and the RKHS reproducing identity, so the new definitions concentrate on what is specific to these pages. The related replace-one estimate in Mohri, Rostamizadeh and Talwalkar's Foundations of Machine Learning uses a different perturbation and constant; it is not interchangeable with this result.

Difficulty

The two minimizers solve different objectives, and the deleted example appears in only one of them. A comparison of their objective values alone does not directly give a bound on their distance in the Hilbert norm. The source also distinguishes an abstract convex class of functions in Lemma 20 from the full RKHS used in Theorem 22. A proof must keep those domains straight while preserving the precise normalization of the truncated objective. Another delicate point is that the kernel bound controls evaluations through the reproducing identity; a bound on $K(x,x)$ is not by itself a bound on loss unless the admissibility condition is also used.

Formalization scope

The Lean model uses an abstract complete real inner product space $H$, an evaluation map $\operatorname{ev}:H\to(X\to\mathbb R)$, a feature map $\Phi:X\to H$, and the published IsRKHSOf predicate tying these to $K$. The completeness instance matches the source's Hilbert-space assumption. Samples have type Fin m → X × Y, so an index i : Fin m already forces $m\ge1$. Minimization ranges over the entire $H$ for Theorem 22 and over the declared convex class for Lemma 20. The objective definitions use the published Loss and EmpiricalError objects. No probability measure or measurability assumption is needed for these deterministic assertions.

There is a printed mismatch that affects what “deletion” means. Theorem 22 names an algorithm defined by equation (26), which, run afresh on $m-1$ points, would normalize its data term by $1/(m-1)$. Lemma 20 and the proof of Theorem 22 instead compare the full objective with equation (20), whose data term uses $1/m$. The formalized goal states that comparison, with its explicit constant, and records the discrepancy for audit. This excludes the tempting shortcut of treating the two normalizations as identical. The regularizer is the genuine squared norm and the second minimizer is required to minimize the genuine truncated objective; neither a restricted hypothesis ball nor an artificially assumed distance bound enters the goal. Contributions that establish minimizer existence or connect the pairwise bound to an algorithmic selection would extend this core without changing its statement.

Selected references

• Olivier Bousquet and André Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002), 499–526. Article and PDF.
• Mehryar Mohri, Afshin Rostamizadeh, and Ameet Talwalkar, Foundations of Machine Learning, second edition, MIT Press, 2018, Chapter 14. Book information.

Motivation

Online decision makers often have to choose an action before seeing the cost assigned to it. A no-regret algorithm performs almost as well, in total, as the best single action that could have been chosen after the costs were known. In a related repeated-game problem, Blackwell approachability asks a player to keep the average of vector payoffs close to a desired set despite an adversary's choices. These two performance criteria look different: one compares scalar costs to a fixed benchmark, while the other measures a geometric distance. Abernethy, Bartlett, and Hazan establish algorithmic reductions between them, with explicit finite-horizon bounds in their COLT 2011 paper. This mission isolates the direction that turns an approachability algorithm into an online linear optimization algorithm.

The bound matters even when the input algorithm has no known rate. It relates the regret of the resulting online algorithm to the actual distance attained on the corresponding sequence. Any subsequent guarantee on that distance then yields a regret guarantee through the same reduction. The paper also gives the reverse reduction and an application to calibrated forecasting; those are separate missions in this series.

Setting

Fix a dimension $d$ and a nonempty compact convex decision set $K\subseteq\mathbb R^d$. On round $t$, an algorithm selects $x_t\in K$ using only the preceding cost vectors $f_1,\ldots,f_{t-1}$. The adversary then reveals $f_t$ in the Euclidean unit ball $B_2(1)$. The incurred linear cost is $\langle f_t,x_t\rangle$. For a horizon $T$, regret compares these costs with the cost of the best single point of $K$ evaluated on all $T$ rounds:

$$\operatorname{Regret}_T = \sum_{t=1}^T\langle f_t,x_t\rangle - \min_{x\in K}\sum_{t=1}^T\langle f_t,x\rangle.$$

The minimum exists because $K$ is nonempty and compact. No probabilistic model for the cost sequence is assumed. The round index begins at one, and $x_t$ cannot depend on $f_t$.

The reduction uses $\kappa=\max_{x\in K}\|x\|$, the maximum norm of a decision. Write $a\oplus x$ for Euclidean concatenation of a scalar and a vector, an element of $\mathbb R^{d+1}$. The generated cone of a set $M$ consists of its nonnegative scalar multiples, $\operatorname{cone}(M)=\{\alpha m:\alpha\ge0,\ m\in M\}$. For a set $C$, its polar cone is $C^0=\{\theta:\langle\theta,z\rangle\le0\text{ for every }z\in C\}$. This negative-sign convention is fixed throughout the mission.

Algorithm 1 of the paper constructs a vector-payoff game. Its player actions are $K$, its adversary actions are $B_2(1)$, its payoff and target are

$$u(x,f)=\bigl(\langle f,x\rangle/\kappa\bigr)\oplus(-f), \qquad S=\operatorname{cone}(\{\kappa\}\times K)^0.$$

A Blackwell approachability algorithm for this game chooses each $x_t$ from the preceding adversary moves. Its finite-horizon approachability rate on a given sequence is $D_T(A)=\operatorname{dist}(T^{-1}\sum_{t=1}^T u(x_t,f_t),S)$, where distance means the Euclidean distance from a point to a set. The online algorithm created by Algorithm 1 uses precisely the same choices $x_t$.

Formalization targets

The goal is Theorem 16 of the paper. For every admissible history-based algorithm, every sequence of unit-ball costs, and every $T\ge1$, it asserts

$$\frac{\operatorname{Regret}_T}{T}\le 2\kappa D_T(A).$$

This is a statement about the rate actually obtained on the chosen cost sequence. It assumes no upper bound on $D_T(A)$ and does not require an oracle call in the statement. Thus it also covers algorithms whose behavior is specified directly rather than through an implementation of the oracle.

The milestone targets are the distance formula of Lemma 13, the conic distance identity in display (8) of Theorem 16's proof, and the existence of a valid halfspace oracle in Lemma 15. Lemma 13 says distance to a nonempty convex cone equals the attained maximum of a linear functional over the polar cone's unit ball. Display (8) specializes this geometry to Algorithm 1's lifted target. Lemma 15 says that every halfspace containing that target admits a player action whose payoff remains in the halfspace against every permitted adversary move. Together these statements specify the geometry and the oracle needed by the reduction.

Significance

Theorem 16 gives a numerical transfer rule: a bound on approachability distance for Algorithm 1's game immediately bounds average regret for the same sequence. Its factor depends only on the size $\kappa$ of the decision set. This permits comparison of algorithms in a common finite-horizon language, without replacing the online cost sequence by a distribution or an asymptotic limit. The source paper uses this direction as one half of its equivalence between approachability and no-regret learning Abernethy, Bartlett, and Hazan, 2011.

The mathematical results are established in that paper; the goal here is a machine-checked Lean development of their statements and eventually their proofs. The mission also supplies reusable definitions of generated and polar cones, a Euclidean lift, a finite-history online algorithm, and regret over a compact decision set. Lemma 13 is useful outside this reduction whenever distance to a cone is compared with linear functionals on its polar. The proposed theorem items currently carry open proofs, while their statements and definition files are checked for elaboration in the pinned Lean environment.

Difficulty

The main obstacle is the change of viewpoint from a scalar regret comparison to distance from a set of lifted vector payoffs. A direct comparison of individual round costs does not describe that distance. The target is a polar cone in one additional Euclidean dimension, so a faithful account must keep the lift's geometry, the cone's sign convention, and the normalization by $\kappa$ aligned. The distance formula also asserts that its maximum is attained. An encoding that merely writes an infimum or supremum with default values can silently make an edge case look valid without representing the paper's claim.

The oracle milestone has a separate quantifier demand. One selected action must work against every adversary move for each halfspace containing the target. It cannot be replaced by a possibly different action for each move, or by a claim only about tangent halfspaces. The theorem includes halfspaces with arbitrary offsets and zero normals because the source oracle accepts any containing halfspace.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin d), and $a\oplus x$ lives in EuclideanSpace ℝ (Fin (d+1)) with the Euclidean norm. The generated cone uses exactly one nonnegative multiple of a point of the generating set, as in Definition 11. The polar uses $\langle\theta,z\rangle\le0$, the opposite sign from a positive dual-cone convention. Distances are Euclidean point-to-set distances. All arithmetic is over exact real numbers, and the regret minimum ranges over the image of the nonempty compact set $K$.

The statements require $\kappa>0$ because the source payoff divides by $\kappa$. This excludes the degenerate case $K=\{0\}$, in which the source instance is undefined. They require $T\ge1$ wherever an average is formed. Admissible histories consist of unit-ball adversary moves, and each round's decision belongs to $K$. The dimension may be zero syntactically, but the positive-$\kappa$ hypothesis excludes that case in results using Algorithm 1. These conditions keep the bound from being satisfied through Lean's default values for division by zero, distance to an empty set, or infima over empty sets.

The paper's display (8) writes $\operatorname{cone}(\kappa\oplus K)$ and labels its unit ball with dimension $d$; the formalization uses the cone of $\{\kappa\}\times K$ in $\mathbb R^{d+1}$, matching Algorithm 1. Lemma 12's printed bipolar claim omits closedness; this mission does not use that uncorrected sentence as a milestone. The oracle statement covers all containing halfspaces. Contributions are welcome for the distance identity, the oracle existence result, and the final regret inequality, as well as geometric lemmas supporting those proofs.

Selected references

• Jacob Abernethy, Peter L. Bartlett, and Elad Hazan, Blackwell Approachability and No-Regret Learning are Equivalent, Proceedings of the 24th Annual Conference on Learning Theory, JMLR Workshop and Conference Proceedings 19, 2011, pp. 27–46. Published paper.

Motivation

The smallest enclosing ball problem asks, for finitely many points $p_1,\dots,p_n\in\mathbb{R}^d$, for a ball of the smallest radius that contains all of them. It appears in clustering, in collision detection and bounding-volume hierarchies, in facility location (placing one service point so that the farthest client is as close as possible), and in the analysis of geometric algorithms. Sylvester posed the planar version in 1857; Megiddo (1983) gave a linear-time algorithm in fixed dimension, and Welzl (1991) a simple randomized one.

This mission formalizes Section 8.7 of Matoušek and Gärtner, Understanding and Using Linear Programming (Springer, 2007), which uses the problem to introduce convex programming. Unlike the geometric problems of the book's Chapter 2, the smallest ball cannot be written as a linear program. The section shows instead that it is a convex quadratic program, derives the Karush–Kuhn–Tucker (KKT) conditions for convex programs in equational form from the duality theorem of linear programming, and uses them to prove that the smallest enclosing ball exists and is unique. It is the book's bridge from linear to convex optimization.

Setting

A function $f:\mathbb{R}^n\to\mathbb{R}$ is convex if $f((1-t)x+ty)\le(1-t)f(x)+tf(y)$ for all $x,y\in\mathbb{R}^n$ and $t\in[0,1]$. A convex program in equational form is

$$\text{minimize } f(x)\quad\text{subject to } Ax=b,\ x\ge 0,$$

with $A$ a real $m\times n$ matrix with columns $a_1,\dots,a_n$, $b\in\mathbb{R}^m$ and $f$ convex. A vector $x$ is feasible if $Ax=b$ and $x\ge 0$ componentwise, and optimal if it is feasible and $f(x)\le f(x')$ for every feasible $x'$. For differentiable $f$, $\nabla f(x)$ is the row vector of partial derivatives, so $\nabla f(x^*)(x-x^*)$ is a scalar.

For points $p_1,\dots,p_n\in\mathbb{R}^d$, write $P=\{p_1,\dots,p_n\}$ and let $Q$ be the $d\times n$ matrix whose $j$th column is $p_j$. The program studied is

$$\text{(8.15)}\qquad \text{minimize } f(x)=x^TQ^TQx-\sum_{j=1}^n x_j\,p_j^Tp_j\quad\text{subject to } \sum_{j=1}^n x_j=1,\ x\ge 0 .$$

A ball is a closed Euclidean ball $B(c,r)=\{z\in\mathbb{R}^d:\|z-c\|\le r\}$. The ball $B(c,r)$ is the unique smallest enclosing ball of a set $S$ if $r\ge 0$, $S\subseteq B(c,r)$, every ball containing $S$ has radius at least $r$, and every ball containing $S$ of radius at most $r$ has center $c$.

Formalization targets

Goal: Theorem 8.7.4

For $n\ge 1$ points $p_1,\dots,p_n\in\mathbb{R}^d$, the objective $f$ of (8.15) is convex, and

1. (8.15) has an optimal solution $x^*$;
2. there is a point $p^*$ with $p^*=Qx^*$ for every optimal $x^*$, and for every optimal $x^*$

$$-f(x^*)\ge 0\quad\text{and}\quad B\big(p^*,\sqrt{-f(x^*)}\big)\ \text{is the unique smallest enclosing ball of } P .$$

Milestones

• Fact 8.7.1. For $C\subseteq\mathbb{R}^n$ convex, $f$ differentiable and convex, and $x^*\in C$: $x^*$ minimizes $f$ over $C$ iff $\nabla f(x^*)(x-x^*)\ge 0$ for all $x\in C$.
• Proposition 8.7.2 (KKT conditions). For $f$ convex with continuous partial derivatives and $x^*$ feasible: $x^*$ is optimal iff there is $\tilde y\in\mathbb{R}^m$ with

$$\nabla f(x^*)_j+\tilde y^Ta_j\ \begin{cases}=0&\text{if } x^*_j>0,\\ \ge 0&\text{otherwise,}\end{cases}\qquad j=1,\dots,n.$$

• Lemma 8.7.3. If $s_1,\dots,s_k$ lie on the boundary of the ball $B$ with center $s^*$, then $B$ is the unique smallest enclosing ball of $\{s_1,\dots,s_k\}$ iff for every $u\in\mathbb{R}^d$ some $j$ has $u^T(s_j-s^*)\le 0$.

Significance

The result. Theorem 8.7.4 gives existence and uniqueness of the smallest enclosing ball together with an explicit certificate: the center is a convex combination $Qx^*$ of the input points, the squared radius is the negated optimum value, and the points $p_j$ with $x^*_j>0$ lie on the boundary. It reduces the geometric problem to a convex quadratic program, for which interior-point and simplex-type solvers exist, and it is the basis of the combinatorial characterization "the center lies in the convex hull of the boundary points" used by Welzl-type algorithms. Proposition 8.7.2 is the KKT theorem for equational-form convex programs; it holds without any constraint qualification because the constraints are linear.

Formalizing it. All results here are classical and proved in the book; none is open. The mission produces machine-checked statements and, when solved, proofs of: the first-order optimality criterion for convex functions on convex sets in $\mathbb{R}^n$; the equational-form KKT theorem derived from LP duality; the boundary characterization of unique smallest enclosing balls; and existence and uniqueness of the smallest enclosing ball in every dimension. Mathlib has first-order necessary conditions at local minima and general convexity theory, but no KKT theorem for linearly constrained convex programs in this form and no smallest-enclosing-ball theory.

Difficulty

Existence of an optimum and convexity of $f$ are routine. For the KKT conditions, the necessary direction needs multipliers, which do not come from calculus alone: the obvious Lagrange-multiplier argument handles only equality constraints and says nothing about the sign pattern forced by $x\ge 0$. For the goal, a solver must connect three layers — the gradient of a quadratic form in matrix notation, the multiplier conditions, and the Euclidean geometry of distances to $p^*$ — and uniqueness of the ball does not follow from uniqueness of the optimizer $x^*$, which in general is not unique (repeated or cospherical points). The statement quantifies over all optimal $x^*$ and asserts that they all yield the same center.

Formalization scope

• Vectors of $\mathbb{R}^n$ are Fin n → ℝ, so the book's indices $1,\dots,n$ become $0,\dots,n-1$. Points of $\mathbb{R}^d$ are EuclideanSpace ℝ (Fin d), so $\|\cdot\|$ and $p^Tq$ are Euclidean. The matrix $Q$ is Matrix (Fin d) (Fin n) ℝ.
• Optimality is stated against every feasible point; no infimum or supremum is taken. $\nabla f(x^*)(x-x^*)$ is the Fréchet derivative applied to $x-x^*$, and $\nabla f(x^*)_j$ its value on the $j$th unit vector. "Continuous partial derivatives" is ContDiff ℝ 1 f. Convexity is ConvexOn ℝ Set.univ f.
• Balls are closed. The squared radius $-f(x^*)$ is expressed by asserting $-f(x^*)\ge 0$ and taking the radius $\sqrt{-f(x^*)}$. "Unique ball of smallest radius" is written out as minimality of the radius among all enclosing closed balls plus equality of centers for every enclosing ball of radius at most the optimum; merely stating that the ball encloses $P$ would not be the theorem.
• The goal assumes $n\ge 1$ (for $n=0$ the feasible set is empty). In Fact 8.7.1 the minimizer $x^*$ is assumed to lie in $C$, as "minimizes $f$ over $C$" presupposes. In Lemma 8.7.3 the radius is nonnegative and each $s_j$ is at distance exactly $r$ from $s^*$.
• Needed infrastructure: gradients of quadratic forms on Fin n → ℝ, LP duality for the pair (maximize $c^Tx$, $Ax=b$, $x\ge0$) / (minimize $b^Ty$, $A^Ty\ge c$), compactness of the standard simplex, and elementary Euclidean geometry. The first-order criterion and the KKT theorem are reusable beyond this mission; proofs through any route are welcome.

Selected references

• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.7, pp. 184–191. https://doi.org/10.1007/978-3-540-30717-4
• S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441
• N. Megiddo, Linear-time algorithms for linear programming in $\mathbb{R}^3$ and related problems, SIAM J. Comput. 12(4), 1983. https://doi.org/10.1137/0212052
• E. Welzl, Smallest enclosing disks (balls and ellipsoids), in New Results and New Trends in Computer Science, LNCS 555, Springer, 1991. https://doi.org/10.1007/BFb0038202
• J. J. Sylvester, A question in the geometry of situation, Quarterly Journal of Pure and Applied Mathematics 1, 1857.

Motivation

Many stochastic and nondifferentiable optimization problems are not solved by minimizing their true objective $f^0$ directly: $f^0$ may be nonsmooth, an expectation that cannot be evaluated, or only approximately known. A standard remedy replaces $f^0$ by a sequence of "good" approximations $F^0(\cdot, s)$ (smoothed versions, sample averages, perturbations) that converge to $f^0$, and runs one step of a descent method on the current approximation at every iteration. Approximation and optimization then proceed simultaneously. More generally, in nonstationary optimization the objective $F^0(\cdot, s)$ and the feasible set $X_s$ change with the iteration number $s$, and the iterates $x^s$ are required to follow the time path of the optimal solutions,

$$\lim_{s\to\infty}\bigl[F^0(x^s, s) - \min\{F^0(x, s) \mid x \in X_s\}\bigr] = 0 .$$

Such procedures are essentially nonmonotone: a step on $F^0(\cdot, s)$ gives no guarantee of decrease of $F^0(\cdot, t)$ for $t \ge s+1$, nor of $f^0$. Their convergence therefore cannot be proved by the usual monotone Lyapunov argument. Section 6.4 of Yu. Ermoliev's chapter "Stochastic Quasigradient Methods" in Ermoliev & Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), gives the basic deterministic convergence theorem for this setting (Theorem 6.3) and the convergence criterion for nonmonotone sequences on which its proof rests (Theorem 6.4, taken from Ermoliev's 1976 monograph; the chapter compares its conditions with Zangwill's necessary and sufficient convergence conditions).

Timeline, as recorded in the chapter's bibliography (pp. 180–181): Ermoliev and Nurminski introduced limit extremal problems, in which $F^0(\cdot, s)$ and $X_s$ both converge ("Limit extremal problems", Kibernetika 1973, [14]); Nurminski gave convergence conditions for stochastic programming algorithms (Kibernetika 1973, [11]); Gupal treated time-varying functions (Kibernetika 1974, [15]); Ermoliev's monograph Stochastic Programming Methods (Nauka, 1976, [5]) contains the criterion stated here as Theorem 6.4 (p. 181); Nurminski formulated the general problem of nonstationary optimization (Kibernetika 1977, [16]); and Gaivoronski proved convergence of stochastic nonstationary procedures (Kibernetika 1978, [19]), the source of the chapter's Theorem 6.5.

Setting

Throughout, points are vectors of $\mathbb R^n$ with the Euclidean norm $\|\cdot\|$ and inner product $\langle\cdot,\cdot\rangle$.

• The projection onto a nonempty closed convex set $X \subseteq \mathbb R^n$ is $\pi_X(y) = \arg\min\{\|y - x\|^2 : x \in X\}$, the unique nearest point of $X$ to $y$.
• A subgradient of a convex function $F : \mathbb R^n \to \mathbb R$ at $x$ is a vector $g$ with $F(y) \ge F(x) + \langle g, y - x\rangle$ for all $y$. The book writes $F^0_x(x, s)$ for a subgradient of $F^0(\cdot, s)$ at $x$.
• The nonstationary projected subgradient method (6.41) starts from any $x^0 \in \mathbb R^n$ and sets

$$x^{s+1} = \pi_X\bigl[x^s - \rho_s g_s\bigr], \qquad g_s \text{ a subgradient of } F^0(\cdot, s) \text{ at } x^s,\quad s = 0, 1, \dots$$

with step sizes $\rho_s \ge 0$.

• For a closed set $X^*$ (in the application, the set of minimizers of $f^0$ on $X$) and a sequence $(x^s)$, the exit time from the $\varepsilon$-ball around $x^{s_k}$ is $\tau_k = \min\{s \ge s_k : \|x^s - x^{s_k}\| > \varepsilon\}$.
• The Lyapunov function of the proof is $V(x) = \min_{x^* \in X^*}\|x^* - x\|^2$, the squared distance to $X^*$.

Formalization targets

Goal: Theorem 6.3 (pp. 153–154)

Let $F^0(\cdot, s)$ and $f^0$ be convex continuous on $\mathbb R^n$, $X$ a nonempty convex compact set, $F^0(\cdot, s) \to f^0$ uniformly on $X$, $\|g_s\| \le C$, $\rho_s \ge 0$, $\rho_s \to 0$ and $\sum_s \rho_s = \infty$. Then the iterates of (6.41) satisfy

$$F^0(x^s, s) \longrightarrow \min\{f^0(x) \mid x \in X\} \qquad (s \to \infty).$$

The statement fixes no rate and no constant: only the qualitative limit, which is what the book proves.

Milestones

1. p. 155 — the one-step recursion $V(x^{s+1}) \le V(x^s) + 2\rho_s\langle g_s, x^*(s) - x^s\rangle + \rho_s^2\|g_s\|^2$, with $x^*(s)$ a point of $X^*$ nearest to $x^s$.
2. p. 156 — the travel bound $\|x^b - x^a\| \le \sum_{s=a}^{b-1}\|x^{s+1} - x^s\| \le C\sum_{s=a}^{b-1}\rho_s$ along (6.41) once $x^a \in X$.
3. p. 155 — conditions (1) and (2)(a) of Theorem 6.4 for (6.41): the iterates stay in a compact set and $\|x^{s+1} - x^s\| \to 0$.
4. Theorem 6.4 (p. 155) — if $X^*$ is closed, $(x^s)$ lies in a compact set, steps vanish along subsequences converging into $X^*$, the sequence leaves every small ball around a subsequential limit outside $X^*$, and it leaves with a strictly lower value of a continuous $V$ that takes countably many values on $X^*$, then $V(x^s)$ converges and all accumulation points lie in $X^*$.
5. pp. 155–156 — conditions (2)(b) and (3) of Theorem 6.4 for (6.41) with $X^* = \arg\min_X f^0$ and $V = \operatorname{dist}(\cdot, X^*)^2$:

$$\limsup_{k\to\infty} V(x^{\tau_k}) < \lim_{k\to\infty} V(x^{s_k}).$$

Significance

Theorem 6.3 is the prototype of the convergence results for simultaneous optimization and approximation. It covers smoothing schemes in which $f^0$ is replaced by $F^0(x, s) = \mathbb E f^0(x + h(s))$ with a vanishing perturbation $h(s)$ (the chapter's (6.39)–(6.40)), penalty and regularization sequences, and the deterministic skeleton of stochastic nonstationary methods such as Theorem 6.5. Theorem 6.4 is reusable well beyond this mission: it is a general tool for proving that accumulation points of a nonmonotone algorithm are solutions; the chapter introduces it as the tool for "essentially nonmonotonic solution procedures" in general.

Both results are classical and proved (Theorem 6.3 in the chapter itself, Theorem 6.4 in Ermoliev's 1976 monograph, whose proof the chapter cites but does not reproduce). No machine-checked proof of either is known to the platform's catalogue (searches for nonstationary optimization, Zangwill-type criteria and nonmonotone convergence return no match). The formalization adds a Lean statement and proof of a nonmonotone convergence criterion, a Lean proof of convergence for projected subgradient steps on a changing objective, and reusable facts about Euclidean projection onto a convex compact set.

Difficulty

The obvious argument for projected subgradient methods tracks $V(x^s) = \operatorname{dist}(x^s, X^*)^2$ and shows that it decreases whenever $x^s$ is far from $X^*$. Here that argument fails at two points. First, the subgradient is taken on $F^0(\cdot, s)$, not on $f^0$, so the decrease of $V$ holds only up to an error controlled by $\sup_X|F^0(\cdot, s) - f^0|$, and only while the iterate stays away from $X^*$; near $X^*$, $V$ may increase. Second, a decrease of $V$ over each excursion does not by itself exclude "cycling": the sequence may visit every neighbourhood of a point $x' \notin X^*$ infinitely often. Theorem 6.4 is formulated in terms of exit times and subsequences rather than single steps for this reason, and its hypothesis that $V$ takes only countably many values on $X^*$ is what separates it from a monotone-descent statement.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); sequences are indexed by ℕ from $s = 0$ as in the book. The iteration (6.41) is a hypothesis on a given sequence, x (s+1) = projX X (x s - ρ s • g s), with a given selection of subgradients g s; the subgradient inequality is required on all of $\mathbb R^n$, and $F^0(\cdot, s)$, $f^0$ are convex and continuous on all of $\mathbb R^n$.
• projX X y is a minimizer of $\|y - x\|^2$ over $X$ (junk value $y$ when none exists; every statement assumes $X$ nonempty, closed and convex). optimalSet f X is the set of minimizers of $f$ on $X$; $V$ is Metric.infDist · X* ^ 2.
• Added hypotheses the page does not print: $\rho_s \ge 0$ (step sizes are nonnegative throughout the chapter) and $X \ne \varnothing$ (the minimum over $X$ must exist). The limit $\min_X f^0$ is written sInf (f '' X); $\sum_s\rho_s = \infty$ is divergence of the partial sums.
• Constants. The only unspecified constant is the $C$ of the travel bound on p. 156 ("where $C$ is a constant"); the proof yields $C$ = the bound of hypothesis (d), $\|g_s\| \le C$, and that is the constant in milestone 2. All other results are qualitative.
• Corrections of the page. (i) Theorem 6.4 (2)(b) is printed as "$\tau_k = \min\{s \mid s \ge s_k, \|x^{s_k} - x^s\| < \varepsilon\} > \infty$", which no sequence satisfies; following the proof of Theorem 6.3 it is read as: $\tau_k = \min\{s \ge s_k : \|x^s - x^{s_k}\| > \varepsilon\}$ is finite. "For $\varepsilon$ sufficiently small and for any $s_k$" is read as "there is $\varepsilon_0 > 0$ such that for all $\varepsilon \in (0,\varepsilon_0)$ and all $k$", and condition (3) is imposed for the same $\varepsilon$. (ii) The left limit in (3) is read as $\limsup$ (the proof prints $\overline{\lim}$); the right limit is $V(x')$. (iii) The display on p. 155 prints "$=$" where the projection gives "$\le$". (iv) The proof on p. 155 prints "$x^{s_k} \to x' \in X^*$" where $x' \notin X^*$ is meant.
• Theorem 6.5 (the stochastic version, p. 156) is not formalized: the chapter states it without proof, citing [19], its moment hypothesis $E\|\xi^0(s)\| < \mathrm{const}$ and the measurability of the random step sizes $\rho_s$ are not pinned down on the page, and it is not used by Theorem 6.3.
• A trivializing formalization is ruled out: the goal is about the iteration (6.41) itself, not a statement that assumes $x^s \to X^*$ and derives the limit of the values, and no hypothesis forces the sequence or the functions to be constant.
• Contributions welcome: properties of projX (existence, uniqueness, nonexpansiveness, the obtuse-angle characterization), a proof of Theorem 6.4, and the two proof steps on pp. 155–156.

Selected references

• Yu. Ermoliev, "Stochastic Quasigradient Methods", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 6, pp. 141–185 (§6.4, pp. 152–156). https://doi.org/10.1007/978-3-642-61370-8
• Yu. M. Ermoliev, Stochastic Programming Methods (in Russian), Nauka, Moscow, 1976 (the chapter's [5]; Theorem 6.4 is on p. 181).
• Yu. M. Ermoliev and E. A. Nurminski, "Limit extremal problems", Kibernetika 1 (1973) (the chapter's [14]).
• E. A. Nurminski, "Convergence conditions of algorithms of stochastic programming", Kibernetika 3 (1973) (the chapter's [11]).
• E. A. Nurminski, "The problem of nonstationary optimization", Kibernetika 2 (1977) (the chapter's [16]).
• A. A. Gaivoronski, "Nonstationary stochastic programming problems", Kibernetika 4 (1978) (the chapter's [19]).
• W. I. Zangwill, Nonlinear Programming: A Unified Approach, Prentice-Hall, 1969.

Motivation

Almost every screening, auction and regulation model asks the same preliminary question: which allocation rules can be made incentive-compatible by some choice of payments? In the one-dimensional models of auction theory and nonlinear pricing the answer is monotonicity: higher types must receive higher allocations. Many applications are not one-dimensional, though. Examples are multi-object auctions, multi-product pricing, and lotteries over several outcomes. For those, a characterization that uses no structure at all is needed. Rochet (1987) gave one: an allocation rule is implementable exactly when it is cyclically monotone, a condition that originates in Rockafellar's characterization of subdifferentials of convex functions. Later work on dominant-strategy implementation, the "weak monotonicity" literature of algorithmic mechanism design, and revenue equivalence all build on it.

This mission formalizes Chapter 5 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): all nine numbered results of the chapter.

Timeline. Rockafellar (1970, Theorem 24.8) characterized the cyclically monotone maps between vector spaces as the subgradient selections of convex functions. Rochet (1987) extended the idea to arbitrary alternatives and types with quasi-linear utility and proved that implementability is exactly cyclical monotonicity. Krishna and Maenner (2001) proved revenue equivalence on convex type spaces with utilities convex in the type. Bikhchandani, Chatterji, Lavi, Mu'alem, Nisan and Sen (2006) showed that for finitely many alternatives, weak monotonicity (the two-type case of cyclical monotonicity) already suffices on rich, order-based domains. Saks and Yu (2005) proved the same on convex domains.

Setting

A designer and one agent choose an alternative $a$ from a set $A$. The agent has a type $\theta$ in a nonempty set $\Theta$. With utility function $u : A \times \Theta \to \mathbb R$, her payoff from $a$ when she pays $t$ is $u(a,\theta) - t$. Neither $A$ nor $\Theta$ carries any structure.

A direct mechanism is a decision rule $q : \Theta \to A$ and a transfer rule $t : \Theta \to \mathbb R$. It is incentive-compatible if $u(q(\theta),\theta) - t(\theta) \ge u(q(\theta'),\theta) - t(\theta')$ for all $\theta,\theta'$. A decision rule is implementable if some $t$ makes it incentive-compatible. It is weakly monotone if $u(q(\theta_1),\theta_1) - u(q(\theta_2),\theta_1) \ge u(q(\theta_1),\theta_2) - u(q(\theta_2),\theta_2)$ for all pairs of types. It is cyclically monotone if for every finite sequence of types $\theta^1,\dots,\theta^k$ with $\theta^k = \theta^1$,

$$\sum_{\kappa=1}^{k-1}\bigl(u(q(\theta^\kappa),\theta^{\kappa+1}) - u(q(\theta^\kappa),\theta^\kappa)\bigr) \le 0 .$$

A complete and transitive order $R$ of $A$ induces a partial order on types: $\theta \succ_R \theta'$ if $\theta$ values every $R$-higher alternative strictly more, relative to an $R$-lower one, than $\theta'$ does, and neither type distinguishes $R$-indifferent alternatives. The type set is one-dimensional if any two distinct types are $\succ_R$-comparable, and bounded if all utility differences lie in $(-c,c)$ for some $c > 0$. It is rich if, for some reflexive and transitive relation $R$, every function $v : A \to \mathbb R$ with $aRb \Rightarrow v(a) \ge v(b)$ is some type's utility function. A mechanism is individually rational with outside option $a$ if every type does at least as well as with $a$ and no payment.

Formalization targets

Goal: Proposition 5.2 (Rochet)

$$q \text{ implementable} \iff q \text{ cyclically monotone},$$

for arbitrary $A$, nonempty $\Theta$ and $u$.

Milestones

1. Proposition 5.1: implementable $\Rightarrow$ weakly monotone.
2. Proposition 5.3: for lotteries over finitely many outcomes, $\Theta \subseteq \mathbb R^\Omega$ convex and $u(p,\theta) = p\cdot\theta$, $q$ is implementable iff there is a convex $U$ on $\Theta$ with $U(\theta') \ge U(\theta) + q(\theta)\cdot(\theta'-\theta)$ for all $\theta,\theta'$.
3. Proposition 5.4: weakly monotone $\Rightarrow$ ($\theta \succ_R \theta' \Rightarrow q(\theta)\,R\,q(\theta')$), for every complete transitive $R$.
4. Proposition 5.5: on one-dimensional type sets, weak monotonicity $\iff$ monotonicity with respect to $R$.
5. Proposition 5.6: $A$ finite, $\Theta$ bounded and one-dimensional: monotone with respect to $R$ $\Rightarrow$ implementable.
6. Proposition 5.7 (Bikhchandani et al.): $A$ finite, rich and consistent domain: weakly monotone $\Rightarrow$ implementable.
7. Proposition 5.8 (revenue equivalence): on convex $\Theta \subseteq \mathbb R^n$ with $u(a,\cdot)$ convex and continuous, if $(q,t)$ is incentive-compatible then $(q,t')$ is iff $t' = t + \tau$ for a constant $\tau$.
8. Proposition 5.9: on one-dimensional type sets with a lowest type $\underline\theta$ and a worst alternative $\underline a$, an incentive-compatible mechanism is individually rational with outside option $\underline a$ iff $u(q(\underline\theta),\underline\theta) - t(\underline\theta) \ge u(\underline a,\underline\theta)$.

Significance

Rochet's theorem turns the existence of payments, an infinite system of linear inequalities in unknowns $t(\theta)$, into a condition on the decision rule alone. It underlies the characterization of implementable rules in multidimensional screening, the taxation principle, and the dominant-strategy characterizations of Chapter 7 (applied agent by agent). Propositions 5.4–5.6 recover the "monotone allocation" results of the one-dimensional chapters from it. Proposition 5.8 is the general form of the payoff-equivalence lemmas used for optimal auctions.

All results are classical and proved on paper, except Propositions 5.7 and 5.8, whose proofs the book omits and refers to the literature. None of them is formalized on Prove2Me. The platform's algorithmic-game-theory series has the weak-monotonicity half in a multi-agent valuation model (types are valuations $A \to \mathbb R$), not the abstract-type statement, and has no cyclical-monotonicity or Rochet result.

Difficulty

Necessity is a two-line telescoping argument. Sufficiency needs a transfer rule built from the decision rule, and the first idea fails: prices attached to alternatives chosen pair by pair (which weak monotonicity supplies) need not be globally consistent. Figure 5.1 of the book gives a three-type example that is weakly monotone but not implementable. The transfer must come from a supremum over all finite chains of types starting at a fixed type. The supremum is finite only because of cyclical monotonicity, and no finiteness, compactness or boundedness is available. Proposition 5.8 needs an envelope argument along segments in $\Theta$ without differentiability. Proposition 5.7 needs a combinatorial argument that uses richness of the domain.

Formalization scope

Alternatives and types are arbitrary Lean types A, Θ with Nonempty Θ, and the utility is u : A → Θ → ℝ. A cycle of length $k = m+1$ is a map Fin (m+1) → Θ with equal first and last entries, and its $m$ summands are indexed by Fin m. Relations are predicates A → A → Prop. For Propositions 5.3 and 5.8, types form a subset S of Ω → ℝ (resp. Fin n → ℝ) used as a subtype. Lotteries are stdSimplex ℝ Ω, and the subgradient inequality is required only at points of S.

The explicit statements are fixed as follows:

• Proposition 5.8's conclusion is the exact translation form $t'(\theta) = t(\theta) + \tau$ for one $\tau$ and all $\theta$.
• Proposition 5.9's condition is the single inequality at $\underline\theta$.
• Boundedness in Proposition 5.6 is Definition 5.9's strict two-sided bound with some $c > 0$.

Two statements are corrected from the page, each with a counterexample to the literal version recorded in its item:

• Proposition 5.7 adds Bikhchandani et al.'s requirement that every type's utility respects $R$.
• Proposition 5.8 adds continuity of $u(a,\cdot)$ on $\Theta$ (automatic in the relative interior).

Both directions of Rochet's theorem are required. The necessity half alone, or a version with finite $\Theta$, finite $A$ or bounded utilities, is a different and much weaker theorem and does not close the goal.

The development needs finite telescoping sums, suprema of sets of reals (sSup with an explicit bounded-above argument), convex functions on sets and one-dimensional convex analysis (Proposition 5.8). The definitions file is reusable for Chapters 6–8 of the series. Contributions of alternative proofs, for example Proposition 5.6 through Rochet's theorem, are welcome.

Selected references

• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 5. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• J.-C. Rochet, "A necessary and sufficient condition for rationalizability in a quasi-linear context," Journal of Mathematical Economics 16 (1987) 191–200. https://doi.org/10.1016/0304-4068(87)90007-3
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, Theorem 24.8.
• V. Krishna and E. Maenner, "Convex potentials with an application to mechanism design," Econometrica 69 (2001) 1113–1119. https://doi.org/10.1111/1468-0262.00233
• S. Bikhchandani, S. Chatterji, R. Lavi, A. Mu'alem, N. Nisan and A. Sen, "Weak monotonicity characterizes deterministic dominant-strategy implementation," Econometrica 74 (2006) 1109–1132. https://doi.org/10.1111/j.1468-0262.2006.00695.x
• M. Saks and L. Yu, "Weak monotonicity suffices for truthfulness on convex domains," Proceedings of the 6th ACM Conference on Electronic Commerce (2005) 286–293. https://doi.org/10.1145/1064009.1064039