Optimization

Motivation

Many optimization problems in machine learning, signal processing and distributed computation have an objective that is a sum of a large number $m$ of component functions: one per data point, per sensor, or per processor. Evaluating the whole sum, or a subgradient of it, at every iteration is expensive when $m$ is large. Incremental methods process one component at a time, cycling through the components or sampling them, and update the iterate after each one. Incremental gradient and subgradient methods go back to the training of neural networks and to least squares; incremental proximal methods replace the subgradient step of a component by a proximal step, which is more stable and handles nonsmooth terms exactly.

Bertsekas (LIDS-P-2847, 2010, rev. 2011; Math. Program. 129 (2011)) proposed a unified family that mixes the two: each component is split as $F_i=f_i+h_i$, a proximal step is taken on $f_i$ and a subgradient step on $h_i$, followed by a projection onto the constraint set. This mission formalizes the convergence analysis of that family under the cyclic order of component selection.

Timeline. Incremental subgradient methods were analysed by Nedić and Bertsekas (SIAM J. Optim. 12 (2001)) for cyclic and randomized orders. Incremental proximal methods were studied by Bertsekas (Optimization for Machine Learning, 2011, ch. 4). The 2011 paper combines the two analyses; its cyclic-order results are Propositions 3–6.

Setting

Let $\mathbb R^n$ carry the Euclidean norm $\|\cdot\|$ and inner product $x'y$. The data are a nonempty closed convex set $X\subseteq\mathbb R^n$ and real-valued convex functions $f_i,h_i:\mathbb R^n\to\mathbb R$, $i=1,\dots,m$. The problem is

$$\text{minimize } F(x)=\sum_{i=1}^m F_i(x),\qquad F_i=f_i+h_i,\qquad\text{subject to } x\in X,$$

with optimal value $F^*=\inf_{x\in X}F(x)$, possibly $-\infty$, and optimal set $X^*=\{x^*\in X:F(x^*)=F^*\}$, possibly empty.

A subgradient $\tilde\nabla f(x)$ of a convex $f$ at $x$ is a vector $g$ with $f(y)\ge f(x)+g'(y-x)$ for all $y$; $P_X(u)$ is the point of $X$ nearest to $u$. At iteration $k$ one component $i_k$ is processed with stepsize $\alpha_k>0$. The three iterations are

$$\begin{aligned} &(19)\quad z_k=P_X\big(x_k-\alpha_k\tilde\nabla f_{i_k}(z_k)\big),&& x_{k+1}=P_X\big(z_k-\alpha_k\tilde\nabla h_{i_k}(z_k)\big),\\ &(20)\quad z_k=x_k-\alpha_k\tilde\nabla f_{i_k}(z_k),&& x_{k+1}=P_X\big(z_k-\alpha_k\tilde\nabla h_{i_k}(z_k)\big),\\ &(21)\quad z_k=x_k-\alpha_k\tilde\nabla h_{i_k}(x_k),&& x_{k+1}=P_X\big(z_k-\alpha_k\tilde\nabla f_{i_k}(x_{k+1})\big). \end{aligned}$$

The $f$-subgradient is taken at the new point, which makes the $f$-part a proximal step (Proposition 1). In the cyclic order $i_k=(k\bmod m)+1$; a block of $m$ consecutive iterations is a cycle, and $\alpha_k$ is constant within a cycle.

The analysis assumes that the subgradients the iteration uses are bounded by a constant $c$ and that, at each cycle start $k>0$, the function values at the intermediate points of the cycle differ from those at $x_k$ by at most $c$ times the distance (Assumption 1 for (19), (20); Assumption 2 for (21)). Both hold, for example, when all $f_i$, $h_i$ are polyhedral or Lipschitz.

Formalization targets

Goal: Proposition 6

If $\alpha_k\to0$ and $\sum_k\alpha_k=\infty$, then

$$\liminf_{k\to\infty}F(x_k)=F^*,$$

and if moreover $X^*\neq\emptyset$ and $\sum_k\alpha_k^2<\infty$, then $x_k\to x^*$ for some $x^*\in X^*$. Both parts are one item, as in the paper.

Milestones

