Machine Learning

Motivation

Online convex optimization is the standard model for learning from a stream of data: in round $t$ a learner commits to a point $x_t$ in a convex set $\mathcal X\subseteq\mathbb R^d$, a convex loss $f_t$ is revealed, and the learner pays $f_t(x_t)+\varphi(x_t)$, where $\varphi$ is a fixed regularizer. Subgradient methods for this model use one fixed geometry (usually the Euclidean one) for every coordinate and every direction, regardless of the data. Duchi, Hazan and Singer (JMLR 12 (2011) 2121–2159) introduced ADAGRAD, which adapts the geometry to the observed subgradients. The diagonal version is one of the most widely used optimizers in machine learning and the ancestor of RMSProp and Adam. This mission formalizes the paper's full-matrix version: the proximal term is built from the matrix square root of the accumulated outer products of the subgradients, so the method adapts to correlated directions, not only to individual coordinates.

The analysis extends the regret bounds of primal-dual subgradient methods and regularized dual averaging (Nesterov 2009; Xiao 2010) and of composite mirror descent to proximal functions that change over time, and combines them with trace inequalities for the matrix square root. Concurrent work by McMahan and Streeter (COLT 2010) studied closely related adaptive proximal methods.

Setting

Vectors live in $\mathbb R^d$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|_2$. In round $t=1,2,\dots$ the learner plays $x_t\in\mathcal X$ and observes a subgradient $g_t\in\partial f_t(x_t)$, that is, $f_t(y)\ge f_t(x_t)+\langle g_t,y-x_t\rangle$ for all $y$. The regret against a comparator $x^*\in\mathcal X$ is

$$R_\phi(T)=\sum_{t=1}^T\big[f_t(x_t)+\varphi(x_t)-f_t(x^*)-\varphi(x^*)\big].$$

The outer product matrix is $G_t=\sum_{\tau=1}^t g_\tau g_\tau^\top$, a symmetric positive semidefinite $d\times d$ matrix, and $S_t=G_t^{1/2}$ is its positive semidefinite square root. With parameters $\eta>0$ and $\delta\ge0$, ADAGRAD with full matrices (Figure 2 of the paper) sets

$$H_t=\delta I+S_t,\qquad \psi_t(x)=\tfrac12\langle x,H_tx\rangle,\qquad B_{\psi_t}(x,y)=\tfrac12\langle x-y,H_t(x-y)\rangle,$$

starts at $x_1=0$, and computes $x_{t+1}$ by one of two updates:

• the primal-dual subgradient update (3): $x_{t+1}\in\operatorname{argmin}_{x\in\mathcal X}\{\eta\langle\tfrac1t\sum_{\tau\le t}g_\tau,x\rangle+\eta\varphi(x)+\tfrac1t\psi_t(x)\}$;
• the composite mirror descent update (4): $x_{t+1}\in\operatorname{argmin}_{x\in\mathcal X}\{\eta\langle g_t,x\rangle+\eta\varphi(x)+B_{\psi_t}(x,x_t)\}$.

The dual (semi)norm of $\psi_t$ is $\|v\|_{\psi_t^*}^2=\langle v,H_t^\dagger v\rangle$, where $A^\dagger$ is the pseudo-inverse.

Formalization targets

Goal: Theorem 7

Assume $\mathcal X$ closed and convex, $f_t$ and $\varphi$ convex, and $\varphi$ minimized over $\mathcal X$ at $x_1=0$. For the primal-dual update with $\delta\ge\max_{t\le T}\|g_t\|_2$, every $x^*\in\mathcal X$ satisfies

$$R_\phi(T)\le\frac\delta\eta\|x^*\|_2^2+\frac1\eta\|x^*\|_2^2\operatorname{tr}(G_T^{1/2})+\eta\operatorname{tr}(G_T^{1/2}),$$

and for the composite mirror descent update with any $\delta\ge0$,

$$R_\phi(T)\le\frac\delta\eta\|x^*\|_2^2+\frac1{2\eta}\max_{t\le T}\|x^*-x_t\|_2^2\operatorname{tr}(G_T^{1/2})+\eta\operatorname{tr}(G_T^{1/2}).$$

Milestones

In the order the proof uses them:

1. Lemma 16 and Propositions 3 and 2: regret bounds for mirror descent and dual averaging with time-varying quadratic proximal functions $\psi_t(x)=\tfrac12\langle x,H_tx\rangle$ ((11) and (10)).
2. Lemma 13: $A\succeq B\succeq0$ implies $A^{1/2}\succeq B^{1/2}$.
3. The first display of the proof of Theorem 7 and inequality (16): the growth of the Bregman terms is controlled by $\operatorname{tr}(G_t^{1/2})$.
4. Lemma 14 ($\nabla_X\operatorname{tr}(X^p)=pX^{p-1}$), Lemma 8 (a first-order concavity inequality for $\operatorname{tr}(B^{1/2})$ at singular $B$), Lemma 9, and Lemma 10, the doubling lemma

$$\sum_{t=1}^T\langle g_t,S_t^\dagger g_t\rangle\le2\sum_{t=1}^T\langle g_t,S_T^\dagger g_t\rangle=2\operatorname{tr}(G_T^{1/2}).$$

5. (17): the dual-norm sums of both updates are at most $2\operatorname{tr}(G_T^{1/2})$.

Significance

The quantity $\operatorname{tr}(G_T^{1/2})$ can be much smaller than the $\sqrt{T}\max_t\|g_t\|_2$ factor in the regret of non-adaptive online gradient descent with a tuned step size: it is small when the subgradients concentrate in a few directions, possibly not aligned with the coordinate axes. The paper's Corollary 11 rewrites it as $\sqrt d$ times the square root of $\inf\{\sum_t g_t^\top S^{-1}g_t: S\succeq0,\operatorname{tr}(S)\le d\}$, the gradient term of the best fixed full-matrix proximal function chosen in hindsight. The supporting results have their own uses. Propositions 2 and 3 are the generic regret bounds for adaptive proximal methods. Lemmas 8–10 are trace inequalities for the matrix square root that appear throughout the analysis of second-order online methods.

The results are proved in the paper. To our knowledge none of them has a machine-checked proof. Formalizing them requires the matrix functional calculus (square roots, pseudo-inverses, real powers) in a form usable for inequalities, which Mathlib has only partly: for instance, monotonicity of the square root is in Mathlib for C*-algebras, which covers complex but not real matrices. A complete development gives a verified regret bound for an adaptive full-matrix method together with these matrix inequalities.

Difficulty

The online-learning half (Lemma 16, Propositions 2 and 3) is a convex-analysis argument once the proximal functions are quadratic. The obstacle is the matrix half. The natural approach to Lemma 10 is induction with a scalar inequality $\sqrt{b-a}\le\sqrt b-a/(2\sqrt b)$ applied eigenvalue by eigenvalue. This fails because $G_{T-1}$ and $G_T$ do not commute, so their eigenvectors differ. One needs the concavity of $A\mapsto\operatorname{tr}(A^{1/2})$ on positive semidefinite matrices and its gradient, at points where $A$ may be singular. That is where Lemma 8 and the pseudo-inverse enter: the inverse root does not exist, and a limit $\delta\downarrow0$ is needed. The same issue arises in Lemma 9 and in the dual norm when $\delta=0$.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), so ‖·‖ is the Euclidean norm. Matrices are Matrix (Fin d) (Fin d) ℝ, acting on vectors through Matrix.toEuclideanLin. The square root is Mathlib's CFC.sqrt under the Loewner order (MatrixOrder). The pseudo-inverse is the functional calculus of $\lambda\mapsto\lambda^{-1}$ with $0^{-1}=0$, and $B^{-1/2}$ is written as $(B^\dagger)^{1/2}$. Mathlib's matrix inverse is used only where the matrix is invertible or the vector is zero. Rounds are 1-based and $G_0=0$. The losses and $\varphi$ are real-valued convex functions, and the constraint is carried by $\mathcal X$. Each update's argmin is a predicate (the next iterate lies in $\mathcal X$ and minimizes the objective there), which does not assert existence or uniqueness. A run consists of the $T$ rounds of Figure 2, with the subgradient relation imposed in every round. The subgradient relation is the platform's published ShorNonsmooth.AlmostDiff.IsSubgradient.

