Missions · Prove2Me

Convex Optimization Optimization·Captain: mikedeng1

Error Bounds, Quadratic Growth, and Linear Convergence of Proximal Methods I: For the Proximal Gradient Method, the Error Bound Condition Is Equivalent to Quadratic GrowthResearch Paper

Motivation

A large share of the optimization problems solved in statistics, signal processing and machine learning have the composite form

\min_x\ \varphi(x) := f(x) + g(x),

where $f$ is smooth and $g$ is convex but possibly nonsmooth or extended-valued (a norm penalty, the indicator of a constraint set). The workhorse algorithm for such problems is the proximal gradient method, which takes a gradient step on $f$ followed by a proximal step on $g$ . Its worst-case rate on convex problems is sublinear, yet in practice it often converges linearly. The classical explanation, going back to Luo and Tseng (1993) Ann. Oper. Res. 46, is an error bound condition: near the solution set, the distance to the minimizers is controlled by the length of the algorithm's own step. Under such a condition the method converges linearly.

The difficulty is that the error bound is stated in terms of the algorithm, not the problem. Drusvyatskiy and Lewis (arXiv:1602.06661, Math. Oper. Res. 43(3), 2018) showed that, for convex problems, it is equivalent to a purely geometric property of $\varphi$ : quadratic growth away from the set of minimizers. This mission formalizes that equivalence (§3 of the paper) together with the three comparison results that build it.

Setting

Write $\mathbb R^n$ for Euclidean space with norm $\|\cdot\|$ , $\overline{\mathbb R} = \mathbb R\cup\{\pm\infty\}$ , and $\operatorname{dist}(x;Q) = \inf_{z\in Q}\|z-x\|$ . A function $g:\mathbb R^n\to\overline{\mathbb R}$ is closed if it is lower semicontinuous. For real $r$ , the sublevel set is $[\varphi\le r] = \{x:\varphi(x)\le r\}$ .

The problem is (3.1): $g$ is a closed convex function, and $f:\mathbb R^n\to\mathbb R$ is convex, $C^1$ -smooth, with $\beta$ -Lipschitz gradient, $\|\nabla f(x)-\nabla f(y)\|\le\beta\|x-y\|$ . Let $S$ be the (nonempty) set of minimizers of $\varphi = f+g$ and $\varphi^*$ its minimal value. For $t>0$ the proximal map is

\operatorname{prox}_{tg}(z) = \operatorname*{argmin}_y\Big\{g(y)+\tfrac1{2t}\|y-z\|^2\Big\},

the proximal gradient method iterates $x_{k+1} = \operatorname{prox}_{tg}(x_k - t\nabla f(x_k))$ , and the prox-gradient mapping is

\mathcal G_t(x) = t^{-1}\big(x - \operatorname{prox}_{tg}(x - t\nabla f(x))\big),

so that $x_{k+1} = x_k - t\,\mathcal G_t(x_k)$ and $\mathcal G_t(x) = 0$ exactly at minimizers.

For $\nu>0$ , $\varphi$ has quadratic growth with constant $\alpha>0$ if $\varphi(x)\ge\varphi^*+\frac\alpha2\operatorname{dist}^2(x;S)$ on $[\varphi\le\varphi^*+\nu]$ (3.12), and the error bound condition with parameters $(\gamma,\nu)$ holds if $\operatorname{dist}(x;S)\le\gamma\|\mathcal G_t(x)\|$ on the same sublevel set (Definition 3.1, (3.13)).

Formalization targets

Goal: Corollary 3.6 (p. 9)

\text{(3.12) with }\alpha\ \Longrightarrow\ \text{(3.13) with }\gamma = (2\alpha^{-1}+t)(1+\beta t),\qquad \text{(3.13) with }\gamma\ \Longrightarrow\ \text{(3.12) for every }\alpha\in(0,\gamma^{-1}),

for every step size $t>0$ and every $\nu>0$ .

Milestones

For a closed convex $h$ with minimizers $S\neq\emptyset$ and minimal value $h^*$ :

Theorem 3.3 (pp. 6–7): quadratic growth on $[h\le h^*+\nu]$ with constant $\alpha$ implies $\operatorname{dist}(x;S)\le L\operatorname{dist}(0;\partial h(x))$ there with $L = 2\alpha^{-1}$ ; conversely the latter implies quadratic growth with any $\alpha\in(0,1/L]$ .
Theorem 3.4 (p. 7): the subdifferential bound with $L$ implies $\operatorname{dist}(x;S)\le\widehat L\,t^{-1}\|x-\operatorname{prox}_{th}(x)\|$ with $\widehat L = L+t$ ; conversely the latter implies the former with $L = \widehat L$ .
Theorem 3.5 (p. 8): for maximal monotone $G,\Phi$ with $\Phi = F + G$ and $F$ single-valued, the forward-backward step satisfies $\|\mathcal G_t(x)\|\le\operatorname{dist}(0;\Phi(x))$ (3.10), and if $F$ is $\beta$ -Lipschitz,

(1-\beta t)\|\mathcal G_t(x)\|\ \le\ \|t^{-1}(x-\operatorname{prox}_{t\Phi}(x))\|\ \le\ (1+\beta t)\|\mathcal G_t(x)\|.\qquad(3.11)

Theorem 3.2, second claim (p. 5, at $t=\beta^{-1}$ ): under the error bound, the iterates converge R-linearly to any limit point $x^*$ , $\|x_{r+k}-x^*\|^2\le(1-\frac1{2\beta\gamma})^kC(\varphi(x_r)-\varphi^*)$ .

Significance

The result. Corollary 3.6 converts a condition on an algorithm into a condition on the objective. Quadratic growth can be checked by hand in many models (strongly convex losses, polyhedral problems, problems with a sharp minimum), and once it holds, Theorem 3.2 gives linear convergence of the proximal gradient method with an iteration count of order $\frac\beta\alpha\ln\frac1\epsilon$ , matching the rate familiar from strongly convex problems. The rest of the paper uses this equivalence as its main tool: §4 proves quadratic growth for structured problems $f(Ax)+g(x)$ under dual strict complementarity, and §§5–8 extend the comparison to prox-linear methods for nonconvex compositions. Theorems 3.3 and 3.4 are statements about a single closed convex function and are of independent use in the analysis of proximal point methods.

Formalizing it. All results here are proved on paper; none of them is machine-checked. The mission produces a Lean statement of the equivalence with the paper's explicit constants, and of the step-length comparison between the forward-backward and the proximal point methods for maximal monotone operators. Formal proofs require the existence, uniqueness and nonexpansiveness of resolvents and proximal maps, the subdifferential sum rule for a smooth plus a convex function, and a quadratic growth argument for convex functions; these are reusable well beyond this paper.

Difficulty

The forward direction is a chain of three inequalities, but each link compares objects that live in different worlds: the subdifferential of $\varphi$ , the proximal map of $\varphi$ , and the proximal map of $g$ evaluated at a gradient-shifted point. The proximal gradient step is not the proximal point step on $\varphi$ , and the obvious attempt to compare $\mathcal G_t(x)$ with $\partial\varphi(x)$ directly gives only one inequality (3.10); the reverse comparison (3.11) needs the resolvent of the sum $\nabla f + \partial g$ and the Lipschitz constant of $\nabla f$ . The converse half of Theorem 3.3 (error bound implies growth) is the deepest step: the paper omits its proof and cites Drusvyatskiy–Ioffe and Drusvyatskiy–Mordukhovich–Nghia. It has to pass from a pointwise bound on subgradients to a bound on function values over the whole sublevel set, which no single subgradient inequality provides.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $\overline{\mathbb R}$ -valued functions are EReal-valued; $f$ is real-valued and $\varphi = f + g$ is computed in EReal. "Closed convex" is the published RockafellarMaxMono.Shared.ProperConvex (never $-\infty$ , somewhere finite, convex) together with LowerSemicontinuous.
$S$ is the set of minimizers, assumed nonempty as in the paper; $\varphi^*$ is a real number equal to $\varphi$ on $S$ ; $\operatorname{dist}$ is Metric.infDist; $\nu>0$ is real.
Proximal maps and resolvents are predicates, never chosen functions: $p=\operatorname{prox}_{tg}(z)$ is the published GoldenRatioVI.Shared.IsProxPoint (fun y => t * g y) z p (same argmin for $t>0$ ), and resolvents are maps satisfying the published ThreeOpSplitting.Convergence.IsResolvent. Conditions are stated for every such point; existence and uniqueness are facts a solver proves.
$\operatorname{dist}(0;\partial h(x))$ follows the convention $\operatorname{dist}(0;\emptyset) = +\infty$ : an inequality " $a\le L\operatorname{dist}(0;\partial h(x))$ " is stated as " $a\le L\|v\|$ for every $v\in\partial h(x)$ ". Using Metric.infDist 0 (∂h x), which is $0$ on the empty set, would turn (3.7) into the false claim that every point of the sublevel set where $\partial h$ is empty is a minimizer; this trivializing or falsifying encoding is ruled out.
The subdifferential is the published ProxAlg.FixedPoint.subdifferential, the gradient is Mathlib's gradient.
Theorem 3.2 is stated at $t = \beta^{-1}$ with $\beta>0$ : the printed range $t\le\beta^{-1}$ relies on the descent inequality (3.2), which fails for smaller $t$ . Its first claim (an iteration count) and Corollary 3.7 are not stated.

Contributions welcome: proofs of the milestones in any order, general lemmas on resolvents of maximal monotone operators and on proximal maps of EReal-valued convex functions, and a proof of the converse half of Theorem 3.3.

Selected references

D. Drusvyatskiy, A. S. Lewis, Error bounds, quadratic growth, and linear convergence of proximal methods, Math. Oper. Res. 43(3), 2018. arXiv:1602.06661v2 — https://arxiv.org/abs/1602.06661
Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46/47:157–178, 1993. https://doi.org/10.1007/BF02096261
D. Drusvyatskiy, A. D. Ioffe, Quadratic growth and critical point stability of semi-algebraic functions, Math. Program. 153(2):635–653, 2015 (reference [15] of the paper).
D. Drusvyatskiy, B. S. Mordukhovich, T. T. A. Nghia, Second-order growth, tilt stability, and metric regularity of the subdifferential, J. Convex Anal. 21(4):1165–1192, 2014 (reference [19] of the paper).
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

13 thms2 active usersReviewed

Completed

Convex Optimization Dynamical Systems Optimization·Captain: mikedeng1

Fast Convergence of Inertial Dynamics and Algorithms with Asymptotic Vanishing Viscosity 2: For Strongly Convex Φ and α > 3, Φ(x(t)) − min Φ, ‖x(t) − x*‖² and ‖ẋ(t)‖² Are O(t^(−2α/3))Research Paper

Motivation

Nesterov's accelerated gradient method minimizes a smooth convex function at the rate $\mathcal O(k^{-2})$ in the number of iterations $k$ , against $\mathcal O(k^{-1})$ for plain gradient descent. Su, Boyd and Candès (arXiv:1503.01243) observed that, as the step size tends to zero, Nesterov's scheme becomes the second-order differential equation

\ddot x(t)+\frac{\alpha}{t}\dot x(t)+\nabla\Phi(x(t))=0\tag{1}

with $\alpha=3$ , a heavy-ball system whose friction coefficient $\alpha/t$ vanishes as $t\to+\infty$ (asymptotic vanishing damping). Studying (1) in continuous time gives Lyapunov arguments that are then discretized into new algorithms.

Attouch, Chbani, Peypouquet and Redont (Math. Program. 168 (2018), DOI 10.1007/s10107-016-0992-8) analyse (1) for general $\alpha$ . This mission formalizes their result for strongly convex $\Phi$ , where the rate of convergence of (1) depends on $\alpha$ and improves without bound as $\alpha$ grows.

Timeline.