1. Proposition 1: the proximal iteration over $X$ equals $P_X(x_k-\alpha_k\tilde\nabla f(x_{k+1}))$, and $\|x_{k+1}-y\|^2\le\|x_k-y\|^2-2\alpha_k(f(x_{k+1})-f(y))-\|x_k-x_{k+1}\|^2$ for $y\in X$.
2. Eq. (30) and Eq. (37): one-iteration estimates for (19)/(20) and for (21).
3. Proposition 3: over one cycle, $\|x_{k+m}-y\|^2\le\|x_k-y\|^2-2\alpha_k(F(x_k)-F(y))+\alpha_k^2\beta m^2c^2$, with $\beta=\frac1m+4$ for (19), (20) and $\beta=\frac5m+4$ for (21).
4. Footnote 5: nonnegative sequences with $Y_{k+1}\le Y_k-Z_k+W_k$ and $\sum W_k<\infty$ have $Y_k$ convergent.
5. Proof of Proposition 6: $\|x_{k+1}-x_k\|\le2\alpha_kc$.
6. Proposition 4 (constant stepsize $\alpha$): $\liminf F(x_k)=F^*$ if $F^*=-\infty$, and $\liminf F(x_k)\le F^*+\alpha\beta m^2c^2/2$ otherwise.

Significance

Proposition 6 is the exact-convergence guarantee for the cyclic incremental subgradient-proximal methods: with a diminishing, non-summable stepsize they reach the optimal value whatever the starting point, and with square-summable stepsizes the iterates converge to a single optimal solution. It covers the pure incremental subgradient method ($f_i=0$) and the pure incremental proximal method ($h_i=0$) as special cases, and it is the template for the randomized-order analysis of the companion mission. Proposition 4 quantifies what a constant stepsize achieves.

These results are proved in the paper. None of them, nor the underlying estimates, is formalized on the platform or, to our knowledge, in Mathlib. The mission produces machine-checked versions of the proximal-step lemma for extended-real-valued functions on a constrained set, of the cycle estimate (27) with its explicit constants, and of the deterministic supermartingale convergence lemma, all reusable for other incremental and proximal methods.

Difficulty

The obvious argument treats one cycle as one step of a subgradient method on $F$. It fails because within a cycle the subgradients are taken at the intermediate points $z_{k+j-1}$ or $x_{k+j-1}$, not at $x_k$, and the proximal steps use subgradients at the points they produce. The error between $F_j(x_k)$ and $F_j$ at those points must be controlled through the drift of the iterates during the cycle, and the bookkeeping differs between (19)/(20) and (21), which is why $\beta$ differs. For the second part of Proposition 6, convergence of the values in the $\liminf$ sense does not by itself give convergence of the iterates, and $X^*$ may contain more than one point.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Components are Fin m (0-based), so $i_k$ is k % m, and the paper's $j=1,\dots,m$ with $z_{k+j-1}$ becomes $j=0,\dots,m-1$ with z (k + j). $m\ge1$ is assumed (NeZero m).
• $P_X$ is a predicate (IsProj: a nearest point of $X$), not a choice function.
• Each iteration is a relation Step between $x_k$, $z_k$, $x_{k+1}$ and the two subgradients it uses, with the $f$-subgradient at the point the paper names. A run records these subgradients, so Assumptions 1–2 bound exactly them. The assumptions are not replaced by Lipschitz continuity, which is only a sufficient condition (p. 9).
• $F^*$ and $\liminf F(x_k)$ are taken in EReal; $F^*=-\infty$ is allowed and no boundedness is assumed.
• The standing assumptions of p. 4 (X nonempty closed convex, $f_i,h_i$ convex), positive stepsizes, constancy within a cycle and Assumptions 1–2 (stated "throughout this section", p. 8) are explicit hypotheses of every statement, including the goal, whose sentence does not repeat them.
• The starting point $x_0$ is arbitrary, as in the paper. Assumptions 1–2 make the cycle-start conditions only for $k>0$, and the bound $\|x_{k+1}-x_k\|\le2\alpha_kc$ needs $x_k\in X$, which holds from $k=1$ on. Proposition 3 and the step bound are therefore stated for $k>0$ and $k\ge1$; this does not affect Propositions 4 and 6.
• Proposition 1 is stated for extended-real-valued closed proper convex $f$, as in the paper, using the published class $\Gamma_0$ (MoreauProx.Characterization.GammaZero) and its subgradients, with relative interiors as Mathlib's intrinsicInterior.

The goal cannot be satisfied vacuously: a sorry-free check confirms that the hypotheses hold together (for $n=1$, $m=2$, $X=\mathbb R$, $\alpha_k=1/(\lfloor k/2\rfloor+1)$, $X^*\neq\emptyset$). Restricting to Lipschitz components, to bounded-below $F$, or to $x_0\in X$ would state a weaker theorem and is ruled out.

Proofs of any item are welcome, as are general lemmas (the projection theorem as a variational inequality, the subdifferential sum rule under the relative-interior condition) that the proofs need.

Selected references

