Optimization

Motivation

Many first-order methods for convex minimization — the forward–backward (proximal gradient) method, alternating minimization, trust-region and majorization–minimization schemes — produce sequences that decrease the objective by an amount proportional to the squared step and whose step controls a subgradient at the new point. Luo and Tseng (Ann. Oper. Res. 1993) used such conditions together with error bounds to derive convergence rates, and Attouch, Bolte and Svaiter (Math. Program. 2013) isolated them as an abstract definition of descent sequences analysed through the Kurdyka–Łojasiewicz (KL) inequality. Those analyses give convergence and asymptotic rates, but not explicit complexity bounds with the constants in view.

Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234; Math. Program. 165, 2017) show that, for convex functions, the KL inequality yields such bounds: the values and iterates of every subgradient descent sequence are dominated by an explicit one-dimensional proximal recursion built from the desingularizing function. This is the paper's main theorem (Theorem 16), and the target of this mission.

Setting

Let $H$ be a real Hilbert space and $f : H \to (-\infty, +\infty]$ proper, lower semicontinuous and convex, with $\operatorname{argmin} f \neq \emptyset$ and, after a shift, $\min f = 0$. The subdifferential is

$$\partial f(x) = \{u \in H : f(y) \ge f(x) + \langle u, y - x\rangle \ \text{for all } y\},$$

and $\partial^0 f(x)$ denotes its least-norm element, with $\|\partial^0 f(x)\| = +\infty$ when $\partial f(x) = \emptyset$.

For $\bar r > 0$, the class $\mathcal K(0, \bar r)$ consists of the functions $\varphi$ continuous on $[0, \bar r)$ and $C^1$ on $(0, \bar r)$ with $\varphi(0) = 0$, $\varphi$ concave and $\varphi' > 0$. The function $f$ has the KL property on $[0 < f < \bar r]$ with desingularizing function $\varphi \in \mathcal K(0, \bar r)$ if

$$\varphi'(f(x))\,\|\partial^0 f(x)\| \ge 1 \qquad \text{whenever } 0 < f(x) < \bar r.$$

A sequence $(x_k)_{k \in \mathbb N}$ is a subgradient descent sequence with constants $a, b > 0$ if $x_0 \in \operatorname{dom} f$ and, for every $k \ge 1$,

• (H1) $f(x_k) + a\|x_k - x_{k-1}\|^2 \le f(x_{k-1})$;
• (H2) some $\omega_k \in \partial f(x_k)$ satisfies $\|\omega_k\| \le b\|x_k - x_{k-1}\|$.

Fix $0 < r_0 < \bar r$, put $\alpha_0 = \varphi(r_0)$, and let $\psi = (\varphi|_{[0, r_0]})^{-1} : [0, \alpha_0] \to [0, r_0]$, an increasing convex profile. Assumption (A): $\psi'$ is Lipschitz continuous on $[0, \alpha_0]$ with constant $\ell > 0$, and $\psi'(0) = 0$. With

$$\zeta = \frac{\sqrt{1 + 2\ell a b^{-2}} - 1}{\ell} > 0, \qquad \alpha_{k+1} = \operatorname{argmin}\Big\{\psi(u) + \tfrac{1}{2\zeta}(u - \alpha_k)^2 : u \ge 0\Big\},$$

$(\alpha_k)$ is the one-dimensional worst-case proximal sequence.

Formalization targets

Goal: Theorem 16

If $(x_k)$ is a subgradient descent sequence with $f(x_0) = r_0$ and (A) holds, then $x_k$ converges strongly to a minimizer $x^*$ and

$$f(x_k) \le \psi(\alpha_k) \quad (k \ge 0), \qquad \|x_k - x^*\| \le \frac{b}{a}\,\alpha_k + \sqrt{\frac{\psi(\alpha_{k-1})}{a}} \quad (k \ge 1).$$

Milestones

1. (20), in the proof of Theorem 14: while $f(x_k) > 0$ and $x_k \neq x_{k-1}$, $\varphi(f(x_k)) - \varphi(f(x_{k+1})) \ge \frac{a}{b}\big(2\|x_k - x_{k+1}\| - \|x_{k-1} - x_k\|\big)$.
2. Theorem 14: with only $f(x_0) \le r_0 < \bar r$, $x_k \to x^* \in \operatorname{argmin} f$ strongly and $\|x_k - x^*\| \le \frac{b}{a}\varphi(f(x_k)) + \sqrt{f(x_{k-1})/a}$ for $k \ge 1$.
3. (23): $(\alpha_k)$ exists, is positive, satisfies $\alpha_{k+1} = (I + \zeta\psi')^{-1}(\alpha_k)$, decreases strictly to $0$, and $\psi(\alpha_k) \to 0$.
4. (27): with $\beta_j = \varphi(f(x_j))$, every $k \ge 1$ with $f(x_k) > 0$ has $(\beta_{k-1} - \beta_k)/\psi'(\beta_k) \ge \zeta$.
5. Claim 1: for $\lambda^0 > \lambda^1 > 0$ and $\gamma > 0$, $(I + \lambda^0\psi')^{-1}(\gamma) < (I + \lambda^1\psi')^{-1}(\gamma)$.
6. Claim 2: proximal sequences with step sizes $\lambda^0_k \ge \lambda^1_k > 0$ from a common start in $(0, \alpha_0]$ satisfy $\beta^0_k \le \beta^1_k$.

Significance

Theorem 16 turns the qualitative KL convergence theory into explicit complexity: once a desingularizing function is known, the number of iterations needed to reach a given accuracy, for both the values and the iterates, can be read off a scalar recursion with constants $a$, $b$, $\ell$ taken from the method and the function. The authors apply it, through its corollaries, to obtain the linear rate of ISTA for $\ell^1$-regularized least squares and complexity bounds for projection methods for convex feasibility problems. The bound on $\|x_k - x^*\|$ holds even when $f$ has a continuum of minimizers.

The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. This mission asks for a Lean proof of Theorem 16 and of the six intermediate results its proof uses, each stated with the paper's exact constants.

Difficulty

The convergence part (Theorem 14) is set in an arbitrary Hilbert space: summability of the steps gives only a Cauchy sequence, identifying its limit as a minimizer needs a closedness property of $\partial f$ that is not available in Mathlib for EReal-valued functions, and the degenerate cases ($x_k = x_{k-1}$ or $f(x_k) = 0$ at some step) need separate treatment.

The complexity part requires one-dimensional analysis that Mathlib does not package: derivatives of the inverse $\psi = \varphi^{-1}$ on a closed interval, a descent inequality for $\psi$ when $\psi'$ is Lipschitz only on $[0, \alpha_0]$, and monotonicity of the scalar resolvents $(I + \lambda\psi')^{-1}$. The obvious approach, comparing $f(x_k)$ with $\psi(\alpha_k)$ one step at a time with the same step size, fails: the sequence $\varphi(f(x_k))$ is itself a proximal sequence for $\psi$, but with step sizes that vary with $k$ and are not known in advance.

