Convex Optimization

Motivation

First order methods (projected gradient, fast gradient) converge only sublinearly on general smooth convex problems, at rates $O(1/k)$ and $O(1/k^2)$ in function value. Linear convergence is classically proved under strong convexity, which fails for many problems arising in practice: least squares with a rank-deficient matrix, dual problems of linearly constrained programs, and compositions $f(x)=g(Ax)$ of a strongly convex $g$ with a singular linear map. For such problems the optimal set is not a single point, yet projected gradient methods are still observed to converge linearly.

Necoara, Nesterov and Glineur (arXiv:1504.06298, later Math. Program. 175 (2019)) introduce a hierarchy of relaxations of strong convexity, each obtained by evaluating a strong convexity inequality only at the projection of a point onto the optimal set, and show that first order methods converge linearly on each class. Two of these relaxations are the subject of this mission: quadratic functional growth and the global error bound stated with the gradient mapping. Error bounds of this kind go back to Luo and Tseng (Ann. Oper. Res. 46 (1993)) and Tseng's analysis of feasible descent methods; quadratic growth conditions appear in Anitescu and in Drusvyatskiy–Lewis (Math. Oper. Res. 43 (2018)).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $\langle u,v\rangle=u^\top v$ and norm $\|\cdot\|$. Problem (P) is

$$f^*=\min_{x\in X} f(x),$$

with $X\subseteq\mathbb R^n$ closed and convex and $f$ convex on $X$, differentiable on $X$, with Lipschitz continuous gradient of constant $L_f>0$ on $X$: $\|\nabla f(x)-\nabla f(y)\|\le L_f\|x-y\|$ for all $x,y\in X$. The optimal set $X^*=\{x\in X: f(x)\le f(y)\ \forall y\in X\}$ is assumed nonempty.

For a set $S$ and a point $u$, $[u]_S$ denotes a point of $S$ nearest to $u$; for nonempty closed convex $S$ it exists and is unique. Write $\bar x=[x]_{X^*}$. The projected gradient step from $x\in X$ is $x^+=[x-\tfrac1{L_f}\nabla f(x)]_X$, and the gradient mapping is

$$g(x)=L_f\,(x-x^+).$$

When $X=\mathbb R^n$, $g(x)=\nabla f(x)$.

• $f$ has quadratic functional growth (22) with constant $\kappa_f>0$ if $f(x)-f^*\ge\frac{\kappa_f}{2}\|x-\bar x\|^2$ for all $x\in X$.
• $f$ satisfies the global error bound (31) with constant $\kappa_f>0$ if $\|g(x)\|\ge\kappa_f\|x-\bar x\|$ for all $x\in X$.

The condition number is $\mu_f=\kappa_f/L_f$. In Lean these are QuadFunGrowth X f κ and ErrorBound X f Lf κ, with $g(x)$ written Lf • (x - xp).

Formalization targets

Goal: Theorem 7

Quadratic functional growth with constant $\kappa_f$ implies the global error bound with constant $\frac{1}{1+\mu_f+\sqrt{1+\mu_f}}\cdot\kappa_f$:

$$\|g(x)\|\ \ge\ \frac{\kappa_f}{1+\mu_f+\sqrt{1+\mu_f}}\,\|x-\bar x\|\qquad\forall x\in X .$$

In class notation, $\mathcal F_{L_f,\kappa_f}(X)\subseteq\mathcal E_{L_f,\kappa_f/(1+\mu_f+\sqrt{1+\mu_f})}(X)$.

Milestones

1. The decrease (28) of a projected gradient step: $f(x^+)\le f(x)-\frac{L_f}{2}\|x^+-x\|^2$.
2. The gradient mapping inequality (29): $f(y)\ge f(x^+)+\langle g(x),y-x\rangle+\frac{1}{2L_f}\|g(x)\|^2$ for $y\in X$.
3. The first chain of the proof of Theorem 7: with $\bar x^+=[x^+]_{X^*}$, $\langle g(x),x^+-\bar x^+\rangle+\frac1{2L_f}\|g(x)\|^2\ge f(x^+)-f^*\ge\frac{\kappa_f}{2}\|x^+-\bar x^+\|^2$.
4. The error bound at $x^+$: $\|g(x)\|\ge\bigl(\sqrt{L_f(\kappa_f+L_f)}-L_f\bigr)\|x^+-\bar x^+\|$.

Companion: Theorem 6

The converse direction, also included as a draft theorem: the error bound with $\kappa_f$ implies quadratic functional growth with constant $\mu_f\cdot\kappa_f$.

Significance

Theorems 6 and 7 together show that, for convex functions with Lipschitz gradient on a closed convex set, quadratic functional growth and the gradient-mapping error bound define the same class of functions up to a change of constant depending only on $\mu_f$. A linear convergence proof for projected gradient methods under one condition therefore transfers to the other, and the paper uses this to place the error-bound class $\mathcal E$ inside its hierarchy of relaxations of strong convexity. The explicit constant matters downstream: rates of the form $(1-c\,\mu_f)^k$ inherit it.

The results are proved in the paper. No machine-checked proof of Theorems 6–7 is known to exist. Related statements formalized elsewhere on the platform concern the unconstrained case (Karimi–Nutini–Schmidt, where $\nabla f$ replaces $g$) or the proximal-gradient error bound on sublevel sets (Drusvyatskiy–Lewis), with different constants. A complete development here yields a reusable library of projected-gradient facts on a general closed convex set: the descent inequality, the gradient-mapping inequality and the existence and characterization of projections.

Difficulty

The obvious approach applies (22) at $x$ and tries to bound $f(x)-f^*$ by $\|g(x)\|\,\|x-\bar x\|$, as in the unconstrained case where $g=\nabla f$ and convexity gives $f(x)-f^*\le\langle\nabla f(x),x-\bar x\rangle$. On a constrained set this fails: $g(x)$ is not a subgradient of $f$ at $x$, and the available inequality for the gradient mapping, (29), controls $f$ only through the value $f(x^+)$ at a different point. Relating the distance to $X^*$ at that point to the distance at $x$, without losing the exact constant $\kappa_f/(1+\mu_f+\sqrt{1+\mu_f})$, is the central difficulty.

At the Lean level, the descent inequality (2) has to be derived on a convex set from a Lipschitz condition assumed only on $X$, and the variational characterization of the Euclidean projection has to be connected to the nearest-point predicate.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). $f$ is a real function on all of $\mathbb R^n$, convex on $X$ (ConvexOn ℝ X f), differentiable at every point of $X$, with $\nabla f$ = gradient f; its values off $X$ never enter.
• Standing assumptions of p. 3 as hypotheses: $X$ closed and convex; (1) on $X$ with $0<L_f$; a named optimal point $x^\star\in X^*$, so $X^*$ is never empty. The paper's "simple" (cheap projection) is not a mathematical assumption and is dropped; "closed convex function" adds nothing for a real-valued convex function continuous on $X$. $X^*$ closed and $f^*$ finite follow and are not assumed.
• Projections are predicates (IsNearest), not choice functions; $x^+$ is the predicate IsPGStep. Every statement quantifies over all points satisfying them. Nearest points in nonempty closed convex sets exist, so these quantifiers are not vacuous.
• $f^*$ is written $f(\bar x)$ for $\bar x\in X^*$, never as an infimum.
• The constant of Theorem 7 is written $\kappa/(1+\kappa/L_f+\sqrt{1+\kappa/L_f})$, of Theorem 6 $\kappa/L_f\cdot\kappa$. $\kappa_f\le L_f$ is not assumed.
• (29) is stated for $x\in X$ rather than $x\in\mathbb R^n$, since $\nabla f$ is only meaningful on $X$ under the standing assumptions.

