Why this ODE needs a well-posedness theorem

Nesterov’s accelerated gradient method is a discrete procedure for minimizing a smooth convex function. Its iterates use both a gradient step and a momentum term, so the position at the next step depends on recent motion as well as on the current gradient. Su, Boyd, and Candès study a continuous-time model of that behavior: a trajectory whose acceleration is driven by the negative gradient and opposed by a time-dependent damping term. The model is useful only if its prescribed starting point determines an actual trajectory. The first theorem of the paper supplies that guarantee for the damping coefficient $3/t$. Su, Boyd, and Candès, 2015, Theorem 1.

The coefficient $3/t$ is undefined at the stated initial time $t=0$. Standard results for differential equations with a continuous right-hand side at the initial time therefore cannot be applied directly. The existence and uniqueness claim is substantive: it makes the trajectory used in the paper’s later rate and restart theorems a defined mathematical object, including its behavior at the singular endpoint. The source proves the result; this mission asks for a machine-checked formalization of its statement and its supporting appendix lemmas.

The setting

Fix a dimension $n$, a starting point $x_0\in\mathbb R^n$, and a real-valued objective $f$. For a constant $L>0$, the paper’s class $\mathcal F_L$ consists of functions that are convex, continuously differentiable, and have an $L$-Lipschitz gradient:

$$\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\| \qquad\text{for all }x,y\in\mathbb R^n.$$

The larger class $\mathcal F_\infty$ is the union of these classes over positive $L$. In particular, the objective need not be strongly convex and need not have a minimizer for this mission.

A solution is a position $X:[0,\infty)\to\mathbb R^n$ and its velocity $V=\dot X$, starting at $X(0)=x_0$ and $V(0)=0$, that satisfy equation (3) at every positive time:

$$\dot V(t)+\frac{3}{t}V(t)+\nabla f(X(t))=0,\qquad t>0.$$

The trajectory is continuously differentiable through the initial endpoint, with a right derivative there, and twice continuously differentiable for $t>0$. The paper also uses a smoothed equation indexed by $\delta>0$, replacing $3/t$ with $3/\max(\delta,t)$. Its solutions are denoted $X_\delta$, and its velocity-growth quantity is

$$M_\delta(t)=\sup_{0<u\le t}\frac{\|\dot X_\delta(u)\|}{u}.$$

For local uniqueness, two solutions $X,Y$ on $[0,a)$ are compared using $\widetilde M(t)=\sup_{0\le u<t}\|\dot X(u)-\dot Y(u)\|$. These quantities appear in the appendix lemmas and are represented by pointwise bounds in the formal statements.

Formalization targets

The goal is Theorem 1, the well-posedness of equation (3). For every $f\in\mathcal F_\infty$ and every $x_0$, it asserts both existence of a global trajectory with the regularity above and uniqueness on nonnegative time:

$$\exists X\ \text{solving (3) from }(x_0,0), \qquad X,Y\ \text{both solve (3) from }(x_0,0) \Longrightarrow X(t)=Y(t)\quad(t\ge0).$$

The milestone list follows the numbered statements in Appendix A. Lemma 16 controls the change in $\nabla f$ along a smoothed trajectory. Lemmas 15 and 17 bound $M_\delta$ on the initial smoothing interval and beyond it, with the explicit thresholds $\delta<\sqrt{6/L}$ and $t<\sqrt{12/L}$. Lemma 18 states that the family of smoothed trajectories with $\delta=\sqrt{3/L}/2^m$ is uniformly bounded and equicontinuous on $[0,\sqrt{6/L}]$. Lemma 14 gives existence for equation (3). Lemma 20 bounds the difference between gradients along two local solutions, and Lemma 19 gives uniqueness in a neighborhood of zero. The goal and milestones preserve the source’s domains, constants, and order of dependence.

What the result provides

Theorem 1 permits the rest of the paper to refer to “the” trajectory of equation (3) from a specified initial point. In particular, statements about its objective value, energy, and restarts need an actual trajectory, and uniqueness makes those statements independent of a choice of solution. The appendix estimates also provide reusable facts about this singular second-order equation: quantitative control of smoothed velocities and local agreement at the singular time.

The paper proves Theorem 1 and the seven listed lemmas on pp. 6 and 28–32. This mission does not claim a new analytical result. Its output would be checked Lean statements and, when solvers finish the proofs, a machine-checked development of the singular initial-value problem. The formal definitions are shared by all items in this mission; the lemmas can be reused in later formal work on accelerated gradient trajectories. No machine-checked proof of these particular statements is being claimed by the draft proposal.

The central difficulty

The initial time is precisely where the damping $3/t$ has no finite value. Treating the problem as an ordinary initial-value problem at $t=0$ leaves the differential equation undefined there. Imposing the equation at $t=0$ after Lean’s total division would instead change it: Lean assigns a value to division by zero, while the paper imposes equation (3) only for $t>0$. The demanded derivative at zero is one-sided, and control of the behavior as $t\downarrow0$ is part of the result.

The smoothed equations are regular at zero, but a statement about each smoothed trajectory does not by itself give a solution of the original singular equation. The appendix’s uniform bounds and equicontinuity are formulated on a common compact interval for a specified sequence of smoothing parameters. Uniqueness has a second boundary issue: local agreement near zero must be connected to ordinary uniqueness at positive time to obtain agreement for every $t\ge0$.

Formalization scope

The Lean space is $\mathrm{EuclideanSpace}\ \mathbb R\ (\mathrm{Fin}\ n)$, with its Euclidean norm; $n$ is arbitrary. The objective class includes convexity, $C^1$ regularity, a positive Lipschitz constant, and a globally Lipschitz gradient. A solution is encoded as a pair $(X,V)$, so $V=\dot X$ is witnessed by derivative assertions rather than by a total derivative operator. The initial conditions specify $X(0)=x_0$, $V(0)=0$, a right derivative of $X$, and right continuity of $V$. The differential equation and ordinary derivatives are required only at positive times. For the smoothed equation, $\delta>0$ is part of the solution predicate.

These choices rule out a vacuous solution predicate and prevent division by zero from defining a different equation. Lean functions are represented on all real times, but the source’s solution lives on $[0,\infty)$; uniqueness is therefore equality on that half-line. At negative times the formal representatives are unrestricted. The paper’s real suprema $M_\delta$ and $\widetilde M$ are expressed as bounds on every member of their defining ranges, so an empty or unbounded real supremum cannot acquire a misleading default value. Every denominator in Lemmas 15 and 17 has the paper’s strict threshold in its hypotheses.

