Convex Optimization

Motivation

In robust optimization, a decision must satisfy a constraint for every parameter value in a prescribed uncertainty set. A nonlinear uncertain constraint can be difficult to use directly because it contains a universal condition over a continuum of parameters. Ben-Tal, den Hertog, and Vial study constraints whose value is concave in the uncertain parameter. Their Theorem 2 replaces the universal condition by one inequality involving a new vector and two conjugate functions. The replacement is the general framework used for the paper's later examples, including uncertainty regions assembled from simpler sets and nonlinear functions whose conjugates have explicit forms. The discussion paper, §§2–4 is the source for this mission; theorem and page numbers refer to that 2012 version.

The paper's result extends a more specialized counterpart for a linear uncertain constraint under a φ-divergence uncertainty region. That 2013 result has a proved formalization on Prove2Me, but its divergence-specific conjugate and uncertainty set are different objects. The same earlier formalization also supplies a proved version of the self-concordant-barrier statement that this paper quotes as Lemma 33, with a differently printed constant. Neither earlier theorem supplies the general concave-constraint result here.

Setting

Fix dimensions $m,n,L$. The nominal vector is $a^0\in\mathbb R^m$, and $A\in\mathbb R^{m\times L}$ maps a primitive uncertainty $\zeta\in Z\subseteq\mathbb R^L$ to an uncertain parameter $a=a^0+A\zeta$. Thus the uncertainty set is $U=\{a^0+A\zeta:\zeta\in Z\}$. The paper assumes that $Z$ is nonempty, convex, and compact, with $0$ in its relative interior $\operatorname{ri}Z$. Relative interior is taken inside the affine hull of a set, so $Z$ may lie in a lower-dimensional plane.

A decision is $x\in\mathbb R^n$. For each decision, $D(x)$ is the effective domain of the uncertain constraint $f(\cdot,x)$: $f(a,x)$ is real on $D(x)$ and is interpreted as $-\infty$ outside it. The function is concave in $a$ on $D(x)$ for every $x$; the paper imposes no convexity assumption in the decision $x$. The robust constraint (RC) is $f(a,x)\le0$ for every $a\in U$. In the domain representation used here, this means every $a\in U\cap D(x)$. The nominal vector is regular when $a^0\in\operatorname{ri}D(x)$ for every decision $x$, as in Definition 1.

The support function of $S$ is $\delta^*(y\mid S)=\sup_{a\in S}y^Ta$. The partial concave conjugate is $f_*(v,x)=\inf_{a\in D(x)}(a^Tv-f(a,x))$. Both have extended-real values: an empty support set has support value $-\infty$, and the conjugate can be $-\infty$ when its infimum is unbounded below. These values matter in the equivalence; replacing them by a default real number changes the constraint.

Formalization targets

The goal is the paper's Theorem 2. Under the standing assumptions and regularity, for every decision $x$,

$$\left[\forall a\in U\cap D(x),\ f(a,x)\le0\right] \quad\Longleftrightarrow\quad \left[\exists v\in\mathbb R^m:\ (a^0)^Tv+\delta^*(A^Tv\mid Z)-f_*(v,x)\le0\right].$$

The right-hand inequality is the Fenchel robust counterpart (FRC). Its existence claim is essential: equality of primal and dual infima alone would not show that an auxiliary vector satisfying FRC exists.

Four source statements form the milestone path. Remark 5 gives the weak-duality inequality and the FRC-to-RC implication without concavity. Equations (16)–(18) calculate the support function of $U$. Equation (7) states the relative-interior qualification. Equations (13)–(15) state the worst-case/dual-value identity and, through the printed minimum, attainment of the dual infimum. The milestone list quotes those source passages and identifies their printed pages. Theorem 2 and its proof appear on pp. 4–5.

Significance

The equivalence gives an exact way to replace an infinite family of uncertain inequalities by an existential constraint. In examples where the support function and concave conjugate can be evaluated or represented with standard optimization constraints, it yields a finite robust counterpart. The conclusion remains a mathematical equivalence even when such an explicit representation has not been found. It is also independent of any convexity of $f$ in the decision variable, a point the paper makes after Corollary 3.

This mission supplies reusable, domain-aware support and conjugate definitions and formal statements for the duality path in the paper's central result. The new goal and milestones are open proof obligations: their Lean declarations compile, but they do not yet have machine-checked proofs. The proved 2013 φ-divergence case is narrower and does not close them. A completed development would make the general relative-interior and attained-duality steps reusable for other robust optimization models.

Difficulty

The delicate point is the direction from RC to the existence of an FRC vector. Weak duality gives only a one-sided bound. Identifying the two optimal values still leaves an existence question when an infimum is not attained. The paper invokes Fenchel duality under a relative-interior intersection condition; replacing relative interior by ordinary interior would exclude lower-dimensional uncertainty sets and effective domains that the source permits. A second difficulty is keeping finite and infinite conjugate values distinct while subtracting them in the counterpart inequality. An unbounded-below conjugate must make a finite-support FRC value $+\infty$, not a plausible finite number.

Formalization scope

Vectors are functions on Fin m, Fin n, and Fin L; $A$ is a real matrix, and dot products use the finite-vector dot product. Mathlib's intrinsicInterior ℝ represents relative interior. The domain map $D(x)$ is explicit, with the concavity hypothesis imposed on that domain. The real representative of $f$ outside $D(x)$ is ignored everywhere. The paper's Notation paragraph calls its generic concave functions closed, but the statements here omit closedness: the finite-dimensional duality qualification used for Theorem 2 needs relative-interior overlap, not that extra regularity. This is a stated strengthening of the source theorem, not a change of its feasible points.

Support functions, conjugates, worst-case values, and dual values use EReal. The paper's “max” in (8), (13), and Remark 5 is read as an extended-real supremum; its “min” in (15) is an infimum accompanied by an attaining vector. The support identity includes $Z=\varnothing$, where both sides are $-\infty$, although Theorem 2 keeps the paper's nonempty, convex, compact $Z$. On the theorem's hypotheses the support value is finite and $D(x)$ is nonempty, so the undefined-looking combinations $+\infty-(+\infty)$ and $-\infty+(+\infty)$ cannot occur in FRC. No all-space real-valued substitute for $f_*$ is used, and the theorem still quantifies over every decision and every allowed uncertainty vector.

The proof development needs finite-dimensional relative-interior behavior under affine maps and Fenchel duality with attainment. General convex conjugates and support functions can serve later missions. Corollary 3 and the paper's complexity discussion are outside this mission. Theorem A.1 is not separately made a milestone here: as printed, its domain-restricted dual maximum has a problematic $-\infty$ case; the directly used, attained identity (13)–(15) is the target under the main theorem's standing assumptions.

Selected references

• A. Ben-Tal, D. den Hertog, J.-P. Vial, Deriving robust counterparts of nonlinear uncertain inequalities, CentER Discussion Paper 2012-053, Tilburg University, 2012. Discussion-paper PDF; journal version, Mathematical Programming, 2015, DOI 10.1007/s10107-014-0750-8.
• A. Ben-Tal et al., Robust solutions of optimization problems affected by uncertain probabilities, Management Science, 2013. Prove2Me formalization of its φ-divergence case.

Motivation

