Optimization

Motivation

Minimizing a smooth function over a closed convex set $\Omega\subseteq\mathbb R^n$ on which projection is cheap (a box, a ball, a simplex) is a routine subproblem in large-scale optimization. Box-constrained minimization is the inner solver of augmented Lagrangian methods, and bound-constrained least squares, image restoration and density estimation all have this form. The classical gradient projection method of Goldstein and of Levitin and Polyak needs only gradients and projections, but with constant or monotone Armijo step lengths it is slow.

Spectral projected gradient (SPG) methods, introduced by Birgin, Martínez and Raydan (paper), combine three ingredients. The first is the projection. The second is the Barzilai–Borwein (spectral) step length $\alpha_{k+1}=\langle s_k,s_k\rangle/\langle s_k,y_k\rangle$, an inverse Rayleigh quotient of the average Hessian along the last step. The third is the nonmonotone line search of Grippo, Lampariello and Lucidi, which compares a trial value with the worst of the last $M$ objective values instead of the current one. The paper defines two variants. This mission concerns SPG1, which backtracks along the projection arc $\lambda\mapsto P(x_k-\lambda g(x_k))$, as in Bertsekas's analysis of the Armijo rule for gradient projection. The companion mission concerns SPG2, which backtracks along a fixed feasible direction.

Timeline:

• 1964–1966: Goldstein; Levitin and Polyak introduce gradient projection.
• 1976: Bertsekas analyses the Armijo rule along the projection arc (IEEE TAC).
• 1986: Grippo, Lampariello and Lucidi introduce the nonmonotone line search for unconstrained problems.
• 1988: Barzilai and Borwein propose the two-point step size. Raydan (1997) combines it with nonmonotone search in the unconstrained case.
• 2000: Birgin, Martínez and Raydan define SPG1 and SPG2 for convex constraints (SIAM J. Optim. 10(4)).
• 2003: the same authors publish the convergence analysis that the proof of Theorem 2.2 adapts, in the inexact setting (IMA J. Numer. Anal. 23).

Setting

Let $\Omega\subseteq\mathbb R^n$ be nonempty, closed and convex, with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $f$ have continuous partial derivatives on an open set $U\supseteq\Omega$, and write $g(x)=\nabla f(x)$. The orthogonal projection $P(z)$ is the unique point of $\Omega$ nearest to $z$. The scaled projected gradient is $g_t(x)=P(x-t\,g(x))-x$ for $x\in\Omega$ and $t>0$. A point $\bar x$ is a constrained stationary point if $\langle g(\bar x),x-\bar x\rangle\ge0$ for all $x\in\Omega$.

The parameters are an integer $M\ge1$, reals $0<\alpha_{\min}<\alpha_{\max}$, a sufficient-decrease constant $\gamma\in(0,1)$ and safeguards $0<\sigma_1<\sigma_2<1$. Algorithm SPG1 (Algorithm 2.1) starts from $x_0\in\Omega$ and $\alpha_0\in[\alpha_{\min},\alpha_{\max}]$. At iteration $k=0,1,\dots$ it does the following.

1. Stop test. If $\|P(x_k-g(x_k))-x_k\|=0$, stop: $x_k$ is stationary.
2. Backtracking along the projection arc. Set $\lambda=\alpha_k$. While the trial point $x_+=P(x_k-\lambda g(x_k))$ fails

$$f(x_+)\le\max_{0\le j\le\min\{k,M-1\}}f(x_{k-j})+\gamma\langle x_+-x_k,g(x_k)\rangle,\qquad(1)$$

replace $\lambda$ by any $\lambda_{\rm new}\in[\sigma_1\lambda,\sigma_2\lambda]$. When (1) holds, set $\lambda_k=\lambda$ and $x_{k+1}=x_+$. 3. Spectral step. With $s_k=x_{k+1}-x_k$, $y_k=g(x_{k+1})-g(x_k)$ and $b_k=\langle s_k,y_k\rangle$, set $\alpha_{k+1}=\alpha_{\max}$ if $b_k\le0$, and otherwise $\alpha_{k+1}=\min\{\alpha_{\max},\max\{\alpha_{\min},\langle s_k,s_k\rangle/b_k\}\}$.

The first trial of each backtracking is the spectral step $\alpha_k$, not $1$. The sufficient-decrease term in (1) is $\gamma\langle x_+-x_k,g(x_k)\rangle=\gamma\langle g(x_k),g_\lambda(x_k)\rangle$, with no factor $\lambda$.

In Lean these objects are written as follows:

• the projection is a function P with the predicate IsProjOnto Ω P;
• $g_t$ is scaledProjGrad P f t;
• stationarity is IsConstrainedStationary Ω f;
• the maximum in (1) is nonmonotoneRef f x M k;
• test (1) is SPG1Test;
• an infinite run is IsSPG1Run Ω f P M αmin αmax γ σ₁ σ₂ x α.

Formalization targets

Goal: Theorem 2.2, accumulation points are stationary

For every infinite run $(x_k,\alpha_k)$ of SPG1 and every accumulation point $\bar x$ of $(x_k)$,

$$\langle g(\bar x),x-\bar x\rangle\ge0\qquad\text{for all }x\in\Omega.$$

The statement fixes no parameter values, and it assumes neither convexity of $f$ nor a bounded level set.

Milestones

• Lemma 2.1 (ii). For $\bar x\in\Omega$ and $t\in(0,\alpha_{\max}]$, $g_t(\bar x)=0$ if and only if $\bar x$ is a constrained stationary point.
• Lemma 2.1 (i). For $x\in\Omega$ and $t\in(0,\alpha_{\max}]$,

$$\langle g(x),g_t(x)\rangle\le-\tfrac1t\|g_t(x)\|_2^2\le-\tfrac1{\alpha_{\max}}\|g_t(x)\|_2^2.$$

• Lemma 2.2 (i). For $x\in\Omega$ and $z\in\mathbb R^n$, the map $s\mapsto\|P(x+sz)-x\|/s$ is nonincreasing on $s>0$.
• Lemma 2.2 (ii). For every $x\in\Omega$ there is $s_x>0$ such that $f(P(x-tg(x)))-f(x)\le\gamma\langle g(x),g_t(x)\rangle$ for all $t\in[0,s_x]$.
• Theorem 2.2, first clause (SPG1 is well defined). At a point where Step 1 does not stop, every admissible backtracking sequence starting at $\alpha\in[\alpha_{\min},\alpha_{\max}]$ reaches a trial point satisfying (1). The statement is for an arbitrary reference value $R\ge f(x)$, which covers the maximum in (1).

Significance

Theorem 2.2 is the global convergence guarantee for SPG1. It holds without monotone decrease of $f$ and with no restriction on the spectral step beyond the safeguards. Lemma 2.2 carries Bertsekas's curvilinear Armijo analysis, stated for monotone gradient projection, over to the nonmonotone spectral setting. The projection-arc search is the natural one when $\Omega$ is a box or a polyhedron: there the arc is piecewise linear and each trial point is feasible by construction.

Status: the theorem is proved in the literature. This paper's proof reads "Use Lemma 2.2 with the proof technique of [7]", and Lemma 2.2 is quoted from Bertsekas's Nonlinear Programming (Lemma 2.3.1 and Theorem 2.3.3 (a)). No Lean formalization of this theorem, of the Armijo analysis along the projection arc, or of the monotonicity of $\|P(x+sz)-x\|/s$ is known. The mission produces a formal proof and a reusable Lean interface for projection-based first-order methods on convex sets.