A full proof development needs ordinary differential equation existence and uniqueness at positive time, continuity and derivative facts at the right endpoint, and compactness of uniformly bounded equicontinuous families. The definitions of the objective class and solution predicates, the quantitative estimates, and the local uniqueness statement are welcome solver contributions. The target is the source theorem with its stated hypotheses and conclusion; a special objective, a weakened time interval, or a proof by an impossible hypothesis does not close it.

Selected references

• Weijie Su, Stephen Boyd, and Emmanuel J. Candès, A Differential Equation for Modeling Nesterov’s Accelerated Gradient Method: Theory and Insights, arXiv:1503.01243v2, 2015; published in Journal of Machine Learning Research 17(153), 2016. Preprint.

Motivation

A newsvendor chooses an order quantity before seeing demand. Unsold units have no salvage value, while demand above the order quantity cannot be filled. If the demand law is unknown but a few moments are known, the decision maker may minimize cost against the worst distribution consistent with those moments. Das, Dhara and Natarajan study this distributionally robust problem when the known moments are the first and an arbitrary real moment of order $\alpha>1$ Das, Dhara and Natarajan, 2019. The high-demand tail matters especially when the cost ratio favors large orders. The mission asks what tail behavior is implicitly selected by the robust objective, even though each admissible distribution has a finite $\alpha$th moment.

The two-moment case $\alpha=2$ goes back to Scarf's newsvendor bound. The paper extends the model to noninteger $\alpha$ and gives lower and upper shortage bounds before proving its tail result. Its preprint is the pinned source for every statement here; the proof of each numbered result follows that result in the paper Das, Dhara and Natarajan, 2019, §§1, 3–4.

Setting

Let $q\ge0$ be the order quantity and let $\tilde d\ge0$ be random demand. The expected shortage under a demand law $F$ is $\mathbb E_F[(\tilde d-q)^+]$, where $x^+=\max(x,0)$. Fix $\alpha>1$, a positive mean $m_1$, and a moment $m_\alpha>m_1^\alpha$. The moment ambiguity set $\mathcal F_{1,\alpha}$ contains all probability laws supported on $[0,\infty)$ whose first moment is $m_1$ and whose finite $\alpha$th moment is $m_\alpha$. Its worst-case expected shortage is

$$\Pi_{1,\alpha}(q)=\sup_{F\in\mathcal F_{1,\alpha}}\mathbb E_F[(\tilde d-q)^+].$$

For a critical ratio $\eta\in[0,1)$, the robust newsvendor minimizes $(1-\eta)q+\Pi_{1,\alpha}(q)$ over $q\ge0$. This mission centers on $\Pi_{1,\alpha}$; the optimal-order threshold is treated in the companion mission. The ambiguity set and objective are the paper's (3.1)–(3.3) Das, Dhara and Natarajan, 2019, pp. 10–11.

A positive function $u$ is regularly varying with index $\rho$ if $u(tx)/u(x)\to t^\rho$ as $x\to\infty$ for every $t>0$. The notation is $u\in RV_\rho$. For a probability law $F$, its survival tail is $\bar F(x)=P_F(\tilde d>x)$; $\bar F\in RV_{-\alpha}$ means a tail parameter $\alpha$ Das, Dhara and Natarajan, 2019, §4.1, p. 26.

Formalization targets

Worst-case shortage

The first target is Theorem 4.3(a):

$$\Pi_{1,\alpha}\in RV_{-(\alpha-1)}.$$

It covers every $\alpha>1$, including $\alpha=2$. Scarf's piecewise formula (1.3), Proposition 3.3, and both parts of Proposition 3.4 supply the paper's cited bounds. Each upper bound retains its strict quantity threshold and its printed denominator Das, Dhara and Natarajan, 2019, pp. 3, 15, 19, 28.

One representative demand law

The full goal, Theorem 4.3, also states that a nonnegative probability law $F^*$ exists outside $\mathcal F_{1,\alpha}$ with

$$\mathbb E_{F^*}[(\tilde d^*-q)^+]=\Pi_{1,\alpha}(q)\quad(q\ge0), \qquad \bar F^*\in RV_{-\alpha}.$$

Every moment of $F^*$ of order $0\le a<\alpha$ is finite, while every moment of order $a\ge\alpha$ is infinite. The milestone list includes the properties of $\Pi_{1,\alpha}$ stated in §2.1 (non-increasing, convex, $\Pi_{1,\alpha}(q)+q=m_1$ for $q\le0$, $\Pi_{1,\alpha}(q)\to0$), the single-law representation (2.1) and the two stated Karamata results used to characterize the tail Das, Dhara and Natarajan, 2019, pp. 6, 27–30.

High critical ratios

A companion milestone is Proposition 4.1. For $\eta\in(0,1)$ let $q^*_\eta$ be a robust optimal order quantity and $C^*_\eta$ the optimal robust cost. Then $q^*_\eta$ is optimal for the standard newsvendor with demand law $F^*$, and

$$q^*_\eta\sim\frac{\alpha-1}{\alpha}\,\frac{1}{1-\eta}\,C^*_\eta,\qquad \eta\to1$$

Das, Dhara and Natarajan, 2019, p. 30, (4.9). It is a consequence of the goal, not a step toward it.

Significance

The theorem connects a decision made against an entire moment class to a single effective law. That law matches the robust expected shortage for every admissible order quantity but has an infinite $\alpha$th moment, so it does not belong to the class being optimized over. This distinction explains why large robust orders behave as though demand were heavy tailed. The paper also uses the result to relate the robust optimal order quantity to the optimal cost at high service levels in Proposition 4.1 Das, Dhara and Natarajan, 2019, pp. 30–31.

The mathematical theorem was proved in the cited paper. This mission asks for a Lean proof of its exact statement and reusable formal results for moment-constrained probability laws, stop-loss transforms, and regular variation. No machine-checked proof of these particular statements is part of the present draft. The cited bounds and analytic results are posed as separate milestones so their hypotheses and constants remain inspectable.

Difficulty

Pointwise optimization over demand laws does not automatically give one law that attains the worst-case shortage for every $q$. For a fixed $q$, an extremal law may depend on $q$, as Scarf's formula illustrates Das, Dhara and Natarajan, 2019, p. 3. The theorem asks for a single $F^*$ and then a precise tail index and a sharp moment cutoff. A generic upper bound on shortages would establish neither the representative law nor its infinite $\alpha$th moment. The regimes $1<\alpha<2$, $\alpha=2$, and $\alpha>2$ have different cited upper-bound statements, yet the final theorem has no regime restriction.

Formalization scope