Robust optimization protects a decision against every realization of uncertain data in a prescribed uncertainty set. The standard approach replaces the uncertain constraints by a deterministic robust counterpart and solves that counterpart directly (Ben-Tal, El Ghaoui, Nemirovski, Robust Optimization, 2009). The counterpart is often a harder problem than the original: a robust linear program with ellipsoidal uncertainty becomes a second-order cone program, and a robust quadratic program can become a semidefinite program. A practitioner who has an efficient, specialised solver for the nominal problem may therefore have no efficient solver for its robust version.

Ben-Tal, Hazan, Koren and Mannor (arXiv:1402.6361, Operations Research 2015) ask whether the robust problem can be solved by repeatedly calling a solver of the nominal problem, with the number of calls independent of the dimension. Their first answer, the dual-subgradient meta-algorithm of §3.1, does so whenever the constraints are concave in the noise and the uncertainty set is convex. It is a primal–dual scheme: an online-learning algorithm picks the noise, and the nominal solver answers. This mission formalizes that result, Theorem 3.

Setting

Let $\mathcal D\subseteq\mathbb R^n$ be a convex domain, $\mathcal U\subseteq\mathbb R^d$ a convex uncertainty set, and $f_1,\dots,f_m:\mathbb R^n\times\mathbb R^d\to\mathbb R$ constraint functions. The robust feasibility problem (3) is

$$\exists\,x\in\mathcal D:\qquad f_i(x,u_i)\le 0\quad\forall u_i\in\mathcal U,\ i=1,\dots,m .$$

(An objective is handled by binary search on its value, so feasibility is the core question.) A point $x\in\mathcal D$ is an $\epsilon$-approximate solution if $f_i(x,u)\le\epsilon$ for all $u\in\mathcal U$ and all $i$.

An $\epsilon$-approximate oracle $\mathcal O_\epsilon$ (Figure 1) takes a noise vector $u=(u_1,\dots,u_m)\in\mathcal U^m$ and either returns some $x\in\mathcal D$ with $f_i(x,u_i)\le\epsilon$ for all $i$, or answers "infeasible", which it may do only if no $x\in\mathcal D$ has $f_i(x,u_i)\le 0$ for all $i$.

The standing assumptions of §3.1 are: each $f_i(\cdot,u)$ is convex on $\mathcal D$; each $f_i(x,\cdot)$ is concave on $\mathcal U$ for $x\in\mathcal D$; $D\ge\|u-v\|_2$ for all $u,v\in\mathcal U$; and $\|\nabla_u f_i(x,u)\|_2\le G$ for $x\in\mathcal D$, $u\in\mathcal U$. Write $P$ for the Euclidean projection onto $\mathcal U$.

Algorithm 1 sets $T=\lceil G^2D^2/\epsilon^2\rceil$ and $\eta=D/(G\sqrt T)$, starts from $u^0_1,\dots,u^0_m\in\mathcal U$, and for $t=1,\dots,T$ updates

$$u^t_i=P\bigl(u^{t-1}_i+\eta\,\nabla_u f_i(x^{t-1},u^{t-1}_i)\bigr),\qquad x^t=\mathcal O_\epsilon(u^t_1,\dots,u^t_m),$$

stopping with "infeasible" as soon as the oracle says so, and otherwise returning $\bar x=\frac1T\sum_{t=1}^T x^t$. In Lean these are alg1T, alg1Eta, alg1U, alg1X, alg1Output and alg1Calls in the namespace OracleRO.DualSubgrad.

Formalization targets

Goal: Theorem 3 (p. 7)

For every $\epsilon$-approximate oracle,

$$\text{output}=\text{"infeasible"}\ \Longrightarrow\ \neg\,\exists x\in\mathcal D\ \forall i\ \forall u\in\mathcal U:\ f_i(x,u)\le 0,$$ $$\text{output}=\bar x\ \Longrightarrow\ \bar x\in\mathcal D\ \text{ and }\ f_i(\bar x,u)\le 2\epsilon\ \ \forall i,\ \forall u\in\mathcal U,$$

and the number of oracle calls is at most $\lceil G^2D^2/\epsilon^2\rceil$.

Milestones

1. Lemma 1 (p. 5, Zinkevich 2003): projected online gradient ascent with step $\eta=D/(G\sqrt T)$ on concave rewards has regret $\sum_t f_t(x^*)-\sum_t f_t(x_t)\le GD\sqrt T$ for every $x^*$ in the decision set.
2. (6) (p. 7): if a point is returned, $\frac1T\sum_{t=1}^T f_i(x^t,u^t_i)\le\epsilon$ for every $i$.
3. (7) (p. 8): for every $i$ and $u\in\mathcal U$, $\frac1T\sum_t f_i(x^t,u)-\frac1T\sum_t f_i(x^t,u^t_i)\le GD/\sqrt T\le\epsilon$.
4. Final inequality of the proof (p. 8): $f_i(\bar x,u)\le\frac1T\sum_t f_i(x^t,u)$ for $u\in\mathcal U$.

Significance

The result. Theorem 3 turns any approximate solver of the nominal problem into an approximate solver of its robust counterpart, at a cost of $\lceil G^2D^2/\epsilon^2\rceil$ solver calls, a number that depends on the geometry of $\mathcal U$ and the sensitivity of the constraints to the noise but not on $n$, $d$ or $m$. It is the prototype of the paper's oracle-based reductions: the same primal–dual template, with a different online learner, gives the dual-perturbation algorithm of §3.2–3.3 for non-convex uncertainty sets, and the applications of §4 (robust linear programs, quadratic programs, semidefinite programs) instantiate it.

Formalizing it. The theorem is proved in the paper; none of it is machine-checked. A formal development adds a checked statement of the reduction with an explicit call count in place of the paper's $O(\cdot)$, and a reusable regret bound for projected online gradient ascent on concave rewards (Lemma 1), which the paper quotes from Zinkevich without proof and which many other online-learning results rest on.

Difficulty

The obvious argument for the dual side fails at one point: in round $t$ the primal point $x^t$ is computed from $u^t$, so the reward $f_i(x^t,\cdot)$ that the dual player faces depends on its own current move. A regret bound that assumed rewards fixed in advance, or drawn independently of the learner's play, would not apply. Lemma 1 must be used in its adversarial form, valid for every sequence of reward functions, including adaptively chosen ones. A second point is that the projection step requires the variational characterization of a nearest point in a convex set, which a mere "map into $\mathcal U$" does not provide.

Formalization scope

Points are elements of EuclideanSpace ℝ (Fin k), so every norm is the $\ell_2$ norm. The projection is a predicate IsProjOnto U P (each $P(y)$ is a nearest point of $\mathcal U$ to $y$), not a construction; the oracle is a function (Fin m → E d) → Option (E n) with none for "infeasible", constrained by the predicate IsApproxOracle on inputs in $\mathcal U^m$. The goal is quantified over every oracle meeting that specification. The gradient $\nabla_u f_i(x,u)$ is a given map gradU with HasGradientAt at points of $\mathcal U$; no differentiability in $x$ is assumed. Rounds are indexed by natural numbers with index $0$ for the initialization; the starting primal point $x^0\in\mathcal D$, used by the first update and left undefined by the algorithm, is an input. Hypotheses $D>0$ and $G>0$ are added so that $\eta$ and $T\ge1$ are meaningful. Maxima over $\mathcal U$ are stated as "for every $u\in\mathcal U$".

Explicit instantiations and corrections:

• The paper's "$O(G^2D^2/\epsilon^2)$ calls" is stated as at most $\lceil G^2D^2/\epsilon^2\rceil$ calls (one call per round, $T$ rounds).
• Lemma 1's "$G\ge\max_t\|f_t(x_t)\|$" is read as the gradient bound $\|\nabla f_t(x_t)\|\le G$, as the same sentence describes it.
• The proof's "Combining (10) and (12)" refers to (6) and (7).

Trivializing formalizations are ruled out: an oracle specification under which "infeasible" is never returned, or an output that is not the average of the oracle's answers, would not be Theorem 3. The "infeasible" conclusion is about the robust problem, not the nominal one.

A complete development needs the variational inequality for nearest points in a convex set, the gradient (supergradient) inequality for a concave function differentiable at a point of a convex set, Zinkevich's telescoping argument, and Jensen's inequality for finite averages. The first two and Lemma 1 are reusable beyond this mission. Proofs of the milestones, in any order, are welcome.

Selected references

• A. Ben-Tal, E. Hazan, T. Koren, S. Mannor, Oracle-Based Robust Optimization via Online Learning, arXiv:1402.6361v1, 2014; Operations Research 63(3), 2015. https://arxiv.org/abs/1402.6361v1
• M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• E. Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization, 2016. https://arxiv.org/abs/1909.05207

Motivation

A decision maker choosing a random outcome $X$ (a portfolio return, a policy's cost savings, a schedule's throughput) often has a reference outcome $Y$, the result of a benchmark policy, and wants the new outcome to be preferable to it for every risk-averse decision maker, not just on average. Expected-utility theory (von Neumann and Morgenstern) makes this precise: $X$ is preferred to $Y$ by every decision maker with a concave nondecreasing utility function $u$ exactly when $X$ dominates $Y$ in the second order, $X\succeq_{(2)}Y$. Requiring $X\succeq_{(2)}Y$ as a constraint in an optimization problem avoids having to elicit any particular utility function, which is rarely possible in practice and impossible when several decision makers must agree.

Dentcheva and Ruszczyński (preprint 2002, published in SIAM J. Optim. 14(2), 2003) introduced optimization problems with stochastic dominance constraints and developed their optimality and duality theory. The central finding is that the Lagrange multiplier of a second-order dominance constraint is itself a concave nondecreasing utility function: the optimal solution maximizes the objective plus an expected utility, for a utility function implied by the problem. This interpretation underlies the later literature on dominance-constrained portfolio optimization, risk-averse stochastic programming, and the dual (quantile) theory of stochastic orders.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $\mathcal L^1=\mathcal L^1(\Omega,\mathcal F,P)$ the space of integrable random variables with its norm topology. For $X\in\mathcal L^1$ the distribution function is $F(X;\eta)=P[X\le\eta]$ and the second-order shortfall function is

$$F_2(X;\eta)=\int_{-\infty}^{\eta}F(X;\alpha)\,d\alpha,\qquad \eta\in\mathbb R. \tag{2.1}$$

Changing the order of integration gives $F_2(X;\eta)=\mathbb E[(\eta-X)_+]$ (2.6), where $(\cdot)_+=\max(0,\cdot)$. The relation $X\succeq_{(2)}Y$ means $F_2(X;\eta)\le F_2(Y;\eta)$ for all $\eta$, and $A_2(Y)=\{X\in\mathcal L^1:X\succeq_{(2)}Y\}$.

The problem data are a reference outcome $Y\in\mathcal L^1$, a convex closed set $C\subseteq\mathcal L^1$, a functional $f$ that is concave and continuous on $C$, and an interval $[a,b]$. The paper studies the relaxation in which dominance is enforced on $[a,b]$:

$$\max f(X)\quad\text{subject to}\quad\mathbb E[(\eta-X)_+]\le\mathbb E[(\eta-Y)_+]\ \ \text{for all }\eta\in[a,b],\qquad X\in C. \tag{3.1–3.3}$$

The uniform dominance condition (Definition 4.1) asks for some $\tilde X\in C$ with $\inf_{\eta\in[a,b]}\{F_2(Y;\eta)-F_2(\tilde X;\eta)\}>0$.

The multiplier class $\mathcal U_1$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave and nondecreasing, vanish on $[b,\infty)$, and are affine on $(-\infty,a]$: $u(t)=u(a)+c(t-a)$ for $t\le a$, with a constant $c\ge0$. The Lagrangian is

$$L(X,u)=f(X)+\mathbb E[u(X)]-\mathbb E[u(Y)]. \tag{4.1}$$

Formalization targets

Goal: Theorem 4.2

Assume the uniform dominance condition. If $\hat X$ is an optimal solution of (3.1)–(3.3), there is $\hat u\in\mathcal U_1$ with

$$L(\hat X,\hat u)=\max_{X\in C}L(X,\hat u)\quad(4.2)\qquad\text{and}\qquad\mathbb E[\hat u(\hat X)]=\mathbb E[\hat u(Y)].\quad(4.3)$$

Conversely, if for some $\hat u\in\mathcal U_1$ a maximizer $\hat X\in C$ of $L(\cdot,\hat u)$ satisfies (3.2) and (4.3), then $\hat X$ is optimal for (3.1)–(3.3).

Milestones

The milestones follow the paper's proof. They are: finiteness of $\mathbb E[u(X)]$ for $u\in\mathcal U_1$; the identity (2.6), already proved on the platform; Proposition 2.3 (convexity and closedness of $A_2(Y)$, and its recession cone); the concavity of the constraint operator $G(X)(\eta)=F_2(Y;\eta)-F_2(X;\eta)$ with respect to the cone of nonnegative functions; the existence of a nonnegative measure multiplier $\hat\mu$ on $[a,b]$ satisfying (4.5)–(4.6); the facts that the function $u_\mu(t)=-\int_t^b\mu([\tau,b])\,d\tau$ ($t<b$), $u_\mu(t)=0$ ($t\ge b$) of a nonnegative measure lies in $\mathcal U_1$ and that every $u\in\mathcal U_1$ is $u_\mu$ for exactly one $\mu$; the key identity

$$\int_a^b F_2(X;\eta)\,d\mu(\eta)=-\mathbb E[u_\mu(X)]; \tag{4.9}$$

and the weak-duality step: (3.2) implies $\mathbb E[u(X)]\ge\mathbb E[u(Y)]$ for every $u\in\mathcal U_1$.

Further: Theorem 5.1

With $D(u)=\sup_{X\in C}L(X,u)$, the dual problem $\min_{u\in\mathcal U_1}D(u)$ has a solution, its value equals the primal optimal value, and its solutions are exactly the $\hat u\in\mathcal U_1$ satisfying (4.2)–(4.3).

Significance

Theorem 4.2 turns an infinite family of constraints, one for each $\eta\in[a,b]$, into a single scalar trade-off: at the optimum, the decision maker behaves as an expected-utility maximizer for an implicit utility $\hat u$, and the dominance constraint is active exactly in the sense $\mathbb E[\hat u(\hat X)]=\mathbb E[\hat u(Y)]$. Theorem 5.1 makes $\mathcal U_1$ the space of dual variables, which is the starting point of dual decomposition and cutting-plane methods for dominance-constrained problems and of their extensions to several constraints and to higher orders (Sections 6–7 of the paper, not part of this mission).

All results are proved in the paper. Apart from the identity (2.6), which is proved on the platform, none of them is formalized as far as the platform records show. A machine-checked development would provide, on top of the paper, a rigorous treatment of the measure–utility correspondence that the paper obtains from a textbook theorem "after an obvious adaptation", and a careful account of the multiplier class itself (see the scope section on the constant $c$). The definitions of $F_2$ and of the identity (2.6) are shared with the platform's missions on Dual Stochastic Dominance and Related Mean-Risk Models (Ogryczak and Ruszczyński, 2002).