A trivializing formalization is ruled out: the error bound uses the gradient mapping $g(x)$ and not $\nabla f(x)$, the projections are not defined by choice, $X^*$ is nonempty, and no junk gradient value off the differentiability set is used.

Needed infrastructure: the descent lemma on a convex set, the obtuse-angle characterization of the projection onto a closed convex set, existence of nearest points (Mathlib's exists_norm_eq_iInf_of_complete_convex), and closedness and convexity of $X^*$. These are reusable well beyond this mission; proofs of the milestones and of Theorem 6 are welcome independently.

Selected references

• I. Necoara, Yu. Nesterov, F. Glineur, Linear convergence of first order methods for non-strongly convex optimization, arXiv:1504.06298v4, 2016; Math. Program. 175 (2019) 69–107. https://arxiv.org/abs/1504.06298
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004, Theorem 2.2.7. https://doi.org/10.1007/978-1-4419-8853-9
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
• D. Drusvyatskiy, A. S. Lewis, Error bounds, quadratic growth, and linear convergence of proximal methods, Math. Oper. Res. 43 (2018) 919–948. https://doi.org/10.1287/moor.2017.0889
• H. Karimi, J. Nutini, M. Schmidt, Linear convergence of gradient and proximal-gradient methods under the Polyak–Łojasiewicz condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636

Motivation

Linear convergence of gradient-type methods is classically proved under strong convexity. Many problems that arise in practice are not strongly convex: dual formulations of linearly constrained convex problems, least-squares and logistic-type regression with rank-deficient data matrices, convex quadratic programs, and routing problems in data networks all have objectives of the form $f(x)=g(Ax)$, where $g$ is strongly convex and smooth but the matrix $A$ has a nontrivial kernel. Such an $f$ is constant along $\ker A$, so it is not strongly convex, and its set of minimizers need not be a single point.

Necoara, Nesterov and Glineur (arXiv:1504.06298v4, published in Math. Program. 175 (2019)) introduce a chain of relaxations of strong convexity: quasi-strong convexity, quadratic gradient growth and quadratic functional growth. They show that projected and fast gradient methods still converge linearly under them. Section 4 of the paper supplies the main examples: compositions $g(Ax)$, possibly with a linear term and polyhedral constraints. This mission formalizes those examples. The tool behind them is the error bound of Hoffman (1952) for systems of linear inequalities; its use for linear convergence goes back to Luo and Tseng (1993) and Wang and Lin (2014).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $\langle u,v\rangle=u^Tv$ and norm $\|\cdot\|$. For a set $X$ and a function $f$, the optimal set is $X^*=\{x\in X: f(x)\le f(y)\ \forall y\in X\}$ and $f^*$ is the optimal value. A nearest point $\bar x=[x]_S$ of a set $S$ to $x$ is a point of $S$ minimizing $\|x-z\|$ over $z\in S$.

The data are:

1. a linear map $A:\mathbb R^n\to\mathbb R^m$, $A\neq0$, with operator (spectral) norm $\|A\|$;
2. a polyhedral feasible set $X=\{x: Cx\le d\}$, with $C:\mathbb R^n\to\mathbb R^p$ linear and the inequality read componentwise;
3. a differentiable function $g:\mathbb R^m\to\mathbb R$ that is $\sigma_g$-strongly convex, $g(\alpha u+(1-\alpha)v)\le\alpha g(u)+(1-\alpha)g(v)-\frac{\sigma_g\alpha(1-\alpha)}2\|u-v\|^2$, and whose gradient is $L_g$-Lipschitz.

The objective is $f(x)=g(Ax)$, or $f(x)=g(Ax)+c^Tx$ in the extensions. The function $f$ has Lipschitz gradient with constant $L_f$ on $X$ if $\|\nabla f(x)-\nabla f(y)\|\le L_f\|x-y\|$ for $x,y\in X$. It is quasi-strongly convex with constant $\kappa$ if, for every $x\in X$ and $\bar x=[x]_{X^*}$,

$$f^*\ge f(x)+\langle\nabla f(x),\bar x-x\rangle+\tfrac\kappa2\|x-\bar x\|^2 .$$

The class $q\mathcal S_{L_f,\kappa_f}(X)$ collects the convex functions with $L_f$-Lipschitz gradient on $X$ satisfying this inequality with $\kappa_f$. The classes $\mathcal G_{L_f,\kappa_f}$ (quadratic gradient growth, $\langle\nabla f(x)-\nabla f(\bar x),x-\bar x\rangle\ge\kappa\|x-\bar x\|^2$) and $\mathcal F_{L_f,\kappa_f}$ (quadratic functional growth, $f(x)-f^*\ge\frac\kappa2\|x-\bar x\|^2$) are defined the same way.

A Hoffman constant $\theta(A,C)>0$ for the polyhedron $P=\{z: Az=t,\ Cz\le d\}$ is a number with

$$\|x-\bar x\|\le\theta(A,C)\sqrt{\|Ax-t\|^2+\|[Cx-d]_+\|^2}\qquad\forall x\in\mathbb R^n,\ \bar x=[x]_P ,$$

where $[v]_+$ is the componentwise positive part.

Formalization targets

Goal: Theorem 8

If $x^*$ is optimal for $\min_{x\in X}g(Ax)$ and $\theta(A,C)>0$ is a Hoffman constant for $\{z: Az=Ax^*,\ Cz\le d\}$, then

$$f=g\circ A\in q\mathcal S_{L_f,\kappa_f}(X),\qquad L_f=L_g\|A\|^2,\qquad \kappa_f=\frac{\sigma_g}{\theta^2(A,C)} .$$

Milestones

1. $\|\nabla f(x)-\nabla f(y)\|\le L_g\|A\|^2\|x-y\|$ on $X$.
2. (39): $Ax^*$ and $\nabla f(x^*)$ are the same for every $x^*\in X^*$.
3. $X^*=\{x: Ax=Ax^*,\ Cx\le d\}$.
4. For feasible $x$, $\|x-\bar x\|\le\theta(A,C)\|Ax-A\bar x\|$.

Companions

• Theorem 9: without constraints, $g(Ax)+c^Tx\in\mathcal G_{L_g\|A\|^2,\ \sigma_g/\theta^2(A,0)}(\mathbb R^n)$.
• Theorem 10: on $X=\{Cx\le d\}$ and for every $M>0$, $g(Ax)+c^Tx\in\mathcal F_{L_f,\kappa_f}(X_M)$ on the sublevel set $X_M=\{x\in X: f(x)-f^*\le M\}$, with $\kappa_f=\sigma_g/\big(\theta^2(A,c,C)(1+M\sigma_g+2c_g^2)\big)$ and $c_g=\|\nabla g(Ax^*)\|$.
• Example 1: $\tfrac12x_1^2+x_2$ on $\mathbb R^2_+$ has no global quadratic growth constant, but $\kappa_f(M)=\min\{1,1/M\}$ works on $\{f\le M\}$ for $M\ge1$.

Significance

Theorem 8 makes the linear convergence results of the paper apply to the whole family $g(Ax)$ over polyhedra. That family covers the duals of linearly constrained strongly convex problems and regression with arbitrary design matrices. The rate is explicit in $\sigma_g$, $L_g$, $\|A\|$ and the Hoffman constant. Theorems 9 and 10 extend the picture to a linear term, at the cost of moving to weaker classes. Example 1 shows that the sublevel restriction in Theorem 10 is needed.

All of these results are proved in the paper. None of them has a machine-checked proof that this mission is aware of. A formal development would produce a Lean proof of the class membership, a formal chain-rule computation of the gradient of $g\circ A$, and the strict-convexity argument that $A$ is constant on the optimal set. These pieces are reusable wherever a composite objective with a rank-deficient linear map appears.

Difficulty

The obvious route, strong convexity of $f$, fails as soon as $\ker A\neq\{0\}$. Two separate facts have to replace it. The first is that the minimizers of a strongly convex function composed with $A$ share the image point $Ax^*$, so the optimal set is itself a polyhedron. The second is that the distance to that polyhedron is controlled linearly by the residual $\|Ax-Ax^*\|$ on feasible points, which is exactly a Hoffman error bound. Neither follows from local information at a single minimizer. In Theorem 10 the linear term destroys the first fact's simplicity: the value $c^Tx$ must also be controlled, and that is possible only on bounded sublevel sets.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). $A$ and $C$ are continuous linear maps, so $\|A\|$ is the operator norm, which is the spectral norm of the page; it is never the Frobenius norm. Strong convexity is Mathlib's StrongConvexOn Set.univ σg g, which is (5) on all of $\mathbb R^m$. The page's "$L_g$-Lipschitz gradient on $X$" is read on $\mathbb R^m$, the domain of $g$. The gradient of the composition is always gradient (fun z => g (A z)), and the identity $\nabla f(x)=A^T\nabla g(Ax)$ is a proof step, not part of any statement. $f^*$ is the value at a nearest point of $X^*$, which is exact because that point is optimal.

Standing assumptions of p. 3: the feasible set is closed and convex (automatic for a polyhedron), the optimal set is nonempty (a named optimal point $x^*$ is a hypothesis), and $f$ has Lipschitz gradient (a conclusion here). The "simple" set and "closed" function add no mathematical content and are dropped. The Hoffman constant is a hypothesis, because the page cites its existence (Hoffman 1952) rather than proving it. The hypothesis is the Hoffman inequality for the specific polyhedron $\{Az=Ax^*,\ Cz\le d\}$, not for every right-hand side.

Trivializing formalizations are ruled out. The projection is a predicate (IsNearest), never a choice function. The optimal set is nonempty by hypothesis. $g$ is differentiable everywhere, so no gradient takes a junk value. A sorry-free sanity file shows that the hypotheses of Theorems 8–10 are jointly satisfiable ($A=\mathrm{id}$ on $\mathbb R^1$, $g=\|\cdot\|^2/2$, $\theta=1$).

A complete development needs the chain rule for gradients through a continuous linear map and its adjoint, first-order characterizations of strong convexity, and optimality conditions for convex differentiable functions on convex sets. Contributions of these as reusable lemmas are welcome, as are proofs of the companion theorems.

Selected references

• I. Necoara, Yu. Nesterov, F. Glineur, Linear convergence of first order methods for non-strongly convex optimization, arXiv:1504.06298v4, 2016; Math. Program. 175 (2019) 69–107. https://arxiv.org/abs/1504.06298
• A. J. Hoffman, On approximate solutions of systems of linear inequalities, J. Res. Nat. Bur. Standards 49 (1952) 263–265. https://doi.org/10.6028/jres.049.027
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
• P.-W. Wang, C.-J. Lin, Iteration complexity of feasible descent methods for convex optimization, J. Mach. Learn. Res. 15 (2014) 1523–1548. https://jmlr.org/papers/v15/wang14a.html
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

First-order methods (projected gradient, fast gradient, feasible descent) converge linearly on smooth strongly convex problems, but many problems met in practice are not strongly convex: least squares with a rank-deficient matrix, the dual of a linearly constrained problem, or $g(Ax)$ with $g$ strongly convex and $A$ singular. Such problems have a whole set of minimisers, and strong convexity, which forces a unique minimiser, fails. Necoara, Nesterov and Glineur (arXiv:1504.06298; Math. Program. 175 (2019)) introduce a family of conditions that relax strong convexity by testing it only against the projection onto the optimal set, and prove that the classical first-order methods still converge linearly under them.

Related unconstrained conditions predate the paper: restricted strong convexity for $X=\mathbb R^n$ (Zhang and Cheng, Optim. Lett. 2015, the paper's reference [16]), and the error bounds of Luo and Tseng (1993). Karimi, Nutini and Schmidt (arXiv:1608.04636, 2016) compared similar unconstrained conditions with the Polyak–Łojasiewicz inequality. The constrained hierarchy treated here, with one constant along the whole chain, is the first section of the Necoara–Nesterov–Glineur paper and the basis of its convergence results.

This mission formalizes that hierarchy: Theorem 4 of the paper (arXiv v4, p. 9) and the results it is assembled from.

Setting

Let $X\subseteq\mathbb R^n$ be a closed convex set, with the Euclidean inner product $\langle u,v\rangle=u^\top v$ and norm $\|u\|$. Let $f$ be a convex function on $X$, differentiable at every point of $X$, with gradient $\nabla f$ Lipschitz on $X$ with constant $L_f>0$:

$$\|\nabla f(x)-\nabla f(y)\|\le L_f\|x-y\|\qquad\forall x,y\in X. \tag{1}$$

The optimal set $X^*=\{x\in X: f(x)\le f(y)\ \forall y\in X\}$ is assumed nonempty, and $f^*$ is the optimal value. For $x\in X$, $\bar x=[x]_{X^*}$ denotes the projection of $x$ onto $X^*$: the point of $X^*$ nearest to $x$.

For a constant $\kappa>0$ the paper considers five inequalities, for all $x,y\in X$:

• (7), first-order strong convexity: $f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac{\kappa}{2}\|x-y\|^2$;
• (10), quasi-strong convexity: $f^*\ge f(x)+\langle\nabla f(x),\bar x-x\rangle+\frac{\kappa}{2}\|x-\bar x\|^2$;
• (13), quadratic under-approximation: $f(x)\ge f^*+\langle\nabla f(\bar x),x-\bar x\rangle+\frac{\kappa}{2}\|x-\bar x\|^2$;
• (17), quadratic gradient growth: $\langle\nabla f(x)-\nabla f(\bar x),x-\bar x\rangle\ge\kappa\|x-\bar x\|^2$;
• (22), quadratic functional growth: $f(x)-f^*\ge\frac{\kappa}{2}\|x-\bar x\|^2$.

The classes $\mathcal S_{L_f,\kappa}(X)$, $q\mathcal S_{L_f,\kappa}(X)$, $\mathcal G_{L_f,\kappa}(X)$, $\mathcal U_{L_f,\kappa}(X)$, $\mathcal F_{L_f,\kappa}(X)$ are the convex functions satisfying (1) and, respectively, (7), (10), (17), (13), (22). In Lean these are the predicates StrongIneq, QuasiStrong, QuadGradGrowth, QuadUnder and QuadFunGrowth of NecoaraNG.Chain.Setting, over optSet X f and the nearest-point predicate IsNearest.

Formalization targets

Goal: Theorem 4 (p. 9)

With the same constant $\kappa$ at every step,

$$(7)\Rightarrow(10)\Rightarrow(17)\Rightarrow(13)\Rightarrow(22),$$

that is

$$\mathcal S_{L_f,\kappa}(X)\subseteq q\mathcal S_{L_f,\kappa}(X)\subseteq\mathcal G_{L_f,\kappa}(X)\subseteq\mathcal U_{L_f,\kappa}(X)\subseteq\mathcal F_{L_f,\kappa}(X). \tag{23}$$

The goal is the conjunction of the four implications under the standing assumptions.

Milestones

1. The projection onto $X^*$ is constant along $[\bar x,x]$: $[\bar x+t(x-\bar x)]_{X^*}=\bar x$ for $t\in[0,1]$ (proof of Theorem 3, p. 8).
2. (11), p. 5: $(7)\Rightarrow(10)$.
3. Theorem 1, p. 6: $(10)\Rightarrow(13)$.
4. Theorem 2, p. 7: $(10)\Rightarrow(17)$.
5. Theorem 3, p. 8: $(17)\Rightarrow(13)$.
6. Proof of Theorem 4, p. 9: $(13)\Rightarrow(22)$.

A companion item states the remark on p. 7: for convex $f$, (10) alone or (13) alone gives (17) with constant $\kappa/2$.

Significance

The chain gives the hierarchy that the paper's convergence theorems are stated for: the projected gradient method converges linearly on $q\mathcal S$ and, in distance to $X^*$, exactly on $\mathcal F$; the fast gradient method keeps its accelerated rate on $q\mathcal S$; and $g(Ax)$ with $g$ strongly convex is in $q\mathcal S$ on a polyhedron. Each such result transfers down the chain once the inclusions are known, and the fact that one $\kappa$ survives every link is what keeps the rates' constants explicit.

All the statements are proved in the paper. None of them is formalized: the platform has unconstrained analogues (the Karimi–Nutini–Schmidt chain, with an existential constant and no feasible set), but no constrained statement and no statement with a fixed constant. A formal proof would also check the projection-invariance step that the paper uses without comment.

Difficulty

The links $(7)\Rightarrow(10)$ and $(13)\Rightarrow(22)$ are one-line substitutions. The substance is in Theorems 1 and 3, and specifically in the constant: combining (10) or (13) with the convexity inequality at a single pair of points gives (17) only with constant $\kappa/2$ (the companion item), and the same loss of a factor 2 appears in a direct derivation of (13) from (10). Keeping the full constant $\kappa$ is what makes (23) a chain of inclusions with one index, and it is where the geometry of the optimal set enters: the conditions are tested only against the projection $\bar x$, which moves with $x$. Convexity of $f$ cannot be dropped: (10) alone does not even imply convexity (p. 5).

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $\nabla f$ is Mathlib's gradient f. The function $f$ is defined on all of $\mathbb R^n$, with differentiability assumed at every point of $X$; "continuously differentiable" on $X$ follows from (1).
• Standing assumptions as hypotheses of every theorem: $X$ closed and convex, $f$ convex on $X$ (ConvexOn ℝ X f), (1) with $L_f>0$, a minimiser $x^*\in X^*$, $\kappa>0$. "Simple" (cheap projection) and "closed" for $f$ carry no mathematical content here and are dropped.
• $[x]_{X^*}$ is the predicate IsNearest (optSet X f) x xbar; each condition is required for every nearest point. $f^*$ is written $f(\bar x)$, which is exact because $\bar x\in X^*$.
• An empty optimal set would make every condition vacuous; the hypothesis $x^*\in X^*$ excludes this. The projection is never a choice function, and the gradient is only evaluated at points of $X$, where $f$ is differentiable, so no junk value enters a statement. (7) is the first-order inequality with $\nabla f$, not Mathlib's StrongConvexOn.
• Needed infrastructure: the fundamental theorem of calculus along a segment for a function differentiable on a convex set, first-order optimality for a minimiser over a convex set, and the elementary geometry of nearest points. All of it is reusable for the other missions of this series.

Selected references

• I. Necoara, Yu. Nesterov, F. Glineur, Linear convergence of first order methods for non-strongly convex optimization, arXiv:1504.06298v4, 2016; Math. Program. 175 (2019) 69–107. https://arxiv.org/abs/1504.06298
• H. Karimi, J. Nutini, M. Schmidt, Linear convergence of gradient and proximal-gradient methods under the Polyak–Łojasiewicz condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
• H. Zhang, L. Cheng, Restricted strong convexity and its applications to convergence analysis of gradient type methods in convex optimization, Optim. Lett. 9 (2015) 961–979. https://doi.org/10.1007/s11590-014-0795-x
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46 (1993) 157–178. https://doi.org/10.1007/BF02096261

Motivation

In decentralized optimization a group of agents minimizes a sum of functions without a central coordinator: agent $i$ knows only its own function $f_i$ and can exchange vectors only with its neighbours in a communication network. The setting covers sensor networks, multi-robot coordination and data-parallel learning in which the data cannot be pooled. The basic algorithm is decentralized gradient descent (DGD), in which every agent averages its neighbours' iterates and takes a local gradient step. It goes back to Nedić and Ozdaglar's distributed subgradient method (IEEE TAC 2009), which used diminishing stepsizes.

Practitioners often run DGD with a fixed stepsize, and with a fixed stepsize DGD does not reach consensus at an optimum: the local gradient term keeps pushing the agents apart. Yuan, Ling and Yin (arXiv:1310.7063v3; SIAM J. Optim. 26(3), 2016) quantify what a fixed stepsize achieves. They show that bounded gradients follow from a stepsize condition rather than being assumed, that the agents stay within $O(\alpha/(1-\beta))$ of their mean, and that under (restricted) strong convexity every agent converges geometrically to an $O(\alpha/(1-\beta))$ neighbourhood of the solution set. This mission formalizes that linear-rate result, Corollary 1 of the paper (p. 14). A companion mission covers the sublinear rate of the convex case (Theorem 2).

Setting

There are $n\ge2$ agents and a decision space $\mathbb R^p$. Agent $i$ holds $f_i:\mathbb R^p\to\mathbb R$, and the agents solve

$$\min_{x\in\mathbb R^p}\ f(x)=\sum_{i=1}^n f_i(x), \qquad (2)$$

with solution set $\mathcal X^*$, assumed nonempty. The network is a graph $G$ on the agents, and the mixing matrix $W=[w_{ij}]$ has $w_{ij}\ne0$ only if $i=j$ or $i,j$ are neighbours. Starting from $x_{(i)}(0)=0$, DGD with stepsize $\alpha$ updates all agents at once:

$$x_{(i)}(k+1)=\sum_{j=1}^n w_{ij}\,x_{(j)}(k)-\alpha\nabla f_i\big(x_{(i)}(k)\big),\qquad i=1,\dots,n. \qquad (4)$$

If $W$ is symmetric, its eigenvalues are real and sorted with multiplicity as $\lambda_1(W)\ge\dots\ge\lambda_n(W)$. The network enters through the second largest eigenvalue magnitude

$$\beta=\max\{|\lambda_2(W)|,|\lambda_n(W)|\}. \qquad (5)$$

Assumption 1 (p. 4): (a) each $f_i$ is convex, differentiable and bounded below, and $\nabla f_i$ is Lipschitz with constant $L_{f_i}>0$; (b) the network is connected, and $W$ is symmetric and doubly stochastic with $\beta<1$.

Write $L_h=\max_iL_{f_i}$, $f_i^o=\inf f_i$, and

$$D=\sqrt{2L_h\sum_{i=1}^n\big(f_i(0)-f_i^o\big)}. \qquad (10)$$

The mean iterate is $\bar x(k)=\frac1n\sum_ix_{(i)}(k)$, and $\bar f=\frac1n\sum_if_i$ has gradient Lipschitz constant $L_{\bar f}=\frac1n\sum_iL_{f_i}$. The function $f$ is strongly convex with modulus $\mu_f>0$ if $\langle\nabla f(x_a)-\nabla f(x_b),x_a-x_b\rangle\ge\mu_f\|x_a-x_b\|^2$ for all $x_a,x_b$. It is restricted strongly convex with modulus $\nu_f>0$ if the same holds with $x_b=\mathrm{Proj}_{\mathcal X^*}(x_a)$ only (7). The solution error is $\bar e(k)=\bar x(k)-x^*(k)$ with $x^*(k)=\mathrm{Proj}_{\mathcal X^*}(\bar x(k))$. Lemma 3 (p. 12) supplies constants $c_1,c_2$: in the strongly convex case $c_1=1/(\mu_{\bar f}+L_{\bar f})$ and $c_2=\mu_{\bar f}L_{\bar f}/(\mu_{\bar f}+L_{\bar f})$; in the restricted case $c_1=\theta/L_{\bar f}$ and $c_2=(1-\theta)\nu_{\bar f}$ with $\theta\in[0,1]$. Here $\mu_{\bar f}=\mu_f/n$ and $\nu_{\bar f}=\nu_f/n$.

Formalization targets

Goal: Corollary 1 (p. 14)

Under Assumption 1, if $f$ is strongly or restricted strongly convex with $c_2>0$, and $0<\alpha<\min\{(1+\lambda_n(W))/L_h,\,c_1\}$, then for every $k\ge0$ and every agent $i$

$$\|x_{(i)}(k)-x^*(k)\|\le c_3^k\|x^*(0)\|+\frac{c_4}{\sqrt{1-c_3^2}}+\frac{\alpha D}{1-\beta},$$

where $c_3=\sqrt{1-\alpha c_2/2}$ and $c_4^2=\alpha^3(\alpha+\delta^{-1})L_h^2D^2/(1-\beta)^2$ at $\delta=c_2/(2(1-\alpha c_2))$.

Milestones

1. Theorem 1, (10), p. 7: under $\alpha\le(1+\lambda_n(W))/L_h$, the stacked gradient satisfies $\|h(k)\|\le D$ for all $k$.
2. Lemma 1, p. 8: $\|x_{(i)}(k)-\bar x(k)\|\le\alpha D/(1-\beta)$.
3. Lemma 2, p. 10: $\|\nabla f_i(x_{(i)}(k))-\nabla f_i(\bar x(k))\|\le\alpha DL_{f_i}/(1-\beta)$ and $\|g(k)-\bar g(k)\|\le\alpha DL_h/(1-\beta)$.
4. (15), p. 10: $\bar x(k+1)=\bar x(k)-\alpha g(k)$.
5. Lemma 3 (a), p. 12: the strongly convex case, already on the platform as ConvexOptAlg.StrongGD.lemma_3_11.
6. Lemma 3 (b), p. 12: the restricted strongly convex case.
7. Theorem 3, p. 12: $\|\bar e(k+1)\|^2\le c_3^2\|\bar e(k)\|^2+c_4^2$ for every $\delta>0$.
8. Theorem 3, "in particular", pp. 12–13: $\|\bar e(k)\|\le c_3^k\|\bar e(0)\|+c_4/\sqrt{1-c_3^2}$.

Significance

The result separates the two error sources of fixed-step DGD. The geometric term $c_3^k$ comes from the optimization, at a rate governed by $\alpha c_2$. The floor $c_4/\sqrt{1-c_3^2}+\alpha D/(1-\beta)$ is $O(\alpha/(1-\beta))$ and comes from the network. Halving the stepsize halves the floor but slows the rate, and a poorly connected network ($\beta$ close to $1$) inflates the floor. This trade-off motivated exact decentralized methods such as EXTRA and gradient tracking, which remove the floor. Corollary 1 is the baseline they are compared against.

The paper's proofs are short and have not been machine-checked. Formalizing them yields reusable Lean infrastructure for decentralized methods: stacked iterates in $\mathbb R^{np}$ with the Euclidean norm, mixing matrices and their spectral gap, the consensus bound of Lemma 1, and the inexact-gradient view (15) of the mean iterate. Lemma 3 (a) is already formalized on the platform (Bubeck, Lemma 3.11, Proved).

Difficulty

The algebra of Theorem 3 is routine once Lemmas 1–3 are available. The work lies elsewhere. Theorem 1 must derive bounded gradients from the stepsize condition alone, with no a priori bound on the iterates and with $\lambda_n(W)$ possibly negative. Lemma 1 requires the operator norm of $W^m-\frac1n\mathbf 1\mathbf 1^\top$, tensored with the identity on $\mathbb R^p$, to equal $\beta^m$, which needs the spectral theorem for symmetric matrices and the fact that $\beta<1$ makes the eigenvalue $1$ simple. Bounding $\|x_{(i)}(k)\|$ directly by summing gradient steps fails, because the bound grows with $k$: the consensus estimate has to go through the deviation from the mean. Lemma 3 (b) holds only at the projection onto $\mathcal X^*$, not at an arbitrary solution, which constrains how it can be applied.

Formalization scope

$\mathbb R^p$ is EuclideanSpace ℝ (Fin p), and stacked vectors live in PiLp 2 over the agents, so $\|h(k)\|$ is the Euclidean norm of $\mathbb R^{np}$, not a maximum norm. DGD is a recursively defined sequence from $x_{(i)}(0)=0$, not an arbitrary sequence with stated properties. $\lambda_2(W)$ and $\lambda_n(W)$ are entries of Mathlib's eigenvalues of a Hermitian matrix sorted nonincreasingly with multiplicity. The definitions return $0$ off the symmetric case, which Assumption 1 excludes. Gradients are Mathlib's gradient, $f_i^o$ is the infimum of $f_i$, and projections are nearest-point predicates. The Lemma 3 constants are a disjunction of the two cases, so the goal covers both.

Additions relative to the page, each disclosed in the items: $n\ge2$, so that $\lambda_2(W)$ exists; $\alpha>0$; $c_2>0$, which the page needs for $c_3<1$; $\mathcal X^*\ne\emptyset$, which is standing on p. 2; and the bound (10) at $k=0$, which Lemma 1's proof uses. Theorem 1's convergence sentence is not stated. It fails at the boundary stepsize $\alpha=(1+\lambda_n(W))/L_h$, and only the bound (10) is used downstream. A trivializing formalization is excluded: the iterates are those of (4), the stack norm is Euclidean, $\beta$ uses the sorted spectrum, and a two-agent instance with $W=\frac12\mathbf 1\mathbf 1^\top$ and $f_i=\|x\|^2/2$ satisfies every hypothesis of the goal. Contributions of proofs of any milestone are welcome. The spectral bound inside Lemma 1 and the descent argument for Theorem 1 are reusable beyond this mission.

Selected references

• K. Yuan, Q. Ling, W. Yin, On the Convergence of Decentralized Gradient Descent, SIAM J. Optim. 26(3), 2016; arXiv:1310.7063v3. https://arxiv.org/abs/1310.7063
• A. Nedić, A. Ozdaglar, Distributed Subgradient Methods for Multi-Agent Optimization, IEEE Trans. Automat. Control 54(1), 2009. https://doi.org/10.1109/TAC.2008.2009515
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004 (Theorem 2.1.12). https://doi.org/10.1007/978-1-4419-8853-9
• W. Shi, Q. Ling, G. Wu, W. Yin, EXTRA: An Exact First-Order Algorithm for Decentralized Consensus Optimization, SIAM J. Optim. 25(2), 2015. https://arxiv.org/abs/1404.6264
• S. Bubeck, Convex Optimization: Algorithms and Complexity, Found. Trends Mach. Learn. 8(3–4), 2015 (Lemma 3.11). https://arxiv.org/abs/1405.4980

Motivation

Many planning problems are made in two stages: a first decision is fixed before an uncertain parameter is observed, and a second, corrective decision is made afterwards. When the second-stage decisions are binary (which route, which facility, which crew), the resulting two-stage robust binary programs are notoriously hard: the second-stage decision is a function of the uncertain parameter, and no general finite reformulation is known.

Bertsimas and Caramanis (IEEE Trans. Automatic Control, 2010) proposed the K-adaptability approximation: instead of a full second-stage policy, the decision maker commits here-and-now to $K$ candidate second-stage decisions and implements the best of them once the parameter is known. Besides being computable, this matches practice in vehicle routing, production scheduling and emergency planning, where a small number of contingency plans is preferred to re-optimizing after every observation. The basic question is how many candidates are needed before nothing is lost. Hanasusanto, Kuhn and Wiesemann (Oper. Res. 63(4), 2015) answer it when the uncertainty affects only the objective function; this mission formalizes that answer, Theorem 1 of their paper.

Setting

The data are matrices $C\in\mathbb R^{Q\times N}$, $Q\in\mathbb R^{Q\times M}$, $T\in\mathbb R^{L\times N}$, $W\in\mathbb R^{L\times M}$, a vector $h\in\mathbb R^L$, a set $\mathcal X\subseteq\mathbb R^N_+$ of first-stage decisions $x$, a set $\mathcal Y\subseteq\{0,1\}^M$ of binary second-stage decisions $y$, and an uncertainty set

$$\Xi=\{\xi\in\mathbb R^Q : A\xi\le b\},$$

a nonempty bounded polyhedron. (The paper writes $Q$ both for the number of uncertain parameters and for the cost matrix; in Lean the dimension is nQ and the matrix Q.)

The two-stage robust binary program with objective uncertainty is

$$\mathcal{PO}:\qquad \min_{x\in\mathcal X}\ \max_{\xi\in\Xi}\Big[\xi^\top Cx+\min_{y\in\mathcal Y}\{\xi^\top Qy : Tx+Wy\le h\}\Big].$$

For $K\ge1$ and $\mathcal K=\{1,\dots,K\}$, the K-adaptability problem is

$$\mathcal{PO}_K:\qquad \min\Big\{\max_{\xi\in\Xi}\Big[\xi^\top Cx+\min_{k\in\mathcal K}\xi^\top Qy^k\Big] : x\in\mathcal X,\ y^k\in\mathcal Y,\ Tx+Wy^k\le h\ \ \forall k\in\mathcal K\Big\}.$$

The affine dimension $\dim\mathcal Y$ is the dimension of the smallest affine subspace containing $\mathcal Y$, and $\operatorname{rk}Q$ is the rank of the cost matrix $Q$.

Formalization targets

Goal: Theorem 1

For every number of policies $K\ge\min\{\dim\mathcal Y,\operatorname{rk}Q\}+1$,

$$\operatorname{opt}(\mathcal{PO}_K)=\operatorname{opt}(\mathcal{PO}).$$

Steps of the paper's proof (milestones)

1. Conservative approximation (p. 12): $\operatorname{opt}(\mathcal{PO})\le\operatorname{opt}(\mathcal{PO}_K)$ for every $K$.
2. With $K=|\mathcal Y|$ policies (p. ec1): $\operatorname{opt}(\mathcal{PO}_{|\mathcal Y|})=\operatorname{opt}(\mathcal{PO})$.
3. Min-max reformulation (EC.1) (p. ec1): for every decision,

$$\max_{\xi\in\Xi}\Big[\xi^\top Cx+\min_{k\in\mathcal K}\xi^\top Qy^k\Big]=\min_{\lambda\in\Delta_K}\max_{\xi\in\Xi}\Big[\xi^\top Cx+\sum_{k\in\mathcal K}\lambda_k\,\xi^\top Qy^k\Big],$$

with $\Delta_K$ the unit simplex in $\mathbb R^K$. 4. (EC.1) = (EC.2) (p. ec2): the randomized problem with $|\mathcal Y|$ policies has the same optimal value as the one with $\dim\mathcal Y+1$ policies; and, for the case $\operatorname{rk}Q<\dim\mathcal Y$, as the one with $\operatorname{rk}Q+1$ policies. 5. (EC.2) is the $(D+1)$-adaptability problem (p. ec2): for every $K$, the randomized problem with $K$ policies has the optimal value of $\mathcal{PO}_K$.

Significance

The set $\mathcal Y$ may contain exponentially many binary vectors, so a priori full adaptability could require exponentially many policies. Theorem 1 says that under objective uncertainty at most $\min\{M,\operatorname{rk}Q\}+1$ policies are ever needed, a number linear in the problem size. It justifies solving $\mathcal{PO}_K$ for small $K$ as an exact method rather than a heuristic whenever $\dim\mathcal Y$ or $\operatorname{rk}Q$ is small, and it is the reason the paper's mixed-integer linear reformulation of $\mathcal{PO}_K$ (Theorem 2) solves $\mathcal{PO}$ itself for such $K$. It also contrasts with the constraint-uncertainty case, where the same paper shows that every $K<|\mathcal Y|$ can leave a strict gap.

Theorem 1 is proved in the paper's e-companion. As far as is known, neither the theorem nor any step of its proof has a machine-checked proof; this mission produces one, together with reusable Lean statements of the problems $\mathcal{PO}$, $\mathcal{PO}_K$ and their randomized relaxations in the extended reals.

Difficulty

The obvious argument lists all feasible second-stage decisions as policies, which needs $|\mathcal Y|$ of them. Reducing this number is not a matter of discarding unused policies: for different $\xi$ different policies are optimal, and which subset of $\dim\mathcal Y+1$ policies suffices is not determined by any single $\xi$. The reduction to $\dim\mathcal Y+1$ policies holds only for the optimal value, not decision by decision, and it passes through a relaxation in which the policies are mixed with weights; exchanging the maximum over $\Xi$ with the minimum over the weights requires compactness and convexity of $\Xi$, and in Lean the exchange has to be carried out for extended-real values. The bound must also hold for every $K$ above the threshold, so monotonicity in the number of policies is part of the statement.

Formalization scope

• The data form one structure Problem N M L nQ R; its fields include the standing assumptions: $\mathcal X\subseteq\mathbb R^N_+$, every point of $\mathcal Y$ is a 0/1 vector ($\mathcal Y$ is a Finset), and $\Xi$ is nonempty and bounded. $\mathcal X$ is an arbitrary set (the paper allows mixed binary first-stage decisions).
• All objective functions and optimal values take values in EReal. Maxima and minima are suprema and infima, as in the paper's notation: a first-stage decision without a feasible second-stage decision has objective $+\infty$, and an infeasible problem has optimal value $+\infty$.
• Policies are indexed by Fin K and need not be distinct; every policy must satisfy $Tx+Wy^k\le h$, as in problem $\mathcal{PO}_K$ of Observation 1.
• $\dim\mathcal Y$ is Module.finrank ℝ (vectorSpan ℝ 𝒴) (so $\dim\emptyset=0$ in Lean; both optimal values are then $+\infty$), and $\operatorname{rk}Q$ is Matrix.rank.
• $\mathcal{PO}_K$ is defined with the minimum over the $K$ policies, not through weights $\lambda\in\Delta_K$; defining it through the randomized relaxation would make the min-max step true by definition and is ruled out.
• Proofs will need Sion's minimax theorem (Sion.minimax in Mathlib), Carathéodory's theorem (convexHull_eq_union), compactness of bounded polyhedra and extended-real iSup/iInf manipulation. Lemmas on suprema of linear functions over compact polyhedra and on min-max exchange in EReal are reusable beyond this mission. Proofs of any milestone, and alternative routes to the goal, are welcome.

Selected references

• G. A. Hanasusanto, D. Kuhn, W. Wiesemann, K-Adaptability in Two-Stage Robust Binary Programming, Operations Research 63(4), 877–891, 2015; formalized from the preprint, Optimization Online 2014/03/4294 (revision of 2015-03-30). https://doi.org/10.1287/opre.2015.1392
• D. Bertsimas, C. Caramanis, Finite Adaptability in Multistage Linear Optimization, IEEE Transactions on Automatic Control 55(12), 2751–2766, 2010. https://doi.org/10.1109/TAC.2010.2049764
• M. Sion, On General Minimax Theorems, Pacific Journal of Mathematics 8(1), 171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171

Motivation

Two-stage robust optimization models decisions taken in two steps around an uncertain parameter: a here-and-now decision $x$ is fixed before the parameter $\xi$ is revealed, and a wait-and-see decision $y$ adapts to it, and the decision maker guards against the worst $\xi$ in an uncertainty set $\Xi$. When the second-stage decisions are binary, as in routing, scheduling and network design, the exact two-stage problem is computationally out of reach. Bertsimas and Caramanis (IEEE TAC, 2010) proposed the K-adaptability approximation: choose $K$ second-stage policies $y^1,\dots,y^K$ here and now, and once $\xi$ is revealed implement the best of those that are feasible. Hanasusanto, Kuhn and Wiesemann (Oper. Res., 2015; preprint Optimization Online 2014/03/4294) study this problem in depth. When the uncertain parameter enters the second-stage constraints, the K-adaptability problem is in general neither convex nor continuous, and to obtain a solvable reformulation the authors first approximate it by a family of problems with closed uncertainty sets. This mission formalizes the statement that this approximation is asymptotically exact.

Setting

The data are matrices $C\in\mathbb R^{Q\times N}$, $Q\in\mathbb R^{Q\times M}$, $T\in\mathbb R^{L\times N}$, $W\in\mathbb R^{L\times M}$, $H\in\mathbb R^{L\times Q}$, a nonempty bounded polyhedron $\Xi=\{\xi\in\mathbb R^Q: A\xi\le b\}$, a first-stage set $\mathcal X\subseteq\{0,1\}^N$ (the standing assumption of §3 of the paper) and a second-stage set $\mathcal Y\subseteq\{0,1\}^M$. A decision is $(x,\{y^k\}_{k\in\mathcal K})\in\mathcal X\times\mathcal Y^K$ with $\mathcal K=\{1,\dots,K\}$. Policy $y^k$ is feasible for $\xi$ if $Tx+Wy^k\le H\xi$. The K-adaptability problem $\mathcal P_K$ minimizes over decisions

$$\sup_{\xi\in\Xi}\Big[\xi^\top Cx+\inf_{k\in\mathcal K}\{\xi^\top Qy^k: Tx+Wy^k\le H\xi\}\Big],$$

which is $+\infty$ when some $\xi$ leaves no feasible policy.

Let $\mathcal L=\{0,\dots,L\}^K$. For $\ell\in\mathcal L$, the set $\Xi(\ell)$ collects the $\xi\in\Xi$ for which every policy with $\ell_k=0$ is feasible and every policy with $\ell_k\neq0$ violates constraint $\ell_k$ strictly: $[Tx+Wy^k]_{\ell_k}>[H\xi]_{\ell_k}$. Problem (6) minimizes

$$\varphi(x,\{y^k\})=\sup_{\ell\in\mathcal L}\ \sup_{\xi\in\Xi(\ell)}\Big[\xi^\top Cx+\min_{k\in\mathcal K:\,\ell_k=0}\xi^\top Qy^k\Big].$$

The sets $\Xi(\ell)$ are not closed. For $\varepsilon>0$ the closed inner approximations $\Xi_\varepsilon(\ell)$ replace the strict inequality by $[Tx+Wy^k]_{\ell_k}\ge[H\xi]_{\ell_k}+\varepsilon$, and problem $(6_\varepsilon)$ has objective $\varphi_\varepsilon$, defined like $\varphi$ with $\Xi_\varepsilon(\ell)$. The effective domains $\mathrm{dom}(6)$ and $\mathrm{dom}(6_\varepsilon)$ are the decisions at which $\varphi$, respectively $\varphi_\varepsilon$, is not $+\infty$.

Formalization targets

Goal: Proposition 2 (pp. 18–19)

(i) There is $\varepsilon_0>0$ such that

$$\mathrm{dom}(6_\varepsilon)=\mathrm{dom}(6)\qquad\text{for all }\varepsilon\in(0,\varepsilon_0].$$

(ii) For every $\kappa>0$ there is $\varepsilon_0>0$ such that for all $\varepsilon\in(0,\varepsilon_0]$ and every decision in $\mathrm{dom}(6)$, both objective values are finite and

$$|\varphi_\varepsilon(x,\{y^k\})-\varphi(x,\{y^k\})|\le\kappa .$$

Milestones

• Proposition 1 (p. 16): for every decision, the objective of $\mathcal P_K$ equals $\varphi$. This anchors (6), and hence the goal, to the K-adaptability problem.
• Proof of Lemma 1, first step (p. ec6): every $\xi\in\Xi(\ell)$ lies in $\Xi_\varepsilon(\ell)$ for all small $\varepsilon$.
• Lemma 1 (p. ec6): if $\Xi(\ell)\ne\emptyset$, then $d^{\mathrm H}(\Xi_\varepsilon(\ell),\Xi(\ell))\to0$ as $\varepsilon\downarrow0$, in Euclidean Hausdorff distance.
• Proof of Proposition 2, chain (a)–(d) (p. ec7): for a decision in $\mathrm{dom}(6)$ and $\varepsilon$ small,

$$|\varphi_\varepsilon-\varphi|\le\Big(\max_{\ell}\sup_{\xi\in\Xi(\ell)}\inf_{\xi'\in\Xi_\varepsilon(\ell)}\|\xi-\xi'\|\Big)\cdot\max_{k}\|Cx+Qy^k\| .$$

Significance

Proposition 2 is the justification for the computational part of §3 of the paper: Theorem 5 reformulates $(6_\varepsilon)$, not (6), as a mixed-integer bilinear program, and Proposition 2 says that solving that program for small $\varepsilon$ recovers the K-adaptability problem's feasible decisions exactly and its objective values to arbitrary accuracy, uniformly over all decisions. Without it the bilinear reformulation would approximate an unrelated problem. Together with Proposition 1 it connects the original K-adaptability problem $\mathcal P_K$ to a family of problems with closed, polyhedral uncertainty sets. The same exhaustion of a non-closed polyhedral set by closed inner approximations appears whenever strict inequalities are replaced by $\varepsilon$-margins.

The results are proved in the paper's e-companion. To our knowledge none of them has a machine-checked proof. The mission produces a Lean model of the K-adaptability problem with constraint uncertainty and its decision-dependent uncertainty sets, which other formalizations of the paper's Theorem 5 or of related K-adaptability work can reuse.

Difficulty

Pointwise, the claim is easy: each $\xi\in\Xi(\ell)$ belongs to $\Xi_\varepsilon(\ell)$ once $\varepsilon$ is below its own constraint slack. That slack can be arbitrarily close to $0$ on $\Xi(\ell)$, because $\Xi(\ell)$ is not closed, so no single $\varepsilon$ works for all $\xi$. Uniformity in $\xi$ needs a compactness argument on the bounded set $\Xi$. Uniformity over decisions needs finiteness of $\mathcal X\times\mathcal Y^K$, which is where $\mathcal X\subseteq\{0,1\}^N$ enters. With a continuous first stage the threshold in (i) could depend on $x$. A second difficulty is bookkeeping: $\varphi$ and $\varphi_\varepsilon$ are extended-real suprema of infima over index sets that may be empty, and the comparison in (ii) must first show that both values are finite.

Formalization scope

• Parameters $\xi$ live in EuclideanSpace ℝ (Fin nQ), so every norm and distance is Euclidean, as in the paper's use of Cauchy–Schwarz. Decisions are pairs (x, y) with y : Fin K → Fin M → ℝ. $\mathcal Y$ is a Finset of 0/1 vectors and $\mathcal X$ a set of 0/1 vectors.
• $\ell$ is a function Fin K → Fin (L+1). The paper's row $l\in\{1,\dots,L\}$ is i.succ for i : Fin L.
• All objective values are in EReal. The paper's max and min are read as sup and inf, an infimum over no admissible policy is $+\infty$, and a supremum over an empty set is $-\infty$. "Finite (do not evaluate to $+\infty$)" in the definition of the effective domains is read as $<+\infty$. Part (ii) asserts that both values are real numbers before comparing them, so the truncation EReal.toReal ⊤ = 0 plays no role.
• Lemma 1 uses the extended Hausdorff distance Metric.hausdorffEDist. The real-valued Metric.hausdorffDist is $0$ when one set is empty, so a statement with it would drop the nonemptiness of $\Xi_\varepsilon(\ell)$ that the lemma contains.
• Part (i) cannot be satisfied by the inclusion $\mathrm{dom}(6)\subseteq\mathrm{dom}(6_\varepsilon)$ alone, which is immediate from $\Xi_\varepsilon(\ell)\subseteq\Xi(\ell)$. The content is the reverse inclusion, with one threshold $\varepsilon_0$ for all decisions. Likewise (ii) has a single threshold for all decisions of the domain, not one per decision.
• A complete development needs: the cover $\bigcup_\ell\Xi(\ell)=\Xi$, finiteness of the decision set, compactness of the closure of $\Xi$, and elementary facts about EReal suprema. Proofs of the milestones, alternative arguments, and variants with $\mathcal X$ continuous under additional hypotheses are welcome.

Selected references

• G. A. Hanasusanto, D. Kuhn, W. Wiesemann, K-Adaptability in Two-Stage Robust Binary Programming, Operations Research 63(4):877–891, 2015. https://doi.org/10.1287/opre.2015.1392 (preprint read: Optimization Online 2014/03/4294, revision of 2015-03-30, https://optimization-online.org/wp-content/uploads/2014/03/4294.pdf)
• D. Bertsimas, C. Caramanis, Finite Adaptability in Multistage Linear Optimization, IEEE Transactions on Automatic Control 55(12):2751–2766, 2010. https://doi.org/10.1109/TAC.2010.2049764