Restrictions and conventions, each stated in the item that needs it:

• $\varphi$ is minimized over $\mathcal X$ at $x_1=0$. This is the paper's $x_1=\arg\min_{\mathcal X}\varphi$. Without it both parts of Theorem 7 are false.
• Lemma 8 assumes $\nu\ge0$. The page says "for any $\nu$", but the inequality fails for $\nu<0$ (for $B=0$, $\nu=-1$ it reads $2\|g\|_2\le0$). The paper only applies the lemma with $\nu=1$.
• Lemma 16 and Propositions 2, 3 are specialised to quadratic proximal functions. In Lemma 16 and Proposition 3, $H_t$ is positive semidefinite and $g_t$ lies in its range, so the dual norm is finite. In Proposition 2, $H_t$ is positive definite, the $H_t$ increase, and $x_1=0$. Lemma 16 asks for $x^*\in\mathcal X$. Proposition 3 is stated for $T\ge1$ rounds.
• $H_0=\delta I$ in the dual norm $\|\cdot\|_{\psi_0^*}$ of (17) and Theorem 7. Figure 2's $H_0=0$ is never used by the updates.
• Lemma 14's gradient is stated as a directional derivative along every symmetric direction.

A formalization in which the next iterate need not lie in $\mathcal X$, the comparator ranges outside $\mathcal X$, $S_t$ is $G_t$ itself or its entrywise square root, or $S_t^\dagger$ is Mathlib's matrix inverse (which vanishes on singular matrices), states a different theorem and is excluded.

Proofs need the convex-analysis optimality conditions for the two updates, the Loewner-order calculus of CFC.sqrt on real matrices (Lemma 13), concavity and differentiability of $\operatorname{tr}(A^{1/2})$, and limits $\delta\downarrow0$ in the functional calculus. The matrix lemmas (13, 14, 8, 9, 10) are reusable outside this paper. Alternative proofs, for instance of Lemma 10 through operator concavity, are welcome.

Selected references

• J. Duchi, E. Hazan, Y. Singer, Adaptive Subgradient Methods for Online Learning and Stochastic Optimization, Journal of Machine Learning Research 12 (2011) 2121–2159. https://jmlr.org/papers/v12/duchi11a.html
• H. B. McMahan, M. Streeter, Adaptive Bound Optimization for Online Convex Optimization, COLT 2010. https://arxiv.org/abs/1002.4908
• L. Xiao, Dual Averaging Methods for Regularized Stochastic Learning and Online Optimization, Journal of Machine Learning Research 11 (2010) 2543–2596. https://jmlr.org/papers/v11/xiao10a.html
• Y. Nesterov, Primal-dual subgradient methods for convex problems, Mathematical Programming 120 (2009) 221–259. https://doi.org/10.1007/s10107-007-0149-x
• T. Ando, Concavity of certain maps on positive definite matrices and applications to Hadamard products, Linear Algebra and its Applications 26 (1979) 203–241. https://doi.org/10.1016/0024-3795(79)90179-4

Why natural policy gradient

Policy gradient methods optimize a parameterized policy directly by gradient ascent on its expected discounted return. They underlie most practical reinforcement-learning systems, yet for a long time their convergence was understood only locally: the objective $\theta\mapsto V^{\pi_\theta}(\rho)$ is not concave, and plain gradient ascent can stall on plateaus. The natural policy gradient (NPG) of Kakade (2001) preconditions the gradient by the pseudoinverse of the Fisher information matrix of the policy, so that steps are measured in the geometry of the induced action distributions rather than in parameter space. NPG is the conceptual ancestor of trust-region methods such as TRPO and PPO.

Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 2021) prove that exact NPG with softmax policies converges to the optimal value at rate $O(1/T)$, with constants that depend on neither the number of states, nor the number of actions beyond $\log|\mathcal A|$, nor any distribution mismatch coefficient. This mission formalizes that result, Theorem 5.3 of the paper, and the lemmas its proof rests on.

Timeline. Kakade (2001) introduced NPG and observed that, for softmax policies, it moves toward the greedy policy. Kakade and Langford (2002) proved the performance difference lemma. Even-Dar, Kakade and Mansour (2009) analyzed experts algorithms in changing MDPs, whose regret argument this proof adapts; Geist, Scherrer and Pietquin (2019) studied regularized policy iteration with related rates. Agarwal et al. (preprint 2019, journal 2021) gave the dimension-free $\log|\mathcal A|/(\eta T)+1/((1-\gamma)^2T)$ bound formalized here.

Setting

A finite discounted MDP consists of finite sets $\mathcal S$ (states) and $\mathcal A$ (actions, nonempty), a transition kernel $P(s'\mid s,a)$, rewards $r(s,a)\in[0,1]$ and a discount factor $\gamma\in[0,1)$. A policy $\pi$ assigns to each state a distribution $\pi(\cdot\mid s)$ over actions. Its value $V^\pi(s)$ is the expected discounted sum of rewards started from $s$; for a start distribution $\rho$, $V^\pi(\rho)=\sum_s\rho(s)V^\pi(s)$. The state–action value is $Q^\pi(s,a)=r(s,a)+\gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$ and the advantage is $A^\pi(s,a)=Q^\pi(s,a)-V^\pi(s)$. The discounted state visitation distribution is

$$d^\pi_\rho(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\,\Pr{}^\pi(s_t=s\mid s_0\sim\rho).$$

An optimal policy $\pi^\star$ has $V^{\pi^\star}(s)\ge V^\pi(s)$ for every policy $\pi$ and every state $s$; write $V^\star=V^{\pi^\star}$.

The softmax policy with parameter $\theta\in\mathbb R^{|\mathcal S||\mathcal A|}$ is $\pi_\theta(a\mid s)=\exp(\theta_{s,a})/\sum_{a'}\exp(\theta_{s,a'})$. The Fisher information matrix with respect to $\rho$ is

$$F_\rho(\theta)=\mathbb E_{s\sim d^{\pi_\theta}_\rho}\mathbb E_{a\sim\pi_\theta(\cdot\mid s)}\big[\nabla_\theta\log\pi_\theta(a\mid s)\,\nabla_\theta\log\pi_\theta(a\mid s)^\top\big],$$

and the NPG update with step size $\eta$ is

$$\theta^{(t+1)}=\theta^{(t)}+\eta\,F_\rho(\theta^{(t)})^\dagger\,\nabla_\theta V^{(t)}(\rho),\tag{15}$$

where $M^\dagger$ is the Moore–Penrose pseudoinverse and $\pi^{(t)},V^{(t)},A^{(t)}$ are the quantities of $\theta^{(t)}$. Following §5.3, every state is assumed reachable from $\rho$: for each $s$ some policy $\pi$ has $d^\pi_\rho(s)>0$. The normalizer $Z_t(s)=\sum_a\pi^{(t)}(a\mid s)\exp(\eta A^{(t)}(s,a)/(1-\gamma))$ appears in the lemmas.

Formalization targets

Goal: Theorem 5.3

For NPG (15) from $\theta^{(0)}=0$ with any fixed $\eta>0$, for all $T>0$,

$$V^{(T)}(\rho)\ \ge\ V^\star(\rho)-\frac{\log|\mathcal A|}{\eta T}-\frac{1}{(1-\gamma)^2T}.$$

Companion: iteration complexity

If moreover $\eta\ge(1-\gamma)^2\log|\mathcal A|$ and $\epsilon>0$, then $V^\star(\rho)-V^{(T)}(\rho)\le\epsilon$ for every $T\ge 2/((1-\gamma)^2\epsilon)$.

Milestones

1. Lemma 3.2 (performance difference): $V^\pi(s_0)-V^{\pi'}(s_0)=\frac{1}{1-\gamma}\mathbb E_{s\sim d^\pi_{s_0}}\mathbb E_{a\sim\pi(\cdot\mid s)}[A^{\pi'}(s,a)]$.
2. Lemma 5.1 (soft policy iteration, policy form): $\pi^{(t+1)}(a\mid s)=\pi^{(t)}(a\mid s)\exp(\eta A^{(t)}(s,a)/(1-\gamma))/Z_t(s)$.
3. Lemma 5.2 (improvement): $V^{(t+1)}(\mu)-V^{(t)}(\mu)\ge\frac{1-\gamma}{\eta}\mathbb E_{s\sim\mu}\log Z_t(s)\ge0$ for every $\mu\in\Delta(\mathcal S)$.
4. Monotonicity (proof of Theorem 5.3): $V^{(t+1)}(s)\ge V^{(t)}(s)$ for all $s$.