Difficulty

The necessity half needs a Lagrange multiplier for a constraint taking values in the infinite-dimensional space $\mathcal C([a,b])$; finite-dimensional convex duality does not apply, and the multiplier first appears as a nonnegative measure on $[a,b]$, an element of the dual of $\mathcal C([a,b])$. A Slater-type point is required: without the uniform dominance condition the multiplier may not exist. This is why the dominance relation, which the paper first poses on all of $\mathbb R$, is relaxed to a bounded interval $[a,b]$: for a reference outcome with a smallest value $y_1$, $F_2(Y;y_1)=0$, so no $\tilde X$ can dominate $Y$ strictly near $y_1$.

The second obstacle is the translation of that measure into a utility function. The identity (4.9) requires an interchange of integrals over $\mathbb R\times[a,b]$ and an integration by parts against the distribution function of an arbitrary integrable $X$, followed by a limit in which the integrability of $X$ controls the linear growth of $u$ at $-\infty$. The converse direction needs every $u\in\mathcal U_1$ to be represented by a unique measure, through the left derivative of a concave function.

Formalization scope

Outcomes are elements of Mathlib's $L^1$ space Ω →₁[P] ℝ over a probability measure P, coerced to functions inside integrals; no statement is pointwise in $\omega$. $F_2$ is the published definition DualSSD.Shared.secondPerformance, a Bochner integral of $P[X\le\alpha]$ over $(-\infty,\eta]$. The problem data form a structure whose fields include every standing assumption of the paper: $C$ convex and closed, $f$ concave and continuous on $C$. The constraint (3.2) is stated in its printed expectation form, while Definition 4.1 and the proof objects use $F_2$, as printed; their equality is (2.6).

Committed conventions:

• $\mathcal U_1$ uses $c\ge0$. The paper prints $c>0$. With $c>0$ the necessity half of Theorem 4.2 is false: take $Y\equiv0$, $[a,b]=[1,2]$, $f(X)=\mathbb EX$ and $C$ the constant random variables with values in $[0,1]$. Then $\tilde X\equiv1$ satisfies Definition 4.1, $\hat X\equiv1$ is optimal, and (4.3) forces $c=0$. The proof itself produces $c=\mu([a,b])$, which vanishes for the zero multiplier of a slack constraint, and the paper calls $\mathcal U_1$ a convex cone, which must contain $0$.
• Definition 4.1's infimum is encoded as a positive lower bound $\varepsilon$ on $[a,b]$. "$=\max_{X\in C}$" is encoded as membership in $C$ plus an upper bound over $C$.
• A nonnegative measure in $\mathbf{rca}([a,b])$ is a finite Borel measure on $\mathbb R$ giving zero mass to the complement of $[a,b]$, which is the paper's own extension by zero. Integrals $\int_a^b\cdot\,d\mu$ are over the closed interval, so atoms at $a$ and $b$ count.
• No relation between $a$ and $b$ is assumed. For $a>b$ every statement remains meaningful: the constraint is vacuous and $\mathcal U_1=\{0\}$.
• Theorem 5.1's dual function takes values in the extended reals.

A trivializing formalization is ruled out: a junk-valued expectation (a Bochner integral of a non-integrable function, which Lean sets to $0$) cannot occur for $u\in\mathcal U_1$, and its integrability is a milestone. Dropping the concavity of $f$ or the convexity of $C$ would make the necessity half false, so these assumptions are fields of the problem data.

Infrastructure a complete development needs: convex duality for cone constraints in $\mathcal C([a,b])$ (or a direct separation argument in $\mathbb R\times\mathcal C([a,b])$), the Riesz representation of nonnegative functionals on $\mathcal C([a,b])$, Fubini and integration by parts for Stieltjes measures, and the measure of a left-continuous monotone function. These pieces are reusable beyond this mission. Contributions to any milestone are welcome. The extensions to several dominance constraints and to higher-order dominance are not included.

Selected references

• D. Dentcheva and A. Ruszczyński, Optimization with stochastic dominance constraints, preprint dated December 27, 2002 (Stochastic Programming E-Print Series); published in SIAM Journal on Optimization 14(2):548–566, 2003. https://doi.org/10.1137/S1052623402420528
• W. Ogryczak and A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM Journal on Optimization 13(1):60–78, 2002. https://doi.org/10.1137/S1052623400375075
• J. F. Bonnans and A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
• J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, Princeton University Press, 1944.

Motivation

In online convex optimization a decision maker picks points $x_1,x_2,\dots,x_n$ in a convex set $S\subseteq\mathbb R^d$, and after each choice pays $c_t(x_t)$ for a convex cost function $c_t$ chosen in advance by an adversary. Performance is measured by regret: the total cost paid minus the cost of the best fixed point in hindsight. Zinkevich (ICML 2003) showed that projected gradient descent has regret $O(\sqrt n)$ when the whole function $c_t$, or at least its gradient at $x_t$, is revealed after each round.

In many applications only the number $c_t(x_t)$ is observed: a seller sets a price and sees revenue, a router picks a path and sees its delay, an advertiser places a bid and sees the cost. This is the bandit setting. Flaxman, Kalai and McMahan (arXiv:cs/0408007, SODA 2005) gave the first simple algorithm for bandit convex optimization against an oblivious adversary with general bounded convex costs: a randomized gradient descent that estimates the gradient from a single function value, with expected regret $O(n^{5/6})$. The same one-point gradient estimate is the starting point of later work on bandit convex optimization and on zeroth-order (derivative-free) stochastic optimization; see, e.g., Bubeck and Cesa-Bianchi's survey (arXiv:1204.5721, Ch. 6) and Hazan's textbook (arXiv:1909.05207, Ch. 6).

Timeline. Zinkevich (2003): $O(\sqrt n)$ regret with full gradient feedback. Kleinberg (NIPS 2004), independently: $O(n^{3/4})$ bandit regret for Lipschitz costs by a different reduction. Flaxman, Kalai, McMahan (2004/2005): $O(n^{5/6})$ for bounded convex costs and $O(n^{3/4})$ for Lipschitz costs, with one function value per round. Later work (Bubeck, Lee, Eldan 2017 and others) reached $\tilde O(\sqrt n)$ with more complex algorithms.

Setting

Let $\mathbb B=\{x\in\mathbb R^d : |x|\le1\}$ and $\mathbb S=\{x : |x|=1\}$ be the closed unit ball and the unit sphere, $d\ge1$. The feasible set $S$ is closed and convex with

$$r\mathbb B\subseteq S\subseteq R\mathbb B,\qquad r>0 .$$

The costs $c_1,c_2,\dots$ are fixed before play (an oblivious adversary); each is convex on $S$ with $|c_t(x)|\le C$ for $x\in S$, where $C>0$. For $K\subseteq\mathbb R^d$, $P_K(z)$ is the nearest point of $K$ to $z$.

The bandit gradient descent algorithm $\mathrm{BGD}(\alpha,\delta,\nu)$ (Figure 1 of the paper) keeps an iterate $y_t$ with $y_1=0$. At period $t$ it draws a unit vector $u_t$ uniformly from $\mathbb S$, independently of the past, plays

$$x_t=y_t+\delta u_t ,$$

observes only $c_t(x_t)$, and updates