Difficulty

For monotone descent methods, the usual argument shows that $f(x_k)$ decreases, so the total decrease is finite and the per-iteration decrease tends to zero. That argument fails here, because $f(x_k)$ need not decrease. Only the window maximum $\max_{0\le j\le\min\{k,M-1\}}f(x_{k-j})$ is nonincreasing, and a small decrease of this maximum does not by itself give a small decrease at the iterates that approach a given accumulation point $\bar x$.

Along the projection arc there is a second obstacle. The decrease predicted by (1) is $\gamma\langle g(x_k),g_{\lambda_k}(x_k)\rangle$, and $g_\lambda(x_k)$ depends nonlinearly on $\lambda$: for $\lambda<\alpha_k$ the trial point is not a rescaling of the first one. So small accepted steps do not translate into small multiples of a fixed direction, as they do for SPG2. The step lengths $\lambda_k$ may also tend to zero, $f$ is $C^1$ only on a neighbourhood of $\Omega$, and no Lipschitz constant for $g$ is available.

Formalization scope

• Space and data. The space is EuclideanSpace ℝ (Fin n) with inner ℝ and the 2-norm. $f$ is a total function EuclideanSpace ℝ (Fin n) → ℝ with ContDiffOn ℝ 1 f U on an open U ⊇ Ω, and $g$ is Mathlib's gradient f. Every trial point is a projection, so the algorithm evaluates $f$ and $g$ only at points of $\Omega$.

• Iteration and trials. Iterations are indexed from $0$. The backtracking choice (2) is universally quantified. At each iteration, a run carries a finite trial list with $\lambda^{(0)}=\alpha_k$ and $\lambda^{(i+1)}\in[\sigma_1\lambda^{(i)},\sigma_2\lambda^{(i)}]$; test (1) fails at every trial but the last and holds at the last.

• Step size. $\alpha_{k+1}$ is given by Step 3 exactly.

• Accumulation point. An accumulation point is MapClusterPt x̄ atTop x.

• Lemma 2.2 (i). The paper names the domain $[0,\infty)$ but defines $h$ only for $s>0$, so the milestone is stated on $(0,\infty)$.

• Excluded simplifications. None of the following is SPG1:

  • a run predicate that accepts any positive step;
  • a run predicate that starts backtracking at $1$;
  • a run predicate that uses SPG2's test $\gamma\lambda\langle d_k,g(x_k)\rangle$;
  • a run predicate that lets $\alpha_{k+1}$ range freely over $[\alpha_{\min},\alpha_{\max}]$.

  Nor is a goal that states $g_t(\bar x)=0$ instead of the variational inequality, or one that adds convexity of $f$, a Lipschitz gradient or a bounded level set.

• Non-vacuity. The hypotheses of the goal are satisfiable. Take $f(x)=\|x\|^2$, $\Omega=\mathbb R^n$, $M=1$, $\alpha_{\min}=1/8$, $\alpha_{\max}=1/4$, $\gamma=1/2$, $\sigma_1=1/10$, $\sigma_2=9/10$ and $v\ne0$. Then the iterates $x_k=2^{-k}v$ with $\alpha_k=1/4$ form an infinite run with accumulation point $0$.

• Infrastructure. A complete development needs:

  • the variational characterization of the projection (Mathlib has it in the iInf form, norm_eq_iInf_iff_real_inner_le_zero) and the nonexpansiveness of the projection;
  • a first-order expansion of a $C^1$ function along curves in $\Omega$;
  • the bookkeeping of the nonmonotone reference value.

  The projection lemmas, including Lemma 2.2 (i), are reusable for any gradient projection method and are welcome as separate contributions.

Selected references

• E. G. Birgin, J. M. Martínez, M. Raydan, Nonmonotone spectral projected gradient methods on convex sets, SIAM J. Optim. 10(4) (2000) 1196–1211; authors' updated version, July 2004. https://doi.org/10.1137/S1052623497330963, https://www.ime.unicamp.br/~martinez/bmr.pdf
• E. G. Birgin, J. M. Martínez, M. Raydan, Inexact spectral projected gradient methods on convex sets, IMA J. Numer. Anal. 23 (2003) 539–559. https://doi.org/10.1093/imanum/23.4.539
• D. P. Bertsekas, Nonlinear Programming, Athena Scientific, 1995, Section 2.3.
• D. P. Bertsekas, On the Goldstein–Levitin–Polyak gradient projection method, IEEE Trans. Automat. Control 21 (1976) 174–184. https://doi.org/10.1109/TAC.1976.1101194
• J. Barzilai, J. M. Borwein, Two-point step size gradient methods, IMA J. Numer. Anal. 8 (1988) 141–148. https://doi.org/10.1093/imanum/8.1.141
• L. Grippo, F. Lampariello, S. Lucidi, A nonmonotone line search technique for Newton's method, SIAM J. Numer. Anal. 23 (1986) 707–716. https://doi.org/10.1137/0723046
• M. Raydan, The Barzilai and Borwein gradient method for the large scale unconstrained minimization problem, SIAM J. Optim. 7 (1997) 26–33. https://doi.org/10.1137/S1052623494266365

Motivation

Many decision problems in operations research are solved in two stages: a model predicts the unknown cost vector of a linear optimization problem from features, and the predicted costs are then passed to a solver. The smart predict-then-optimize (SPO) loss of Elmachtoub and Grigas measures the quality of a prediction by the excess true cost of the decision it induces, rather than by the prediction error itself. El Balghiti, Elmachtoub, Grigas and Tewari study how well the empirical SPO loss generalizes. Their margin-based bounds (Theorems 4 and 5 of the paper) require a geometric condition on the feasible region, the strength property, and a way to compute the distance to degeneracy that enters the margin loss.

Section 5 of the paper verifies this condition in the two cases that matter in practice. For strongly convex regions it is Theorem 7 (mission III of this series). This mission covers the other case, §5.2: feasible regions that are polytopes given by a list of points, which includes the unit simplex of multiclass classification and the feasible regions of shortest-path, assignment and other combinatorial problems written as convex hulls.

Setting