• D. P. Bertsekas, Incremental Proximal Methods for Large Scale Convex Optimization, Report LIDS-P-2847, MIT, 2010 (rev. March 2011); Math. Program. 129(2) (2011) 163–195. https://doi.org/10.1007/s10107-011-0472-0
• A. Nedić, D. P. Bertsekas, Incremental Subgradient Methods for Nondifferentiable Optimization, SIAM J. Optim. 12(1) (2001) 109–138. https://doi.org/10.1137/S1052623499362111
• D. P. Bertsekas, Incremental Gradient, Subgradient, and Proximal Methods for Convex Optimization: A Survey, in Optimization for Machine Learning, MIT Press, 2011. https://arxiv.org/abs/1507.01030
• D. P. Bertsekas, A. Nedić, A. E. Ozdaglar, Convex Analysis and Optimization, Athena Scientific, 2003.

Motivation

A finite-sum optimization problem asks for one vector that performs well across many component objectives. In empirical risk minimization, each component can represent the loss from one data point. A full gradient uses every component, whereas a stochastic gradient uses one component and can be much cheaper per step. The latter carries sampling noise, so a method must control that noise while moving toward the optimum. Allen-Zhu's Katyusha paper gives a direct accelerated stochastic method for this setting. Its strongly convex result, Theorem 2.1, bounds the expected objective error of a specified algorithm after a specified number of epochs.

The problem is relevant when the number of terms is large enough that a full gradient at every iteration is costly, but individual component gradients and proximal steps remain practical. Katyusha combines a periodically refreshed full gradient with individual component gradients. The paper's result concerns the actual returned snapshot of Algorithm 1, Option I, whose weighted averaging rule matters to the claim. Formalizing a generic noisy gradient method would leave the paper's central algorithmic guarantee unstated.

Setting

Let $f_1,\ldots,f_n:\mathbb R^d\to\mathbb R$ be differentiable functions, with $n\ge1$. Their finite-sum objective is $f(x)=n^{-1}\sum_{i=1}^n f_i(x)$. A real-valued regularizer $\psi$ gives the composite objective

$$F(x)=f(x)+\psi(x).$$

Each $f_i$ is convex and $L$ smooth: its gradient is $L$ Lipschitz in the Euclidean norm. The regularizer is $\sigma$ strongly convex, with $L,\sigma>0$, in the paper's convention that the quadratic term has coefficient $\sigma/2$. The comparison point $x^*$ minimizes the full objective $F$.

Algorithm 1 starts from $x_0$ and keeps three vectors: a snapshot $\widetilde x$, a proximal sequence $z$, and another proximal sequence $y$. In each epoch it computes $\nabla f(\widetilde x)$. At a current point $x$, it samples $i$ uniformly from $\{1,\ldots,n\}$ and forms the gradient estimator

$$\widetilde\nabla=\nabla f(\widetilde x)+\nabla f_i(x)-\nabla f_i(\widetilde x).$$

The algorithm then makes two proximal updates using $\widetilde\nabla$ and $\psi$. Its next snapshot is a weighted average of the new $y$ values, with weights $(1+\alpha\sigma)^j$ for $j=0,\ldots,m-1$. The iterates $y$ and $z$ persist between epochs. In the theorem's run the epoch length is $m=2n$, and $\tau_2=1/2$, $\tau_1=\min\{\sqrt{m\sigma}/\sqrt{3L},1/2\}$, and $\alpha=1/(3\tau_1L)$. The output after $S$ epochs is $\widetilde x^S$.

Formalization targets

Theorem 2.1: objective error after $S$ epochs

For every starting point $x_0$ and minimizer $x^*$ of $F$, the target is the paper's two-case expected bound:

$$\mathbb E F(\widetilde x^S)-F(x^*)\le\begin{cases}4(1+\sqrt{\sigma/(3Lm)})^{-Sm}\bigl(F(x_0)-F(x^*)\bigr),&m\sigma/L\le3/4,\\3(2/3)^S\bigl(F(x_0)-F(x^*)\bigr),&m\sigma/L>3/4.\end{cases}$$

The expectation is over every independent uniform index sampled by the run. The two regimes meet at the threshold where the algorithm's minimum defining $\tau_1$ changes branch. The milestone list follows Lemmas 2.3–2.7 and the displayed one-epoch inequalities of Section 2.2. It includes the variance bound, the proximal estimates, and the two regime-specific epoch estimates that feed the final theorem.

Significance

The theorem gives an accelerated linear reduction of the expected composite-objective error under the paper's strong convexity assumptions. It identifies how the rate depends on component count $n$, smoothness $L$, strong convexity $\sigma$, and epoch count $S$. The author also translates the result into an iteration-complexity statement and uses it as a basis for later reductions and generalizations in the paper. The objective-error theorem is the stable mathematical claim formalized here; the complexity paraphrase is outside this mission's Lean goal.