$$y_{t+1}=P_{(1-\alpha)S}\big(y_t-\nu\,c_t(x_t)\,u_t\big).$$

The smoothed cost is $\hat c_t(x)=\mathbb E_{v\in\mathbb B}[c_t(x+\delta v)]$ with $v$ uniform on $\mathbb B$. The expected regret after $n$ rounds is

$$\mathbb E\Big[\sum_{t=1}^n c_t(x_t)\Big]-\min_{x\in S}\sum_{t=1}^n c_t(x).$$

Formalization targets

Goal: Theorem 1 (p. 8)

For every $n\ge(3Rd/2r)^2$, with $\nu=R/(C\sqrt n)$, $\delta=\sqrt[3]{rR^2d^2/(12n)}$ and $\alpha=\sqrt[3]{3Rd/(2r\sqrt n)}$,

$$\mathbb E\Big[\sum_{t=1}^n c_t(x_t)\Big]-\min_{x\in S}\sum_{t=1}^n c_t(x)\le 3Cn^{5/6}\sqrt[3]{\frac{12\,dR}{r}} .$$

The paper prints the constant $3Cn^{5/6}\sqrt[3]{dR/r}$. Its own last step bounds the regret by $a/\delta+b\delta/\alpha+c\alpha$ with $a=RdC\sqrt n$, $b=6Cn/r$, $c=2Cn$, and with the stated $\delta$ and $\alpha$ this equals $3\sqrt[3]{abc}=3Cn^{5/6}\sqrt[3]{12dR/r}$. The goal states the bound the proof establishes.

Milestones

1. Lemma 1 (p. 5): $\mathbb E_{u\in\mathbb S}[f(x+\delta u)u]=\frac\delta d\nabla\hat f(x)$, the one-point gradient estimate.
2. Lemma 2 (p. 6): gradient descent with conditionally unbiased gradient estimates of norm at most $G$ has expected regret at most $RG\sqrt n$ for $\eta=R/(G\sqrt n)$.
3. Observations 1–3 (pp. 7–8): the comparator over $(1-\alpha)S$ is within $2\alpha Cn$ of that over $S$; balls of radius $\alpha r$ around $(1-\alpha)S$ lie in $S$; on $(1-\alpha)S$ the costs satisfy $|c_t(x)-c_t(y)|\le\frac{2C}{\alpha r}|x-y|$.
4. The played points are feasible (p. 8).
5. Regret against the smoothed costs (p. 9): at most $RdC\sqrt n/\delta$.
6. Display (10) (p. 9): regret at most $RdC\sqrt n/\delta+3\delta Ln+2\alpha Cn$ with $L=2C/(\alpha r)$.

Companion items

The tuning identity (p. 9): $a/\delta+b\delta/\alpha+c\alpha=3\sqrt[3]{abc}$ at $\delta=\sqrt[3]{a^2/bc}$, $\alpha=\sqrt[3]{ab/c^2}$, for $a,b,c>0$.

Theorem 2 (p. 9). If each $c_t$ is $L$-Lipschitz on $S$, then with $\nu=R/(C\sqrt n)$, $\delta=n^{-1/4}\sqrt{RdCr/(3(Lr+C))}$, $\alpha=\delta/r$, and $n$ large enough that $\delta<r$,

$$\mathbb E\Big[\sum_{t=1}^n c_t(x_t)\Big]-\min_{x\in S}\sum_{t=1}^n c_t(x)\le 2n^{3/4}\sqrt{3RdC\big(L+C/r\big)} .$$

Significance

The theorem shows that bandit feedback costs only a polynomial factor in regret for arbitrary bounded convex costs, with an algorithm that is gradient descent plus one random perturbation per round. Lemma 1 is the general tool behind it: an unbiased estimate of the gradient of a smoothed function from one function value. It is reused across zeroth-order optimization, bandit learning and stochastic approximation. Lemma 2 is a self-contained regret bound for projected gradient descent with noisy gradients, the shape in which Zinkevich's analysis is most often applied.

The results are proved in the paper and are standard. To the platform's knowledge none of them has a machine-checked proof. Related statements from Bubeck and Cesa-Bianchi's survey, for differentiable Lipschitz losses, are open on the platform, and two earlier formalizations of the textbook versions were disproved because of missing regularity or independence hypotheses. Formalizing this mission produces a checked one-point gradient identity for continuous (not differentiable) functions on the sphere, a measure-theoretic regret bound for stochastic projected gradient descent, and the corrected constant of Theorem 1.

Difficulty

The bandit algorithm itself is simple; the difficulty sits in Lemma 1 and in the measure theory around it. The paper derives Lemma 1 from Stokes' theorem, $\nabla\int_{\delta\mathbb B}f(x+v)\,dv=\int_{\delta\mathbb S}f(x+u)\frac{u}{|u|}\,du$, and the ratio $\delta/d$ of the volume to the surface area of a ball. Mathlib has neither this divergence identity on balls in $\mathbb R^d$ nor the explicit link between its spherical measure and the surface integral needed here. The identity must hold for functions that are merely continuous near the ball, since convex costs need not be differentiable.

The obvious first idea, differentiating under the integral sign in $\hat f(x)=\mathbb E_v[f(x+\delta v)]$, fails because $f$ is not differentiable. The second obvious idea, applying Lemma 1 to $c_t$ as given, fails at the boundary of $S$, where $c_t$ is unconstrained. Lemma 2's conditional expectation $\mathbb E[g_t\mid x_t]$ requires that the direction $u_t$ be independent of the iterate $y_t$, and the integrability and measurability of the played points come from continuity of convex functions in the interior of $S$.

Formalization scope

Points are EuclideanSpace ℝ (Fin d) with $d\ge1$, and rounds are numbered $1,\dots,n$. The costs are functions on $\mathbb R^d$, and no statement assumes anything about them outside $S$: no global convexity, continuity, differentiability or Lipschitz bound. The standing model is part of the goal's hypotheses: $S$ is convex with $r\mathbb B\subseteq S\subseteq R\mathbb B$, the costs are convex on $S$ with values in $[-C,C]$ there, and $C>0$. Additions and conventions:

• $S$ is assumed closed. The paper's projection oracle $P_S(x)=\arg\min_{z\in S}|x-z|$ presupposes that the minimum is attained.
• The directions $u_t$ are measurable, independent, and each uniform on $\mathbb S$ (the published uniformSphere d). Uniform marginals alone are not enough.
• The BGD run is a relation (IsBGDRun) required for every outcome. Projection uses the published predicate IsNearestPoint, and regret the published pseudoRegret, whose minimum is an infimum over the subtype; it is attained in every use here.
• Lemma 1 adds continuity of $f$ on an open set containing $x+\delta\mathbb B$. As printed ("for any function $f$") it is false. The application in Theorem 1 supplies this hypothesis.
• The smoothed-regret and (10) milestones use the strict $\delta<\alpha r$ (the page has $\delta/r\le\alpha$), which keeps every smoothing ball in the interior of $S$. They use $\alpha\le1$ in place of $\alpha<1$; Theorem 1's $\alpha$ equals $1$ at $n=(3Rd/2r)^2$.
• Theorem 2's "for $n$ sufficiently large" is the hypothesis $\delta<r$, the only place the proof uses it.

A formalization that assumed integrability of the costs along the run, assumed differentiable or globally Lipschitz costs, dropped the independence of the directions, or stated $\nabla\hat f$ through Mathlib's gradient (which is $0$ off differentiability) would trivialize or change the result. All of these are ruled out.