Significance

The result. Theorem 5.3 is a global, non-asymptotic guarantee for a non-concave policy optimization problem, with no dependence on $|\mathcal S|$ and no distribution mismatch coefficient: the same analysis does not go through for plain softmax policy gradient, whose rates in the same paper carry such coefficients or are only asymptotic. It explains why Fisher preconditioning helps, and it is the template for the paper's later analysis of NPG with function approximation (§6) and for subsequent work on linear convergence of NPG and on entropy-regularized variants.

Formalizing it. The theorem is proved on paper; no machine-checked proof is known. A formal development needs: a policy-gradient identity for softmax policies, the computation of the Moore–Penrose pseudoinverse of a singular, block-structured Fisher matrix acting on the policy gradient, the performance difference lemma in the unnormalized convention, and a telescoping regret argument with Kullback–Leibler divergences between action distributions. Each of these is reusable: the performance difference lemma and the visitation-distribution calculus serve every result of the paper and much of the reinforcement-learning literature.

Difficulty

The obvious approach, treating NPG as gradient ascent on a smooth objective, fails: $V^{\pi_\theta}(\rho)$ is non-concave and its smoothness constant grows with $1/(1-\gamma)^3$, which would give a rate depending on the state space and on distribution mismatch. The dimension-free rate comes only after the NPG step is rewritten exactly as a multiplicative-weights update on each state's action distribution, and this rewriting is itself delicate. The Fisher matrix is always singular (each state's block annihilates the all-ones vector), the pseudoinverse returns the minimum-norm solution, which is not $A^{(t)}/(1-\gamma)$ but differs from it by a state-dependent offset; and the identity holds at a state only if that state carries positive visitation weight, which is why reachability from $\rho$ is assumed. A newcomer's first idea, replacing $F^\dagger$ by "any solution of $Fu=\nabla V$" or by an ordinary inverse, does not define the algorithm.

Formalization scope

Lean conventions (Mathlib, namespace PolicyGradTheory.NPG):

• Policies are functions S → A → ℝ (π s a $=\pi(a\mid s)$) satisfying the published IsPolicy; transitions P s a s' $=P(s'\mid s,a)$; values, $Q$-functions and state occupation probabilities are the published FoundationsML definitions PolicyValue, QFunction, OccupationDist, and optimality is IsOptimalPolicy. $V^\star(\rho)$ is the value of a policy assumed optimal, never a supremum over arbitrary functions.
• Parameters live in EuclideanSpace ℝ (S × A), so norms are Euclidean and gradient is $\nabla_\theta$.
• The pseudoinverse is the published predicate VectorSpaceOpt.IsPseudoinverse (minimum-norm least-squares inverse, which on Euclidean space is the Moore–Penrose pseudoinverse); Mathlib has none.
• Standing assumptions carried by every statement: rewards in $[0,1]$, $\gamma\in[0,1)$, $\mathcal A$ nonempty, $\rho\in\Delta(\mathcal S)$, every state reachable from $\rho$ (§5.3, footnote 6). The goal also assumes $\theta^{(0)}=0$ and $\eta>0$, as the page does. Lemmas 5.1 and 5.2 hold from any start.
• $\log$ is the natural logarithm; $T$ counts updates and $T>0$ is a natural number.