Lean represents a demand law by a Borel measure on $\mathbb R$ with probability mass one and zero mass below zero. Membership in $\mathcal F_{1,\alpha}$ requires both real moments to be integrable; this makes the moment equalities genuine rather than default values of a nonintegrable Bochner integral. Under $m_1>0$ and $m_\alpha>m_1^\alpha$, the paper's two-point law (3.6) makes the ambiguity set nonempty. Its shortage values are bounded above by $m_1+|q|$, so the real supremum defining $\Pi_{1,\alpha}$ is finite and meaningful. The strict thresholds in Propositions 3.3–3.4 keep their power denominators positive Das, Dhara and Natarajan, 2019, pp. 12, 15, 19.

Regular variation includes eventual positivity, excluding a zero-over-zero ratio from passing as a tail law. Infinite moments of $F^*$ are lower Lebesgue integrals in extended nonnegative reals. The existence of $F^*$ is asserted rather than built into a definition. Theorem 4.2(b)'s displayed limit has a negative sign in the preprint, although its nonnegative numerator and denominator require the positive value $\alpha$; the formal statement uses the corrected sign. Its regularly varying tail integral is eventually positive, which ensures genuine finite tail integrals for large lower limits. Theorem 4.1 explicitly requires local integrability. Two encodings would trivialize the goal and are excluded: defining $F^*$ inside the statement (it is existential), and a regular-variation predicate satisfied by the zero function. The properties of $\Pi$ and the representation (2.1) are stated for $\mathcal F_{1,\alpha}$, the instance the paper uses, rather than for a general finite-mean ambiguity set. In Proposition 4.1 the optimal cost is the cost at the chosen optimizer, the statement holds for every selection of optimizers, and $\sim$ means that the ratio of the two sides tends to $1$ as $\eta\uparrow1$. These analytic conventions and the probability and measure infrastructure can be reused beyond this mission. Contributions to any of the ten source milestones, including the difficult root assertion in Proposition 3.4(b), are welcome.

Selected references

• B. Das, A. Dhara, and K. Natarajan, On the Heavy-Tail Behavior of the Distributionally Robust Newsvendor, Operations Research 69(4), 2021; preprint arXiv:1806.05379v2, 2019. Preprint, DOI.
• H. Scarf, A min-max solution of an inventory problem, in K. Arrow, S. Karlin and H. Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958, pp. 201–209.
• A. Shapiro and A. Kleywegt, Minimax analysis of stochastic problems, Optimization Methods and Software 17, 2002, pp. 523–542. DOI.
• N. H. Bingham, C. M. Goldie and J. L. Teugels, Regular Variation, Cambridge University Press, 1987. DOI.

Why composition matters

Optimization models often build an objective from several intermediate quantities: constraints, penalties, and transformed measurements are evaluated first, then combined by an outer function. These intermediate and outer functions can be Lipschitz without being differentiable at the point of interest. Ordinary differentiation supplies no chain rule there. The generalized-gradient framework gives a set of possible first-order slopes, while semismoothness provides stronger directional behavior along sequences approaching the point. Mifflin's IIASA report asks whether this behavior survives such compositions and how the generalized gradient of the result relates to those of its ingredients.

The report first establishes basic properties of the generalized gradient in §2, including almost-everywhere differentiability and a nonsmooth mean value theorem. Section 4 then states a chain-rule inclusion as Theorem 4 and the semismooth composition result as Theorem 5. The report is dated December 1976; a journal version appeared in 1977. The mission cites theorem numbers and pages from the report version throughout. No claim about differences between the report and journal texts is needed here.

Setting and definitions

Work in finite-dimensional Euclidean spaces. Let $f_i:\mathbb R^n\to\mathbb R$, for $i=1,\ldots,m$, be component functions, and let $E:\mathbb R^m\to\mathbb R$ be an outer function. Define the component map $Y$ and the composite $F$ by

$$Y(x)=(f_1(x),\ldots,f_m(x)),\qquad F(x)=E(Y(x)).$$

The functions are locally Lipschitz in the report's precise sense: on each bounded subset of their Euclidean domain they have a finite Lipschitz constant. For a scalar function $H$, a point $x$, and a direction $d$, the generalized directional derivative $H^0(x;d)$ is the joint upper limit of $[H(x+h+td)-H(x+h)]/t$ as $h\to0$ and $t\downarrow0$. Its associated generalized gradient is the support set

$$\partial H(x)=\{g:\langle g,d\rangle\le H^0(x;d)\text{ for every direction }d\}.$$

This is the definition used in Mifflin's report, not an identification assumed in advance with a hull of ordinary gradient limits. Proposition 1(c) supplies that identification under the paper's Lipschitz assumption. The ordinary one-sided directional derivative $H'(x;d)$ is the limit of $[H(x+td)-H(x)]/t$ for $t\downarrow0$, when that limit exists.

Mifflin calls $H$ semismooth at $x$ if it is Lipschitz on a ball about $x$ and the scalar sequence $\langle g_k,d\rangle$ has exactly one accumulation point whenever $t_k>0$ tends to zero, $\theta_k/t_k\to0$, and $g_k\in\partial H(x+t_kd+\theta_k)$. The quantification is over every direction and every such sequence. This pointwise condition is Definition 1 of the report, and its link to one-sided directional derivatives is Lemma 2.

To state the chain rule, form the set

$$G(x)=\operatorname{conv}\left\{\sum_{i=1}^{m}w_i g^i:g^i\in\partial f_i(x)\text{ for every }i,\quad w\in\partial E(Y(x))\right\}.$$

The same $w$ is used across all components. The sum is the action of the report's matrix $[g^1\cdots g^m]$ on $w$.

Formalization targets

Generalized-gradient chain rule

Theorem 4 asserts that $F$ is locally Lipschitz and that, at every point,

$$\partial F(x)\subseteq G(x).$$

This is an inclusion, not a general equality. The report gives an example immediately after Theorem 4 in which the inclusion is strict: two identical absolute-value components cancel under an outer difference, while $G(0)$ remains larger than $\partial F(0)$.

Semismooth composition

The goal, Theorem 5, assumes the setting of Theorem 4. If each $f_i$ is semismooth at a selected $x$ and $E$ is semismooth at $Y(x)$, then

$$E\circ Y\text{ is semismooth at }x.$$

The conclusion is pointwise. It does not assert semismoothness throughout $\mathbb R^n$ from hypotheses at one point. The milestone list contains the chain rule and the source's stated support results: Proposition 2, Lemma 1, Proposition 1(c) and (d), Lemma 2, and the claims (4.2) and (4.11)–(4.12) from the proofs.

What the results provide

Theorem 5 permits composite nonsmooth objectives to be treated within the same semismooth class as their components. Theorem 4 gives a concrete set built from component generalized gradients that contains the composite's generalized gradient. Together, they let later statements about a composite use first-order information from its stated ingredients, subject to the inclusion's possible strictness. These are results proved in Mifflin's report, not open mathematical conjectures.