Needed infrastructure: the divergence identity for the ball average (Lemma 1), conditional expectation given $\sigma(x_t)$ for vector-valued variables, continuity of convex functions on the interior of a convex set, and nearest-point projection onto closed convex sets. The first two are reusable well beyond this mission. Contributions toward Lemma 1 in particular are welcome.

Selected references

• A. D. Flaxman, A. T. Kalai, H. B. McMahan, Online convex optimization in the bandit setting: gradient descent without a gradient, SODA 2005; arXiv:cs/0408007v1, 2004. https://arxiv.org/abs/cs/0408007
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://www.cs.cmu.edu/~maz/publications/ICML03.pdf
• R. Kleinberg, Nearly tight bounds for the continuum-armed bandit problem, NIPS 2004. https://papers.nips.cc/paper/2634-nearly-tight-bounds-for-the-continuum-armed-bandit-problem
• S. Bubeck, N. Cesa-Bianchi, Regret analysis of stochastic and nonstochastic multi-armed bandit problems, Foundations and Trends in ML, 2012. https://arxiv.org/abs/1204.5721
• E. Hazan, Introduction to online convex optimization, 2nd ed., 2019. https://arxiv.org/abs/1909.05207
• S. Bubeck, Y. T. Lee, R. Eldan, Kernel-based methods for bandit convex optimization, STOC 2017. https://arxiv.org/abs/1607.03084

Motivation

Many problems in machine learning and statistics are regularized empirical risk minimization: minimize an average $f(x)=\frac1n\sum_{i=1}^n f_i(x)$ of $n$ loss terms, one per data point, plus a regularizer $\psi(x)$ such as $\lambda\|x\|_1$. When $n$ is large, a full gradient $\nabla f$ costs $n$ component gradients, so stochastic gradient methods that touch one $f_i$ per step are preferred. Variance-reduced methods (SVRG, SAGA) correct the stochastic gradient with a periodically recomputed full gradient and reach the rates of full-gradient descent at the cost of stochastic steps; accelerated full-gradient methods (Nesterov) improve the rate from $O(1/T)$ to $O(1/T^2)$ on convex problems.

Combining the two directly was open until Allen-Zhu's Katyusha (arXiv:1603.05953, STOC 2017, JMLR 2018). Before it, accelerated stochastic rates were obtained either for special structure (accelerated coordinate and dual methods, which need strong convexity or dual access) or through reductions such as Catalyst and APPA, which wrap a non-accelerated method in an outer proximal-point loop and lose logarithmic factors. Katyusha adds a third momentum term, the Katyusha momentum, that pulls each iterate back to the snapshot point, and obtains the accelerated rate directly. This mission concerns the paper's second main result: the variant Katyusha$^{\mathrm{ns}}$ (Algorithm 2) for objectives that are convex but not strongly convex.

Setting

Problem (1.1) of the paper is

$$\min_{x\in\mathbb R^d} F(x)=f(x)+\psi(x)=\frac1n\sum_{i=1}^n f_i(x)+\psi(x),$$

where $n\ge1$, each component $f_i:\mathbb R^d\to\mathbb R$ is convex and $L$-smooth, $\|\nabla f_i(x)-\nabla f_i(y)\|\le L\|x-y\|$, and the regularizer $\psi$ is convex. A point $x^*$ minimizes $F$.

Katyusha$^{\mathrm{ns}}(x_0,S,L)$ runs $S$ epochs of $m$ iterations each (the paper takes $m=2n$). It keeps three sequences $y_k$, $z_k$ and a snapshot $\widetilde x^s$, all starting at $x_0$, and fixes $\tau_2=\frac12$. Epoch $s$ uses the weight $\tau_{1,s}=\frac{2}{s+4}$ and the step $\alpha_s=\frac{1}{3\tau_{1,s}L}$, computes $\nabla f(\widetilde x^s)$ once, and performs, for $k=sm,\dots,sm+m-1$:

1. the coupling $x_{k+1}=\tau_{1,s}z_k+\tau_2\widetilde x^s+(1-\tau_{1,s}-\tau_2)y_k$;
2. the SVRG estimator $\widetilde\nabla_{k+1}=\nabla f(\widetilde x^s)+\nabla f_i(x_{k+1})-\nabla f_i(\widetilde x^s)$, with $i$ uniform in $\{1,\dots,n\}$, independent across iterations;
3. the mirror step $z_{k+1}=\arg\min_z\{\frac1{2\alpha_s}\|z-z_k\|^2+\langle\widetilde\nabla_{k+1},z\rangle+\psi(z)\}$;
4. the gradient step (Option I) $y_{k+1}=\arg\min_y\{\frac{3L}2\|y-x_{k+1}\|^2+\langle\widetilde\nabla_{k+1},y\rangle+\psi(y)\}$.

At the end of the epoch the new snapshot is the average $\widetilde x^{s+1}=\frac1m\sum_{j=1}^m y_{sm+j}$. The output is $\widetilde x^S$. Throughout, $D_k=F(y_k)-F(x^*)$ and $\widetilde D^s=F(\widetilde x^s)-F(x^*)$.

Formalization targets

Goal: Theorem 4.1 with the constants of its proof

$$\mathbb E\big[F(\widetilde x^S)\big]-F(x^*)\le\frac{16\,\big(F(x_0)-F(x^*)\big)}{(S+3)^2}+\frac{12\,L\,\|x_0-x^*\|^2}{m\,(S+3)^2}\qquad(S\ge0,\ m\ge1).$$

The paper states $O\big(\frac{F(x_0)-F(x^*)}{S^2}+\frac{L\|x_0-x^*\|^2}{mS^2}\big)$; the explicit form above is what its proof in Appendix C.1 establishes.

Milestones, in the order of the proof

1. Lemma 2.7 for $\sigma=0$: the one-iteration inequality coupling $D_k$, $\mathbb E[D_{k+1}]$, $\widetilde D$ and the distances $\|z_k-x^*\|^2$, $\mathbb E\|z_{k+1}-x^*\|^2$.
2. (C.1): Lemma 2.7 summed over one epoch.
3. (C.2): the epoch inequality for $s\ge1$, after inserting the average snapshot and $\alpha_s=1/(3\tau_{1,s}L)$.
4. (C.3): the same for the base epoch $s=0$.
5. The parameter inequalities $\frac1{\tau_{1,s}^2}\ge\frac{1-\tau_{1,s+1}}{\tau_{1,s+1}^2}$ and $\frac{\tau_{1,s}+\tau_2}{\tau_{1,s}^2}\ge\frac{\tau_2}{\tau_{1,s+1}^2}$.
6. (C.4): the bound telescoped over $S$ epochs.

Significance

Theorem 4.1 gives the accelerated $O(1/S^2)$ rate for non-strongly convex composite finite sums with a direct method: $\varepsilon$ error after $O\big(\frac{n\sqrt{F(x_0)-F(x^*)}}{\sqrt\varepsilon}+\frac{\sqrt{nL}\,\|x_0-x^*\|}{\sqrt\varepsilon}\big)$ stochastic gradient evaluations, a factor $S$ better than the $O(1/S)$ of non-accelerated variance-reduced methods such as SAGA (Remark 4.2). The non-strongly convex case covers $\ell_1$-regularized and unregularized convex losses, where no strong-convexity parameter is available to tune a linear-rate method.