The goal does not assume the soft-policy-iteration form, the improvement bound or monotonicity; those are milestones to be proved, and a statement taking any of them as a hypothesis would not be Theorem 5.3. The parameter form "$\theta^{(t+1)}=\theta^{(t)}+\frac{\eta}{1-\gamma}A^{(t)}$" of Lemma 5.1 is not stated, since the pseudoinverse step differs from it by a state-dependent offset (as the lemma's own proof on p. 70 shows); only the policy form, which is invariant to that offset, is a target.

Contributions welcome: the softmax policy-gradient identity and score-function formula, existence and uniqueness of the minimum-norm least-squares inverse on Euclidean space, Kullback–Leibler identities for finite distributions, and the summability facts behind the visitation distribution.

Selected references

• A. Agarwal, S. M. Kakade, J. D. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, JMLR 22(98), 2021; preprint arXiv:1908.00261v5, 2020. https://arxiv.org/abs/1908.00261v5
• S. M. Kakade, A Natural Policy Gradient, NeurIPS 2001. https://proceedings.neurips.cc/paper/2001/hash/4b86abe48d358ecf194c56c69108433e-Abstract.html
• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• E. Even-Dar, S. M. Kakade, Y. Mansour, Online Markov Decision Processes, Mathematics of Operations Research 34(3), 2009. https://doi.org/10.1287/moor.1090.0396
• M. Geist, B. Scherrer, O. Pietquin, A Theory of Regularized Markov Decision Processes, ICML 2019. https://arxiv.org/abs/1901.11275

Motivation

Stochastic and online subgradient methods are the workhorse of large-scale learning: each step touches one example, costs time linear in the dimension, and needs no line search. Their weak point is the step size. A single global step size treats every coordinate alike, while in high-dimensional, sparse problems (text, click-through data, bag-of-words features) most coordinates are zero in most examples, and the few informative rare features receive vanishingly small updates.

AdaGrad (Duchi, Hazan and Singer, JMLR 2011; McMahan and Streeter, COLT 2010, independently) chooses a separate step size per coordinate from the gradients observed so far. Its diagonal version is the ancestor of RMSProp and Adam and is one of the most widely used optimizers in machine learning. This mission targets the paper's regret guarantee for diagonal AdaGrad, which explains when per-coordinate adaptation pays off.

Timeline. Zinkevich (2003) proved $O(\sqrt T)$ regret for online projected gradient descent. Nesterov (2009) and Xiao (2010) analysed dual averaging with a regularizer; Duchi, Shalev-Shwartz, Singer and Tewari (2010) analysed composite mirror descent. Auer and Gentile (2000) proved the scalar inequality that makes adaptive step sizes work. Duchi, Hazan and Singer (2011) combined these into adaptive proximal functions with data-dependent regret bounds.

Setting

Work in $\mathbb R^d$ with the Euclidean inner product and $\|x\|_\infty=\max_i|x_i|$. A closed convex set $\mathcal X\subseteq\mathbb R^d$ with $0\in\mathcal X$ is fixed, together with a convex regularizer $\varphi:\mathbb R^d\to\mathbb R$ (for example $\lambda\|x\|_1$). In rounds $t=1,2,\dots$ a learner plays $x_t\in\mathcal X$, a convex loss $f_t$ is revealed, and the learner observes a subgradient $g_t$ of $f_t$ at $x_t$: $f_t(y)\ge f_t(x_t)+\langle g_t,y-x_t\rangle$ for all $y$. The regret against a comparator $x^*\in\mathcal X$ is

$$R_\varphi(T)=\sum_{t=1}^T\big[f_t(x_t)+\varphi(x_t)-f_t(x^*)-\varphi(x^*)\big].$$

For each coordinate $i$, let $g_{1:t,i}=(g_{1,i},\dots,g_{t,i})$ and $s_{t,i}=\|g_{1:t,i}\|_2$. Diagonal AdaGrad (Figure 1 of the paper) has parameters $\eta>0$, $\delta\ge0$, starts at $x_1=0$, and in round $t$ uses the proximal function $\psi_t(x)=\frac12\langle x,(\delta I+\mathrm{diag}(s_t))x\rangle$. It updates by one of two rules:

• the primal-dual subgradient update (3): $x_{t+1}$ minimizes $\eta\langle\frac1t\sum_{\tau\le t}g_\tau,x\rangle+\eta\varphi(x)+\frac1t\psi_t(x)$ over $\mathcal X$;
• the composite mirror descent update (4): $x_{t+1}$ minimizes $\eta\langle g_t,x\rangle+\eta\varphi(x)+B_{\psi_t}(x,x_t)$ over $\mathcal X$, where $B_{\psi_t}(x,y)=\frac12\sum_i(\delta+s_{t,i})(x_i-y_i)^2$ is the Bregman divergence of $\psi_t$.

Formalization targets

Goal: Theorem 5

For the primal-dual update with $\delta\ge\max_{t\le T}\|g_t\|_\infty$, and every $x^*\in\mathcal X$,

$$R_\varphi(T)\le\frac\delta\eta\|x^*\|_2^2+\frac1\eta\|x^*\|_\infty^2\sum_{i=1}^d\|g_{1:T,i}\|_2+\eta\sum_{i=1}^d\|g_{1:T,i}\|_2 .$$

For the composite mirror descent update with $\delta=0$, and every $x^*\in\mathcal X$,

$$R_\varphi(T)\le\frac1{2\eta}\max_{t\le T}\|x^*-x_t\|_\infty^2\sum_{i=1}^d\|g_{1:T,i}\|_2+\eta\sum_{i=1}^d\|g_{1:T,i}\|_2 .$$

Milestones

1. Lemma 16: the one-step inequality of composite mirror descent.
2. Proposition 3: the regret of composite mirror descent with time-varying proximal functions.
3. Proposition 2: the regret of primal-dual subgradient (dual averaging) with time-varying proximal functions.
4. Inequality (24): $\sum_{t\le T}a_t^2/\|a_{1:t}\|_2\le2\|a_{1:T}\|_2$ for any real sequence.
5. Lemma 4: $\sum_{t\le T}\langle g_t,\mathrm{diag}(s_t)^{-1}g_t\rangle\le2\sum_i\|g_{1:T,i}\|_2$.
6. Inequality (13): the mirror-descent gradient term is at most $2\sum_i\|g_{1:T,i}\|_2$.
7. The primal-dual analogue of (13) (§3, after (13)).
8. Inequality (14): the drift of the Bregman divergences is controlled by $\max_t\|x^*-x_t\|_\infty^2\sum_i\|g_{1:T,i}\|_2$.

Lemma 16 and Propositions 2 and 3 are stated in the paper for general proximal functions; here they are specialised to diagonal quadratic ones, $\psi_t(y)=\frac12\sum_ih_{t,i}y_i^2$.

Significance

The result. The quantity $\sum_i\|g_{1:T,i}\|_2$ is never larger than $\sqrt d\,\big(\sum_t\|g_t\|_2^2\big)^{1/2}$ and can be far smaller when gradients are sparse or coordinate scales differ. Theorem 5 shows that diagonal AdaGrad does as well as the best fixed diagonal preconditioner chosen in hindsight, up to a constant, without knowing the gradients in advance (Corollary 1 and Corollary 6 of the paper). Through online-to-batch conversion the same bound gives convergence rates for stochastic convex optimization with sparse data. The theorem underpins the theoretical case for per-coordinate adaptive step sizes.

Formalizing it. The result is proved on paper; to our knowledge no machine-checked proof of AdaGrad's regret bound exists, in Lean or elsewhere. The formalization produces checked versions of the two regret templates (composite mirror descent and dual averaging with changing proximal functions), which are reused by most later analyses of adaptive methods, and of the Auer–Gentile inequality. The formal statements also make precise two hypotheses the printed theorem leaves implicit (see Formalization scope).

Difficulty

The obvious argument fixes one proximal function and applies the classical mirror-descent or dual-averaging bound. That fails because AdaGrad's $\psi_t$ changes every round and depends on the very subgradients whose norms are being bounded: the classical bounds assume a fixed $\psi$, and with changing $\psi_t$ new drift terms appear that must be shown to be small. The gradient term $\sum_t\|g_t\|^2_{\psi_t^*}$ has denominators that grow with the data, so it is not bounded term by term; it has to be bounded as a whole sum. For dual averaging there is an additional index shift: round $t$'s subgradient is measured in the dual norm of $\psi_{t-1}$, which has not yet seen $g_t$.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin d), so ‖·‖ is the Euclidean norm; $\|\cdot\|_\infty$ is a separate definition supNorm. Rounds are 1-based, with sums over Finset.Icc 1 T; $s_0=0$. Losses and the regularizer are real-valued convex functions on all of $\mathbb R^d$, so extended-valued regularizers (indicator functions) are excluded, and the constraint is carried by $\mathcal X$. The subgradient relation is the published platform definition ShorNonsmooth.AlmostDiff.IsSubgradient. Each update is a predicate ($x_{t+1}\in\mathcal X$ and minimizes the update objective over $\mathcal X$), since the minimizer need not be unique; the theorems hold for every run. The factor $\frac12$ in $\psi_t$ follows Figure 1. Dual norms use Lean's division, where $a/0=0$ is the paper's $0/0=0$. The losses are a fixed sequence, which also covers adaptive adversaries because the run is determined by the losses.

Two restrictions relative to the printed Theorem 5, both forced by the paper's own proof:

1. The mirror-descent part is stated for $\delta=0$. The proof bounds $B_{\psi_1}(x^*,x_1)$ by $\frac12\|x^*-x_1\|_\infty^2\langle\mathbf 1,s_1\rangle$, which drops $\frac\delta2\|x^*-x_1\|_2^2$. For large $\delta>0$ the printed bound is false. $\delta=0$ is the case the proof covers and the one the paper's corollaries use.
2. $\varphi$ is minimized over $\mathcal X$ at $x_1=0$. Propositions 2 and 3 rely on this ("$x_1=\operatorname{argmin}_{x\in\mathcal X}\varphi(x)$", "w.l.o.g. $\varphi(x_1)=0$"). It holds for $\varphi=0$, $\lambda\|x\|_1$ and $\lambda\|x\|_2^2$. Without it the bounds fail.