This mission drafts machine-checkable statements of those known results and their definition layer. The local Lean modules compile with proof placeholders; this staging does not supply machine-checked proofs of the theorems. A complete development would formalize the known arguments or another proof of the same statements. The reusable output would include the support-set generalized gradient, sequence-based semismoothness, the nonsmooth mean value result, and the chain-rule inclusion, all with their source assumptions exposed.

Main difficulty

At a point where $F$ is differentiable, the component functions $f_i$ need not be differentiable, and the outer function $E$ need not be differentiable at $Y(x)$. The ordinary smooth chain rule therefore cannot simply multiply ordinary gradients. The candidate $G(x)$ is a convex set of combinations of generalized gradients; a single chosen combination does not in general describe all nearby limiting slopes. The report's strict-inclusion example also shows why replacing Theorem 4 by equality would be false. For semismoothness, the condition concerns every admissible sequence of generalized gradients near the point, so checking just one path or one gradient selection does not establish Theorem 5.

Formalization scope

The Lean domain is EuclideanSpace ℝ (Fin n) and the outer domain is EuclideanSpace ℝ (Fin m). The report's norm is the Euclidean norm and its pairing is the real inner product. An index of type Fin m represents the $m$ components; $m=0$ is admitted, in which case the component space is a point and the composite is constant. A finite sum represents the column-matrix product. The generalized gradient is defined by all directional support inequalities, so Proposition 1(c) remains a theorem rather than becoming true by definition.

The generalized directional derivative is imported from the published definition matching the report's joint limit. Lean's real limsup has a default value for an unbounded quotient; Lipschitz hypotheses are carried wherever that operation is used. “Locally Lipschitz” is imported as Lipschitzness on every bounded subset, and the explicit constants of §2 use nonnegative reals, equivalent to the report's positive constants by enlarging them. The directional derivative is a relation asserting a limit, so no value is assigned when the limit fails. “Exactly one accumulation point” remains an existence-and-uniqueness assertion about cluster points. The report's $t_k\downarrow0$ means positive convergence to zero, as its proof of Lemma 2 says explicitly. These choices exclude a vacuous formulation that only asks about one convenient sequence or gives a default directional value.

The scope includes the two local definition files and the cited theorem statements, including both conclusions of Theorem 4 and Lemma 2. Proof contributions would need finite-dimensional Lipschitz and differentiability infrastructure, limiting-gradient compactness, convex hull and separation facts, and sequence convergence facts. Results about the alternative Qi–Sun vector-valued semismoothness notion are outside this mission's definition layer.

Selected references

• R. Mifflin, Semismooth and Semiconvex Functions in Constrained Optimization, IIASA Research Report RR-76-21, December 1976. Report PDF.
• R. Mifflin, “Semismooth and Semiconvex Functions in Constrained Optimization,” SIAM Journal on Control and Optimization 15(6), 1977. DOI. This mission's page and theorem references are to the IIASA report.

Motivation

A probability distribution on the real line is self-decomposable (of class L) if its characteristic function satisfies $\varphi(t)=\varphi(\alpha t)\,\varphi_\alpha(t)$ for every $\alpha\in(0,1)$, with $\varphi_\alpha$ again a characteristic function. Equivalently, a random variable $X$ can be written as $X\overset{d}{=}\alpha X'+X_\alpha$ with $X'$ a copy of $X$ independent of $X_\alpha$. Class L consists exactly of the limit laws of normalized sums of independent summands, and its members are infinitely divisible, absolutely continuous (when nondegenerate) and unimodal.

None of this transfers to counting variables: apart from $X\equiv0$, no random variable on $\mathbb N_0=\{0,1,2,\dots\}$ satisfies $X=\alpha X'+X_\alpha$, because $\alpha X'$ leaves the lattice. Steutel and van Harn (Memorandum COSOR 78-07, 1978; Ann. Probab. 7 (1979) 893–899) replaced scalar multiplication by binomial thinning, which keeps the variable integer valued. The resulting notion of discrete self-decomposability later became the basis of integer-valued autoregressive (INAR) time-series models (Al-Osh and Alzaid, 1987).

Timeline:

• 1968: Feller, An Introduction to Probability Theory and Its Applications, vol. 1, 3rd ed., characterizes the infinitely divisible distributions on $\mathbb N_0$ as the compound Poisson distributions.
• 1971: Steutel, On the zeros of infinitely divisible densities (Ann. Math. Statist. 42), and 1977: van Harn and Steutel, Generalized renewal sequences and infinitely divisible lattice distributions (Stoch. Proc. Appl. 5), give the recursive criterion $(n+1)p_{n+1}=\sum_k p_k r_{n-k}$ with $r_n\ge0$.
• 1978–1979: Steutel and van Harn introduce discrete self-decomposability and discrete stability and prove the canonical form (Theorem 2.2, the goal of this mission), unimodality, and the characterization of the discrete stable laws.

Setting

A distribution on $\mathbb N_0$ is a sequence $p_n\ge0$ with $\sum_n p_n=1$; its probability generating function (p.g.f.) is $P(z)=\sum_{n\ge0}p_nz^n$. The generating function of a sequence $(g_n)$ is written $G$.

The $\alpha$-thinning of a variable $X$ with p.g.f. $P$ is $\alpha\circ X=\sum_{j=1}^{X}N_j$ with independent Bernoulli($\alpha$) variables $N_j$; its p.g.f. is $P(1-\alpha+\alpha z)$. A distribution with p.g.f. $P$ is discrete self-decomposable (Definition 2.1) if for every $\alpha\in(0,1)$

$$P(z)=P(1-\alpha+\alpha z)\,P_\alpha(z)\qquad(|z|\le1)$$

with $P_\alpha$ a p.g.f.; in variables, $X\overset{d}{=}\alpha\circ X'+X_\alpha$.

A distribution is infinitely divisible if for every $n\ge1$ its p.g.f. is the $n$-th power of a p.g.f. When $p_0>0$, its canonical sequence $(r_n)$ is the unique solution of

$$(n+1)\,p_{n+1}=\sum_{k=0}^{n}p_k\,r_{n-k}\qquad(n\in\mathbb N_0).$$

Throughout §2 the paper assumes $0<p_0<1$.

Formalization targets

Goal: Theorem 2.2

For a distribution $(p_n)$ with $0<p_0<1$:

$$(p_n)\ \text{discrete self-dec}\iff P(z)=\exp\Big\{-\lambda\int_z^1\frac{1-G(u)}{1-u}\,du\Big\}\quad(0\le z<1)$$