Formalization scope

• $f$ is a function $H \to$ EReal satisfying the published GammaZero (never $-\infty$, somewhere finite, convex epigraph, lower semicontinuous), with CompleteSpace H. $\partial f$ is the published subgrad; $\min f = 0$ with $\operatorname{argmin} f \neq \emptyset$ is the hypothesis "$f \ge 0$ and $f$ vanishes somewhere".
• The KL inequality is required for every $v \in \partial f(x)$, which is the least-norm form with the convention $\|\partial^0 f(x)\| = +\infty$ off $\operatorname{dom}\partial f$. The class $\mathcal K(0, \bar r)$ is the published IsDesingularizer; $\varphi'$ is deriv φ, used only on $(0, \bar r)$.
• $\psi$ is a real function given as data with $\psi(\varphi(s)) = s$ on $[0, r_0]$; only its values on $[0, \alpha_0]$ matter. $\psi'$ is the derivative within $[0, \alpha_0]$, and the minimization in (22) runs over $[0, \alpha_0]$, the domain of $\psi$. The argmin is unique, so (22) is a predicate on sequences; (23) proves that the predicate is satisfiable, so Theorem 16 is not vacuous. Resolvent points $(I + \lambda\psi')^{-1}(\gamma)$ are likewise predicates.
• $\alpha_0 = \varphi(r_0)$, $\zeta$ and the coefficient $b/a$ are fixed by the data; none is existentially quantified. The inequality $f(x_k) \le \psi(\alpha_k)$ is stated in EReal.
• Claim 2 is printed with $\beta^0_0 = \beta^1_0 \in (0, r_0]$; the resolvents act on $[0, \alpha_0]$ and the claim is applied with $\beta_0 = \alpha_0$, so it is formalized on $(0, \alpha_0]$.
• Theorem numbers, equation numbers and pages refer to the arXiv version arXiv:1510.08234v3, not to the journal version.

Useful infrastructure, reusable beyond this mission: the inverse-function derivative on an interval, the one-dimensional descent lemma with a derivative Lipschitz on a closed interval, and monotonicity of scalar resolvents. Contributions of these as separate lemmas are welcome.

Selected references

• J. Bolte, T. P. Nguyen, J. Peypouquet, B. W. Suter, From error bounds to the complexity of first-order descent methods for convex functions, Math. Program. 165 (2017) 471–507. arXiv:1510.08234v3, doi:10.1007/s10107-016-1091-6
• H. Attouch, J. Bolte, B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137 (2013) 91–129. doi:10.1007/s10107-011-0484-9
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46 (1993) 157–178. doi:10.1007/BF02096261
• J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17 (2007) 1205–1223. doi:10.1137/050644641

Motivation

Accelerated gradient methods use information from earlier iterates to reduce the objective gap of a smooth convex optimization problem faster than ordinary gradient descent. Their behavior depends on the precise momentum rule. Attouch, Chbani, Fadili, and Riahi study a discrete rule with an additional difference of consecutive gradients, motivated by an inertial differential equation with Hessian driven damping. This mission concerns their inertial gradient algorithm with Hessian damping, called IGAHD, and the rates proved for it in Theorem 6 of the source paper. The result matters when one wants a rate for objective values together with control of the gradients seen during the run.

The paper appeared as a 2020 preprint and subsequently in Mathematical Programming. The mission follows the pinned arXiv version, whose theorem and equation numbers supply all citations here. The proximal and strongly convex algorithms elsewhere in the paper have separate missions; their dynamics and rate statements differ from IGAHD.

Setting

Let $H$ be a real Hilbert space and let $f:H\to\mathbb R$ be convex and differentiable. Assume that its gradient $\nabla f$ is $L$-Lipschitz: $\|\nabla f(u)-\nabla f(v)\|\le L\|u-v\|$ for every $u,v\in H$, where $L>0$. Choose a minimizer $x^*$, so $f(x^*)=\min_H f$. The positive step size $s$ satisfies $s\le1/L$. The momentum parameter $\alpha$ is at least $3$, and the damping parameter $\beta$ lies in $[0,2\sqrt{s})$.

Given $x_0,x_1\in H$, the algorithm takes the following two steps for every integer $k\ge1$:

$$\begin{aligned} y_k={}&x_k+\left(1-\frac{\alpha}{k}\right)(x_k-x_{k-1}) -\beta\sqrt{s}\bigl(\nabla f(x_k)-\nabla f(x_{k-1})\bigr) -\frac{\beta\sqrt{s}}{k}\nabla f(x_{k-1}),\\ x_{k+1}={}&y_k-s\nabla f(y_k). \end{aligned}$$

The paper sets $t_{k+1}=k/(\alpha-1)$ and $v_k=x_{k-1}-x^*+t_k(x_k-x_{k-1}+\beta\sqrt{s}\nabla f(x_{k-1}))$. Its Lyapunov quantity is $E_k=t_k^2(f(x_k)-f(x^*))+(2s)^{-1}\|v_k\|^2$ for $k\ge1$. These expressions are fixed by the source formulas (14)–(15), p. 15, not chosen to simplify a later proof.

Formalization targets

The central target is the full rate statement of Theorem 6. In the range where the paper's monotonicity argument applies, $E_k$ is eventually nonincreasing. For every IGAHD run,

$$f(x_k)-\min_H f=O(k^{-2})\quad(k\to\infty).$$

When $\beta>0$, the theorem also gives both weighted gradient summability claims:

$$\sum_{k\ge0} k^2\|\nabla f(y_k)\|^2<\infty, \qquad \sum_{k\ge0} k^2\|\nabla f(x_k)\|^2<\infty.$$

The milestone list follows claims the authors state while proving that target. It begins with the extended descent inequality (Lemma 1, (28)), records the identities for $t_k$ and $v_k$, and then captures the displayed energy and $\varepsilon$ inequalities. Remark 4 asks for the $O(k^{-3})$ bound on the smallest squared gradient norm among the first $k$ iterates; Remark 5 asks for the $O(k^{-2})$ objective gap at $y_k$. Those are companion statements and are not substituted for the main theorem.

Significance

The rate bounds give three kinds of information about one trajectory. The objective gap controls the values attained at the iterates. The two summable series imply that the gradients at both the extrapolated points and the iterates become small in a weighted aggregate sense when damping is positive. The paper then uses this series estimate to derive the best-iterate estimate of Remark 4 and the extrapolated-value estimate of Remark 5, all on p. 18.

The result is proved in the cited paper; the open work here is its Lean proof and the supporting smooth convex analysis. The development makes the precise discrete algorithm, the Lyapunov quantity, and the descent inequality reusable as mathematical interfaces. A complete formal proof would also make explicit where the author's finite-index monotonicity wording needs correction.

Difficulty