Proposition 2 is stated with strictly positive weights. The primal-dual part of the goal with $\delta=0$ is a degenerate case in which every $g_t$ vanishes.

A run predicate without the subgradient link $g_t\in\partial f_t(x_t)$, an argmin without $x_{t+1}\in\mathcal X$, a comparator outside $\mathcal X$, or $s_t$ computed without round $t$ would each make the statement trivial or different. The definitions rule all of these out.

Needed infrastructure: elementary convex analysis on $\mathbb R^d$ (first-order optimality of a convex objective over a convex set), finite sums and square roots. Nothing beyond Mathlib is required. The two regret templates (Propositions 2 and 3) and inequality (24) are reusable beyond this mission. Proofs of any milestone, and of the full-matrix analogues, are welcome.

Selected references

• J. Duchi, E. Hazan, Y. Singer, Adaptive Subgradient Methods for Online Learning and Stochastic Optimization, Journal of Machine Learning Research 12 (2011) 2121–2159. https://jmlr.org/papers/v12/duchi11a.html
• H. B. McMahan, M. Streeter, Adaptive Bound Optimization for Online Convex Optimization, COLT 2010. https://arxiv.org/abs/1002.4908
• P. Auer, C. Gentile, Adaptive and Self-Confident On-Line Learning Algorithms, COLT 2000; J. Comput. System Sci. 64 (2002) 48–75. https://doi.org/10.1006/jcss.2001.1795
• J. Duchi, S. Shalev-Shwartz, Y. Singer, A. Tewari, Composite Objective Mirror Descent, COLT 2010.
• L. Xiao, Dual Averaging Methods for Regularized Stochastic Learning and Online Optimization, Journal of Machine Learning Research 11 (2010) 2543–2596. https://jmlr.org/papers/v11/xiao10a.html
• Y. Nesterov, Primal-dual subgradient methods for convex problems, Mathematical Programming 120 (2009) 221–259. https://doi.org/10.1007/s10107-007-0149-x
• M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003.

Motivation

Many optimization problems in statistics, machine learning and operations research ask to minimize a smooth convex function over a simple convex set: a box, a ball, a simplex, a cone of positive semidefinite matrices. Projected gradient descent is the most basic first-order method for such problems. It takes a gradient step and then returns to the feasible set by Euclidean projection. Its cost per iteration is one gradient evaluation and one projection, independent of the dimension apart from the cost of manipulating vectors, which is why it remains a workhorse in very high dimension.

This mission is the fifth in a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980). Chapter 3 of the monograph treats "dimension-free" convex optimization. Its §3.2 first proves that gradient descent on a convex $\beta$-smooth function on $\mathbb R^n$ has rate $O(\beta\|x_1-x^*\|^2/t)$ (Theorem 3.3, the subject of mission IV), and then turns to the constrained case, which is the subject of this mission. The analysis follows Nesterov's Introductory Lectures on Convex Optimization (2004).

Setting

Write $x^\top y$ for the Euclidean inner product on $\mathbb R^n$ and $\|\cdot\|$ for the Euclidean norm. The constraint set $\mathcal X\subseteq\mathbb R^n$ is compact and convex; this is the standing assumption of Chapter 3. The Euclidean projection of $y\in\mathbb R^n$ onto $\mathcal X$ is

$$\Pi_{\mathcal X}(y)=\operatorname*{argmin}_{z\in\mathcal X}\|y-z\| ,$$

which exists and is unique for a nonempty closed convex set.

A differentiable function $f:\mathbb R^n\to\mathbb R$ is $\beta$-smooth on $\mathcal X$ if its gradient is $\beta$-Lipschitz there:

$$\|\nabla f(x)-\nabla f(y)\|\le\beta\|x-y\|\qquad(x,y\in\mathcal X).$$

It is $\alpha$-strongly convex on $\mathcal X$ if $f(x)-f(y)\le\nabla f(x)^\top(x-y)-\frac\alpha2\|x-y\|^2$ for $x,y\in\mathcal X$. A minimizer $x^*\in\mathcal X$ of $f$ over $\mathcal X$ is assumed to exist, as everywhere in the monograph.

Projected gradient descent with step size $\eta=1/\beta$ starts at $x_1\in\mathcal X$ and iterates

$$x_{t+1}=\Pi_{\mathcal X}\Bigl(x_t-\tfrac1\beta\nabla f(x_t)\Bigr)\qquad(t\ge1).$$

For a point $x$ with projected step $x^+=\Pi_{\mathcal X}\bigl(x-\frac1\beta\nabla f(x)\bigr)$, the gradient mapping is $g_{\mathcal X}(x)=\beta(x-x^+)$. Without constraints it equals $\nabla f(x)$.

Formalization targets

Goal: Theorem 3.7 (p. 270)

For $f$ convex and $\beta$-smooth on $\mathcal X$, projected gradient descent with $\eta=1/\beta$ satisfies, for every $t\ge1$,

$$f(x_t)-f(x^*)\le\frac{3\beta\|x_1-x^*\|^2+f(x_1)-f(x^*)}{t}.$$

Milestones

1. Lemma 3.1 (p. 263): for $x\in\mathcal X$ and $y\in\mathbb R^n$, $(\Pi_{\mathcal X}(y)-x)^\top(\Pi_{\mathcal X}(y)-y)\le0$, and hence $\|\Pi_{\mathcal X}(y)-x\|^2+\|y-\Pi_{\mathcal X}(y)\|^2\le\|y-x\|^2$. The first claim is an already proved platform theorem.
2. (3.7) (p. 270): $\nabla f(x)^\top(x^+-y)\le g_{\mathcal X}(x)^\top(x^+-y)$ for $y\in\mathcal X$.
3. Lemma 3.6 (p. 270): for $x,y\in\mathcal X$,

$$f(x^+)-f(y)\le g_{\mathcal X}(x)^\top(x-y)-\frac1{2\beta}\|g_{\mathcal X}(x)\|^2 .$$

4. Descent and gap (pp. 270–271): $f(x_{s+1})-f(x_s)\le-\frac1{2\beta}\|g_{\mathcal X}(x_s)\|^2$ and $f(x_{s+1})-f(x^*)\le\|g_{\mathcal X}(x_s)\|\,\|x_s-x^*\|$.
5. Distances decrease (p. 271): $\|x_{s+1}-x^*\|\le\|x_s-x^*\|$.
6. Recursion and induction (p. 271): with $\delta_s=f(x_s)-f(x^*)$, $\delta_{s+1}\le\delta_s-\frac{1}{2\beta\|x_1-x^*\|^2}\delta_{s+1}^2$, and an induction on this recursion gives the bound of Theorem 3.7.

Companion: Theorem 3.10 (p. 278)

If $f$ is in addition $\alpha$-strongly convex on $\mathcal X$, with condition number $\kappa=\beta/\alpha$, then the strengthened Lemma 3.6, display (3.14), gives for every $t\ge0$

$$\|x_{t+1}-x^*\|^2\le\exp\Bigl(-\frac t\kappa\Bigr)\|x_1-x^*\|^2 .$$

Significance

Theorem 3.7 shows that a constraint set with a cheap projection costs nothing in the order of convergence: the $O(\beta\|x_1-x^*\|^2/t)$ rate of unconstrained gradient descent survives, with a constant that depends on $f(x_1)-f(x^*)$. Lemma 3.6 is the reusable part. It isolates the gradient mapping as the quantity that measures progress under constraints, and the same inequality, with a strong-convexity term added, gives the linear rate of Theorem 3.10. It is also the starting point of the analysis of proximal gradient methods for composite objectives.