for some $\lambda>0$ and some p.g.f. $G$ of a distribution with $G(0)=0$, the pair $(\lambda,G)$ being unique; and

$$(p_n)\ \text{discrete self-dec}\iff (p_n)\ \text{inf div and } (r_n)\ \text{nonincreasing}.$$

Milestones

1. Lemma 1.1: $\lim_{x\uparrow1}(1-x)P'(x)=0$ for every p.g.f.
2. Lemma 1.2: for $0<p_0<1$, $P$ is infinitely divisible iff $P(z)=\exp\{\lambda(G(z)-1)\}$ (unique $\lambda>0$, $G(0)=0$), iff $P(z)=\exp\{-\int_z^1R(u)\,du\}$ with $R=\sum r_nu^n$, $r_n\ge0$ (necessarily $\sum r_n/(n+1)<\infty$), iff the canonical sequence is nonnegative.
3. (2.6): if $P$ is discrete self-decomposable, $\exp\{-r(1-z)P'(z)/P(z)\}$ is a p.g.f. for every $r>0$.
4. (2.7)–(2.8): the form (2.4) gives $P'/P=\lambda(1-G)/(1-z)$, infinite divisibility, and $r_n=\lambda\sum_{j>n}g_j$, nonincreasing.
5. The converse (pp. 3–4): if $P$ is infinitely divisible with nonincreasing $r_n$, then $P(z)/P(1-\alpha+\alpha z)$ is an infinitely divisible p.g.f. for each $\alpha\in(0,1)$.

Significance

Theorem 2.2 reduces discrete self-decomposability, a condition quantified over all $\alpha\in(0,1)$ and over unknown factors $P_\alpha$, to a single monotonicity condition on the sequence $(r_n)$ computed recursively from $(p_n)$. It is the entry point of the rest of the paper: combined with Theorem 2.3 it gives unimodality of every discrete self-decomposable distribution (Corollary 2.4), and §3 shows that discrete stable distributions are discrete self-decomposable. In time-series modelling it identifies the marginals that a stationary INAR(1) process $X_t=\alpha\circ X_{t-1}+\varepsilon_t$ can have for every $\alpha\in(0,1)$.

The result has been proved since 1979; to our knowledge none of it is formalized in any proof assistant, and Mathlib has neither probability generating functions on $\mathbb N_0$ nor infinite divisibility. The mission produces a machine-checked version of the canonical form together with the compound-Poisson characterization of infinite divisibility on $\mathbb N_0$ (Lemma 1.2), which the paper only cites.

Difficulty

The forward direction is not a consequence of (2.1) for any single $\alpha$: one factorization $P(z)=P(1-\alpha+\alpha z)P_\alpha(z)$ constrains $P$ very little, and the information sits in the whole family of factors $P_\alpha$, $\alpha\in(0,1)$, which are not given explicitly. Turning that family into a statement about $P$ needs a passage to a limit of p.g.f.'s, and the fact that such a limit is again a p.g.f. (the continuity theorem for p.g.f.'s, Feller vol. 1, p. 280) is not in Mathlib. The paper does not prove Lemma 1.2 either; it cites Feller and Steutel. For the converse, nonnegativity of the canonical sequence is not enough: the obvious attempt to show that $P(z)/P(1-\alpha+\alpha z)$ has nonnegative coefficients fails for infinitely divisible $P$ in general, and the monotonicity of $r_n$ is exactly what is needed. Finally, every identity is stated between real functions on $[0,1]$, and passing to identities between coefficients requires the uniqueness of power-series coefficients on a real interval.

Formalization scope

• A distribution is p : ℕ → ℝ with ∀ n, 0 ≤ p n and HasSum p 1; the p.g.f. is the real function pgf p z = ∑' n, p n * z ^ n. All identities between p.g.f.'s are required for real $z\in[0,1]$ (or $[0,1)$ for (1.4), (2.4), (2.6), (2.7)), not for complex $|z|\le1$; p.g.f.'s agreeing on $[0,1]$ have equal coefficients, so this is equivalent. $P'$ is Lean's deriv of pgf p.
• Infinite divisibility follows Feller: for every $n\ge1$ an $n$-th root that is the p.g.f. of a distribution on $\mathbb N_0$. It is not defined as $r_n\ge0$ or as the form (1.3); those are Lemma 1.2.
• The canonical sequence is defined by the recursion $r_n=((n+1)p_{n+1}-\sum_{k=1}^np_kr_{n-k})/p_0$; every statement using it assumes $p_0>0$.
• The standing assumption $0<p_0<1$ of §2 is a hypothesis of Theorem 2.2 and of the §2 milestones.
• The improper integrals in (1.4) and (2.4) carry an explicit integrability clause on $(z,1)$, and the series $R$ an explicit convergence clause on $[0,1)$. Lean's integral of a non-integrable function, and the sum of a divergent series, are $0$; without these clauses the forms (1.4) and (2.4) could hold vacuously, so a formalization that drops them does not state the theorem.
• Uniqueness of $(\lambda,G)$ in (1.3) and (2.4) is part of the statements.

Reusable beyond this mission: the p.g.f. and infinite-divisibility vocabulary, Lemma 1.2 (compound Poisson characterization), and Lemma 1.1. A continuity theorem for p.g.f.'s on $\mathbb N_0$, and the uniqueness of power-series coefficients from values on $[0,1)$, are welcome as independent contributions.

Selected references

• F. W. Steutel, K. van Harn, Discrete analogues of self-decomposability and stability, Memorandum COSOR 78-07, Technische Hogeschool Eindhoven, 1978. https://pure.tue.nl/ws/files/1719387/340666.pdf — published as Ann. Probab. 7(5) (1979) 893–899. https://doi.org/10.1214/aop/1176994950
• W. Feller, An Introduction to Probability Theory and Its Applications, vol. 1, 3rd ed., Wiley, New York, 1968 (XII.2; continuity theorem p. 280).
• F. W. Steutel, On the zeros of infinitely divisible densities, Ann. Math. Statist. 42 (1971) 812–815.
• K. van Harn, F. W. Steutel, Generalized renewal sequences and infinitely divisible lattice distributions, Stochastic Process. Appl. 5 (1977) 47–55.
• M. A. Al-Osh, A. A. Alzaid, First-order integer-valued autoregressive (INAR(1)) process, J. Time Series Anal. 8 (1987) 261–275. https://doi.org/10.1111/j.1467-9892.1987.tb00438.x

Motivation