Let $E$ be a finite-dimensional real vector space (the paper's $\mathbb R^d$) with a norm $\|\cdot\|$. A cost vector $\hat c$ is a linear functional on $E$; its value at $w$ is written $\hat c^\top w$, and its dual norm is $\|\hat c\|_*=\max_{\|w\|\le1}\hat c^\top w$.

The feasible region is a polytope with a known convex hull representation: pairwise distinct points $v_1,\dots,v_K\in E$ and

$$S=\mathrm{conv}\{v_1,\dots,v_K\}.$$

Redundant points (points that are convex combinations of the others) are allowed. For a cost vector $\hat c$, $P(\hat c)$ is the problem $\min_{w\in S}\hat c^\top w$, and an optimization oracle $w^*$ is any map with $w^*(\hat c)\in\arg\min_{w\in S}\hat c^\top w$ for every $\hat c$.

• The degenerate set $\mathcal C^\circ$ is the set of cost vectors $\hat c$ for which $P(\hat c)$ has more than one optimal solution.
• The distance to degeneracy is $\nu_S(\hat c)=\inf_{c\in\mathcal C^\circ}\|c-\hat c\|_*$.
• $S$ has the strength property with parameter $\mu>0$ if

$$\hat c^\top\big(w-w^*(\hat c)\big)\ \ge\ \frac{\mu\,\nu_S(\hat c)}{2}\,\|w-w^*(\hat c)\|^2\qquad\text{for all } w\in S\text{ and all }\hat c.$$

• The negative normal cone at $v_j$ is $\mathcal K_j=-N_S(v_j)=\{\hat c:\hat c^\top(w-v_j)\ge0\ \text{for all } w\in S\}$, the cost vectors for which $v_j$ is optimal.
• The diameter is $\Delta(S)=\sup_{w_1,w_2\in S}\|w_1-w_2\|$.

Formalization targets

Goal: Theorem 8, strength claim (p. 25)

If $S=\mathrm{conv}\{v_1,\dots,v_K\}$ is not a singleton, then for every oracle $w^*$, $S$ has the strength property with parameter

$$\mu=\frac{2}{\Delta(S)}>0 .$$

Milestones, in attack order

1. Eq. (9) (p. 24): each cone is described by finitely many inequalities,

$$\mathcal K_j=\{\hat c:\hat c^\top(v_i-v_j)\ge0\ \text{for all } i=1,\dots,K\}.$$

2. Proposition 2 (p. 25): $P(\hat c)$ has a unique optimal solution if and only if $\hat c\in\mathrm{int}(\mathcal K_j)$ for some $j$; hence

$$\mathcal C^\circ=\mathbb R^d\setminus\bigcup_{j=1}^K\mathrm{int}(\mathcal K_j).$$

3. Diameter (p. 25, the sentence before Theorem 8): $\Delta(S)=\max_{i,j}\|v_i-v_j\|$.
4. Theorem 8, eq. (10) (p. 25): for every oracle and every $\hat c$,

$$\nu_S(\hat c)=\min_{j:\,v_j\ne w^*(\hat c)}\frac{\hat c^\top(v_j-w^*(\hat c))}{\|v_j-w^*(\hat c)\|}.$$

Significance

The result. Formula (10) turns the distance to degeneracy, defined as an infimum over an infinite non-convex set, into a minimum of $K$ explicit ratios that needs one oracle call. This makes the margin SPO loss of the paper computable for polytopes. The strength claim, combined with the paper's Theorems 4 and 5, yields margin-based generalization bounds for the SPO loss over any polytope with a known vertex list, with a dependence on the hypothesis class through its multivariate Rademacher complexity rather than through a Natarajan dimension. For the unit simplex it recovers known margin bounds for multiclass classification (Example 8).

Formalizing it. The results are proved in the paper; to our knowledge none of them is machine-checked. A formalization produces, beyond the four statements, a Lean account of the normal fan of a polytope presented by a point list, its interplay with uniqueness of linear-optimization solutions, and distances to its boundary measured in a dual norm. These are standard facts of polyhedral theory that Mathlib does not yet state in this form.

Difficulty

The obstacle is that $\nu_S$ is a distance to the degenerate set, and that set is neither convex nor given by inequalities: it is a union of lower-dimensional pieces of the normal fan, so no projection formula applies, and its description depends on which points of the representation are redundant. Relating a dual-norm ball around $\hat c$ to the finitely many inequalities of eq. (9) is where the argument needs care. A Euclidean shortcut is not available: the norm is arbitrary, and the numerator of (10) and the distance $\nu_S$ are measured in different norms. A second trap is the oracle: at a degenerate $\hat c$ it may return a point that is not among the $v_j$, and (10) must still hold.

Formalization scope

• $E$ is a finite-dimensional real normed space; cost vectors are elements of StrongDual ℝ E, whose operator norm is the dual norm. Interiors and distances in the cost space use that norm.
• The polytope is v : Fin K → E, injective, with $S$ = convexHull ℝ (Set.range v). Nonemptiness, compactness and convexity of $S$ (the paper's §2 standing assumptions) follow from this representation; Proposition 2 and the diameter identity add $K\ge1$, which is that nonemptiness.
• "Not a singleton" is S.Nontrivial. Without it $\mathcal C^\circ=\emptyset$, $\nu_S\equiv0$ and the strength property holds for free; with it, $0\in\mathcal C^\circ$ and $\nu_S$ is a genuine distance. The goal's parameter $2/\Delta(S)$ is stated to be positive, so the Lean conventions $\mathrm{diam}=0$ on unbounded or one-point sets and $2/0=0$ cannot trivialize it.
• The oracle is arbitrary: every theorem quantifies over all maps $w$ with $w(\hat c)\in\arg\min_S\hat c$, never a fixed selection.
• $\nu_S$ is Metric.infDist to $\mathcal C^\circ$; $\Delta(S)$ is Metric.diam, correct here because $S$ is bounded. Minima and maxima over finite index sets are stated with IsLeast/IsGreatest, so no junk value of min' or sInf enters.
• Reusable infrastructure: the negative normal cones and normal fan of a point-list polytope, the characterization of unique optima of linear optimization over a polytope, and the dual-norm distance to the boundary of a polyhedral cone. Contributions of any of these as standalone lemmas are welcome.

Selected references

• O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, arXiv:1905.11488v3, 2022 (Mathematics of Operations Research, 2023). https://arxiv.org/abs/1905.11488
• A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 2022. https://doi.org/10.1287/mnsc.2020.3922
• G. M. Ziegler, Lectures on Polytopes, Graduate Texts in Mathematics 152, Springer, 1995. https://doi.org/10.1007/978-1-4613-8431-1
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 2009. https://doi.org/10.1007/978-3-642-02431-3

Motivation

The k-median problem asks to open $k$ facilities among a set of candidate sites so that the total distance from clients to their nearest open facility is as small as possible. It is a basic model of facility location and of clustering, and it is NP-hard, so the question studied in approximation algorithms is how close a polynomial-time method can get to the optimum.

Local search is the method most used in practice: start from any $k$ facilities and repeatedly replace a few of them by others whenever this lowers the cost. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave the first analysis of a local search for k-median with a bounded performance guarantee using only $k$ medians. For single swaps they proved a locality gap of $5$ (Theorem 3.2, the subject of the first mission of this series); allowing up to $p$ facilities to be exchanged at once improves the gap to $3 + 2/p$, which the paper notes improves on the $4$-approximation of Charikar and Guha. That $p$-swap bound is the result this mission formalizes.

Timeline (as recounted in §1 of the paper):

• Shmoys, Tardos and Aardal, and Charikar, Guha, Tardos and Shmoys: LP rounding gives a $6\tfrac23$-approximation for k-median.
• Jain and Vazirani: primal–dual schema and Lagrangian relaxation give a $6$-approximation; Charikar and Guha improve it to $4$.
• Korupolu, Plaxton and Rajaraman: local search with add, delete and swap moves gives a solution with $k(1+\epsilon)$ facilities and service cost at most $3 + 5/\epsilon$ times the optimum.
• Arya et al.: locality gap $5$ for single swaps and $3 + 2/p$ for $p$-swaps with exactly $k$ facilities, with a tight example.
• Later work (Li and Svensson, 2013/2016) goes below $3$ with methods other than local search.

Setting

A metric instance consists of a finite set $C$ of clients, a finite set $F$ of facilities and a distance $d$ on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality; $c_{ji} = d(j,i)$ is the cost of serving client $j$ by facility $i$.

For a nonempty set $S \subseteq F$ of open facilities, each client is served by its nearest open facility, and

$$\mathrm{cost}(S) = \sum_{j \in C} \min_{i \in S} c_{ji}.$$

Fix an integer $p \ge 1$. A $p$-swap $\langle A, B\rangle$ deletes a set $A \subseteq S$ of at most $p$ facilities and adds a set $B \subseteq F$ of the same size. The $p$-swap neighbourhood of $S$ is

$$\mathcal B(S) = \{(S \setminus A) \cup B \mid A \subseteq S,\ B \subseteq F,\ |A| = |B| \le p\},$$

and $S$ is locally optimum when $\mathrm{cost}(S) \le \mathrm{cost}(S')$ for every $S' \in \mathcal B(S)$. The locality gap is the supremum, over instances, of the ratio between the cost of a locally optimum solution and the cost of a global optimum.

In Lean the instance is MetricInstance Cl Fa with the distance on Cl ⊕ Fa, the cost is kmCost I S hS (defined only for nonempty S), and local optimality is IsPSwapLocalOpt I p S hS, all in the namespace LocalSearchFL.MultiSwap.

Formalization targets

Goal: locality gap at most $3 + 2/p$

For every metric instance, every integer $p \ge 1$, every $k \ge 1$, every locally optimum $S$ with $|S| = k$, and every nonempty $O \subseteq F$ with $|O| \le k$,

$$\mathrm{cost}(S) \le \left(3 + \frac{2}{p}\right)\mathrm{cost}(O).$$

This is the bound concluded at the end of §3.4 (p. 553, announced p. 551). The comparison solution $O$ is arbitrary, not only an optimum, which is the strongest form printed.

Milestones

1. §3.4, p. 551: for sets $X, Y \subseteq S$, disjoint sets have disjoint captures, and $X \subseteq Y$ implies $\mathrm{capture}(X) \subseteq \mathrm{capture}(Y)$, where $\mathrm{capture}(A) = \{o \in O \mid |N_S(A) \cap N_O(o)| > |N_O(o)|/2\}$.
2. Claim 3.1, p. 552: when $|S| = |O|$, there are partitions $A_1,\dots,A_r$ of $S$ and $B_1,\dots,B_r$ of $O$ with $|A_i| = |B_i|$, $B_i = \mathrm{capture}(A_i)$ and exactly one bad facility in $A_i$ for $i < r$, and only good facilities in $A_r$.
3. §3.4, pp. 552–553: a family of swaps of size at most $p$ with positive weights, such that each $o \in O$ is swapped in with total weight exactly $1$, each $s \in S$ is swapped out with total weight at most $(p+1)/p$, and $\mathrm{capture}(A) \subseteq B$ for every swap $\langle A, B\rangle$.
4. Property 3.2, p. 553: a bijection $\pi$ of $N_O(o)$ with $\pi(P) \cap P = \emptyset$ for every class $P$ of a partition of $N_O(o)$ with $|P| \le \tfrac12|N_O(o)|$.

Significance

The bound shows that the simplest optimization heuristic, stopped at any local optimum, is within a constant factor of optimal for metric k-median, and that the factor tends to $3$ as the neighbourhood grows; the paper's tight example (§3.5, given for $p = 2$ and stated to generalize to every $p$) shows that the analysis cannot be improved for this neighbourhood. Combined with the standard $\varepsilon$-improvement rule (p. 548), it yields a polynomial-time $(3 + 2/p + \varepsilon)$-approximation. The analysis template (charging each client's reassignment through a bijection of $N_O(o)$, and averaging the local-optimality inequalities of carefully chosen swaps) was reused for facility location, capacitated variants and k-means.

The result has been proved since 2001. What this mission adds is a machine-checked proof: no formalization of the k-median problem or of any locality-gap bound is known to exist in Mathlib or on this platform. The combinatorial milestones (capture, the partition of Claim 3.1, the weighted swaps, the bijection of Property 3.2) are independent of the metric and are reusable in any local-search analysis of clustering objectives.

Difficulty

For single swaps each facility of $O$ is paired with one facility of $S$ and a direct counting argument suffices. With $p$-swaps, a facility of $S$ may capture several facilities of $O$ at once, and a group of facilities of $S$ may jointly capture a facility of $O$ that none of them captures alone. Pairing facilities one by one then fails: the clients of a captured facility cannot be reassigned cheaply unless the capturing set is swapped out together with everything it captures. Swapping whole groups is only allowed when a group has at most $p$ members; larger groups must be split into single swaps, and the weights must be chosen so that every facility of $O$ is counted exactly once while no facility of $S$ is counted more than $(p+1)/p$ times. Getting the constant $3 + 2/p$ (rather than a weaker one) depends on this exact accounting.

Formalization scope

• Clients and facilities are types Cl, Fa with Fintype and DecidableEq; solutions are Finset Fa. The distance is real-valued on Cl ⊕ Fa; d x x = 0 is not assumed (the paper neither states nor uses it).
• The cost is the nearest-facility cost of a nonempty set; the empty set has no cost, so no junk value enters. The bound is stated multiplied out, kmCost I S hS ≤ (3 + 2 / (p : ℝ)) * kmCost I O hO, with the constant computed in $\mathbb R$.
• $|S| = k$ is required; $O$ ranges over all nonempty sets with $|O| \le k$. §3.3 introduces multiswaps with $p > 1$; the statement takes $p \ge 1$, where $p = 1$ is Theorem 3.2 (bound $5$).
• Local optimality is over the whole neighbourhood (3), including sets $B$ that meet $S$, not only over the swaps used in the analysis. Restricting it to those swaps would state a theorem with a stronger hypothesis.
• The milestones state Claim 3.1, the swap construction and Property 3.2 in existence form; the procedure of Figure 8 is not formalized. Capture, good and bad are computed against the original $S$ and $O$. The client assignments in the milestones are arbitrary functions; nearest-facility assignments are a special case. Milestone 3 also records that the deleted sets of two swaps are equal or disjoint, which is immediate from the construction and is what makes Property 3.2 applicable.
• The per-swap reassignment inequality is not a milestone: the paper describes it only as "similar to the one presented for the single-swap heuristic" and prints no inequality.
• Out of scope: the tight example (§3.5), the polynomial-time wrapper, and arbitrary client demands.

Needed infrastructure: finite sums over clients, Finset.inf', permutations (Equiv.Perm), and a weighted double-counting argument over the swaps. Proofs of the combinatorial milestones and alternative routes to the goal are welcome.

Selected references

• V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3):544–562, 2004. https://doi.org/10.1137/S0097539702416402
• M. Charikar, S. Guha, É. Tardos, D. Shmoys, A Constant-Factor Approximation Algorithm for the k-Median Problem, J. Comput. System Sci. 65(1):129–149, 2002. https://doi.org/10.1006/jcss.2002.1882
• K. Jain, V. Vazirani, Approximation Algorithms for Metric Facility Location and k-Median Problems Using the Primal-Dual Schema and Lagrangian Relaxation, J. ACM 48(2):274–296, 2001. https://doi.org/10.1145/375827.375845
• M. Korupolu, C. Plaxton, R. Rajaraman, Analysis of a Local Search Heuristic for Facility Location Problems, J. Algorithms 37(1):146–188, 2000. https://doi.org/10.1006/jagm.2000.1100
• S. Li, O. Svensson, Approximating k-Median via Pseudo-Approximation, SIAM J. Comput. 45(2):530–547, 2016. https://doi.org/10.1137/130938645

Motivation

Line searches are the step-size rules inside most methods for smooth unconstrained minimization $\min_{x \in \mathbb{R}^n} f(x)$: steepest descent, conjugate gradient, quasi-Newton and limited-memory methods all choose a direction $d_k$ and then a step $\alpha_k$ along it. Classical Armijo and Wolfe rules are monotone: they require $f(x_{k+1}) < f(x_k)$. Grippo, Lampariello and Lucidi (SIAM J. Numer. Anal., 1986) observed that insisting on monotone decrease can slow a method down, and proposed comparing $f(x_{k+1})$ with the maximum of the last $M$ function values instead. That max-based rule discards good function values and depends strongly on $M$, and Dai showed that R-linearly convergent iterates can violate it for every fixed memory $M$.

Zhang and Hager (SIAM J. Optim., 2004) replaced the maximum by a weighted average of all previous function values. Their averaged nonmonotone line search is used in practical codes, for example with L-BFGS and in later nonmonotone spectral and conjugate-gradient methods. This mission formalizes the paper's first main result: global convergence to stationary points for nonconvex $f$.

Setting

Let $f : \mathbb{R}^n \to \mathbb{R}$ be continuously differentiable, with gradient $g_k = \nabla f(x_k)$ at the $k$-th iterate. The Nonmonotone Line Search Algorithm (NLSA) has parameters

$$0 \le \eta_{\min} \le \eta_{\max} \le 1, \qquad 0 < \delta < \sigma < 1 < \rho, \qquad \mu > 0.$$

It maintains weights $Q_k$ and reference values $C_k$:

$$Q_0 = 1,\ C_0 = f(x_0), \qquad Q_{k+1} = \eta_k Q_k + 1, \qquad C_{k+1} = \frac{\eta_k Q_k C_k + f(x_{k+1})}{Q_{k+1}}, \qquad (1.6)$$

with $\eta_k \in [\eta_{\min}, \eta_{\max}]$ chosen at each step. The iterates are $x_{k+1} = x_k + \alpha_k d_k$, where the step $\alpha_k > 0$ satisfies one of two rules, fixed for the whole run:

• the nonmonotone Wolfe conditions

$$f(x_k + \alpha_k d_k) \le C_k + \delta \alpha_k g_k^{\mathsf T} d_k \quad (1.4), \qquad \nabla f(x_k + \alpha_k d_k) d_k \ge \sigma g_k^{\mathsf T} d_k \quad (1.5);$$

• the nonmonotone Armijo conditions: $\alpha_k = \bar\alpha_k \rho^{h_k}$, where $\bar\alpha_k > 0$ is a trial step and $h_k$ is the largest integer such that (1.4) holds and $\alpha_k \le \mu$.

The choice $\eta_k = 0$ gives $C_k = f(x_k)$, the monotone line search; $\eta_k = 1$ gives $C_k = A_k = \frac{1}{k+1}\sum_{i \le k} f(x_i)$.

The direction assumption asks for constants $c_1, c_2 > 0$ with $g_k^{\mathsf T} d_k \le -c_1\|g_k\|^2$ (2.4) and $\|d_k\| \le c_2\|g_k\|$ (2.5) for all sufficiently large $k$. The level set is $\mathcal L = \{x : f(x) \le f(x_0)\}$, and $\bar{\mathcal L}$ is the set of points whose distance to $\mathcal L$ is at most $\mu d_{\max}$, where $d_{\max} = \sup_k \|d_k\|$.

Formalization targets

Goal: Theorem 2.2

Suppose $f$ is bounded from below, $g_k^{\mathsf T} d_k \le 0$ for every $k$, the direction assumption holds, and $\nabla f$ is Lipschitz continuous on $\mathcal L$ (Wolfe rule) or on $\bar{\mathcal L}$ (Armijo rule). Then

$$\liminf_{k \to \infty} \|\nabla f(x_k)\| = 0, \qquad (2.6)$$

and if $\eta_{\max} < 1$,

$$\lim_{k \to \infty} \nabla f(x_k) = 0, \qquad (2.7)$$

so every limit of a convergent subsequence of iterates is a stationary point. No convexity is assumed.

Milestones

• Lemma 1.1: $f_k \le C_k \le A_k$ along the run, and a Wolfe step and a largest Armijo exponent exist whenever $g_k^{\mathsf T} d_k < 0$ and $f$ is bounded below.
• Eq. (1.8): $Q_{j+1} = 1 + \sum_{i=0}^{j} \prod_{m=0}^{i} \eta_{j-m} \le j+2$.
• Lemma 2.1: the lower bounds (2.1) and (2.2) on accepted Wolfe and Armijo steps.
• Eqs. (2.8)–(2.9): $f_{k+1} \le C_k - \beta\|g_k\|^2$ with the explicit constant

$$\beta = \min\left\{\frac{\delta\mu c_1}{\rho}, \frac{2\delta(1-\delta)c_1^2}{L\rho c_2^2}, \frac{\delta(1-\sigma)c_1^2}{Lc_2^2}\right\}.$$

• Eq. (2.14): $\sum_k \|g_k\|^2 / Q_{k+1} < \infty$.
• Eq. (2.15): $Q_{k+1} \le 1/(1-\eta_{\max})$ when $\eta_{\max} < 1$.
• Corollary 2.3: the analogue of Theorem 2.2 when (2.5) is replaced by the growth condition $\|d_k\|^2 \le \tau_1 + \tau_2 k$ (2.16).

Significance

Theorem 2.2 is the convergence guarantee that makes the averaged reference value $C_k$ usable in practice: any direction method whose directions are uniformly gradient-related (for example L-BFGS with bounded Hessian approximations) inherits stationarity of its limit points when combined with this line search, for every choice of the weights $\eta_k$. The monotone Wolfe and Armijo results are the special case $\eta_k \equiv 0$. The same estimates, (2.8) and (2.15), are the input to the paper's second main result, R-linear convergence for strongly convex $f$ (Theorem 3.1, a separate mission in this series).

The result is proved in the paper. It has no machine-checked proof that this mission is aware of: the platform has monotone backtracking statements for convex problems, but no nonmonotone line search, no Wolfe conditions and no Zoutendijk-type global convergence theorem for nonconvex $f$. A complete development also provides reusable Lean statements of the Wolfe and Armijo conditions and of step-size lower bounds under local Lipschitz continuity of the gradient.

Difficulty

Each step is elementary, but the argument has several places where a naive formalization fails. The Lipschitz hypothesis is only local: on $\mathcal L$ for the Wolfe rule, on the $\mu d_{\max}$-neighbourhood $\bar{\mathcal L}$ for the Armijo rule. So the proof must first show that every iterate stays in $\mathcal L$ even though $f(x_k)$ is not monotone. This needs $f_k \le C_k$ and the monotonicity of $C_k$, and then that the Armijo rule's rejected trial point $x_k + \rho\alpha_k d_k$ lies in $\bar{\mathcal L}$. The Armijo lower bound uses the maximality of the integer exponent $h_k$ and a first-order Taylor bound along a segment. The passage from (2.14) to (2.6) and (2.7) uses the two growth bounds on $Q_{k+1}$. The first gives only $\liminf$, since $\sum \|g_k\|^2/(k+2) < \infty$ does not force $g_k \to 0$.

Formalization scope

The space is EuclideanSpace ℝ (Fin n) with the Euclidean norm, $f$ is ContDiff ℝ 1, and the paper's row vector $\nabla f(x)$ acting on $d$ is the inner product of Mathlib's gradient f x with $d$. $Q_k$, $C_k$ and $A_k$ are defined by recursion from the run. A run is an infinite sequence $(x_k, d_k, \alpha_k, \eta_k)$ satisfying the update, $\eta_k \in [\eta_{\min}, \eta_{\max}]$, and the chosen rule at every $k$. The stopping test is not modelled. The Armijo exponent ranges over $\mathbb{Z}$ (it may be negative since $\rho > 1$), and "largest" is IsGreatest. $d_{\max}$ and the distance to $\mathcal L$ are computed in $[0, \infty]$, so unbounded directions give $\bar{\mathcal L} = \mathbb{R}^n$.

The following repairs and readings of the printed statements are made:

1. Theorem 2.2 and Corollary 2.3 assume $\nabla f(x_k) d_k \le 0$ for every $k$. The printed theorem constrains $d_k$ only for large $k$, but its proof needs $f(x_{k+1}) \le C_k$ at every step, which is the hypothesis of Lemma 1.1. Without it an early ascent step could leave $\mathcal L$, where nothing is assumed. The direction assumption itself stays "for all sufficiently large $k$".
2. $\liminf_k \|\nabla f(x_k)\| = 0$ is stated as "for every $\varepsilon > 0$, $\|\nabla f(x_k)\| < \varepsilon$ for infinitely many $k$".
3. The final "Hence" sentence of Theorem 2.2 is stated under $\eta_{\max} < 1$, from which it is derived.
4. In Corollary 2.3, "positive constants $\tau_1, \tau_2$" is read as $\tau_1 > 0$, $\tau_2 \ge 0$, since the corollary itself treats $\tau_2 = 0$.
5. Lemma 2.1 is stated pointwise for one iteration. Its Armijo case makes explicit the fact $f(x_k) \le C_k$ that the paper's proof invokes.

The following formalizations would make the goal trivial or empty and are ruled out:

• a (2.6) written with Lean's real liminf, which is $0$ for a divergent sequence;
• a run class in which the step rule does not constrain $\alpha_k$ (Wolfe without (1.4), Armijo without maximality of $h_k$), or which no sequence satisfies. The constant run $f \equiv 0$, $d_k = 0$ satisfies both rules, so the class is nonempty;
• assuming $\nabla f$ globally Lipschitz or the directions bounded.

Welcome contributions: proofs of the milestones in the listed order, and general lemmas on Wolfe and Armijo steps under local gradient Lipschitz continuity, which are reusable for other line-search methods.

Selected references

• H. Zhang, W. W. Hager, A Nonmonotone Line Search Technique and Its Application to Unconstrained Optimization, SIAM J. Optim. 14(4):1043–1056, 2004. https://doi.org/10.1137/S1052623403428208
• L. Grippo, F. Lampariello, S. Lucidi, A Nonmonotone Line Search Technique for Newton's Method, SIAM J. Numer. Anal. 23(4):707–716, 1986. https://doi.org/10.1137/0723046
• Y.-H. Dai, On the Nonmonotone Line Search, J. Optim. Theory Appl. 112(2):315–330, 2002. https://doi.org/10.1023/A:1013653923062

Motivation

Retailers of fashion and seasonal goods sell a fixed stock over a short season and routinely cut the price part-way through it. The markdown trades off two effects: a late discount keeps early, high-valuation customers paying the full price, while an early discount reaches customers whose interest in the product fades as the season goes on. Aviv and Pazgal (MSOM 2008) build a two-price model of this trade-off with Poisson arrivals and valuations that decline exponentially over the season, and compare sellers facing myopic customers, who buy as soon as the current price is acceptable, with sellers facing strategic customers, who may wait for the discount.

This mission formalizes the benchmark of that comparison in which the problem can be solved in closed form: myopic customers who all share the same base valuation, so that the only source of price discrimination is the decline of valuations over time. Proposition 4 of the paper identifies the optimal premium price, discount price and discount time, and the paper's Proposition 5 and Example 1 then measure how much strategic behaviour costs the seller against it.

Setting

The season is $[0, 1]$. Customers arrive as a Poisson process with rate $\lambda > 0$, so $\lambda$ is the expected number of arrivals in the season. Every customer has base valuation $1$, and a customer's valuation at time $t$ is $\rho^t$ for a fixed decline parameter $0 < \rho < 1$ (equivalently $e^{-\alpha t}$ with $\alpha = -\ln\rho$; $\rho$ is the fraction of the valuation left at the end of the season). In the paper's notation this is the case $c = 0$, $\mu = 1$, $H = 1$ of a family of Gamma-distributed base valuations with mean $\mu$ and coefficient of variation $c$; the tail of the base valuation is $\bar F(x) = 1$ for $x \le 1$ and $0$ otherwise.

The seller posts a premium price $p_1$ on $[0, T)$ and a discount price $p_2 \le p_1$ from the discount time $T \in [0, 1]$ on, and has unlimited inventory. A myopic customer arriving at $t < T$ buys at once iff $\rho^t \ge p_1$; otherwise the customer waits and buys at $T$ iff $\rho^T \ge p_2$. A customer arriving after $T$ buys iff the current valuation is at least $p_2$. The expected numbers of buyers in the three groups are the segment rates $\Lambda_I(p_1) = \lambda\int_0^T \bar F(p_1e^{\alpha t})\,dt$, $\Lambda_W(p_1, p_2) = \lambda\int_0^T[\bar F(\min\{p_1e^{\alpha t}, p_2e^{\alpha T}\}) - \bar F(p_1 e^{\alpha t})]\,dt$ and $\Lambda_L(p_2) = \lambda\int_T^1 \bar F(p_2 e^{\alpha t})\,dt$, and the expected revenue is

$$R_\rho(p_1, p_2; T) = p_1\,\Lambda_I(p_1) + p_2\,\big(\Lambda_W(p_1, p_2) + \Lambda_L(p_2)\big).$$

For a price $p \in [\rho, 1]$ let $\tau(p) = \ln p/\ln\rho$, the time at which the valuation has fallen to $p$, and write $\tau_1 = \tau(p_1)$, $\tau_2 = \tau(p_2)$. The reduced objective is

$$G(p_1, p_2) = (p_1 - p_2)\,\frac{\ln p_1}{\ln\rho} + p_2\,\frac{\ln p_2}{\ln\rho}, \qquad \rho \le p_2 \le p_1 \le 1 .$$

Formalization targets

Goal: Proposition 4 (p. 351)

$$\pi^*_{C/N} = \lambda\cdot\max_{\rho \le p_2 \le p_1 \le 1} G(p_1, p_2) = \max_{0 < p_2 \le p_1,\ 0 \le T \le 1} R_\rho(p_1, p_2; T),$$

every maximizer $(p_1^*, p_2^*)$ of $G$ together with every $T$ with $p_2^* \le \rho^T \le p_1^*$ attains $\pi^*_{C/N}$, and, if $\rho \le e^{-2+e^{-1}}$, the maximizer is unique,

$$p_1^* = e^{-1+e^{-1}}, \qquad p_2^* = p_1^*/e, \qquad \pi^*_{C/N} = -\frac{\lambda\, e^{-1+e^{-1}}}{\ln\rho},$$

and every $T$ with $\rho^T \in [e^{-2+e^{-1}}, e^{-1+e^{-1}}]$ is optimal.

Milestones (Proof of Proposition 4, p. 359)

For $\rho \le p_2 \le p_1 \le 1$:

1. $R_\rho(p_1, p_2; T) \le R_\rho(p_1, p_2; \tau_1)$ for $T \in [0, \tau_1]$;
2. $R_\rho(p_1, p_2; T) \le R_\rho(p_1, p_2; \tau_2)$ for $T \in [\tau_2, 1]$;
3. $R_\rho(p_1, p_2; T) = \lambda\, G(p_1, p_2)$ for $T \in [\tau_1, \tau_2]$;
4. for $\rho \le e^{-2+e^{-1}}$, $\max G = -e^{-1+e^{-1}}/\ln\rho$, attained only at $(e^{-1+e^{-1}}, e^{-2+e^{-1}})$.

Significance

Proposition 4 gives an explicit optimal markdown policy in a model where segmentation happens purely by arrival time: it shows that the discount time is not pinned down but can be placed anywhere in the interval in which the valuation lies between the two prices, and that for strongly declining valuations the optimal prices do not depend on $\rho$ at all. The paper uses it as the benchmark $\pi^*_{C/N}$ against which the strategic-customer equilibrium of Proposition 5 and the losses of Example 1 are measured.

The result is proved in the paper by a short argument; nothing in it has been machine-checked. A formal development makes the three observations of the proof precise (in particular, that prices outside $[\rho, 1]$ are dominated, which the paper leaves implicit) and supplies the omitted calculus for the special case.

Difficulty

The revenue is defined through integrals of a step function of time, and the reduction to $G$ needs these integrals evaluated in every configuration of $p_1$, $p_2$ and $T$, including prices above $1$ (nobody buys) and below $\rho$ (everyone buys, at a needlessly low price). The paper's proof covers only $\rho \le p_2 \le p_1 \le 1$ and asserts the domination of the remaining prices without argument. The special case is a constrained two-variable maximization of a function that is not jointly concave; the unconstrained critical point must be shown to be feasible exactly when $\rho \le e^{-2+e^{-1}}$, and boundary points of the region must be excluded.

Formalization scope

Everything is over $\mathbb R$. Logarithms are Real.log, powers $\rho^T$ are real powers, the segment rates are interval integrals ∫ t in a..b of the tail $\bar F(x) = \mathbf 1\{x \le 1\}$, and $\alpha = -\ln\rho$ with $H = 1$. The model definitions ($\Lambda_I$, $\Lambda_W$, $\Lambda_L$ and the revenue) are stated for a general tail $\bar F$, decline factor, season length and discount time and then specialized.

The following readings of the paper's words are fixed:

• "$c = 0$": every base valuation equals $\mu = 1$ (the degenerate end of the paper's Gamma family, outside §3's "continuous distribution").
• "$Q/\lambda \to \infty$": unlimited inventory; the truncated Poisson mean $N(q, \Lambda)$ is replaced by $\Lambda$. With unlimited inventory, choosing the contingent discount at time $T$ and choosing both prices in advance give the same optimum.
• Myopic waiting customers buy at $T$ iff their valuation at $T$ is at least $p_2$, as in $\Lambda_W$.
• "$T$ could be optimally selected": $T \in [0, 1]$ is a decision variable together with the prices, which range over all $0 < p_2 \le p_1$, not only over $[\rho, 1]$.
• "Maximize his expected revenues": IsGreatest of the set of attainable revenues.
• "Setting $T$ to any value within the range $p_2^* \le \rho^T \le p_1^*$", and "it would be optimal to select $T$ so that $\rho^T \in [e^{-2+e^{-1}}, e^{-1+e^{-1}}]$": every such $T$ is optimal; it is not claimed that no other $T$ is.
• "The prices $p_1^*$ and $p_2^*$ that solve the problem" in the special case: the maximizer of $G$ is unique.
• "Never optimal" in the first two observations: a weak inequality between revenues.

The decimals $0.196$ and $0.532$ are not stated. A formalization that restricted prices to $[\rho, 1]$ in the revenue maximization, or that fixed $T$ in advance, would assume half of what the proposition proves and is ruled out. Welcome contributions include general lemmas evaluating interval integrals of indicator functions of intervals, and the domination argument for prices outside $[\rho, 1]$.

Selected references

• Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
• N. Stokey, Intertemporal Price Discrimination, Quarterly Journal of Economics 93(3):355–371, 1979. https://doi.org/10.2307/1883163
• D. Besanko and W. L. Winston, Optimal Price Skimming by a Monopolist Facing Rational Consumers, Management Science 36(5):555–567, 1990. https://doi.org/10.1287/mnsc.36.5.555

Why shrink an uncertainty set

Robust optimization (RO) protects a decision against every parameter value in an uncertainty set. For a decision $v$ and a parameter $x \in \mathbb{R}^m$ with objective $f(v, x)$ to be maximized, the robust problem around a nominal parameter $x_0$ with a deviation set $\Delta$ is

$$\max_{v} \min_{x_\delta \in \Delta} f(v, x_0 + x_\delta).$$

When deviations are not adversarial, this formulation is known to be conservative (Delage and Mannor, 2010; Xu and Mannor, NIPS 2006). A common remedy in practice is uncertainty set shrinkage: fix $\alpha \in (0,1)$ and solve the same problem over the shrunken set $\alpha\Delta = \{\alpha x : x \in \Delta\}$. The heuristic is easy to implement, but the meaning of the set $\alpha\Delta$ is unclear, and it has lacked a justification.

Section 4.2 of Xu, Caramanis and Mannor (2012) supplies one, using the paper's distributional interpretation of RO: the shrunken problem approximately solves a distributionally robust stochastic program (DRSP) with two scenarios. This mission formalizes that result, Theorem 4.1, and its two corollaries.

Setting

Let $\mathbb{R}^m$ carry the Euclidean norm $\|\cdot\|_2$ and its Borel $\sigma$-algebra, and let $\mathcal P$ be the set of Borel probability measures on $\mathbb{R}^m$. Let $V$ be any set of decisions and $f : V \times \mathbb{R}^m \to \mathbb{R}$. Fix $x_0 \in \mathbb{R}^m$, a deviation set $\Delta \subseteq \mathbb{R}^m$, and $\alpha \in (0,1)$. Write $x_0 + \Delta = \{x_0 + x : x \in \Delta\}$.

The two-scenario set is

$$\hat{\mathcal P}' = \{\mu \in \mathcal P \mid \mu(\{x_0\}) \ge 1-\alpha,\ \mu(x_0 + \Delta) = 1\}.$$

A distribution in $\hat{\mathcal P}'$ describes a system that is, with probability at least $1-\alpha$, in a normal state where the parameter equals $x_0$, and otherwise in an abnormal state where the parameter deviates by an element of $\Delta$. The DRSP value of a decision $v$ is $\inf_{\mu \in \hat{\mathcal P}'} \int f(v, x)\, d\mu(x)$.