Allen-Zhu proved Theorem 2.1 in the paper. The Lean declarations in this proposal are targets with proof placeholders, not machine-checked proofs of Katyusha's convergence. Completing them would produce a checked account of the exact algorithm, its finite probability space, and the conditional inequalities for an epoch. The finite-sum and proximal-point definitions reused here are already published in the SAGA formalization; Katyusha's weighted snapshot and coupling statements require their own development.

Difficulty

The estimator is unbiased, but that fact alone does not give the claimed acceleration. Its variance depends on the snapshot and current point, and a direct descent estimate retains a variance penalty. The bound in Lemma 2.4 expresses that penalty through a smooth convex gap which can have either sign before it is combined with other terms. The two proximal sequences and the snapshot therefore have to be accounted for together. Across an epoch, the $y$ iterates are averaged with nonuniform weights, while $y$ and $z$ themselves are carried into the next epoch. Replacing the snapshot with the final $y$ value or with a uniform average changes the algorithm and the theorem.

The two rate cases also reflect different parameter values. When $m\sigma/L\le3/4$, $\tau_1$ is determined by a square root; above that threshold it is fixed at $1/2$. A proof of only one branch would omit part of the source result. Treating the sampled indices as a single arbitrary path would ask for a false pathwise guarantee, whereas stating the result for a favorable path would lose the expectation bound.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d) and component indices are Fin n, translating the paper's one-based $\{1,\ldots,n\}$ to a zero-based finite type. The goal fixes $m=2n$ as Algorithm 1 does; the conditional one-epoch statements admit any positive $m$. The number of epochs $S$ can be zero, in which case the output is the initial snapshot. The objective is real-valued. Thus $\psi$ may be nondifferentiable but does not include extended-valued indicator functions. The component gradient fields are required to be the actual gradients of their functions, and the comparison point minimizes $F$, not merely $f$.

A proximal map $P(\gamma,\cdot)$ is an explicit argument constrained, for every $\gamma>0$, to minimize the proximal objective of the given $\psi$. The run computes the paper's two proximal updates with that map. The expectation is the finite uniform average over all $n^{Sm}$ sequences, equivalent to $Sm$ independent uniform samples. It never quantifies over a convenient sequence. These links prevent a vacuous or unrelated encoding of the method.

The paper writes both rates using $O(\cdot)$. Its Section 2.2 bounds yield the concrete coefficient $4$ in the square-root regime and $3$ in the $1.5^{-S}$ regime; these are the expressions in the Lean goal. For Case 1 the rate is represented by division by $(1+\sqrt{\sigma/(3Lm)})^{Sm}$, a positive denominator. For Case 2 it is $3(2/3)^S$. The statement retains both conclusions at their stated boundary. The one-step lemmas average only a fresh sampled index with the current state fixed, and the epoch statements average the current epoch's $m$ indices.

The development needs finite sums and finite expectations, Euclidean smooth and strong convexity facts, proximal minimizer inequalities, and algebra of the weighted snapshot. The finite-sum objective, averaged gradient, proximal-point predicate, and finite index expectation are shared definitions; the Katyusha run, progress value, potential, and epoch inequalities are specific to this algorithm. Contributions proving the milestone statements, establishing existence and uniqueness of the proximal map under these assumptions, or improving reusable proximal and finite-expectation lemmas are within scope.

Selected references

• Zeyuan Allen-Zhu, Katyusha: The First Direct Acceleration of Stochastic Gradient Methods, Journal of Machine Learning Research 18 (2018), 1–51; arXiv:1603.05953v6. The formalization uses the pinned arXiv version, pp. 1, 6–13.
• Aaron Defazio, Francis Bach, and Simon Lacoste-Julien, SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives, Advances in Neural Information Processing Systems 27 (2014); arXiv:1407.0202. The published finite-sum and proximal-point definitions are reused as common objects.

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

Nonlinear model predictive control (NMPC) computes a feedback law by solving, at every sampling time, an optimal control problem that starts from the currently measured state. The control actually applied is the first control of that problem's solution. When the dynamics are fast relative to the time an optimizer needs, solving each problem to convergence is impossible, and the delay between measuring the state and applying the control degrades or destabilises the closed loop.

Diehl, Bock and Schlöder (SIAM J. Control Optim. 43(5), 2005) analysed the real-time iteration: a scheme that performs a single Newton-type iteration per sampling time and then moves on to the next problem. The scheme is the basis of widely used NMPC software (for example the ACADO toolkit and acados) and of much of the later theory on suboptimal and "anytime" MPC. The paper's Theorem 4.1 is the first contraction result for it; Theorem 5.1 bounds the price paid in closed-loop cost for not solving each problem to optimality.

Setting

A discrete-time system $x_{k+1}=f_k(x_k,u_k)$, $k=0,\dots,N-1$, has states $x_k\in\mathbb R^{n_x}$ and controls $u_k\in\mathbb R^{n_u}$. For $k\le N$ and a state $x_k$, the shrinking-horizon problem $P_k(x_k)$ is