The usual smooth descent estimate alone gives a decrease after one gradient step, but the extrapolated point $y_k$ also carries a momentum term and a gradient difference. Its objective value is therefore not the same quantity as $f(x_k)$, and a direct comparison of successive objective values does not give the claimed summability. The source uses a stronger descent inequality with a squared difference of gradients. The energy change then contains a quadratic expression in $\nabla f(y_k)$ and $\nabla f(x_k)$ whose sign depends on $\beta<2\sqrt{s}$ and, at first, on how large $k$ is. Establishing that sign uniformly over the relevant tail of the run is the central obstruction.

Formalization scope

The Lean space is a complete real inner product space. Convexity is ConvexOn ℝ Set.univ f; differentiability is explicit because the phrase “whose gradient is $L$-Lipschitz” presupposes a gradient. The existence of a minimizer is represented by a selected $x^*$ with $f(x^*)\le f(z)$ for every $z$. Positive $L$ and positive $s$ make $s\le1/L$ meaningful. The algorithm is a predicate on sequences $x,y:\mathbb N\to H$, imposed from $k=1$ so no coefficient is divided by zero. The first two $x$ terms are free, and $y_0$ is unused. The $O$ statements use the filter at infinity, so finite initial terms do not affect them; summability uses the ordinary series over natural indices.

The printed claim that $(E_k)$ is nonincreasing from its first term is false for the paper's own definitions. On $H=\mathbb R$ with $f(u)=u^2/2$, $L=s=1$, $\alpha=3$, $\beta=0$, $x_0=0$, and $x_1=1$, one gets $E_1=0$ and $E_2=1/8$. The formal goal keeps eventual monotonicity, as supported by the proof on pp. 16–18. This correction is disclosed rather than treated as a new hypothesis. No energy decrease, gradient bound, or conclusion is assumed in the run predicate. The milestone definitions also specify $B_k$ exactly as on p. 17. Contributions to the goal, to the extended descent lemma, or to the explicit energy estimates are all useful; the definition layer and smooth convex lemmas can serve later optimization formalizations.

Selected references

• H. Attouch, Z. Chbani, J. Fadili, and H. Riahi, First-order optimization algorithms via inertial systems with Hessian driven damping, Mathematical Programming, 2020; arXiv:1907.10536v2, especially §3.2, pp. 15–18, and Appendix A.1, p. 34.

Motivation

Accelerated first-order methods for convex minimization, such as Nesterov's method and Polyak's heavy ball method, are now routinely studied through their continuous-time limits: second-order differential equations whose trajectories descend toward a minimizer. In the time-continuous setting the convergence analysis is a Lyapunov argument, and a good Lyapunov function for the ODE usually suggests one for the algorithm obtained by discretizing it.

Attouch, Chbani, Fadili and Riahi (arXiv:1907.10536v2, Math. Program. 2020) study inertial dynamics with Hessian-driven damping: besides the viscous friction term $\gamma\dot x$, the equation contains a term $\beta\nabla^2 f(x(t))\dot x(t)$, which equals $\beta\frac{d}{dt}\nabla f(x(t))$. This damping is known to reduce the oscillations of the heavy ball trajectory, and because it is a time derivative of the gradient, explicit and implicit time discretizations of it produce first-order algorithms with no Hessian evaluation. This mission covers the strongly convex continuous-time result of the paper, Theorem 7 (§4.1, pp. 19–21). For $\beta=0$ it reduces to the heavy ball equation with friction $2\sqrt\mu$, whose exponential rate is due to Siegel (arXiv:1903.05671, Theorem 2.2), as the paper's Remark 7 records. For $\beta>0$, Remark 7 points to a result on a related but different dynamical system by Wilson, Recht and Jordan (arXiv:1611.02635, Theorem 1), whose rate is slightly worse. The algorithms (IPAHD-SC) and (IGAHD-SC) of §5 of the paper are the discrete counterparts of this theorem.

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $f:\mathcal H\to\mathbb R$ be a convex function of class $\mathcal C^2$, with gradient $\nabla f$ and Hessian $\nabla^2 f$. For $\mu>0$, $f$ is $\mu$-strongly convex (Definition 1) if $f-\frac\mu2\|\cdot\|^2$ is convex. Such an $f$ is assumed to have a minimizer $x^\star$, and $\min_{\mathcal H} f=f(x^\star)$.

Fix $t_0>0$ and a real constant $\beta$. A solution trajectory of

$$\ddot x(t)+2\sqrt{\mu}\,\dot x(t)+\beta\nabla^2 f(x(t))\dot x(t)+\nabla f(x(t))=0 \tag{19}$$

