Convex Optimization

Motivation

Many problems in signal processing, statistics and machine learning take the form $\min_x \Phi(x)+\Psi(x)$, where $\Psi$ is smooth and $\Phi$ is convex but nonsmooth (a norm, the indicator of a constraint set). The forward-backward method takes a gradient step on $\Psi$ followed by a proximal step on $\Phi$. Its accelerated, inertial version — FISTA of Beck and Teboulle, built on Nesterov's method — reaches the rate $O(1/k^2)$ for the objective values. In practice the gradient or the proximal step is computed only approximately, so it matters whether the accelerated method survives errors, and whether its iterates converge at all, not only its objective values.

• 1983–2009. Nesterov introduces the accelerated gradient method with rate $O(1/k^2)$; Güler extends it to proximal steps; Beck and Teboulle publish FISTA (SIAM J. Imaging Sci. 2009). Convergence of the FISTA iterates themselves remains open.
• 2011. Schmidt, Le Roux and Bach show that the $O(1/k^2)$ value rate of accelerated proximal-gradient methods persists under errors that decay fast enough (NeurIPS 2011).
• 2014–2015. Su, Boyd and Candès read Nesterov's scheme as a discretization of $\ddot x+\frac{\alpha}{t}\dot x+\nabla\Phi(x)=0$ (JMLR 2016). Chambolle and Dossal prove weak convergence of the iterates when the inertial coefficient is $\frac{k-1}{k+\alpha-1}$ with $\alpha>3$, without errors (JOTA 2015).
• 2015. Attouch, Chbani, Peypouquet and Redont (this source) treat the dynamics and the algorithm together, and prove value rates and weak convergence of the iterates for the version with errors.

Setting

Let $\mathcal H$ be a real Hilbert space. Let $\Phi:\mathcal H\to\mathbb R\cup\{+\infty\}$ be proper, lower semicontinuous and convex, and let $\Psi:\mathcal H\to\mathbb R$ be convex and continuously differentiable, with gradient $\nabla\Psi$ Lipschitz continuous with constant $L$. Write $\Theta=\Phi+\Psi$ and $S=\operatorname{argmin}\Theta$.

The proximal map of $s\Phi$ ($s>0$) sends $x$ to the unique minimizer of $\xi\mapsto\Phi(\xi)+\frac1{2s}\|\xi-x\|^2$.

Fix $\alpha>0$, a step $s$ with $0<s<1/L$, and perturbations $g_k\in\mathcal H$. The perturbed inertial forward-backward algorithm (55) generates

$$y_k=x_k+\frac{k-1}{k+\alpha-1}(x_k-x_{k-1}),\qquad x_{k+1}=\operatorname{prox}_{s\Phi}\big(y_k-s(\nabla\Psi(y_k)-g_k)\big).$$

With $g_k=0$ and $\alpha=3$ this is FISTA. The analysis uses $z_k=\frac{k+\alpha-1}{\alpha-1}y_k-\frac{k}{\alpha-1}x_k$ and, for $x^*\in S$, the energy

$$\mathcal G(k)=\frac{2s}{\alpha-1}(k+\alpha-2)^2\big(\Theta(x_k)-\Theta(x^*)\big)+(\alpha-1)\|z_k-x^*\|^2 .$$

Formalization targets

Goal: Theorem 5.3

If $S\neq\emptyset$, $\alpha>3$, $0<s<1/L$ and $\sum_k k\|g_k\|<+\infty$, then

$$\sum_k k\big(\Theta(x_k)-\min\Theta\big)<\infty,\qquad \sum_k k\|x_{k+1}-x_k\|^2<\infty,\qquad x_k\rightharpoonup\bar x\ \text{ for some }\bar x\in S .$$

The goal makes no claim about rates of the iterates and no claim of strong convergence.

Value rate: Theorem 5.1

For $\alpha\ge3$, with an explicit constant $C$ depending on $x_0$, $y_0$, $x^*$ and $\sum_j(j+\alpha-1)\|g_j\|$,

$$\Theta(x_k)-\min\Theta\le\frac{C(\alpha-1)}{2s(k+\alpha-2)^2}.$$

Milestones

The proof's steps, in order: the proximal-gradient inequality (63); the energy step (66); the discrete Gronwall–Bellman Lemma A.9; the bound (68) on $\|z_k-x^*\|$; Theorem 5.1; the descent inequality (69); the velocity bound (72); the second-order inequality (80) for $h_k=\frac12\|x_k-x^*\|^2$; Lemma A.5; Opial's Lemma A.3.

Significance

The result. Theorem 5.3 gives convergence of the iterates of a FISTA-type method that tolerates computational error, and summability estimates that are stronger than the $O(1/k^2)$ value rate: $\sum_k k(\Theta(x_k)-\min\Theta)<\infty$ implies the rate $o(1/k^2)$ along the sequence. The summability condition $\sum_k k\|g_k\|<\infty$ is the discrete counterpart of $\int t\|g(t)\|\,dt<\infty$ for the perturbed dynamics, which makes the algorithm a faithful discretization of the continuous model studied in the same paper. For $\alpha=3$ (FISTA itself) convergence of the iterates was not known when the paper was written.

Formalizing it. The unperturbed case ($g_k\equiv0$) is already on Prove2Me and proved: the weak convergence theorem and the energy, descent and summability facts (namespace NesterovFB), and the proximal-gradient inequality, which this mission reuses as milestone (63). This mission poses the perturbed statements, which no existing item covers: the error terms change the energy step, require boundedness of $(z_k)$ through a Gronwall-type argument, and turn the Fejér-type estimate into an inhomogeneous one. The discrete Gronwall–Bellman and Opial lemmas are reusable well beyond this paper.

Difficulty

Without errors the energy $\mathcal G(k)$ is nonincreasing and every estimate follows from summing (66). With errors, (66) has the extra term $2s(k+\alpha-1)\langle g_k,z_{k+1}-x^*\rangle$, which can only be summed once $(z_k)$ is known to be bounded — and the bound on $z_k$ itself comes from the energy. The circularity is broken only by an implicit quadratic inequality and a discrete Gronwall–Bellman argument; a direct summation fails. The same issue reappears for the velocities, where (71) bounds $k^2\|x_{k+1}-x_k\|^2$ in terms of itself. Finally, weak convergence needs that $\lim\|x_k-x^*\|$ exists for every minimizer; for the inertial scheme $\|x_k-x^*\|$ is not monotone, and one must pass through the second-order inequality (80) and Lemma A.5 rather than a Fejér argument.

Formalization scope

$\mathcal H$ is a real inner product space, complete; nothing is finite-dimensional, and weak convergence is the published WeakTendsto ($\langle x_k,v\rangle\to\langle\bar x,v\rangle$ for every $v$), not norm convergence. $\Phi$ is EReal-valued with IsProperClosedConvex, and $\operatorname{prox}_{s\Phi}$ is a map $P$ with IsProx s Φ P (published definitions). $\Theta$ is the published NesterovFB.Rates.theta Φ Ψ; that definition names its arguments the other way round (nonsmooth first). $L$ is a nonnegative real and "$0<s<1/L$" is written $0<s$, $sL<1$. The algorithm is the predicate IsPerturbedRun on two sequences $x,y:\mathbb N\to\mathcal H$; $y_0$ is free, which covers every value of the unspecified $x_{-1}$. Series are Summable statements, sums such as $\sum_j(j+\alpha-1)\|g_j\|$ are tsums used only under the summability hypothesis.