Many objective functions in engineering design, Chebyshev approximation and game-theoretic planning are extremal-valued: they are the pointwise maximum or minimum of a family of smooth functions, $E(x)=\max_{u\in U} f(x,u)$. Such a function is typically not differentiable at points where two or more members of the family are active, so gradient methods do not apply directly. In 1976 R. Mifflin introduced the class of semismooth functions to identify which nondifferentiable functions can be minimized by bundle-type and line-search methods whose convergence relies only on generalized gradients (Mifflin, IIASA RR-76-21; journal version SIAM J. Control Optim. 15 (1977), doi:10.1137/0315061). For that class to be useful it must contain the functions that actually occur in practice. §3 of the report shows that it contains min–max objectives, which is the content of this mission.

Background: F. H. Clarke defined the generalized gradient of a locally Lipschitz function and computed it for max functions (Clarke, Trans. AMS 205 (1975), Theorem 2.1). A. Feuer's Columbia dissertation (1974) proved the formulas of Theorem 1 below under stronger assumptions and a result close to semismoothness, from which Mifflin's proof of Theorem 2 is adapted (report, Remark, p. 8). Mifflin's notion of semismoothness was later extended to vector-valued maps by Qi and Sun (1993), where it became the standard hypothesis for superlinear convergence of nonsmooth Newton methods.

Setting

Let $\mathbb R^n$ carry the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $|\cdot|$, and let $F:\mathbb R^n\to\mathbb R$. $F$ is Lipschitz on a set $B$ if $|F(y)-F(z)|\le K|y-z|$ for all $y,z\in B$. Clarke's generalized directional derivative is

$$F^0(x;d)=\limsup_{h\to 0,\ t\downarrow 0}\frac{F(x+h+td)-F(x+h)}{t},$$

and the generalized gradient is $\partial F(x)=\{g:\langle g,d\rangle\le F^0(x;d)\ \forall d\}$. When $\lim_{t\downarrow 0}[F(x+td)-F(x)]/t$ exists it is the directional derivative $F'(x;d)$; $F$ is quasidifferentiable at $x$ if $F'(x;d)$ exists and equals $F^0(x;d)$ for all $d$.

$F$ is semismooth at $x$ (Definition 1) if it is Lipschitz on a ball about $x$ and, for each $d$ and all sequences $t_k\downarrow 0$, $\theta_k$ with $\theta_k/t_k\to 0$, and $g_k\in\partial F(x+t_kd+\theta_k)$, the real sequence $\langle g_k,d\rangle$ has exactly one accumulation point. $F$ is semiconvex at $x$ with respect to $X$ (Definition 2) if it is Lipschitz on a ball about $x$, quasidifferentiable at $x$, and $x+d\in X$, $F'(x;d)\ge 0$ imply $F(x+d)\ge F(x)$.

In §3, $B\subseteq\mathbb R^n$ is open, $T$ is a topological space, $U\subseteq T$ is sequentially compact, $f:\mathbb R^n\times T\to\mathbb R$, and $E:\mathbb R^n\to\mathbb R$ satisfies either (d) $E(x)=\max_{u\in U}f(x,u)$ on $B$ or (d′) $E(x)=\min_{u\in U}f(x,u)$ on $B$. The active set is $A(x)=\{u\in U:E(x)=f(x,u)\}$, and $\partial_x f(x,u)$ is the generalized gradient of $f(\cdot,u)$ at $x$. Hypotheses (a)–(c) ask that $f$ be continuous on $B\times U$, Lipschitz in $x$ uniformly in $u$, and that $\partial_x f$ be upper semicontinuous on $B\times U$; (e) and (e′) ask that $f'_x(x,u;d)$ exist and equal $f^0_x(x,u;d)$, respectively $-f^0_x(x,u;-d)$.

Formalization targets

Goal: Theorem 2 (p. 8)

If (a) holds, $E$ has the max form (d) or the min form (d′), $f(\cdot,u)$ is differentiable on $B$ for each $u\in U$, and $\nabla_x f$ is continuous and bounded on $B\times U$, then

$$E\ \text{is semismooth on } B.$$

Milestones

• Proposition 1(a), (b), (d) (p. 3): $\partial F(x)$ is nonempty, convex and compact; $F^0(x;d)=\max\{\langle g,d\rangle:g\in\partial F(x)\}$; $\partial F$ is bounded by the Lipschitz constant and upper semicontinuous.
• Theorem 1 (pp. 7–8), max and min forms: $E$ is Lipschitz on $B$,

$$\partial E(x)=\operatorname{conv}\bigcup_{u\in A(x)}\partial_x f(x,u),\qquad E'(x;d)=E^0(x;d)=\max\{\langle g,d\rangle:g\in\partial_x f(x,u),\ u\in A(x)\}$$

in the max form, and $E'(x;d)=-E^0(x;-d)=\min\{\cdots\}$ in the min form.

• Two claims from the proof of Theorem 2 (p. 8): the smoothness assumption yields (b), (c), (e), (e′) and $\partial_x f=\{\nabla_x f\}$; and $\limsup_k\langle g_k,d\rangle\le E'(x;d)$.
• Theorem 3 (p. 10): a max function of functions semiconvex at $x$ is semiconvex at $x$.
• Propositions 3 and 4 (pp. 5–6): convex, concave and continuously differentiable functions are semismooth, with the corresponding semiconvexity and quasidifferentiability statements.

Significance

Theorem 2 places every min–max objective with continuously differentiable data inside the class on which Mifflin's descent algorithms, and the bundle methods that followed them, are proved to converge. Theorem 1 is the generalized-gradient form of Danskin's theorem, the standard tool for computing subgradients of max functions. Theorem 3 shows that semiconvexity, unlike pseudoconvexity, survives pointwise maximization, which is what the sufficient optimality results of §5 of the report need.

All of these results are proved in the report and in the literature since 1977; none is open. As far as is known, none of them has a machine-checked proof. Mathlib has Fréchet derivatives and convex analysis but no Clarke generalized gradient calculus, no semismoothness and no Danskin-type theorem. A formalization produces those pieces as reusable infrastructure, and checks the report's statements under exactly stated hypotheses. One printed claim already needs a correction (see Formalization scope).

Difficulty