2014–2016: Su, Boyd and Candès prove $\Phi(x(t))-\min\Phi=\mathcal O(t^{-2})$ for convex $\Phi$ and $\alpha\ge3$ , and $\mathcal O(t^{-3})$ for strongly convex $\Phi$ when $\alpha>9/2$ ([44, Theorem 4.2] in the paper).
2015 (this paper): every trajectory converges weakly to a minimizer when $\alpha>3$ ; for strongly convex $\Phi$ and every $\alpha>3$ , the values, the squared distance to the minimizer and the squared velocity are $\mathcal O(t^{-2\alpha/3})$ .

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ , and let $\Phi:\mathcal H\to\mathbb R$ be continuously differentiable with gradient $\nabla\Phi$ . Fix $\alpha>0$ and $t_0>0$ . A solution of (1) is a twice differentiable trajectory $x:[t_0,+\infty[\to\mathcal H$ with velocity $\dot x$ satisfying (1) at every $t\ge t_0$ .

$\Phi$ is strongly convex with constant $\mu>0$ if

\Phi(y)\ge\Phi(x)+\langle\nabla\Phi(x),y-x\rangle+\frac\mu2\|x-y\|^2\qquad\text{for all }x,y\in\mathcal H.

Such a $\Phi$ has exactly one minimizer $x^*$ , and $\min\Phi=\Phi(x^*)$ .

For $\lambda\ge0$ , $p\ge0$ the anchored energy is

\mathcal E^p_\lambda(t)=t^p\Big(t^2\big(\Phi(x(t))-\min\Phi\big)+\tfrac12\|\lambda(x(t)-x^*)+t\dot x(t)\|^2\Big),

a sum of nonnegative terms. The proof of the main theorem fixes

p=\tfrac23(\alpha-3),\qquad\lambda=\tfrac23\alpha,\qquad t_1=\max\Big\{t_0,\sqrt{p\lambda/\mu}\Big\}.

Formalization targets

Goal: Theorem 3.4 (p. 11)

For strongly convex $\Phi$ and $\alpha>3$ , every solution $x$ of (1) converges strongly to the unique minimizer $x^*$ , and

\Phi(x(t))-\min\Phi=\mathcal O\big(t^{-\frac23\alpha}\big),\qquad\|x(t)-x^*\|^2=\mathcal O\big(t^{-\frac23\alpha}\big),\qquad\|\dot x(t)\|^2=\mathcal O\big(t^{-\frac23\alpha}\big)\tag{25}

as $t\to+\infty$ . The goal states the asymptotic form; the explicit constants are milestones.

Milestones (explicit forms, valid for $t\ge t_1$ )

The derivative identity (10) for $\mathcal E^p_\lambda$ along solutions of (1), for any $\lambda,p\ge0$ .
Its strongly convex upper bound (first display of the proof of Theorem 3.4).
(26): $\mathcal E^p_\lambda(t)\le\mathcal E^p_\lambda(t_1)+\frac{\lambda p}{4}t^p\|x(t)-x^*\|^2\le\mathcal E^p_\lambda(t_1)+\frac{\lambda p}{2\mu}t^p(\Phi(x(t))-\min\Phi)$ .
(27): $\Phi(x(t))-\min\Phi\le2\mathcal E^p_\lambda(t_1)\,t^{-\frac23\alpha}$ .
(28): $\|x(t)-x^*\|^2\le\frac2\mu(\Phi(x(t))-\min\Phi)\le\frac4\mu\mathcal E^p_\lambda(t_1)\,t^{-\frac23\alpha}$ .
Last display of the proof: $\|\dot x(t)\|^2\le4\big(1+\sqrt{\alpha/(\alpha-3)}\big)^2\mathcal E^p_\lambda(t_1)\,t^{-\frac23\alpha}$ .

Significance

The theorem shows that the rate of (1) on strongly convex functions is not capped at $\mathcal O(t^{-2})$ or $\mathcal O(t^{-3})$ : the exponent $2\alpha/3$ grows linearly in $\alpha$ , and it already exceeds $2$ for every $\alpha>3$ . It extends [44, Theorem 4.2], which needs $\alpha>9/2$ and gives $\mathcal O(t^{-3})$ . The same parametrized energy $\mathcal E^p_\lambda$ is the template for the discrete analyses of Nesterov-type algorithms with parameter $\alpha$ , so its derivative identity (10) is reusable beyond this mission.

The result is proved on paper. To the best of current knowledge none of it is formalized: Mathlib has no theory of inertial dynamics, and the platform's strongly convex rates concern discrete methods. A completed mission gives a machine-checked Lyapunov analysis of a non-autonomous second-order ODE in a Hilbert space, with the explicit constants of the paper.

Difficulty

The derivative identity (10) is a computation, but it must be carried out with one-sided derivatives at $t_0$ , real powers $t^p$ , and the chain rule for $\Phi\circ x$ in an infinite-dimensional space. The obvious argument, that $\mathcal E^p_\lambda$ is nonincreasing, fails: even with the best choice of $p$ and $\lambda$ the bound on its derivative keeps a term $\frac{\lambda p}{2}t^p\langle x-x^*,\dot x\rangle$ of no fixed sign, and only for $t\ge t_1$ is the quadratic term in $\|x-x^*\|^2$ nonpositive. Passing from the differential inequality to (26) therefore needs integration on $[t_1,t]$ for functions known only through one-sided derivatives. The velocity bound then combines (26), (27) and (28) through square roots, and the goal additionally requires the existence of the minimizer in an infinite-dimensional space, which is a compactness argument (weak lower semicontinuity) and not an algebraic one.

Formalization scope

$\mathcal H$ is any real Hilbert space (InnerProductSpace ℝ H, CompleteSpace H), not $\mathbb R^n$ . $\Phi$ is ContDiff ℝ 1 and $\nabla\Phi$ is Mathlib's gradient.
A solution is a pair $(x,v)$ with $t_0>0$ , where $x$ has derivative $v(t)$ and $v$ has derivative $-\frac\alpha t v(t)-\nabla\Phi(x(t))$ within $[t_0,+\infty[$ at every $t\ge t_0$ ; $\dot x$ is $v$ .
Strong convexity is the gradient inequality printed on p. 10, with $\mu>0$ ; $\min\Phi$ is written $\Phi(x^*)$ with $x^*$ a minimizer.
$t^p$ is the real power, only evaluated at $t\ge t_0>0$ ; $p$ , $\lambda$ , $t_1$ are named definitions shared by the milestones.
$\mathcal O$ in (25) is Asymptotics.IsBigO along atTop; strong convergence is norm convergence. The existence and uniqueness of $x^*$ are conclusions of the goal, not hypotheses, so the goal cannot be satisfied vacuously by an empty argmin; the strong-convexity hypothesis is satisfiable (e.g. $\Phi=\|\cdot\|^2$ with $\mu=2$ , and $x\equiv0$ solves (1)).
Theorem numbers and pages are those of the Optimization Online preprint 5179 (October 2015), not of the journal typesetting.

Useful infrastructure: the derivative of $\Phi\circ x$ via gradient, integration of differential inequalities on $[t_0,+\infty[$ , and existence of minimizers of strongly convex continuous functions on Hilbert spaces. Proofs of any milestone, and of the goal from the milestones, are welcome.

Selected references

H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing damping, Optimization Online preprint 5179, 2015. https://optimization-online.org/wp-content/uploads/2015/10/5179.pdf
H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Math. Program. 168 (2018), 123–175. https://doi.org/10.1007/s10107-016-0992-8
W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, J. Mach. Learn. Res. 17 (2016). https://arxiv.org/abs/1503.01243
Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Math. Dokl. 27 (1983), 372–376.

9 thms2 active usersReviewed

Operations Research Optimal Transport Optimization+1·Captain: mikedeng1

On a Problem of Optimal Transport Under Marginal Martingale Constraints 1: An Optimal Martingale Transport Plan Is Concentrated on a Borel Set No Finite Rerouting ImprovesResearch Paper

Motivation

In classical optimal transport, a transport plan that minimizes the total cost is characterized through its support: an optimal plan is $c$ -cyclically monotone, meaning that no finite collection of its transported particles can be re-paired more cheaply (Villani, Optimal Transport, Old and New, 2009, Ch. 4–5). This pointwise criterion is how most structural results in optimal transport are proved: it is what turns a global minimization over measures into a statement about finitely many points.

The martingale transport problem adds a constraint motivated by mathematical finance: the plan must be the law of a one-step martingale $(X, Y)$ with given marginals $X\sim\mu$ , $Y\sim\nu$ . Its value gives model-independent bounds on the price of an exotic option whose payoff is the cost function, given the prices of all vanilla options at two dates (Beiglböck, Henry-Labordère, Penkner, Model-independent bounds for option prices, Finance Stoch. 2013). Because the martingale constraint ties together all points with the same first coordinate, the classical re-pairing argument does not carry over: swapping two destinations generally destroys the martingale property.

M. Beiglböck and N. Juillet (On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 2016; arXiv:1208.1509v2) prove a martingale replacement for $c$ -cyclical monotonicity, the variational lemma (Lemma 1.11). It is the tool from which they derive the left-monotone structure of optimal plans, the uniqueness of the left-curtain coupling as optimizer for costs $h(y-x)$ with $h'$ strictly convex, and the support bounds for optimizers. This mission is the first of a series formalizing that paper.

Setting

All measures live on $\mathbb R$ or $\mathbb R\times\mathbb R$ with their Borel $\sigma$ -algebras. Two probability measures $\mu,\nu$ on $\mathbb R$ with finite first moment are in convex order, $\mu\preceq_C\nu$ , if $\int\varphi\,d\mu\le\int\varphi\,d\nu$ for every convex $\varphi:\mathbb R\to\mathbb R$ .

A transport plan is a measure $\pi$ on $\mathbb R^2$ with first marginal $\mu$ and second marginal $\nu$ . It is a martingale transport plan, $\pi\in\Pi_M(\mu,\nu)$ , if under $\pi$ the conditional mean of $y$ given $x$ equals $x$ ; equivalently,

\int\rho(x)\,(y-x)\,d\pi(x,y)=0\quad\text{for every bounded Borel }\rho .

A cost is a Borel function $c:\mathbb R^2\to\mathbb R$ satisfying the sufficient integrability condition $c(x,y)\ge a(x)+b(y)$ with $a\in L^1(\mu)$ , $b\in L^1(\nu)$ ; then the cost of a plan, $\int c\,d\pi$ , is well defined in $(-\infty,+\infty]$ . A plan $\pi\in\Pi_M(\mu,\nu)$ is optimal if $\int c\,d\pi\le\int c\,d\pi'$ for every $\pi'\in\Pi_M(\mu,\nu)$ , and it leads to finite costs if $\int c\,d\pi<+\infty$ .

A measure $\alpha'$ on $\mathbb R^2$ is a competitor of $\alpha$ (Definition 1.10) if it has the same two marginals as $\alpha$ and the same conditional barycentres: $\int y\,d\alpha_x(y)=\int y\,d\alpha'_x(y)$ for almost every $x$ , where $(\alpha_x)$ , $(\alpha'_x)$ are disintegrations with respect to the first marginal. A competitor redistributes the mass of $\alpha$ in a way that a martingale plan could absorb: replacing a piece $\alpha$ of a martingale plan by $\alpha'$ keeps both marginals and the martingale property.

Formalization targets

Goal: the variational lemma (Lemma 1.11, p. 8)

Let $\mu\preceq_C\nu$ be probability measures, $c$ a Borel cost satisfying the sufficient integrability condition, and $\pi\in\Pi_M(\mu,\nu)$ optimal with $\int c\,d\pi<+\infty$ . Then there is a Borel set $\Gamma\subseteq\mathbb R^2$ with $\pi(\Gamma)=1$ such that

\int c\,d\alpha\le\int c\,d\alpha'\quad\text{for every finitely supported }\alpha\text{ with }\operatorname{spt}\alpha\subseteq\Gamma\text{ and every competitor }\alpha'\text{ of }\alpha .

The set $\Gamma$ is chosen once, before $\alpha$ ; the quantifier order is the content.

Milestones

The milestones are the steps of the paper's proof (§3, pp. 16–19), in attack order:

Theorem 3.1 (p. 17), Kellerer's duality in the form of Beiglböck–Goldstern–Maresch–Schachermayer: for a Polish probability space $(Z,\zeta)$ and a Borel $M\subseteq Z^n$ , either $M\subseteq\bigcup_i M_i$ with $\zeta(\operatorname{proj}^iM_i)=0$ , or some measure $\gamma$ with $\gamma(M)>0$ has all marginals $\le\zeta$ .
The set $M\subseteq(\mathbb R^2)^n$ of $n$ -tuples carrying a non-optimal finite measure is Borel (p. 17).
In case (1), a Borel $\Gamma_n$ of full $\pi$ -measure supports no improvable $\alpha$ with $|\operatorname{spt}\alpha|\le n$ (p. 18).
Every finitely supported $\alpha$ has a cost-minimizing competitor (p. 18).
If $\omega\le\pi$ and a competitor $\omega'$ is cheaper than $\omega$ , then $\pi-\omega+\omega'$ is a cheaper martingale plan (p. 18).
For an optimal $\pi$ of finite cost, case (2) cannot occur (pp. 18–19).
$\Gamma=\bigcap_n\Gamma_n$ is as required (p. 17).

Significance

The result. The variational lemma converts optimality of a martingale plan, a property of a measure, into a condition on finite configurations of points in its support. In the paper it is applied, together with a lemma on accumulation points of sections (Lemma 3.2), to show that optimizers for costs $h(y-x)$ with $h'$ strictly convex are left-monotone, which by the paper's Theorem 1.5 identifies them as the left-curtain coupling; it also yields the bound $|\operatorname{spt}\pi_x|\le k$ of Theorem 7.1 and the two-graph structure of the optimizers for $\pm|y-x|$ . Later missions of this series use it as a milestone. Its converse, under continuity assumptions, is the separate Lemma A.2 of the paper's appendix.

Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization needs a usable form of Kellerer's duality for multi-marginal problems, which is not in Mathlib, and the bookkeeping that finite rearrangements of a martingale plan stay in $\Pi_M(\mu,\nu)$ . Both are reusable well beyond this paper: Kellerer's theorem underlies the analogous results for classical, multi-marginal and martingale transport.

Difficulty

The classical proof of $c$ -cyclical monotonicity perturbs an optimal plan by moving a small amount of mass around a finite cycle of its support points. For martingale plans this fails: the perturbation must preserve the conditional barycentre of every $x$ , and mass sitting at isolated points of a non-atomic plan cannot be moved without moving mass at uncountably many other points. The proof therefore cannot argue point by point. It works with whole families of bad configurations at once, which requires the measure-theoretic duality of Kellerer (resting on Choquet's capacitability theorem) and a measurable choice of an optimal competitor for each configuration. Proving that the set of bad configurations is Borel, and that a positive-mass family of them can be glued into a cheaper competitor $\omega'$ of a piece $\omega\le\pi$ , is the technical core.

Formalization scope

The Lean development uses Mathlib's Measure ℝ and Measure (ℝ × ℝ). Costs and integrals that may be infinite take values in EReal, through the published definition ModelRiskOT.Duality.extIntegral ( $\int f^+-\int f^-$ , with $(+\infty)-(+\infty)=-\infty$ ); no Bochner integral of a possibly non-integrable function is compared. Martingale plans and competitors are encoded through test functions $\rho(x)$ (the paper's characterization (4), p. 10) instead of disintegrations. A finitely supported finite measure is written $\sum_{s\in S}w_s\delta_s$ with $S$ a finite set and weights $w_s\ge0$ ; this covers every such measure, and masses are taken finite. $(\mathbb R^2)^n$ is Fin n → ℝ × ℝ.

Committed conventions and disclosed additions:

the goal's hypothesis "leads to finite costs" is $\int c\,d\pi<+\infty$ ; without it, a cost under which every plan has infinite cost makes optimality empty;
Theorem 3.1 is stated for Borel $M$ , the case proved in the cited source and the only case the paper uses; $\zeta(\operatorname{proj}^iM_i)=0$ is the outer measure, since the projections need not be Borel;
in milestone 3, $\Gamma_n$ is a Borel subset of the paper's $\mathbb R^2\setminus N$ of full measure, because $N$ need not be Borel;
milestone 4 states, for the uniform measure $\alpha_p$ on the points of an $n$ -tuple $p$ , both that an optimal competitor $\alpha'_p$ exists and that it can be chosen measurably in $p$ (p. 18), with Mathlib's σ-algebra on the space of measures.

A formalization in which $\Gamma$ is empty or $\pi$ -null, or in which $\Gamma$ is allowed to depend on $\alpha$ , is trivial and is ruled out by the statement: $\pi(\Gamma^c)=0$ and $\exists\Gamma\,\forall\alpha$ . The competitor $\alpha'$ ranges over all measures, not only finitely supported ones.

Welcome contributions: a general form of Kellerer's duality theorem (milestone 1), the Borel-measurability of the bad set, and the gluing step of milestone 6.

Selected references

M. Beiglböck, N. Juillet, On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 42–106, 2016. arXiv:1208.1509, doi:10.1214/14-AOP966
M. Beiglböck, M. Goldstern, G. Maresch, W. Schachermayer, Optimal and better transport plans, J. Funct. Anal. 256(6), 1907–1927, 2009. doi:10.1016/j.jfa.2009.01.013
H. G. Kellerer, Duality theorems for marginal problems, Z. Wahrsch. Verw. Gebiete 67(4), 399–432, 1984. doi:10.1007/BF00532047
M. Beiglböck, P. Henry-Labordère, F. Penkner, Model-independent bounds for option prices — a mass transport approach, Finance Stoch. 17(3), 477–501, 2013. doi:10.1007/s00780-013-0205-8
C. Villani, Optimal Transport, Old and New, Springer, 2009. doi:10.1007/978-3-540-71050-9

11 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Error Bounds, Quadratic Growth, and Linear Convergence of Proximal Methods II: Dual Strict Complementarity and Firm Convexity of the Components Give the Error Bound for f(Ax) + g(x)Research Paper

Motivation

Proximal gradient methods are used to minimize an objective with one smooth part and one convex part whose proximal map can be evaluated. A small proximal gradient step is a practical stopping signal, but it indicates proximity to an optimizer only when the objective has an appropriate error bound. Section 4 of Drusvyatskiy and Lewis gives conditions for that bound in the structured problem $f(Ax)+g(x)$ : the conditions concern the dual problem and the growth of the two component functions, rather than requiring strong convexity of their sum. This matters for problems with a nontrivial solution set and for penalties that are not strongly convex. The paper places this result after its §3 comparison of quadratic growth and proximal gradient error bounds (pp. 9–11).

Setting

Let $E_n=\mathbb R^n$ and $E_m=\mathbb R^m$ , with their Euclidean inner products and norms. Let $A:E_n\to E_m$ be linear, $f:E_m\to\mathbb R$ be continuously differentiable and convex, and $g:E_n\to(-\infty,+\infty]$ be proper, lower semicontinuous, and convex. The primal objective and its minimizer set are

\varphi(x)=f(Ax)+g(x),\qquad S=\operatorname*{argmin}_{x\in E_n}\varphi(x).

The mission assumes $S$ is nonempty and bounded. Its minimum $\varphi^*$ is finite. For an extended-real function $h$ , its Fenchel conjugate is $h^*(v)=\sup_z\{\langle v,z\rangle-h(z)\}$ . The dual objective is $\Psi(y)=f^*(y)+g^*(-A^\top y)$ , and $\bar y$ denotes a dual minimizer. The effective domain is $\operatorname{dom}h=\{z:h(z)<+\infty\}$ ; $\operatorname{ri}$ denotes relative interior. The paper assumes dual nondegeneracy, $0\in A^\top(\operatorname{ri}\operatorname{dom}f^*)+\operatorname{ri}\operatorname{dom}g^*$ , and dual strict complementarity, $0\in\operatorname{ri}\partial\Psi(\bar y)$ (p. 10).

A closed convex function $h$ is firmly convex relative to $v$ when its tilt $h_v(x)=h(x)-\langle v,x\rangle$ grows at least quadratically away from its minimizers on each compact set. The positive coefficient may depend on the compact set. Theorem 4.2 assumes this property for $f$ at $\bar y$ and for $g$ at $-A^\top\bar y$ (Definition 4.1, p. 11).

For $t>0$ , a proximal gradient step is $p=\operatorname{prox}_{tg}(x-t\nabla(f\circ A)(x))$ , and its residual is $G_t(x)=t^{-1}(x-p)$ . The error bound asks whether the distance from $x$ to $S$ is controlled by $\|G_t(x)\|$ whenever $x$ lies below a prescribed objective threshold (Definition 3.1, p. 5).

Formalization targets

Component and composite growth

The milestone path records the Kuhn–Tucker description of $S$ , the relative-interior identity (4.3), the compact-set distance estimate (4.4), the two component inequalities (4.5), and the resulting quadratic growth of $\varphi$ on every sublevel set. In particular, for each $\nu>0$ there is $\mu>0$ such that

\varphi(x)\ge\varphi^*+\mu\operatorname{dist}^2(x,S) \quad\text{if }\varphi(x)\le\varphi^*+\nu.

These are the claims stated in §4 and in the proof of Theorem 4.2, pp. 10–11. The milestone for (4.5) retains the paper's printed $c,\alpha\ge0$ in its quotation, while the Lean statement uses positive constants, as Definition 4.1 requires for nontrivial quadratic growth.

Goal: a proximal gradient error bound

The goal is Theorem 4.2: under the conditions above, for every $t>0$ there exist $\gamma,\nu>0$ such that

\operatorname{dist}(x,S)\le\gamma\|G_t(x)\| \quad\text{whenever }\varphi(x)\le\varphi^*+\nu.

The formal statement makes explicit that $\nabla f$ has a Lipschitz constant. This is part of the §3 setting used by the paper's Corollary 3.6 to reach the displayed error bound. A companion statement, Theorem 4.5, pp. 12–13, says that the Moreau envelope of a firmly convex function retains firm convexity relative to the same vector.

Significance

The conclusion converts dual geometric information and component growth into an error bound expressed through a proximal gradient step. The residual is available when running the method, whereas the distance to $S$ is generally not. Combined with the paper's §3 results, the error bound yields local convergence guarantees for the proximal gradient method in structured convex problems (Corollary 3.6 and Theorem 4.2). The statement covers settings in which component functions have local quadratic growth after a tilt while the composite objective need not be strongly convex.

The research result is proved in the paper. The work of this mission is to formalize its exact assumptions and claims, including the convex dual and the relative-interior statements, then supply machine-checked proofs. The resulting Euclidean conjugate, firm-convexity, and structured-objective definitions can also support other convex optimization formalizations. The statements in this proposal are proof obligations; compiling the statements alone does not establish the theorems.

Difficulty

Component growth concerns distance to separate subdifferential inverse images. The desired error bound concerns distance to their intersection, which is the primal solution set. Two small component distances do not automatically control distance to an intersection: the sets can meet at a poor angle. The dual interior hypotheses supply the regularity needed in (4.4). The argument also changes the quantity being controlled from objective growth to a proximal gradient residual. Those two changes are the substantive steps a proof must justify; treating either as an unrestricted distance identity would change the theorem.

Formalization scope

The Lean spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); dimensions zero are permitted. The linear map is continuous, and $A^\top$ is its adjoint. Extended-real values use EReal; properness excludes $-\infty$ values, and lower semicontinuity encodes closedness. Conjugates take suprema in EReal, and the dual objective follows (4.2). Relative interior is intrinsicInterior ℝ. The published convex subdifferential, proper-convex predicate, and proximal-point predicate are imported as reference items because their meanings match the paper's objects. The paper's Euclidean conjugate is defined locally because the available published conjugate has a strong-dual codomain.

The minimum value is real and is pinned to the nonempty primal minimizer set. The dual point is pinned as a minimizer of $\Psi$ . Proximal steps are expressed as argmin predicates, so no default result is chosen for a failed minimization. The firm-convexity predicate requires a nonempty minimizer set of the tilted function: otherwise Lean's real distance to the empty set would be zero while the source uses an infinite distance. The growth constant $\alpha$ of Definition 4.1 and the constants $c,\alpha$ of (4.5) are strictly positive: the page leaves the sign implicit or prints $\ge 0$ , but with a zero constant every convex function would be firmly convex, contradicting the page's own example $x^4$ , and the growth statements would be empty. The error bound is restricted to the stated sublevel set, and all of its constants are positive. The goal includes a nonnegative Lipschitz constant for $\nabla f$ , disclosed because the source's §3 bridge to the error bound assumes one; the component-growth milestones do not assume it.

Contributions should establish the Euclidean convex-duality identities, the compact-set regularity estimate, the component and composite growth claims, and the proximal gradient conclusion. The Moreau-envelope preservation theorem is a separate companion target. None of the dual interior conditions or the firm-convexity assumptions may be replaced by a vacuous condition: the goal concerns their effect on the actual solution set of $f(Ax)+g(x)$ .

Selected references

D. Drusvyatskiy and A. S. Lewis, Error bounds, quadratic growth, and linear convergence of proximal methods, Mathematics of Operations Research 43(3), 2018. arXiv:1602.06661v2.

10 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Optimality Gap of Constant-Order Policies Decays Exponentially in the Lead Time for Lost Sales Models: C(π_r∞)/OPT(L) ≤ 1 + h((1−γ)g)⁻¹(E[D] − r∞ + (eϑ(L+1))⁻¹)γ^{L+1} for Every Lead Time L ≥ 1Research Paper

Why lost-sales inventory with lead times matters

In many retail and spare-parts settings, demand that cannot be met from stock is lost rather than backlogged, and replenishment orders arrive only after a positive lead time. The resulting lost-sales inventory model is a basic model of inventory theory. Its optimal policy depends on the whole pipeline of outstanding orders, so dynamic programming over that state becomes intractable as the lead time grows. This is why the model is often replaced by its backlogged counterpart, even when that approximation is poor (Bijvank and Vis, 2011).

Simple heuristics are therefore of practical interest. The simplest is the constant-order policy, which orders the same amount in every period regardless of the state. Reiman (2004, unpublished manuscript) showed that the best constant-order policy sometimes outperforms the base-stock policy, and Goldberg, Katz-Rogozhnikov, Lu, Sharma and Squillante (arXiv:1211.4063, Math. Oper. Res. 2016) proved that it is asymptotically optimal as the lead time grows, with a gap that decays polynomially in the lead time. Xin and Goldberg (arXiv:1409.1499v2, Oper. Res. 2016) proved that for the infinite-horizon average-cost problem the gap actually decays exponentially, with an explicit rate and explicit constants. This mission formalizes that result.

Timeline:

1958: Karlin and Scarf introduce the lost-sales model with a positive lead time; convexity results follow in Karlin and Scarf (1958) and Morton (1969).
1962: Kingman bounds how fast the expected waiting time of an initially empty GI/G/1 queue approaches its steady-state value (doi).
2004: Reiman finds that the best constant-order policy can outperform the base-stock policy.
2009: Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science 55(3)) prove base-stock policies asymptotically optimal as the lost-sales penalty grows.
2011: Huh, Janakiraman and Nagarajan (Operations Research 59(1)) give the existence of stationary optimal policies used by the paper.
2015–2016: Goldberg et al. prove asymptotic optimality of constant-order policies as the lead time grows; Xin and Goldberg prove exponential decay of the gap.

The setting

Demands $D_1,D_2,\dots$ are i.i.d. copies of a nonnegative random variable $D$ with law $\mathcal D$ , finite mean $\mathbb E[D]$ and strictly positive variance. The lead time $L\ge1$ is an integer, $h>0$ is the unit holding cost and $p>0$ the unit lost-sales penalty. At the start of period $t$ there is on-hand inventory $I_t$ and a pipeline $\mathbf x_t=(x_{1,t},\dots,x_{L,t})$ of orders placed but not yet delivered. In each period, $x_{1,t}$ arrives, a new order is placed (it enters the end of the pipeline), demand $D_t$ is realized, and the period cost

C_t=h\,(I_t+x_{1,t}-D_t)^++p\,(I_t+x_{1,t}-D_t)^-

is incurred; then $I_{t+1}=(I_t+x_{1,t}-D_t)^+$ . The system starts empty. A policy $\pi$ chooses orders from the information available, and its long-run average cost is $C(\pi)=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$ . The optimal cost is $\mathrm{OPT}(L)=\inf_\pi C(\pi)$ .

The constant-order policy $\pi_r$ orders $r$ in every period. Its cost is governed by the random walk $jr-\sum_{i=1}^jD_i$ through

I^r_\infty=\sup_{j\ge0}\Big(jr-\sum_{i=1}^jD_i\Big),\qquad I^r_L=\max_{j=0,\dots,L}\Big(jr-\sum_{i=1}^jD_i\Big),

the steady-state and $L$ -th waiting times of a single-server queue with interarrival law $\mathcal D$ and constant service time $r$ . The best constant order $r_\infty$ is the least minimizer of $C(\pi_r)$ over $0\le r\le\mathbb E[D]$ . The rate and constants are

\gamma=\inf_{\theta\ge0}e^{\theta r_\infty}\mathbb E[e^{-\theta D}],\qquad g=\inf_{x\in\mathbb R}\mathbb E\big[h(x-D)^++p(x-D)^-\big],

with $\vartheta$ the largest minimizer in the definition of $\gamma$ ( $\vartheta=\infty$ if the infimum is not attained, and $1/\infty=0$ ).

Formalization targets

Goal: Theorem 1 (p. 8)

\frac{C(\pi_{r_\infty})}{\mathrm{OPT}(L)}\le1+h\big((1-\gamma)g\big)^{-1}\Big(\mathbb E[D]-r_\infty+\big(e\vartheta(L+1)\big)^{-1}\Big)\gamma^{L+1}\qquad\text{for all }L\ge1 .

The quantities $r_\infty,\gamma,\vartheta,g$ depend on $\mathcal D,h,p$ but not on $L$ .

Milestones, in the order the proof uses them

Eq. (3): $C(\pi_r)=h\,\mathbb E[I^r_\infty]+p\,\mathbb E[D]-pr$ for $r\in[0,\mathbb E[D])$ .
Sec. 2.2: the best constant exists and $r_\infty<\mathbb E[D]$ ; Sec. 2.3: $\vartheta>0$ , $\gamma\in[0,1)$ , $g>0$ and $\mathrm{OPT}(L)\ge g$ .
Observation 1 (convexity of $\mathfrak f_{\mathbf d}$ and a Jensen bound) and Lemma 2: $\mathrm{OPT}(L)\ge C_L(r_L)$ and the decomposition (5) of $C(\pi_{r_\infty})-\mathrm{OPT}(L)$ .
Lemma 3 (Kingman's series and the tail bound), Lemma 4 ( $r_\infty\le r_L$ ), Lemma 5 ( $\sum_n\mathbb P(nr_\infty\ge\sum_{i\le n}D_i)\ge p/h$ ), the Chernoff step $\mathbb P(nr_\infty\ge\sum_{i\le n}D_i)\le\gamma^n$ , and the bound on the term (6).
Further: Lemma 1 (monotonicity of $\gamma$ in $p/h$ ) and Corollary 1 (the closed form for exponential demand).

Significance

The theorem shows that a lead time of order $\log(\epsilon^{-1})$ suffices for the constant-order policy to be within a factor $1+\epsilon$ of optimal, whereas the earlier bounds of Goldberg et al. needed a lead time polynomial in $\epsilon^{-1}$ . The constants are explicit and computable from the demand law: for exponential demand with $p=h$ and $L=1$ the bound is already about $3.36$ , and it approaches $1$ quickly as $L$ grows (Table 1 of the paper). Lemma 1 adds that the rate $\gamma$ worsens as $p/h$ grows, the regime opposite to the one in which base-stock policies are known to be nearly optimal.

The result is proved on paper; no machine-checked proof is known to exist. A formalization would produce a checked infinite-horizon lost-sales model and a checked statement of Kingman's random-walk identities for this queue. It would also produce checked comparisons of an arbitrary history-dependent policy with constant-order policies through convexity. The statement here is taken over a policy class at least as large as the paper's, so a proof also extends the result to randomized history-dependent policies.

Difficulty

The cost of the constant-order policy is the expected supremum of a random walk, while the optimal policy has no closed form and may not even induce a stationary distribution. The paper avoids the steady state of the optimal policy by constructing a random vector with the needed stationarity properties (Theorem 2). That construction is not part of this mission. Here, the lower bound on $\mathrm{OPT}(L)$ in Lemma 2 instead goes through the published, proved lower certificate for the full policy class. The second obstacle is quantitative: the exponential rate comes from comparing the minimizers $r_\infty$ and $r_L$ of two different convex functions (Lemma 4) and from a first-order optimality condition involving a non-differentiable expectation (Lemma 5). Neither follows from the observation that one function dominates the other.

Formalization scope

The model is the published CappedBaseStock model: zero-based time, an empty initial state, demand laws on $[0,\infty)$ with finite positive mean, and costs and long-run averages in $[0,\infty]$ . $\mathrm{OPT}(L)$ is the infimum over all measurable, history-dependent, possibly randomized policies. That class contains the paper's Markov deterministic class $\Pi$ , so every statement involving $\mathrm{OPT}(L)$ is at least as strong as printed. "Strictly positive variance" is encoded as "the demand law is not a point mass". It is a hypothesis wherever the paper's argument needs it; the Chernoff step, eq. (3) and Corollary 1 do not need it.

$C(\pi_r)$ is the model's long-run cost of the constant policy, not formula (3), and $\mathbb E[I^r_\infty]$ is a lower integral in $[0,\infty]$ , so that eq. (3) and Lemma 3 are not true by definition. $r_\infty$ and $r_L$ are infima of the argmin sets, whose nonemptiness is a milestone. $1/\vartheta$ is encoded with the paper's convention $1/\infty=0$ . Lemma 3's tail bound is stated additively in $[0,\infty]$ , and the series in Lemmas 3 and 5 are extended-real series indexed from $0$ . The goal's ratio is taken in $[0,\infty]$ , where $x/0=\infty$ for $x\neq0$ . None of $\gamma<1$ , $g>0$ or $r_\infty<\mathbb E[D]$ is assumed: all three are milestones. A formalization that defines $\mathrm{OPT}$ over constant-order policies only, fixes $r$ instead of $r_\infty$ , treats $\gamma,\vartheta,g$ as free parameters, or takes the ratio in $\mathbb R$ after truncating infinite costs would make the goal trivial and is ruled out. The objects are defined from the full parameter record, which includes $L$ . That they do not depend on $L$ follows from eq. (3) and the existence milestone.

No statement corrects a printed slip. Theorem 2 (existence of the stationary vector) and eq. (2) (bounded stationary optimal policies) are not stated; Observation 1 instead takes Theorem 2's properties (i)–(iii) as hypotheses on an arbitrary law. The source is arXiv:1409.1499v2, whose printed page numbers equal the PDF's. Useful infrastructure: Lindley-type random-walk suprema, Spitzer–Kingman identities, Chernoff bounds for i.i.d. sums (Mathlib's measure_le_le_exp_mul_mgf), and Cesàro limits of expected costs. All of it is reusable for other queueing and inventory missions. Proofs of any milestone are welcome, and the Chernoff step is the natural entry point.

Selected references

L. Xin, D. A. Goldberg, Optimality gap of constant-order policies decays exponentially in the lead time for lost sales models, Operations Research 64(6), 2016; preprint arXiv:1409.1499v2. https://arxiv.org/abs/1409.1499v2
D. A. Goldberg, D. A. Katz-Rogozhnikov, Y. Lu, M. Sharma, M. S. Squillante, Asymptotic optimality of constant-order policies for lost sales inventory models with large lead times, Mathematics of Operations Research, 2016; preprint arXiv:1211.4063. https://arxiv.org/abs/1211.4063
J. F. C. Kingman, Some inequalities for the queue GI/G/1, Biometrika 49, 1962. https://doi.org/10.1093/biomet/49.3-4.315
M. Bijvank, I. F. A. Vis, Lost-sales inventory theory: a review, European Journal of Operational Research 215(1), 2011. https://doi.org/10.1016/j.ejor.2011.02.004
S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97236

21 thms2 active usersReviewed

Completed

Analysis Operations Research Optimization·Captain: mikedeng1

Extrapolated Proximal Subgradient Algorithms for Nonconvex and Nonsmooth Fractional Programs 3: Enhanced e-PSG Cluster Points Are Strong Lifted Stationary Points for Max-Type DenominatorsResearch Paper

Motivation

Fractional programs minimize a ratio $f(x)/g(x)$ over a constraint set. They arise whenever a quantity has to be normalized: the scale-invariant sparse recovery model minimizes $\|x\|_1/\|x\|_2$ (Rahimi, Wang, Dong, Lou 2019), robust Sharpe-ratio portfolio selection maximizes a mean-to-worst-case-risk ratio, and generalized eigenvalue problems minimize Rayleigh quotients. Classical methods such as Dinkelbach's algorithm assume convex $f$ and concave $g$ ; many modern instances have neither.

Boţ, Dao and Li (arXiv:2003.04124, Math. Oper. Res. 2022) study the nonconvex nonsmooth case in which the numerator is a smooth convex part plus a lower semicontinuous part and the denominator is weakly convex on the constraint set. Their basic method, the extrapolated proximal subgradient (e-PSG) algorithm, converges subsequentially to lifted stationary points. When the denominator is a maximum of finitely many smooth functions, a lifted stationary point may be spurious: it only requires one element of the subdifferential of $g$ to balance the numerator. Section 6 of the paper proposes an enhanced algorithm, in the spirit of the enhanced DC algorithm of Pang, Razaviyayn, Alvarado 2017, whose cluster points satisfy the stronger condition for all such elements. This mission formalizes that result.

Setting

$H$ is a finite-dimensional real Hilbert space, $S\subseteq H$ is nonempty, closed and convex, and the problem is

\min_{x\in S}\ \frac{f(x)}{g(x)} .\qquad (P)

Numerator (Assumption 1). $f=f^{\mathfrak s}+f^{\mathfrak n}$ , where $f^{\mathfrak s}:H\to\mathbb R$ is convex and continuously differentiable with an $\ell$ -Lipschitz gradient, $f^{\mathfrak n}:H\to(-\infty,+\infty]$ is proper and lower semicontinuous, $S\cap\operatorname{dom}f\neq\emptyset$ , and $f\ge0$ on $S\cap\operatorname{dom}f$ .
Denominator (Assumption 2′). $g=\max\{g_i:1\le i\le p\}$ , each $g_i$ continuously differentiable on an open set containing $S$ and weakly convex on $S$ with modulus $\beta\ge0$ , meaning $g_i+\frac\beta2\|\cdot\|^2$ is convex on $S$ . The boundedness condition (BC) holds: $m\le g\le M$ on $S\cap\operatorname{dom}f$ for some $m,M>0$ .
Active sets. $I_\varepsilon(x)=\{i: g_i(x)\ge g(x)-\varepsilon\}$ ; $I_0(x)$ is the set of indices attaining the maximum.
Subdifferentials. $\partial_L$ is the limiting (Mordukhovich) subdifferential, and $\iota_S$ is the indicator of $S$ .
Strong lifted stationarity (Definition 3.1(iii)). $\bar x\in S$ is a strong lifted stationary point if $f(\bar x)\,\partial_L g(\bar x)\subseteq g(\bar x)\,\partial_L(f+\iota_S)(\bar x)$ .

Algorithm 2 starts from $x_{-1}=x_0\in S\cap\operatorname{dom}f$ . At step $n$ it sets $\theta_n=f(x_n)/g(x_n)$ , picks a step size $\tau_n$ and extrapolation weights $\kappa_n\in[0,\bar\kappa]$ , $\mu_n\in[0,\bar\mu\tau_n]$ , and forms $u_n=x_n+\kappa_n(x_n-x_{n-1})$ and $v_n=x_n+\mu_n(x_n-x_{n-1})$ . For every $i\in I_\varepsilon(x_n)$ it computes a proximal candidate

w_n^{i}\in\operatorname*{argmin}_{x\in S}\Big(f^{\mathfrak n}(x)+\langle\nabla f^{\mathfrak s}(u_n),x\rangle+\tfrac1{2\tau_n}\|x-v_n-\tau_n\theta_n\nabla g_i(x_n)\|^2+\tfrac\ell2\|x-u_n\|^2\Big)

(up to constants), and keeps as $x_{n+1}$ the candidate minimizing the merit value $f(w)-\theta_n g(w)+\frac12\big(\frac{1-\sqrt\beta\zeta}{\tau_n}-\frac{M\mu_n}{\sqrt{mM}\tau_n}\big)\|w-x_n\|^2$ .

Formalization targets

Goal: Theorem 6.1(iii)

Assume the sublevel set $S_0=\{x\in S: f(x)/g(x)\le f(x_0)/g(x_0)\}$ is bounded and $\liminf_n\tau_n=\bar\tau>0$ . Then every cluster point $\bar x$ of $(x_n)$ satisfies $\bar x\in S\cap\operatorname{dom}f$ , $f(x_n)/g(x_n)\to f(\bar x)/g(\bar x)$ ,

\frac{f(\bar x)}{g(\bar x)}\bigcup_{i\in I_0(\bar x)}\nabla g_i(\bar x)\subseteq\partial_L(f+\iota_S)(\bar x),\qquad(28)

and, if $f$ is weakly convex on $S$ , $\bar x$ is a strong lifted stationary point of (P).

Milestones, in proof order

Lemma 4.4 (descent lemma; already proved on the platform) and Lemma 4.3 (subgradient inequality for weakly convex functions).
Inequality (32): the merit value of $x_{n+1}$ is at most that of any candidate, which is bounded by a model of $f$ at any $x\in S$ .
The one-step decrease of $f(x_n)/g(x_n)$ that follows from (32).
Theorem 6.1(i): $x_n\in S\cap\operatorname{dom}f$ , and the sequence $F_n=f(x_n)/g(x_n)+\big(\frac{\ell\bar\kappa^2}{2m}+\frac{\bar\mu}{2\sqrt{mM}}\big)\|x_n-x_{n-1}\|^2$ of (27) is nonincreasing and convergent.
Theorem 6.1(ii): the iterates are bounded and $\sum_n\|x_{n+1}-x_n\|^2<+\infty$ .
The limit inequality at a cluster point, and inclusion (34) (= (28)).
Lemma 2.2(i): $\partial_L(h+\iota_S)$ is closed and convex for weakly convex $h$ .

Significance

For max-type denominators the result separates the enhanced algorithm from the basic one. A lifted stationary point only needs $0\in g(\bar x)\partial_L(f+\iota_S)(\bar x)-f(\bar x)\partial_L g(\bar x)$ . The paper's Example 3.3 ( $\min_{|x|\le1}(x^2+1)/(|x|+1)$ ) has the lifted stationary point $0$ , which is not a local minimizer; the strong lifted stationary points of that example are exactly its minimizers. Lemma 3.4 of the paper identifies strong lifted stationarity with d-stationarity of $f-\frac{f(\bar x)}{g(\bar x)}g$ on $S$ when $f+\iota_S$ and $g$ are weakly convex. This is the sharpest first-order notion used for DC-type programs.

The theorem is proved in the paper (pp. 22–24). No machine-checked version of it, of the e-PSG analysis, or of lifted stationarity exists on the platform. Formalizing it checks the step-size bookkeeping that the printed algorithm gets wrong (see below). It also produces reusable statements about weakly convex functions and the limiting subdifferential of $h+\iota_S$ .

Difficulty

The descent part follows the template of the basic e-PSG analysis, but the merit criterion couples the candidate selection with the extrapolation: the coefficient $\frac{1-\sqrt\beta\zeta}{\tau_n}-\frac{M\mu_n}{\sqrt{mM}\tau_n}$ has to stay positive, and the cross term $\langle w-x_n,x_n-x_{n-1}\rangle$ has to be split with the specific weight $\sqrt{m/M}$ for the constants of (27) to close.

The limit step is the main obstacle. The algorithm works with $I_\varepsilon(x_n)$ , but the conclusion concerns $I_0(\bar x)$ at a limit point. One must show that every index active at $\bar x$ was a candidate along the subsequence. One must also show that $f(x_{k_n+1})\to f(\bar x)$ although $f$ is only lower semicontinuous. The naive approach, passing to the limit in the optimality condition of a single subproblem, gives one element of $\partial_L g(\bar x)$ only, which is lifted stationarity again. The final step needs the limiting subdifferential of a finite max of $C^1$ functions to be the convex hull of the active gradients. The paper uses this fact without proof, and Mathlib does not provide it for $\partial_L$ .

Formalization scope

Carrier. $H$ is EuclideanSpace ℝ (Fin N). Functions into $(-\infty,+\infty]$ are EReal-valued. $\partial_L$ is the published NonconvexSplitting.Shared.LimitingSubdiff, and properness is IsProperFn.
Indices and the max. Indices are Fin p with $p\ge1$ , so they run $0,\dots,p-1$ . $g$ is defined as Finset.sup' of the $g_i$ , never as an independent function. The standing assumptions of (P) are kept: $g$ is lower semicontinuous and positive on $S$ .
Weak convexity. "Modulus" means "a valid constant". For real $g_i$ it is ConvexOn of $g_i+\frac\beta2\|\cdot\|^2$ on $S$ . For extended-real $f$ it is convexity of the epigraph of $f+\iota_S+\frac\rho2\|\cdot\|^2$ .
Algorithm 2. A run is a predicate on iterates, candidates, selected indices, step sizes and weights. Each argmin is "some minimizer", candidates outside $I_\varepsilon(x_n)$ are unconstrained, $x_{-1}=x_0$ , and ratios are real numbers on $S\cap\operatorname{dom}f$ .
Two misprints corrected. Step 1 declares an unused $\omega$ and never declares $\varepsilon$ ; it is read as $\varepsilon>0$ . The printed step-size rule $\tau_n\le1/\max\{\beta\theta_n/(1-\zeta),\delta\}$ does not give the inequality $\beta\theta_n\le\sqrt\beta\zeta/\tau_n$ that the proof uses. The run therefore uses $\tau_n\le1/\max\{\sqrt\beta\theta_n/\zeta,\delta\}$ , the rule of Algorithm 1.
Other conventions. $\bar\tau$ is Filter.liminf τ atTop, which is well defined because $0<\tau_n\le1/\delta$ . The $\bar\kappa$ -range is multiplied out to avoid dividing by $\ell$ .
Ruled out. The theorem cannot be satisfied trivially: the run constrains every iterate, and the strong lifted conclusion quantifies over all of $\partial_L g(\bar x)$ . Membership $\bar x\in\operatorname{dom}f$ is concluded explicitly, so the toReal value of $+\infty$ never enters.
Needed infrastructure. The subgradient inequality for weakly convex functions, the convexity of $\partial_L(h+\iota_S)$ for weakly convex $h$ , a Fermat rule for $\partial_L$ , and the formula for $\partial_L\max_i g_i$ . Each is reusable beyond this paper, and a contribution of any of them is welcome.

Selected references

R. I. Boţ, M. N. Dao, G. Li, Extrapolated proximal subgradient algorithms for nonconvex and nonsmooth fractional programs, arXiv:2003.04124v2 (2020); Math. Oper. Res. 47 (2022). https://arxiv.org/abs/2003.04124
J.-S. Pang, M. Razaviyayn, A. Alvarado, Computing B-stationary points of nonsmooth DC programs, Math. Oper. Res. 42(1) (2017). https://doi.org/10.1287/moor.2016.0795
Y. Rahimi, C. Wang, H. Dong, Y. Lou, A scale invariant approach for sparse signal recovery, SIAM J. Sci. Comput. 41 (2019). https://arxiv.org/abs/1812.08852
B. S. Mordukhovich, Variational Analysis and Generalized Differentiation I, Springer, 2006. https://doi.org/10.1007/3-540-31247-1
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

16 thms2 active usersReviewed

Algebra Combinatorics Discrete Geometry·Captain: mikedeng1

Maximum Scattered Linear Sets and Complete Caps in Galois Spaces 2: For q = 2^t, t Even, and n ≥ 4 Even, AG(n, q) Has a Complete Cap of Size 2√(q^(n−1))Research Paper

Small complete caps in Galois spaces

A cap in an affine or projective space over a finite field is a set of points no three of which are collinear; a cap is complete when it is maximal with respect to inclusion, so that every point outside it lies on a line through two of its points. Caps are closely connected with error-correcting codes: projective caps can serve as parity-check columns for linear codes with minimum distance at least 4. Constructing small complete caps explicitly is a long-standing question in finite geometry; Giulietti's survey collects the known families.

Counting the lines through pairs of points gives the trivial lower bound

\sqrt{2} \cdot \sqrt{q^{n-1}} \qquad (1)

for the size of a complete cap in a Galois space of dimension $n$ and order $q$ . A short timeline:

Segre (1959) constructed complete caps of size $3q + 2$ in $PG(3, q)$ , $q$ even.
Pambianco and Storme (1996) generalized this to complete caps of size $2q^s$ in $AG(2s+1, q)$ , $q$ even: bound (1) is sharp up to a constant in odd dimension, for even $q$ .
Giulietti (2007) studied translation caps in $AG(r, 2^t)$ and the doubling construction, which turns a translation cap of the largest possible size into a complete cap one dimension higher.
Bartoli, Giulietti, Marino and Polverino (arXiv 2015, Combinatorica 2017) proved that (1) is sharp up to a constant also in even dimension $n \ge 4$ , when $q$ is an even square. This mission formalizes that result.

Setting

Let $q = 2^t$ and let $\mathbb F_q$ be the field with $q$ elements. The affine space $AG(r, q)$ has as points the vectors $(a_1, \dots, a_r) \in \mathbb F_q^r$ ; three points are collinear when they lie on a common affine line over $\mathbb F_q$ .

For an additive subgroup $G$ of $\mathbb F_q^r$ , $\mathcal K_G$ is the set of points whose coordinate vectors lie in $G$ . A translation cap is a cap of the form $\mathcal K_G$ . By Giulietti, Proposition 2.5, for $t > 1$ a translation cap has at most $q^{r/2}$ points; one attaining this bound is a maximal translation cap.

On the projective side, let $V = \mathbb F_{2^t}^r$ , so that $PG(V, \mathbb F_{2^t}) = PG(r-1, 2^t)$ . An $\mathbb F_2$ -subspace $U$ of $V$ (an additive subgroup) of $\mathbb F_2$ -dimension $k$ , the rank, defines the $\mathbb F_2$ -linear set $L_U = \{\langle u \rangle_{\mathbb F_{2^t}} : u \in U \setminus \{0\}\}$ . It is scattered when every point $\langle u\rangle$ meets $U$ in exactly $\{0, u\}$ , i.e. has weight one. A scattered linear set has rank at most $rt/2$ (Blokhuis–Lavrauw); one of rank $3t/2$ in the plane $PG(2, 2^t)$ is called maximum.

Formalization targets

Goal: Theorem 1.3

For $q = 2^t$ , $t$ even, and $n \ge 4$ even, there is a complete cap $S$ in $AG(n, q)$ with

|S| = 2\sqrt{q^{n-1}}.

The exponent $t(n-1)/2$ is an integer because $t$ is even.

Milestones

Theorem 4.2 ([6, Lemma 2.1]): for $q$ even, $\mathcal K_G$ is a translation cap iff any two distinct non-zero vectors of $G$ are $\mathbb F_q$ -linearly independent.
Proposition 4.3: for $t > 1$ , $L_U$ is a scattered $\mathbb F_2$ -linear set of $PG(r-1, 2^t)$ iff $\mathcal K_U$ is a translation cap of $AG(r, 2^t)$ .
The bound of [6, Prop. 2.5]: a translation cap in $AG(r, 2^t)$ , $t > 1$ , has at most $q^{r/2}$ points.
Lemma 4.5 ([6, Prop. 2.8]): the product of maximal translation caps in $AG(r, 2^t)$ and $AG(\bar r, 2^t)$ is a maximal translation cap in $AG(r + \bar r, 2^t)$ .
The parabola $\{(x, x^2) : x \in \mathbb F_{2^t}\}$ is a translation cap in $AG(2, 2^t)$ .
Lemma 4.6 (doubling, [6, Cor. 2.12]): if $\mathcal K_G$ is a maximal translation cap in $AG(r, 2^t)$ , then $\mathcal K_{G \times \{0,1\}}$ is a complete cap in $AG(r+1, 2^t)$ .
Proposition 4.7: a maximum scattered linear set in $PG(2, q)$ yields a complete cap in $AG(n, q)$ of size $2q^{(n-1)/2}$ .
The existence input, restated from Section 2: Lemma 2.8 and Proposition 2.9 (a suitable coefficient $b$ ), Theorem 2.10 (the scattered $\mathbb F_2$ -linear set $\{x^2 + bx^{2^{2n+1}} + x\omega\}$ of rank $3n$ in $PG(2, 2^{2n})$ , covering $t = 2n \ge 4$ ), and the Baer-subplane case $r = 3$ , $t = 2$ (covering $q = 4$ ).

Significance

Theorem 1.3 shows that the trivial bound (1) is sharp up to the factor $\sqrt 2$ in even dimension $n \ge 4$ for every even square $q$ , extending to even dimension what the constructions of Segre and Pambianco–Storme give in odd dimension. The construction supplies caps near the elementary size lower bound in a parameter range where the paper reports no comparably small infinite family. Remark 4.8 of the paper extends the construction to complete caps of comparable size in $PG(n, q)$ . The proof also establishes Proposition 4.3, a dictionary between scattered $\mathbb F_2$ -linear sets and translation caps, so that any new maximum scattered linear set yields new small complete caps.

The result is proved on paper; no machine-checked proof of it or of the cited results of [6] (Lemmas 4.5, 4.6 and the bound of Prop. 2.5, whose proofs are not in this paper) is known to exist. The mission produces a formal statement of Theorem 1.3, the cap–linear set correspondence, and formal statements of the three results the paper imports from [6].

Difficulty

Assembling Proposition 4.7 from the milestones is short. The difficulty lies in the inputs. The doubling construction requires showing that every point of $AG(r+1, q)$ outside $\mathcal K_{G\times\{0,1\}}$ lies on a secant, which uses the maximality $|G| = q^{r/2}$ in a counting argument; it is cited from [6], not proved in the paper. The existence of a maximum scattered linear set in $PG(2, 2^t)$ is the deep input: Lemma 2.8 needs a bound on the value set of a non-permutation polynomial (Turnwald) and a point count on a plane curve over $\mathbb F_{2^{3n}}$ . A tempting shortcut, taking any maximal cap obtained by greedy extension, gives a complete cap of unknown and generally much larger size; the content of the theorem is the exact size.

Formalization scope

$AG(r, q)$ is Fin r → K for a finite field $K$ with $|K| = 2^t$ ; collinearity is Mathlib's affine Collinear K, over $K$ itself. A complete cap is quantified against every point of $AG(r, q)$ .
Sizes are Set.ncard. The goal's size $2\sqrt{q^{n-1}}$ is written $2\cdot 2^{t(n-1)/2}$ with natural-number division, exact because $t$ is even; maximality of a translation cap is the squared form $|S|^2 = q^r$ , and the [6] bound is $|S|^2 \le q^r$ .
Scattered-ness is the weight-one condition " $c\,u \in U$ , $c \in \mathbb F_{2^t}$ , $u \ne 0$ imply $c \in \mathbb F_2$ "; rank $k$ means $|U| = 2^k$ . "Maximum" in Proposition 4.7 is read as rank $3t/2$ , as in the first line of its proof.
In Section 2, $\mathbb F_{2^m}$ is the fixed field of $x \mapsto x^{2^m}$ inside $E$ with $|E| = 2^{6n}$ ; norms are explicit Frobenius products. $\omega$ ranges over all of $\mathbb F_{2^{2n}} \setminus \mathbb F_{2^n}$ (the paper's standing $\omega$ ). Proposition 2.9 carries the standing assumption $n \ge 2$ of Section 2.
Lemmas 4.5, 4.6 and the [6] bound carry $t > 1$ ; for $t = 1$ every subset of $AG(r, 2)$ is a cap and Lemma 4.6 fails.
Ruled out: stating the goal with $\le$ or $\ge$ in place of the exact size, or measuring collinearity over $\mathbb F_2$ (over which every set is a cap), would make it trivial.
Citation basis: arXiv:1512.07467v1; all theorem numbers and pages refer to that version.

Welcome contributions: a general library of caps and translation caps in $AG(r, q)$ ; the scattered-linear-set/translation-cap dictionary; a formalization of the doubling construction of [6]; transport of the $\mathbb F_{2^{6n}}$ -model of Theorem 2.10 to coordinates $\mathbb F_{2^{2n}}^3$ . The linear-set definitions mirror those of the companion mission on scattered linear sets and are reusable there.

Selected references

D. Bartoli, M. Giulietti, G. Marino, O. Polverino, Maximum scattered linear sets and complete caps in Galois spaces, arXiv:1512.07467v1, 2015; Combinatorica 37 (2017). arXiv:1512.07467v1
[3] A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geom. Dedicata 81 (2000), 231–243. https://doi.org/10.1023/A:1005283806897
[6] M. Giulietti, Small complete caps in PG(N, q), q even, J. Combin. Des. 15(5) (2007), 420–436. https://doi.org/10.1002/jcd.20131
[7] M. Giulietti, The geometry of covering codes: small complete caps and saturating sets in Galois spaces, in Surveys in Combinatorics 2013, LMS Lecture Note Series 409, Cambridge University Press, 2013, pp. 51–90. https://doi.org/10.1017/CBO9781139506748.003
[17] F. Pambianco, L. Storme, Small complete caps in spaces of even characteristic, J. Combin. Theory Ser. A 75(1) (1996), 70–84. https://doi.org/10.1006/jcta.1996.0064
[19] B. Segre, On complete caps and ovaloids in three-dimensional Galois spaces of characteristic two, Acta Arith. 5 (1959), 315–332. https://doi.org/10.4064/aa-5-3-315-332
[20] G. Turnwald, A new criterion for permutation polynomials, Finite Fields Appl. 1 (1995), 64–82. https://doi.org/10.1006/ffta.1995.1005

14 thms2 active usersReviewed

Completed

Operations Research Optimal Transport Optimization+1·Captain: mikedeng1

Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes 4: A Worst-Case Distribution Is the Law of X + √δ G A(X)⁻¹β, Spending the Whole Budget δResearch Paper

Why the worst case matters

Distributionally robust optimization (DRO) replaces the expected loss $E_{P_0}[\ell(\beta^{\mathsf T}X)]$ of a linear decision rule $\beta$ by its worst case over all data laws $P$ within transport distance $\delta$ of the baseline $P_0$ . When $P_0$ is an empirical distribution this covers regularized regression and classification (Blanchet, Kang, Murthy 2019; Esfahani, Kuhn 2018). The optimal value is one number; a practitioner also wants to know which distribution realizes it, the adversary's best response. It shows which data points the robust model guards against, it gives stress-test scenarios, and its structure is what the paper's comparative statics (Theorem 7) and iterative schemes build on.

J. Blanchet, K. Murthy and F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes (arXiv:1810.02403v3; Math. Oper. Res. 47(2), 2022), answer this for a state-dependent Mahalanobis cost. Theorem 6 of that paper describes the worst-case distribution through the solution of the one-dimensional dual problem. This mission formalizes Theorem 6.

Setting

The data $X$ take values in $\mathbb R^d$ with law $P_0$ , a Borel probability measure. The decision $\beta$ ranges over a convex set $B\subseteq\mathbb R^d$ (a standing assumption of the paper). Moving mass from $x$ to $x'$ costs

c(x,x')=(x-x')^{\mathsf T}A(x)(x-x'),

where $A(x)$ is positive definite. Assumption 1 asks that $c$ be lower semicontinuous and that $\rho_{\min}\|v\|^2\le v^{\mathsf T}A(x)v\le\rho_{\max}\|v\|^2$ for $P_0$ -almost every $x$ , with $\rho_{\min}>0$ . The optimal transport cost $D_c(P_0,P)$ is the least value of $E_\pi[c(X,X')]$ over couplings $\pi$ of $P_0$ and $P$ . For $\delta>0$ the worst-case objective is

\sup_{P:\,D_c(P_0,P)\le\delta}E_P\bigl[\ell(\beta^{\mathsf T}X)\bigr].\tag{6}

Assumption 2 asks that the loss $\ell:\mathbb R\to\mathbb R$ be convex, that the growth exponent $\kappa=\inf\{s\ge0:\sup_u(\ell(u)-su^2)<\infty\}$ be finite, and that $E_{P_0}\|X\|^4<\infty$ .

The dual side is built from

F(\gamma,\beta,\lambda;x)=\ell\bigl(\beta^{\mathsf T}x+\gamma\sqrt\delta\,\beta^{\mathsf T}A(x)^{-1}\beta\bigr)-\lambda\sqrt\delta\bigl(\gamma^2\beta^{\mathsf T}A(x)^{-1}\beta-1\bigr),

the robust loss $\ell_{\rm rob}(\beta,\lambda;x)=\sup_{\gamma}F$ , the dual objective $f_\delta(\beta,\lambda)=E_{P_0}[\ell_{\rm rob}(\beta,\lambda;X)]\in\mathbb R\cup\{\infty\}$ and the maximizer set $\Gamma^*(\beta,\lambda;x)=\arg\max_\gamma F(\gamma,\beta,\lambda;x)$ . By the paper's Theorem 1, (6) equals $\inf_{\lambda\ge0}f_\delta(\beta,\lambda)$ , and a minimizer $\lambda_*(\beta)$ , the dual optimizer, exists. The threshold is $\lambda_{thr}(\beta)=\kappa\sqrt\delta\,\mathrm{ess\,sup}_{P_0}\,\beta^{\mathsf T}A(X)^{-1}\beta$ ; below it $f_\delta=\infty$ .

Formalization targets

Goal: Theorem 6(c)

Let $\beta\ne0$ and $\lambda_*(\beta)>\lambda_{thr}(\beta)$ . Let $G_\pm(x)\in\Gamma^*(\beta,\lambda_*(\beta);x)$ be measurable selections with the largest and smallest square, $\bar c=E[G_+^2\beta^{\mathsf T}A(X)^{-1}\beta]$ , $\underline c=E[G_-^2\beta^{\mathsf T}A(X)^{-1}\beta]$ , and let $Z\sim\mathrm{Bernoulli}(q)$ be independent of $X$ with $q=(\bar c-1)/(\bar c-\underline c)\in[0,1]$ . Then

X^*=X+\sqrt\delta\,\bigl(ZG_-+(1-Z)G_+\bigr)A(X)^{-1}\beta,\qquad E[c(X,X^*)]=\delta,

and the law of $X^*$ attains the supremum in (6).

Milestones

Lemma 1: $\Gamma^*\ne\emptyset$ and $\ell_{\rm rob}<\infty$ when $\lambda>\kappa\sqrt\delta\,\beta^{\mathsf T}A(x)^{-1}\beta$ , and $\ell_{\rm rob}=\infty$ below that; hence $\{\lambda>\lambda_{thr}\}\subseteq\{f_\delta<\infty\}\subseteq\{\lambda\ge\lambda_{thr}\}$ .
Lemma 3(a): $\sqrt\delta|g|\beta^{\mathsf T}A(x)^{-1}\beta\le1+C_1\varepsilon^{-1}(1+|\beta^{\mathsf T}x|)$ for $g\in\Gamma^*$ once $\lambda\ge(\kappa+\varepsilon)\sqrt\delta\beta^{\mathsf T}A(x)^{-1}\beta$ .
Proposition 2 (a) and its $\lambda$ -part: the one-sided $\lambda$ -derivatives of $\ell_{\rm rob}$ are the minimum and the maximum of $-\sqrt\delta(\gamma^2\beta^{\mathsf T}A(x)^{-1}\beta-1)$ over $\Gamma^*$ .
The one-sided $\lambda$ -derivatives of $f_\delta$ on $\{\lambda>\lambda_{thr}\}$ :

\partial_\pm f_\delta/\partial\lambda=\sqrt\delta\bigl(1-E[\beta^{\mathsf T}A(X)^{-1}\beta\,\inf/\sup_{g\in\Gamma^*}g^2]\bigr).

[Blanchet–Murthy 2019, Theorem 1]: strong duality and complementary slackness (already proved on the platform).

Companion statements

Theorem 6(a): $\lambda_*>0$ unless $\ell$ is constant. Theorem 6(b): $\lambda_*\ge\lambda_{thr}$ . Theorem 6(d), as the paper's example: for $\ell(u)=u^2-|u|(1-e^{-|u|})$ , $P_0=\delta_0$ , $A=I$ and $\|\beta\|=1$ , $\lambda_*=\lambda_{thr}=\sqrt\delta$ and no distribution attains the value $\delta$ . Theorem 6(e), with Lemma 8: if $\ell''\le M$ and $\lambda_*>\tfrac12M\sqrt\delta\,\mathrm{ess\,sup}\,\beta^{\mathsf T}A(X)^{-1}\beta$ , then $\Gamma^*$ is a singleton $\{G(x)\}$ almost surely and the law of $X+\sqrt\delta G(X)A(X)^{-1}\beta$ is the unique worst case.

Significance

The result reduces a search over all probability measures to a scalar problem per data point. Each point is pushed along the single direction $A(x)^{-1}\beta$ , by an amount read off the maximizers of $F$ , and the budget $\delta$ is always spent completely. When the maximizer is not unique, randomization between two extreme maximizers is needed and suffices. Part (d) shows that the threshold condition cannot be removed, and part (e) gives a deterministic transport map (a Monge solution) under smoothness. Theorem 7 of the paper, the monotone growth of worst-case displacements in $\delta$ , is a statement about the random variable $G$ produced here.

None of these statements has been machine-checked before. The general strong duality with complementary slackness of Blanchet–Murthy (arXiv:1604.01446) is proved on the platform, so this mission connects that abstract theorem to an explicit worst-case law. A formal proof also has to settle one point the printed text leaves loose: which extreme maximizers enter the mixture (see Formalization scope).

Difficulty

The first idea is to take the pointwise maximizers of $F$ at $\lambda_*$ and push $P_0$ forward. That works only when the maximizer is unique and the budget constraint happens to be tight. In general the maximizer set is not a singleton, and the derivative of $f_\delta$ at $\lambda_*$ only lies between a left and a right derivative. Turning the first-order condition $\partial_+f_\delta\ge0\ge\partial_-f_\delta$ into an exact cost $\delta$ needs three things. The one-sided derivatives must be identified as expectations over $\Gamma^*$ , an envelope theorem under an integral with a non-compact parameter set. The extreme maximizers must be compact and measurably selectable. Finally the resulting coupling must be certified optimal through complementary slackness. Each step needs a hypothesis that is easy to lose: the growth control of Lemma 3, the essential supremum in $\lambda_{thr}$ , measurability of selections.

Formalization scope

Points of $\mathbb R^d$ are EuclideanSpace ℝ (Fin d), $\beta^{\mathsf T}x$ is the inner product, and $\beta^{\mathsf T}A(x)^{-1}\beta$ is quadInv A β x. $\ell_{\rm rob}$ and $f_\delta$ are extended-real valued; $f_\delta$ uses the published extended integral ModelRiskOT.Duality.extIntegral. The worst-case objective (6) is the published primal problem primalValue: a supremum over couplings $\pi$ with first marginal $P_0$ and $\int c\,d\pi\le\delta$ (primalFeasible). A distribution attains (6) when a coupling with that second marginal has value primalValue. The random worst case $X^*$ is encoded by the joint law of $(X,X^*)$ , a mixture of two graph couplings, because $E[c(X,X^*)]$ depends on the pair. A dual optimizer is a real $\lambda_*\ge0$ minimizing $f_\delta(\beta,\cdot)$ on $[0,\infty)$ .

Standing hypotheses on every statement: $P_0$ a probability measure, Assumptions 1 and 2, $\delta>0$ , $B$ convex. The following departures from the printed text are disclosed in each item:

In (c), $G_\pm$ are the selections of extreme square used in the proof (p. 40), not $\inf\Gamma^*$ and $\sup\Gamma^*$ as printed; a two-point example shows the printed choice can fail.
In (e), "for every $x$ " is read as "for $P_0$ -almost every $x$ ", which is what the proof gives.
Lemma 8 is stated for $\beta\ne0$ .
Proposition 2 is formalized for part (a) and the $\lambda$ -derivatives only.

Every expectation used in the goal ( $\bar c$ , $\underline c$ ) carries an integrability conjunct. The cost identity and optimality are asserted for the measure itself, so no junk value of a non-integrable integral can make the goal hold vacuously. A statement asserting only first-order conditions for $\lambda_*$ would not be Theorem 6. The goal asserts primal attainment and the exact cost.

Needed infrastructure, reusable beyond this mission: envelope (Danskin) theorems for one-sided derivatives of suprema, differentiation of convex integral functionals, measurable selection of argmax sets, and complementary slackness through the published Blanchet–Murthy theorem. Contributions of any of these as standalone lemmas are welcome.

Selected references

J. Blanchet, K. Murthy, F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Math. Oper. Res. 47(2), 2022. arXiv:1810.02403v3, doi:10.1287/moor.2021.1178
J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2), 2019. arXiv:1604.01446
J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein Profile Inference and Applications to Machine Learning, J. Appl. Probab. 56(3), 2019. doi:10.1017/jpr.2019.49
P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171, 2018. doi:10.1007/s10107-017-1172-1
D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978 (Proposition 7.50, measurable selection).

15 thms2 active usersReviewed

Dynamical Systems Machine Learning Optimization·Captain: mikedeng1

Convergence and Dynamical Behavior of the ADAM Algorithm for Nonconvex Stochastic Optimization 2: The Continuous-Time Adam Trajectory Converges to the Critical Points of FResearch Paper

Motivation

Adam (Kingma and Ba, 2015) is the default optimizer for training neural networks. At step $n$ it keeps an exponential moving average $m_n$ of stochastic gradients and an exponential moving average $v_n$ of their squared coordinates, corrects both for their initialization at zero (the bias correction or debiasing step), and moves the iterate by $-\gamma\,\hat m_n/(\varepsilon + \sqrt{\hat v_n})$ coordinatewise. Despite its use, its convergence on nonconvex objectives was poorly understood when Barakat and Bianchi wrote their paper: Reddi, Kale and Kumar (2018) exhibited convex online problems on which constant-parameter Adam fails to converge, and earlier analyses either dropped the bias correction or replaced Adam by a modified algorithm.

Barakat and Bianchi (arXiv:1810.02263v4, SIAM J. Math. Data Sci. 2021) study Adam through the ODE method: as the step size $\gamma \to 0$ with $1-\alpha \sim a\gamma$ and $1-\beta \sim b\gamma$ , the interpolated iterates follow a non-autonomous ordinary differential equation, the continuous-time version of Adam. This mission formalizes their convergence theorem for that ODE (Theorem 3.2): trajectories started as Adam is started, with zero moment estimates, approach the critical points of the objective.

Setting

Let $F : \mathbb R^d \to \mathbb R$ be continuously differentiable with locally Lipschitz gradient $\nabla F$ , and let $S : \mathbb R^d \to \mathbb R^d$ be locally Lipschitz. In the paper $F(x) = \mathbb E f(x,\xi)$ is the objective and $S(x) = \mathbb E\,\nabla f(x,\xi)^{\odot 2}$ the coordinatewise second moment of the stochastic gradient; §7 only uses the two properties above. Assume $F$ is coercive ( $F(x) \to +\infty$ as $\|x\| \to \infty$ ) and $S(x) > 0$ coordinatewise for every $x$ . Fix constants $a, b, \varepsilon > 0$ with $b \le 4a$ .

The state is $z = (x, m, v) \in \mathcal Z = \mathbb R^d \times \mathbb R^d \times \mathbb R^d$ , and $\mathcal Z_+$ is the part where $v \ge 0$ . All vector operations are coordinatewise. The Adam field (3.3) is, for $t > 0$ ,

h(t, z) = \Big( -\frac{(1-e^{-at})^{-1}\, m}{\varepsilon + \sqrt{(1-e^{-bt})^{-1} v}},\ a(\nabla F(x) - m),\ b(S(x) - v) \Big),

and (ODE) is $\dot z(t) = h(t, z(t))$ . The factors $(1-e^{-at})^{-1}$ and $(1-e^{-bt})^{-1}$ are the continuous-time bias corrections; they blow up as $t \downarrow 0$ . A global solution with initial condition $(x_0, 0, 0)$ is a continuous $z : [0, +\infty) \to \mathcal Z_+$ , continuously differentiable on $(0,+\infty)$ , satisfying (ODE) for every $t > 0$ , with $z(0) = (x_0, 0, 0)$ . The critical set is $\mathcal S = \{x : \nabla F(x) = 0\}$ .

The proof passes through the autonomous field $h_\infty(z) = \lim_{t\to\infty} h(t,z) = (-m/(\varepsilon+\sqrt v),\ a(\nabla F(x)-m),\ b(S(x)-v))$ , its semiflow $\Phi$ on $\mathcal Z_+$ , and the notions of equilibrium point, strict Lyapunov function and asymptotic pseudotrajectory (APT) of a semiflow.

Formalization targets

Goal: Theorem 3.2

Assume in addition that $F(\mathcal S)$ has empty interior in $\mathbb R$ . For every global solution $z = (x, m, v)$ with initial condition $(x_0, 0, 0)$ , the set $\mathcal S$ is non-empty and

\lim_{t\to\infty} d(x(t), \mathcal S) = 0, \qquad \lim_{t\to\infty} m(t) = 0, \qquad \lim_{t\to\infty} \big(S(x(t)) - v(t)\big) = 0 .

The theorem does not claim that $x(t)$ converges; convergence to a single critical point needs a Łojasiewicz condition (Theorem 3.4, a separate mission).

Milestones

The milestones are the numbered results of §7.1–7.3 used in the proof, in the order the proof uses them: positivity of $v$ along solutions (Lemma 7.4); decrease of $V_\infty$ along $h_\infty$ (Lemma 7.5, autonomous part); compactness of trajectories (Propositions 7.6, 7.7) and lower bounds on $v$ (Lemma 7.8); well-posedness of the autonomous system and its semiflow (Proposition 7.13); the abstract limit-set theorem for APTs (Proposition 7.14, quoted from Benaïm); the strict Lyapunov function $W_\delta(x,m,v) = V_\infty(x,m,v) - \delta\langle\nabla F(x), m\rangle + \delta\|S(x)-v\|^2$ (Proposition 7.15); and the APT property of the (ODE) solution (Proposition 7.17).

Significance

Theorem 3.2 is the deterministic core of the paper's analysis of Adam. Combined with the paper's tracking result (constant-step Adam converges in probability to the ODE solution as $\gamma \to 0$ , Theorem 4.3) it says that for small steps Adam's iterates spend their time near critical points of $F$ ; it is also the input of the decreasing-step almost-sure convergence theorem (Theorem 5.2) and of the convergence-rate theorem (Theorem 3.4), which both rely on the same Lyapunov function and limit-set argument. The condition $b \le 4a$ under which the Lyapunov function decreases is satisfied by the default parameters $\alpha = 0.9$ , $\beta = 0.999$ .

The result is proved in the paper; to the best of current knowledge it has not been machine-checked. The mission produces a formal proof of the theorem, and reusable formal statements about semiflows on metric spaces: strict Lyapunov functions, and the limit set of a relatively compact asymptotic pseudotrajectory.

Difficulty

The obvious route is to show that $V(t, z(t)) = F(x) + \tfrac12\|m\|^2_{U(t,v)^{-1}}$ decreases and apply LaSalle's invariance principle. This fails on two counts. First, (ODE) is non-autonomous, and LaSalle's principle is a statement about autonomous systems: the derivative of $V$ along the flow vanishes only on a set that depends on $t$ . Second, the field is singular: $h(\cdot, z)$ blows up at $t = 0$ and $h(t, \cdot)$ is not Lipschitz near $v = 0$ , because of $\sqrt v$ , so neither existence and uniqueness nor continuous dependence on initial data come from standard theorems. The energy $V_\infty(z) = \lim_{t\to\infty} V(t,z)$ of the autonomous limit $\dot z = h_\infty(z)$ is a Lyapunov function but not a strict one: it is constant along some non-equilibrium orbits, so non-increase of an energy alone does not identify the limit points.

Formalization scope

Each block $x, m, v$ lives in EuclideanSpace ℝ (Fin d) and $\mathcal Z$ is their product; Mathlib's norm on the product is the maximum of the three Euclidean norms, which is equivalent to the Euclidean norm of $\mathbb R^{3d}$ and changes no statement. $F$ and $S$ are abstract, with the hypotheses of the paper's §7 (Assumptions 7.1, 7.2, 2.3, 2.4); this generality implies the printed theorem for the $F$ , $S$ of (2.2). Solutions are maps $\mathbb R \to \mathcal Z$ constrained only on $[0, +\infty)$ (or $[0, T)$ ), and the equation is required at $t > 0$ only. The field is extended off $\mathcal Z_+$ by $v \mapsto |v|$ , as on p. 12 of the paper. A semiflow is Mathlib's Flow ℝ≥0 M, on the subtype $\mathcal Z_+$ or on a compact subset of it. The semiflow $\Phi$ in the milestones is always assumed to be the flow of $(\mathrm{ODE}_\infty)$ , never an arbitrary flow. The APT and limit-set definitions are the published StochApproxDyn.LimitSet ones.

The goal is stated for every global solution of the specific field (3.3), and keeps " $\mathcal S$ is non-empty" in the conclusion. A statement about some solution of an unspecified field, or with " $F(\mathcal S)$ has empty interior" strengthened to " $\mathcal S$ is finite", is a different theorem and does not count.

A complete development needs: Grönwall-type comparison and chain-rule arguments along $C^1$ trajectories; well-posedness of the autonomous system on $\mathcal Z_+$ and continuity of its flow; and the limit-set theory of asymptotic pseudotrajectories (Benaïm 1999), adapted to strict Lyapunov functions in the paper's sense. The last part is independent of Adam and reusable in stochastic approximation. Contributions to any milestone are welcome; Propositions 7.13 and 7.14 are the largest pieces of infrastructure.

Selected references

A. Barakat, P. Bianchi, Convergence and Dynamical Behavior of the ADAM Algorithm for Nonconvex Stochastic Optimization, SIAM J. Math. Data Sci. 3(1), 2021; arXiv:1810.02263v4. https://arxiv.org/abs/1810.02263v4
D. P. Kingma, J. Ba, Adam: A Method for Stochastic Optimization, ICLR 2015. https://arxiv.org/abs/1412.6980
S. J. Reddi, S. Kale, S. Kumar, On the Convergence of Adam and Beyond, ICLR 2018. https://arxiv.org/abs/1904.09237
M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999. https://doi.org/10.1007/BFb0096509

14 thms2 active usersReviewed

Convex Optimization Operations Research Optimal Transport+1·Captain: mikedeng1

Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes 3: The Dual Objective Is √δκ₁-Strongly Convex in (β, λ) Near the Dual OptimizersResearch Paper

Motivation

A decision based on observed data can change when the data law differs from the one used to choose it. Distributionally robust optimization addresses this by evaluating each decision against a family of nearby probability laws. Optimal transport gives one way to define “nearby”: a candidate law is admissible when probability mass can be moved from the baseline law at a bounded expected cost. For a linear decision rule, the resulting worst-case expectation is usually harder to optimize than an ordinary sample-average loss. Blanchet, Murthy, and Zhang identify a dual objective whose variables are the decision vector and a scalar transport multiplier, then study its curvature near the multipliers that actually minimize it (Blanchet–Murthy–Zhang, 2022).

The paper proves that this dual objective is jointly strongly convex on a specified region for sufficiently small transport radius. This matters because ordinary convexity allows flat directions in the joint decision–multiplier space. The joint lower Hessian bound gives local curvature in every direction with one positive modulus that remains independent of the radius apart from the paper's explicit factor $\sqrt{\delta}$ (Theorem 4, p. 11).

Setting

Let $X\in\mathbb R^d$ have a baseline probability law $P_0$ , and let a decision be a vector $\beta$ in a nonempty compact convex set $B\subseteq\mathbb R^d$ . The loss of a possible outcome $x$ is $\ell(\beta^{\mathsf T}x)$ for a convex function $\ell:\mathbb R\to\mathbb R$ . A state-dependent positive-definite matrix $A(x)$ sets the cost of moving mass from $x$ to $x'$ :

c(x,x')=(x-x')^{\mathsf T}A(x)(x-x').

Assumption 1 requires this cost to be lower semicontinuous and the eigenvalues of $A(x)$ to lie between positive constants $\rho_{\min}$ and $\rho_{\max}$ for $P_0$ -almost every $x$ . Assumption 2 requires at most quadratic growth of $\ell$ and a finite fourth moment of $P_0$ . The ambiguity radius $\delta$ is positive (Assumptions 1–2, pp. 9–10).

The paper's dual objective is an expectation under the known law $P_0$ . Write $q_A(\beta,x)=\beta^{\mathsf T}A(x)^{-1}\beta$ . For a scalar $\lambda\ge0$ and an auxiliary scalar $\gamma$ , set

F(\gamma,\beta,\lambda;x) =\ell\bigl(\beta^{\mathsf T}x+\gamma\sqrt\delta\,q_A(\beta,x)\bigr) -\lambda\sqrt\delta\bigl(\gamma^2q_A(\beta,x)-1\bigr), \qquad f_\delta(\beta,\lambda)=\mathbb E_{P_0}\!\left[\sup_{\gamma\in\mathbb R}F(\gamma,\beta,\lambda;X)\right].

This value may be $+\infty$ . Under the paper's duality conditions, minimizing $f_\delta(\beta,\lambda)$ over $\lambda\ge0$ gives the worst-case loss at $\beta$ (Theorem 1 and (7), p. 10).

Formalization targets

Assumption 3 bounds $\ell''$ above by $M>0$ and excludes an almost surely zero $\ell'(\beta^{\mathsf T}X)$ for each $\beta\in B$ . Assumption 4 makes $B$ compact. Lemma 6 supplies positive constants $\underline L,\overline L$ bounding $\mathbb E_{P_0}[\ell'(\beta^{\mathsf T}X)^2]$ uniformly over $B$ . With $R_\beta=\sup_{\beta\in B}\|\beta\|$ , the constants $K_1,K_2$ are those of (28), and

\mathbb V_\delta=\{(\beta,\lambda):\beta\in B,\ \lambda\ge0,\ K_1\|\beta\|\le\lambda\le K_2\|\beta\|\}.

Theorem 3 first gives a bounded Hessian on $\mathbb V_\delta$ and a positive lower bound on its $\beta$ block when $0<\delta<\delta_0$ , with the explicit $\delta_0$ from p. 36. The goal, Theorem 4, adds Assumption 5: $\ell$ is locally strongly convex and, at each $\beta\in B$ , the loss derivative and the linear score are simultaneously separated from zero with positive probability. It asserts the joint bound

\exists\,\delta_1\in(0,\delta_0),\ \kappa_1>0\quad \forall\,\delta\in(0,\delta_1),\ \forall\,\theta\in\mathbb V_\delta:\quad \nabla^2 f_\delta(\theta)\succeq\sqrt\delta\,\kappa_1 I_{d+1}.

The order of the quantifiers is part of the target: $\kappa_1$ works for every sufficiently small $\delta$ (Theorems 3–4, p. 11).

Significance

The Hessian bound makes the joint dual parameters locally identifiable by curvature on a region that contains every dual optimizer. In the paper, this structure also underlies the analysis of algorithms and of how the optimizer changes with the transport radius (Proposition 1, p. 11; §3 and §5.4). Theorem 4 is already proved in the paper; this mission asks for its machine-checked formalization, together with the stated bounds on multipliers, the maximizing scalar, and the intermediate curvature results. The general optimal-transport integral used here already has a published Prove2Me definition from Blanchet and Murthy's earlier model-risk work. The new definitions specify this paper's Mahalanobis model, regions, and smoothness assumptions.

Difficulty

Convexity alone gives only a nonnegative Hessian; it cannot produce a strictly positive joint lower bound. Even curvature of $\ell$ does not by itself control directions that combine a change in $\beta$ with a change in $\lambda$ . The inner supremum over $\gamma$ can become infinite outside its effective domain, while at $\beta=0$ its maximizer ceases to be unique. The theorem therefore needs a region where the dual objective is finite and differentiable and a probabilistic condition that prevents the relevant score and derivative from vanishing together. The target keeps the actual $\sqrt\delta$ scale instead of settling for a radius-dependent positive constant (§2.2.2 and Remark 4, pp. 10–12, 39).

Formalization scope

Lean uses EuclideanSpace ℝ (Fin d) for $\mathbb R^d$ , a Borel probability measure for $P_0$ , and EReal for $f_\delta$ and the inner supremum. The reused extended-real integral records the $+\infty$ and $-\infty$ cases; the Hessian is taken only where $f_\delta$ is finite on a neighborhood and its real representative is differentiable there. Quadratic Hessian forms use $\|v_\beta\|^2+v_\lambda^2$ , since Lean's product norm is not the paper's Euclidean norm. The compact set $B$ is explicitly nonempty, and the positive ambiguity radius $\delta$ is quantified inside the goal so that $\delta_1$ and $\kappa_1$ are uniform in $\delta$ . Theorem 3 additionally assumes $R_\beta>0$ for the proof's explicit formula for $\delta_0$ : nonempty compact $B=\{0\}$ would make that formula zero. Assumption 5 already gives $R_\beta>0$ in the goal.

The goal retains Assumption 5's per-decision quantifiers. That assumption itself excludes $0\in B$ : its strict score event is empty at $\beta=0$ . Intermediate statements where the printed wording includes $\beta=0$ but the claim fails there state $\beta\ne0$ explicitly. Lemma 5 also states the differentiability and positive-multiplier conditions needed for its derivative and division. Proposition 9(b)'s printed strict curvature-margin inequality is corrected to the nonstrict inequality derived in its proof; its original wording is preserved in the milestone quotation. The claims are about the expectation $f_\delta$ , with $\kappa_1$ independent of $\delta$ , rather than a pointwise or merely convex substitute.

A complete development needs measurable extended-real integration, the matrix quadratic form and its inverse, almost-everywhere spectral bounds, differentiability under an expectation, and Hessian estimates for an optimized scalar. The transport integral, the assumptions and constants, and the multiplier bounds are intended as reusable interfaces for the companion missions. Contributions that close the listed lemmas or add the paper's omitted second-order kernel formula are within scope.

Selected references

José Blanchet, Karthyek Murthy, and Fan Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Mathematics of Operations Research 47(2), 2022. arXiv:1810.02403v3; DOI:10.1287/moor.2021.1178.
José Blanchet and Karthyek Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research 44(2), 2019. arXiv:1604.01446v2.

17 thms2 active usersReviewed

Completed

Complexity Theory Linear Optimization Operations Research+2·Captain: mikedeng1

A Comment on "Computational Complexity of Stochastic Programming Problems" 3: An ε-Optimal Decision of the Random-Recourse Program (11) Decides the Integer Feasibility ProblemResearch Paper

Motivation

A linear two-stage stochastic program chooses a first-stage decision $x$ before an uncertain parameter $\tilde\xi$ is revealed, and pays the optimal value $Q(x,\xi)$ of a second-stage linear program once the realization $\xi$ is known. Such programs are the basic model of planning under uncertainty in operations research, and their computational complexity determines which solution methods can be expected to work. In 2006, Dyer and Stougie argued that linear two-stage stochastic programs with fixed recourse are #P-hard even when the random data follow independent uniform distributions. Hanasusanto, Kuhn and Wiesemann showed that this proof is not correct and gave a corrected one, which also covers approximate evaluation to sufficiently high accuracy; their note also shows that, when the second-stage constraint matrix itself depends on $\xi$ (random recourse), even finding an approximately optimal decision is strongly NP-hard.

This mission formalizes that last result, Theorem 4 of the note. The previous missions of the series treat the hardness of evaluating the expected recourse with fixed and with random recourse.

Setting

The Integer Feasibility Problem. An instance is an integer matrix $A\in\mathbb Z^{m\times n}$ and an integer vector $b\in\mathbb Z^m$ such that the polytope $\{y\in\mathbb R^n:Ay\le b\}$ lies in the unit cube $[0,1]^n$ . The question is whether some binary vector $y\in\{0,1\}^n$ satisfies $Ay\le b$ . This problem is strongly NP-hard (Garey and Johnson).

The second-stage problem. For a decision $x\in\mathbb R$ and a realization $\xi\in[0,1]^n$ , write $e$ for the all-ones vector and consider

\begin{aligned} Q(x,\xi)=\ \text{minimize}\ \ & e^\top y\\ \text{subject to}\ \ & y\in\mathbb R^n_+,\ \lambda\in\mathbb R^m_+,\ x\ge e^\top y,\\ & y_i\ge \xi_i+(b-A\xi)^\top\lambda,\quad y_i\ge(1-\xi_i)+(b-A\xi)^\top\lambda\qquad(i=1,\dots,n). \end{aligned}

The coefficient of $\lambda$ in each constraint depends on $\xi$ , which is what makes the recourse random.

Problem (11). With $\tilde\xi$ uniformly distributed on $[0,1]^n$ ,

\text{minimize}\ \ x+\mathbb E\big[Q(x,\tilde\xi)\big]\quad\text{subject to}\ \ x\in\mathbb R .

The second stage is not feasible for every $x$ (the problem lacks relatively complete recourse), so a decision $x$ is feasible only if the second stage is feasible for every $\xi\in[0,1]^n$ . Let $f^\star$ be the infimum of the objective over feasible decisions. A feasible $x$ is $\epsilon$ -optimal if

\frac{\big|f^\star-\big(x+\mathbb E[Q(x,\tilde\xi)]\big)\big|}{\max\{|f^\star|,1\}}\le\epsilon .

The constant $\epsilon'$ . Lemma 4 fixes $\epsilon'$ with $0\le\epsilon'<\tfrac12$ and $\epsilon'\sum_j|A_{ij}|<1$ for every row $i$ .

Formalization targets

Goal: Theorem 4 as a reduction

For an instance with nonempty polytope, $n\ge1$ , $\epsilon'$ as above, $0\le\epsilon<\epsilon'/(4n)$ , and any $\epsilon$ -optimal decision $x$ of (11),

\exists\,y\in\{0,1\}^n:\ Ay\le b\iff x>n-\frac{\epsilon'}{2}.

This is the mathematical content of "determining an $\epsilon$ -optimal decision is strongly NP-hard whenever $\epsilon<\epsilon'/4n$ ": a single comparison of any approximate decision with a threshold answers the NP-hard question.

Milestones

Lemma 4. $Ay\le b$ has a binary solution iff it has a solution in $([0,\epsilon']\cup[1-\epsilon',1])^n$ .
The second stage. If $A\xi\le b$ , the second stage is feasible iff $\sum_i\max\{\xi_i,1-\xi_i\}\le x$ , with value $\sum_i\max\{\xi_i,1-\xi_i\}$ ; otherwise it is feasible iff $x\ge0$ , with value $0$ . Optimal $y$ is unique in both cases.
The optimal decision. $x$ is feasible iff $x\ge x^\star$ , and $x^\star$ is the unique optimal decision, where

x^\star=\max\Big\{\sum_{i=1}^n\max\{\xi_i,1-\xi_i\}:A\xi\le b\Big\}.

The dichotomy. The answer is affirmative iff $x^\star=n$ , and negative iff $x^\star<n-\epsilon'$ .
Accuracy of the decision. Every $\epsilon$ -optimal $x$ satisfies $|x^\star-x|\le2n\epsilon$ .

Significance

The result. Theorem 4 implies that, unless the problems in NP admit an efficient solution scheme, there is no fully polynomial-time approximation scheme for two-stage stochastic programs with random recourse, even with a one-dimensional first stage and a uniform distribution. Together with the #P-hardness results of the same note, it delimits what algorithms such as sample average approximation can guarantee once relatively complete recourse and fixed recourse are dropped.

Formalizing it. The theorem has a short published proof, but that proof leaves several conventions implicit: the index set of the constraint block, the meaning of first-stage feasibility, and the condition on $\epsilon'$ when $A$ has a zero row. A machine-checked version fixes each of them and verifies that the claimed formula for $x^\star$ is correct under the chosen reading. To our knowledge none of these statements has been formalized before. The objects are elementary (finite-dimensional linear programs, a set integral on the unit cube), and the second-stage solution and rounding lemma are reusable for related reductions from integer feasibility.

Difficulty

The individual steps are short; the difficulty is bookkeeping across three layers. The second stage is an optimisation over $(y,\lambda)$ whose feasibility depends on the sign pattern of $b-A\xi$ ; the first stage requires a supremum over a polytope to be attained (compactness), and the expected recourse to be the same integral for all feasible decisions (integrability of a piecewise-defined value function over the cube). The tempting shortcut, reading off feasibility from the value of $Q$ , fails: an infeasible linear program has no meaningful value, and treating it as cost $0$ would make every decision look optimal. Similarly, an almost-sure notion of feasibility looks natural for a stochastic program but invalidates the formula for $x^\star$ whenever the polytope has measure zero, as it typically does for integer feasibility instances written with equalities.

Formalization scope

All objects live in SPHardness.IntFeas. Vectors are functions on Fin n and Fin m; $A$ and $b$ are integer and are cast to $\mathbb R$ , and integrality is kept because Lemma 4 depends on it. The uniform law on $[0,1]^n$ is Lebesgue measure restricted to the cube (volume $1$ ); expectations are set integrals. The recourse value, $f^\star$ and $x^\star$ are sInf/sSup in $\mathbb R$ , and second-stage feasibility, first-stage feasibility and $\epsilon$ -optimality are separate predicates, so no statement depends on the junk value of an empty infimum.

Pinned readings and added conventions:

The page writes the constraint block as " $\forall i=1,\dots,m$ " and $x^\star$ with $\sum_{i=1}^m$ , adding " $n=m=k$ ". Here the block ranges over $i=1,\dots,n$ , $\xi\in[0,1]^n$ , and $m$ (the number of rows of $A$ ) is arbitrary.
First-stage feasibility is robust: feasible for every $\xi\in[0,1]^n$ , not almost every $\xi$ .
$\epsilon'<\min_i\{(\sum_j|A_{ij}|)^{-1}\}$ is encoded as $\epsilon'\sum_j|A_{ij}|<1$ for every row, together with $0\le\epsilon'<\tfrac12$ .
Added hypotheses, all disclosed in the statements: the polytope $\{A\xi\le b\}$ is nonempty (the proof's own assumption), $n\ge1$ , and $\epsilon\ge0$ .

Strong NP-hardness, the FPTAS consequence, running times and encoding lengths are not formalized; the goal is the correctness of the reduction. A statement in which $x$ ranges over arbitrary reals satisfying a hypothesised identity, rather than over $\epsilon$ -optimal decisions of the program (11) built from $(A,b)$ , would be trivial and is ruled out: every object in the goal is defined from the instance.

Contributions welcome: proofs of the milestones, in particular measurability and integrability of the recourse function on the cube and attainment of $x^\star$ , which are reusable for other piecewise-linear recourse functions.

Selected references

G. A. Hanasusanto, D. Kuhn, W. Wiesemann, A comment on "computational complexity of stochastic programming problems", Mathematical Programming (2016); preprint Optimization Online 2015/03/4825 (version of October 6, 2015). https://optimization-online.org/wp-content/uploads/2015/03/4825.pdf, DOI https://doi.org/10.1007/s10107-015-0958-2
M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Mathematical Programming 106 (2006) 423–432. https://doi.org/10.1007/s10107-005-0597-0
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
J. R. Birge, F. Louveaux, Introduction to Stochastic Programming, Springer, 1997 (2nd ed. 2011, https://doi.org/10.1007/978-1-4614-0237-4).

8 thms2 active usersReviewed

Numerical Analysis Operations Research Optimization·Captain: mikedeng1

The Proximal Alternating Direction Method of Multipliers in the Nonconvex Setting: Convergence Analysis and Rates 2: Finite, Linear or Sublinear Rates for the Iterates Under the Łojasiewicz PropertyResearch Paper

Motivation

The alternating direction method of multipliers (ADMM) is one of the standard splitting methods for problems of the form $\min_x\{g(Ax) + h(x)\}$ , in which a nonsmooth term acts on a linear image of the variable. It is used in signal and image processing, statistical learning and matrix completion, and in many of these applications $g$ or $h$ is nonconvex: sparsity penalties such as $\ell_0$ or $\ell_p$ with $p<1$ , rank constraints, or indicator functions of nonconvex sets. For convex problems the convergence theory of ADMM is classical; for nonconvex problems the questions of whether, and how fast, the iterates converge were open until the last decade.

R. I. Boţ and D.-K. Nguyen (arXiv:1801.01994v2, Math. Oper. Res. 45(2), 2020, DOI) analyse a proximal ADMM with variable metrics and its linearized variant in the nonconvex setting. Their first main result (Theorem 14, the subject of the companion mission of this series) shows that bounded iterates converge to a KKT point when a regularization of the augmented Lagrangian has the Kurdyka–Łojasiewicz property. This mission formalizes their second main result, Theorem 20: when that function has the Łojasiewicz property with exponent $\theta$ , the iterates converge in finitely many steps, linearly, or sublinearly, according to the value of $\theta$ .

Timeline. Łojasiewicz (1963) proved his gradient inequality for real-analytic functions; Attouch and Bolte (Math. Program. 2009) derived from its nonsmooth version the rates $\theta=0$ / $\theta\in(0,\frac12]$ / $\theta\in(\frac12,1)$ for the proximal point algorithm; Bolte, Sabach and Teboulle (Math. Program. 2014) gave a general KL-based convergence scheme (PALM); Li and Pong (SIAM J. Optim. 2015) proved convergence of a proximal ADMM under KL assumptions; Boţ and Nguyen (2018/2020) treated variable metrics, relaxation parameters $\rho\in(0,2)$ , and the linearized variant, with explicit rates.

Setting

Let $g:\mathbb R^m\to\mathbb R\cup\{+\infty\}$ be proper and lower semicontinuous, $h:\mathbb R^n\to\mathbb R$ differentiable with $L$ -Lipschitz gradient, and $A:\mathbb R^n\to\mathbb R^m$ linear. The augmented Lagrangian with parameter $r>0$ is

L_r(x,z,y) = g(z) + h(x) + \langle y, Ax - z\rangle + \frac r2\|Ax-z\|^2 .

Given positive semidefinite matrices $M_1^k$ , $M_2^k$ and $\rho\in(0,2)$ , Algorithm 1 produces $(x^k,z^k,y^k)_{k\ge0}$ from any starting point by: $z^{k+1}$ minimizes $L_r(x^k,z,y^k) + \frac12\|z-z^k\|^2_{M_2^k}$ ; $x^{k+1}$ minimizes $L_r(x,z^{k+1},y^k) + \frac12\|x-x^k\|^2_{M_1^k}$ ; and $y^{k+1} = y^k + \rho r(Ax^{k+1} - z^{k+1})$ . Algorithm 2 replaces $h(x)$ in the $x$ -step by $\langle x - x^k,\nabla h(x^k)\rangle$ .

Assumption 2 requires $g$ and $h$ to be bounded below, $A$ to be surjective with $\lambda\|y\|^2\le\|A^*y\|^2$ ( $\lambda>0$ ), $\|M_1^k\|\le\mu_1$ , $\|M_2^k\|\le\mu_2$ , $r\ge4T_0L>0$ , and $2M_1^k + rA^*A\succeq(L + C'_{\mathbf M}/r)\,\mathrm{Id}$ for all $k$ , where $T_0$ and $C'_{\mathbf M}$ are explicit functions of $\lambda,\rho,L,\mu_1$ .

The analysis runs on the regularized augmented Lagrangian of Section 3

\mathcal F_r(x,z,y,x',y') = L_r(x,z,y) + 2T_1\|A^*(y-y')\|^2 + C_1\|x-x'\|^2,

with explicit constants $T_1$ , $C_1$ . Along a run, $\mathcal F_k = \mathcal F_r(x^k,z^k,y^k,x^{k-1},y^{k-1})$ . If the run converges to $(\hat x,\hat z,\hat y)$ , put $\hat u = (\hat x,\hat z,\hat y,\hat x,\hat y)$ , $\mathcal F_* = \mathcal F_r(\hat u)$ and $\mathcal E_k = \mathcal F_k - \mathcal F_*$ . $\mathcal F_r$ has the Łojasiewicz property at $\hat u$ with constant $C_L>0$ and exponent $\theta\in[0,1)$ if

|\mathcal F_r(u) - \mathcal F_*|^\theta \le C_L\operatorname{dist}(0,\partial\mathcal F_r(u))

for all $u$ near $\hat u$ , where $\partial$ is the limiting subdifferential.

Formalization targets

Goal: Theorem 20 (p. 28)

Under Assumption 2, for a bounded run converging to $(\hat x,\hat z,\hat y)$ at which $\mathcal F_r$ has the Łojasiewicz property with exponent $\theta$ :

\theta = 0:\quad (x^k,z^k,y^k) = (\hat x,\hat z,\hat y)\ \text{ for all large } k;

\theta\in(0,\tfrac12]:\quad \|x^k-\hat x\|,\ \|y^k-\hat y\|,\ \|z^k-\hat z\| \le \hat C\,\hat Q^k,\quad \hat Q\in[0,1);

\theta\in(\tfrac12,1):\quad \|x^k-\hat x\|,\ \|y^k-\hat y\| \le \hat C(k-1)^{-\frac{1-\theta}{2\theta-1}},\quad \|z^k-\hat z\|\le\hat C(k-2)^{-\frac{1-\theta}{2\theta-1}}.

All constants are existential and independent of $k$ ; the goal fixes only the shape of each rate.

Milestones

Lemma 15 (p. 23): a real sequence with $e_{k-l_0} - e_k \ge C_e e_k^{2\theta}$ decreases to $0$ in finite time, linearly, or as $(k - l_0 + 1)^{-1/(2\theta-1)}$ .
Lemma 16 (p. 25): the descent inequality (80) under Assumption 2.
(83) (p. 25): $\mathcal F_{k+1} + \frac{C_1}4\|x^{k+1}-x^k\|^2 + \frac12\|z^{k+1}-z^k\|^2_{M_2^k} + \frac1{\rho r}\|y^{k+1}-y^k\|^2\le\mathcal F_k$ .
The subgradient estimate of p. 26: an explicit $D^{k+1}\in\partial\mathcal F_r$ with $|||D^{k+1}|||\le C_{14}\|x^{k+1}-x^k\| + C_{15}\|y^{k+1}-y^k\| + C_{16}\|y^k-y^{k-1}\|$ .
Lemma 17 (p. 26): $\mathcal E_{k-1} - \mathcal E_{k+1}\ge C_{19}\mathcal E_{k+1}^{2\theta}$ .
Theorem 18 (p. 27): the three rates for $\mathcal E_k$ .
Lemma 19 (p. 27): $\|x^k-\hat x\|$ , $\|y^k-\hat y\|$ , $\|z^k - \hat z\|$ bounded by $\max\{\sqrt{\mathcal E},\varphi(\mathcal E)\}$ with $\varphi(s) = \frac{C_L}{1-\theta}s^{1-\theta}$ .

Significance

Theorem 20 is the quantitative half of the paper: it converts a local growth condition on one explicit function into convergence rates for the iterates of two practical nonconvex splitting methods. Since semi-algebraic functions satisfy the Łojasiewicz property with some exponent, the theorem applies to most of the sparsity- and rank-type models for which ADMM is used, and it explains when finite termination or linear convergence is to be expected. The intermediate results (Lemma 15 in particular) are the standard route from a Łojasiewicz inequality to rates and recur in the analysis of many first-order methods.

The result is proved in the paper; to our knowledge no part of it has a machine-checked proof. The mission produces a formal statement and proof of the rates, with every constant of the paper defined explicitly, and records where the paper's constants need recomputing: the constants $C_8$ and $C_{10}$ of Lemma 9 are reused on p. 26 for a regularization whose gradient is twice as large.

Difficulty

Lemma 15 is elementary but delicate: the recurrence has a lag $l_0$ and, for $\theta>\frac12$ , a nonlinearity that a direct induction does not control, and the index bookkeeping determines the exponent. The rates for $\mathcal F_k$ require a bound on an explicit subgradient of $\mathcal F_r$ , whose limiting subdifferential involves the nonsmooth $g$ , so the calculus of limiting subgradients for a sum of a lower semicontinuous and a smooth function on a product space is needed. Transferring rates from $\mathcal F_k$ to the iterates needs a finite-length estimate with explicit constants, uniform in the tail. A tempting shortcut, applying the Łojasiewicz inequality directly to $L_r$ , fails: $L_r$ does not decrease along the iterates; only the regularized $\mathcal F_r$ does.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin n); $g$ takes values in EReal and is proper and lower semicontinuous; $L_r$ and $\mathcal F_r$ take values in EReal. Points of $\mathbb R^n\times\mathbb R^m\times\mathbb R^m\times\mathbb R^n\times\mathbb R^m$ form a nested WithLp 2 product, so the norm and the inner product are the Euclidean ones of the paper. The limiting subdifferential is the published NonconvexSplitting.Shared.LimitingSubdiff. The two algorithms are the constructors of an inductive type; a run is a relation (any minimizer may be taken), and every statement holds for both. $\lambda_{\min}(AA^*)$ and $\sup_k\|M_i^k\|$ are replaced by arbitrary valid bounds. $\mathcal F_*$ is $\mathcal F_r(\hat u)$ , which the paper shows equals $\lim_k\mathcal F_k$ .

The Łojasiewicz hypothesis requires the inequality for every subgradient, so that $\operatorname{dist}(0,\emptyset) = +\infty$ , and only at points with $\mathcal F_r(u)\ne\mathcal F_*$ , the convention $0^0 = 0$ ; with Lean's $0^0 = 1$ the hypothesis would be unsatisfiable at $\theta = 0$ , and a Łojasiewicz hypothesis that no function satisfies, an Assumption 2 that no data satisfy, or a rate whose constant depends on $k$ would each make the targets trivial. Assumption 2 together with the run predicate is satisfiable (checked on a one-dimensional instance), and all constants are quantified before $k$ .

Labelled corrections: $\mathcal F_r$ uses $C_1$ as displayed on p. 25 (not $C_1/2$ ); $C_8 = 4C_1 + C_5$ and $C_{10} = C_7 + 8T_1\|A\|^2$ are recomputed for the Section 3 $\mathcal F_r$ ; Lemma 17 asks for $k_0\ge2$ ; Lemma 19 assumes $C_1>0$ , since for $C_1 = 0$ the paper's $C_{20}$ is $+\infty$ .

Needed infrastructure: calculus of the limiting subdifferential for the sum of a lower semicontinuous function and a $C^1$ function on a product space, the descent lemma, and real-power estimates for sequences. Lemma 15 is independent of ADMM and reusable. Proofs of individual milestones are welcome in any order.

Selected references

R. I. Boţ, D.-K. Nguyen, The proximal alternating direction method of multipliers in the nonconvex setting: convergence analysis and rates, Math. Oper. Res. 45(2), 2020. https://arxiv.org/abs/1801.01994 (v2), https://doi.org/10.1287/moor.2019.1008
H. Attouch, J. Bolte, On the convergence of the proximal algorithm for nonsmooth functions involving analytic features, Math. Program. 116, 2009. https://doi.org/10.1007/s10107-007-0133-5
J. Bolte, S. Sabach, M. Teboulle, Proximal alternating linearized minimization for nonconvex and nonsmooth problems, Math. Program. 146, 2014. https://doi.org/10.1007/s10107-013-0701-9
G. Li, T. K. Pong, Global convergence of splitting methods for nonconvex composite optimization, SIAM J. Optim. 25(4), 2015. https://doi.org/10.1137/140998135

14 thms2 active usersReviewed

Completed

Convex Optimization Numerical Analysis Optimization·Captain: mikedeng1

From Error Bounds to the Complexity of First-Order Descent Methods for Convex Functions 3: ISTA for ℓ1-Regularized Least Squares Satisfies f(x_k) − min f ≤ (f(x_0) − min f)/q^k with q = 1 + 2aγ_R/b²Research Paper

Motivation

The ℓ1-regularized least squares problem (the Lasso, or basis pursuit denoising) is the model problem of compressed sensing and sparse inverse problems: given a matrix $A\in\mathbb R^{m\times n}$ , data $d\in\mathbb R^m$ and a weight $\mu>0$ , one seeks a vector $x$ that fits $Ax\approx d$ while having few nonzero entries. The standard first-order method for it is the iterative shrinkage thresholding algorithm (ISTA), a forward-backward splitting scheme whose backward step is componentwise soft thresholding. Each iteration costs two matrix–vector products, which is why ISTA and its variants are used on problems far too large for interior-point methods.

The classical complexity guarantee for ISTA is $f(x_k)-\min f=O(1/k)$ , the rate of the proximal gradient method on any convex composite problem (Beck–Teboulle 2009). ISTA itself goes back to Daubechies–Defrise–De Mol 2004, and its link with forward-backward splitting to Combettes–Wajs 2005. An asymptotic linear rate was known, with an explanation through partial smoothness (Liang–Fadili–Peyré), but there was no global, explicit, non-asymptotic bound. Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234v3, Math. Program. 2017) derive such a bound from two ingredients: an error bound for the Lasso objective on $\ell_1$ balls, with a constant written through a Hoffman constant, and their general theory turning a Kurdyka–Łojasiewicz (KL) inequality into complexity bounds for descent methods.

Setting

Write $\mathbb R^n$ with the Euclidean norm $\|\cdot\|$ , and $\|x\|_1=\sum_i|x_i|$ . For a matrix $M$ , $\|M\|$ is its spectral norm, the operator norm from $\mathbb R^n$ to $\mathbb R^m$ with Euclidean norms. The objective is

f(x)=\mu\|x\|_1+\tfrac12\|Ax-d\|^2,\qquad \mu>0,

with $\min f=\inf_x f(x)$ and $S=\operatorname{argmin} f$ . Put $g=\mu\|\cdot\|_1$ and $h=\tfrac12\|A\cdot-d\|^2$ . Then $h$ is convex with gradient $A^T(Ax-d)$ , Lipschitz with constant $L=\|A^TA\|$ .

Given stepsizes $0<\lambda^-\le\lambda_k\le\lambda^+$ with $\lambda^+L<2$ and any $x_0$ , ISTA is

x_{k+1}=\operatorname{prox}_{\lambda_k\mu\|\cdot\|_1}\big(x_k-\lambda_k(A^TAx_k-A^Td)\big),\qquad k\ge0,

where $\operatorname{prox}_\varphi(v)$ is the minimizer of $\varphi(y)+\tfrac12\|y-v\|^2$ . More generally, in a real Hilbert space $H$ with $g$ proper, lower semicontinuous and convex and $h$ convex with $L$ -Lipschitz gradient, the forward-backward method takes $x_{k+1}$ to be a minimizer of $g(z)+\langle\nabla h(x_k),z-x_k\rangle+\frac1{2\lambda_k}\|z-x_k\|^2$ .

A sequence is a subgradient descent sequence for a convex $f$ with constants $a,b>0$ if $x_0\in\operatorname{dom} f$ and, for every $k\ge1$ ,

(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)$ has $\|\omega_k\|\le b\|x_k-x_{k-1}\|$ .

With $\min f=0$ , $f$ has the KL property on a set $X\cap[0<f<\bar r]$ with desingularizing function $\varphi$ if $\varphi'(f(x))\|v\|\ge1$ for every such $x$ and every $v\in\partial f(x)$ .

A number $\nu\ge0$ is a Hoffman constant for a pair of matrices $(A',E)$ if, for every right-hand side with $X=\{A'x\le a'\}$ and $Y=\{Ex=e\}$ intersecting, $\operatorname{dist}(x,X\cap Y)\le\nu\|Ex-e\|$ for all $x\in X$ .

Formalization targets

Goal: Theorem 25

Put $a=\frac1{\lambda^+}-\frac L2$ and $b=\frac1{\lambda^-}+L$ , and $R=\max\big(\frac{f(x_0)}\mu,1+\frac{\|d\|^2}{2\mu}\big)$ . Let $\gamma_R>0$ be such that $f(x)-\min f\ge2\gamma_R\operatorname{dist}^2(x,S)$ whenever $\|x\|_1\le R$ . Then ISTA converges to some $x^*\in S$ and

f(x_k)-\min f\le\frac{f(x_0)-\min f}{q^k}\quad(k\ge0),\qquad \|x_k-x^*\|\le C\,\frac{\sqrt{f(x_0)-\min f}}{q^{(k-1)/2}}\quad(k\ge1),

q=1+\frac{2a\gamma_R}{b^2},\qquad C=\frac1{\sqrt a}\Bigg(1+\frac1{ab^{-2}\gamma_R\sqrt{1+\frac1{2ab^{-2}\gamma_R}}}\Bigg).

Milestones

Lemma 10, (9)–(10): for $R>\|d\|^2/(2\mu)$ the error bound holds with $\gamma_R=1/\big(4\nu^2(1+\mu R+(R\|A\|+\|d\|)(4R\|A\|+\|d\|))\big)$ . Here $\nu$ is a Hoffman constant of an explicit pair of matrices built from $A$ and $\mu$ .
Lemma 10, KL consequence: under the error bound, $f-\min f$ has the KL property on the $\ell_1$ ball with $\varphi(s)=\sqrt{2s/\gamma_R}$ .
Proposition 13: the forward-backward method satisfies (H1) and (H2) with the constants $a,b$ above.
§5.3: every ISTA iterate satisfies $\|x_k\|_1\le R$ .
Corollary 20 in the stable-set form of Corollary 19: a subgradient descent sequence that stays in a set $X$ , on which the KL inequality holds with $\psi(s)=\frac\ell2s^2$ , satisfies $f(x_k)\le f(x_0)/(1+2a\sigma)^k$ and the companion bound on $\|x_k-x^*\|$ , $\sigma=\ell b^{-2}$ .

Significance

The result. The theorem replaces the sublinear $O(1/k)$ guarantee of ISTA by a global linear rate with explicit constants depending only on $\mu$ , $A$ , $d$ , the stepsizes, $x_0$ and a Hoffman constant. It also bounds the distance of the iterates to the limit, not only the objective gap, and needs no uniqueness of the minimizer. Through $\gamma_R$ , it shows that conditioning of the objective near its minimizers, rather than strong convexity, governs the complexity of the method. The general machinery behind it (Theorem 16 of the paper, a separate mission of this series) applies to any method producing subgradient descent sequences.

Formalizing it. The result is proved on paper, and no machine-checked proof of it or of its ingredients is known. A formalization would give a verified linear-rate certificate for a widely deployed algorithm. It would also yield reusable lemmas: the descent and relative-error properties of the forward-backward method in a Hilbert space, and quadratic growth for the Lasso on $\ell_1$ balls. Lemma 10 rests on an external result (Beck–Shtern, Lemma 2.5) that a complete development must also formalize.

Difficulty

The Lasso objective is not strongly convex when $A$ has a nontrivial kernel, and its minimizer need not be unique. The textbook argument for linear convergence of proximal gradient methods, which uses strong convexity, therefore does not apply. Quadratic growth $f-\min f\ge2\gamma\operatorname{dist}^2(\cdot,S)$ is the substitute, but it holds only on bounded sets, with a constant degrading in the radius. The analysis must therefore show that the iterates stay in a fixed $\ell_1$ ball and keep track of how the growth constant enters the rate. Deriving the explicit $\gamma_R$ requires recasting the problem as a quadratic program over a polyhedron with $2^n+1$ facets and invoking a Hoffman-type error bound for it.

Formalization scope

Citations refer to the arXiv preprint arXiv:1510.08234v3 (20 July 2016), with its numbering and pages; the journal version is not used. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and matrices act through Matrix.toEuclideanLin. Spectral norms are operator norms of the associated continuous linear maps, never Mathlib's default entrywise matrix norm. The data vector, called $b$ in §3.2.1 of the paper and $d$ in §5.3, is $d$ throughout; $b$ is the constant of (H2).

Functions with values in $(-\infty,+\infty]$ are EReal-valued. The convex subdifferential, Γ₀, $\|\cdot\|_1$ , the prox predicate and the class $\mathcal K(0,\bar r)$ of desingularizing functions are reused from published platform definitions. The stepsize condition $\lambda^+<2/L$ is written $\lambda^+L<2$ , so that $A=0$ (where $L=0$ ) is covered. $\min f$ is the infimum of $f$ , and $q^{(k-1)/2}$ is a real power.

In the goal, $\gamma_R$ is any positive constant satisfying the error bound on the ball of radius $R$ ; it is not fixed to the value (10) and not existentially quantified. The constants $a,b,q,C,R$ are fixed formulas, never existentials. A statement with an unspecified constant, with $\gamma_R$ chosen after the sequence, or with the stepsize hypothesis written as $\lambda^+<2/L$ (unsatisfiable or vacuous at $L=0$ ) would trivialize the goal and is ruled out.

The subgradient-descent and KL notions duplicate, in the sub-namespace ErrBoundCplx.ISTA, those of the series' first mission, because draft items cannot import each other. Proofs of any milestone are welcome, in particular Proposition 13 and the KL consequence of Lemma 10, which are self-contained. A formalization of Hoffman's error bound and of Beck–Shtern's Lemma 2.5 is the main infrastructure Lemma 10 needs.

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. https://arxiv.org/abs/1510.08234v3
A. Beck, S. Shtern, Linearly convergent away-step conditional gradient for non-strongly convex functions, preprint (cited as [10], Lemma 2.5). https://arxiv.org/abs/1504.05002
A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sci. 2 (2009) 183–202. https://doi.org/10.1137/080716542
A. J. Hoffman, On approximate solutions of systems of linear inequalities, J. Res. Natl. Bur. Stand. 49 (1952) 263–265. https://doi.org/10.6028/jres.049.027
I. Daubechies, M. Defrise, C. De Mol, An iterative thresholding algorithm for linear inverse problems with a sparsity constraint, Comm. Pure Appl. Math. 57 (2004) 1413–1457. https://doi.org/10.1002/cpa.20042
J. Liang, J. Fadili, G. Peyré, Local linear convergence of forward-backward under partial smoothness, preprint. https://arxiv.org/abs/1407.5611
P. L. Combettes, V. R. Wajs, Signal recovery by proximal forward-backward splitting, Multiscale Model. Simul. 4 (2005) 1168–1200. https://doi.org/10.1137/050626090
H. Attouch, J. Bolte, B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137 (2013) 91–129. https://doi.org/10.1007/s10107-011-0484-9

14 thms2 active usersReviewed

Algebra Combinatorics Discrete Geometry+1·Captain: mikedeng1

Maximum Scattered Linear Sets and Complete Caps in Galois Spaces 1: Scattered 𝔽_q-Linear Sets of Rank rt/2 Exist in PG(r − 1, q^t) for t Even, in Three Families of (q, t)Research Paper

Motivation

Linear sets are the main tool for building point sets with few intersection sizes in finite projective spaces: sets meeting every hyperplane, two-intersection sets, translation ovoids, and the geometric side of finite semifields and rank-metric codes (Polverino, 2010). Among them, scattered linear sets are those whose points all carry the smallest possible weight, and a scattered linear set of the largest possible rank is called maximum scattered. By Blokhuis and Lavrauw (2000), a maximum scattered linear set of $\mathrm{PG}(r-1,q^t)$ of rank $rt/2$ is a two-intersection set with respect to hyperplanes, so each one yields a two-weight code and a strongly regular graph.

Timeline.

2000, Blokhuis–Lavrauw: the rank of a scattered $\mathbb F_q$ -linear set of $\mathrm{PG}(r-1,q^t)$ is at most $rt/2$ , and for $r$ even this bound is attained.
2000, Ball–Blokhuis–Lavrauw: examples of rank $6$ in $\mathrm{PG}(2,q^4)$ .
Classical: for $r=3$ , $t=2$ the bound $3$ is attained by Baer subplanes.
2000, Blokhuis–Lavrauw, Thm 4.4: existence (without explicit examples) for $r>3$ , $t=2$ , $q=2$ and for $r\ge3$ , $(t-1)\mid r$ , $t$ even, $q>2$ .
2015, Bartoli, Giulietti, Marino and Polverino (arXiv:1512.07467v1, Combinatorica 37 (2017)): three explicit families in $\mathrm{PG}(2,q^{2n})$ and, by direct sums, maximum scattered linear sets in $\mathrm{PG}(r-1,q^t)$ for $t$ even in three families of $(q,t)$ . This mission formalizes that result; the companion mission formalizes the paper's application to complete caps.

Setting

Let $q$ be a prime power, $t\ge1$ , and let $V$ be an $r$ -dimensional vector space over $\mathbb F_{q^t}$ ; $\mathrm{PG}(V,\mathbb F_{q^t})=\mathrm{PG}(r-1,q^t)$ has as points the spans $\langle v\rangle_{\mathbb F_{q^t}}$ of nonzero $v\in V$ . An $\mathbb F_q$ -subspace $U\subseteq V$ is a subset closed under addition and under multiplication by $\mathbb F_q$ . It defines the $\mathbb F_q$ -linear set

L_U=\{\langle u\rangle_{\mathbb F_{q^t}} : u\in U\setminus\{0\}\},

whose rank is $\dim_{\mathbb F_q}U$ . A linear set comes paired with $U$ , so every statement here is about $U$ . The weight of a point $\langle v\rangle$ is $\dim_{\mathbb F_q}(\langle v\rangle_{\mathbb F_{q^t}}\cap U)$ , and $L_U$ is scattered when every point of $L_U$ has weight $1$ ; equivalently, for every nonzero $u\in U$ ,

\lambda\in\mathbb F_{q^t},\ \lambda u\in U\ \Longrightarrow\ \lambda\in\mathbb F_q .

The plane construction (§2). Fix $n\ge2$ and the field $E=\mathbb F_{q^{6n}}$ with its subfields $\mathbb F_q\subseteq\mathbb F_{q^n}\subseteq\mathbb F_{q^{2n}}$ and $\mathbb F_{q^{3n}}$ . As an $\mathbb F_{q^{2n}}$ -space $E$ has dimension $3$ , so $\mathrm{PG}(E,\mathbb F_{q^{2n}})=\mathrm{PG}(2,q^{2n})$ . For $\omega\in\mathbb F_{q^{2n}}\setminus\mathbb F_{q^n}$ and an $\mathbb F_q$ -linear $f:\mathbb F_{q^{3n}}\to\mathbb F_{q^{3n}}$ the paper studies

U_f=\{f(x)+x\omega : x\in\mathbb F_{q^{3n}}\},

with $f$ a monomial $ax^{q^i}$ or a binomial $f_{i,a,b}(x)=ax^{q^i}+bx^{q^{2n+i}}$ . The relative norms $N_{q^m/q^d}(x)=\prod_{j<m/d}x^{q^{dj}}$ enter the hypotheses.

Formalization targets

Goal: Theorem 1.2 (p. 3)

For $t$ even and $r\ge2$ , in each of the cases (a) $q=2$ , $t\ge4$ ; (b) $t\not\equiv0\pmod3$ ; (c) $q\equiv1\pmod3$ , $t\equiv0\pmod3$ ,

\exists\,U\subseteq\mathbb F_{q^t}^{\,r}\ \ \mathbb F_q\text{-subspace}:\qquad \dim_{\mathbb F_q}U=\frac{rt}{2},\quad L_U\ \text{scattered}.

Milestones, in proof order

Proposition 2.1 (p. 5): $U_f$ has rank $3n$ , and $L_{U_f}$ is scattered iff $Q_f\cap\mathbb F_{q^{2n}}=\mathbb F_q$ , where $Q_f$ is the set of quotients $\frac{f(x)+x\omega}{f(y)+y\omega}$ , $y\ne0$ .
Proposition 2.2 (p. 6): the same criterion through the polynomial system (5)–(6).
Theorems 2.3, 2.4 (pp. 7, 9): the monomial families, for $n\not\equiv0\pmod 3$ and for $q\equiv1\pmod3$ .
Theorem 2.5 (p. 10): existence in $\mathrm{PG}(2,q^{2n})$ in those two regimes.
Lemma 2.6 (p. 11): $\varphi(x)/x$ and $\bar\varphi(x)/x$ have the same image, where $\bar\varphi$ is the trace adjoint.
Proposition 2.7, Lemma 2.8, Proposition 2.9, Theorem 2.10 (pp. 12–16): the binomial family for $q=2$ .
Theorem 3.1 (p. 16): direct sums of scattered linear sets are scattered, of rank $rt/2$ iff each summand has rank $s_it/2$ .
The line example (p. 2, cited from Lavrauw's thesis) and the Baer-subplane case $r=3$ , $t=2$ (p. 3).

Significance

Theorem 1.2 gives maximum scattered linear sets, and hence two-intersection sets, two-weight codes and strongly regular graphs, for infinitely many $(q,t)$ with $r$ odd, a regime where earlier existence results covered only a few values of $t$ . The $q=2$ case feeds the paper's second main result: scattered $\mathbb F_2$ -linear sets of $\mathrm{PG}(2,2^t)$ of rank $3t/2$ are translation caps, from which complete caps of size $2\sqrt{q^{\,n-1}}$ in $\mathrm{AG}(n,q)$ are built.

All statements are proved in the preprint; none has a machine-checked proof. Formalizing them requires a usable theory of subfields of a finite field as Frobenius fixed fields, relative norms and their images, linearized polynomials and their trace adjoints, and the passage between $\mathbb F_q$ -dimension, cardinality and weight. Each of these is reusable for later work on linear sets, MRD codes and semifields.

Difficulty

The criterion of Proposition 2.2 reduces scatteredness to a polynomial system, but the system has to be solved for a specific $f$ . For the monomials this rests on the solvability of $z^{q^i-1}=c$ in $\mathbb F_{q^{3n}}$ , a norm condition interacting with the gcd hypotheses. For the binomial with $q=2$ , the existence of a suitable $b$ (Lemma 2.8) needs a value-set bound for non-permutation polynomials (Turnwald, 1995) and a point count on a plane curve. The higher-dimensional statement then needs the elementary bound $\dim U\le st/2$ for scattered $U$ to obtain the rank equivalence in Theorem 3.1. A tempting shortcut, taking $U=\mathbb F_q^{\,r}$ or any small subspace, is scattered but has the wrong rank; the content is in the rank $rt/2$ .

Formalization scope

Citation basis. arXiv:1512.07467v1; page numbers equal PDF pages.
Fields. $\mathbb F_{q^m}\subseteq E$ is the fixed field of $x\mapsto x^{q^m}$ in a finite field $E$ of characteristic $p$ with $|E|=q^{6n}$ , $q=p^h$ . Norms and traces are explicit Frobenius products and sums.
Subspaces and rank. An $\mathbb F_q$ -subspace is a carrier set with closure conditions. Rank $k$ is $|U|=q^k$ ; in Theorem 3.1 rank $rt/2$ is $|W|^2=q^{rt}$ .
Points. Scatteredness takes the spanning field as an argument: $\mathbb F_{q^{2n}}$ in §2, the whole $\mathbb F_{q^t}$ in Theorem 1.2 and §3. $\mathrm{PG}(r-1,q^t)$ is modelled on Fin r → K; the plane of §2 on $E$ itself.
Pinned readings.
- Theorem 1.2 prints no range for $r$ . The preceding sentence and the proof (p. 17) say $r\ge5$ , and $r=1$ is false. The goal assumes $r\ge2$ , covered by the line example ( $r=2$ ), §2 with the Baer case ( $r=3$ ) and Theorem 3.1 ( $r\ge4$ ).
- $\omega$ is quantified over all of $\mathbb F_{q^{2n}}\setminus\mathbb F_{q^n}$ .
- The index ranges $1\le i\le3n-1$ (monomial) and $2n+i\le3n-1$ (binomial) come from the case headings on pp. 7 and 10.
- Proposition 2.7's printed " $wx$ " is $\omega x$ .
- Theorem 2.10 keeps its printed hypothesis $N_{2^{3n}/2^n}(b)\ne1$ .
- Theorem 3.1's rank clause assumes $t\ge2$ ; for $t=1$ it is false.
Ruled out. Taking the span over $E$ or over $\mathbb F_q$ , or dropping the rank, would make the statements false or trivial; every existence statement fixes the rank, and the span field is explicit.
Contributions welcome. Frobenius-fixed-field cardinalities, norm surjectivity, the criteria of Propositions 2.1–2.2, the monomial and binomial families, and the direct-sum rank computation.

Selected references

D. Bartoli, M. Giulietti, G. Marino, O. Polverino, Maximum scattered linear sets and complete caps in Galois spaces, arXiv:1512.07467v1 (2015); Combinatorica 37 (2017). https://arxiv.org/abs/1512.07467, https://doi.org/10.1007/s00493-016-3531-6
A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geom. Dedicata 81 (2000), 231–243. https://doi.org/10.1023/A:1005283806897
O. Polverino, Linear sets in finite projective spaces, Discrete Math. 310 (2010), 3096–3107. https://doi.org/10.1016/j.disc.2010.04.007
S. Ball, A. Blokhuis, M. Lavrauw, Linear (q + 1)-fold blocking sets in PG(2, q⁴), Finite Fields Appl. 6 (2000), 294–301.
M. Lavrauw, Scattered Spaces with respect to Spreads and Eggs in Finite Projective Spaces, Ph.D. thesis, TU Eindhoven, 2001.
G. Turnwald, A new criterion for permutation polynomials, Finite Fields Appl. 1 (1995), 64–82.

15 thms2 active usersReviewed

Completed

Information Theory Operations Research Probability+1·Captain: mikedeng1

Bootstrap Robust Prescriptive Analytics 3: Any Distance Exceeding the Bootstrap Distance Near Some D Loses the Disappointment Rate −rResearch Paper

Motivation

Data-driven decision making estimates the cost of a decision from training data and then optimizes that estimate. The optimized estimate is biased downwards: the decision that looks best on the training data tends to disappoint on fresh data. Distributionally robust optimization counters this by optimizing the worst case of the estimate over all distributions within a radius $r$ of the empirical distribution, measured by a chosen distance function $R$ . Many distance functions are in use (φ-divergences, Wasserstein distances, moment sets), and the choice is usually justified by tractability.

Bertsimas and Van Parys, Bootstrap robust prescriptive analytics (arXiv:1711.09974v2), measure disappointment on bootstrap data: resamples drawn with replacement from the training data. Their Theorem 6 shows that with the entropic bootstrap distance $B$ the bootstrap disappointment decays exponentially in the sample size at rate at least $r$ . Proposition 1, the subject of this mission, is the converse: $B$ is the smallest distance function with this guarantee. Any distance that is strictly larger than $B$ near some distribution admits a nominal formulation whose disappointment decays strictly slower than $e^{-nr}$ . The result is in the spirit of Van Parys, Esfahani and Kuhn (arXiv:1704.04118), where the relative entropy is shown to be the optimal ambiguity set for i.i.d. data.

Setting

The distinct training points form a finite set $\Omega_n$ , written $\iota$ in Lean. A distribution on it is a vector $D\in\mathbb R^\iota$ with nonnegative entries summing to one; the simplex of all such vectors is $\mathcal D_n$ . The training data have the empirical distribution $D_{\rm tr}\in\mathcal D_n$ , which gives positive weight to every point of $\Omega_n$ .

The bootstrap distance (Definition 6, Eq. (27)) is the relative entropy

B(D,D')=\sum_{i\in\iota}D_i\log\frac{D_i}{D'_i},

with $0\log0=0$ and $B(D,D')=+\infty$ if some $D_i>0=D'_i$ .

A distribution distance function (Definition 4) is a map $R:\mathcal D_n\times\mathcal D_n\to(-\infty,+\infty]$ that is nonnegative, vanishes exactly on the diagonal ( $R(D',D)=0$ iff $D'=D$ ), and is convex in its first argument. $B$ is one.

A bootstrap sample of size $n$ is $n$ independent draws from $D_{\rm tr}$ (Eq. (14)); its law is the product $D_{\rm tr}^n$ , and its empirical distribution is $D_{{\rm bs}[n]}$ , the frequency of each point of $\iota$ among the $n$ draws.

A nominal formulation here is a loss $G:\iota\to\mathbb R_+$ with cost estimator $\mathbb E_D[G]=\sum_iD_iG_i$ . Its robust counterpart (Eq. (24)) replaces the estimate by $\sup\{\mathbb E_{D'}[G]: D'\in\mathcal D_n,\ R(D',D_{\rm tr})\le r\}$ , and its disappointment set is

\mathcal R=\Big\{D\in\mathcal D_n:\ \mathbb E_D[G]>\sup_{D'\in\mathcal D_n,\ R(D',D_{\rm tr})\le r}\mathbb E_{D'}[G]\Big\},

the bootstrap distributions on which the realized cost exceeds the robust budget.

Formalization targets

Goal: Proposition 1 (p. 16)

Let $R$ be a distribution distance function, $D\in\mathcal D_n$ with $B(D,D_{\rm tr})=r$ , and $\mathcal N\subseteq\mathcal D_n$ a neighbourhood of $D$ , open in $\mathcal D_n$ , on which $R(\cdot,D_{\rm tr})>r$ . Then there is a loss $G\ge0$ whose disappointment set satisfies

-r<\liminf_{n\to\infty}\frac1n\log D^\infty_{\rm tr}\big[D_{{\rm bs}[n]}\in\mathcal R\big],

stated in Lean in the equivalent form: for some $\varepsilon>0$ , eventually $D^n_{\rm tr}[D_{{\rm bs}[n]}\in\mathcal R]\ge e^{-n(r-\varepsilon)}$ .

Milestones (Appendix B.2, p. 27, and Eq. (31), p. 16)

Separation. The $R$ -ball $\{R(\cdot,D_{\rm tr})\le r\}$ and a convex open $\mathcal N$ on which $R>r$ are separated by a linear functional: $\mathbb E_D[G]\le a<\mathbb E_{D'}[G]$ .
Inclusion. For such $G$ and $a$ , ${\rm int}\,\mathcal N=\mathcal N\subseteq\mathcal R$ .
Sanov's lower bound (31). $-\inf_{D\in{\rm int}\,\mathcal C}B(D,D_{\rm tr})\le\liminf_n\frac1n\log D^\infty_{\rm tr}[D_{{\rm bs}[n]}\in\mathcal C]$ for every set $\mathcal C$ .
Convexity step. $B(\lambda D+(1-\lambda)D_{\rm tr},D_{\rm tr})\le\lambda B(D,D_{\rm tr})+(1-\lambda)B(D_{\rm tr},D_{\rm tr})<r$ for $\lambda\in(0,1)$ .
Infimum below $r$ . $\inf_{D'\in\mathcal N}B(D',D_{\rm tr})<r$ .

Significance

Proposition 1 turns Theorem 6 from a sufficient condition into a characterization. Theorem 6 says the bootstrap distance guarantees disappointment rate $r$ ; Proposition 1 says no distance function that is larger than $B$ on an open set does, for some nominal formulation. A practitioner who wants the bootstrap guarantee with the least conservative ambiguity set therefore has no better choice than $B$ in this sense. The result is one instance of a pattern in data-driven optimization, where large-deviation rate functions appear as the optimal ambiguity sets.

The paper's proof is a short combination of three standard facts: strict separation of convex sets, Sanov's theorem, and convexity of relative entropy. None of the three is available on the platform in the form needed. Sanov's theorem for empirical distributions on a finite alphabet has no machine-checked proof in Mathlib or on the platform; the lower bound (31) is a self-contained, reusable result of independent interest. The separation step needs strict separation inside the affine hull of the simplex, which Mathlib provides only in the ambient vector space. The result is proved on paper; none of it is formalized.

Difficulty

The separation and convexity steps are routine once the relative topology of the simplex is handled. The central difficulty is the lower bound (31), a large-deviation lower bound for the empirical distribution of i.i.d. draws. The bootstrap probability of an event is a sum of multinomial probabilities over the empirical distributions with denominator $n$ that fall in the event, and the bound must hold for every point of the relative interior, including points on the boundary of the simplex, where some coordinates vanish and the distance $B$ is not differentiable. An argument that only treats distributions of full support, or only open sets of $\mathbb R^\iota$ , does not cover these points.

A second difficulty is bookkeeping between the three topologies in play: the ambient space $\mathbb R^\iota$ , the simplex $\mathcal D_n$ , and the affine hull in which separation takes place.

Formalization scope

$\Omega_n$ is a finite type $\iota$ with decidable equality; distributions are stdSimplex ℝ ι. Covariates, responses, neighbourhood weights and the decision $z$ are abstracted away: the nominal formulation is the estimator $D\mapsto\sum_iD_iG_i$ (the estimator (18) with $k=n$ and unit weights), so the robust prescription $z^r_{\rm tr}(x_0)$ plays no role.
$D_{\rm tr}$ has all coordinates positive (the support convention of the paper).
$B$ and $R$ are EReal-valued; convexity of $R$ is written out in EReal. The supremum defining $\mathcal R$ is an EReal supremum. It is never empty, because $D_{\rm tr}$ lies in the $R$ -ball, so $\mathcal R$ cannot collapse to all of $\mathcal D_n$ .
The bootstrap law is the $n$ -fold product Measure.pi of $\sum_iD_{{\rm tr},i}\,\delta_i$ , with $D_{\rm tr}$ fixed while $n\to\infty$ .
"Open" and "int" are relative to $\mathcal D_n$ . With the ambient topology, no nonempty subset of the simplex is open and every interior is empty, which would make Proposition 1 and (31) vacuous; this formalization rules that out, as it rules out a junk real logarithm ( $\log0=0$ ) by using the explicit- $\varepsilon$ form of every rate statement.
Disclosed additions: the separation milestone assumes $\mathcal N$ is convex, nonempty and inside the relative interior of the simplex; the infimum milestone assumes $r>0$ , which holds in Proposition 1.

A complete development needs the method of types on a finite alphabet, strict separation in an affine subspace, and the convexity of relative entropy. The method-of-types lower bound is reusable well beyond this mission (hypothesis testing, large deviations of empirical measures). Proofs of any milestone, and alternative proofs of (31), are welcome.

Selected references

D. Bertsimas, B. Van Parys, Bootstrap robust prescriptive analytics, arXiv:1711.09974v2, 2021; Mathematical Programming, 2021. https://arxiv.org/abs/1711.09974
A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 2009 (Theorem 6.2.10, Sanov's theorem). https://doi.org/10.1007/978-3-642-03311-7
B. Van Parys, P. Mohajerin Esfahani, D. Kuhn, From data to decisions: distributionally robust optimization is optimal, Management Science 67(6), 2021. https://arxiv.org/abs/1704.04118
I. Csiszár, The method of types, IEEE Transactions on Information Theory 44(6), 1998. https://doi.org/10.1109/18.720546
B. Efron, The Jackknife, the Bootstrap and Other Resampling Plans, SIAM, 1982. https://doi.org/10.1137/1.9781611970319

9 thms2 active usersReviewed

Completed

Operations Research Optimization Probability+1·Captain: mikedeng1

From Data to Decisions: Distributionally Robust Optimization Is Optimal 1: The Relative-Entropy Robust Predictor Is the Least Conservative Predictor Whose Disappointment Decays at Rate rResearch Paper

Motivation

A decision maker who must choose $x$ before observing an uncertain outcome $\xi$ usually does not know the distribution of $\xi$ ; only past observations $\xi_1,\dots,\xi_T$ are available. Data-driven optimization replaces the unknown expected cost by an estimate computed from the data. The simplest estimate, the sample average, is optimistically biased: the cost realized out of sample is, with probability close to one half, higher than predicted. Many corrections have been proposed: robust optimization over moment, $\phi$ -divergence or Wasserstein ambiguity sets (Delage & Ye 2010; Ben-Tal et al. 2013; Bertsimas, Gupta & Kallus 2018), and empirical-likelihood methods (Lam 2019; Duchi, Glynn & Namkoong 2021). Each is justified by a guarantee it satisfies. Van Parys, Mohajerin Esfahani and Kuhn (arXiv:1704.04118; Management Science 67(6), 2021) ask a different question: among all estimates that satisfy a given guarantee, which one is the least conservative? Their answer singles out one distributionally robust predictor, built on the relative entropy, as the best possible one in a precise sense. This mission formalizes that answer for the prediction problem with finitely many outcomes.

Setting

The outcome $\xi$ takes values in $\Xi=\{1,\dots,d\}$ . Decisions range over a compact set $X\subseteq\mathbb R^n$ , and the cost $\gamma(x,i)$ is continuous in $x$ for each $i$ . These are the standing assumptions of §2 (p. 5).

A model is a point $\mathbb P$ of the probability simplex $\mathcal P=\{\mathbb P\in\mathbb R^d_+:\sum_i\mathbb P(i)=1\}$ , with the topology inherited from $\mathbb R^d$ . Under a model the expected cost is $c(x,\mathbb P)=\sum_i\mathbb P(i)\gamma(x,i)$ .

The data are $T$ independent draws from an unknown model. They enter only through the empirical distribution $\hat{\mathbb P}_T(i)=\frac1T\#\{t\le T:\xi_t=i\}$ . Write $\mathbb P^\infty(\cdot)$ for probabilities when the samples are drawn from $\mathbb P$ .

A data-driven predictor is a continuous function $\hat c:X\times\mathcal P\to\mathbb R$ ; the number $\hat c(x,\hat{\mathbb P}_T)$ estimates $c(x,\mathbb P)$ . The set of all of them is $\mathcal C$ . Its out-of-sample disappointment is the probability $\mathbb P^\infty\big(c(x,\mathbb P)>\hat c(x,\hat{\mathbb P}_T)\big)$ that the true cost exceeds the prediction.

The relative entropy of $\mathbb P'$ with respect to $\mathbb P$ is

I(\mathbb P',\mathbb P)=\sum_{i}\mathbb P'(i)\log\frac{\mathbb P'(i)}{\mathbb P(i)}\in[0,\infty],

with $0\log(0/p)=0$ and $p'\log(p'/0)=+\infty$ for $p'>0$ .

For a threshold $r\ge0$ , the distributionally robust predictor is

\hat c_r(x,\mathbb P')=\sup_{\mathbb P\in\mathcal P}\{c(x,\mathbb P):I(\mathbb P',\mathbb P)\le r\}.\tag{10}

It is the worst expected cost over all models under which the observed frequencies $\mathbb P'$ are not exponentially unlikely at rate more than $r$ . The observed frequencies are the first argument of $I$ .

Formalization targets

Goal: Theorem 4 (strong optimality)

The paper's meta-optimization problem (5) is

\min_{\hat c\in\mathcal C}{}^{\preceq_{\mathcal C}}\ \hat c\quad\text{s.t.}\quad\limsup_{T\to\infty}\frac1T\log\mathbb P^\infty\big(c(x,\mathbb P)>\hat c(x,\hat{\mathbb P}_T)\big)\le-r\quad\forall x\in X,\ \mathbb P\in\mathcal P,

where $\hat c_1\preceq_{\mathcal C}\hat c_2$ means $\hat c_1\le\hat c_2$ pointwise on $X\times\mathcal P$ . A feasible $\hat c^\star$ is strongly optimal if $\hat c^\star\preceq_{\mathcal C}\hat c$ for every feasible $\hat c$ . The goal is:

\text{If } r>0,\ \text{then } \hat c_r \text{ is strongly optimal in (5).}

This statement contains feasibility (continuity and the decay rate) and pointwise domination of every feasible competitor.

Milestones

Proposition 1(ii) and (iii): $I$ is jointly convex and lower semicontinuous on $\mathcal P\times\mathcal P$ .
The supremum in (10) is attained.
Theorem 2: the strong LDP $\mathbb P^\infty(\hat{\mathbb P}_T\in\mathcal D)\le(T+1)^de^{-T\inf_{\mathcal D}I(\cdot,\mathbb P)}$ .
Theorem 1: the weak LDP, upper bound (7a) and, for $\mathbb P>0$ , lower bound (7b) with the interior of $\mathcal D$ .
Proposition 2: the dual representation $\hat c_r(x,\mathbb P')=\min_{\alpha\ge\bar\gamma(x)}\alpha-e^{-r}\prod_i(\alpha-\gamma(x,i))^{\mathbb P'(i)}$ , with a minimizer in an explicit interval.
Proposition 3 and Theorem 3: $\hat c_r$ is continuous, and is feasible in (5) for every $r\ge0$ .
Display (15): a maximizer in the closed relative entropy ball can be approximated in cost by a strictly positive model in the open ball.

Two further statements are included without milestones: Proposition 1(i), the information inequality, and Theorem 5, the finite-sample bound $(T+1)^de^{-rT}$ on the disappointment of $\hat c_r$ .

Significance

The theorem turns a choice among robust estimators into a uniqueness statement. If a decision maker asks only for a disappointment probability that decays exponentially at rate $r$ under every possible model, then $\hat c_r$ is the unique least conservative continuous predictor. Any predictor that is smaller anywhere fails the guarantee for some model. The reverse predictor (12) and the restricted predictor (13), which fix the other argument of $I$ or hedge only against models absolutely continuous with respect to the observed frequencies and are common in the literature, differ from $\hat c_r$ (Remark 3, pp. 15–16), so the theorem does not single them out. The companion missions of this series extend the result to predictor–prescriptor pairs (mission 2) and to compact continuous outcome spaces (mission 3).

The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. A formal development would also give Mathlib-level statements of the method of types: Sanov's theorem for finite alphabets in both its finite-sample and asymptotic forms, together with the convexity and semicontinuity of the relative entropy with the $+\infty$ convention. These are reusable far beyond this paper.

Difficulty

Feasibility (Theorem 3) is a direct consequence of the LDP upper bound, once the disappointment set is seen to lie outside the relative entropy ball. The difficulty is the optimality half. Showing that a competitor $\hat c$ with $\hat c(x,\mathbb P_0')<\hat c_r(x,\mathbb P_0')$ at a single point must be infeasible requires a lower bound on a disappointment probability. The obvious approach evaluates the LDP lower bound at a maximizer $\mathbb P_0$ of (10). That fails: the lower bound (7b) needs a strictly positive model, the maximizer usually lies on the boundary of the simplex and on the boundary of the ball $I(\mathbb P_0',\cdot)\le r$ , and the bound is only in terms of the interior of the disappointment set. The argument has to move to a nearby model, and this uses the continuity of $\hat c$ , the convexity of $I$ , and the $+\infty$ convention of $I$ in its second argument. The asymptotic statements also require care with the logarithm of a vanishing probability.

Formalization scope

Outcomes and models. $\Xi$ is Fin d. $\mathcal P$ is the subtype of stdSimplex ℝ (Fin d), so interiors and continuity are relative to $\mathcal P$ , as footnote 1 (p. 12) requires.
Decisions and cost. $X$ is a compact subset of EuclideanSpace ℝ (Fin n), and $\gamma : X\to\mathbb R^d$ is continuous in $x$ for each outcome.
Relative entropy. $I$ is EReal-valued and is $+\infty$ whenever $\mathbb P(i)=0<\mathbb P'(i)$ . A real-valued sum would give a finite value there under Lean's log 0 = 0, and so change $\hat c_r$ .
Probabilities. Sampling probabilities are finite sums over sample paths $\Xi^T$ . The empirical distribution is defined for $T\ge1$ ; finite-sample statements assume $T\ge1$ .
Decay rates. Rates are stated without logarithms: $\limsup\frac1T\log p_T\le-r$ is written "for every $r'<r$ , eventually $p_T\le e^{-r'T}$ ". The form through Real.log would give a never-disappointed predictor rate $0$ , which makes Theorem 3 false.
Infima. Infima of $I$ are taken in the extended reals.
Competitors. They range over all jointly continuous functions on $X\times\mathcal P$ . Dropping continuity makes Theorem 4 false.
Sets $\mathcal D$ . The LDP statements require Borel $\mathcal D\subseteq\mathcal P$ , represented by MeasurableSet D in the simplex subtype.
Display (15). The clause $0<r_2$ is dropped: it is unused, and it fails for $d=1$ .

Welcome contributions: the method of types on Fin d (type classes, their cardinality bounds and probabilities); joint convexity and lower semicontinuity of the finite relative entropy with the $+\infty$ convention; and Berge's maximum theorem in the form used for Proposition 3. These are reusable beyond this mission. The definitions duplicate those of mission 2 of this series and are meant to be merged once published.

The source is the arXiv preprint arXiv:1704.04118v3 (22 Dec 2019); all theorem, display and page numbers refer to it.

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.04118v3 — https://doi.org/10.1287/mnsc.2020.3678
T. M. Cover, J. A. Thomas, Elements of Information Theory, 2nd ed., Wiley, 2006 (Theorems 2.6.3, 2.7.2, 11.4.1). https://doi.org/10.1002/047174882X
A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 1998. https://doi.org/10.1007/978-1-4612-5320-4
A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3), 2010. https://doi.org/10.1287/opre.1090.0741
C. Berge, Topological Spaces, Oliver & Boyd, 1963 (pp. 115–116, maximum theorem).

13 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Constrained Assortment Optimization for the Nested Logit Model 7: Under Space Constraints, for Every α > 1, O(⌈α/(α−1)⌉ n^(⌈α/(α−1)⌉+2)) Candidate Assortments Include an α-Approximate SolutionResearch Paper

Motivation

A retailer that sells products in categories must decide which products to offer in each category. When customers choose among the offered products according to the nested logit model, the expected revenue depends on the offered assortment in a nonlinear way, and the retailer's shelf space adds a knapsack constraint in every category. Gallego and Topaloglu (Management Science, 2014) show that the resulting space-constrained assortment problem is NP-hard even with a single nest (via Lemma 2.1 of Rusmevichientong, Shen and Shmoys, cited in the paper as 2009), give a factor-2 approximation through a linear program, and then, in Online Supplement C of the paper, refine the approach into an approximation scheme: for every desired guarantee $\alpha>1$ , a polynomially sized family of candidate assortments per nest suffices.

The scheme follows the partial-enumeration idea of Frieze and Clarke (1984) for multi-dimensional knapsack problems, but has to work for a whole one-parameter family of knapsack problems, one for every value of a scalar $u\ge0$ , with a single collection of candidates fixed in advance.

Setting

There are nests $i\in M$ and products $j\in N=\{1,\dots,n\}$ . Product $j$ of nest $i$ has a preference weight $v_{ij}>0$ , a revenue $r_{ij}\in\mathbb R$ (no sign or order is assumed), and a space requirement $w_{ij}>0$ ; nest $i$ has capacity $c_i$ with $w_{ij}\le c_i$ . An assortment of nest $i$ is a set $S\subseteq N$ ; it is feasible, $S\in\mathcal C_i$ , when $\sum_{j\in S}w_{ij}\le c_i$ . Write

V_i(S)=\sum_{j\in S}v_{ij},\qquad R_i(S)=\frac{\sum_{j\in S}r_{ij}v_{ij}}{V_i(S)}\quad(R_i(\emptyset)=0).

For $u\ge0$ , problem (7) is $\max_{S\in\mathcal C_i}V_i(S)(R_i(S)-u)$ , which equals the knapsack problem (10) $\max_{S\in\mathcal C_i}\sum_{j\in S}v_{ij}(r_{ij}-u)$ . The quantity $v_{ij}(r_{ij}-u)$ is the utility of product $j$ ; $z^\ast(u)$ denotes the optimal value of (10). An assortment $\hat S\in\mathcal C_i$ is $\alpha$ -approximate at $u$ when $V_i(S)(R_i(S)-u)\le\alpha V_i(\hat S)(R_i(\hat S)-u)$ for all $S\in\mathcal C_i$ .

For a set $J\subseteq N$ , problem (17) is the linear program

\max\Big\{\sum_{j}v_{ij}(r_{ij}-u)x_{ij} : \sum_j w_{ij}x_{ij}\le c_i,\ x_{ij}=1\ (j\in J),\ 0\le x_{ik}\le\mathbf 1\big(v_{ik}(r_{ik}-u)\le\min_{j\in J}v_{ij}(r_{ij}-u)\big)\ (k\notin J)\Big\},

the LP relaxation of (10) with the products of $J$ fixed in the knapsack and every product whose utility exceeds the smallest utility in $J$ removed. Its optimal value is $\zeta^\ast(u,J)$ . Rounding a solution $x$ down gives the assortment $\lfloor x\rfloor=\{j:x_{ij}=1\}$ . $\wp_q$ is the family of subsets of $N$ with at most $q$ elements.

Formalization targets

Goal: Theorem 9 (p. 40)

For every $\alpha>1$ , with $q=\lceil\alpha/(\alpha-1)\rceil$ , there is a collection $\{A_i^t:t\in\mathcal T_i\}\subseteq\mathcal C_i$ such that

|\mathcal T_i|\le 5(q+1)\,n^{q+2}+1\quad\text{and}\quad\forall u\ge0\ \exists t:\ A_i^t\text{ is }\alpha\text{-approximate for (7) at }u .

The paper writes $|\mathcal T_i|=O(\lceil\alpha/(\alpha-1)\rceil n^{\lceil\alpha/(\alpha-1)\rceil+2})$ ; the explicit bound above is of that order.

Milestones

Whenever (17) is feasible, it has an optimal solution with at most one fractional component (p. 39).
If an optimal $S^\ast_i$ of (10) at $\hat u$ has $|S^\ast_i|\le q$ , then rounding down an optimal solution of (17) with $J=S^\ast_i$ solves (10) at $\hat u$ (p. 41).
If $|S^\ast_i|>q$ and $J^\ast_i$ holds $q$ products of $S^\ast_i$ of largest utility, a fractional component $j'$ of an optimal solution of (17) at $(\hat u,J^\ast_i)$ satisfies $v_{ij'}(r_{ij'}-\hat u)\le z^\ast(\hat u)/q$ (pp. 41–42).
In the same situation $S^\ast_i$ is feasible for (17), so $z^\ast(\hat u)\le\zeta^\ast(\hat u,J^\ast_i)$ (p. 42).
Lemma 8 (p. 40), per $u$ : for $q\ge2$ and every $u\ge0$ some $J\in\wp_q$ makes every optimal solution of (17) with at most one fractional component round down to a $q/(q-1)$ -approximate solution of (10).

Significance

Together with Theorem 4 of the paper (an $\alpha$ -approximate candidate per nest for every $u$ yields an $\alpha$ -approximate assortment for the whole problem) and Theorem 2 (the best combination of candidates solves a linear program with $1+m$ variables), Theorem 9 gives, for every $\alpha>1$ , an $\alpha$ -approximation of the space-constrained nested logit assortment problem by a single linear program with $O(m\lceil\alpha/(\alpha-1)\rceil n^{\lceil\alpha/(\alpha-1)\rceil+2})$ constraints; for $\alpha=3/2$ this is $O(mn^5)$ . It shows that the factor 2 of Section 5 is not a barrier of the method.

The result is proved in the paper. As far as the platform's records show, none of it is formalized; this mission produces a machine-checked proof of Lemma 8 and Theorem 9, including the explicit counting of parameter intervals that the paper only sketches.

A related but different construction, with large and small products and a continuous knapsack whose weights are preference weights, appears in the unconstrained variants of Davis, Gallego and Topaloglu (items NestedLogitVariants.PowersDelta.*); it is not reused here.

Difficulty

Two points resist the obvious argument. First, rounding down the plain LP relaxation of (10) drops one fractional product whose utility can be as large as the whole optimum, which is why Section 5 only reaches a factor 2; no choice of rounding of that relaxation alone does better. The guarantee has to come from the partially fixed problems (17), and their indicator constraint is delicate: it excludes only products of strictly larger utility than the least utility in $J$ , and a version that also excludes ties can cut off the optimal assortment of (10), and the comparison with $z^\ast(u)$ is then lost.

Second, the collection must be fixed before $u$ . The optimal solution of (17) depends on $u$ through the ordering of the utilities, the ordering of the utility-to-space ratios and the signs of the utilities, which change only at the intersection points of $2(n+1)$ lines. Because the feasible set of (17) itself depends on $u$ through the indicator constraint, the solution on an open interval between two such points need not remain optimal at its endpoints; the count must treat the breakpoints as pieces of their own.

Formalization scope

Nests are a finite type ι; products are Fin n (0-based); assortments are Finset (Fin n), with $\emptyset$ for $\bar 0$ .
The published model NestedLogitVariants.LP.Model is referenced; its within-nest no-purchase weight is set to zero (I.vnp i = 0), which makes V and R the paper's $V_i$ and $R_i$ . The paper's extension $V_i(S_i)=v_{i0}\mathbf 1(S_i\ne\bar 0)+\dots$ is not formalized.
Added hypotheses, all flagged in the items: $v_{ij}>0$ , $w_{ij}>0$ , $c_i\ge0$ (the empty assortment is feasible even when $n=0$ ), $q\ge2$ in Lemma 8 and $q\ge1$ in milestone 3. The paper's $w_{ij}\le c_i$ is kept in the goal.
The paper's $O(\cdot)$ is pinned to $5(q+1)n^{q+2}+1$ , with a constant that does not depend on $\alpha$ , as the paper's explicit factor $\lceil\alpha/(\alpha-1)\rceil$ indicates: for $n\ge1$ , at most $(q+1)n^q$ sets in $\wp_q$ times at most $2n(n+1)+1\le5n^2$ pieces of $[0,\infty)$ ; the $+1$ covers $n=0$ .
$q=\lceil\alpha/(\alpha-1)\rceil$ is Nat.ceil; $\alpha>1$ is strict.
The collection is quantified before $u$ ; problem (17) is a real LP over $[0,1]^n$ ; its indicator constraint excludes only products of strictly larger utility.
Lemma 8 is stated per $u$ : the interval solutions $x_i^g(J)$ are not defined, and their counting belongs to Theorem 9.
Trivializing formalizations are ruled out: the size bound is part of the goal (without it $A=\mathcal C_i$ works, and a bound like $2^n$ would do the same); $\alpha$ is arbitrary in $(1,\infty)$ , not fixed; and (17) carries its indicator constraint, without which the $q/(q-1)$ argument fails.
Welcome contributions: a reusable greedy theorem for the fractional knapsack LP (one fractional component), and a general lemma counting the pieces on which a finite family of affine functions has constant order and signs.

Selected references

G. Gallego and H. Topaloglu, Constrained Assortment Optimization for the Nested Logit Model, Management Science 60(10), 2014. https://doi.org/10.1287/mnsc.2014.1931 (cited from the authors' manuscript of Sept. 11, 2013).
A. M. Frieze and M. R. B. Clarke, Approximation algorithms for the m-dimensional 0–1 knapsack problem: worst-case and probabilistic analyses, European Journal of Operational Research 15(1), 1984. https://doi.org/10.1016/0377-2217(84)90053-5
P. Rusmevichientong, Z.-J. M. Shen and D. B. Shmoys, Dynamic assortment optimization with a multinomial logit choice model and capacity constraint, Operations Research 58(6), 2010. https://doi.org/10.1287/opre.1100.0866
J. M. Davis, G. Gallego and H. Topaloglu, Assortment Optimization Under Variants of the Nested Logit Model, Operations Research 62(2), 2014. https://doi.org/10.1287/opre.2014.1256

9 thms2 active usersReviewed

Convex Optimization Dynamical Systems Optimization·Captain: mikedeng1

First-Order Optimization Algorithms via Inertial Systems with Hessian Driven Damping I: Under (G₂)–(G₃), (DIN-AVD)α,β,b Trajectories Satisfy f(x(t)) − min f = O(1/(t²w(t)))Research Paper

Motivation

Accelerated first-order methods for convex minimization, starting with Nesterov's 1983 scheme, reach the rate $f(x_k)-\min f=\mathcal O(1/k^2)$ , which is optimal for the class of convex functions with Lipschitz gradient. Su, Boyd and Candès (NIPS 2014; JMLR 2016) showed that Nesterov's method is a discretization of the second-order ODE $\ddot x+\frac3t\dot x+\nabla f(x)=0$ , and since then continuous-time inertial dynamics have been the main tool for designing and analysing accelerated algorithms: a Lyapunov argument for the ODE is found first, and then transcribed to the discrete scheme.

Nesterov-type methods oscillate. Adding to the dynamic a damping term driven by the Hessian, $\beta(t)\nabla^2f(x(t))\dot x(t)$ , attenuates these oscillations, and because $\nabla^2f(x(t))\dot x(t)$ is the time derivative of $\nabla f(x(t))$ , time discretizations of such dynamics remain first-order methods. Attouch, Chbani, Fadili and Riahi (arXiv:1907.10536, Math. Program. 2020) develop this programme. This mission formalizes its first result: a convergence-rate theorem for the continuous dynamic with general damping and time-scale functions.

Timeline.

2014: Su, Boyd and Candès identify $\ddot x+\frac3t\dot x+\nabla f(x)=0$ as the continuous limit of Nesterov's method and prove $\mathcal O(1/t^2)$ .
2016: Attouch, Peypouquet and Redont (J. Differential Equations 261; reference [12] of arXiv:1907.10536) add the constant Hessian damping $\beta\nabla^2 f(x)\dot x$ , prove $\mathcal O(1/t^2)$ for $\alpha>3$ and $\int t^2\|\nabla f(x(t))\|^2dt<\infty$ .
2019–2020: Attouch, Chbani, Fadili and Riahi allow time-dependent $\beta(t)$ and a time scale $b(t)$ , and isolate the growth conditions $(\mathcal G_2)$ , $(\mathcal G_3)$ under which the Lyapunov argument works (Theorem 1 here).

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$ that attains its minimum at some point $x^\star$ . Fix a starting time $t_0>0$ , a constant $\alpha\ge1$ , and two non-negative continuous functions $\beta,b:[t_0,+\infty[\to\mathbb R_+$ . These are the paper's standing assumptions (H).

A solution trajectory of

(\mathrm{DIN\text{-}AVD})_{\alpha,\beta,b}\qquad \ddot x(t)+\frac{\alpha}{t}\dot x(t)+\beta(t)\nabla^2 f(x(t))\dot x(t)+b(t)\nabla f(x(t))=0

is a twice differentiable curve $x:[t_0,+\infty[\to\mathcal H$ satisfying this equation at every $t\ge t_0$ . The coefficient $\alpha/t$ is an asymptotically vanishing viscous damping, $\beta(t)$ weights the Hessian-driven damping, and $b(t)$ is a time-scale factor in front of the gradient.

When $\beta$ is differentiable, set

w(t):=b(t)-\dot\beta(t)-\frac{\beta(t)}{t},\qquad \delta(t):=t^2w(t).

The rate in Theorem 1 is expressed through $w$ .

Formalization targets

Goal: Theorem 1

Assume $w$ is differentiable and the growth conditions

(\mathcal G_2)\quad b(t)>\dot\beta(t)+\frac{\beta(t)}{t},\qquad (\mathcal G_3)\quad t\dot w(t)\le(\alpha-3)w(t)

hold for all $t\ge t_0$ . Then $w(t)>0$ and

f(x(t))-\min_{\mathcal H}f=\mathcal O\!\Big(\frac1{t^2w(t)}\Big),\qquad \int_{t_0}^{\infty}t^2\beta(t)w(t)\|\nabla f(x(t))\|^2dt<\infty,

\int_{t_0}^{\infty}t\big((\alpha-3)w(t)-t\dot w(t)\big)\big(f(x(t))-\min f\big)dt<\infty .

The goal leaves $\beta$ and $b$ general. Specific choices are the companions below.

Milestones

The paper's own proof steps, in order:

the derivative (3) of the energy $E(t)=\delta(t)(f(x(t))-f(x^\star))+\frac12\|v(t)\|^2$ , where $v(t)=(\alpha-1)(x(t)-x^\star)+t(\dot x(t)+\beta(t)\nabla f(x(t)))$ ;
the identity $\dot v(t)=t[\dot\beta(t)+\beta(t)/t-b(t)]\nabla f(x(t))$ ;
the differential inequality (4);
the monotonicity of $E$ via (5)–(6);
the two integral bounds by $E(t_0)$ .

Companions

Theorem 3: $\beta(t)\equiv\beta$ , $b(t)=1+\beta/t$ , $\alpha\ge3$ give $\mathcal O(1/t^2)$ and, for $\beta>0$ , $\int t^2\|\nabla f(x(t))\|^2<\infty$ .
Theorem 2: the Attouch–Peypouquet–Redont case $b\equiv1$ , $\alpha>3$ , with the same conclusions.

Significance

The result. Theorem 1 contains the $\mathcal O(1/t^2)$ rate of the continuous Nesterov dynamic as the case $\beta\equiv0$ , $b\equiv1$ , $\alpha\ge3$ . It recovers the Attouch–Peypouquet–Redont theorem and the vanishing-coefficient system of Case 2 as special cases. The time scale $b$ gives faster rates $\mathcal O(1/(t^2w(t)))$ when $w$ grows. For $\beta>0$ it also gives the integral estimate on $\|\nabla f(x(t))\|^2$ , which is the continuous counterpart of the fast decay of gradients proved for the algorithms (IPAHD) and (IGAHD) later in the paper.

Formalizing it. The result is proved in the paper, and nothing about it has been machine-checked. The mission produces:

a reusable predicate for solutions of second-order ODEs with Hessian damping on a half-line;
the Lyapunov identity and inequality for that predicate;
a checked version of the integration step that turns a pointwise differential inequality into finite integrals.

Difficulty

The energy estimate is an exact computation that has to match term by term. The cross terms $\langle\nabla f(x(t)),\dot x(t)\rangle$ cancel only because $\delta=t^2w$ is chosen to match $\dot v$ . That computation needs the chain rule $\frac{d}{dt}\nabla f(x(t))=\nabla^2 f(x(t))\dot x(t)$ in a Hilbert space.

The naive conclusion " $\dot E\le0$ , so integrate (4)" hides two analytic steps:

monotonicity from a one-sided derivative on a closed half-line;
integrability on an unbounded interval of non-negative functions that need not be continuous, because $\dot w$ is only assumed to exist.

The (i) rate needs the positivity of $w$ from $(\mathcal G_2)$ to divide by $\delta(t)$ .

Formalization scope

Lean conventions:

$\mathcal H$ is a real inner product space that is complete. $\nabla f$ is Mathlib's gradient f, and $\nabla^2 f(x)u$ is fderiv ℝ (gradient f) x u.
Trajectories are maps $\mathbb R\to\mathcal H$ with explicit velocity and acceleration maps, tied to them by HasDerivWithinAt on $[t_0,+\infty[$ . Values before $t_0$ are irrelevant, and derivatives at $t_0$ are one-sided.
$\dot\beta$ and $\dot w$ are explicit maps with derivative hypotheses. The paper writes them, so it presupposes they exist.
$\min f$ is $f(x^\star)$ for a given global minimizer. $\mathcal O$ is =O[atTop], with constants depending on all data.
" $\int<\infty$ " is IntegrableOn on $[t_0,+\infty[$ , never a bound on a Bochner integral that could be the junk value $0$ .

These choices rule out trivial readings: Lean's zero value for the derivative of a non-differentiable function, an ODE with an unlinked velocity, and an integral that is zero because the integrand is not integrable. The goal assumes nothing about $E$ , $v$ or (4)–(6), which appear only in milestones.

Companion items:

Theorems 2 and 3 add $\beta>0$ to the gradient-integral claim. The paper derives it from Theorem 1 (ii), which carries a factor $\beta$ , so it says nothing at $\beta=0$ .
Theorem 2 must cope with growth conditions that hold only for large $t$ .

Contributions are welcome: the chain rule for gradient along a curve, a monotonicity lemma for one-sided derivatives on Ici, and the integrability lemma for non-negative functions bounded by a non-increasing energy.

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
H. Attouch, J. Peypouquet, P. Redont, Fast convex minimization via inertial dynamics with Hessian driven damping, J. Differential Equations 261, No. 10 (2016) 5734–5783 (as cited in arXiv:1907.10536v2, ref. [12]). https://arxiv.org/abs/1907.10536
W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, NIPS 27 (2014) 2510–2518; journal version J. Mach. Learn. Res. 17 (2016). https://jmlr.org/papers/v17/15-084.html
Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Math. Dokl. 27 (1983) 372–376.

7 thms2 active usersReviewed

Completed

Numerical Analysis Operations Research Optimization·Captain: mikedeng1

The Proximal Alternating Direction Method of Multipliers in the Nonconvex Setting: Convergence Analysis and Rates 1: Bounded Iterates Converge to a KKT Point with Finite Length Under the KL PropertyResearch Paper

Motivation

Many problems in signal processing, statistics and machine learning are of the form $\min_x \{g(Ax)+h(x)\}$ : a smooth data-fitting term $h$ , plus a possibly nonsmooth and nonconvex regularizer $g$ applied to a linear image $Ax$ of the variable. Examples are total-variation-type penalties with nonconvex potentials, $\ell_0$ -type sparsity terms, and constraints $Ax\in C$ with $C$ nonconvex. The alternating direction method of multipliers (ADMM) treats $g$ and $h$ separately, which makes it the method of choice for this class. For convex problems its convergence theory is classical. For nonconvex problems it was long used as a heuristic, and the Kurdyka–Łojasiewicz (KŁ) framework of Attouch, Bolte, Redont, Soubeyran and Svaiter, and of Bolte, Sabach and Teboulle, is now the standard tool for proving that such methods converge.

Timeline. Li and Pong (SIAM J. Optim. 2015) proved global convergence of a proximal ADMM with $\rho=1$ for twice differentiable $h$ under a KŁ hypothesis. Hong, Luo and Razaviyayn (SIAM J. Optim. 2016) studied related nonconvex ADMM schemes under other assumptions. Boţ and Nguyen (arXiv:1801.01994v2, Math. Oper. Res. 45(2), 2020) extended this in three directions. Their scheme uses variable metrics $M_1^k$ , $M_2^k$ . It allows a relaxation parameter $\rho\in(0,2)$ in the dual step. It covers both a proximal and a proximal-linearized $x$ -update. Under these conditions they proved that bounded iterates have finite length and converge to a KKT point whenever a regularized augmented Lagrangian has the KŁ property. This mission formalizes that theorem.

Setting

Let $g:\mathbb R^m\to\mathbb R\cup\{+\infty\}$ be proper and lower semicontinuous, let $h:\mathbb R^n\to\mathbb R$ be differentiable with $L$ -Lipschitz gradient, and let $A:\mathbb R^n\to\mathbb R^m$ be linear. The augmented Lagrangian with parameter $r>0$ is

L_r(x,z,y)=g(z)+h(x)+\langle y,Ax-z\rangle+\tfrac r2\|Ax-z\|^2 .

Let $M_1^k$ and $M_2^k$ be symmetric positive semidefinite matrices, and write $\|v\|_M^2=\langle Mv,v\rangle$ . Fix $0<\rho<2$ . From an arbitrary starting point $(x^0,z^0,y^0)$ , Algorithm 1 generates

$z^{k+1}\in\arg\min_z\{g(z)+\langle y^k,Ax^k-z\rangle+\frac r2\|Ax^k-z\|^2+\frac12\|z-z^k\|^2_{M_2^k}\}$ ,
$x^{k+1}\in\arg\min_x\{h(x)+\langle y^k,Ax-z^{k+1}\rangle+\frac r2\|Ax-z^{k+1}\|^2+\frac12\|x-x^k\|^2_{M_1^k}\}$ ,
$y^{k+1}=y^k+\rho r(Ax^{k+1}-z^{k+1})$ .

Algorithm 2 is the same, except that $h(x)$ in the $x$ -update is replaced by its linearization $\langle x-x^k,\nabla h(x^k)\rangle$ . Assumption 1 asks for four things:

$g$ and $h$ are bounded below;
$A$ is surjective;
$\mu_i=\sup_k\|M_i^k\|<\infty$ ;
$r\ge4T_0L>0$ and $2M_1^k+rA^*A\succeq(L+C_M/r)\mathrm{Id}$ , where $T_0$ and $C_M$ are explicit in $\rho$ , $L$ , $\mu_1$ and $\lambda_{\min}(AA^*)$ .

With the constants $T_1$ and $C_1$ of §2.2 of the paper, the regularized augmented Lagrangian is

F_r(x,z,y,x',y')=L_r(x,z,y)+T_1\|A^*(y-y')\|^2+\tfrac{C_1}2\|x-x'\|^2 .

A KKT point of the problem is a triple $(\hat x,\hat z,\hat y)$ with $-A^*\hat y=\nabla h(\hat x)$ , $\hat y\in\partial g(\hat z)$ and $\hat z=A\hat x$ , where $\partial$ is the limiting subdifferential. A proper lower semicontinuous $\Psi$ is a KŁ function if, near every point of $\operatorname{dom}\partial\Psi$ , a concave desingularizing function $\varphi$ satisfies $\varphi'(\Psi(u)-\Psi(\hat u))\operatorname{dist}(0,\partial\Psi(u))\ge1$ .

Formalization targets

Goal: Theorem 14

Under Assumption 1, let $\{(x^k,z^k,y^k)\}$ be a bounded sequence generated by Algorithm 1 or Algorithm 2. If $F_r$ is a KŁ function, then

\sum_{k\ge0}\|x^{k+1}-x^k\|<\infty,\quad\sum_{k\ge0}\|z^{k+1}-z^k\|<\infty,\quad\sum_{k\ge0}\|y^{k+1}-y^k\|<\infty,

and $(x^k,z^k,y^k)\to(\hat x,\hat z,\hat y)$ for some KKT point $(\hat x,\hat z,\hat y)$ .

Milestones

The milestones follow the order in which the paper's proof uses them:

the descent lemma (Remark 1, already proved on the platform);
the monotonicity inequality for $L_r+T_1\|A^*\Delta y\|^2$ (Lemma 4);
the increment estimates (Lemma 5);
the Lyapunov property and convergence of $F_k$ (Theorem 7);
explicit subgradients of $L_r$ and $F_r$ with bounds (Lemma 8, Lemma 9, Corollary 10);
the limit-set properties (Lemmas 11 and 12);
the uniformized KŁ property (Lemma 13, shared with the PALM mission);
a summability lemma for three-step recursions (Lemma 3).

Theorem 6, the boundedness of the iterates under coercivity, is included as a supporting item that discharges the boundedness hypothesis.

Significance

The theorem gives global convergence of the whole sequence, not just subsequences, for a broad family of nonconvex splitting methods. The family includes full-splitting variants, in which $M_1^k=t_k\mathrm{Id}-rA^*A$ makes the $x$ -update explicit. The KŁ hypothesis on $F_r$ holds, for example, whenever $g$ and $h$ are semi-algebraic. The finite length conclusion is also the starting point for the rates of Section 3 of the paper, which are the subject of the companion mission.

The paper result is proved; this mission formalizes the known proof. As far as the platform records go, no machine-checked proof of convergence of a nonconvex ADMM exists. The Li–Pong ADMM theorems on the platform are open statements about a different algorithm. A completed development would supply the following reusable pieces:

the Lyapunov analysis of a variable-metric ADMM with relaxed dual step;
subdifferential calculus for an augmented Lagrangian on a product space;
a second instance of the generic KŁ finite-length argument.

Difficulty

The obvious Lyapunov candidate, $L_r$ itself, does not decrease along the iterates: the dual step increases it by $\frac1{\rho r}\|y^{k+1}-y^k\|^2$ . That increase has to be paid for by primal progress, and this is possible only because surjectivity of $A$ lets the dual increment be controlled by $x$ -increments over two consecutive steps. This is where the specific constants $T_0$ , $T_1$ , $C_1$ and the coupling condition (15) come from. The KŁ argument must therefore be run on the lifted function $F_r$ in five variables, whose subgradient bound (Corollary 10) involves three past increments and two telescoping terms. The textbook one-step KŁ argument therefore does not apply directly, and the recursion has to be closed with the three-step summability Lemma 3. For $\rho\ne1$ the dual update is relaxed, and the estimates must handle $|1-\rho|$ in both regimes $\rho<1$ and $\rho>1$ .

Formalization scope

Spaces are EuclideanSpace ℝ (Fin n), and products such as $\mathbb R^n\times\mathbb R^m\times\mathbb R^m$ and the 5-fold domain of $F_r$ are nested WithLp 2 products. Their norm is the Euclidean product norm the paper uses, not the sup norm. The function $g$ and the functions $L_r$ , $F_r$ take values in EReal. The data are bundled in a structure Data, and the algorithm is a parameter Variant (prox for Algorithm 1, linearized for Algorithm 2), so every statement covers both algorithms. A run is a relation: any minimizer may be selected at each step, and existence of minimizers is not claimed. $\lambda_{\min}(AA^*)$ and $\mu_1,\mu_2$ are replaced by parameters with the inequalities the proofs use ( $\mathrm{lam}\,\|y\|^2\le\|A^*y\|^2$ with $\mathrm{lam}>0$ , and $\|M_i^k\|\le\mu_i$ ). The paper's statements are the instance $\mathrm{lam}=\lambda_{\min}(AA^*)$ , $\mu_i=\sup_k\|M_i^k\|$ . The subdifferential is the published limiting subdifferential, and "KŁ function" is the published IsKLFunction. In that definition, $\operatorname{dist}(0,\partial\Psi(u))$ is read as a bound for every subgradient, so $\operatorname{dist}(0,\emptyset)=+\infty$ . Corrections read past: the paper indexes $\{F_k\}_{k\ge0}$ although $F_k$ exists only for $k\ge1$ , and it writes "defined in Assumption 1" for $T_1$ and $C_1$ , which are defined on p. 10.

There are three ways to formalize the statement trivially, and all are excluded:

a run predicate that no sequence satisfies, or a junk value making $T_0=0$ so that Assumption 1 cannot hold (a sorry-free check shows that Assumption 1 and the run relation are jointly satisfiable for both algorithms);
a KŁ hypothesis on an arbitrary function: the hypothesis is on the specific $F_r$ built from $T_1$ and $C_1$ ;
the weaker conclusion " $\hat x$ is stationary": the conclusion is the full KKT triple.

Contributions are welcome at every milestone. Lemma 3 and the subdifferential calculus behind Lemmas 8–9 are independent of the algorithm, and are good entry points.

Selected references

R. I. Boţ, D.-K. Nguyen, The proximal alternating direction method of multipliers in the nonconvex setting: convergence analysis and rates, arXiv:1801.01994v2, 2020; Math. Oper. Res. 45(2), 2020. https://arxiv.org/abs/1801.01994, https://doi.org/10.1287/moor.2019.1008
J. Bolte, S. Sabach, M. Teboulle, Proximal alternating linearized minimization for nonconvex and nonsmooth problems, Math. Program. 146, 2014. https://doi.org/10.1007/s10107-013-0701-9
H. Attouch, J. Bolte, B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137, 2013. https://doi.org/10.1007/s10107-011-0484-9
G. Li, T. K. Pong, Global convergence of splitting methods for nonconvex composite optimization, SIAM J. Optim. 25(4), 2015. https://doi.org/10.1137/140998135
M. Hong, Z.-Q. Luo, M. Razaviyayn, Convergence analysis of alternating direction method of multipliers for a family of nonconvex problems, SIAM J. Optim. 26(1), 2016. https://doi.org/10.1137/140990309

16 thms2 active usersReviewed

Completed

Optimization Statistics·Captain: mikedeng1

Fast Best Subset Selection: Coordinate Descent and Local Combinatorial Optimization Algorithms II: CD-PSI(k) Terminates Finitely at a Partial Swap Inescapable Minimum of Order kResearch Paper

Motivation

Best subset selection asks for the linear model that fits a response with as few predictors as possible. It is a basic problem of statistics and a standard test case for mixed-integer optimization. The penalized form

\min_{\beta\in\mathbb R^p}\ \tfrac12\|y-X\beta\|^2+\lambda_0\|\beta\|_0

is NP-hard in general. Exact mixed-integer methods (Bertsimas, King, Mazumder 2016) certify global optimality but scale to moderate $p$ only. Hazimeh and Mazumder (arXiv:1803.01454, Operations Research 2020) proposed a hierarchy of local minima for the $L_0$ -penalized problem, together with algorithms that reach each class. These are coordinate descent for coordinate-wise minima, and coordinate descent combined with small combinatorial swap searches for the finer swap inescapable minima. The software built on these algorithms, L0Learn, runs on problems with $p$ in the millions.

The companion mission (part I) proves that the coordinate descent stage converges. This mission proves the guarantee of the second stage: the local combinatorial search stops after finitely many rounds, and it stops at a partial swap inescapable minimum.

Setting

Data and objective. Let $X\in\mathbb R^{n\times p}$ have columns $X_1,\dots,X_p$ of unit Euclidean norm, let $y\in\mathbb R^n$ , and let $\lambda_0>0$ , $\lambda_1,\lambda_2\ge0$ . Problem (2) is

\min_{\beta\in\mathbb R^p}F(\beta)=f(\beta)+\lambda_0\|\beta\|_0,\qquad f(\beta)=\tfrac12\|y-X\beta\|^2+\lambda_1\|\beta\|_1+\lambda_2\|\beta\|_2^2,

where $\|\beta\|_0$ is the number of nonzero entries. The paper names three cases: (L0), with $\lambda_1=\lambda_2=0$ ; (L0L1), with $\lambda_1>0=\lambda_2$ ; and (L0L2), with $\lambda_1=0<\lambda_2$ . $\operatorname{Supp}(\beta)=\{i:\beta_i\neq0\}$ , and $U_S\beta$ keeps the entries of $\beta$ in $S$ and zeroes the others.

Classes of minima. A stationary solution has nonnegative lower directional derivative $F'(\beta;d)=\liminf_{\alpha\downarrow0}(F(\beta+\alpha d)-F(\beta))/\alpha$ in every direction $d$ . A CW minimum is a point where each coordinate $\beta_i$ minimizes $F$ with the other coordinates held fixed. For a positive integer $k$ , a PSI( $k$ ) minimum is a stationary $\beta^*$ with support $S$ such that, for all $S_1\subseteq S$ and $S_2\subseteq S^c$ with $|S_1|,|S_2|\le k$ ,

F(\beta^*)\le\min_{\beta_{S_2}}F\big(\beta^*-U_{S_1}\beta^*+U_{S_2}\beta\big).

In words, dropping at most $k$ active coordinates, adding at most $k$ new ones and optimizing only over the added ones never lowers the objective.

Algorithm 1 (CDSS) is cyclic coordinate descent. Each step sets one coordinate to the minimizer given by the thresholding operator $T$ of (12). Every time a support has been visited $Cp$ times, the algorithm also performs a spacer step: one pass of coordinate descent on $f$ restricted to that support.

Algorithm 2 (CD-PSI( $k$ )) alternates two steps. It runs Algorithm 1 from $\hat\beta^\ell$ to obtain $\beta^{\ell+1}$ . It then searches the swap problem (14),

\min_{\beta,S_1,S_2}F\big(\beta^{\ell+1}-U_{S_1}\beta^{\ell+1}+U_{S_2}\beta\big)\ \ \text{s.t.}\ \ S_1\subseteq S,\ S_2\subseteq S^c,\ |S_1|,|S_2|\le k,

with $S=\operatorname{Supp}(\beta^{\ell+1})$ , for a feasible $\hat\beta$ with $F(\hat\beta)<F(\beta^{\ell+1})$ . If it finds one, it sets $\hat\beta^{\ell+1}=\hat\beta$ and continues; otherwise it terminates.

Formalization targets

Goal: Theorem 4

Assume the (L0), (L0L1) or (L0L2) setting. For (L0) and (L0L1), assume also that every $\min\{n,p\}$ columns of $X$ are linearly independent (Assumption 1) and, when $p>n$ , that the start $\beta^0$ satisfies the objective bound of Assumption 2. Then every run of CD-PSI( $k$ ) satisfies

\exists L:\quad \text{(14) is improving at }\beta^1,\dots,\beta^L,\quad \text{(14) is not improving at }\beta^{L+1},\quad \beta^{L+1}\in\mathrm{PSI}(k).

No bound on $L$ is part of the goal, and the paper states none.

Milestones

Theorem 2 (p. 12): the iterates of Algorithm 1 have eventually constant support and converge to a CW minimum with that support. This is the goal of the companion mission, restated here on this mission's definitions.
Lemma 3 (p. 7): CW minima are characterized by the thresholding conditions (8).
Lemma 1 (p. 6): $\beta$ is stationary iff $\nabla_{\operatorname{Supp}(\beta)}f(\beta)=0$ .
§A.8, p. 44, same objective: a CW minimum minimizes $f$ over the vectors supported in its support, so two CW minima with the same support have the same $F$ .
§A.8, p. 44, distinct supports: along a run that has not yet terminated, $F(\beta^{\ell})$ strictly decreases and no support repeats.

Significance

The result. Theorem 4 makes CD-PSI( $k$ ) an algorithm with a guarantee. It always stops, and its output satisfies an optimality condition that is strictly stronger than coordinate-wise optimality: the hierarchy (4) of the paper places PSI( $k$ ) minima inside CW minima, and for large $k$ they coincide with global minimizers. The same termination argument underlies the full-optimization variant (FSI minima) and the swap heuristics of L0Learn, which the paper treats "by the same argument".

Formalizing it. The theorem is proved on paper, in a short argument in Appendix A.8 that rests on the convergence of Algorithm 1 (Theorem 2, the companion mission). No part of it has been machine-checked. This mission produces checked definitions of PSI minima, of the swap problem and of the two-level algorithm; a formal proof of the finite termination; and the bridge lemmas between CW minima, stationarity and the restricted least-squares problem, which any formal treatment of $L_0$ -penalized regression needs.

Difficulty

The obvious argument is that each round lowers the objective, there are finitely many supports, so the algorithm stops. A strict decrease of $F$ alone gives no finiteness: a real-valued sequence can decrease forever. What makes the argument work is that the value of $F$ at an output of Algorithm 1 depends only on its support. That needs every output to be a CW minimum, which is Theorem 2, a nontrivial convergence theorem for a discontinuous objective. It also needs every CW minimum to minimize the convex function $f$ over its support, which uses the characterization (8) and convexity.

A second difficulty is bookkeeping. Algorithm 1 never stops ("while not converged"), so its output is a limit. Each call of Algorithm 1 inside Algorithm 2 must satisfy the hypotheses of Theorem 2, in particular Assumption 2 for the new starting point, and that holds only because the objective has decreased since $\beta^0$ .

Formalization scope

Vectors are Fin p → ℝ, so indices are $0$ -based. All norms are explicit sums, never Lean's sup norm. $\operatorname{sign}$ is Real.sign, with $\operatorname{sign}(0)=0$ . The lower directional derivative is EReal-valued. The theorems are stated for the three named problems, via the hypothesis $\lambda_1=0\lor\lambda_2=0$ . Assumptions 1–2 are required only when $\lambda_2=0$ .

Algorithm 1 is a deterministic state machine with a cyclic pointer, a table $\mathrm{Count}$ and a pending-spacer flag, following the box on p. 11. A run of Algorithm 2 is a pair of sequences: $\beta^{\ell+1}$ is the limit of the CDSS iterates from $\hat\beta^\ell$ , and $\hat\beta^{\ell+1}$ is any improving feasible point of (14), required only while the run has not terminated. The predicate is not vacuous: on the instance $n=p=1$ , $X=y=1$ , $\lambda_0=1/4$ , $\lambda_1=\lambda_2=0$ , $C=k=1$ , $\beta^0=0$ , a run exists and terminates at $\ell=0$ . " $\le\min_{\beta_{S_2}}$ " in Definition 3 is read as " $\le$ every value".

A statement that assumes the outputs of Algorithm 1 are CW minima, or that the run terminates, or that only finitely many supports are visited, would trivialize the goal. All three are conclusions of the mission, not hypotheses.

The development needs the CDSS model shared with the companion mission, convexity of the restricted least-squares objective and a finiteness argument over Finset (Fin p). The definitions of Problem (2), Algorithm 1 and the stationarity notions are reusable for any later mission on $L_0$ -penalized regression. Proofs of the milestones independently of the goal are welcome; Theorem 2 can also be imported once the companion mission proves it. Theorem and page numbers are those of arXiv:1803.01454v3.

Selected references

H. Hazimeh, R. Mazumder, Fast Best Subset Selection: Coordinate Descent and Local Combinatorial Optimization Algorithms, Operations Research 68(5), 2020. arXiv:1803.01454v3. https://arxiv.org/abs/1803.01454 , https://doi.org/10.1287/opre.2019.1919
D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
A. Beck, Y. C. Eldar, Sparsity Constrained Nonlinear Optimization: Optimality Conditions and Algorithms, SIAM J. Optim. 23(3), 2013. https://doi.org/10.1137/120869778

8 thms2 active usersReviewed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Stochastic Dual Coordinate Ascent Methods for Regularized Loss Minimization 3: Under Refined Dual Strong Convexity, SDCA Reaches Expected Dual Sub-optimality ε after 2(n/s)·log(2/ε) IterationsResearch Paper

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

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).
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$ .
Lemma 3 (p. 15): the conjugate of an $L$ -Lipschitz function is $+\infty$ outside $[-L,L]$ .
Lemma 6 (p. 20): $G_*(s)\le4L^2N(s/(\lambda n))/n$ .
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$ .
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

13 thms2 active usersReviewed

Completed

Numerical Analysis Optimization·Captain: mikedeng1

Proximal Gradient Method for Nonsmooth Optimization over the Stiefel Manifold: Every Limit Point of ManPG Is Stationary, and an ε-Stationary Point Is Reached Within ⌈2L(F(X₀)−F*)/(γᾱε²)⌉ IterationsResearch Paper

Motivation

Many problems in statistics and signal processing ask for an orthonormal frame $X\in\mathbb R^{n\times r}$ that is both a good fit to the data and sparse or otherwise structured. Sparse principal component analysis, compressed modes in physics, unsupervised feature selection and sparse blind deconvolution all take the form

\min_{X}\ F(X)=f(X)+h(X)\quad\text{s.t.}\quad X^\top X=I_r,

with $f$ smooth and $h$ convex but nonsmooth, typically an $\ell_1$ penalty. Before the work of Chen, Ma, So and Zhang, algorithms for this class fell into three groups: subgradient-oriented methods, which solve a quadratic program over sampled subgradients in every step; proximal point algorithms, whose subproblems are as hard as the original problem; and operator-splitting methods such as SOC and MADMM. The manifold proximal gradient method (ManPG) carries the Euclidean proximal gradient method over to the Stiefel manifold. The paper shows that ManPG keeps the global convergence and the $O(\varepsilon^{-2})$ iteration complexity that Riemannian gradient descent has for smooth objectives (Boumal, Absil and Cartis, 2019).

Setting

The feasible set is the Stiefel manifold

\mathcal M=\mathrm{St}(n,r)=\{X\in\mathbb R^{n\times r}: X^\top X=I_r\},\qquad r\le n.

The ambient space $\mathbb R^{n\times r}$ carries the Frobenius inner product $\langle A,B\rangle=\operatorname{Tr}(A^\top B)$ and norm $\|A\|_F$ . The tangent space at $X\in\mathcal M$ is $T_X\mathcal M=\{V: V^\top X+X^\top V=0\}$ . The orthogonal projection onto it is $\operatorname{Proj}_{T_X\mathcal M}(Y)=(I_n-XX^\top)Y+\tfrac12X(X^\top Y-Y^\top X)$ .

The standing assumptions on $F=f+h$ are imposed on all of $\mathbb R^{n\times r}$ :

(i) $f$ is differentiable, and its gradient $\nabla f$ is $L$ -Lipschitz;
(ii) $h$ is convex and $L_h$ -Lipschitz.

A point $X\in\mathcal M$ is stationary (Definition 3.3) if

0\in\operatorname{grad}f(X)+\operatorname{Proj}_{T_X\mathcal M}\partial h(X),\qquad \operatorname{grad}f(X)=\operatorname{Proj}_{T_X\mathcal M}\nabla f(X),

where $\partial h$ is the convex subdifferential.

A retraction $\mathrm{Retr}_X(\xi)$ maps tangent vectors at $X$ back to $\mathcal M$ , with $\mathrm{Retr}_X(0)=X$ . On the compact manifold $\mathcal M$ every retraction satisfies, for some $M_1,M_2>0$ and all $X\in\mathcal M$ , $\xi\in T_X\mathcal M$ (Fact 3.6),

\|\mathrm{Retr}_X(\xi)-X\|_F\le M_1\|\xi\|_F,\qquad \|\mathrm{Retr}_X(\xi)-(X+\xi)\|_F\le M_2\|\xi\|_F^2.

ManPG (Algorithm 1) takes $X_0\in\mathcal M$ , $\gamma\in(0,1)$ and $t>0$ . In iteration $k$ it solves the convex subproblem

V_k=\operatorname*{argmin}_{V\in T_{X_k}\mathcal M}\ \langle\nabla f(X_k),V\rangle+\frac1{2t}\|V\|_F^2+h(X_k+V).\tag{4.3}

It then backtracks $\alpha=1,\gamma,\gamma^2,\dots$ until $F(\mathrm{Retr}_{X_k}(\alpha V_k))\le F(X_k)-\alpha\|V_k\|_F^2/(2t)$ , and sets $X_{k+1}=\mathrm{Retr}_{X_k}(\alpha_kV_k)$ .

A point $X\in\mathcal M$ is $\varepsilon$ -stationary (Definition 5.4) if the solution of (4.3) at $X$ with $t=1/L$ has $\|V\|_F\le\varepsilon/L$ . The proof of Lemma 5.2 uses a bound $G$ on $\|\nabla f\|_F$ over $\mathcal M$ and the constants

c_0=M_2G+\frac{LM_1^2}{2},\qquad \bar\alpha=\frac{1}{2(c_0+L_hM_2)t}.

Formalization targets

Goal: Theorem 5.5

For every run of ManPG:

every limit point $\bar X$ of $\{X_k\}$ is stationary;
with $t=1/L$ , for every $\varepsilon>0$ some

k\le\left\lceil\frac{2L\,(F(X_0)-F^*)}{\gamma\bar\alpha\varepsilon^2}\right\rceil

has $\|V_k\|_F\le\varepsilon/L$ and $X_k$ is $\varepsilon$ -stationary.

Here $F^*$ is the optimal value of (1.1). The constant is the paper's, kept exactly.

Milestones, in the order the proof uses them

Lemma 5.1: $g(\alpha V_k)-g(0)\le\frac{(\alpha-2)\alpha}{2t}\|V_k\|_F^2$ for $\alpha\in[0,1]$ , where $g$ is the objective of (4.3).
(5.5): $f(\mathrm{Retr}_{X}(\alpha V))-f(X)\le\alpha\langle\nabla f(X),V\rangle+c_0\alpha^2\|V\|_F^2$ .
Lemma 5.2, split into three parts:
- sufficient decrease for every $0<\alpha\le\min\{1,\bar\alpha\}$ ;
- well-definedness of the line search: a run exists from every $X_0$ ;
- the run form $\gamma\min\{1,\bar\alpha\}\le\alpha_k\le1$ , with $F(X_{k+1})-F(X_k)\le-\frac{\alpha_k}{2t}\|V_k\|_F^2$ .
Lemma 5.3: $V_k=0$ implies $X_k$ is stationary.
Two displays of the proof of Theorem 5.5:
- $\|V_k\|_F^2\to0$ ;
- the telescoped chain $F(X_0)-F^*>\frac{tK\varepsilon^2}{2}\gamma\bar\alpha$ when $\|V_k\|_F>\varepsilon/L$ for all $k<K$ .

Significance

Theorem 5.5 is the paper's main result. It certifies ManPG as a first-order method for nonsmooth problems on the Stiefel manifold with the same $O(\varepsilon^{-2})$ complexity as Riemannian gradient descent in the smooth case. When $h=0$ the bound reduces to the Boumal–Absil–Cartis rate (Remark 5.6). Later proximal methods on matrix manifolds build on this analysis. Lemmas 5.1–5.3 are the reusable steps: descent of the subproblem, sufficient decrease after retraction, and the stopping test as a stationarity certificate.

The result is proved in the paper; it is not formalized anywhere. No proof assistant library contains the convergence theory of a proximal method on a matrix manifold. The mission produces a machine-checked version of the full chain from the subproblem to the iteration bound. Along the way it builds infrastructure that Mathlib lacks: the Frobenius geometry of $\mathbb R^{n\times r}$ as a trace formula, the tangent space and projection of the Stiefel manifold, and optimality conditions for convex problems restricted to a subspace.

Difficulty

The bookkeeping inequalities (Lemma 5.1, (5.5), the decrease estimate, the telescoping) are short computations once the right facts are available. The difficulty lies elsewhere.

Lemma 5.3 and the limit-point claim need the optimality condition of the subproblem (4.3): a subdifferential sum rule for a convex function restricted to the linear subspace $T_X\mathcal M$ , followed by the projection formula. The paper cites this condition rather than proving it.
The limit-point claim also needs a closedness argument. Subgradients of the Lipschitz function $h$ are bounded by $L_h$ , so along a convergent subsequence they have a limit point that is again a subgradient. The projection $X\mapsto\operatorname{Proj}_{T_X\mathcal M}$ must be shown continuous. The paper's proof leaves both steps implicit.
The well-definedness of the line search requires existence of a minimizer of (4.3), by strong convexity and coercivity on a subspace.
The descent lemma for $f$ has to be derived from the derivative along lines and the Lipschitz gradient.

A natural first idea is to restate everything for the Riemannian gradient and reuse smooth Riemannian results. That route does not work: $h$ is nonsmooth, and the argument runs in the ambient space through the Euclidean subdifferential.

Formalization scope

Representation.
- Matrices are Matrix (Fin n) (Fin r) ℝ.
- The inner product is trace (Aᵀ * B) and the norm is its square root. No Mathlib matrix norm instance is used.
- $\mathrm{St}(n,r)$ is the published definition ProjLikeRetr.Stiefel.stiefel.
Assumptions.
- $f$ comes with a gradient map gradf, tied to it by derivatives along every line.
- $\nabla f$ is $L$ -Lipschitz in the Frobenius norm, with $L>0$ .
- $h$ is convex and $L_h$ -Lipschitz on the whole ambient space.
- $r\le n$ .
Retraction. The retraction is any map sending tangent vectors at points of $\mathcal M$ into $\mathcal M$ , with $\mathrm{Retr}_X(0)=X$ and the bounds (3.1)–(3.2). By Fact 3.6 this covers every retraction; smoothness is never used.
Constants.
- $G$ , $M_1$ , $M_2$ , $L$ , $L_h$ are parameters, each with its defining hypothesis.
- $c_0$ and $\bar\alpha$ are the explicit formulas above.
- $F^*$ is an attained lower bound of $F$ on $\mathcal M$ .
The run. A run of Algorithm 1 is a predicate on sequences $(X_k,V_k,\alpha_k)$ . Each $V_k$ minimizes (4.3), $\alpha_k=\gamma^j$ for the least passing $j$ , and $X_{k+1}=\mathrm{Retr}_{X_k}(\alpha_kV_k)$ .
The goal's conventions.
- A limit point is a cluster point of the sequence.
- "Returns an $\varepsilon$ -stationary point within $N$ iterations" means some $k\le N$ passes the stopping test $\|V_k\|_F\le\varepsilon/L$ , with $N=\lceil\cdot\rceil$ as Nat.ceil.

Two encodings would trivialize the theorem, and the mission excludes both.

An unsatisfiable run predicate would make the goal vacuous. The well-definedness milestone asserts that a run exists from every $X_0\in\mathcal M$ .
A projection or stationarity condition that holds trivially would make the first claim empty. Stationarity uses the explicit projection formula and the convex subdifferential on all of $\mathbb R^{n\times r}$ .

Lemma 5.2 as printed fixes $\alpha\le\min\{1,\bar\alpha\}$ and asserts the decrease for the accepted iterate. What its proof establishes is three separate facts: decrease at every trial stepsize $\alpha\le\min\{1,\bar\alpha\}$ , termination of the line search, and $\alpha_k\ge\gamma\min\{1,\bar\alpha\}$ along a run. The mission states these three facts.

Contributions are welcome at every level: proofs of the milestones, and general lemmas such as the descent lemma for $C^{1,1}$ functions on $\mathbb R^{n\times r}$ , the optimality condition of a strongly convex problem on a subspace, and properties of the Stiefel tangent projection. Theorem numbers and pages refer to arXiv:1811.00980v2, the version read for this mission.

Selected references

S. Chen, S. Ma, A. M.-C. So, T. Zhang, Proximal gradient method for nonsmooth optimization over the Stiefel manifold, SIAM Journal on Optimization 30(1), 2020. https://doi.org/10.1137/18m122457x (arXiv:1811.00980v2: https://arxiv.org/abs/1811.00980)
N. Boumal, P.-A. Absil, C. Cartis, Global rates of convergence for nonconvex optimization on manifolds, IMA Journal of Numerical Analysis 39(1), 2019. https://doi.org/10.1093/imanum/drx080
P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244

12 thms2 active usersReviewed

Machine Learning Optimal Transport Probability+1·Captain: mikedeng1

Minimax Statistical Learning with Wasserstein Distances I: Data-Dependent High-Probability Bound on the Local Worst-Case RiskResearch Paper

Motivation

Training data describe one probability distribution, while a deployed prediction rule may be evaluated under a nearby distribution. Distributionally robust learning measures a rule by its worst expected loss over a specified set of nearby laws. This changes the question from how well the rule fits the observed sample to how well it performs when probability mass can move. Wasserstein distance supplies a geometric notion of “nearby”: moving mass farther across the instance space costs more. The setting is relevant to the domain drift discussed by Lee and Raginsky and to Wasserstein robust optimization as developed by Mohajerin Esfahani and Kuhn.

Theorem 1 of Lee and Raginsky's 2018 paper gives a finite-sample answer. It controls the local worst-case risk at the true population law using quantities computed from the empirical law, and also controls the empirical local worst-case risk using population quantities. Both assertions are simultaneous over the entire loss class. This mission concerns exactly those two probability inequalities and the displayed claims in Appendix C.1 that support them. The source is the pinned arXiv:1705.07815v2 preprint, containing the NeurIPS 2018 paper and its supplementary appendix.

Setting

The instance space $\mathcal Z$ is a bounded Polish metric space with distance $d_{\mathcal Z}$ . A probability measure $P$ generates $n\ge1$ independent observations $Z_1,\ldots,Z_n$ . Their empirical distribution is $P_n=n^{-1}\sum_{i=1}^n\delta_{Z_i}$ . A loss $f:\mathcal Z\to\mathbb R$ has risk $R(Q,f)=\int f\,dQ$ under a probability law $Q$ . The class $\mathcal F$ consists of upper semicontinuous losses satisfying $0\le f(z)\le M$ for every $f\in\mathcal F$ and $z\in\mathcal Z$ , as in Assumption 2 of the paper.

For $p\ge1$ , the $p$ -Wasserstein distance $W_p(Q,P)$ is the least $p$ th-power transport cost over couplings of $Q$ and $P$ , raised to the power $1/p$ . The Wasserstein ball $B^W_{\varrho,p}(P)$ consists of probability laws $Q$ with $W_p(Q,P)\le\varrho$ , where $\varrho>0$ . The local worst-case risk is

R_{\varrho,p}(P,f)=\sup_{Q\in B^W_{\varrho,p}(P)}R(Q,f).

The dual expression uses the envelope $\varphi_{\lambda,f}(z)=\sup_{z'\in\mathcal Z}\{f(z')-\lambda d_{\mathcal Z}(z,z')^p\}$ for $\lambda\ge0$ . To measure the size of $\mathcal F$ , let $\mathcal N(\mathcal F,\|\cdot\|_\infty,u)$ be its uniform-metric covering number at radius $u$ . The entropy integral is $\mathfrak C(\mathcal F)=\int_0^\infty\sqrt{\log\mathcal N(\mathcal F,\|\cdot\|_\infty,u)}\,du$ . These symbols match the local Lean setting and the source's notation.

Formalization targets

Theorem 1: two data-dependent risk bounds

For every $t>0$ , the mission goal is the conjunction of the paper's two displays:

\mathbb P\!\left\{\exists f\in\mathcal F:\ R_{\varrho,p}(P,f)>\inf_{\lambda\ge0}\left[(\lambda+1)\varrho^p+\mathbb E_{P_n}\varphi_{\lambda,f}+\frac{M\sqrt{\log(\lambda+1)}}{\sqrt n}\right]+\frac{24\mathfrak C(\mathcal F)+Mt}{\sqrt n}\right\}\le 2e^{-2t^2},

\mathbb P\!\left\{\exists f\in\mathcal F:\ R_{\varrho,p}(P_n,f)>\inf_{\lambda\ge0}\left[(\lambda+1)\varrho^p+\mathbb E_P\varphi_{\lambda,f}+\frac{M\sqrt{\log(\lambda+1)}}{\sqrt n}\right]+\frac{24\mathfrak C(\mathcal F)+Mt}{\sqrt n}\right\}\le 2e^{-2t^2}.

The seven milestones preserve displayed claims from Appendix C.1: the deterministic comparison through the supremum deviation $X_\lambda$ , its concentration and symmetrization bounds, the entropy-integral estimate with constant $24$ , the fixed- $\lambda$ probability bound, and the integer-grid union and comparison with real multipliers. They are statements from the author's argument, ordered by their appearance. The goal retains both directions of the published theorem and every printed constant.

Significance

The first bound provides a sample-dependent certificate for the worst-case population loss of every member of $\mathcal F$ at once. The second compares the robust empirical quantity with a population envelope. Together they make it possible to assess what a local Wasserstein ambiguity set buys in finite samples, rather than relying only on asymptotic convergence. The complexity term depends on the geometry of the loss class through its covering numbers, following a line of empirical-process bounds also seen in Bartlett and Mendelson's study of Rademacher complexity. Lee and Raginsky emphasize that this class complexity can reflect hypotheses outside the support of the data-generating law.

The mathematical theorem is proved in the 2018 paper; the particular declarations in this mission remain open Lean goals. A complete formal development would connect probability inequalities for supremum processes to the published Wasserstein distance and ball, make the entropy integral and its measurability consequences explicit, and verify both directions of the final bound. The reusable output includes a precise internal uniform covering number and a finite-sample Rademacher process for metric-space loss classes.

Difficulty

A fixed multiplier $\lambda$ is easier to control than the infimum over all $\lambda\ge0$ . A pointwise concentration bound alone does not produce a simultaneous statement over an uncountable multiplier set. The source's final formula contains a logarithmic multiplier penalty, and retaining its coefficient $M$ and the probability factor $2$ requires accounting for that parameter range exactly. Independently, the supremum over an arbitrary loss class is a genuine random variable only with enough regularity. The boundedness of individual losses does not by itself settle the measurability of their unrestricted supremum.

The envelope $\varphi_{\lambda,f}$ also mixes the metric geometry with empirical-process complexity. Estimating a class of envelopes must remain tied to the covering properties of the original class $\mathcal F$ . Replacing the envelope class by a finite hand-picked subclass or assuming the desired concentration inequality as a new hypothesis would change the theorem being formalized.

Formalization scope

Lean uses a metric space with its Borel measurable structure and a Polish-space instance, together with boundedness of the whole carrier. The Wasserstein distance and ball are imported from the published WassersteinLinOpt.Ball definitions. Because the carrier is bounded, every probability measure has a finite $p$ th moment, matching the source's $\mathcal P_p(\mathcal Z)$ . The ball is a subtype of probability measures; its supremum is taken only over feasible laws. Sample outcomes are functions Fin n → 𝒵, and the product measure gives their independent common law. The empirical law is a normalized finite sum of Dirac masses, while $\mathbb E_{P_n}$ is written as its equal finite average.

The paper does not specify whether covering centres must lie in $\mathcal F$ . This formalization uses the internal covering number, whose centres do; its value is at least the external covering number. The entropy integral is extended nonnegative and is required to be finite in statements that convert it to a real number. This disclosed restriction avoids the default conversion of $+\infty$ to zero and supports the separability needed for expected suprema. Milestones using $X_\lambda$ also require $\mathcal F$ to be nonempty, so a real supremum never acquires the empty-family default value. The empty-class case of Theorem 1 remains valid because its failure events are empty.

The source writes minima over nonnegative real multipliers and positive integers. The Lean statements use bounded-below real infima; for the final bound, the appendix's comparison holds at every multiplier, so this reading is at least as strong as the printed minimum. All radii are positive, $p\ge1$ , $n\ge1$ , and $t>0$ where it appears. Failure probabilities use outer measure of the sample event directly, with no conversion through toReal. The goal never quantifies over arbitrary distributions outside the Wasserstein ball, and expectations of supremum processes are guarded by the finite-entropy hypothesis. Contributions are welcome on the concentration, symmetrization, covering-number, and transport-risk interfaces as well as the goal itself.

Selected references

Jaeho Lee and Maxim Raginsky, Minimax Statistical Learning with Wasserstein Distances, Advances in Neural Information Processing Systems 31, 2018. arXiv:1705.07815v2.
Peyman Mohajerin Esfahani and Daniel Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: Performance guarantees and tractable reformulations, Mathematical Programming 171, 2018. DOI:10.1007/s10107-017-1172-1.
Peter L. Bartlett and Shahar Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3, 2002. JMLR paper.

11 thms2 active usersReviewed

Optimization Statistics·Captain: mikedeng1

Fast Best Subset Selection: Coordinate Descent and Local Combinatorial Optimization Algorithms I: Cyclic Coordinate Descent with Spacer Steps Converges to a Coordinate-Wise MinimumResearch Paper

Motivation

Best subset selection asks for the linear model that fits a response best using only a few of many candidate predictors. In its penalized form it is the least-squares problem with an $L_0$ penalty, the number of nonzero coefficients. The problem is NP-hard. Mixed-integer optimization can solve it to certified optimality at moderate sizes (Bertsimas, King, Mazumder 2016), but statisticians who fit whole regularization paths with tens of thousands of predictors need something faster. Hazimeh and Mazumder (arXiv:1803.01454, Operations Research 2020) proposed cyclic coordinate descent for the $L_0$ -penalized problem, the method that glmnet made standard for the lasso. Their algorithm underlies the L0Learn software package.

Coordinate descent on a convex smooth-plus-separable objective converges by classical arguments (Tseng 2001). Those arguments do not cover the $L_0$ penalty, which is discontinuous. The paper adds occasional spacer steps to plain cyclic coordinate descent and proves that the modified algorithm converges to a coordinate-wise minimum. This mission formalizes that convergence theorem.

Setting

Let $X\in\mathbb R^{n\times p}$ be a model matrix whose columns $X_1,\dots,X_p$ have unit Euclidean norm, and let $y\in\mathbb R^n$ . For $\beta\in\mathbb R^p$ let

f(\beta)=\tfrac12\|y-X\beta\|^2+\lambda_1\|\beta\|_1+\lambda_2\|\beta\|_2^2,\qquad F(\beta)=f(\beta)+\lambda_0\|\beta\|_0,

with $\lambda_0>0$ and $\lambda_1,\lambda_2\ge0$ ; $\|\beta\|_0$ counts the nonzero coordinates. Problem (2) is $\min_\beta F(\beta)$ . Its three named cases are (L0) ( $\lambda_1=\lambda_2=0$ ), (L0L1) ( $\lambda_1>0=\lambda_2$ ) and (L0L2) ( $\lambda_1=0<\lambda_2$ ). $\mathrm{Supp}(\beta)=\{i:\beta_i\ne0\}$ .

Fix all coordinates but the $i$ -th. With unit-norm columns, minimizing $F$ over $\beta_i$ amounts to minimizing a scalar function of $\tilde\beta_i=\langle y-\sum_{j\ne i}X_j\beta_j,X_i\rangle$ . The minimizer set is $\tilde T(\tilde\beta_i,\lambda_0,\lambda_1,\lambda_2)$ (7). The thresholding operator $T$ (12) picks one element of it:

T(a,\lambda_0,\lambda_1,\lambda_2)=\mathrm{sign}(a)\frac{|a|-\lambda_1}{1+2\lambda_2}\ \text{ if }\ \frac{|a|-\lambda_1}{1+2\lambda_2}\ge\sqrt{\frac{2\lambda_0}{1+2\lambda_2}},\qquad 0\ \text{ otherwise.}

A coordinate-wise (CW) minimum is a $\beta$ such that every $\beta_i$ minimizes $F$ in coordinate $i$ with the others fixed (Definition 2). A stationary solution is a $\beta$ whose lower directional derivative $F'(\beta;d)=\liminf_{\alpha\downarrow0}(F(\beta+\alpha d)-F(\beta))/\alpha$ is nonnegative in every direction $d$ (Definition 1).

Algorithm 1 (CDSS) takes an initial point $\beta^0$ and a positive integer $C$ . It sweeps the coordinates cyclically. Each non-spacer step sets the current coordinate to $T(\tilde\beta_i,\lambda_0,\lambda_1,\lambda_2)$ and increments a counter for the resulting support. When the counter of a support $S$ reaches $Cp$ , a spacer step follows: one sequential pass over the coordinates of $S$ with the $L_0$ term switched off, $\beta_i\leftarrow T(\tilde\beta_i,0,\lambda_1,\lambda_2)$ . The counter of $S$ is then reset. The iterates $\beta^k$ count both kinds of step.

For (L0) and (L0L1) the paper adds Assumption 1: every $\min\{n,p\}$ columns of $X$ are linearly independent. It also adds Assumption 2, which constrains the initial point when $p>n$ : $F(\beta^0)\le\lambda_0 n$ for (L0), and $F(\beta^0)\le\min_\beta f(\beta)+\lambda_0 n$ for (L0L1).

Formalization targets

Goal: Theorem 2 (p. 12)

For (L0), (L0L1) and (L0L2), under Assumptions 1–2 in the first two cases, there are $m$ and a support $S$ with

\mathrm{Supp}(\beta^k)=S\ \ (k\ge m),\qquad \beta^k\to B,\qquad B\text{ a CW minimum},\qquad \mathrm{Supp}(B)=S .

The two parts share $S$ : the support stabilizes, and the limit is a CW minimum on that support.

Milestones

Lemma 5, monotone descent: $F(\beta^{k+1})\le F(\beta^k)$ and $F(\beta^k)\downarrow F^*\ge0$ .
Lemma 6: $\|\beta^k\|_0\le\min\{n,p\}$ for (L0), (L0L1).
Lemma 8: $\{\beta^k\}$ is bounded.
Lemma 1: stationarity is equivalent to $\nabla_S f(\beta)=0$ on the support $S$ .
Lemma 9: along a support $S$ recurring in non-spacer steps, the spacer iterates eventually keep support $S$ . Every subsequence with support $S$ converges to the unique minimizer $\beta^*$ of $f$ on $S$ , and $|\beta^*_j|\ge\sqrt{2\lambda_0/(1+2\lambda_2)}$ on $S$ .
Lemma 10: the support of every limit point occurs infinitely often.
Lemma 2: closed form of $\tilde T$ .
Lemma 11: for two limit points whose supports differ by one index $j$ , $|B^{(2)}_j|$ exceeds $\sqrt{2\lambda_0/(1+2\lambda_2)}$ , or equals it, according to whether $X_j$ is correlated with the smaller support.
Lemma 12: zeroing a nonzero coordinate decreases $F$ by at least $\frac{1+2\lambda_2}{2}\big(|\beta^k_j|-\sqrt{2\lambda_0/(1+2\lambda_2)}\big)^2$ .
Lemma 3: the coordinatewise characterization (8) of CW minima, with the condition $|\tilde\beta_i|>\lambda_1$ of (5) on the support (see Formalization scope).

Significance

Theorem 2 guarantees that exact cyclic coordinate descent on Problem (2), with spacer steps, has a limit, and that the limit is a CW minimum. That class is strictly smaller than the stationary solutions and the fixed points of iterative hard thresholding ((4), p. 5). It also serves as the inner solver of the paper's local combinatorial search (Algorithm 2, Theorem 4). So the guarantee transfers to the partial-swap-inescapable minima studied in the companion mission. Support stabilization (part 1) is also what reduces the asymptotic analysis to smooth strongly convex coordinate descent on a fixed support (Theorem 3).

The result is proved in the paper; no machine-checked version exists. A formalization would check the convergence argument for a discontinuous objective, where the bookkeeping of supports, counters and step indices is easy to get wrong. It would also provide a reusable Lean model of $L_0$ -penalized least squares and its thresholding operators.

Difficulty

The standard proof for cyclic coordinate descent needs a uniform decrease per step or a continuous objective. Neither holds here. A coordinate may switch between zero and a nonzero value infinitely often while $F$ decreases by arbitrarily small amounts, so the descent property alone gives neither support stabilization nor convergence of the iterates. Coordinates dropped infinitely often and coordinates added infinitely often must both be excluded. The tie-breaking rule in $T$ matters here: with the other choice on ties the algorithm is different. The exclusion of coordinates added infinitely often is only sketched in the paper (p. 43), and a complete proof has to supply it.

Formalization scope

Vectors are Fin p → ℝ with 0-based indices. Every norm is written as an explicit sum; Mathlib's sup norm on function types is never used. Unit-norm columns, $\lambda_0>0$ , $\lambda_1,\lambda_2\ge0$ and $p\ge1$ are hypotheses. The case $\lambda_1,\lambda_2>0$ , which the paper never names, is excluded from the statements about the algorithm's limits. $\mathrm{sign}$ is Real.sign. $T$ chooses the nonzero solution on ties, as in (12). The lower directional derivative takes values in EReal, since it is $+\infty$ in directions leaving the support. Lemma 3 is stated with the condition $|\tilde\beta_i|>\lambda_1$ on the support, taken from (5). The printed condition (8) omits it, and without it the equivalence fails for $\lambda_1>0$ . Indices and pages throughout are those of arXiv:1803.01454v3.

Algorithm 1 is a deterministic state machine: iterate, cyclic pointer, the counter array Count, and a flag for a pending spacer step. The iterates are therefore defined from $\beta^0$ and $C$ , not quantified over. The pointer advances only on non-spacer steps, following the pseudocode box; the prose formula $i=(k+1)\bmod(p+1)$ on p. 10 contradicts it. A statement about an arbitrary sequence satisfying a step predicate, or one that adds a step size or a sufficient-decrease hypothesis, would describe a different algorithm and is ruled out.

Useful infrastructure includes the scalar thresholding lemmas and coercivity of $f$ under Assumption 1 on supports of size at most $\min\{n,p\}$ . Contributions of proofs for any milestone are welcome, as are lemmas on the state machine (descent of each step type, the counter bookkeeping).

Selected references

H. Hazimeh, R. Mazumder, Fast Best Subset Selection: Coordinate Descent and Local Combinatorial Optimization Algorithms, Operations Research 68(5), 2020; arXiv:1803.01454v3. https://arxiv.org/abs/1803.01454
D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
P. Tseng, Convergence of a block coordinate descent method for nondifferentiable minimization, J. Optim. Theory Appl. 109, 2001. https://doi.org/10.1023/A:1017501703105
A. Beck, Y. C. Eldar, Sparsity constrained nonlinear optimization: optimality conditions and algorithms, SIAM J. Optim. 23(3), 2013. https://doi.org/10.1137/120869778
J. Friedman, T. Hastie, R. Tibshirani, Regularization paths for generalized linear models via coordinate descent, J. Stat. Softw. 33(1), 2010. https://doi.org/10.18637/jss.v033.i01

12 thms2 active usersReviewed

Dynamical Systems Machine Learning Optimization·Captain: mikedeng1

Convergence and Dynamical Behavior of the ADAM Algorithm for Nonconvex Stochastic Optimization 3: Under a Łojasiewicz Condition the Adam ODE Converges to One Critical Point at Rate t^(−θ/(1−2θ))Research Paper

Motivation

Adam (Kingma and Ba, 2015) is the default optimizer for training neural networks. At each step it keeps an exponential moving average $m$ of stochastic gradients and an exponential moving average $v$ of their squared coordinates, corrects both for their initialization at zero (the bias correction), and moves the iterate by $-\gamma\,\hat m/(\varepsilon+\sqrt{\hat v})$ coordinatewise.

Barakat and Bianchi (arXiv:1810.02263v4, SIAM J. Math. Data Sci. 2021) study Adam through the ODE method: as the step size $\gamma\to0$ with $1-\alpha\sim a\gamma$ and $1-\beta\sim b\gamma$ , the interpolated iterates follow a non-autonomous ordinary differential equation. Their Theorem 3.2 shows that the trajectory of this ODE approaches the critical set of the objective. That leaves open whether the trajectory settles at a single critical point, and how fast. For gradient-like systems the classical answer goes through the Łojasiewicz gradient inequality (Łojasiewicz, 1963, for real-analytic functions), and the dissipative-systems framework of Haraux and Jendoubi (2015) turns such an inequality into convergence with a rate. This mission formalizes the paper's Theorem 3.4, which brings that conclusion to the continuous-time Adam dynamics.

Timeline.

1963: Łojasiewicz proves the gradient inequality for real-analytic functions and derives convergence of bounded gradient-flow trajectories.
2009: Attouch and Bolte show convergence of the proximal algorithm under the Łojasiewicz property, with rates according to the exponent.
2014: Bolte, Sabach and Teboulle prove the same kind of result for proximal alternating linearized minimization.
2015: Haraux and Jendoubi collect the continuous-time theory for dissipative autonomous systems.
2018–2021: Barakat and Bianchi prove the result for the Adam ODE, which is non-autonomous and has a singular field at $t=0$ .

Setting

Let $F:\mathbb R^d\to\mathbb R$ be continuously differentiable with locally Lipschitz gradient $\nabla F$ , and let $S:\mathbb R^d\to\mathbb R^d$ be locally Lipschitz. In the paper $F(x)=\mathbb E f(x,\xi)$ and $S(x)=\mathbb E\,\nabla f(x,\xi)^{\odot2}$ . Its §7 uses only the two properties above, and so does this mission. Assume $F$ is coercive ( $F(x)\to+\infty$ as $\|x\|\to\infty$ ) and $S(x)>0$ coordinatewise for every $x$ . Fix constants $a,b,\varepsilon>0$ with $b\le 4a$ .

The state is $z=(x,m,v)\in\mathcal Z=\mathbb R^d\times\mathbb R^d\times\mathbb R^d$ , and all vector operations are coordinatewise. The Adam field (3.3) is, for $t>0$ ,

h(t,z)=\Big(-\frac{(1-e^{-at})^{-1}m}{\varepsilon+\sqrt{(1-e^{-bt})^{-1}v}},\ a(\nabla F(x)-m),\ b(S(x)-v)\Big),

and (ODE) is $\dot z(t)=h(t,z(t))$ . A global solution with initial condition $(x_0,0,0)$ is a continuous $z:[0,+\infty)\to\mathbb R^d\times\mathbb R^d\times[0,+\infty)^d$ that is continuously differentiable on $(0,+\infty)$ , satisfies (ODE) for every $t>0$ , and has $z(0)=(x_0,0,0)$ . The critical set is $\mathcal S=\{x:\nabla F(x)=0\}$ .

A number $\theta$ is a Łojasiewicz exponent of $F$ at $x^*$ if there are $c>0$ and $\sigma>0$ with

\|\nabla F(x)\|\ \ge\ c\,|F(x)-F(x^*)|^{1-\theta}\qquad\text{whenever }\|x-x^*\|\le\sigma. \tag{3.7}

Assumption 3.3 (the Łojasiewicz property) requires an exponent $\theta\in(0,\tfrac12]$ at every $x^*\in\mathcal S$ . It holds for real-analytic and semialgebraic $F$ .

The proof uses the Lyapunov function $V(t,z)=F(x)+\tfrac12\sum_i m_i^2/U_i(t,v)$ , where $U_i(t,v)=a(1-e^{-at})(\varepsilon+\sqrt{v_i/(1-e^{-bt})})$ (3.4)–(3.5). It also uses its perturbation $\tilde W_\delta(t,z)=V(t,z)-\delta\langle\nabla F(x),m\rangle+\delta\|S(x)-v\|^2$ (7.11) and $w_\delta(t)=\tilde W_\delta(t,z(t))$ .

Formalization targets

Goal: Theorem 3.4

Assume Assumption 3.3 and that $F(\mathcal S)$ has empty interior in $\mathbb R$ . Let $z=(x,m,v)$ be a global solution with initial condition $(x_0,0,0)$ . Then there is $x^*\in\mathcal S$ with $x(t)\to x^*$ as $t\to\infty$ . Moreover, if $\theta\in(0,\tfrac12]$ is a Łojasiewicz exponent of $F$ at $x^*$ , then

\|x(t)-x^*\|\le C\,t^{-\frac{\theta}{1-2\theta}}\quad(t>0)\ \text{ if }0<\theta<\tfrac12,\qquad \|x(t)-x^*\|\le C\,e^{-\delta t}\quad(t\ge0)\ \text{ if }\theta=\tfrac12,

for a constant $C>0$ (and, in the second case, some $\delta>0$ ) depending on the trajectory, $x^*$ and $\theta$ but not on $t$ .

Milestones

The milestones follow the proof in §7.4:

the decrease of $V$ along the non-autonomous field (Lemma 7.5, $V$ part);
convergence to the critical set (Theorem 3.2, restated here);
the upper bound (7.12) on $w_\delta$ by the four residual terms $|F(x)|$ , $\|m\|^2$ , $\|\nabla F(x)\|^2$ , $\|S(x)-v\|^2$ ;
the absolute continuity of $w_\delta$ and the derivative bound (7.13);
the differential inequality $\dot w_\delta\le-c_4\,w_\delta^{2(1-\theta)}$ of step iv), after the limit value of $F(x(t))$ is normalised to $0$ .

Significance

Theorem 3.2 only places the limit points of the trajectory in $\mathcal S$ . When $\mathcal S$ contains a continuum of critical points, the trajectory could in principle drift along it forever. Theorem 3.4 excludes this under the Łojasiewicz property. It shows that continuous-time Adam has finite length and converges to one critical point, and it makes the speed explicit. The speed is polynomial with exponent $\theta/(1-2\theta)$ in general and exponential when $\theta=\tfrac12$ , which holds for instance at a nondegenerate critical point. The theorem places continuous-time Adam in the same class as gradient flow, heavy-ball dynamics and proximal methods.

The result is proved in the paper (§7.4, with the final integration delegated to arguments of Haraux and Jendoubi). It has not, to current knowledge, been machine-checked. The mission produces a formal proof, together with formal statements of the Lyapunov estimates (7.12)–(7.13) for the Adam ODE. The Łojasiewicz-rate step is reusable for other perturbed gradient-like systems.

Difficulty

The standard Łojasiewicz argument for gradient flow uses $F$ itself as the Lyapunov function, whose derivative is $-\|\nabla F\|^2$ . For the Adam ODE neither $F$ nor $V$ works. $V$ decreases only at the rate $\|m\|^2$ , which says nothing about $\|\nabla F(x)\|$ when the momentum is small. The system is also non-autonomous, with a field that is singular at $t=0$ and only locally Lipschitz in $z$ . As a result $w_\delta$ is only absolutely continuous, so all derivative inequalities hold only almost everywhere. A further obstacle is that the Łojasiewicz inequality at a single critical point does not by itself control the trajectory: the limit set is a connected compact subset of $\mathcal S$ , and the inequality has to be made uniform on a neighbourhood of it. Finally, the rate has to be stated for an arbitrary exponent at the limit point, not only for the uniform exponent the argument produces.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) and $\mathcal Z$ is the product E × E × E, whose Mathlib norm is the maximum of the three Euclidean norms. This does not change any statement here, which concern $x$ , $m$ , $v$ separately. $F$ and $S$ are abstract, under the hypotheses of §7 (ContDiff ℝ 1 F, LocallyLipschitz (gradient F), LocallyLipschitz S, $S>0$ coordinatewise, coercivity as Tendsto F (cocompact _) atTop). Under Assumption 2.2 the paper's $F$ and $S$ satisfy these, so the statements imply the printed ones. A solution is a map ℝ → E × E × E constrained only on $[0,\infty)$ . The field uses $|v|$ in place of $v$ (the paper's extension, p. 12) and is never evaluated at $t=0$ . Statements are made for every global solution; there is exactly one (Theorem 3.1, a separate mission).

The polynomial bound is stated for $t>0$ , because Lean's real power gives $0^{-r}=0$ while the paper's right-hand side is $+\infty$ at $t=0$ . The constant $C$ is quantified before $t$ . A version with $C$ chosen after $t$ , or one that assumes $x(t)$ converges, would be trivial and is not the theorem. (7.13) states absolute continuity of $w_\delta$ on every $[1,T]$ together with the almost-everywhere derivative bound, since an almost-everywhere bound alone says nothing about $w_\delta$ .

A complete development needs the Lyapunov calculus of §7.1, compactness of the trajectory, the limit-set theory behind Theorem 3.2, the uniformisation of the Łojasiewicz inequality on a compact connected set of critical points, and the Haraux–Jendoubi integration lemmas. Contributions to the last two are reusable beyond this mission and are welcome, as are proofs of the individual milestones.

Selected references

A. Barakat and P. Bianchi, Convergence and Dynamical Behavior of the ADAM Algorithm for Nonconvex Stochastic Optimization, SIAM J. Math. Data Sci. 3(1), 2021; arXiv:1810.02263v4. https://arxiv.org/abs/1810.02263v4
D. P. Kingma and J. Ba, Adam: A Method for Stochastic Optimization, ICLR 2015. https://arxiv.org/abs/1412.6980
S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, Les Équations aux Dérivées Partielles, CNRS, 1963, pp. 87–89.
A. Haraux and M. A. Jendoubi, The Convergence Problem for Dissipative Autonomous Systems, SpringerBriefs in Mathematics, 2015. https://doi.org/10.1007/978-3-319-23407-6
H. Attouch and J. Bolte, On the convergence of the proximal algorithm for nonsmooth functions involving analytic features, Math. Program. 116, 2009, pp. 5–16. https://doi.org/10.1007/s10107-007-0133-5
J. Bolte, S. Sabach and M. Teboulle, Proximal alternating linearized minimization for nonconvex and nonsmooth problems, Math. Program. 146, 2014, pp. 459–494. https://doi.org/10.1007/s10107-013-0701-9

9 thms2 active usersReviewed

All missions

Error Bounds, Quadratic Growth, and Linear Convergence of Proximal Methods I: For the Proximal Gradient Method, the Error Bound Condition Is Equivalent to Quadratic GrowthResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 3.6 (p. 9)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Fast Convergence of Inertial Dynamics and Algorithms with Asymptotic Vanishing Viscosity 2: For Strongly Convex Φ and α > 3, Φ(x(t)) − min Φ, ‖x(t) − x*‖² and ‖ẋ(t)‖² Are O(t^(−2α/3))Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.4 (p. 11)

Milestones (explicit forms, valid for t≥t1t\ge t_1t≥t1​)

Significance

Difficulty

Formalization scope

Selected references

On a Problem of Optimal Transport Under Marginal Martingale Constraints 1: An Optimal Martingale Transport Plan Is Concentrated on a Borel Set No Finite Rerouting ImprovesResearch Paper

Motivation

Setting

Formalization targets

Goal: the variational lemma (Lemma 1.11, p. 8)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Error Bounds, Quadratic Growth, and Linear Convergence of Proximal Methods II: Dual Strict Complementarity and Firm Convexity of the Components Give the Error Bound for f(Ax) + g(x)Research Paper

Motivation

Setting

Formalization targets

Component and composite growth

Goal: a proximal gradient error bound

Significance

Difficulty

Formalization scope

Selected references

Optimality Gap of Constant-Order Policies Decays Exponentially in the Lead Time for Lost Sales Models: C(π_r∞)/OPT(L) ≤ 1 + h((1−γ)g)⁻¹(E[D] − r∞ + (eϑ(L+1))⁻¹)γ^{L+1} for Every Lead Time L ≥ 1Research Paper

Why lost-sales inventory with lead times matters

The setting

Formalization targets

Goal: Theorem 1 (p. 8)

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Extrapolated Proximal Subgradient Algorithms for Nonconvex and Nonsmooth Fractional Programs 3: Enhanced e-PSG Cluster Points Are Strong Lifted Stationary Points for Max-Type DenominatorsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.1(iii)

Milestones, in proof order

Significance

Difficulty

Formalization scope

Selected references

Maximum Scattered Linear Sets and Complete Caps in Galois Spaces 2: For q = 2^t, t Even, and n ≥ 4 Even, AG(n, q) Has a Complete Cap of Size 2√(q^(n−1))Research Paper

Small complete caps in Galois spaces

Setting

Formalization targets

Goal: Theorem 1.3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes 4: A Worst-Case Distribution Is the Law of X + √δ G A(X)⁻¹β, Spending the Whole Budget δResearch Paper

Why the worst case matters

Setting

Formalization targets

Goal: Theorem 6(c)

Milestones

Companion statements

Significance

Difficulty

Milestones (explicit forms, valid for $t\ge t_1$ )