Two printed statements are corrected as their proofs require. In Theorem 5.3 iii) the limit minimizes $\Phi+\Psi$ (the page says $\operatorname{argmin}\Phi$, the proof applies Opial's lemma with $S=\operatorname{argmin}(\Phi+\Psi)$). In Theorem 5.1 the constant uses $\sqrt{\mathcal G(0)/(\alpha-1)}$, the quantity the proof derives, instead of the printed $\sqrt{\mathcal E(0)/(\alpha-1)}$. Theorem 5.1 and (68) assume $\Phi(x_0)<+\infty$ so that the constant is a real number; Theorem 5.3 does not.

A trivializing formalization is ruled out: the step condition is $sL<1$ rather than $s<1/L$ (which is unsatisfiable for $L=0$ in Lean), and a sorry-free check confirms that $\Phi=\Psi=0$, $g=0$, $P=\mathrm{id}$ and constant sequences satisfy every hypothesis of the goal, so the hypotheses are jointly satisfiable.

Theorem numbers and pages are those of the Optimization Online preprint 5179 (October 2015), not of the Mathematical Programming typesetting. Welcome contributions: proofs of the appendix lemmas A.3, A.5, A.9 (independent of the algorithm), of (66) and (69) from the referenced inequality (63), and the chain (68) → Theorem 5.1, (72), (80) → Theorem 5.3.

Selected references

• H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing damping, Optimization Online preprint 5179, 2015. https://optimization-online.org/wp-content/uploads/2015/10/5179.pdf ; published as …asymptotic vanishing viscosity, Math. Program. 168 (2018). https://doi.org/10.1007/s10107-016-0992-8
• A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sci. 2 (2009). https://doi.org/10.1137/080716542
• A. Chambolle, Ch. Dossal, On the convergence of the iterates of the "fast iterative shrinkage/thresholding algorithm", J. Optim. Theory Appl. 166 (2015). https://doi.org/10.1007/s10957-015-0746-4
• W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, J. Mach. Learn. Res. 17 (2016). https://arxiv.org/abs/1503.01243
• M. Schmidt, N. Le Roux, F. Bach, Convergence rates of inexact proximal-gradient methods for convex optimization, NeurIPS 2011. https://arxiv.org/abs/1109.2415
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73 (1967). https://doi.org/10.1090/S0002-9904-1967-11761-0

Motivation

Learning with expert advice and online linear optimization over the probability simplex are the basic models behind boosting, multiplicative-weights methods for linear programming and zero-sum games, and adversarial bandit algorithms. The algorithm that solves them, under the names Weighted Majority, Hedge and Exponentiated Gradient (EG), keeps a probability vector over $d$ coordinates and multiplies each weight by $e^{-\eta z_t[i]}$ after observing the loss vector $z_t$.

• Littlestone and Warmuth (1994) introduced Weighted Majority for predicting with expert advice (doi:10.1006/inco.1994.1009).
• Freund and Schapire (1997) analysed the same update as Hedge, for losses in $[0,1]$ (doi:10.1006/jcss.1997.1504).
• Kivinen and Warmuth (1997) introduced Exponentiated Gradient as an online algorithm for linear prediction (doi:10.1006/inco.1996.2612).
• Beck and Teboulle (2003) identified the update as mirror descent with the entropy on the simplex (doi:10.1016/S0167-6377(02)00231-6).
• Shalev-Shwartz's survey (2011/2012) derives it as Online Mirror Descent with a normalized-entropy regularizer and proves, by Fenchel duality, a regret bound in which each round contributes a local norm of the loss vector instead of its sup norm (doi:10.1561/2200000018, §2.8).

The local-norm form is the one needed when loss vectors are large on coordinates of small weight, which is the situation of importance-weighted loss estimates in adversarial bandits.

Setting

Fix a dimension $d \ge 1$ and a learning rate $\eta > 0$. In round $t = 1, 2, \dots$ the learner plays a vector $w_t$ in the probability simplex $S = \{w \in \mathbb R^d : w \ge 0,\ \sum_i w[i] = 1\}$, then observes a loss vector $z_t \in \mathbb R^d$ and suffers the linear loss $\langle w_t, z_t\rangle$. Write $z_{1:t} = z_1 + \dots + z_t$.

Normalized EG starts from $w_1 = (1/d, \dots, 1/d)$ and updates

$$w_{t+1}[i] = \frac{w_t[i]\, e^{-\eta z_t[i]}}{\sum_j w_t[j]\, e^{-\eta z_t[j]}}, \qquad\text{equivalently}\qquad w_t[i] = \frac{e^{-\eta z_{1:t-1}[i]}}{\sum_j e^{-\eta z_{1:t-1}[j]}} .$$

Its regret against a comparator $u \in S$ after $T$ rounds is $\sum_{t=1}^T \langle w_t - u, z_t\rangle$.

The analysis is phrased for general Online Mirror Descent (OMD): given a link function $g$, predict $w_t = g(-z_{1:t-1})$. For a regularizer $R$ on a set $S$ (equal to $+\infty$ off $S$), the Fenchel conjugate is $R^\star(\theta) = \sup_{w\in S} (\langle w,\theta\rangle - R(w))$, and the Bregman divergence of a differentiable $F$ is $D_F(a\,\|\,b) = F(a) - F(b) - \langle \nabla F(b), a - b\rangle$. Normalized EG is OMD with $g = \nabla R^\star$ for the normalized entropy $R(w) = \frac1\eta\sum_i w[i]\log w[i]$ on $S$, whose conjugate is $R^\star(\theta) = \frac1\eta\log\sum_i e^{\eta\theta[i]}$ and whose gradient is the softmax.

Formalization targets

Goal: Theorem 2.22 (p. 153)

If $\eta z_t[i] \ge -1$ for all $t$ and $i$, then for every $T$ and every $u \in S$,

$$\sum_{t=1}^T \langle w_t - u, z_t\rangle \le \frac{\log d}{\eta} + \eta \sum_{t=1}^T \sum_{i=1}^d w_t[i]\, z_t[i]^2 .$$

The comparator is unquantified on the page; it ranges over the simplex $S$, the competing set of the normalized-entropy regularizer. The bound fails for $u$ outside $S$.

Milestones, in proof order

1. Lemma 2.20 (p. 150). OMD with link $g = \nabla R^\star$ satisfies, for every $u \in S$,

$$\sum_{t=1}^T \langle w_t - u, z_t\rangle \le R(u) - R(w_1) + \sum_{t=1}^T D_{R^\star}(-z_{1:t}\,\|\,-z_{1:t-1}),$$

with equality for a minimizer of $R(u) + \sum_t\langle u, z_t\rangle$ over $S$. 2. (2.16)–(2.18) (p. 153). For $R^\star(\theta) = \frac1\eta\log\sum_i e^{\eta\theta[i]}$, the gradient is the softmax, $w_t = \nabla R^\star(-z_{1:t-1})$, and

$$D_{R^\star}(-z_{1:t}\,\|\,-z_{1:t-1}) = \frac1\eta \log\Big(\sum_i w_t[i]\, e^{-\eta z_t[i]}\Big) + \langle w_t, z_t\rangle .$$

3. The per-round bound (pp. 153–154). If $\eta z_t[i] \ge -1$ for every $i$, then $D_{R^\star}(-z_{1:t}\,\|\,-z_{1:t-1}) \le \eta\sum_i w_t[i]\, z_t[i]^2$.

Significance

The result. Since $\sum_i w_t[i] z_t[i]^2 \le \|z_t\|_\infty^2$, Theorem 2.22 improves the standard bound $\log(d)/\eta + \eta\sum_t\|z_t\|_\infty^2$ of normalized EG. The improvement matters when a coordinate with tiny weight carries a huge loss: the local norm weights that loss by its probability. This is what gives the $O(\sqrt{dT\log d})$ regret of Exp3-type bandit algorithms, whose loss estimates are of order $1/w_t[i]$. The theorem allows negative losses down to $-1/\eta$, so it also applies to gains and to centred or shifted losses.

Formalizing it. The theorem is proved in the survey; no machine-checked proof of it is known. The platform has a proved Hedge bound for non-negative losses compared with a single expert (Hazan, Introduction to Online Convex Optimization, Theorem 1.5). It does not imply Theorem 2.22: the latter allows negative losses, and its local-norm term is not invariant under shifting $z_t$ by a constant vector, so the shift that reduces signed losses to non-negative ones changes the bound. Lemma 2.20 is a general duality identity for OMD and is reusable for every OMD instance (Euclidean, $p$-norm, unnormalized entropy).

Difficulty

The obvious argument for Hedge tracks the potential $\log\sum_i e^{-\eta z_{1:t}[i]}$ and bounds the one-step increase using $e^{-a} \le 1 - a + a^2/2$ for $a \ge 0$. With negative losses that inequality fails. The weaker form $e^{-a} \le 1 - a + a^2$ is valid only for $a \ge -1$, which is where the hypothesis $\eta z_t[i] \ge -1$ comes from. The bound is also stated against the whole simplex, not against single experts, so the potential argument has to be combined with an entropy bound for a general comparator.

Formalization scope

• Vectors are Fin d → ℝ, with 0 < d and 0 < η. Rounds are numbered from $0$ in Lean, so index $t$ is the paper's round $t+1$ and sums over rounds run over Finset.range T.
• The algorithm is the published definition UnderstandingML.wmWeights η z t (reference item UnderstandingML_Online), which is exactly the closed form of normalized EG for arbitrary real loss vectors; wmWeights η z 0 is the uniform vector $w_1$.
• The comparator in the goal ranges over the probability simplex (0 ≤ u i, ∑ i, u i = 1). A statement over all $u \in \mathbb R^d$ is false, and a statement over vertices only would be the weaker expert bound; both are ruled out.
• $\log$ is the natural logarithm; all its arguments in the statements are positive.
• Lemma 2.20 is stated on a real Hilbert space $E$ with a real-valued $R$ and a set $S$. "$g = \nabla R^\star$" is three hypotheses: $g$ maps into $S$, $g(\theta)$ attains the supremum defining $R^\star(\theta)$, and $R^\star$ has gradient $g(\theta)$ at $\theta$. Differentiability of $R^\star$ is the paper's consequence of Lemma 2.19, which is cited to the literature and is assumed here. These hypotheses are satisfiable; a sorry-free check on $E = \mathbb R$ with $R(w) = w^2/2$ accompanies the draft.
• The Bregman divergence of the log-sum-exp conjugate on $\mathbb R^d$ is written with explicit coordinate sums, and its gradient is stated as a Fréchet derivative, because Fin d → ℝ carries the sup norm in Mathlib.
• The theorem has no $O(\cdot)$; all constants are the paper's.
• Not included: Theorem 2.15 and Corollary 2.16 (the $\|z_t\|_\infty^2$ bound via strong convexity), Theorem 2.21 (which rests on Lemma 2.19), Theorem 2.23 (unnormalized EG, in the Winnow mission of this series), Theorem 3.1 and Corollary 4.2.

Welcome contributions: proofs of the three milestones and of the goal, and general Mathlib-style lemmas on the gradient of log-sum-exp and on the Fenchel–Young inequality for conjugates defined as suprema over a set.

Selected references

• S. Shalev-Shwartz, Online Learning and Online Convex Optimization, Foundations and Trends in Machine Learning 4(2), 107–194, 2011 (© 2012). doi:10.1561/2200000018
• J. Kivinen and M. K. Warmuth, Exponentiated gradient versus gradient descent for linear predictors, Information and Computation 132(1), 1–63, 1997. doi:10.1006/inco.1996.2612
• Y. Freund and R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, Journal of Computer and System Sciences 55(1), 119–139, 1997. doi:10.1006/jcss.1997.1504
• N. Littlestone and M. K. Warmuth, The weighted majority algorithm, Information and Computation 108(2), 212–261, 1994. doi:10.1006/inco.1994.1009
• A. Beck and M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3), 167–175, 2003. doi:10.1016/S0167-6377(02)00231-6
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., MIT Press, 2022. arXiv:1909.05207