Two further quantities enter. The radius of the deviation set is $D = \max_{x \in \Delta} \|x\|_2$. The curvature bound is a constant $h \ge 0$ with

$$-hI \preceq H_v(x) \preceq hI \quad \text{for all } v, x,$$

where $H_v(x)$ is the Hessian of $f(v, \cdot)$ at $x$ and $\preceq$ is the positive-semidefinite order. In the Lean development these are scenarioSet x₀ Δ (1 - α), drspValue, devRadius Δ and HasBoundedHessian (f v) h, all in the namespace DistInterpRO.Shrinkage.

Formalization targets

Goal: Theorem 4.1 (p. 104)

If $f(v,\cdot)$ is twice differentiable with $-hI \preceq H_v(x) \preceq hI$ for all $v, x$, then for all $v$

$$\inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x) - \alpha D^2 h \;\le\; \min_{x_\delta \in \alpha\Delta} f(v, x_0 + x_\delta) \;\le\; \inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x) + \alpha D^2 h.$$

Milestones (the displays of the proof on p. 105)

1. The mean-value step $f(v, x_0 + x_1) = f(v, x_0) + g_v(x_0 + \beta x_1)x_1$ for some $\beta \in [0,1]$, where $g_v$ is the gradient of $f(v,\cdot)$.
2. The gradient bound $\|g_v(x_0 + \beta x_1) - g_v(x_0 + \alpha\beta' x_1)\| \le h\|\beta x_1 - \alpha\beta' x_1\| \le h\|x_1\| \le hD$, stated together with the general fact that the Hessian bound makes $g_v$ $h$-Lipschitz.
3. The pointwise sandwich: for $x_1 \in \Delta$, $f(v, x_0 + \alpha x_1)$ lies within $\alpha D^2 h$ of $(1-\alpha) f(v, x_0) + \alpha f(v, x_0 + x_1)$.
4. The min sandwich: $\min_{\alpha\Delta} f(v, x_0 + \cdot)$ lies within $\alpha D^2 h$ of $(1-\alpha) f(v, x_0) + \alpha \min_{\Delta} f(v, x_0 + \cdot)$.
5. The two-scenario value: $(1-\alpha) f(v, x_0) + \alpha \min_{x_\delta\in\Delta} f(v, x_0 + x_\delta) = \inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x)$, which the paper derives from its Corollary 5.2 (p. 107).