$$\min\ \sum_{i=k}^{N-1}L_i(s_i,q_i)+E(s_N)\quad\text{s.t.}\quad x_k-s_k=0,\quad f_i(s_i,q_i)-s_{i+1}=0\ \ (i=k,\dots,N-1).$$

Its primal-dual vector is $y=(\lambda_k,s_k,q_k,\dots,\lambda_N,s_N)\in\mathbb R^{n_k}$ and its Lagrangian is

$$\mathcal L^k(y)=\sum_{i=k}^{N-1}L_i(s_i,q_i)+E(s_N)+\lambda_k^T(x_k-s_k)+\sum_{i=k}^{N-1}\lambda_{i+1}^T\big(f_i(s_i,q_i)-s_{i+1}\big).$$

The projection $\Pi^{k+1}:\mathbb R^{n_k}\to\mathbb R^{n_{k+1}}$ drops the block $(\lambda_k,s_k,q_k)$.

A Newton-type method solves $\nabla_y\mathcal L^k(y)=0$ by steps $\Delta y=-J^k(y)^{-1}\nabla_y\mathcal L^k(y)$, where $J^k(y)$ is the KKT matrix $\nabla^2_y\mathcal L^k(y)$ with its Hessian blocks $\nabla^2_{(s_i,q_i)}\mathcal L^k$ (and the terminal block) replaced by approximations, for instance those of the constrained Gauss–Newton method. The real-time iteration starts from a guess $y^0$ and, for $k=0,1,\dots$, computes $\Delta y^k=-J^k(y^k)^{-1}\nabla_y\mathcal L^k(y^k)$ for $P_k(x_k)$, applies $u_k:=q^k_k+\Delta q^k_k$, lets the system evolve to $x_{k+1}=f_k(x_k,u_k)$, and sets $y^{k+1}:=\Pi^{k+1}(y^k+\Delta y^k)$.

The analysis uses a neighbourhood $D_0\ni y^0$ and its projections $D_{k+1}:=\Pi^{k+1}D_k$, norms $\|\cdot\|_k$ on $\mathbb R^{n_k}$ with $\|\Pi^{k+1}y\|_{k+1}\le\|y\|_k$ and $\|(\Pi^{k+1})^T\tilde y\|_k=\|\tilde y\|_{k+1}$, two constants $\kappa$ (the Hessian approximation error) and $\omega$ (a Lipschitz-type constant of $J^k$), the rates $\delta_k:=\kappa+\frac\omega2\|\Delta y^k\|_k$, and the ball $B_0:=\{y:\|y-y^0\|_0\le\|\Delta y^0\|_0/(1-\delta_0)\}$.

Formalization targets

Goal: Theorem 4.1 (local contractivity)

Assume $\mathcal L^k$ is twice continuously differentiable on $D_k$, $J^k$ is continuous with bounded inverse on $D_k$, the conditions (4.1a)–(4.1c) hold with $\kappa<1$, $\delta_0<1$ and $B_0\subseteq D_0$. Then for $k=0,\dots,N$

$$y^k\in\Pi^k\cdots\Pi^1B_0\subseteq D_k,\tag{4.2}$$

for $k=0,\dots,N-1$

$$\|\Delta y^{k+1}\|_{k+1}\le\Big(\kappa+\frac\omega2\|\Delta y^k\|_k\Big)\|\Delta y^k\|_k=\delta_k\|\Delta y^k\|_k\le\delta_0\|\Delta y^k\|_k,\tag{4.3}$$

and the Newton-type iterates of $P_k(x_k)$ started at $y^k$ converge to a stationary point $y^k_*$ with

$$\|y^k-y^k_*\|_k\le\frac{\|\Delta y^k\|_k}{1-\delta_k}\le\frac{(\delta_0)^k\|\Delta y^0\|_0}{1-\delta_0}.\tag{4.4}$$

No constant is chosen by the formalization: all of them are the paper's.

Milestones

The proof has three parts (contraction, well-definedness, distance to the stationary points). The milestones are its steps: the gradient transition identity between consecutive problems; the block identity $\Pi^{k+1}(\nabla^2\mathcal L^k-J^k)=(\nabla^2\mathcal L^{k+1}-J^{k+1})\Pi^{k+1}$; the one-step contraction; the recursion $\delta_{k+1}\le\delta_k\le\delta_0$; the lifting of a nearby point of $\mathbb R^{n_k}$ to $B_0$; the contraction (4.7) of the Newton-type method on a fixed problem; and the convergence of those iterates to $y^k_*$.

Companion: Theorem 5.1 (loss of optimality)