Motivation

Online convex optimization is a repeated game between a learner and an environment. In each round the learner commits to a vector, the environment then reveals a convex loss function, and the learner pays the loss of its vector. No statistical assumption is made about how the losses are generated; they may be chosen adversarially. Performance is measured against the best fixed vector in hindsight. This model underlies online prediction with expert advice, online regression and classification, portfolio selection, and the analysis of stochastic gradient methods through online-to-batch conversion.

Shai Shalev-Shwartz's survey Online Learning and Online Convex Optimization (Foundations and Trends in Machine Learning, 2011/2012) organizes most first-order online algorithms around a single template, Follow-the-Regularized-Leader (FoReL), and derives their regret bounds from one theorem: Theorem 2.11 (p. 138). Online gradient descent, the experts algorithm with exponential weights, and the bounds of Sections 2.6–2.8 of the survey are instances of it. This mission formalizes that theorem and the lemmas its proof rests on.

Timeline. Follow-the-Leader goes back to Hannan (1957) and the "be the leader" argument appears in Kalai and Vempala (2005). Regularized variants and their analysis via strong convexity were developed by Shalev-Shwartz and Singer (2007) and by Abernethy, Hazan and Rakhlin (2008); the survey (2011) presents the strong-convexity analysis in the form formalized here.

Setting

Let $E$ be a real normed space with norm $\|\cdot\|$ and $S \subseteq E$ a set of admissible predictions. Rounds are numbered $t = 1, 2, \dots$. In round $t$ the learner predicts $w_t \in S$, receives a loss function $f_t : S \to \mathbb R$, and suffers $f_t(w_t)$. The regret after $T$ rounds with respect to a competing vector $u \in S$ is (eq. (2.1))

$$\mathrm{Regret}_T(u) = \sum_{t=1}^{T} f_t(w_t) - \sum_{t=1}^{T} f_t(u).$$

Given a regularization function $R : S \to \mathbb R$, Follow-the-Regularized-Leader predicts

$$w_t \in \operatorname*{argmin}_{w \in S} \Big( \sum_{i=1}^{t-1} f_i(w) + R(w) \Big), \qquad t \ge 1,$$

with ties broken arbitrarily; in particular $w_1$ minimizes $R$ over $S$. With $R = 0$ this is Follow-the-Leader (FTL).

A function $f$ is $L$-Lipschitz over $S$ if $|f(u) - f(v)| \le L\|u - v\|$ for all $u, v \in S$. A function $R$ is $\sigma$-strongly-convex over a convex set $S$ if, for all $x, y \in S$ and $a, b \ge 0$ with $a + b = 1$,

$$R(a x + b y) \le a R(x) + b R(y) - a b\, \frac{\sigma}{2} \|x - y\|^2 .$$

Formalization targets

Goal: Theorem 2.11

Let $f_1, \dots, f_T$ be convex on $S$, with $f_t$ $L_t$-Lipschitz over $S$, and let $\frac1T \sum_{t=1}^T L_t^2 \le L^2$. If FoReL is run with a regularizer $R$ that is $\sigma$-strongly-convex over $S$ ($\sigma > 0$) with respect to the same norm, then for all $u \in S$

$$\mathrm{Regret}_T(u) \le R(u) - \min_{v \in S} R(v) + \frac{T L^2}{\sigma}.$$

Milestones, in the order the proof uses them

1. Lemma 2.1 (p. 125). FTL satisfies $\mathrm{Regret}_T(u) \le \sum_{t=1}^T (f_t(w_t) - f_t(w_{t+1}))$. Already proved on the platform as LogRegretOCO.FTAL.ftl_be_the_leader and referenced here.
2. Lemma 2.3 (p. 128). For arbitrary $f_t$ and $R$, FoReL satisfies