is a twice differentiable map $x:[t_0,+\infty[\to\mathcal H$ satisfying the equation at every $t\ge t_0$. This is the dynamic $(\mathrm{DIN})_{\gamma,\beta}$ of the paper with the constant viscous damping $\gamma=2\sqrt\mu$.

The proof uses two auxiliary functions. The first is the Lyapunov function

$$\mathcal E(t)=f(x(t))-\min_{\mathcal H}f+\tfrac12\big\|\sqrt\mu(x(t)-x^\star)+\dot x(t)+\beta\nabla f(x(t))\big\|^2 .$$

The second is $Z(t)=2\beta(f(x(t))-f(x^\star))+\sqrt\mu\|x(t)-x^\star\|^2$. Both appear in the milestones under the names lyap and Zfun.

Formalization targets

Goal: Theorem 7 (p. 19)

Assume $0\le\beta\le\frac1{2\sqrt\mu}$. Then three statements hold. First, for all $t\ge t_0$,

$$\frac\mu2\|x(t)-x^\star\|^2\le f(x(t))-\min_{\mathcal H}f\le C e^{-\frac{\sqrt\mu}{2}(t-t_0)},\qquad C:=f(x(t_0))-\min_{\mathcal H}f+\mu\|x(t_0)-x^\star\|^2+\|\dot x(t_0)+\beta\nabla f(x(t_0))\|^2 .$$

Second, there is $C_1>0$ such that for all $t\ge t_0$

$$e^{-\sqrt\mu t}\int_{t_0}^t e^{\sqrt\mu s}\|\nabla f(x(s))\|^2\,ds\le C_1e^{-\frac{\sqrt\mu}{2}t}.$$

Third,

$$\int_{t_0}^\infty e^{\frac{\sqrt\mu}{2}t}\|\dot x(t)\|^2\,dt<+\infty .$$

Milestones

The milestones are the displayed steps of the paper's proof, in order:

1. the strong convexity inequality $\langle\nabla f(y),y-x^\star\rangle\ge f(y)-f(x^\star)+\frac\mu2\|y-x^\star\|^2$;
2. the first differential inequality for $\mathcal E$;
3. the nonnegativity of $\frac\mu4X^2+\frac{\beta}{2\sqrt\mu}Y^2-\beta\sqrt\mu XY$;
4. $\frac{d}{dt}\mathcal E+\frac{\sqrt\mu}2\mathcal E+\frac{\sqrt\mu}2\|\dot x\|^2\le0$;
5. $\mathcal E(t)\le\mathcal E(t_0)e^{-\frac{\sqrt\mu}2(t-t_0)}$;
6. the differential inequality for $Z$.

Companion: the case $\beta=0$

The last sentence of Theorem 7 states that for $\beta=0$, $f(x(t))-\min f=\mathcal O(e^{-\sqrt\mu t})$. The paper gives no proof of it and attributes it to Siegel. It is a separate item, listed as the last milestone, and is not part of the goal.

Significance

Theorem 7 gives exponential decay, at the rate $e^{-\frac{\sqrt\mu}2 t}$, of the values and of the distance to the minimizer for the whole range $0\le\beta\le1/(2\sqrt\mu)$ of Hessian damping. It also gives an averaged exponential decay of $\|\nabla f(x(t))\|^2$, which the authors describe as new in the literature, and weighted integrability of the squared velocity. These estimates guide the design of the strongly convex algorithms of §5, whose linear rates $q=1/(1+\frac12\sqrt{\mu s})$ mirror the continuous rate.

Formalizing it builds machine-checked continuous-time Lyapunov arguments in a Hilbert space: differentiation of energy functions along a trajectory that is only one-sidedly differentiable at $t_0$, the chain rule through $\nabla f$ (the Hessian term), and Grönwall-type integration of differential inequalities. To our knowledge none of Theorem 7 has a machine-checked proof; the paper's proof is complete apart from the gap at $\beta=0$ in part (ii) noted under Difficulty.

Difficulty

The algebra of the first differential inequality is a direct but long expansion, and the quadratic form is where the upper bound on $\beta$ enters. The main analytic steps are elsewhere. First, the energy must be shown differentiable along the trajectory, which requires the derivative of $t\mapsto\nabla f(x(t))$, a chain rule through the Fréchet derivative of the gradient. Second, the differential inequalities must be integrated on $[t_0,+\infty[$ with one-sided derivatives at $t_0$. Third, part (ii) must be derived from the $Z$-inequality. The paper's derivation divides by $\beta^2$, so it covers only $\beta>0$. At $\beta=0$ part (ii) is still true, but it needs a separate argument, for example local Lipschitz continuity of $\nabla f$ near $x^\star$ together with the convergence $x(t)\to x^\star$ from part (i). A proof that only follows the printed text does not cover the case $\beta = 0$.

Formalization scope

• Space and function. $\mathcal H$ is a real inner product space that is complete. $f$ is ConvexOn ℝ univ and ContDiff ℝ 2, $\nabla f$ is Mathlib's gradient f, and the Hessian applied to $v$ at $x$ is fderiv ℝ (gradient f) x v.
• Strong convexity is Definition 1 verbatim, with $\mu>0$ as a separate hypothesis. Convexity of $f$ is kept from the standing hypothesis (H) of p. 2 even though strong convexity implies it.
• The minimizer. $\operatorname{argmin}f\neq\emptyset$ is a point xstar with $f(x^\star)\le f(y)$ for all $y$. $\min f$ is written f xstar.
• The trajectory is a triple $x,\dot x,\ddot x:\mathbb R\to\mathcal H$. At every $t\ge t_0$, $x$ has derivative $\dot x(t)$ and $\dot x$ has derivative $\ddot x(t)$ within $[t_0,+\infty[$, and (19) holds. Values before $t_0$ play no role, and $\dot x(t_0)$ in the constant $C$ is the right derivative. $\beta$ is a real constant and $t_0>0$, as in (H).
• Derivatives in milestones are stated as the existence of a number that is the one-sided derivative and satisfies the inequality. Such a number is unique.
• Integrals. Part (ii) is an interval integral of a function continuous on $[t_0,t]$. The "Moreover" clause is stated as integrability on $[t_0,+\infty[$ of the nonnegative integrand. The constant $C_1$ is existentially quantified after the trajectory, so it may depend on it, as on the page.
• Ruling out trivial readings. The goal never mentions $\mathcal E$ or $Z$: its conclusions are about $f(x(t))$, $\|x(t)-x^\star\|$, $\nabla f(x(t))$ and $\dot x(t)$ only. The solution predicate is satisfiable: the constant trajectory at $x^\star$ satisfies it.
• Infrastructure needed: the chain rule for $\nabla f\circ x$ with one-sided derivatives, differentiation of $\|\cdot\|^2$ and $\langle\cdot,\cdot\rangle$ along curves, and a Grönwall-type lemma $u'\le-cu\Rightarrow u(t)\le u(t_0)e^{-c(t-t_0)}$ on $[t_0,\infty)$ with one-sided derivatives. These are reusable for the other continuous-time missions of the series. Contributions of these general lemmas are welcome as separate theorems.

Selected references

• H. Attouch, Z. Chbani, J. Fadili, H. Riahi, First-order optimization algorithms via inertial systems with Hessian driven damping, Math. Program. (2020); arXiv:1907.10536v2. https://arxiv.org/abs/1907.10536
• J. W. Siegel, Accelerated first-order methods: differential equations and Lyapunov functions, 2019. https://arxiv.org/abs/1903.05671
• A. C. Wilson, B. Recht, M. I. Jordan, A Lyapunov analysis of momentum methods in optimization, J. Mach. Learn. Res. 22 (2021); arXiv:1611.02635. https://arxiv.org/abs/1611.02635
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Comput. Math. Math. Phys. 4 (1964). https://doi.org/10.1016/0041-5553(64)90137-5

Motivation

Regularized loss minimization covers support vector machines, logistic and ridge regression, and the absolute-deviation regression of robust statistics. Stochastic dual coordinate ascent (SDCA) solves these problems by maximizing the Fenchel dual one randomly chosen coordinate at a time. Shalev-Shwartz and Zhang (arXiv:1209.1873, JMLR 2013) gave the first analysis of SDCA in terms of the duality gap. For smooth losses their rate is linear; for Lipschitz but non-smooth losses such as the hinge loss it is of order $1/\epsilon$, which is no better than stochastic gradient descent, although SDCA is observed to converge much faster than SGD on SVM problems asymptotically.

Section 5 of the paper explains that observation. Many non-smooth losses are smooth at most points: the hinge loss $\max(0,1-uy_i)$ fails to be smooth only at $uy_i=1$. If, at the optimum, most margins stay away from the kink, the dual is strongly concave in most coordinates, and SDCA converges linearly in the dual objective. Earlier linear-rate results for dual coordinate ascent on SVMs (Luo and Tseng, 1992) depend on the smallest nonzero eigenvalue of the data Gram matrix, which can be arbitrarily small when two data points are close; the condition of Section 5 avoids the Gram matrix.

Setting

Data $x_1,\dots,x_n\in\mathbb R^d$ (Euclidean norm), scalar convex losses $\varphi_1,\dots,\varphi_n:\mathbb R\to\mathbb R$ and $\lambda>0$ define the primal problem

$$\min_{w\in\mathbb R^d} P(w),\qquad P(w)=\frac1n\sum_{i=1}^n\varphi_i(w^\top x_i)+\frac\lambda2\|w\|^2 .$$

The convex conjugate of $\varphi_i$ is $\varphi_i^*(u)=\sup_z(zu-\varphi_i(z))\in(-\infty,+\infty]$. The dual problem is $\max_{\alpha\in\mathbb R^n}D(\alpha)$ with

$$D(\alpha)=\frac1n\sum_{i=1}^n-\varphi_i^*(-\alpha_i)-\frac\lambda2\|w(\alpha)\|^2,\qquad w(\alpha)=\frac{1}{\lambda n}\sum_{i=1}^n\alpha_ix_i .$$

A dual variable is feasible when every $\varphi_i^*(-\alpha_i)$ is finite. A function is $L$-Lipschitz if $|\varphi_i(a)-\varphi_i(b)|\le L|a-b|$. The standing assumptions are $\|x_i\|\le1$, $\varphi_i\ge0$ and $\varphi_i(0)\le1$.

Procedure SDCA starts from $\alpha^{(0)}=0$. At iteration $t$ it picks $i$ uniformly at random, independently of the past, chooses $\Delta\alpha_i$ maximizing $-\varphi_i^*(-(\alpha_i^{(t-1)}+\Delta\alpha_i))-\frac{\lambda n}{2}\|w(\alpha^{(t-1)})+(\lambda n)^{-1}\Delta\alpha_ix_i\|^2$, and sets $\alpha^{(t)}=\alpha^{(t-1)}+\Delta\alpha_ie_i$. Let $\alpha^*$ be a dual optimum and $w^*=w(\alpha^*)$.

The refined dual strong convexity condition (Definition 2, (4)) asks for functions $\gamma_i(\cdot)\ge0$ with

$$\varphi_i^*(-a)-\varphi_i^*(-b)+u(a-b)\ge\gamma_i(u)|a-b|^2\qquad\text{for all }a,b\text{ and }u\in\partial\varphi_i^*(-b).$$

For the hinge loss one may take $\gamma_i(u)=|uy_i-1|$. With constants $\gamma_i\ge0$, the dual strong convexity inequality (5) is

$$D(\alpha^*)-D(\alpha)\ge\frac1n\sum_{i=1}^n\gamma_i|\alpha_i-\alpha_i^*|^2+\frac\lambda2\|w(\alpha)-w^*\|^2\quad\text{for every feasible }\alpha,$$

and $N(u)=\#\{i:\gamma_i<u\}$ counts the coordinates with small modulus.

Formalization targets

Goal: Theorem 5 (p. 9)

Assume convex $L$-Lipschitz losses, the standing assumptions, and (5) with constants $\gamma_i\ge0$. For every $\epsilon_D>0$ and $s\in(0,1]$ with $\epsilon_D\ge 8L^2\frac{s}{\lambda n}N(\frac{s}{\lambda n})/n$,

$$t\ge2\frac ns\log\frac2{\epsilon_D}\quad\Longrightarrow\quad\mathbb E\bigl[D(\alpha^*)-D(\alpha^{(t)})\bigr]\le\epsilon_D .$$

The constants $2$ and $8$ are the paper's.

Milestones

1. Proposition 1 (pp. 8–9): condition (4), with $\gamma_i=\gamma_i(w^{*\top}x_i)$, implies (5), and $|(w^*-w)^\top x_i|\ge\gamma_i|a_i-\alpha_i^*|$ whenever $-a_i\in\partial\varphi_i(w^\top x_i)$ (6).
2. Lemma 5 (p. 19): under (5), one step raises the expected dual by at least $\frac{s}{2n}$ times the dual sub-optimality, plus $\frac{3s\lambda}{4n}\|w^*-w\|^2$, minus $(\frac sn)^2G_*(s)/(2\lambda)$ with $G_*(s)=\frac1n\sum_i(\|x_i\|^2-\gamma_i\lambda n/s)(\alpha_i^*-\alpha_i)^2$.
3. Lemma 3 (p. 15): the conjugate of an $L$-Lipschitz function is $+\infty$ outside $[-L,L]$.
4. Lemma 6 (p. 20): $G_*(s)\le4L^2N(s/(\lambda n))/n$.
5. Dual recursion (§7.6, p. 20): $\epsilon_D^{(t)}\le(1-\frac s{2n})\epsilon_D^{(t-1)}+(\frac sn)^2\frac{G_*(s)}{2\lambda}$ and $\epsilon_D^{(t)}\le(1-\frac s{2n})^t\epsilon_D^{(0)}+\frac sn\frac{G_*(s)}\lambda$, with $G_*(s)=4L^2N(s/(\lambda n))/n$.
6. Lemma 2 (p. 13): $D(\alpha)\le P(w^*)\le P(0)\le1$ and $D(0)\ge0$.

Significance

Theorem 5 gives a linear rate for the dual sub-optimality of SDCA on non-smooth losses whenever few constants $\gamma_i$ are small. If $N(s_0/(\lambda n))=0$ for some $s_0>0$ (for the SVM, $\lambda n|w^{*\top}x_iy_i-1|\ge s_0$ for all $i$), the iteration count is $(2n/s_0)\log(2/\epsilon_D)$, compared with order $n+L^2/(\lambda\epsilon)$ from the Lipschitz analysis of Theorem 1 of the same paper. The paper uses Theorem 5 to explain the observed asymptotic advantage of SDCA over SGD, and its Theorem 6 converts it into a duality-gap bound.

The result is proved in the paper. It has not been formalized: no SDCA convergence result is on Prove2Me, and Mathlib has no conjugate-duality theory for this problem class. The mission produces a formal account of the dual objective in extended reals, of the exact coordinate maximization step, and of the averaging over uniformly random coordinate sequences, together with a checked proof of the rate. The companion missions of this series cover Theorem 1 (Lipschitz losses) and Theorem 2 (smooth losses).

Difficulty

Condition (5) gives a modulus $\gamma_i$ per coordinate, and some $\gamma_i$ may be zero, so the dual is not strongly concave and the standard linear-rate argument for strongly concave coordinate ascent does not apply. The per-step progress has a variance term with the sign of $\|x_i\|^2-\gamma_i\lambda n/s$, which is positive exactly on the coordinates with small modulus; that term must be controlled by bounding the dual variables themselves, which requires the Lipschitz structure through the conjugate. The extended-real-valued conjugate is a second source of work: every quantity must be shown finite along the run before it can be manipulated as a real number.

Formalization scope

Lean works in EuclideanSpace ℝ (Fin d), with $n$ data points indexed by Fin n, $n>0$. The conjugate is an EReal supremum and $D$ is EReal-valued, $-\infty$ exactly at infeasible points. Real-valued expectations of dual values appear only together with a conjunct stating their finiteness. The SDCA step is a map $\Delta$ with the hypothesis that $\Delta(\alpha,i)$ is an exact maximizer of the coordinate objective. The run is a fold over the sequence of chosen coordinates, and the expectation is the uniform average over all sequences of length $t$ (SAGA.Convex.expectIdx, a published definition). The optimum $\alpha^*$ is a hypothesis $D(\beta)\le D(\alpha^*)$ for all $\beta$; in (5), $w^*$ is $w(\alpha^*)$. Inequality (5) quantifies over feasible $\alpha$ only. Lemmas 5 and 6 are stated for an arbitrary feasible current state, which is stronger than the history-averaged form printed. The paper's range $s\in[0,1]$ becomes $s\in(0,1]$, because at $s=0$ the iteration bound $2(n/s)\log(2/\epsilon_D)$ is undefined. A formalization that admits $s=0$ would evaluate it to $0$ and claim the bound at $t=0$, which is false.

The development needs elementary facts about conjugates of scalar functions in EReal (convexity, the Fenchel–Young inequality, the Lipschitz domain bound), the weak duality inequality $D\le P$, and finite averages over coordinate sequences. The conjugate facts and the expectation calculus are reusable by the other two missions of the series. Proofs of individual milestones are welcome independently.

Selected references

• S. Shalev-Shwartz and T. Zhang, Stochastic Dual Coordinate Ascent Methods for Regularized Loss Minimization, Journal of Machine Learning Research 14 (2013), 567–599; preprint arXiv:1209.1873v2. https://arxiv.org/abs/1209.1873
• Z.-Q. Luo and P. Tseng, On the convergence of coordinate descent method for convex differentiable minimization, Journal of Optimization Theory and Applications 72 (1992), 7–35. https://doi.org/10.1007/BF00939948
• C.-J. Hsieh, K.-W. Chang, C.-J. Lin, S. S. Keerthi and S. Sundararajan, A dual coordinate descent method for large-scale linear SVM, ICML 2008. https://doi.org/10.1145/1390156.1390208

Motivation

A decision maker who chooses $x$ to minimize an expected cost $c(x,\mathbb P)=\mathbb E_{\mathbb P}[\gamma(x,\xi)]$ rarely knows the distribution $\mathbb P$ of the random parameter $\xi$. What is available is a sample $\xi_1,\dots,\xi_T$. Any rule that turns the sample into a cost estimate can disappoint: the realized expected cost may exceed the estimate. In a cost-minimization context such underestimates are more harmful than overestimates, which is why distributionally robust optimization replaces the unknown $\mathbb P$ by a worst case over a set of distributions consistent with the data.

Van Parys, Mohajerin Esfahani and Kuhn (arXiv:1704.04118, Management Science 2021) asked which such rule is best. They define a data-driven predictor to be least conservative among all predictors whose probability of disappointment decays exponentially at a prescribed rate $r$, and they prove that a single predictor, the worst-case expected cost over a relative-entropy ball around the empirical distribution, is the unique strong solution. Their main results are for a finite set of outcomes $\Xi=\{1,\dots,d\}$. Section 5 extends the predictor result to an arbitrary compact $\Xi\subseteq\mathbb R^d$; this mission formalizes that extension. The version used throughout is the arXiv preprint arXiv:1704.04118v3 (22 December 2019), and every index below is the preprint's.

Setting

Fix compact sets $X\subseteq\mathbb R^n$ (decisions) and $\Xi\subseteq\mathbb R^d$ (outcomes), and a cost $\gamma:X\times\Xi\to\mathbb R$ that is jointly continuous.

• The model class $\mathcal P$ is the set of Borel probability distributions on $\Xi$, with the topology of weak convergence. $X\times\mathcal P$ carries the product topology.
• The model-based predictor is $c(x,\mathbb P)=\int_\Xi\gamma(x,\xi)\,\mathrm d\mathbb P(\xi)$.
• The relative entropy of $\mathbb P'$ with respect to $\mathbb P$ (Definition 8) is $I(\mathbb P',\mathbb P)=\int_\Xi\log\frac{\mathrm d\mathbb P'}{\mathrm d\mathbb P}\,\mathrm d\mathbb P'$ if $\mathbb P'\ll\mathbb P$, and $+\infty$ otherwise.
• Given independent samples $\xi_1,\dots,\xi_T$ from $\mathbb P$, the empirical distribution is $\hat{\mathbb P}_T=\frac1T\sum_{t=1}^T\delta_{\xi_t}$, and $\mathbb P^\infty$ denotes the law of the sample path.
• A data-driven predictor is a continuous function $\hat c:X\times\mathcal P\to\mathbb R$; the estimate after $T$ samples is $\hat c(x,\hat{\mathbb P}_T)$. Its out-of-sample disappointment is $\mathbb P^\infty\big(c(x,\mathbb P)>\hat c(x,\hat{\mathbb P}_T)\big)$.
• Problem (5): $\hat c$ is feasible if, for all $x\in X$ and $\mathbb P\in\mathcal P$,

$$\limsup_{T\to\infty}\frac1T\log\mathbb P^\infty\big(c(x,\mathbb P)>\hat c(x,\hat{\mathbb P}_T)\big)\le -r,$$

and strongly optimal if it is feasible and $\hat c(x,\mathbb P')\le\hat c'(x,\mathbb P')$ for all $(x,\mathbb P')$ and every feasible $\hat c'$.

• The distributionally robust predictor is $\hat c_r(x,\mathbb P')=\sup\{c(x,\mathbb P):\mathbb P\in\mathcal P,\ I(\mathbb P',\mathbb P)\le r\}$.
• $\bar\gamma(x)=\max_{\xi\in\Xi}\gamma(x,\xi)$ is the worst-case cost and $\Xi^\star(x)$ the set of its maximizers.

Formalization targets

Goal: Theorem 10 (p. 26)

$$r\ge0\ \Longrightarrow\ \hat c_r\text{ is feasible in (5)},\qquad r>0\ \Longrightarrow\ \hat c_r\text{ is strongly optimal in (5)}.$$

Both halves are in the goal. The case $r=0$ of feasibility is the statement that $\hat c_0=c$ is continuous.

Milestones

• Lemma 1 (p. 23): $c$ is continuous on $X\times\mathcal P$.
• Lemma 2 (33), p. 29: $\hat c_r$ equals a supremum over pairs $(\mathbb P_c,p)$ with $\mathbb P'\ll p\,\mathbb P_c\ll\mathbb P'$, where the mass $1-p$ is placed at cost $\bar\gamma(x)$.
• Lemma 3 (p. 31): the perturbed problem (34), $\hat c_{r,\epsilon}$, satisfies $\hat c_r\le\hat c_{r,\epsilon}\le\hat c_r+\epsilon$.
• Lemma 4 (35), p. 31:

$$\hat c_{r,\epsilon}(x,\mathbb P')\le\min_{\alpha\ge\bar\gamma(x)+\epsilon}\ \alpha-e^{-r}\exp\Big(\int_\Xi\log(\alpha-\gamma(x,\xi))\,\mathrm d\mathbb P'(\xi)\Big),$$

with a minimizer $\alpha^\star\le(\bar\gamma(x)+\epsilon-e^{-r}c(x,\mathbb P'))/(1-e^{-r})$, and with equality for $\epsilon>0$.

• Proposition 6 (p. 25): $\hat c_r$ is continuous on $X\times\mathcal P$ for $r\ge0$.
• Theorem 9 (24a)/(24b), p. 25: the weak large deviation principle for $\hat{\mathbb P}_T$ in the weak topology, with the closure $\operatorname{cl}\mathcal D$ in the upper bound and the interior in the lower bound.
• (41), p. 35: if $\mathbb P_0(\Xi^\star(x))<1$ and $c(x,\mathbb P_0)\ge\hat c_r(x,\mathbb P')$, then $I(\mathbb P',\mathbb P_0)\ge r$.
• Proposition 1(ii), (iii) in the general setting (p. 24): $I$ is jointly convex and jointly lower semicontinuous on $\mathcal P\times\mathcal P$.

Proposition 5, the dual representation (23) of $\hat c_r$ itself, is included as a further item; the proof of Theorem 10 goes through Lemmas 3–4 and does not use it.

Significance

Theorem 10 says that, on any compact outcome space, no continuous predictor is less conservative than $\hat c_r$ while keeping its disappointment probability below $e^{-rT}$ to first order in the exponent. Relative-entropy distributionally robust optimization is therefore not one choice among many ambiguity sets but the optimal one for this criterion, and the dual representation turns its evaluation into a one-dimensional convex problem. The paper also shows that the continuous-state analogue of its prescriptor result (Theorem 11) only holds up to an arbitrarily small shift, so the predictor statement formalized here is the clean part of the extension.

The results are proved in the paper; none is formalized. A complete development yields a formal Sanov-type weak large deviation principle for empirical measures in the weak topology, joint convexity and lower semicontinuity of the Kullback–Leibler divergence for probability measures on a compact metric space, and a measure-theoretic dual representation of a relative-entropy worst-case expectation. Mathlib has the Kullback–Leibler divergence klDiv and the weak topology on probability measures, but none of these three results.

Difficulty

The finite-state proof of feasibility bounds the disappointment through the large deviations upper bound over the disappointment set $\mathcal D$ itself. On a continuous space that bound only holds over the closure $\operatorname{cl}\mathcal D$ in the weak topology (24a), and the paper notes that this invalidates the finite-state argument (p. 25). The rate must then be controlled on a larger, closed set of empirical distributions, where the strict inequality defining a disappointment is lost; this is where the mass that $\mathbb P_0$ puts on the worst-case scenarios $\Xi^\star(x)$ starts to matter, as the hypothesis of (41) shows.

Continuity of $\hat c_r$ in the weak topology is the second obstacle. The supremum runs over an infinite-dimensional set of distributions, a worst-case distribution may put mass outside the support of $\mathbb P'$, and the integrals involved can diverge or take the value $-\infty$. Weak convergence controls integrals of bounded continuous functions only, and $\log(\alpha-\gamma)$ is unbounded below at $\alpha=\bar\gamma(x)$.

Formalization scope

• $\mathcal P$ is ProbabilityMeasure ↥Ξ for the Borel σ-algebra of the subtype, with Mathlib's weak-convergence topology. $X$ and $\Xi$ are compact subsets of Euclidean spaces, $\gamma:↥X\to↥\Xi\to\mathbb R$ is jointly continuous; these standing assumptions of §2 (p. 5) and §5 (p. 23) appear as hypotheses of every theorem. No other hypothesis is added. Nonemptiness of $\Xi$ is automatic wherever a distribution on $\Xi$ is in scope.
• $I$ is Mathlib's InformationTheory.klDiv, valued in $[0,\infty]$. It equals Definition 8, including the value $+\infty$ when $\mathbb P'\not\ll\mathbb P$ or when the log-likelihood ratio is not integrable.
• The empirical distribution is defined for $T\ge1$. The probability of an event about $\hat{\mathbb P}_T$ is the outer measure under the product measure $\mathbb P^{\otimes T}$, and is $0$ at $T=0$; all statements are asymptotic in $T$.
• Decay rates are stated without logarithms: $\limsup\frac1T\log p_T\le-s$ becomes "for every $r'<s$, eventually $p_T\le e^{-r'T}$", which is equivalent and handles $p_T=0$. A naive Real.log encoding would be wrong, since Lean sets $\log0=0$. Predictors must be continuous for the weak topology; dropping continuity, or replacing the weak topology by a finer one, changes the problem.
• The constraint $\int\log(\frac1p\frac{\mathrm d\mathbb P'}{\mathrm d\mathbb P_c})\,\mathrm d\mathbb P'\le r$ in (33)–(34) carries an explicit integrability requirement, so that a divergent integral fails the constraint instead of evaluating to $0$. The geometric mean $\exp\int\log(\alpha-\gamma)\,\mathrm d\mathbb P'$ follows the paper's convention $\log0=-\infty$; it is defined as $\inf_{\delta>0}\exp\int\log(\alpha+\delta-\gamma)\,\mathrm d\mathbb P'$, which is the same value for $\alpha\ge\bar\gamma(x)$.
• At the end of the proof of Theorem 10 the page writes "when $\epsilon>0$" for strong optimality; the theorem statement says $r>0$, which is what is formalized.

Contributions are welcome at every level: a Sanov upper and lower bound for empirical measures on compact metric spaces, convexity and lower semicontinuity of klDiv, and the measure-theoretic duality of Lemma 4 are each reusable beyond this mission.

Selected references

• B. P. G. Van Parys, P. Mohajerin Esfahani, D. Kuhn, From Data to Decisions: Distributionally Robust Optimization is Optimal, Management Science 67(6), 2021. Preprint arXiv:1704.04118v3. https://arxiv.org/abs/1704.04118
• I. Csiszár, A simple proof of Sanov's theorem, Bulletin of the Brazilian Mathematical Society 37(4), 2006. https://doi.org/10.1007/s00574-006-0023-1
• T. van Erven, P. Harremoës, Rényi divergence and Kullback–Leibler divergence, IEEE Transactions on Information Theory 60(7), 2014. https://doi.org/10.1109/TIT.2014.2320500
• A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 1998. https://doi.org/10.1007/978-1-4612-5320-4

Motivation

A classifier trained from finitely many examples can perform well on those examples while responding poorly to changes in the feature distribution or to mislabeled observations. Distributionally robust learning addresses this by choosing a classifier against every probability distribution within a specified distance of the empirical distribution. The resulting optimization appears to range over an infinite-dimensional family of distributions. Shafieezadeh-Abadeh, Kuhn, and Mohajerin Esfahani show that, for linear classification with a convex Lipschitz loss, this problem has an exact finite convex reformulation. That result is Theorem 3.11(ii) of the 2019 arXiv preprint, which is the source used here.

The authors' transport metric allows a data point's features to move and its binary label to flip, with separate prices for those two changes. This matters when robustness to inaccurate labels is part of the model. A label-preserving metric cannot express that choice. The paper builds on its Section 2 learning model and the transport duality developed in Appendix A.1; the present mission isolates the classification result and the intermediate statements used for it. The preprint's Corollary 3.14 specializes the result to logloss, while its Corollary 3.12 treats hinge loss. A logloss-specific reformulation and a label-preserving classification result already have proved statements on Prove2Me; the general convex-Lipschitz, finite label-cost theorem remains the target of this mission.

Setting

Let $V$ be a finite-dimensional real vector space with a chosen norm $\|\cdot\|$. Features are $x\in V$ and labels are $y\in\{-1,+1\}$. A linear classifier is a continuous linear functional $w:V\to\mathbb R$, with score $\langle w,x\rangle=w(x)$. Its dual norm $\|w\|_*$ is the operator norm induced by $\|\cdot\|$. Given $N\ge1$ training pairs $(\hat x_i,\hat y_i)$, their empirical distribution is $\hat P_N=N^{-1}\sum_{i=1}^N\delta_{(\hat x_i,\hat y_i)}$.

For $\kappa>0$, the transport cost between pairs is

$$d((x,y),(x',y'))=\|x-x'\|+\kappa\mathbf1_{y\ne y'}.$$

The Wasserstein distance $W(Q,P)$ is the least expected transport cost among joint distributions whose two marginals are $Q$ and $P$. For a radius $\rho\ge0$, the Wasserstein ball $\mathbb B_\rho(\hat P_N)$ contains probability distributions $Q$ satisfying $W(Q,\hat P_N)\le\rho$. The loss is $L(y\langle w,x\rangle)$, where $L:\mathbb R\to[0,\infty)$ is convex and Lipschitz continuous. The Lipschitz modulus $\operatorname{lip}(L)$ is the smallest Lipschitz bound for $L$, defined as the supremum of its difference quotients. These are the objects and standing conventions of Sections 1.1, 2, and 3.2 of the preprint.

Formalization targets

The goal is Theorem 3.11(ii): for every fixed $w$, the worst-case expected loss equals the value of program (18),

$$\sup_{Q\in\mathbb B_\rho(\hat P_N)}\mathbb E^Q[L(y\langle w,x\rangle)] = \inf_{\lambda,s}\left\{\lambda\rho+\frac1N\sum_{i=1}^{N}s_i: \begin{array}{l} L(\hat y_i\langle w,\hat x_i\rangle)\le s_i,\\ L(-\hat y_i\langle w,\hat x_i\rangle)-\kappa\lambda\le s_i\quad(i=1,\ldots,N),\\ \operatorname{lip}(L)\|w\|_*\le\lambda \end{array}\right\}.$$

Taking the infimum of both sides over $w$ gives equality between problem (4) and the full program (18). The fixed-$w$ identity is stated explicitly because it is the stronger assertion established in the proof. The milestone list follows the paper's appendix: Lemma A.1 converts the robust expectation into a scalar transport-price infimum; the label split isolates the two possible labels; Lemma A.3 evaluates the feature supremum; the ensuing display gives the program in terms of conjugate slopes; and the final identity identifies those slopes with $\operatorname{lip}(L)$. Each milestone is tied to its printed page in the preprint.

Significance

The theorem replaces a search over probability distributions by a finite convex program with one scalar $\lambda$ and one slack variable $s_i$ per sample, in addition to the classifier $w$. It makes the price of label changes explicit through $\kappa\lambda$ and the price of feature changes through $\operatorname{lip}(L)\|w\|_*$. Consequently, different convex Lipschitz classification losses can be treated within the same transport model rather than by deriving a new distributional optimization problem for each loss. The preprint applies the result to hinge, smoothed hinge, and logloss examples in the paragraphs following Theorem 3.11.

The result is proved in the cited paper. Its general statement and the paper's appendix milestones are not yet machine-checked in this mission. A verified development would connect the published definitions of the Wasserstein ball and Lipschitz modulus to an exact program-value theorem that later work can import. The loss-specific proved statements already available on Prove2Me provide useful comparisons, but their narrower losses or label-preserving transport costs do not replace this theorem.

Difficulty

The visible finite constraints contain no probability distributions, while the left-hand side optimizes over all probability measures in a Wasserstein ball. Establishing that the two values coincide requires control of the transport budget and the inner worst-case loss at the same time. The straightforward comparison of feasible values gives only one inequality. It does not show that every improvement allowed by a distribution can be represented by the scalar transport price and the samplewise constraints. The case $\rho=0$ also needs care: Lemma A.1's strong-duality proof cites a result for strictly positive radius, whereas the theorem itself allows zero radius and states an infimum rather than an attained minimum.

Formalization scope

Lean represents $V$ by an abstract finite-dimensional real normed space with its Borel measurable structure. This retains the arbitrary norm of $\mathbb R^n$ in the paper. Labels are Bool, interpreted as $+1$ and $-1$; the published DRLogReg_Reformulation_Core definition supplies their sign map, the metric, Wasserstein distance, ball, and empirical distribution. The published WassersteinDRO_Duality_lipschitzModulus definition supplies the exact Lipschitz modulus. The mission's own definitions add the general loss, the feasible set of (18), the fixed-classifier program value, and the effective domain $\Theta=\{\theta:L^*(\theta)<\infty\}$ of the convex conjugate. The same objects and conventions are used across all milestones.

All potentially infinite robust values are represented in $[0,\infty]$; the unbounded feature suprema in Lemma A.3 and the label split use extended reals. The standing loss condition $L\ge0$ comes from the paper's Section 2.1 loss codomain. It also makes the lower Lebesgue integral and the finite program's extended-nonnegative objective faithful. The sample size is positive, $\kappa>0$, and the goal allows $\rho=0$. Lemma A.1 separately assumes $\rho>0$, matching the strong-duality condition used on page 29. The printed extra index $j\in[J]$ in the page-35 classification display is carried in its verbatim milestone provenance but not in the Lean statement, because no $j$ exists in part (ii). The formalization does not obtain the theorem by restricting $L$ to a constant loss, by taking a singleton feature space, or by substituting an arbitrary Lipschitz bound for its modulus. Contributions that establish transport duality, the conjugate-domain slope identity, or the zero-radius case are directly reusable.

Selected references

• S. Shafieezadeh-Abadeh, D. Kuhn, and P. Mohajerin Esfahani, Regularization via Mass Transportation, arXiv preprint arXiv:1710.10016v3, 2019. Preprint.
• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, and D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28, 2015. Published Prove2Me formalization.