Further results

Corollary 4.2 (p. 104): if every $f(v,\cdot)$ is linear, the shrunken value equals the DRSP value exactly. Corollary 4.3 (p. 105): if $\Delta$ is star shaped, every $f(v,\cdot)$ is convex with $f(v, x_0) - \min_{\Delta} f(v, x_0 + \cdot) \ge 1$ and has Hessian bounded by $h$, then the shrunken value lies between the DRSP values over $\hat{\mathcal P}''$ and $\hat{\mathcal P}'$, where $\hat{\mathcal P}''$ requires only $\mu(\{x_0\}) \ge \max(0, 1-\alpha-\alpha D^2 h)$.

Significance

The result gives a physical meaning to the parameter $\alpha$ of the shrinkage heuristic: $1-\alpha$ is a lower bound on the probability that the system is in its nominal state. The error $\alpha D^2 h$ vanishes when the objective is linear in the parameter (Corollary 4.2), which covers linear programs with uncertain costs and Markov decision processes with uncertain rewards; in that case shrinkage is exactly a two-scenario DRSP. The paper also shows by example (p. 104) that without a curvature condition the two problems can differ, so the Hessian bound is the operative hypothesis.

The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it adds a checked link between the discrete two-point structure of the DRSP value and the smooth analysis of the shrunken minimum, with every standing hypothesis written out (see below). The mean-value and gradient-Lipschitz steps are general facts about functions on Euclidean space with bounded Hessian and are reusable elsewhere.