$$\sum_{t=1}^T (f_t(w_t) - f_t(u)) \le R(u) - R(w_1) + \sum_{t=1}^T (f_t(w_t) - f_t(w_{t+1})).$$

3. Lemma 2.8 (p. 135). If $f$ is $\sigma$-strongly-convex over $S$ and $w$ minimizes $f$ over $S$, then $f(u) - f(w) \ge \frac{\sigma}{2}\|u - w\|^2$ for all $u \in S$.
4. Equation (2.7) (p. 138). Under the hypotheses of Lemma 2.10 without Lipschitzness, $\sigma\|w_t - w_{t+1}\|^2 \le f_t(w_t) - f_t(w_{t+1})$.
5. Lemma 2.10 (p. 137). If $f_t$ is $L_t$-Lipschitz, then $f_t(w_t) - f_t(w_{t+1}) \le L_t\|w_t - w_{t+1}\| \le L_t^2/\sigma$.

Significance

Theorem 2.11 is the result from which the survey's concrete regret bounds are read off. With the Euclidean regularizer $R(w) = \frac{1}{2\eta}\|w\|_2^2$ it gives the bound $\frac{1}{2\eta}\|u\|_2^2 + \eta T L^2$ of online gradient descent (Corollary 2.12), hence $O(\sqrt T)$ regret after tuning $\eta$; with the entropic regularizer over the probability simplex and the $\ell_1$ norm it gives the $\sqrt{2 \log(d)\, T}$-type bounds for prediction with expert advice (Corollaries 2.13–2.14). Through online-to-batch conversion such regret bounds become excess-risk bounds for stochastic optimization.

The survey's proofs are complete, so the formalization adds no new mathematics; it produces machine-checked versions of the FoReL regret theorem, of the stability lemma, and of the quadratic-growth property of strongly convex functions over a general normed space and a general convex constraint set. To our knowledge none of these is in Mathlib. The platform already has the FTL lemma over $\mathbb R^n$ (proved) and the special case of Lemma 2.8 with $S = E$ and the Euclidean norm (UnderstandingML.strongly_convex_lemma, part 3); the general statements are new here.

Difficulty

Lemma 2.3 and Lemma 2.1 use different round indexings (FoReL's regularizer plays the role of a round-zero loss), so Lemma 2.1 cannot be applied verbatim. The main obstacle is Lemma 2.8 on a constrained set without differentiability: the obvious argument sets the gradient at the minimizer to zero, which is unavailable when $R$ is not differentiable or the minimizer lies on the boundary of $S$. A second point is that the strong convexity of $\sum_{i<t} f_i + R$ must be derived from the convexity of the $f_i$ on $S$, not on all of $E$, and from the strong convexity of $R$ on $S$.

Formalization scope

Conventions committed to in the Lean statements:

• The carrier is an arbitrary real normed space E (NormedAddCommGroup E, NormedSpace ℝ E); no inner product is assumed. Every norm on $\mathbb R^d$, including $\ell_1$ as used in Corollary 2.14, is an instance. The Lipschitz and the strong-convexity hypotheses use the one norm of E, as the theorem requires ("the same norm").
• Strong convexity is Mathlib's StrongConvexOn S σ R, the modulus $\frac{\sigma}{2}r^2$ form above. The survey's Definition 2.4 is stated with subgradients and a pairing $\langle z, u - w\rangle$; the two agree for convex functions that have subgradients on $S$, and the Mathlib form needs neither a dual space nor subgradients. With this choice Lemma 2.8 is a genuine lemma, not an unfolding of the definition.
• Losses and regularizer are real-valued functions on E, of which only the values on S matter; convexity is ConvexOn ℝ S. The survey's convention $R = \infty$ outside $S$ is the constraint $w_t \in S$.
• Rounds are 1-based; w 0 and f 0 are unused. A FoReL run is a predicate on the whole trajectory (IsFoReLRun), so every tie-breaking rule gives a run, and no argmin is chosen.
• Convexity and Lipschitzness are assumed for the rounds $1, \dots, T$ (Theorem 2.11) or $1, \dots, t$ (Lemma 2.10, (2.7)), not for all rounds.
• $\min_{v \in S} R(v)$ is written sInf (R '' S). It is attained at $w_1$ whenever a run exists, so it is the true minimum, not a default value. The hypothesis $T \ge 1$ is present only because of the factor $1/T$.
• No $O(\cdot)$ appears in any statement of this mission; every bound is the explicit one on the page.
• Erratum: the proof of Lemma 2.10 ends with "$\|w_t - w_{t+1}\| \le L/\sigma$", a misprint for $L_t/\sigma$. The lemma's statement is correct and is formalized as printed, with both inequalities of the chain.

A trivializing formalization would make the run predicate unsatisfiable, so that Theorem 2.11 holds vacuously; the drafted predicate is satisfied by online gradient descent with $R(w) = \frac{1}{2\eta}w^2$ on $\mathbb R$ (Example 2.3), and that regularizer is $(1/\eta)$-strongly convex, so the hypotheses of the goal are jointly satisfiable.

Out of scope, and welcome as follow-up work: the derived bounds (Corollaries 2.12–2.14), Theorem 2.15 (which needs dual norms), Lemma 2.9, Corollary 2.2 and the doubling trick. Contributions of general lemmas — strong convexity of a convex plus strongly convex function on a set, quadratic growth at a constrained minimizer — are reusable well beyond this mission.

Selected references

• S. Shalev-Shwartz, Online Learning and Online Convex Optimization, Foundations and Trends in Machine Learning 4(2) (2011) 107–194. https://doi.org/10.1561/2200000018
• J. Hannan, Approximation to Bayes risk in repeated play, Contributions to the Theory of Games III, Annals of Mathematics Studies 39 (1957) 97–139. https://doi.org/10.1515/9781400882151-006
• A. Kalai, S. Vempala, Efficient algorithms for online decision problems, Journal of Computer and System Sciences 71(3) (2005) 291–307. https://doi.org/10.1016/j.jcss.2004.10.016
• S. Shalev-Shwartz, Y. Singer, A primal-dual perspective of online learning algorithms, Machine Learning 69 (2007) 115–142. https://doi.org/10.1007/s10994-007-5014-x
• J. Abernethy, E. Hazan, A. Rakhlin, Competing in the dark: an efficient algorithm for bandit linear optimization, COLT 2008. https://www.learningtheory.org/colt2008/papers/123-Abernethy.pdf
• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007) 169–192. https://doi.org/10.1007/s10994-007-5016-8

Motivation

Stochastic gradient descent (SGD) is the standard method for minimizing an expected loss $F(w) = \mathbb E_z[\ell(w, z)]$ when only noisy gradients are available: in machine learning, $w$ is a predictor, $z$ a random example, and each step uses the gradient of the loss on one fresh example. When $F$ is strongly convex, as for regularized learning problems such as the SVM, the minimax-optimal error after $T$ oracle calls is of order $1/T$. Rakhlin, Shamir and Sridharan (arXiv:1109.5647, ICML 2012) asked whether plain SGD attains this rate, or whether the $O(\log T/T)$ bound known for averaged SGD is the truth.

Their §3 settles the case where $F$ is in addition smooth at its minimizer: both the last iterate and the average of all iterates attain $O(1/T)$, with explicit constants. This mission formalizes that section.

Timeline of the relevant bounds:

• 2007–2009. Hazan, Agarwal and Kale (doi:10.1007/s10994-007-5016-8) show $O(\log T)$ regret for online gradient descent on strongly convex losses, which by online-to-batch conversion gives $O(\log T/T)$ for the averaged SGD iterate.
• 2009. Nemirovski, Juditsky, Lan and Shapiro (doi:10.1137/070704277) give an $O(1/T)$ bound for the last iterate when $F$ is strongly convex and smooth.
• 2011. Hazan and Kale (arXiv:1006.2425) obtain $O(1/T)$ for strongly convex, possibly non-smooth $F$ with a modified algorithm.
• 2012. Rakhlin, Shamir and Sridharan prove the $O(1/T)$ bounds of this mission for SGD under smoothness at the optimum only, show the $\log T$ is real for averaged SGD on non-smooth problems, and recover $O(1/T)$ with suffix averaging.