If moreover $\|\nabla^2_y\mathcal L^0\|\le C$ on $B_0$, then $F_{\rm real}\le F_{\rm opt}+2C\big(\frac{\delta_0}{1-\delta_0}\big)^2\|\Delta y^0\|_0^2$, and for $\kappa=0$ the loss is $\frac C2\big(\frac{\omega}{1-\frac\omega2\|\Delta y^0\|_0}\big)^2\|\Delta y^0\|_0^4$. The intermediate estimate (5.4), $\|y_{\rm real}-y^0_*\|_0\le2\delta_0\|\Delta y^0\|_0/(1-\delta_0)$, is a separate item.

Significance

Theorem 4.1 says that a scheme which never solves any problem to convergence still produces iterates that contract at the rate of the underlying Newton-type method and approach the exact solutions of the problems along the closed loop, geometrically. It justifies the "one iteration per sample" design of real-time NMPC under explicit, checkable conditions on the Hessian approximation, and its constants $\kappa,\omega$ are those of the classical affine-invariant Newton-type convergence theory, so it extends to Gauss–Newton and other approximations. Theorem 5.1 turns the contraction into a closed-loop performance guarantee: the suboptimality is quadratic in the first step, quartic for exact Newton.

The results are proved in the paper; none is formalized. A formal proof would supply the details the paper leaves implicit (that the segments used by the integral mean value theorem stay in the domains, that the ball $B_k$ around $y^k$ lies in $D_k$), would give a reusable Lean model of discrete-time optimal control problems with their KKT structure and shrinking-horizon projections, and would make the classical local contraction argument for Newton-type methods available for general norms.

Difficulty

Each single estimate is a variant of the textbook local convergence proof for Newton-type methods. The difficulty is that the real-time iteration changes the problem at every step: the next step is computed for a different, smaller problem at a different initial state, so the textbook argument does not apply as is. The proof needs two structural facts that tie consecutive problems together, the gradient transition along the undisturbed closed loop and the block identity of the Hessian errors, together with the compatibility of the norms with the projections. A second obstacle is well-definedness: the iterates must be shown to stay in regions where the hypotheses hold, which requires tracking the projections of $B_0$ through all shrinking spaces.

Formalization scope

$\mathbb R^{n_k}$ is a Euclidean space whose coordinates are indexed by (multiplier, state or control block, stage, component) for the stages $\ge k$; $\Pi^{k+1}$ is a restriction and its transpose the extension by zero. The gradient and Hessian are Mathlib's gradient and fderiv; the inverse is ContinuousLinearMap.inverse. The approximations of the stage Hessian blocks depend on $(s_i,q_i,\lambda_{i+1})$ (the paper's misprinted $\lambda_{k+1}$ read as $\lambda_{i+1}$), the terminal block may be approximated as in §2.2, and symmetry of the approximations is not required. The norms $\|\cdot\|_k$ are a structure carrying the norm axioms and the two compatibility conditions. The real-time iterates follow the undisturbed closed loop. The hypotheses (4.1a)–(4.1c) are imposed at the points of $D_k$ where the paper's functions are defined, that is, for $t$ with $y+t\Delta y\in D_k$; no convexity of $D_0$ is assumed. Theorem 5.1 is stated with Euclidean norms on every $\mathbb R^{n_k}$, because its last step bounds $z^TMz$ by $\|M\|\|z\|^2$; $F_{\rm opt}$ is the objective at the primal part of $y^0_*$, not an infimum.

Mathlib's inverse is $0$ at a non-invertible operator and its derivative is $0$ at non-differentiable points; either junk value would make every step vanish and every bound trivial. The statements therefore require invertibility and twice continuous differentiability at the points of $D_k$, keep the membership (4.2) as a conclusion, and pin $y^k_*$ as the limit of the Newton-type scheme started at $y^k$, so it cannot be chosen after the fact. Degenerate norms are excluded by the norm axioms.

Some milestones add a hypothesis that Theorem 4.1 supplies internally: a segment $[y,y+\Delta y]\subseteq D_k$, the ball around the starting point contained in $D_k$, or $\omega\ge0$ for the abstract δ-recursion. Contributions welcome: proofs of the milestones, a sorry-free instance of the hypotheses for a linear-quadratic problem, and general lemmas on the integral mean value theorem for gradients in arbitrary norms.

Selected references

• M. Diehl, H. G. Bock, J. P. Schlöder, A real-time iteration scheme for nonlinear optimization in optimal feedback control, SIAM J. Control Optim. 43(5):1714–1736, 2005. https://doi.org/10.1137/S0363012902400713
• P. Deuflhard, Newton Methods for Nonlinear Problems: Affine Invariance and Adaptive Algorithms, Springer Series in Computational Mathematics 35, 2004 (softcover reprint 2011). https://doi.org/10.1007/978-3-642-23899-4
• B. Houska, H. J. Ferreau, M. Diehl, ACADO toolkit — An open-source framework for automatic control and dynamic optimization, Optimal Control Applications and Methods 32(3):298–312, 2011. https://doi.org/10.1002/oca.939