Difficulty

Two points need care. First, the step from the Hessian bound $-hI \preceq H_v \preceq hI$, a bound on a quadratic form, to the Lipschitz bound on the gradient requires the operator norm of the Hessian, which equals the largest absolute value of its quadratic form only because the Hessian is symmetric; symmetry of second derivatives must be invoked for a function that is merely twice (Fréchet) differentiable, not twice continuously differentiable. Second, the DRSP value is an infimum over an infinite-dimensional set of measures; identifying it with the two-point value requires both a construction of a near-optimal measure and a lower bound valid for every admissible measure, including measures that spread their abnormal mass over all of $x_0 + \Delta$.

Formalization scope

$\mathbb{R}^m$ is EuclideanSpace ℝ (Fin m) with its Borel $\sigma$-algebra. Measures are Measures, and membership in $\hat{\mathcal P}'$ includes IsProbabilityMeasure. Infima are real infima over subtypes; integrals are Bochner integrals.

The formalization makes the following readings explicit:

1. $\Delta$ is compact. The page writes min over $\alpha\Delta$ and max over $\Delta$, which presuppose attainment. Compactness together with continuity of $f(v,\cdot)$ gives attainment, a finite $D$, finite integrals and measurability of $x_0 + \Delta$. The goal additionally states that the minimum over $\alpha\Delta$ is attained.
2. $0 \in \Delta$. Without it $\hat{\mathcal P}'$ is empty, since $\mu(\{x_0\}) \ge 1-\alpha > 0$ and $\mu(x_0+\Delta)=1$ force $x_0 \in x_0 + \Delta$. The page's two-scenario reading presupposes it. In Corollary 4.3 it follows from star-shapedness once $\Delta$ is nonempty, and nonemptiness is added there.
3. Twice differentiable with bounded Hessian means that $f(v,\cdot)$ and its derivative are differentiable everywhere and $|D^2 f(v,\cdot)(x)[y,y]| \le h\|y\|_2^2$ for all $x, y$. The constant $h$ is one constant for all $v$.
4. The minima over $\Delta$ and $\alpha\Delta$ are written as infima, which equal the minima under the hypotheses above.

The Lean functions drspValue and devRadius return $0$ on an empty or unbounded input; the hypotheses above exclude those inputs, so no statement holds through a junk value. A formalization that dropped $0 \in \Delta$ would make the inequalities hold or fail for the wrong reason and is ruled out.

Contributions welcome: the Lipschitz-gradient lemma for bounded Hessians in Euclidean space, the evaluation of the two-scenario DRSP value, and the combination into Theorem 4.1 and its corollaries.

Selected references

• H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
• E. Delage, S. Mannor, Percentile Optimization for Markov Decision Processes with Parameter Uncertainty, Operations Research 58(1):203–213, 2010. https://doi.org/10.1287/opre.1080.0685
• E. Delage, Y. Ye, Distributionally Robust Optimization under Moment Uncertainty with Applications to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• D. Bertsimas, D. B. Brown, C. Caramanis, Theory and Applications of Robust Optimization, SIAM Review 53(3):464–501, 2011. https://doi.org/10.1137/080734510