Setting

Let $W \subseteq \mathbb R^d$ be a closed convex set containing $0$, let $F : \mathbb R^d \to \mathbb R$, and let $D$ be a probability distribution on a measurable space $\mathcal Z$.

• $F$ is $\lambda$-strongly convex on $W$, $\lambda > 0$: for all $w, w' \in W$ and every subgradient $g$ of $F$ at $w$, $F(w') \ge F(w) + \langle g, w' - w\rangle + \frac{\lambda}{2}\|w' - w\|^2$ (equation (1)).
• $F$ attains its minimum over $W$ at $w^* \in W$.
• A stochastic subgradient oracle is a measurable map $g : \mathbb R^d \times \mathcal Z \to \mathbb R^d$ such that, for every $w \in W$, the mean $\mathbb E_{z \sim D}[g(w, z)]$ is a subgradient of $F$ at $w$ relative to $W$, and $\mathbb E_{z\sim D}\|g(w,z)\|^2 \le G^2$.
• $F$ is $\mu$-smooth with respect to $w^*$ if

$$F(w) - F(w^*) \le \frac{\mu}{2}\|w - w^*\|^2 \qquad \text{for all } w \in W. \tag{2}$$

Projected SGD with step sizes $\eta_t = 1/(\lambda t)$ starts at $w_1 = 0$, draws $z_1, z_2, \dots \sim D$ independently and sets

$$w_{t+1} = \Pi_W\big(w_t - \eta_t\, g(w_t, z_t)\big),$$

where $\Pi_W$ is the Euclidean projection onto $W$. The averaged iterate is $\bar w_T = (w_1 + \dots + w_T)/T$. In Lean the run is UnderstandingML.sgdStrongIterates lam W g S and the average UnderstandingML.sgdStrongAverage lam W g S, for a sample S : Fin T → Z drawn from UnderstandingML.iidLaw D T.

Formalization targets

Goal: Theorem 2 (averaged iterate)

If $F$ is $\lambda$-strongly convex and $\mu$-smooth with respect to $w^*$, then for every $T \ge 1$

$$\mathbb E\big[F(\bar w_T) - F(w^*)\big] \le \frac{16\,\mu G^2}{\lambda^2 T}.$$

Milestones

1. Lemma 2. If $\mathbb E\|g(w,z)\|^2 \le G^2$ at a point $w \in W$, then $\|w - w^*\|^2 \le 4G^2/\lambda^2$.
2. Lemma 1. For every $T \ge 1$, $\mathbb E\|w_T - w^*\|^2 \le 4G^2/(\lambda^2 T)$, without smoothness.
3. Theorem 1 (last iterate). Under smoothness, $\mathbb E[F(w_T) - F(w^*)] \le 2\mu G^2/(\lambda^2 T)$.
4. Averaged-iterate distance (App. B.3). For every $T \ge 1$, $\mathbb E\|\bar w_T - w^*\|^2 \le 32G^2/(\lambda^2 T)$, without smoothness.

The constants are the paper's. Theorem 1 is a companion of the goal rather than a step of its proof; both rest on Lemma 1.

Significance

The result. Theorem 2 shows that the $\log T$ factor in the standard bound for averaged SGD is not needed when $F$ grows at most quadratically away from its minimizer. Condition (2) holds for logistic and least-squares regression and, in general, for linear predictors with losses that have Lipschitz-continuous gradients. Together with the paper's Theorem 4, which shows that the $\log T$ factor is unavoidable for averaged SGD on some non-smooth problems, it locates where the extra logarithm comes from. Lemma 1 is the paper's key lemma: an $O(1/T)$ bound on the expected squared distance of the last iterate that needs no smoothness, and it is reused in the paper's suffix-averaging analysis.

Formalizing it. All results are proved in the paper; none is formalized. The platform has UnderstandingML.sgd_strongly_convex (Shalev-Shwartz and Ben-David, Theorem 14.11), the classical $(\rho^2/(2\lambda T))(1 + \log T)$ bound for the same averaged iterate without smoothness. This mission adds the $O(1/T)$ bounds under (2), on the same SGD run, together with a reusable expected-distance bound for the projected iterates.

Difficulty

The obvious route to Theorem 2 is to apply smoothness to each iterate, use Lemma 1, and average: by Jensen, $\mathbb E[F(\bar w_T)] - F(w^*) \le \frac{1}{T}\sum_t \frac{2\mu G^2}{\lambda^2 t}$, which is of order $\log T/T$. Removing the logarithm requires controlling $\mathbb E\|\bar w_T - w^*\|^2$ directly, where the iterates are dependent and the cross terms $\mathbb E\langle \bar w_t - w^*, w_{t+1} - w^*\rangle$ do not vanish. The resulting recursion is nonlinear in $\mathbb E\|\bar w_t - w^*\|^2$, and an induction with the constant $32$ fails at its first step unless the base case uses the sharper bound of Lemma 2. On the formal side, the expectations are over the product of $T$ independent samples, and each one-step argument needs the independence of $z_t$ from $w_t$ and the measurability of the projected iterates.

Formalization scope