The result is proved in the paper; no machine-checked proof of Katyusha or Katyusha$^{\mathrm{ns}}$ is known to exist. The mission produces a formal statement of the algorithm and its rate with explicit constants, and a formal chain of the paper's intermediate inequalities. A SAGA mission on this platform states SAGA's non-accelerated $O(1/k)$ rate for the same problem class, so the two results become directly comparable in Lean.

Difficulty

Each step uses only convexity, smoothness and the optimality of proximal points, but the steps interlock. The variance of $\widetilde\nabla_{k+1}$ cannot be bounded by $F(\widetilde x)-F(x^*)$ as in SVRG's analysis without losing acceleration; the paper's bound (Lemma 2.4) leaves a linear term $\langle\nabla f(x_{k+1}),\widetilde x-x_{k+1}\rangle$ that is cancelled only by the specific weight $\tau_2=\frac12$ of the Katyusha momentum (Lemmas 2.6–2.7). Without strong convexity the per-epoch inequalities do not contract, so the proof must telescope across epochs with epoch-dependent weights $\tau_{1,s}$: the coefficients of $D_{sm+j}$ produced by epoch $s$ must dominate those consumed by epoch $s+1$, and the snapshot term $m\widetilde D^s$ must be charged to the previous epoch's iterates. Getting the boundary epoch $s=0$ (whose snapshot is $x_0$) and the last epoch right is where the constants come from.

Formalization scope

The Lean development works on EuclideanSpace ℝ (Fin d) with components indexed by Fin n ($n\ge1$). Gradients are given functions $\nabla f_i$ tied to $f_i$ by HasGradientAt; $L$-smoothness is the Lipschitz bound on them with $L>0$; convexity is ConvexOn ℝ Set.univ. $f$ and $\nabla f$ are the published SAGA.Convex.fAvg and SAGA.Convex.gradAvg. The regularizer $\psi$ is real-valued and convex, so extended-valued regularizers such as indicator functions of constraint sets are not covered. The two arg-min steps are evaluated through a map $P$ assumed to return a proximal point of $\psi$ (the published SAGA.Convex.IsProxPoint) for every positive step; for real-valued convex $\psi$ such points exist and are unique, so the hypothesis is satisfiable. $x^*$ is assumed to minimize $F$ (without strong convexity a minimizer need not exist). Randomness is modelled by finite sequences of indices: the expectation is the uniform average over all index sequences (SAGA.Convex.expectIdx), with the $Sm$ indices split into epochs by Mathlib's finProdFinEquiv.

Conventions committed to:

• Explicit constants for O(·). The goal's $O(\cdot)$ is instantiated as $16\,(F(x_0)-F(x^*))/(S+3)^2+12L\|x_0-x^*\|^2/(m(S+3)^2)$: the proof bounds $\widetilde D^S$ by $\frac{2\tau_{1,S-1}^2}{m}$ times the right-hand side of (C.4), which equals $2m\,(F(x_0)-F(x^*))+\frac{3L}2\|x_0-x^*\|^2$, with $\tau_{1,S-1}=\frac2{S+3}$. The bound holds trivially at $S=0$, so the goal is stated for all $S$.
• Epoch length. $m\ge1$ is a parameter (the algorithm sets $m=2n$); every statement holds for every $m\ge1$.
• Option I only; the unused input $\sigma$ and Option II are not modelled.
• Lemma 2.7 is stated for $\sigma=0$ with the paper's implicit side conditions $\alpha>0$, $0<\tau_1\le\frac12$.
• (C.2) is stated for an epoch $s\ge1$ whose snapshot is the average of given previous iterates; (C.1) and (C.3) are stated from an arbitrary epoch start state, which is the paper's "the randomness in the first $s-1$ epochs is fixed".
• The typo $\|z_{Sm}-z^*\|^2$ in (C.4) is read as $\|z_{Sm}-x^*\|^2$.

A trivializing formalization is ruled out: the prox map, the gradients and $x^*$ are all tied to $\psi$, $f_i$ and $F$ by hypotheses that a quadratic instance satisfies, and the expectation averages over every index sequence rather than a chosen one. The iteration count stated "in other words" after Theorem 4.1 is not a target.

Contributions welcome: proofs of the milestones in any order; general lemmas about proximal points of convex functions (the three-point inequality behind Lemma 2.5) and the co-coercivity of convex $L$-smooth functions (behind Lemma 2.4) are reusable beyond this mission.

Selected references

• Z. Allen-Zhu, Katyusha: The First Direct Acceleration of Stochastic Gradient Methods, STOC 2017; JMLR 18(221), 2018. arXiv:1603.05953v6. https://arxiv.org/abs/1603.05953
• A. Defazio, F. Bach, S. Lacoste-Julien, SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives, NeurIPS 2014. https://arxiv.org/abs/1407.0202
• R. Johnson, T. Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, NeurIPS 2013. https://papers.nips.cc/paper/4937
• Y. Nesterov, Introductory Lectures on Convex Programming, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Large-scale nonsmooth convex problems, such as minimising a Lipschitz convex function over a probability simplex with millions of coordinates, are routinely solved by first-order methods that use one subgradient per iteration. The classical projected subgradient method reaches accuracy $\varepsilon$ after $O(L^2 R^2/\varepsilon^2)$ iterations, where $L$ and $R$ are measured in the Euclidean norm; on the simplex this hides a factor of order $n$ in the dimension. Nemirovski and Yudin's mirror descent algorithm (MDA) replaces the Euclidean geometry by one adapted to the feasible set and, on the simplex, reduces the dimension dependence to $\ln n$.

Beck and Teboulle (Oper. Res. Lett. 31 (2003) 167–175, doi:10.1016/S0167-6377(02)00231-6) showed that mirror descent is a projected subgradient method in which the squared Euclidean distance is replaced by a Bregman-type distance $B_\psi$. This viewpoint gives a short convergence proof, and with the entropy as $\psi$ it yields a fully explicit method on the simplex, the entropic mirror descent algorithm (EMDA), the same multiplicative update that underlies exponentiated-gradient and Hedge-type algorithms in online learning.

Timeline. Nemirovski and Yudin (1983) introduce mirror descent with a $O(\sqrt{\ln n}/\sqrt k)$ rate on the simplex. Ben-Tal, Margalit and Nemirovski (SIAM J. Optim. 12 (2001)) analyse MDA with the $\ell_p$ potential $\tfrac12\|x\|_p^2$, $p = 1 + 1/\ln n$, whose conjugate requires a one-dimensional root-finding at each step. Beck and Teboulle (2003) derive MDA as a nonlinear projected subgradient method (SANP), prove its efficiency estimate for an arbitrary norm, and show that the entropy gives the same $\sqrt{2\ln n}\,L_f/\sqrt k$ rate with a closed-form update.

Setting

Let $E$ be $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and $\|z\|_* = \max\{\langle x, z\rangle : \|x\| \le 1\}$ the dual norm. The problem is $\min\{f(x) : x \in X\}$ under Assumption A: $X$ is closed and convex; $f$ is convex on $X$ and Lipschitz there, $|f(x) - f(y)| \le L_f\|x - y\|$; $f$ has a minimiser $x^* \in X$; and a subgradient $f'(x)$ can be computed at every $x \in X$.

Let $\psi : X \to \mathbb R$ be strongly convex with parameter $\sigma > 0$ and differentiable. The distance-like function (3.10) is

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

The subgradient algorithm with nonlinear projections (SANP, (3.11)) starts from $x^1$ and sets, with step sizes $t_k > 0$,