Motivation

Retailers decide which product variants to stock, and most assortment-planning tools model consumer choice with the multinomial logit (MNL) model: a consumer who does not find an acceptable variant simply leaves without buying. Cachon, Terwiesch and Xu (Retail Assortment Planning in the Presence of Consumer Search, working paper of December 2002; published in MSOM 7(4), 2005, doi:10.1287/msom.1050.0088) point out that consumers also search: a consumer who likes what the store offers may still walk out to look elsewhere, and that is more likely when the assortment is narrow.

In practice a retailer does not know consumer preferences; it estimates them from sales data and re-plans. This mission formalizes §5.1 of the paper, which asks what happens when a retailer runs this estimate-and-replan loop with the traditional no-search MNL model while consumers actually search. The loop can settle at a heuristic equilibrium in the sense of Cachon and Kok (2002), and the question is how that equilibrium compares with the truly optimal assortment.

Setting

There are $n$ product variants, labelled from most to least popular, with preferences $v_1\ge v_2\ge\dots\ge v_n>0$, and a no-purchase option ("variant 0") with preference $v_0>0$. An assortment of depth $x\in\{0,\dots,n\}$ is the set $\{1,\dots,x\}$. Variant $i$ has margin $m_i$, with $m_j\ge m_k$ whenever $v_j\ge v_k$ (monotone margins, p. 6), and carrying it at demand $q$ incurs an operational cost $c(q)$, where $c$ is concave and increasing on $[0,1]$ (demand is normalised to one consumer).

True demand: the independent assortment model. With a constant $\lambda>0$ (Theorem 1 of the paper: $\lambda=\exp[-(\bar U/\mu+\gamma)]$) and $V_x=v_0+\sum_{j=1}^{x}v_j$, the probability that a consumer searches is $H(x)=e^{-\lambda V_x}$, and variant $i\le x$ has demand

$$d_i(x)=\frac{v_i}{V_x}\,\bigl(1-H(x)\bigr).$$

The no-purchase demand is $d_0(x)=1-\sum_{i=1}^{x}d_i(x)$, and the true profit is $\pi(x)=\sum_{i=1}^{x}\bigl(m_i d_i(x)-c(d_i(x))\bigr)$.

Estimates. Observing $d_0(x),\dots,d_x(x)$ for $x\ge1$, the retailer fits the MNL model, normalised by $\hat v_1(x)=1$: $\hat v_i(x)=d_i(x)/d_1(x)$ for $0\le i\le x$, and for variants not carried it reuses the estimates $\hat v_i(n)$ from an initial depth test with the full assortment. The no-search model fed with preferences $w$ predicts the shares $q_i^m(x\mid w)=w_i/(w_0+\sum_{j\le x}w_j)$ and the profit $\pi(x\mid w)=\sum_{i\le x}\bigl(m_i q_i^m(x\mid w)-c(q_i^m(x\mid w))\bigr)$.

Heuristic equilibrium. A depth $1\le x^*\le n$ is a heuristic equilibrium when $x^*$ maximises $\pi(\cdot\mid\hat v(x^*))$ over $0,\dots,n$: the assortment is optimal for the estimated preferences, and the estimates are those observed under the assortment. An optimal depth $x^o$ maximises the true profit $\pi$ over $0,\dots,n$.

Formalization targets

Goal: Theorem 8 (p. 23)

If $x^*$ is a heuristic equilibrium and $x^o$ is an optimal depth such that every deeper depth is strictly worse ($\pi(x)<\pi(x^o)$ for $x^o<x\le n$), then

$$x^*\le x^o.$$

Milestones

• IIA among product variants (p. 21): $d_i(x)/d_j(x)=v_i/v_j$ for $i,j$ in the assortment.
• Correct relative estimates (p. 21): $\hat v_i(x)/\hat v_j(x)=v_i/v_j$ for all product variants $0<i<j\le n$.
• No-purchase ratio (p. 21): $\dfrac{d_0(x)}{d_i(x)}=\dfrac{q_0^m(x)+\sum_{j\le x}q_j^m(x)H(x)}{q_i^m(x)(1-H(x))}$.
• $Z$ is decreasing (proof of Theorem 7): $Z(\delta)=\delta e^{-\lambda\delta}/(1-e^{-\lambda\delta})$ is non-increasing on $(0,\infty)$.
• Theorem 7 (p. 22): for $1\le x\le n$,