• Space. The paper's Hilbert space is specialized to $\mathbb R^d$ with the Euclidean norm (UnderstandingML.Vec d).
• Domain. Convex ℝ W, IsClosed W (so the projection exists; tacit in the paper) and 0 ∈ W (the paper's initialization).
• Strong convexity is Mathlib's StrongConvexOn W lam F with 0 < lam. Combined with relative subgradients, it gives (1).
• Oracle. OptimalSGD.Suffix.IsSubgradientOracleOn W F D g (the series' shared oracle predicate): for $w \in W$, g w is integrable and its mean is a subgradient of $F$ at $w$ relative to $W$. Measurable (Function.uncurry g) and a probability measure $D$ are assumed. The second-moment bound holds at every $w \in W$, which is the paper's "regardless of how the iterates evolve".
• Smoothness is (2) exactly (IsSmoothWrt W F μ wstar), with $\mu \ge 0$. It is not a Lipschitz-gradient assumption, and $F$ need not be differentiable.
• Indexing. Iterates are indexed from $0$. The paper's $w_T$ is sgdStrongIterates lam W g S (T - 1), and $\bar w_T$ averages indices $0,\dots,T-1$. Statements quantify over $T \ge 1$, including $T = 1$ ($\bar w_1 = w_1 = 0$).
• Expectations. Bounds on $\|\cdot\|^2$ use the lower Lebesgue integral. Bounds on $F$ use the Bochner integral, and the integrability of $F(w_T)$ or $F(\bar w_T)$ is part of the conclusion.

A statement whose Bochner integral is not shown to be integrable would hold vacuously, because non-integrable functions integrate to $0$; the integrability conjuncts rule this out. The run and the average are the published Understanding Machine Learning definitions, so the bounds here apply to the same object as UnderstandingML.sgd_strongly_convex.

Needed infrastructure: measurability of the projected iterates in the sample, independence of $z_t$ from $w_t$ under the product measure, conditional unbiasedness of the oracle along the run, non-expansiveness of the projection (available as UnderstandingML.projection_lemma), and an elementary induction on the scalar recursions. Contributions of these as standalone lemmas are welcome, and they are reusable for mission 1 of this series (suffix averaging) and for other projected-SGD analyses.

Selected references

• A. Rakhlin, O. Shamir, K. Sridharan, Making Gradient Descent Optimal for Strongly Convex Stochastic Optimization, ICML 2012; arXiv:1109.5647v7. https://arxiv.org/abs/1109.5647
• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69, 2007. https://doi.org/10.1007/s10994-007-5016-8
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM J. Optim. 19(4), 2009. https://doi.org/10.1137/070704277
• E. Hazan, S. Kale, Beyond the regret minimization barrier: an optimal algorithm for stochastic strongly-convex optimization, COLT 2011; arXiv:1006.2425. https://arxiv.org/abs/1006.2425
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, §14.4.4. https://doi.org/10.1017/CBO9781107298019

Motivation

Karmarkar's projective method (1984) was the first interior-point algorithm for linear programming with a polynomial bound that was also fast in practice. Its analysis rests on a potential function that combines the logarithm of the objective gap with a logarithmic barrier: if every iteration lowers the potential by a fixed constant, then the gap shrinks geometrically. Nesterov and Nemirovskii (1994, §4.3) carried the method over to general convex cones with self-concordant barriers, but only with short steps, which move a fraction of the way to the boundary of a ball in the local norm.

Nesterov and Todd (1997) introduced self-scaled barriers, the class behind the cones of linear, second-order cone and semidefinite programming. They used it to allow long steps, which go a large fraction of the way to the boundary of the cone itself. Section 7.1 of that paper analyses the Karmarkar method with long steps on a self-scaled cone. It shows that the potential decrease per iteration is at least the absolute constant $1-\ln 2$, independent of the barrier parameter, as in the linear-programming case. This mission formalizes that analysis.

Timeline:

• 1984, Karmarkar: projective method for linear programming, with potential decrease per step bounded below by a constant.
• 1986, Anstreicher: a strengthened acceptance criterion for approximate projections in Karmarkar's algorithm for standard linear programming, containing the result that Lemma 7.1 of the 1997 paper generalizes (p. 28).
• 1994, Nesterov–Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, §4.3: the extension to self-concordant barriers on general cones, short steps.
• 1997, Nesterov–Todd: self-scaled barriers and long steps (this paper, Theorem 7.2).

Setting

Let $E=\mathbb R^n$ with inner product $\langle\cdot,\cdot\rangle$, which identifies the dual space $E^*$ with $E$. Let $K\subseteq E$ be a closed convex cone with nonempty interior that contains no line, and let $K^*=\{s:\langle s,x\rangle\ge0\ \forall x\in K\}$ be its dual cone. A $\nu$-self-scaled barrier $F:\operatorname{int}K\to\mathbb R$ is a self-concordant barrier that is logarithmically homogeneous, $F(\tau x)=F(x)-\nu\ln\tau$, and satisfies the two scaling conditions of Definition 2.1 of the paper. $F'$ and $F''$ are its gradient and Hessian.

Two measures of a direction $p\in E$ at $x\in\operatorname{int}K$ are used:

• the local norm $\|p\|_x=\langle F''(x)p,p\rangle^{1/2}$;
• the σ-measure $\sigma_x(p)=\min\{\beta\ge0:\beta x-p\in K\}$, and the uniform norm $|p|_x=\max\{\sigma_x(p),\sigma_x(-p)\}$.

The point $x-\alpha p$ stays in $\operatorname{int}K$ exactly when $\alpha\,\sigma_x(p)<1$.

The problem is in Karmarkar form:

$$(P)\qquad\min\ \langle c,x\rangle\quad\text{s.t.}\quad Bx=0,\ \ \langle d,x\rangle=1,\ \ x\in K,$$

with $B:E\to\mathbb R^m$ linear and surjective and $d\in K^*$. Its dual is $\max\{\zeta: B^*y+d\zeta+s=c,\ s\in K^*\}$. The standing assumptions are that (P) and the dual have strictly feasible points, and that $\langle c,\cdot\rangle$ is not constant on the feasible set of (P). The optimal value is $\zeta^*$. The method decreases the potential

$$\Phi(x;\zeta)=\nu\ln\langle c-\zeta d,x\rangle+F(x),$$

which is homogeneous of degree $0$ in $x$.

One iteration starts from a strictly feasible $\hat x$ and a lower bound $\hat\zeta\le\zeta^*$:

1. Put $\hat c=c+\frac{\langle c,\hat x\rangle}{\nu}F'(\hat x)$ and $\hat d=d+\frac{\langle d,\hat x\rangle}{\nu}F'(\hat x)$. Let $p(c)$, $p(d)$ be their projections into $\ker B$ with respect to $F''(\hat x)$: $Bp(u)=0$ and $B^*y(u)+F''(\hat x)p(u)=\hat u$ (7.3).
2. Put $\tilde x(\zeta)=\frac{\langle c-\zeta d,\hat x\rangle}{\nu}\hat x+p(c)-\zeta p(d)$ (7.4). If $\tilde x(\hat\zeta)\notin\operatorname{int}K$, keep $\zeta^+=\hat\zeta$. Otherwise raise the bound to $\zeta^+=\hat\zeta+1/\sigma_{\tilde x(\hat\zeta)}(p(d)+\hat x/\nu)$ (7.6).
3. Take the direction $p=p(c)-\zeta^+p(d)$ (7.5) and the new point $x^+=\hat x-\alpha p$.

Formalization targets

Goal: Theorem 7.2 (p. 28)

For a suitable $\alpha>0$, the point $x^+=\hat x-\alpha p$ lies in $\{x\in\operatorname{int}K:Bx=0\}$ and

$$\Phi(x^+;\zeta^+)\le\Phi(\hat x;\hat\zeta)-\frac{\|p\|_{\hat x}^2}{|p|_{\hat x}^2}(1-\ln2)\le\Phi(\hat x;\hat\zeta)-(1-\ln2).\qquad(7.9)$$

The goal asserts the existence of the step, not a particular step size, so it does not commit to the step chosen in the proof.

Milestones

• Lemma 7.1 (p. 27): $\zeta^+\le\zeta^*$, and $\langle c,\hat x\rangle-\zeta^+\le\nu\,\sigma_{\hat x}(-p)$ (7.7).
• (7.8) (p. 28): $\|p\|_{\hat x}^2=\langle c-\zeta^+d,p\rangle$.

Companion: Theorem 7.1 (p. 26)

With $\bar K=\{x\in K:Bx=0,\ \langle c,x\rangle\le\max(\langle c,x_0\rangle,0)+1,\ \langle d,x\rangle\le1\}$ and $\underline F$ the minimum of $F$ over it: if $\Phi(x;\zeta)\le\Phi(x_0;\zeta_0)-\Delta$ with $\zeta\in[\zeta_0,\zeta^*]$ and $\Delta$ large enough, then

$$\langle c,x\rangle-\zeta\le(\langle c,x_0\rangle-\zeta_0)\,e^{(F(x_0)-\underline F)/\nu}\,e^{-\Delta/\nu}.\qquad(7.2)$$

Significance

Theorem 7.2 together with Theorem 7.1 gives the $O(\nu\ln(1/\epsilon))$ iteration bound of the long-step conic Karmarkar method. The decrease constant $1-\ln2$ does not depend on $\nu$ or on the cone. The finer bound $\frac{\|p\|^2}{|p|^2}(1-\ln 2)$ can be much larger than $1-\ln 2$, since $\|p\|_x\ge|p|_x$ always holds. This explains why long steps outperform short ones in practice. Lemma 7.1 shows that the lower bound obtained from dual information is valid and tight enough to drive the analysis. The paper presents it as a generalization of a result of Anstreicher (1986) for standard linear programming.

The results are proved in the paper; none of them is formalized anywhere. A formal development checks the interplay of the lower-bound update with the σ-measure and the homogeneity of $\Phi$, which the paper treats briefly. It also records a correction: on p. 27 the paper prints $\hat c=c-\frac{\langle c,\hat x\rangle}{\nu}F'(\hat x)$ (and likewise $\hat d$). The paper's own surrounding identities, in particular $\langle\hat u,\hat x\rangle=0$ on p. 28, require the sign "$+$", and the formalization uses "$+$".

Difficulty

The obvious argument bounds the change of $F$ along $x-\alpha p$ with self-concordance in the local norm. That argument only controls steps with $\alpha\|p\|_{\hat x}<1$, and it gives a decrease that degrades with the step length. The long step goes up to $1/\sigma_{\hat x}(p)$, which can be much larger. Reaching it requires the long-step barrier bound for self-scaled barriers (Theorem 4.2 of the paper, stated in another mission of this series). That bound controls $F(x-\alpha p)$ through $\sigma_x(p)$ instead of $\|p\|_x$.

The second obstacle is the linear term. The decrease in $\nu\ln\langle c-\zeta^+d,\cdot\rangle$ must be compared with $\|p\|^2$, which needs both the identity (7.8) and the gap bound (7.7). The gap bound is the step at which the lower-bound update is essential: without the update, $\langle c,\hat x\rangle-\hat\zeta$ is not bounded by $\nu\sigma_{\hat x}(-p)$.

Formalization scope

The Lean development reuses the published self-scaled setting of the series SelfScaledIPM (IsProperCone, IsSelfScaledBarrier, hess, lnorm, sigma, absn) and ConvexOptimization.dualCone. Conventions:

• $E=$ EuclideanSpace ℝ (Fin n), with $E^*$ identified with $E$.
• $F''$ is assumed nondegenerate on $\operatorname{int}K$. This follows from the other axioms for a pointed cone.
• The conjugate barrier is a supremum over $\operatorname{int}K$.
• $\nu\ge1$ is a binder. The paper derives it from pointedness on p. 3.
• $\zeta^*$ is a real infimum, made finite by the strict dual feasibility assumption, which every statement carries. Nonconstancy of the objective is stated as the existence of two feasible points with different objective values.
• The projections $p(c)$, $p(d)$ are data satisfying (7.3), not chosen by a selection function. The lower-bound update and the direction are definitions computed from them.
• The goal adds the conjunct $\langle c-\zeta^+d,x^+\rangle>0$, so that the logarithm in $\Phi(x^+;\zeta^+)$ is genuine. It does not assert $\langle d,x^+\rangle=1$, which the paper notes may fail.
• Identity (7.8) is stated for every real $\zeta$, which contains the page's $\zeta=\zeta^+$.
• $\underline F$ is an infimum over $\bar K\cap\operatorname{int}K$, where the barrier is finite.
• $\hat c$ and $\hat d$ carry the corrected sign "$+$".

A statement with $\zeta^+$ an arbitrary real, or with $p$ an arbitrary vector, would be false or vacuous. The statements here fix both by the page's construction (7.3)–(7.6), and the logarithm in $\Phi$ is guarded by the positivity conjunct.

A proof needs the long-step barrier inequality (Theorem 4.2), the monotonicity facts of Proposition 4.1, $K^*=F''(v)K$ (Theorem 3.1 (iii)), and $\|p(u)\|^2_w=\langle u,p(u)\rangle$ (Proposition 6.2). These are milestones of the other missions of this series, and contributions proving them are reusable here. Elementary facts about $\sigma$ (positive homogeneity, the boundary characterization $x-\alpha p\in\partial K$ at $\alpha=1/\sigma_x(p)$) are useful beyond this mission.

Selected references

• Yu. E. Nesterov and M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Mathematics of Operations Research 22(1), 1997, 1–42. https://doi.org/10.1287/moor.22.1.1
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, 373–395. https://doi.org/10.1007/BF02579150
• K. M. Anstreicher, A strengthened acceptance criterion for approximate projections in Karmarkar's algorithm, Operations Research Letters 5, 1986, 211–214. https://www.sciencedirect.com/journal/operations-research-letters/vol/5
• Yu. Nesterov and A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
• Yu. E. Nesterov and M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM Journal on Optimization 8(2), 1998, 324–364. https://doi.org/10.1137/S1052623495290209

Motivation

Potential-reduction methods solve a linear or conic program by driving down a single merit function that combines the objective gap with a barrier for the constraint cone. For linear programming the primal version goes back to Karmarkar (1984) and, without Karmarkar's special problem form, to Gonzaga (1990, Math. Programming 49, 7–21), whose method reduces the potential by a constant at every step while updating a lower bound on the optimal value. Nesterov and Nemirovskii (1994) extended such methods to general convex cones with self-concordant barriers, but their analysis only allows short steps: steps confined to a ball of the local norm, which in practice is a small fraction of the way to the boundary.

Nesterov and Todd (1997) singled out the self-scaled cones (the nonnegative orthant, the second-order cone, the cone of positive semidefinite matrices, and their products) and showed that for them long steps are admissible. This mission formalizes their extension of Gonzaga's method (§7.2 of the paper): a primal potential-reduction step, with a lower-bound update, that decreases the potential by a constant and, when the potential parameter is large enough, by an amount that scales with how far the step can go.

Setting

Let $E = \mathbb R^n$ with its inner product, identified with its dual $E^*$. Let $K \subseteq E$ be a closed convex pointed cone with nonempty interior, and $F$ a $\nu$-self-scaled barrier for $K$: a $\nu$-self-concordant logarithmically homogeneous barrier ($F(\tau x) = F(x) - \nu\ln\tau$) such that for all $w, x \in \operatorname{int} K$ the Hessian satisfies $F''(w)x \in \operatorname{int} K^*$ and $F_*(F''(w)x) = F(x) - 2F(w) - \nu$, where $K^*$ is the dual cone and $F_*$ the conjugate barrier. Here $\nu \ge 1$.

The problem is

$$(P)\qquad \min\ \langle c, x\rangle \quad\text{s.t.}\quad Ax = b,\ x \in K,$$

with $A : E \to \mathbb R^m$ linear and surjective, and dual $(D)$: $\max \langle b, y\rangle$ s.t. $A^*y + s = c$, $s \in K^*$. Both have strictly feasible points: $S^0(P) = \{x \in \operatorname{int}K : Ax = b\}$ and $S^0(D)$ are nonempty, and the objective is not constant on the feasible region of $(P)$. Let $\zeta^*$ be the optimal value.

At $x \in \operatorname{int}K$ the local norm is $\|p\|_x = \langle F''(x)p, p\rangle^{1/2}$, its dual is $\|u\|^*_x = \langle u, [F''(x)]^{-1}u\rangle^{1/2}$, and $\sigma_x(p) = \min\{\beta \ge 0 : \beta x - p \in K\}$ measures how far one can move from $x$ along $-p$: the point $x - \alpha p$ stays in $\operatorname{int}K$ for $\alpha\sigma_x(p) < 1$. The uniform norm is $|p|_x = \max\{\sigma_x(p), \sigma_x(-p)\} \le \|p\|_x$.

For $\mu > \nu$ and a lower bound $\zeta \le \zeta^*$, the primal potential is

$$\Phi(x;\zeta) = \mu\ln(\langle c, x\rangle - \zeta) + F(x).$$

At an iterate $\hat x \in S^0(P)$ with lower bound $\hat\zeta$, let $p(c)$ and $p(d)$ be the projections of $c$ and of $d = F'(\hat x)$ into $\ker A$ with respect to $F''(\hat x)$: $Ap(u) = 0$, $A^*y(u) + F''(\hat x)p(u) = u$. For $\lambda \in \mathbb R$ put $\tilde s(\lambda) = F''(\hat x)(p(c) + \lambda p(d)) - \lambda F'(\hat x)$. Whenever $\tilde s(\lambda) \in K^*$, the number $\langle c, \hat x\rangle - \langle \tilde s(\lambda), \hat x\rangle$ is the value of a feasible dual solution, hence a lower bound on $\zeta^*$. The updated lower bound $\zeta^+$ is the larger of $\hat\zeta$ and the best such bound. Finally $\lambda^+ = (\langle c, \hat x\rangle - \zeta^+)/\mu$ and the search direction is $p = p(c) + \lambda^+ p(d)$, which is $\lambda^+$ times the projected gradient of $\Phi(\cdot;\zeta^+)$. Write $p_+ = \sigma_{\hat x}(p)$.

Formalization targets

Goal: Theorem 7.4 (b), the long step

If $\mu \ge 2\nu$, there is $\alpha > 0$ with $x^+ = \hat x - \alpha p \in S^0(P)$ and

$$\Phi(x^+;\zeta^+) \le \Phi(\hat x;\hat\zeta) - \frac{\|p\|^2_{\hat x}}{(\max\{p_+, |p|_{\hat x}\})^2}(1-\ln 2) = \Phi(\hat x;\hat\zeta) - \frac{\|p\|^2_{\hat x}}{|p|^2_{\hat x}}(1-\ln 2) \le \Phi(\hat x;\hat\zeta) - (1-\ln 2).$$

Companion: Theorem 7.4 (a), the short step

If $\mu \ge \nu + \sqrt\nu$, there is $\alpha > 0$ with $x^+ = \hat x - \alpha p \in S^0(P)$ and

$$\Phi(x^+;\zeta^+) \le \Phi(\hat x;\hat\zeta) - \frac{\|p\|^2_{\hat x}}{(\max\{p_+, \|p\|_{\hat x}\})^2}(1-\ln 2) = \Phi(\hat x;\hat\zeta) - (1-\ln 2).$$

Milestones

1. (§7.2, p. 31) The gap $\langle\tilde s(\lambda), \hat x\rangle = \langle -F'(\hat x), p(c)\rangle + \lambda\big((\|F'(\hat x)\|^*_{\hat x})^2 - \|p(d)\|^2_{\hat x}\big)$ is nondecreasing in $\lambda$.
2. (Lemma 7.2) If $\mu \ge \nu + \sqrt\nu$ then $\lambda^+ \le \|p\|_{\hat x}$; if $\mu \ge 2\nu$ then $\lambda^+ \le |p|_{\hat x}$.