Lipschitz continuity of $E$ and the inequality $\limsup_k\langle g_k,d\rangle\le E'(x;d)$ follow from Theorem 1 and the upper semicontinuity of $\partial E$. The difficulty is the matching lower bound: semismoothness asks that the slopes $\langle g_k,d\rangle$ along an arbitrary sequence $x_k=x+t_kd+\theta_k$, with arbitrary $g_k\in\partial E(x_k)$, not accumulate strictly below $E'(x;d)$. A generalized gradient of $E$ at $x_k$ is only a convex combination of gradients of the active functions at $x_k$, and the active set can change discontinuously along the sequence. Upper semicontinuity of $\partial E$ alone does not prevent this; the function $x^2\sin(1/x)$ (p. 6) is Lipschitz and has an upper semicontinuous $\partial F$ but is not semismooth at $0$. The argument has to use the continuity of $\nabla_x f$ jointly in $(x,u)$ and the compactness of $U$. Theorem 1 itself needs a mean value theorem for Lipschitz functions and a compactness argument over the active set, neither of which is in Mathlib in this form.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). $F^0$ is the published ClarkeGradients.Shared.genDirDeriv, a real limsup; every statement assumes the Lipschitz hypothesis of the page at the points where $F^0$ or $\partial F$ is used, so that this limsup is the true value. $\partial F$ is the support-set definition of the page, not Clarke's convex hull of gradient limits; the two coincide by Proposition 1(c), which is not assumed. $F'(x;d)$ is a relation (HasDirDeriv), so "$F'(x;d)\ge 0$" means "exists and is nonnegative". "Exactly one accumulation point" is a unique cluster point, not convergence. "$t_k\downarrow 0$" is read as "positive and tending to $0$", as the report reads it in the proof of Lemma 2. "max" and "min" are attained extrema (IsGreatest, IsLeast), never suprema with default values.

$E$ is a given function constrained by (d) or (d′), not a supremum; this rules out the trivializing formalization in which $E$ is defined as ⨆ u ∈ U, f x u and takes the default value $0$ for an empty or unbounded family. (d) and (d′) force $U\neq\emptyset$. The page's "for each $x\in B$ either (d) and (e) or (d′) and (e′)" is read as one form on all of $B$, as the proof of Theorem 2 treats it, and Theorem 1 is stated as two items. Hypothesis (c) is the sequential accumulation-point form in which Proposition 1(d) glosses upper semicontinuity.

The goal does not assume (b), (c), (e), (e′) or convexity of $B$; the report derives the first four from smoothness. The report claims (b) on all of $B$, which fails for non-convex open $B$ (a bounded gradient gives a uniform Lipschitz constant only on convex sets). The corresponding milestone states (b) on balls contained in $B$, which is all the proof needs.

The development needs Clarke's calculus for Lipschitz functions on $\mathbb R^n$ (Propositions 1 and 2, a Lebourg mean value theorem), a Danskin-type theorem, and the regularity of $C^1$ functions. These are reusable well beyond this mission; a companion mission of the series covers Propositions 1(c), 2 and the chain rule. Contributions are welcome on any milestone, including alternative proofs of Theorem 1.

Selected references

• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, IIASA Research Report RR-76-21, December 1976. https://pure.iiasa.ac.at/id/eprint/524/ (journal version: SIAM J. Control Optim. 15(6) (1977) 959–972, https://doi.org/10.1137/0315061).
• F. H. Clarke, Generalized gradients and applications, Trans. Amer. Math. Soc. 205 (1975) 247–262. https://doi.org/10.1090/S0002-9947-1975-0367131-6
• A. Feuer, An Implementable Mathematical Programming Algorithm for Admissible Fundamental Functions, Ph.D. dissertation, Department of Mathematics, Columbia University, 1974.
• G. Lebourg, Valeur moyenne pour gradient généralisé, C. R. Acad. Sci. Paris Sér. A 281 (1975) 795–797.
• L. Qi and J. Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275

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

1. Lemma 4.4 (descent lemma; already proved on the platform) and Lemma 4.3 (subgradient inequality for weakly convex functions).
2. 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$.
3. The one-step decrease of $f(x_n)/g(x_n)$ that follows from (32).
4. 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.
5. Theorem 6.1(ii): the iterates are bounded and $\sum_n\|x_{n+1}-x_n\|^2<+\infty$.
6. The limit inequality at a cluster point, and inclusion (34) (= (28)).
7. 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

Motivation

Many first-order methods for nonconvex and nonsmooth optimization are analysed with the same template: a merit function decreases by a definite amount at every step, a subgradient of the merit function at the current point is bounded by the step length, and the Kurdyka–Łojasiewicz (KL) property of the merit function turns these two facts into a proof that the whole sequence of iterates has finite length and converges. Attouch and Bolte (Math. Program. 2009), Attouch, Bolte and Svaiter (Math. Program. 2013) and Bolte, Sabach and Teboulle (Math. Program. 2014) isolated this template as a set of abstract conditions. Later frameworks for methods with inertia or extrapolation, such as iPiano (Ochs, Chen, Brox and Pock, SIAM J. Imaging Sci. 2014), needed the relative error bound to involve more than one past step.

Boţ, Dao and Li (arXiv:2003.04124, Math. Oper. Res. 2022) state a framework (H1)–(H5) in which the relative error bound is a convex combination of several step lengths, past or future, plus a summable error, and the iterates of the algorithm may live in a different space from the merit function. They prove finite length, convergence, stationarity and, for KL exponent at most $\tfrac12$, linear rates; they then apply it to an extrapolated proximal subgradient method for fractional programs. This mission formalizes that abstract result, Theorem 5.2 of the paper.

Setting

Let $\mathcal H$ and $\mathcal K$ be finite-dimensional real Hilbert spaces and $h:\mathcal K\to(-\infty,+\infty]$ a proper (never $-\infty$, finite somewhere) lower semicontinuous function. $\partial_L h(z)$ denotes the limiting subdifferential of $h$ at $z$, empty where $h(z)=+\infty$, and $\operatorname{dist}(0,\emptyset)=+\infty$.

Data: sequences $(x_n)$ in $\mathcal H$ and $(z_n)$ in $\mathcal K$; $\alpha_n,\beta_n>0$; $\Delta_n,\varepsilon_n\ge0$, with the convention $\Delta_k=0$ for $k<0$; integers $\underline\imath\le\bar\imath$ (not necessarily positive), $I=\{\underline\imath,\dots,\bar\imath\}$, and weights $\lambda_i\ge0$ with $\sum_{i\in I}\lambda_i=1$. The conditions, for all $n\in\mathbb N$, are:

• (H1) sufficient decrease: $h(z_{n+1})+\alpha_n\Delta_n^2\le h(z_n)$;
• (H2) relative error: $\beta_n\operatorname{dist}(0,\partial_L h(z_n))\le\sum_{i\in I}\lambda_i\Delta_{n-i}+\varepsilon_n$;
• (H3) continuity: some subsequence $z_{k_n}\to\tilde z$ has $h(z_{k_n})\to h(\tilde z)$;
• (H4) parameters: $\underline\alpha:=\inf\alpha_n>0$, $\underline\gamma:=\inf\alpha_n\beta_n>0$, $\sum\varepsilon_n<+\infty$;
• (H5) distance: there are $j\in\mathbb Z$, $c\in\mathbb R$ with $\|x_{n+1}-x_n\|\le c\,\Delta_{n+j}$.