$$x^{k+1} = \operatorname*{argmin}_{x \in X}\Big\{\langle x, f'(x^k)\rangle + \tfrac{1}{t_k} B_\psi(x, x^k)\Big\}.$$

With $\psi = \tfrac12\|\cdot\|_2^2$ this is the projected subgradient method.

On the unit simplex $\Delta = \{x \in \mathbb R^n : x \ge 0,\ \sum_j x_j = 1\}$ take the entropy $\psi_e(x) = \sum_j x_j \ln x_j$ (5.27), with $0\ln0 = 0$. SANP becomes the entropic descent algorithm (EDA):

$$x^{k+1}_j = \frac{x^k_j\,e^{-t_k f'_j(x^k)}}{\sum_{i=1}^n x^k_i\,e^{-t_k f'_i(x^k)}} .$$

Formalization targets

Goal: Theorem 5.1 (p. 174)

If $f$ is convex and $L_f$-Lipschitz on $\Delta$ for $\|\cdot\|_1$, with subgradients satisfying $\|f'(x)\|_\infty \le L_f$, and the EDA is started at $x^1 = n^{-1}e$ with step $t = \sqrt{2\ln n}/(L_f\sqrt k)$ for a horizon $k \ge 1$, then

$$\min_{1 \le s \le k} f(x^s) - \min_{x \in \Delta} f(x) \le \frac{\sqrt{2\ln n}\;L_f}{\sqrt k}.$$

The general estimate: Theorems 4.1 and 4.2 (pp. 171–172)

For any norm, any $\sigma$-strongly convex $\psi$ and any SANP run,

$$\min_{1 \le s \le k} f(x^s) - \min_X f \le \frac{B_\psi(x^*, x^1) + (2\sigma)^{-1}\sum_{s=1}^k t_s^2\|f'(x^s)\|_*^2}{\sum_{s=1}^k t_s},$$

and with the optimal constant step this gives $L_f\sqrt{2B_\psi(x^*, x^1)/\sigma}/\sqrt k$.

The milestones follow the paper's proof: the three-point identity (Lemma 4.1), the optimality condition (4.16), the lower bound $B_\psi \ge \tfrac\sigma2\|\cdot\|^2$, the one-step inequality (4.21), Theorem 4.1(a), Proposition 4.1 (optimal step), Theorem 4.2 and its version with an upper bound on $B_\psi(x^*, x^1)$; then for the simplex, the 1-strong convexity of $\psi_e$ for $\|\cdot\|_1$ (Proposition 5.1(a), Remark 5.1), the bound $B_{\psi_e}(x^*, n^{-1}e) \le \ln n$ (Proposition 5.1(c)), and the identification of the EDA with SANP.

Significance

The result shows that for nonsmooth convex minimisation over the simplex an explicit first-order method attains accuracy $\varepsilon$ in $O(L_f^2\ln n/\varepsilon^2)$ iterations, with $L_f$ measured in the $\ell_\infty$ dual norm. The general estimate of Theorem 4.2 applies to any norm and any strongly convex potential, and is the template for later analyses of mirror descent, its stochastic and online variants, and mirror-prox methods.

Formalizing the paper produces a norm-agnostic, machine-checked proof of the mirror descent efficiency estimate, in which subgradients are dual-space objects and the dual norm is explicit, and a verified link between the entropy, the $\ell_1$ geometry and the multiplicative-weights update. To our knowledge none of these statements is formalized; existing formal developments of online mirror descent work in Euclidean space with Legendre potentials and bound regret for linear losses, which is a different statement.

Difficulty

The algebra of Theorem 4.1 is short, but it rests on facts that are not available off the shelf. The first-order optimality condition (4.16) must be derived for a minimiser over a convex set without assuming the set has interior (the simplex has none in $\mathbb R^n$). The bound $B_\psi(u, y) \ge \tfrac\sigma2\|u - y\|^2$ must be obtained from the chord definition of strong convexity for an arbitrary norm. On the simplex, strong convexity of the entropy with respect to $\|\cdot\|_1$ is a form of Pinsker's inequality, and it must hold on the closed simplex, where the entropy is not differentiable at the boundary. Finally, the EDA must be shown to be the exact minimiser of the SANP subproblem over $\Delta$, which is a Gibbs variational principle. A tempting shortcut, working throughout in Euclidean space, fails: it changes the dual norm of the subgradients from $\ell_\infty$ to $\ell_2$ and the strong convexity constant of the entropy, and loses the $\ln n$ rate.

Formalization scope

Sections 3–4 live in a general real normed space; a subgradient is a continuous linear functional, $\langle u, f'(x)\rangle$ is its value at $u$, and $\|\cdot\|_*$ is the operator norm. $\nabla\psi$ is the Fréchet derivative. Iterates are indexed from $1$. A SANP run is a predicate on sequences: each step size is positive, each iterate lies in $X$, $\psi$ is differentiable there, and the next iterate minimises the SANP objective. This encodes the paper's standing assumption that SANP is well defined, and replaces "$X$ has nonempty interior" and "$x^1 \in \operatorname{int} X$". Section 5 works on $\mathbb R^n$ as functions $\{1, \dots, n\} \to \mathbb R$ with explicit $\ell_1$ and $\ell_\infty$ sums; $\operatorname{int}\Delta$ is the relative interior, and the entropy formula is evaluated on $\Delta$ only. "$\min_{1\le s\le k} f(x^s) - \min_X f \le R$" is stated as the existence of $s \in \{1, \dots, k\}$ with $f(x^s) - f(x^*) \le R$.

Added hypotheses, each disclosed in the item: a bound $\|f'(x)\|_* \le L_f$ on the oracle (used by the proofs of Theorems 4.1(b), 4.2 and 5.1, not implied by the Lipschitz condition for subgradients relative to $X$); $D^{-1}b > 0$ in Proposition 4.1, without which the proposition as printed is false; $L_f > 0$ in the step sizes. The step sizes of (4.23) and of the EDA are constant over a fixed horizon $k$, which is what the proof chooses; Theorem 5.1 is stated with $L_f$, since the free index in the printed bound (5.28) cannot be bound, and $L_f$ is what the proof yields.

Trivializing formalizations are ruled out: $B_\psi$ is never evaluated where fderiv is a junk value (the run requires differentiability at every iterate), the SANP step is never chosen by Classical.epsilon, the bound of Theorem 5.1 is not stated with a maximum of $\|f'(x^s)\|_\infty$ over the run, and the step is not an anytime schedule $t_s \propto 1/\sqrt s$.

A complete development needs first-order optimality conditions over convex sets, strong convexity and Bregman distances in normed spaces, Pinsker-type inequalities for finite distributions, and the Gibbs variational principle. These are reusable beyond this mission; proofs of any milestone, and general lemmas that serve several of them, are welcome.

Selected references

• A. Beck, M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Oper. Res. Lett. 31 (2003) 167–175. https://doi.org/10.1016/S0167-6377(02)00231-6
• A. Ben-Tal, T. Margalit, A. Nemirovski, The ordered subsets mirror descent optimization method with applications to tomography, SIAM J. Optim. 12 (2001) 79–108. https://doi.org/10.1137/S1052623499354564
• A. Nemirovsky, D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.
• G. Chen, M. Teboulle, Convergence analysis of a proximal-like minimization algorithm using Bregman functions, SIAM J. Optim. 3 (1993) 538–543. https://doi.org/10.1137/0803026