Companion: Theorem 7.3

A total potential decrease $\Delta > \mu\ln(\langle c, x_0\rangle - \zeta_0) + F(x_0) - \underline F$ from the starting pair $(x_0, \zeta_0)$ forces $\langle c, x\rangle - \zeta \le (\langle c, x_0\rangle - \zeta_0)\,e^{(F(x_0) - \underline F)/\mu}\,e^{-\Delta/\mu}$, where $\underline F$ is the minimum of $F$ on a bounded truncation $\bar K$ of the homogenized feasible region.

Significance

Theorem 7.4 together with Theorem 7.3 gives an $O(\mu\ln(1/\epsilon))$-iteration method for conic programming over self-scaled cones that needs only a primal strictly feasible point and a lower bound, and that, for $\mu = O(\nu)$, matches the complexity of the short-step theory. Part (b) is the substantive claim: the step $\alpha$ may go a large fraction of the way to the boundary of $K$ (half way when $\sigma_{\hat x}(p) = \sigma_{\hat x}(-p)$) and the guaranteed decrease $(\|p\|^2_{\hat x}/|p|^2_{\hat x})(1 - \ln 2)$ is typically much larger than $1 - \ln 2$. This is the property that distinguishes self-scaled barriers from general self-concordant ones, for which only steps inside the local unit ball are controlled.