$\Omega$ is the set of cluster points of $(z_n)$, $\Omega_0=\{\bar z\in\Omega:h(z_n)\to h(\bar z)\}$, and $\bar h=h(\bar z)$ for $\bar z\in\Omega_0$. A desingularizing function $\varphi\in\Phi_\eta$ is continuous and concave on $[0,\eta)$, vanishes at $0$, and is $C^1$ with $\varphi'>0$ on $(0,\eta)$. $h$ has the KL property at $\bar z$ if for some neighbourhood $U$ of $\bar z$, $\eta>0$ and $\varphi\in\Phi_\eta$, $\varphi'(h(z)-h(\bar z))\operatorname{dist}(0,\partial_L h(z))\ge1$ whenever $z\in U$ and $h(\bar z)<h(z)<h(\bar z)+\eta$; it has the KL property with exponent $a\in[0,1)$ if $\varphi$ can be taken as $\gamma s^{1-a}$.

Formalization targets

Goal: Theorem 5.2

Assume (H1)–(H4), $(z_n)$ bounded, $h$ constant on $\Omega$ with the KL property at every point of $\Omega$. Then

$$\text{(i)}\ \sum_{n=0}^{\infty}\Delta_n<\infty;\qquad \text{(ii)}\ \text{(H5)}\Rightarrow\sum_{n=0}^{\infty}\|x_{n+1}-x_n\|<\infty \text{ and } x_n\to\bar x;\qquad \text{(iii)}\ \inf\beta_n>0\Rightarrow 0\in\partial_L h(\bar z)\ \ \forall\bar z\in\Omega_0;$$

(iv) if $h$ has KL exponent $a\le\tfrac12$ on $\Omega$, $\underline\imath\le1$, $\inf_{n,i}\alpha_{n-i}\beta_n^2>0$ and $\varepsilon_n/\beta_n=O(\sqrt{h(z_{n-\bar\imath})-h(z_{n+1-\underline\imath})})$, then for some $\gamma_1>0$, $\rho\in(0,1)$,

$$h(z_n)-\bar h\le\gamma_1\rho^n\quad\forall n,$$

and under (H5) and $\sum_{k\ge n}\varepsilon_k=O(\sqrt{h(z_{n-\bar\imath})-\bar h})$, $\|x_n-\bar x\|\le\gamma_2\rho^{n/2}$ for the same $\rho$.

Milestones

Lemma 2.3 (uniformized KL along a bounded sequence, and its power form under an exponent); Lemma 5.1(i)–(iii) (nonemptiness of $\Omega_0$ and monotone convergence of values; $\sum\Delta_n^2\le(h(z_0)-h(\bar z))/\underline\alpha$; the subgradient bound and stationarity); the tail bound (24) from the proof of (i); Theorem 5.2(i); and the first claim of Theorem 5.2(iv).

Significance

The theorem separates what is specific to an algorithm (checking (H1)–(H5) for its iterates) from what is common to all KL-based analyses (finite length, convergence, rates). In the paper it yields global convergence of the extrapolated proximal subgradient method (Theorem 5.5) with $z_n=(x_{n+1},x_n)$ and $I=\{0,1\}$, and Remark 5.4 shows that the frameworks of Attouch–Bolte–Svaiter, Bolte–Sabach–Teboulle, Frankel–Garrigos–Peypouquet and iPiano are special cases, while the linear rate for the iterates in the multi-step setting is new relative to those frameworks.

The result is proved on paper. To our knowledge no machine-checked version of this abstract framework exists. A formal proof yields a reusable theorem: any later mission that verifies (H1)–(H5) for a specific method gets convergence and rates by citation. Related single-algorithm KL convergence results on the platform (proximal alternating minimization, PALM, proximal ADMM) each repeat the same argument; this framework is the common abstraction.

Difficulty

The naive argument—sum (H1) to get $\sum\Delta_n^2<\infty$—gives only square-summability, which does not imply convergence of the iterates. Finite length needs the KL inequality along the whole tail of the sequence with one function $\varphi$, but the KL property is only pointwise; this requires a uniformization over the (compact) cluster set and the restriction to $\Omega_0$, where values converge. The multi-step error with possibly negative indices in $I$ means the right-hand side of (H2) can involve future steps, so the telescoping estimate must absorb sums with shifted index ranges. For the rates, the KL exponent turns the inequality into a recursion between $r_{n+1-\underline\imath}$ and $r_{n-\bar\imath}$ separated by several steps, whose contraction must be shown to give a geometric rate.

Formalization scope

$\mathcal H$ is EuclideanSpace ℝ (Fin N) and $\mathcal K$ is EuclideanSpace ℝ (Fin P); $h$ takes values in EReal, with properness and limiting subdifferential from the published NonconvexSplitting.Shared definitions and the KL property (HasKLProperty, IsDesingularizer, KLIneq) from the published NonconvexSplitting.ADMMKL definitions. $\eta$ is a positive real. $\Delta$ is indexed by $\mathbb Z$ and vanishes on negative integers. $\operatorname{dist}(0,\partial_L h(z))\le r$ is encoded as "some $v\in\partial_L h(z)$ has $\|v\|\le r$", and the KL inequality as "every $v\in\partial_L h(z)$ satisfies $\varphi'(\cdot)\|v\|\ge1$"; Metric.infDist is never used, because it returns $0$ on the empty set where the paper's distance is $+\infty$, which would make (H2) trivially satisfiable. Infima are encoded by positive lower bounds; $O(\cdot)$ hypotheses as eventual bounds with a constant; $\bar h$ by quantifying over $\Omega_0$. Lemma 5.1(ii) assumes $h(z_0)<+\infty$ explicitly, which the page presupposes.

The definitions file FracPSG.Abstract.Basic (the setting, (H1)–(H5), $\Omega$, $\Omega_0$, the KL exponent) is reusable by any mission that instantiates the framework. Contributions welcome: proofs of the milestones, the uniformized KL lemma in general form, and summation lemmas for sequences indexed by $\mathbb Z$.

Selected references

• R. I. Boţ, M. N. Dao, G. Li, Extrapolated Proximal Subgradient Algorithms for Nonconvex and Nonsmooth Fractional Programs, Math. Oper. Res., 2022; preprint arXiv:2003.04124v2 (2020). https://arxiv.org/abs/2003.04124
• 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
• 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, 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
• P. Ochs, Y. Chen, T. Brox, T. Pock, iPiano: Inertial proximal algorithm for nonconvex optimization, SIAM J. Imaging Sci. 7, 2014. https://doi.org/10.1137/130942954