All of these results are classical and proved in the textbook. As far as a search of the platform shows, none of them is formalized there. A related platform theorem on constrained gradient descent for well-conditioned functions (from Hazan's Introduction to Online Convex Optimization) bounds function values with a different exponent. It is not Theorem 3.10, which bounds distances with rate $\exp(-t/\kappa)$. This mission adds machine-checked statements of the constrained analysis in Bubeck's formulation, with the book's constants. The definitions of $\beta$-smoothness on a set, the gradient mapping and the run predicate can be reused by later missions on accelerated and proximal methods.

Difficulty

The obvious attempt is to copy the unconstrained proof, which rests on the descent inequality $f(x-\frac1\beta\nabla f(x))\le f(x)-\frac1{2\beta}\|\nabla f(x)\|^2$. That inequality fails under constraints: the projection can cut the step short, so the decrease in $f$ is not controlled by $\|\nabla f(x)\|$. At a boundary minimizer, for instance, $\nabla f(x^*)\neq0$ while no step makes progress. The proof has to replace the gradient by the gradient mapping throughout. It also has to show separately that the iterates do not move away from $x^*$, a fact that came for free without constraints from co-coercivity of the gradient (display (3.6)).

The closing induction is not routine either. The step from $s$ to $s+1$ works only from $s=2$ on, and the step from $1$ to $2$ needs a direct computation that uses the term $f(x_1)-f(x^*)$ in the numerator.

Formalization scope

• Space. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), and $x^\top y$ is ⟪x, y⟫_ℝ.
• Constraint set and minimizer. Every statement assumes $\mathcal X$ compact (IsCompact X) and convex (Convex ℝ X), the standing assumption of Chapter 3. Every statement about a run assumes a minimizer $x^*\in\mathcal X$ with $f(x^*)\le f(y)$ for all $y\in\mathcal X$, the monograph's standing assumption.
• Gradient. The gradient is an explicit map g with HasGradientAt f (g x) x at every point of $\mathbb R^n$, so $\nabla f(x)$ is defined at boundary points of $\mathcal X$. $\beta$-smoothness on $\mathcal X$ (IsBetaSmoothOn X f g β) asks this together with $\beta\ge0$ and the Lipschitz bound on $\mathcal X$ only. It is not the quadratic upper bound (3.4), which is a consequence.
• Strong convexity. It is the published predicate OnlineConvexOpt.ConvexBasics.StronglyConvexOn X f g α, which is display (3.13) with the same gradient map. Display (3.14) and Theorem 3.10 use $\alpha>0$.
• Projection. The projection is the published relation IsMetricProjection X y p: $p\in\mathcal X$ and $\|y-p\|\le\|y-z\|$ for every $z\in\mathcal X$. No choice function is used.
• Run. A run is IsProjGDRun X g β x: $\beta>0$, $x_1\in\mathcal X$, and for every $t\ge1$ the iterate $x_{t+1}$ is a projection of $x_t-\beta^{-1}g(x_t)$. Indices start at $1$ as in the book, and x 0 is unused.
• Gradient mapping. gradMap β x xplus $=\beta(x-x^+)$ takes the projected point of the run as an argument.
• Positivity. $\beta>0$ is assumed, as the step size $1/\beta$ requires, and $\alpha>0$ for Theorem 3.10, as $\kappa=\beta/\alpha$ requires.
• The recursion. The recursion of milestone 6 is stated multiplied by $2\beta\|x_1-x^*\|^2$, so the case $x_1=x^*$ needs no division.
• No trivial readings. A run predicate with a free step size, or $\beta$-smoothness replaced by the quadratic bound (3.4), would change the content. Both are excluded: the step is fixed to $1/\beta$, and smoothness is the Lipschitz condition on the gradient.

Contributions are welcome on any milestone. Lemma 3.1 and (3.7) need only the variational characterization of the projection. Lemma 3.6 needs the quadratic upper bound for a function whose gradient is Lipschitz on a convex set, together with the first-order characterization of convexity relative to a set. Both are of independent use. The induction milestone is a self-contained statement about real sequences.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer Academic Publishers, 2004. doi:10.1007/978-1-4419-8853-9
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., MIT Press, 2022. arXiv:1909.05207

Motivation

Many convex optimization problems in machine learning and statistics have objectives that are convex but not differentiable: hinge losses, $\ell_1$ penalties, maxima of finitely many affine functions, and the dual functions of Lagrangian relaxations. Methods that rely on gradients do not apply to them directly, while cutting-plane methods such as the ellipsoid method pay a price that grows with the dimension. The projected subgradient method replaces the gradient by an arbitrary subgradient and restores feasibility by a Euclidean projection. Its guarantee depends on the dimension only through two constants, a radius $R$ and a Lipschitz constant $L$. This is the reason it, and its descendants (mirror descent, stochastic gradient descent, online gradient descent), are the standard tools for large-scale nonsmooth problems.

The rate analysed here goes back to the subgradient methods of Shor and Polyak in the 1960s and 1970s and to the lower bounds of Nemirovski and Yudin (1983). The book follows the presentation of Nesterov, Introductory Lectures on Convex Optimization (2004). The strongly convex variant with weights proportional to $s$ is from Lacoste-Julien, Schmidt and Bach (2012).

This mission is the third of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015), and covers the preamble of Chapter 3, Section 3.1 and Section 3.4.1.

Setting

Let $\mathbb R^n$ carry the Euclidean inner product $x^\top y$ and norm $\|\cdot\|$. Let $\mathcal X\subseteq\mathbb R^n$ be compact and convex, and let $f$ be a convex function on $\mathcal X$ with a minimizer $x^*\in\mathcal X$.

A vector $g$ is a subgradient of $f$ at $x\in\mathcal X$ if $f(x)-f(y)\le g^\top(x-y)$ for every $y\in\mathcal X$. The set of subgradients at $x$ is written $\partial f(x)$. The projection $\Pi_{\mathcal X}(y)$ of a point $y\in\mathbb R^n$ is the point of $\mathcal X$ nearest to $y$.

Fix step sizes $\eta_s>0$. Projected subgradient descent starts at some $x_1\in\mathcal X$ and iterates, for $s\ge1$,

$$y_{s+1}=x_s-\eta_s g_s,\quad g_s\in\partial f(x_s),\qquad x_{s+1}=\Pi_{\mathcal X}(y_{s+1}).$$

Any subgradient may be chosen at each step. In Section 3.1 the step is constant, $\eta_s=\eta$. The set $\mathcal X$ lies in the Euclidean ball of radius $R$ centred at $x_1$, and the subgradients have norm at most $L$.

A function $f$ is $\alpha$-strongly convex on $\mathcal X$ if $f(x)-f(y)\le g^\top(x-y)-\frac{\alpha}{2}\|x-y\|^2$ for all $x,y\in\mathcal X$ and $g\in\partial f(x)$.

Formalization targets

Goal: Theorem 3.2

For every horizon $t\ge1$, projected subgradient descent with the constant step $\eta=R/(L\sqrt t)$ satisfies

$$f\Big(\frac1t\sum_{s=1}^{t}x_s\Big)-f(x^*)\le\frac{RL}{\sqrt t}.$$

Milestones

1. Lemma 3.1. For $x\in\mathcal X$ and $y\in\mathbb R^n$: $(\Pi_{\mathcal X}(y)-x)^\top(\Pi_{\mathcal X}(y)-y)\le0$, already on the platform as a published theorem. The mission also states its consequence

$$\|\Pi_{\mathcal X}(y)-x\|^2+\|y-\Pi_{\mathcal X}(y)\|^2\le\|y-x\|^2 .$$

2. The per-step inequality in the proof of Theorem 3.2:

$$f(x_s)-f(x^*)\le\frac1{2\eta}\big(\|x_s-x^*\|^2-\|y_{s+1}-x^*\|^2\big)+\frac\eta2\|g_s\|^2 .$$

3. The summed inequality for any constant step $\eta>0$:

$$\sum_{s=1}^{t}\big(f(x_s)-f(x^*)\big)\le\frac{R^2}{2\eta}+\frac{\eta L^2t}{2}.$$

Companion: Theorem 3.9

If $f$ is $\alpha$-strongly convex and its subgradients are bounded by $L$, then with $\eta_s=2/(\alpha(s+1))$,

$$f\Big(\sum_{s=1}^{t}\frac{2s}{t(t+1)}x_s\Big)-f(x^*)\le\frac{2L^2}{\alpha(t+1)}.$$

Significance

Theorem 3.2 gives an oracle complexity of $O(R^2L^2/\varepsilon^2)$ for reaching an $\varepsilon$-optimal point, independent of the ambient dimension. Section 3.5 of the book shows this rate is unimprovable for black-box first-order methods once the dimension is large. Theorem 3.9 shows how strong convexity improves the rate to $O(1/t)$, with the averaging weights changed from uniform to linear. These two bounds are the reference points against which the rest of Chapter 3 and Chapters 4 to 6 (smooth, accelerated, mirror, stochastic methods) are measured.

The results are classical and their proofs are short. Formalizing them produces a reusable, machine-checked account of the basic projected first-order step: the projection inequality, the one-step distance recursion, and the telescoping argument with Jensen's inequality for averaged iterates. To our knowledge, no machine-checked proof of the averaged-iterate bound for the projected subgradient method exists in Mathlib. Related platform items cover other algorithms or other averaging schemes.

Difficulty

The arithmetic is elementary, and the obvious argument works. The care is in the bookkeeping. The projection must be shown not to increase the distance to $x^*$, which needs convexity of $\mathcal X$ and the variational characterization of the nearest point. The sum must telescope with a horizon-dependent constant step. Jensen's inequality must be applied to a finite convex combination of points of $\mathcal X$, which requires showing that the average lies in $\mathcal X$. In Theorem 3.9 the step sizes and the averaging weights are coupled, so neither can be changed independently. In Lean, the iterates are indexed from $1$ with natural-number horizons, and the bounds involve $\sqrt t$, so these casts need care.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The iterates are sequences ℕ → EuclideanSpace ℝ (Fin n) with the first iterate at index $1$. The projection is the published relation OnlineConvexOpt.FirstOrder.IsMetricProjection ($x_{s+1}\in\mathcal X$ is a nearest point to $y_{s+1}$). Subgradients are taken relative to $\mathcal X$ (Definition 1.2). A run is a predicate on the steps $s=1,\dots,t$, and every theorem holds for all runs, that is, for every choice of subgradients. Compactness and convexity of $\mathcal X$, convexity of $f$ on $\mathcal X$ and the existence of the minimizer $x^*$ are the book's standing assumptions and appear as hypotheses. $R>0$, $L>0$ and $\alpha>0$ are explicit, because Lean's division by zero would otherwise turn the step size into a junk value.

The book assumes $\|g\|\le L$ for every subgradient at every point of $\mathcal X$. With subgradients relative to a compact $\mathcal X$, that assumption can never hold at a boundary point, since every outward normal can be added to a subgradient. Stated that way the theorems would be vacuous. The mission therefore assumes the bound only for the subgradients $g_1,\dots,g_t$ that the run uses. This is a weaker hypothesis and gives a stronger, non-vacuous statement. Bounding only these subgradients is a deliberate choice, not a trivialization: the bound still constrains every quantity the conclusion depends on.

Contributions welcome: proofs of the four inequalities and of the two rates, and a reusable lemma that the convex combination of finitely many points of a convex set lies in the set, together with Jensen's inequality in the form used here.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. https://arxiv.org/abs/1405.4980
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.
• S. Lacoste-Julien, M. Schmidt and F. Bach, A simpler approach to obtaining an O(1/t) convergence rate for the projected stochastic subgradient method, 2012. https://arxiv.org/abs/1212.2002
• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer, 1985. https://doi.org/10.1007/978-3-642-82118-9

Motivation

Local Rademacher averages measure the complexity of a learning problem only near the functions that matter, such as those with small empirical error, rather than over the whole function class. Bartlett, Bousquet and Mendelson (Local Rademacher complexities, Ann. Statist. 33 (2005)) show that error bounds for empirical risk minimization are governed by the fixed point of a sub-root upper bound on such local averages, and that these bounds give fast rates ($1/n$ rather than $1/\sqrt n$) under variance conditions. A bound is only useful in practice if it can be computed from the data. For classification with the discrete loss, the paper's Corollary 6.2 states the bound in terms of a localized empirical Rademacher average $\hat\psi_n(r)$. That average is a supremum over a constrained subclass, and it is not obvious how to evaluate it.

Theorem 6.3 of the paper answers this. An upper bound on $\hat\psi_n(r)$ can be computed by any algorithm that minimizes a weighted empirical classification error. A similar reduction was known for the global Rademacher average of a classification class: Bartlett, Boucheron and Lugosi (Model selection and error estimation, Machine Learning 48 (2002)) observed that the empirical Rademacher average equals one half minus an expected empirical risk minimum with random labels, and Lemma 6.4 of the paper is adapted from their argument. Theorem 6.3 shows that localization and the use of star-hulls keep this reduction intact.

Setting

Fix inputs $X_1,\dots,X_n$ in a set $\mathcal X$ ($n\ge1$) and labels $Y_1,\dots,Y_n\in\{-1,1\}$. Everything below is deterministic given this sample. A classifier is a function $f:\mathcal X\to\{-1,1\}$, and $\mathcal F$ is a class of classifiers. The discrete loss is $\ell(y,y')=\mathbf 1[y\ne y']$. For a vector $z\in\mathbb R^n$ write

$$P_n\ell(f(X),z)=\frac1n\sum_{i=1}^n\ell(f(X_i),z_i),\qquad P_n\ell_f=P_n\ell(f(X),Y),$$

so $P_n\ell_f$ is the empirical risk of $f$.

A sign vector $\sigma\in\{-1,1\}^n$ plays the role of Rademacher signs, and $\mathbb E_\sigma$ is the average over all $2^n$ sign vectors. The empirical Rademacher average of the loss functions of the classifiers with empirical risk at most $b$ is

$$\mathbb E_\sigma R_n\{\ell_f : f\in\mathcal F,\ P_n\ell_f\le b\}=\frac1n\,\mathbb E_\sigma\sup_{f\in\mathcal F,\ P_n\ell_f\le b}\ \sum_{i=1}^n\sigma_i\,\ell(f(X_i),Y_i).$$

For $c\ge0$, $x>0$ and $0<r\le1/2$, the empirical local Rademacher complexity of the classification loss class is

$$\hat\psi_n(r)=c\sup_{\alpha\in[\sqrt{2r},1]}\alpha\,\mathbb E_\sigma R_n\{\ell_f : f\in\mathcal F,\ P_n\ell_f\le 2r/\alpha^2\}+\frac{26x}{n}.$$

In Corollary 6.2, $c=20$. The parameter $\alpha$ comes from the star-hull of the loss class: rescaling a loss function by $\alpha$ turns the constraint $P_n(\alpha\ell_f)^2\le 2r$ into $P_n\ell_f\le 2r/\alpha^2$.

For a sign vector $\sigma$ and a multiplier $\mu\ge0$, the weighted empirical risk minimum is