The results are proved in the paper. None of them, nor the long-step theory of self-scaled barriers on which they rest, is formalized in any proof assistant as far as is known.

Difficulty

The obvious approach bounds $F(\hat x - \alpha p) - F(\hat x)$ by the self-concordance inequality, which controls $F$ only for $\alpha\|p\|_{\hat x} < 1$; that is the short-step regime and yields at best part (a). Part (b) requires a bound on $F$ along $-p$ valid all the way to $\alpha < 1/\sigma_{\hat x}(p)$, which holds for self-scaled barriers but not for self-concordant ones. The second difficulty is the interplay with the lower-bound update: the decrease of the barrier term must be paid for by the decrease of $\mu\ln(\langle c, x\rangle - \zeta^+)$, and this needs the scaling factor $\lambda^+$ of the direction to be at most $|p|_{\hat x}$, which in turn depends on how $\zeta^+$ was chosen. With an arbitrary admissible lower bound the claim fails.

Formalization scope

$E$, $E^*$ are EuclideanSpace ℝ (Fin n) identified through the inner product, and the problem data are $A : \mathbb R^n \to_L \mathbb R^m$ surjective, $b$, $c$. The cone, the barrier, the local norms $\|\cdot\|_x$ (lnorm), $\|\cdot\|^*_x$ (dnorm), $\sigma_x$ (sigma) and $|\cdot|_x$ (absn) are the published definitions of the SelfScaledIPM.ShortStep setting; the paper's starred dual norms map to dnorm at a primal point. Nondegeneracy of $F''$ is part of that barrier definition, and the conjugate barrier is an sSup over $\operatorname{int}K$.

Standing assumptions are hypotheses of every statement: surjectivity of $A$ (6.1), strict dual feasibility (6.3) (strict primal feasibility follows from the given iterate), the objective not constant on the feasible region, and $\nu \ge 1$. The optimal value $\zeta^*$ is the infimum of the objective over the feasible set, finite under these assumptions. The projections (7.12) are given as data satisfying their defining equations. The updated lower bound $\zeta^+$ is defined as $\max(\hat\zeta, \sup G)$, with $G$ the set of dual bounds $\langle c, \hat x\rangle - \langle\tilde s(\lambda), \hat x\rangle$ over $\lambda$ with $\tilde s(\lambda) \in K^*$, and $\zeta^+ = \hat\zeta$ when $G$ is empty. Because the gap is nondecreasing in $\lambda$, this equals the paper's value at the minimal admissible $\lambda$. "A suitable value of $\alpha$" is an existential over $\alpha > 0$, and the conclusion also asserts $\langle c, x^+\rangle > \zeta^+$ so that the logarithm in $\Phi(x^+;\zeta^+)$ is genuine. $\bar K$ and $\underline F$ of Theorem 7.3 are defined explicitly, with $\underline F$ the infimum of $F$ over $\bar K \cap \operatorname{int}K$.

A statement in which $\zeta^+$ is an arbitrary lower bound above $\hat\zeta$, or $p$ an arbitrary vector in $\ker A$, or $\alpha$ arbitrary instead of existentially chosen, would be false; the formalization fixes $\zeta^+$ by (7.17) and $p$ by (7.14).

A complete development needs the theory of self-scaled barriers along a line (Theorem 4.2 and Proposition 4.1 of the paper, posed in the sibling mission I of this series), the projection identities (Propositions 6.2–6.3, posed in mission IV), weak conic duality, and the inequalities $\langle -F'(x), p\rangle \le \sqrt\nu\|p\|_x$ and $\langle -F'(x), p\rangle \le \nu\sigma_x(p)$. These are reusable across self-scaled interior-point methods; proofs of any of them are welcome.

Selected references

• Yu. E. Nesterov and M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Mathematics of Operations Research 22(1), 1997, 1–42. https://doi.org/10.1287/moor.22.1.1
• Yu. E. Nesterov and M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM Journal on Optimization 8(2), 1998, 324–364. https://doi.org/10.1137/S1052623495290209
• Yu. Nesterov and A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
• C. C. Gonzaga, Polynomial affine algorithms for linear programming, Mathematical Programming 49, 1990, 7–21 (cited as in the paper's reference list).
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, 373–395. https://doi.org/10.1007/BF02579150