$$d_0(x')\ge q_0^m(x'\mid\hat v(x))\ \ (x'<x),\qquad d_0(x'')\le q_0^m(x''\mid\hat v(x))\ \ (x<x''\le n).$$

• Exact prediction at the estimating assortment: $\pi(x)=\pi(x\mid\hat v(x))$.
• No loss-making variant at equilibrium: $m_iq_i^m(x^*\mid\hat v(x^*))-c(q_i^m(x^*\mid\hat v(x^*)))\ge0$ for $i\le x^*$.
• Over-estimation of narrower assortments: $\pi(x)\le\pi(x\mid\hat v(x^*))$ for $1\le x<x^*$.

Significance

Theorem 8 says that a retailer who ignores consumer search and plans iteratively from its own sales data can only err on the side of a too-narrow assortment, never a too-deep one. The bias is structural: Theorem 7 shows that the estimates get every product variant's relative preference right but misjudge the no-purchase option in a direction fixed by the depth. The result thus separates the part of the MNL model that survives consumer search (IIA among products) from the part that does not (IIA with respect to the no-purchase option).

The results are proved in the paper, by short arguments, but some steps are only asserted: the non-negativity of variant profits at the equilibrium is attributed to "the previous section", and the overlapping assortment model is dismissed with "the similar process". No machine-checked proof of these results is known. A formalization makes explicit the hypotheses the paper leaves implicit ($c(0)\ge0$, and a strict-deeper condition on $x^o$ in place of the presumed uniqueness of the optimum), and delivers a reusable formal model of MNL estimation under search.

Difficulty

Each step is elementary, and the difficulty lies in keeping two profit functions apart and carrying the right inequalities between them. The tempting shortcut, "the estimates are correct, so the no-search optimum is the true optimum", fails: the estimates are correct only up to the no-purchase preference $\hat v_0(x)$, which depends on $x$, and that single number shifts every predicted share. The proof of Theorem 7 must reduce the comparison of $\hat v_0(x')$ and $\hat v_0(x)$ to the monotonicity of the function $Z$. The step from no-purchase demand to profit needs every predicted variant profit to be non-negative, which requires the monotone labelling of preferences and margins together with concavity of $c$ and $c(0)\ge0$; the paper asserts it without proof.

Formalization scope

• Variants are Fin n, 0-based: the paper's variant $i$ is index $i-1$. Depths are natural numbers, and depth $x$ is the published RetailVariety.Structure.popularSet n x; the MNL share is the published RetailVariety.Structure.share.
• The no-purchase option is not an element of Fin n; its preference $v_0$ and estimate $\hat v_0(x)$ are separate reals.
• $\lambda>0$ is a free parameter standing for Theorem 1's $\exp[-(\bar U/\mu+\gamma)]$; the results use only $\lambda>0$.
• $c:\mathbb R\to\mathbb R$ is concave and monotone on $[0,1]$, with the added hypothesis $c(0)\ge0$. Margins and preferences are antitone in the index (the paper's standing assumptions, pp. 5–6).
• The estimates are defined by the closed-form solution of the paper's linear system; for variants not carried, by the depth-test values $\hat v_i(n)$. They are used only for $1\le x\le n$.
• Optimality, for both $x^*$ (predicted profit) and $x^o$ (true profit), is over depths $0,\dots,n$, as in the paper's proof.
• Only the independent assortment model is formalized. The overlapping model is asserted by the paper with "the similar logic" and "the similar process", and would also need the search threshold $\bar U(x)$ to be monotone in $x$, which the paper asserts on p. 17 without proof.

Trivializing formalizations are ruled out: the estimates are not the true preferences (in particular $\hat v_0\ne v_0$, which would force $x^*=x^o$); $x^o$ is not an arbitrary maximiser but one with all deeper depths strictly worse; $x^*=0$, where nothing is observed, is excluded rather than given junk estimates; and nothing is claimed for the overlapping model.

Contributions welcome: proofs of the milestones, in particular Theorem 7 and the positivity step, and a formal treatment of the overlapping model with its additional hypotheses.

Selected references

• G. P. Cachon, C. Terwiesch, Y. Xu, Retail Assortment Planning in the Presence of Consumer Search, working paper, The Wharton School, December 20, 2002 (the version cited here); published in Manufacturing & Service Operations Management 7(4):330–346, 2005. https://doi.org/10.1287/msom.1050.0088
• G. P. Cachon, A. G. Kok, Heuristic equilibrium in the newsvendor model with clearance pricing, working paper, 2002; published in Management Science 53(3):934–951, 2007. https://doi.org/10.1287/mnsc.1060.0661
• G. J. van Ryzin, S. Mahajan, On the relationship between inventory costs and variety benefits in retail assortments, Management Science 45(11):1496–1509, 1999. https://doi.org/10.1287/mnsc.45.11.1496