$$J(\mu)=\min_{f\in\mathcal F}\frac1n\sum_{i=1}^n|\sigma_i+\mu Y_i|\,\ell\big(f(X_i),\operatorname{sign}(\sigma_i+\mu Y_i)\big).$$

It is the smallest weighted training error when the labels are corrupted to $\operatorname{sign}(\sigma_i+\mu Y_i)$ and example $i$ has weight $|\sigma_i+\mu Y_i|$.

Formalization targets

Goal: Theorem 6.3

If some $f\in\mathcal F$ has $P_n\ell_f\le 2r$, then

$$\hat\psi_n(r)\le c\sup_{\alpha\in[\sqrt{2r},1]}\alpha\,\mathbb E_\sigma\min_{\mu\ge0}\Big(\Big(\frac{2r}{\alpha^2}-\frac12\Big)\mu+\frac1{2n}\sum_{i=1}^n|\sigma_i+\mu Y_i|-J(\mu)\Big)+\frac{26x}{n}.$$

The multiplier $c$ is kept general, and the term $26x/n$ appears on both sides as printed.

Milestones

1. Lemma 6.4. For every $b\in[0,1]$ with a feasible classifier,

$$\mathbb E_\sigma R_n\{\ell_f : f\in\mathcal F,\ P_n\ell_f\le b\}=\frac12-\mathbb E_\sigma\min\{P_n\ell(f(X),\sigma) : f\in\mathcal F,\ P_n\ell(f(X),Y)\le b\}.$$

2. Weak duality (proof of Theorem 6.3). With $L(f,\mu)=P_n\ell(f(X),\sigma)+\mu(P_n\ell(f(X),Y)-2r/\alpha^2)$ and $g(\mu)=\min_{f\in\mathcal F}L(f,\mu)$, for every $\mu\ge0$,

$$\min\{P_n\ell(f(X),\sigma) : f\in\mathcal F,\ P_n\ell(f(X),Y)\le 2r/\alpha^2\}\ge g(\mu).$$

3. The identity for $g(\mu)$ (proof of Theorem 6.3, corrected).

$$g(\mu)=J(\mu)-\frac1{2n}\sum_{i=1}^n|\sigma_i+\mu Y_i|+\frac{1+\mu}2-\mu\frac{2r}{\alpha^2}.$$

Significance

The theorem turns a quantity defined by a supremum over a data-dependent subclass into one computable by a standard learning primitive. For each sign vector and each multiplier $\mu$, $J(\mu)$ is the value of a weighted classification problem, which any weighted empirical risk minimizer solves. The expectation over signs can be estimated by repeated sampling. The paper notes that $J$ is Lipschitz in $\mu$, so a finite grid of $\mu$ values suffices, and that a sub-root upper bound on $\hat\psi_n$ can then be read off. Combined with Corollary 6.2, this yields error bounds for empirical risk minimization in classification that are computable from the training data and that localize: they depend only on the classifiers with small empirical error.

The result is proved in the paper. It has not been formalized; as far as a search of the Prove2Me catalog shows, neither the classification loss class nor $J(\mu)$ exists as a formal object. This mission produces machine-checked statements of the theorem and of its three proof steps. These cover the exact identity between Rademacher averages of the discrete loss class and random-label empirical risk minimization, and a Lagrangian duality bound for constrained empirical risk minimization.

Difficulty

The obvious route is to apply Lemma 6.4 and then exchange the constrained minimum for a Lagrangian. Each step has a point where a careless argument fails.

• Lemma 6.4 needs a change of variables on sign vectors ($\sigma_i\mapsto-Y_i\sigma_i$) that preserves the uniform average. It also needs the identity $\ell(y,y')=|y-y'|/2$ on $\{\pm1\}$, which fails off $\{\pm1\}$.
• The Lagrangian step gives only weak duality. The bound is an inequality, and attempts to prove equality in Theorem 6.3 fail in general.
• The identity for $g(\mu)$ rests on $\ell(y,\hat y)=(1-y\hat y)/2$. This holds only for $\pm1$ arguments, while $\operatorname{sign}(\sigma_i+\mu Y_i)$ is $0$ when $\mu=1$ and $\sigma_i=-Y_i$. Those terms carry weight zero, and the bookkeeping has to show this.
• Passing the per-$\alpha$, per-$\sigma$ inequalities through the outer supremum and the average requires every supremum and minimum to be over a nonempty, bounded set. This is where the feasibility hypothesis is used.

Formalization scope

• Representation. Inputs are xs : Fin n → X for an arbitrary type X. Labels and signs are real vectors Fin n → ℝ. Classifiers are functions X → ℝ with values in $\{\pm1\}$, a class is a Set (X → ℝ), and the discrete loss is defined on all real pairs. Sign vectors are indexed by Fin n → Bool through the published UnderstandingML.signVec. Every $\mathbb E_\sigma$, on both sides of every statement, is the finite average over these $2^n$ vectors; no probability measure is used. The empirical Rademacher average is the published UnderstandingML.rademacher applied to the set of loss vectors.
• Suprema and minima. Every supremum and minimum is Lean's real ⨆/⨅ over a subtype. The hypotheses make each index set nonempty and each family bounded, so these are true suprema and minima. The convention Real.sign 0 = 0 is used where the paper's sign is undefined; it affects only weight-zero terms.
• Added hypotheses. Each of these is implicit on the page:
  • $n\ge1$;
  • $c\ge0$ (for $c<0$ the inequality reverses);
  • $0<r\le1/2$ (otherwise the range of $\alpha$ is empty);
  • $x>0$ (Corollary 6.2's "fix $x>0$");
  • a classifier with $P_n\ell_f\le 2r$ in the goal, and a feasible classifier in Lemma 6.4 and in the weak duality step (the page's minima presuppose one);
  • a nonempty $\mathcal F$ in the $g(\mu)$ identity.
• Corrections of the print. The last display of the proof on p. 30 ends each line with $-2r/\alpha^2$. From the page's own definition $g(\mu)=\min_f L(f,\mu)$, the constant is $-\mu\,2r/\alpha^2$, which is the form Theorem 6.3's term $(2r/\alpha^2-1/2)\mu$ requires. The milestone states the corrected identity.
• No trivialization. Without the feasibility hypothesis, Lean would evaluate the empty-class Rademacher average and the unbounded $\mu$-minimum to the junk value $0$, and the goal would compare junk values. The feasibility hypothesis rules this out. The goal is the inequality between the two expressions for $\hat\psi_n$ as printed; it is not restated through $g(\mu)$, $L(f,\mu)$ or Lemma 6.4.
• Contributions welcome. A reusable lemma that the uniform average over $\{\pm1\}^n$ is invariant under coordinatewise sign flips would serve beyond this mission, as would general facts about real infima over finite-valued families. Proofs of the three milestones, and of the goal from them, are the main targets.

Selected references

• P. L. Bartlett, O. Bousquet, S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 1497–1537, 2005. arXiv:math/0508275v1 (cited version): https://arxiv.org/abs/math/0508275, DOI https://doi.org/10.1214/009053605000000282 — §6.2, Corollary 6.2 and Theorem 6.3 (pp. 28–29), Lemma 6.4 (p. 29), proof of Theorem 6.3 (p. 30).
• P. L. Bartlett, S. Boucheron, G. Lugosi, Model selection and error estimation, Machine Learning 48, 85–113, 2002. https://doi.org/10.1023/A:1013999503812
• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian complexities: risk bounds and structural results, Journal of Machine Learning Research 3, 463–482, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 26 (the Rademacher complexity reused here). https://doi.org/10.1017/CBO9781107298019