All missions

Motivation

Algorithms for smooth constrained optimization stop when an approximate optimality test passes. The tests used in practice are sequential optimality conditions: properties of a sequence of iterates $x^k\to x^*$ rather than of the limit alone. Every local minimizer satisfies them, with or without a constraint qualification, which makes them natural stopping criteria. The price is that a point passing such a test need not satisfy the Karush–Kuhn–Tucker (KKT) conditions. A strict constraint qualification for a sequential condition $S$ is a property of the constraints at $x^*$ under which $S$ implies KKT for every objective function. The weaker this property, the more problems on which the stopping test is guaranteed to certify a KKT point.

The Approximate Gradient Projection (AGP) condition was introduced by Martínez and Svaiter (2003) and is the natural stopping criterion of inexact restoration methods. It is strictly stronger than the Approximate KKT condition (AKKT), and it does not require Lagrange multiplier estimates. Andreani, Martínez, Ramos and Silva (Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018, doi:10.1287/moor.2017.0879) determined the weakest strict constraint qualification associated with AGP and with several other sequential conditions. For AKKT the answer had been found earlier: the Cone Continuity Property of Andreani, Martínez, Ramos and Silva (2016). This mission formalizes the AGP case, Theorem 4.2 of the preprint, together with its linear-constraint variant, Theorem 4.6.

Setting

Consider the nonlinear program

$$\min f(x)\quad\text{subject to}\quad h(x)=0,\ g(x)\le0, \tag{1.1}$$

with $h=(h_1,\dots,h_m)$ and $g=(g_1,\dots,g_p)$ continuously differentiable on $\mathbb R^n$. The feasible set is $\Omega=\{x:h(x)=0,\ g(x)\le0\}$, and $J(x^*)=\{j:g_j(x^*)=0\}$ is the set of active inequalities. The KKT condition holds at $x^*$ for $f$ if there are $\lambda\in\mathbb R^m$ and $\mu\in\mathbb R^p_+$, with $\mu_j=0$ for $j\notin J(x^*)$, such that $\nabla f(x^*)+\sum_i\lambda_i\nabla h_i(x^*)+\sum_j\mu_j\nabla g_j(x^*)=0$.

The linearized cone is $L_\Omega(x^*)=\{d:\langle\nabla h_i(x^*),d\rangle=0\ \forall i,\ \langle\nabla g_j(x^*),d\rangle\le0\ \forall j\in J(x^*)\}$, and $K^\circ=\{v:\langle v,k\rangle\le0\ \forall k\in K\}$ is the polar of a set $K$. For a convex set $S$, the normal cone $N_S(y)=\{w:\langle w,z-y\rangle\le0\ \forall z\in S\}$ is defined for $y\in S$ and is empty for $y\notin S$. $P_S$ denotes the Euclidean projection onto a closed convex set $S$.

For $\gamma\in[-\infty,0]$ and a point $x$, the linearized set $\Omega(x,\gamma)$ of (4.2) consists of the $z$ with

• $\langle\nabla h_i(x),z-x\rangle=0$ for all $i$;
• $\langle\nabla g_j(x),z-x\rangle\le0$ if $g_j(x)\ge0$;
• $g_j(x)+\langle\nabla g_j(x),z-x\rangle\le0$ if $\gamma<g_j(x)<0$.

A feasible $x^*$ satisfies AGP($\gamma$) for $f$ if there is a sequence $x^k\to x^*$ with

$$P_{\Omega(x^k,\gamma)}\big(x^k-\nabla f(x^k)\big)-x^k\to0. \tag{4.1}$$

The outer limit $\limsup_{z\to z^*}F(z)$ of a set-valued map is the set of limits of sequences $w^k\in F(z^k)$ with $z^k\to z^*$ (1.6). The point $x^*$ is AGP-regular (Definition 4.1) if

$$\limsup_{(x,\varepsilon)\to(x^*,0)}N_{\Omega(x,-\infty)}(x+\varepsilon)\subset N_{\Omega(x^*,-\infty)}(x^*).$$

Formalization targets

Goal: Theorem 4.2

For continuously differentiable constraints and a feasible $x^*$,

$$x^*\ \text{AGP-regular}\iff\big(\forall f\in C^1:\ \mathrm{AGP}(-\infty)\text{ at }x^*\Rightarrow\text{KKT at }x^*\big).$$

The forward implication says AGP-regularity is a strict constraint qualification for AGP; the backward one says it is implied by every such qualification.

Milestones

1. Proposition 3.1: for nonempty closed convex $C$ and $x\in C$, $\omega\in N_C(x)\iff P_C(x+\omega)=x$.
2. Nonexpansiveness of $P_C$, used in (4.10).
3. (4.6): $N_{\Omega(x^*,-\infty)}(x^*)=L_\Omega(x^*)^\circ$ at a feasible $x^*$.
4. $-\nabla f(x^*)\in L_\Omega(x^*)^\circ\iff$ KKT at $x^*$.
5. (4.8): $N_{\Omega(x^k,\gamma)}(x^k+\varepsilon^k)\subset N_{\Omega(x^k,-\infty)}(x^k+\varepsilon^k)$ for $k$ large.
6. (4.7)–(4.9): under AGP-regularity, AGP($\gamma$) implies KKT for every $\gamma\in[-\infty,0)$.
7. (4.10)–(4.11): every $\omega^*$ in the outer limit makes AGP($-\infty$) hold for $f(x)=-\langle\omega^*,x\rangle$.

Companion: Theorem 4.6

The same characterization for the Linear AGP condition (LAGP), in which the linear constraints are kept exact and the iterates stay in the set $\Omega_L$ they define. LAGP-regularity (Definition 4.4) is outer semicontinuity of $(x,\varepsilon)\mapsto N_{\Omega_{NL}(x,-\infty)\cap\Omega_L}(x+\varepsilon)$ relative to $x\in\Omega_L$. Two further items accompany it: Proposition 4.1, the explicit form of $N_{\Omega(x,-\infty)}(x+\varepsilon)$, and the equality $N_{\Omega_{NL}(x^*,-\infty)\cap\Omega_L}(x^*)=L_\Omega(x^*)^\circ$ appended to Definition 4.4.

Significance

Theorem 4.2 gives the exact boundary of the problems on which an AGP-based stopping test certifies KKT points. Any constraint qualification already known to make AGP imply KKT, for instance the Cone Continuity Property, implies AGP-regularity. Conversely, at a point that is not AGP-regular some objective function has an AGP sequence converging to a non-KKT point. In Section 5 of the paper the theorem places AGP-regularity in the hierarchy of constraint qualifications, with the regularity notions for CAKKT and SAKKT next to it.

The paper's result is proved, and no part of it is formalized on the platform. The mission adds machine-checked statements of the characterization and of the convex-analysis facts it rests on: the projection characterization of normal cones, nonexpansiveness, and the polyhedral normal cone of $\Omega(x^*,-\infty)$ as the polar of the linearized cone. These facts are reusable for any sequential optimality condition built on projections.

Difficulty

The forward direction passes to the limit in normal cones of sets $\Omega(x^k,\gamma)$ that vary with $k$ and are evaluated at perturbed points $x^k+\varepsilon^k$, which may lie outside $\Omega(x^k,-\infty)$. For finite $\gamma$ the inclusion of $N_{\Omega(x^k,\gamma)}$ in $N_{\Omega(x^k,-\infty)}$ fails at such points. It holds only for $k$ large, through a continuity argument on the inactive constraints. The backward direction must manufacture an objective function and an AGP sequence from an arbitrary element of an outer limit, which requires existence of projections onto every $\Omega(x^k,-\infty)$. The identification of $N_{\Omega(x^*,-\infty)}(x^*)$ with $L_\Omega(x^*)^\circ$ needs the localization of a polyhedral normal cone, and the link between $L_\Omega(x^*)^\circ$ and KKT multipliers is Farkas' lemma for a finitely generated cone.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); indices are Fin m and Fin p; gradients are Mathlib's gradient.
• The standing hypothesis is that every $h_i$ and $g_j$ is $C^1$. Objectives in the characterizations are $C^1$ and are quantified inside the equivalence, for fixed constraints and fixed feasible $x^*$.
• KKT is the multiplier form with sign and complementarity. The paper's reading $-\nabla f(x^*)\in L_\Omega(x^*)^\circ$ is a milestone.
• $\gamma$ is an extended real and $-\infty$ is its bottom element. The goal states AGP as AGP($-\infty$). The paper's AGP is the $\gamma$-independent condition of Martínez–Svaiter, which this paper does not prove; milestone 6 gives the forward direction for every $\gamma<0$.
• The normal cone is empty outside the set. A normal cone that is nonempty at infeasible points makes AGP-regularity a different, stronger condition. The projection is a predicate (a nearest point), not a choice function.
• The outer limit is sequential, as in (1.6).
• The paper says the inclusion (4.8) "always holds"; it is stated for $k$ large, which is what the proof uses. Definition 4.4's "$\Omega_L\times\mathbb R^m$" is read as $\Omega_L\times\mathbb R^n$.
• A formalization with junk gradients (no $C^1$ hypothesis where the proof needs continuity), an objective quantified outside the equivalence, or KKT without sign or complementarity is ruled out by the statements above.

All objects are defined in the namespace StrictCQ.AGP. Proofs of the convex-analysis milestones are reusable beyond this mission.

Selected references

• R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, Strict constraint qualifications and sequential optimality conditions for constrained optimization, Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018. https://doi.org/10.1287/moor.2017.0879
• J. M. Martínez, B. F. Svaiter, A practical optimality condition without constraint qualifications for nonlinear programming, J. Optim. Theory Appl. 118:117–133, 2003. https://doi.org/10.1023/A:1023617925436
• R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, A cone-continuity constraint qualification and algorithmic consequences, SIAM J. Optim. 26(1):96–110, 2016. https://doi.org/10.1137/15M1008488
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Motivation

The shortest-path problem in a graph of convex sets (SPP in GCS), introduced by Marcucci, Umenberger, Parrilo and Tedrake (arXiv:2101.11565, SIAM J. Optim. 2024), asks for a path through a directed graph whose vertices carry convex sets, together with a point in each visited set, minimizing a sum of convex edge lengths. It models motion planning around obstacles, hybrid-system control and other problems that mix a discrete choice with continuous positions. The paper formulates it as a mixed-integer convex program whose only nonconvexity, before relaxation, is a family of bilinear equalities $Z = xy^\top$ that couple the continuous positions $x$ with the flow variables $y$.

Section 7 of the paper studies the convex relaxation used for these bilinear equalities in isolation. Products of valid inequalities linearized by $Z = xy^\top$ are the idea behind the McCormick envelope (McCormick 1976) and the Reformulation-Linearization Technique of Sherali and Adams. This mission formalizes the paper's result that the relaxation is exact at every extreme point of the polytope $\mathcal Y$, which is the property that makes the mixed-integer formulation exact at binary flows.

Setting

Fix $\mathcal X \subseteq \mathbb R^n$ and $\mathcal Y \subseteq \mathbb R^m$. Points of $\mathbb R^n\times\mathbb R^m\times\mathbb R^{n\times m}$ are written $(x, y, Z)$.

• The perspective of $\mathcal X$ (Definition 4.1) is $\tilde{\mathcal X} := \operatorname{cl}\{(x, \lambda) : \lambda \ge 0,\ x \in \lambda\mathcal X\} \subseteq \mathbb R^n \times \mathbb R$.
• The cone of valid inequalities (Definition 4.8) is $\mathcal X^\circ := \{(a, b) : a^\top x + b \ge 0 \text{ for all } x \in \mathcal X\}$.
• The dual cone of $\mathcal K \subseteq \mathbb R^n\times\mathbb R$ is $\mathcal K^* := \{(a, b) : a^\top x + b\lambda \ge 0 \text{ for all } (x, \lambda) \in \mathcal K\}$.
• The bilinear set (7.1) is $\mathcal S := \{(x, y, Z) : x \in \mathcal X,\ y \in \mathcal Y,\ Z = xy^\top\}$.
• The set-based relaxation (7.2) multiplies every valid inequality of $\mathcal X$ by every valid inequality of $\mathcal Y$ and replaces $xy^\top$ by $Z$:

$$\mathcal S' := \{(x, y, Z) : a^\top Zc + d\,a^\top x + b\,c^\top y + bd \ge 0 \text{ for all } (a, b) \in \mathcal X^\circ,\ (c, d) \in \mathcal Y^\circ\}.$$

• A polytope is a bounded set $\mathcal Y = \{y : c_i^\top y + d_i \ge 0 \text{ for all } i \in \mathcal I\}$ with $\mathcal I$ finite. Its asymmetric relaxation (7.3) is $\{(x, y, Z) : (Zc_i + d_i x,\ c_i^\top y + d_i) \in \tilde{\mathcal X} \text{ for all } i \in \mathcal I\}$.

Always $\mathcal S \subseteq \mathcal S'$, and $\mathcal S'$ is convex.

Formalization targets

Goal: Lemma 7.4 (p. 13)

Let $\mathcal X$ be compact and convex, let $\mathcal Y$ be a polytope and let $\hat y$ be an extreme point of $\mathcal Y$. Then for all $x$ and $Z$,

$$(x, \hat y, Z) \in \mathcal S \iff (x, \hat y, Z) \in \mathcal S'.$$

Milestones

1. (7.2), p. 12: $\mathcal S \subseteq \mathcal S'$ for arbitrary sets.
2. The sentence after (7.2), p. 12: for closed convex $\mathcal X, \mathcal Y$, every point of $\mathcal S'$ has $x \in \mathcal X$ and $y \in \mathcal Y$.
3. Lemma 4.9, p. 6: for nonempty closed convex $\mathcal X$, $(\tilde{\mathcal X})^* = \mathcal X^\circ$ and $(\mathcal X^\circ)^* = \tilde{\mathcal X}$.
4. Proposition 7.1, inclusion $\subseteq$, p. 12: $\mathcal S'$ is contained in the asymmetric relaxation (7.3), for every family of halfspaces.
5. Remark 4.2, p. 5: for compact convex $\mathcal X$, $\tilde{\mathcal X} = \{(x, \lambda) : \lambda \ge 0,\ x \in \lambda\mathcal X\}$, without closure.
6. Proof of Lemma 7.4, p. 13: at an extreme point of a polyhedron with finitely many inequalities, $m$ linearly independent inequalities are active.
7. Proposition 7.1, p. 12: $\mathcal S'$ equals (7.3), when the trivial inequality $1 \ge 0$ is a nonnegative combination of the defining inequalities.
8. Remark 7.5, p. 14: if $\mathcal Y \subseteq [0,1]^m$, every point of $\mathcal Y \cap \{0,1\}^m$ is an extreme point of $\mathcal Y$.
9. (7.4), p. 13: for compact convex $\mathcal X$ and $\mathcal Y = \operatorname{conv}\{\hat y_j\}_{j\in\mathcal J}$, $\operatorname{conv}\mathcal S = \{\sum_j (x_j, \lambda_j\hat y_j, x_j\hat y_j^\top) : \sum_j \lambda_j = 1,\ (x_j, \lambda_j) \in \tilde{\mathcal X}\}$.

Significance

The result. In the paper's mixed-integer program each vertex $v$ contributes a bilinear set $\mathcal S_v$ in which $\mathcal X$ is the convex set at $v$ and $\mathcal Y$ is the polytope of flows on the edges at $v$. Binary flows corresponding to a path are extreme points of these polytopes, so Lemma 7.4 says that replacing $\mathcal S_v$ by $\mathcal S'_v$ loses nothing at the integer points of the program. This gives the paper's second, geometric proof that its mixed-integer convex formulation is exact (Theorem 5.7). By Remark 7.5 the lemma also extends a known property of the first-level Reformulation-Linearization Technique for bilinear programs with binary variables from polytopes $\mathcal X$ to compact convex sets $\mathcal X$. Proposition 7.1 is what makes the relaxation finite: it replaces the infinitely many inequalities of $\mathcal S'$ by one perspective-cone constraint per facet of $\mathcal Y$.

Formalizing it. The results are proved on paper; none of them has a machine-checked proof. The formalization also settles the exact hypotheses. Three statements of this section are false as printed (see Formalization scope), and the corrected versions are posed here with the counterexamples recorded. The perspective cone, the cone of valid inequalities and their duality (Lemma 4.9) are general convex-analysis facts that recur across conic and disjunctive programming.

Difficulty

The direction $\mathcal S \subseteq \mathcal S'$ is one line, since $(a^\top x + b)(c^\top y + d) \ge 0$. The converse at $\hat y$ needs three ingredients that are each standard and none of which is in Mathlib in this form.

• The duality between $\tilde{\mathcal X}$ and $\mathcal X^\circ$ is a bipolar theorem for the closed cone generated by $\mathcal X \times \{1\}$, in the product $\mathbb R^n \times \mathbb R$ with the pairing $a^\top x + b\lambda$. The cone needs care at $\lambda = 0$.
• The active-constraint characterization of extreme points of a polyhedron in halfspace form has to be proved directly.
• The step "$(u, 0) \in \tilde{\mathcal X}$ implies $u = 0$" is where boundedness enters. For unbounded $\mathcal X$ the slice $\lambda = 0$ of $\tilde{\mathcal X}$ is the recession cone, and the argument, and the lemma, fail.

Proposition 7.1 as an equality needs an affine Farkas lemma, and its printed proof skips the case of the valid inequality $(0, 1)$.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ, inner products are dotProduct, $Zc$ is Z *ᵥ c and $xy^\top$ is Matrix.vecMulVec x y. Triples are (x, y, Z) in (Fin n → ℝ) × (Fin m → ℝ) × Matrix (Fin n) (Fin m) ℝ. A polytope is given by a finite family (c i, d i) over a Fintype index and the hypothesis Bornology.IsBounded; extreme points are Mathlib's Set.extremePoints ℝ, never a predicate defined through active constraints. The dual cone uses the pairing $a^\top x + b\lambda$ on the product, not an inner product.

Hypotheses added relative to the page, each with a counterexample to the printed form:

• Lemma 7.4 and (7.4): $\mathcal X$ compact. Section 7.1 only asks $\mathcal X$ to be closed and convex. For $\mathcal X = [0, \infty)$, $\mathcal Y = [0, 1]$ and $\hat y = 0$, the point $(1, 0, \tfrac12)$ is in $\mathcal S'$ but not in $\mathcal S$. Compactness is the standing assumption of Section 2 on the sets $\mathcal X_v$ that $\mathcal X$ stands for.
• Lemma 4.9: $\mathcal X$ nonempty. For $\mathcal X = \emptyset$, $\tilde{\mathcal X} = \emptyset$ but $(\mathcal X^\circ)^* = \{0\}$.
• Proposition 7.1 (equality): $1 \ge 0$ is a nonnegative combination of the rows. For $\mathcal Y = \{0\}$ written as $\{y \ge 0, -y \ge 0\}$ and $\mathcal X = [0, 1]$, the point $(5, 0, 0)$ satisfies (7.3) but not (7.2). The hypothesis holds for every polytope with an interior point and for the flow polytopes of the paper.

Several hypotheses are dropped where they are not needed, which strengthens the statements: nonemptiness of $\mathcal X$ throughout, and boundedness and finiteness in the inclusion of Proposition 7.1 and in the active-constraint milestone.

Trivializing formalizations ruled out: $\mathcal S'$ quantifies over all of $\mathcal X^\circ \times \mathcal Y^\circ$ and is not replaced by (7.3) in the goal; $\mathcal X$ is never allowed to be merely closed in the goal; the hypotheses of the goal are satisfiable ($\mathcal X = \mathcal Y = [0,1]$, $\hat y = 0$ is checked in Lean).

A complete development needs the bipolar theorem for closed convex cones in $\mathbb R^{n}\times\mathbb R$, the closedness of the cone over a compact convex set, the active-constraint characterization of extreme points, and a finite affine Farkas lemma. All of these are reusable well beyond this mission and are welcome as separate contributions.

Selected references

• T. Marcucci, J. Umenberger, P. A. Parrilo, R. Tedrake, Shortest Paths in Graphs of Convex Sets, SIAM J. Optim. 34(1), 2024. arXiv:2101.11565v5 (the version cited). https://arxiv.org/abs/2101.11565 , https://doi.org/10.1137/22M1523790
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Corollary 11.7.2, Theorem 14.1). https://doi.org/10.1515/9781400873173
• G. P. McCormick, Computability of global solutions to factorable nonconvex programs: Part I — Convex underestimating problems, Math. Program. 10, 1976. https://doi.org/10.1007/BF01580665
• H. D. Sherali, W. P. Adams, A Reformulation-Linearization Technique for Solving Discrete and Continuous Nonconvex Problems, Kluwer, 1999. https://doi.org/10.1007/978-1-4757-4388-3

Motivation

Practical algorithms for nonlinear programming do not stop at an exact Karush–Kuhn–Tucker (KKT) point; they stop when an approximate stationarity test passes. Sequential optimality conditions formalize what such tests certify: they are properties of a feasible point $x^*$ phrased through sequences $x^k \to x^*$ and multiplier estimates, and every local minimizer satisfies them without any constraint qualification. The question that links them back to classical theory is which conditions on the constraints guarantee that a point satisfying a sequential condition is in fact a KKT point. Andreani, Martínez, Ramos and Silva call these strict constraint qualifications and ask, for each sequential condition, for the weakest one.

For the Approximate KKT condition (AKKT) the answer, the Cone Continuity Property, was given by Andreani, Martínez, Ramos and Silva in 2016 (SIAM J. Optim. 26(1)). Section 2 of the present paper treats the Scaled-AKKT condition, which divides the stationarity residual by the size of the multipliers. This scaling appears in the stopping criteria of practical codes and in complexity analyses of nonlinear programming methods. Scaled-AKKT is weaker than AKKT, and the paper uses it as the first, self-contained example of the analysis it then carries out for AGP, CAKKT and SAKKT.

Setting

Fix $n, m, p \ge 0$ and continuously differentiable functions $h_1,\dots,h_m$, $g_1,\dots,g_p : \mathbb R^n \to \mathbb R$, where $\mathbb R^n$ carries the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. The feasible set is $\Omega = \{x : h_i(x) = 0,\ g_j(x) \le 0 \text{ for all } i, j\}$, and $x^* \in \Omega$ is fixed. An index $j$ is active when $g_j(x^*) = 0$.

For an objective $f$, the point $x^*$ satisfies KKT if there are $\lambda \in \mathbb R^m$ and $\mu \in \mathbb R^p$ with $\mu \ge 0$, $\mu_j = 0$ for inactive $j$, and $\nabla f(x^*) + \sum_i \lambda_i \nabla h_i(x^*) + \sum_j \mu_j \nabla g_j(x^*) = 0$.

Scaled-AKKT holds at $x^*$ for $f$ if there are sequences $x^k \to x^*$, $\lambda^k \in \mathbb R^m$ and $\mu^k \in \mathbb R^p$ with $\mu^k \ge 0$, such that $\min\{\mu^k_j, -g_j(x^k)\} \to 0$ for every $j$, and

$$\lim_{k\to\infty} \max\{1, \|\lambda^k\|_\infty, \|\mu^k\|_\infty\}^{-1}\, \Big\|\nabla f(x^k) + \sum_{i=1}^m \lambda^k_i \nabla h_i(x^k) + \sum_{j=1}^p \mu^k_j \nabla g_j(x^k)\Big\| = 0,$$

where $\|\cdot\|_\infty$ is the supremum norm of a multiplier vector.

The Mangasarian–Fromovitz constraint qualification (MFCQ) holds at $x^*$ if $\nabla h_1(x^*),\dots,\nabla h_m(x^*)$ are linearly independent and some $d$ satisfies $\langle \nabla h_i(x^*), d\rangle = 0$ for all $i$ and $\langle \nabla g_j(x^*), d\rangle < 0$ for all active $j$. The cone of active gradients is

$$K(x^*) = \Big\{\sum_{i=1}^m \lambda_i \nabla h_i(x^*) + \sum_{j:\,g_j(x^*)=0} \mu_j \nabla g_j(x^*) : \lambda \in \mathbb R^m,\ \mu_j \ge 0\Big\}.$$

Formalization targets

Goal: the weakest strict constraint qualification for Scaled-AKKT

For a $C^1$ constraint system and a feasible $x^*$,

$$\big(\text{MFCQ at } x^* \ \text{ or } \ K(x^*) = \mathbb R^n\big) \iff \forall f \in C^1:\ \big(\text{Scaled-AKKT at } x^* \text{ for } f\big) \Rightarrow \big(\text{KKT at } x^* \text{ for } f\big). \qquad (2.3)$$

The forward implication says that (2.3) is a strict constraint qualification for Scaled-AKKT; the backward implication says that every strict constraint qualification for Scaled-AKKT implies (2.3).

Milestones

1. If $K(x^*) = \mathbb R^n$, then $x^*$ is a KKT point for every objective (p. 3).
2. Scaled-AKKT with a bounded multiplier set $\{\lambda^k, \mu^k\}$ implies KKT (p. 3).
3. Scaled-AKKT with an unbounded multiplier set yields $\lambda$, $\mu \ge 0$ supported on the active set, with $\max\{\|\lambda\|_\infty, \|\mu\|_\infty\} = 1$, solving $\sum_i \lambda_i \nabla h_i(x^*) + \sum_{j \text{ active}} \mu_j \nabla g_j(x^*) = 0$, display (2.4) (pp. 3–4).
4. Such a normalized solution of (2.4) excludes MFCQ (p. 4).
5. Conversely, failure of MFCQ yields a normalized solution of (2.4) (p. 4).
6. Given a normalized solution of (2.4), Scaled-AKKT holds at $x^*$ for every linear objective $f(x) = \langle x, c\rangle$ (p. 4).

Significance

The result separates Scaled-AKKT sharply from AKKT. For AKKT the weakest strict constraint qualification (the Cone Continuity Property) is implied by many classical conditions, including CPLD and RCPLD. For Scaled-AKKT it is essentially MFCQ, a much stronger requirement. A stopping test of the Scaled-AKKT type therefore certifies a KKT point only under MFCQ, apart from the degenerate case of a full active cone. The other sections of the paper characterize the weakest strict constraint qualifications for AGP, CAKKT and SAKKT, using the same "iff over all objectives" template that this mission formalizes in its simplest form.

The paper's argument is a half-page sketch. A formalization makes explicit several points it leaves implicit: the role of the $1$ in the scaling factor, the vanishing of inactive multipliers forced by the complementarity limit, and the theorem of the alternative that converts failure of MFCQ into a nonzero solution of (2.4). None of these results is formalized on Prove2Me or, to our knowledge, in Mathlib.

Difficulty

The forward direction splits on whether the multipliers stay bounded, and the unbounded case requires normalizing by $\max\{1, \|\lambda^k\|_\infty, \|\mu^k\|_\infty\}$ and extracting a convergent subsequence. Along that subsequence one must check that the normalized multipliers have supremum norm exactly one, that the normalized objective gradient tends to zero, and that inactive multipliers tend to zero; only then does the limit contradict MFCQ. The backward direction needs a theorem of the alternative (Motzkin or Gordan type) for the active gradients, together with linear dependence of the equality gradients. The paper uses it without stating it. It also needs a vector $c$ with $-c \notin K(x^*)$. The printed text chooses $c \notin K(x^*)$, which has the wrong sign for the objective $\langle x, c\rangle$; milestone 6 is stated for every $c$, so the sign issue does not propagate.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); the constraints are index families Fin m → E → ℝ and Fin p → E → ℝ; gradients are Mathlib's gradient. Multiplier vectors live in Fin m → ℝ and Fin p → ℝ, whose Mathlib norm is the supremum norm, while residuals use the Euclidean norm. Standing hypotheses: every $h_i$, $g_j$ is $C^1$ (the paper's "continuous first-order derivatives"), every objective in the goal is $C^1$, and $x^*$ is feasible. The objective is quantified inside the equivalence, so the left side of the goal depends on $h$, $g$, $x^*$ alone. "or" is inclusive. The cone condition is equality of the cone with all of $\mathbb R^n$, not with its linear span. KKT carries both the sign condition $\mu \ge 0$ and complementarity. MFCQ is defined in its primal (direction) form; defining it as "no nonzero nonnegative null combination" would make milestones 4 and 5 hold by definition, and that reading is excluded. Milestone 2 omits the MFCQ hypothesis present in the paper's sentence because the bounded case does not use it.

A complete development needs subsequence extraction in finite-dimensional spaces, continuity of gradients of $C^1$ functions, and a theorem of the alternative for finitely many vectors. The last two are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

• R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, Strict constraint qualifications and sequential optimality conditions for constrained optimization, Optimization Online 5197 (2015); Mathematics of Operations Research 43(3), 2018. https://doi.org/10.1287/moor.2017.0879
• R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, A cone-continuity constraint qualification and algorithmic consequences, SIAM Journal on Optimization 26(1), 2016. https://doi.org/10.1137/15M1008488
• O. L. Mangasarian, S. Fromovitz, The Fritz John necessary optimality conditions in the presence of equality and inequality constraints, Journal of Mathematical Analysis and Applications 17, 1967. https://doi.org/10.1016/0022-247X(67)90163-1
• R. Andreani, G. Haeser, J. M. Martínez, On sequential optimality conditions for smooth constrained optimization, Optimization 60(5), 2011. https://doi.org/10.1080/02331930903578700

Motivation

Multistage stochastic linear programs model decisions taken over time under uncertainty: reservoir releases in hydro-thermal scheduling, production and inventory plans, capacity expansion. Their standard solution method, stochastic dual dynamic programming (SDDP, Pereira and Pinto 1991), approximates each stage's cost-to-go function from below by cutting planes. This gives a lower bound on the optimal value and a candidate policy, but no guaranteed upper bound: in the risk-neutral case the policy's expected cost is estimated by Monte Carlo simulation.

Planners who are averse to risk replace the expectation in each stage by a coherent risk measure (Artzner, Delbaen, Eber and Heath 1999), nested stage by stage so that the resulting dynamic risk measure is time consistent (Ruszczyński and Shapiro 2006). Under such a nested objective, simulation no longer estimates the cost of a policy: the nested risk of a policy is not an average over sampled scenarios. Philpott, de Matos and Finardi (2013) address this by an inner approximation of the cost-to-go functions from above, built from convex combinations of finitely many points with known upper bounds. Their Proposition 5 shows that the optimal value $y$ of the resulting first-stage problem bounds the nested risk-adjusted cost of the policy defined by the inner approximation. This gives a deterministic upper bound that complements the SDDP lower bound, and they apply it to the Brazilian hydro-thermal system.

Setting

There are $T\ge2$ stages. The decision at stage $t$ is $x_t\in\mathbb R^n$; $A_t,E_t$ are $m\times n$ matrices and $c_t\in\mathbb R^n$. Stage 1 is deterministic: $A_1x_1=b_1$. For $t\ge2$ a random outcome $\omega_t$ ranges over a finite set $\Omega_t$, independently of earlier stages, and enters through the right-hand side $b_t(\omega_t)$. The feasible set of stage $t$ given the previous decision $x_{t-1}$ is

$$\mathcal X_t(\omega_t)=\{x_t\ge0:\ A_tx_t=b_t(\omega_t)-E_tx_{t-1}\}.$$

A coherent risk measure $\rho$ maps random costs $Z:\Omega\to\mathbb R$ to $\mathbb R$ and is subadditive, monotone ($Z_1\le Z_2\Rightarrow\rho(Z_1)\le\rho(Z_2)$), positively homogeneous and translation equivariant ($\rho(\lambda+Z)=\lambda+\rho(Z)$). Larger is worse: these are costs. Each stage $t\ge2$ carries a one-step coherent risk measure $\rho_t$ on random costs over $\Omega_t$. It is extended to costs in $\mathbb R\cup\{+\infty\}$ by $\bar\rho_t(Z)=+\infty$ whenever some outcome has infinite cost.

For $s=2,\dots,T$ fix points $x^1_{s-1},\dots,x^{J_{s-1}}_{s-1}$ and numbers $q^1_s,\dots,q^{J_{s-1}}_s$. The inner approximation is the lower boundary of the convex hull of the pairs $(x^j_{s-1},q^j_s)$:

$$\hat{\mathcal Q}_s(x)=\min\Big\{\sum_j\lambda^jq^j_s:\ \sum_j\lambda^jx^j_{s-1}=x,\ \lambda\ge0,\ \sum_j\lambda^j=1\Big\},$$

which is $+\infty$ off the convex hull of the points, with $\hat{\mathcal Q}_{T+1}\equiv0$. The policy's stage problem (13) and the first-stage problem (8) are

$$q_t(x_{t-1},\omega_t)=\min_{x_t\in\mathcal X_t(\omega_t)}c_t^\top x_t+\hat{\mathcal Q}_{t+1}(x_t),\qquad y=\min_{A_1x_1=b_1}c_1^\top x_1+\hat{\mathcal Q}_2(x_1).$$

The numbers $q^j_s$ are upper bounds when $q^j_s\ge\bar\rho_s\big(q_s(x^j_{s-1},\omega_s)\big)$ for all $s$ and $j$. A policy defined by the inner approximation, $\hat\pi$, takes at each state $x_{t-1}$ and outcome $\omega_t$ an action $\hat x_t(x_{t-1},\omega_t)$ solving (13), and a first-stage action $\hat x_1$ solving (8). The actual risk-adjusted cost of $\hat\pi$ over stages $t,\dots,T$ is

$$\hat v_t(x_{t-1},\omega_t)=c_t^\top\hat x_t+\bar\rho_{t+1}\big(\hat v_{t+1}(\hat x_t,\omega_{t+1})\big),$$

with no future term at $t=T$. The nested risk-adjusted cost of the policy is $v(\hat\pi)=c_1^\top\hat x_1+\bar\rho_2(\hat v_2(\hat x_1,\omega_2))$.

Formalization targets

Goal: Proposition 5

$$v(\hat\pi)\ \le\ y.$$

The bound holds for every $T\ge2$, every family of coherent $\rho_t$, every choice of points satisfying the upper-bound property, and every minimizing selection $\hat\pi$.

Milestones

1. The convexity display of §2: subadditivity and positive homogeneity imply $\rho(\alpha Z_1+(1-\alpha)Z_2)\le\alpha\rho(Z_1)+(1-\alpha)\rho(Z_2)$.
2. $\hat{\mathcal Q}_s$ is the lower boundary of the convex hull $\mathcal H$ of the pairs $(x^j_{s-1},q^j_s)$ (its epigraph is $\mathcal H$ plus the vertical half-line), hence convex with $\hat{\mathcal Q}_s(x^j_{s-1})\le q^j_s$, and every convex function bounded by the $q^j_s$ at the points lies below $\hat{\mathcal Q}_s$.
3. $q_t(\cdot,\omega_t)$ is convex in $x_{t-1}$.
4. The interpolation bound $\bar\rho_t\big(q_t(x_{t-1},\omega_t)\big)\le\hat{\mathcal Q}_t(x_{t-1})$.
5. The induction claim $\bar\rho_t\big(\hat v_t(x_{t-1},\omega_t)\big)\le\hat{\mathcal Q}_t(x_{t-1})$ for $t=2,\dots,T$ and every $x_{t-1}$.

Companions

Proposition 3, the risk-neutral case $\rho_t=\mathbb E$. Proposition 4, the subgradient rule $\sum_mp_m\tilde\zeta_mg(\tilde x,\omega_m)\in\partial_x\rho(Z(x,\omega))$ for $\rho$ given by its dual representation. The existence of a policy $\hat\pi$, which shows that the hypotheses of the goal can be met.

Significance

Proposition 5 makes the inner approximation a certificate. Any policy computed by minimizing against $\hat{\mathcal Q}_{t+1}$ has nested risk-adjusted cost at most $y$, a number obtained by solving one linear program. Together with the lower bound $z$ from outer approximation it brackets the risk-adjusted optimal value. The gap $y-z$ then measures the quality of a risk-averse SDDP policy without simulation, which the nested objective does not allow. The bound covers every coherent nesting used in practice, such as mixtures of expectation and CVaR.

The results are proved in the paper. None of them is machine-checked. A formalization adds a precise account of the infinite values the paper does not discuss: infeasible stages, points outside the convex hull, and the extension of $\rho_t$ to $+\infty$. It also pins down the exact form of the upper-bound hypothesis the induction needs.

Difficulty

The obvious reading of the hypothesis on p. 16, "$q^j_{t+1}$ is an upper bound on $\rho_{t+1}(Q_{t+1}(x^j_t,\omega_{t+1}))$" with the true value function $Q_{t+1}$, does not support the induction. The policy $\hat\pi$ does not act optimally, so its cost can exceed the true value, and the inductive step compares $\hat v_t$ with the policy's own stage value $q_t$, not with $Q_t$. The hypothesis that works bounds the risk-adjusted optimal value of the policy's stage problem (13) at the points, which is what the paper's Upper Bound Computation actually computes.

The second difficulty is infinite values, which the paper never discusses. A risk measure is defined on real random costs, yet stage problems can be infeasible, $\hat{\mathcal Q}_s$ is $+\infty$ off a convex hull, and a convex combination may put zero weight on a point whose bound is $+\infty$. Every inequality of the paper has to be re-read in $\mathbb R\cup\{+\infty\}$, and the extended-real arithmetic must not silently produce a value the paper does not intend.

Formalization scope

Vectors are Fin n → ℝ, all stages share $n$ and $m$, and costs that may be infinite are EReal. Minima are EReal infima, $+\infty$ on an empty set. Attainment of a minimum is never built into a definition: the policy is a selection with a minimizing property, required at every state where the stage problem is feasible. Stages are natural numbers. Points and bounds are indexed by the stage $s$ of the function $\hat{\mathcal Q}_s$ they define, so pts s j is $x^j_{s-1}$ and qv s j is $q^j_s$. Stagewise independence is built in: $\omega_t$ ranges over $\Omega_t$ whatever happened before.

Standing assumptions made explicit in the statements:

• $T\ge2$;
• $\rho_t$ coherent for $t=2,\dots,T$ (all four axioms, though the proof uses only monotonicity and convexity);
• the terminal convention $\rho_{T+1}(Q_{T+1})=0$, so $\hat{\mathcal Q}_{T+1}\equiv0$;
• (8) without the constraint $x_1\ge0$, as printed;
• the upper-bound hypothesis in the form above.

The risk measures $\rho_t$ act on real random costs and are extended by $\bar\rho_t(Z)=+\infty$ when some outcome has infinite cost. In Proposition 4, $\rho$ is given by its dual representation (10); the representation theorem itself is not part of the mission. The existence statement adds solvability of $A_1x_1=b_1$ and boundedness below of the last-stage program, without which (8) or the last stage has no solution.

The goal is not to be trivialized. Its hypotheses mention neither $\hat v_t$ nor the induction claim; the policy must minimize at every feasible state, not only along visited states; and the statement is for general $T$ and general coherent $\rho_t$, not the expectation. The bound is trivially true when $y=+\infty$ and is informative when $\hat x_1$ lies in the convex hull of the stage-1 points.

A complete development needs:

• convexity of extended-real linear-programming value functions in their right-hand side;
• convexity of the convex-hull function $\hat{\mathcal Q}$;
• finite Jensen-type inequalities for monotone convex risk measures;
• linear-programming attainment, for the existence companion.

The first two are reusable for any SDDP-type development. Proofs of the milestones in any order are welcome.

Selected references

• A. B. Philpott, V. L. de Matos, E. Finardi, On Solving Multistage Stochastic Programs with Coherent Risk Measures, Operations Research 61(4), 2013. https://doi.org/10.1287/opre.2013.1175
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent Measures of Risk, Mathematical Finance 9(3), 1999. https://doi.org/10.1111/1467-9965.00068
• A. Ruszczyński, A. Shapiro, Conditional Risk Mappings, Mathematics of Operations Research 31(3), 2006. https://doi.org/10.1287/moor.1060.0204
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52, 1991. https://doi.org/10.1007/BF01582895
• A. Shapiro, Analysis of stochastic dual dynamic programming method, European Journal of Operational Research 209(1), 2011. https://doi.org/10.1016/j.ejor.2010.08.007

Motivation

Multistage stochastic programs model sequential decisions under uncertainty: hydro-thermal scheduling, inventory and capacity planning, portfolio management. The dominant solution methods, Stochastic Dual Dynamic Programming (SDDP, Pereira and Pinto 1991) and its relatives CUPPS and DOASA, never compute the Bellman (future-cost) functions of the problem. Instead they build outer approximations of them by cutting planes: affine minorants obtained from the optimal values and Lagrange multipliers of one-stage subproblems. Practitioners run these methods on very large problems, so the question of whether, and in what sense, the approximations converge is of direct practical relevance.

Earlier convergence proofs (Philpott and Guan 2008; Shapiro 2011) rely on linear stage problems, where only finitely many distinct cuts can be generated and convergence is finite. Girardeau, Leclère and Philpott (Math. Oper. Res. 2015) prove convergence for convex stage problems, where infinitely many distinct cuts may appear and finite termination is lost. This mission covers the first half of that paper: the deterministic multistage problem (§2), whose proof contains the whole scheme of the argument. The stochastic scenario-tree version is the companion mission of this series.

Setting

Fix a horizon $T\ge1$. States lie in $\mathbb R^d$ and controls in $\mathbb R^p$; values are in $\overline{\mathbb R}=\mathbb R\cup\{\pm\infty\}$. The data are state sets $\mathcal X_t\subseteq\mathbb R^d$, control multifunctions $\mathcal U_t:\mathbb R^d\rightrightarrows\mathbb R^p$, stage costs $C_t(x,u)\in\mathbb R\cup\{+\infty\}$, linear dynamics $f_t(x,u)$, a final cost $V_T$ and an initial state $x_0$. The problem (1) is

$$\min_{x,u}\ \sum_{t=0}^{T-1}C_t(x_t,u_t)+V_T(x_T)\quad\text{s.t. } x_{t+1}=f_t(x_t,u_t),\ x_t\in\mathcal X_t,\ u_t\in\mathcal U_t(x_t).$$

The Bellman functions are $V_t(x)=\inf_{u\in\mathcal U_t(x)}W_t(x,u)$ on $\mathcal X_t$ and $+\infty$ elsewhere, with $W_t(x,u)=C_t(x,u)+V_{t+1}(f_t(x,u))$.

Assumptions (H₁) require $\mathcal U_t$ to be a convex multifunction with convex compact values; $C_t$ and $V_T$ to be convex, lower semicontinuous and proper; and $V_T$ to be finite and Lipschitz on $\mathcal X_T$. They also require extended relatively complete recourse (ERCR): for some $\delta_t>0$, on the enlarged set $\mathcal X'_t=\mathcal X_t+B_t(\delta_t)$ (a $\delta_t$-neighbourhood inside the affine hull of $\mathcal X_t$) the cost $C_t$ is finite and some admissible control leads into $\mathcal X_{t+1}$.

The cutting-plane method keeps approximations $V^k_t$, starting from $V^0_t\equiv-\infty$ and with $V^k_T=V_T$. At iteration $k$ it runs forward from $x^k_0=x_0$. At each stage it solves the one-stage problem with $V^{k-1}_{t+1}$ in place of $V_{t+1}$, which gives a minimizer $u^k_t$, the optimal value $\theta^k_t$ and a Lagrange multiplier $\beta^k_t$ of the constraint $x=x^k_t$. It then adds the cut

$$V^k_t(x)=\max\big(V^{k-1}_t(x),\ \theta^k_t+\langle\beta^k_t,x-x^k_t\rangle\big)$$

and moves to $x^k_{t+1}=f_t(x^k_t,u^k_t)$. The approximate cost-to-go is $W^k_t(x,u)=C_t(x,u)+V^k_{t+1}(f_t(x,u))$.

Formalization targets

Goal: Theorem 2.1

For every run of the method and every $t=0,\dots,T-1$,

$$\lim_{k\to\infty}W_t(x^k_t,u^k_t)-V_t(x^k_t)=0\qquad\text{and}\qquad\lim_{k\to\infty}V_t(x^k_t)-V^k_t(x^k_t)=0.$$

The first limit says the computed decisions become optimal for the true Bellman functions; the second says the cuts become exact at the visited states. Nothing is claimed away from the generated trajectories.

Milestones

In the order the proof uses them:

• Lemma 5.1 (marginal functions of convex problems over convex multifunctions are convex, and attained);
• the tightness identity (10), $V^k_t(x^k_t)=\theta^k_t=W^{k-1}_t(x^k_t,u^k_t)$;
• Lemma 2.2 (i)–(iii): $V_t$ convex and Lipschitz on $\mathcal X_t$; validity $V^k_t\le\tilde V_t\le V_t$; bounded multipliers;
• Corollary 2.1 (one Lipschitz constant for all cuts);
• Lemma 5.2 (monotone Lipschitz minorants on a compact set);
• the two halves of the backward induction step of the proof of Theorem 2.1.

Companion items state that runs exist under (H₁) and give Kelley's cutting-plane lemma (Lemma 2.1), the warm-up result of §2.

Significance

Theorem 2.1 is a convergence guarantee for cutting-plane decomposition of nonlinear convex multistage problems. It does not depend on finitely many dual extreme points, so it covers problems with nonlinear convex costs and convex control constraints. The result is the template for the stochastic Theorem 3.1, which covers SDDP, CUPPS and DOASA as special cases of a general node-selection scheme. Along the way the paper isolates ERCR, a constraint qualification that is exactly what bounds the Lagrange multipliers and makes the cuts uniformly Lipschitz.

The result is proved in the paper; as far as is known it has no machine-checked proof. This mission produces a Lean statement of the deterministic algorithm, with extended-real Bellman functions, cut validity, and multiplier selection as a predicate on runs. It also supplies the statements of the reusable lemmas: marginal-function convexity, the monotone-minorant lemma, Kelley's method. Formal proofs of the milestones, alternative arguments, and explicit Lipschitz constants are all open.

Difficulty

The naive argument, "the approximations increase and are bounded by $V_t$, so they converge", only gives pointwise convergence of $V^k_t$ to some limit below $V_t$. It does not show that the limit equals $V_t$ at the states actually visited, and the visited states change from iteration to iteration. The proof must control cuts computed at one state when they are evaluated at another. This needs a uniform bound on the multipliers $\beta^k_t$. That bound comes from ERCR (moving a distance $\delta_t/2$ in every direction of the affine hull stays where the cost is finite), together with Lipschitz continuity of $V_t$ on a compact set lying inside the relative interior of its domain. Without ERCR the multipliers can be unbounded and the argument breaks. A second difficulty is the backward induction itself: the conclusion at stage $t$ uses both limits at stage $t+1$, and passing from $V^k_{t+1}$ to $V^{k-1}_{t+1}$ needs a compactness argument (Lemma 5.2).

Formalization scope

States are EuclideanSpace ℝ (Fin d) and controls EuclideanSpace ℝ (Fin p); costs and value functions are EReal-valued. Convexity of an extended-real function means convexity of its epigraph. Minima are EReal infima ($+\infty$ over an empty set), with attainment stated separately. $V_T$ is extended by $+\infty$ outside $\mathcal X_T$.

The Lagrange multiplier condition is encoded by (12): $\beta^k_t$ lies in the direction space of $\operatorname{Aff}(\mathcal X_t)$ and is a subgradient, on $\operatorname{Aff}(\mathcal X_t)$, of the stage optimal value at $x^k_t$. A run is a predicate on $(x,u,\theta,\beta)$: any minimizer and any multiplier are allowed. The paper's iteration $k\ge1$ is Lean's k + 1.

Standing assumptions added to (H₁), all used by the paper's proofs:

• $T>0$;
• every $\mathcal X_t$ ($t\le T$) is convex and compact (the paper uses this on pp. 5, 8 and 11 and states it as (H₂)(1) in §3);
• $x_0\in\mathcal X_0$.

Deviations from the page:

• Lemma 5.1 is stated for a jointly convex $J(x,u)$, the form its proof and its use need.
• Lemma 2.2 (ii) states $V^k_t\le\tilde V_t$ on $\operatorname{Aff}(\mathcal X_t)$. The printed "everywhere" fails outside the affine hull when that hull is a proper subspace.
• Corollary 2.1 is stated wherever $V^k_t$ is finite, because $V^k_t\equiv-\infty$ during the first $T-1-t$ iterations.

Limits are Tendsto … (𝓝 0) in EReal. There, convergence to $0$ forces the differences to be eventually finite, so a value of $\pm\infty$ cannot make a limit hold for free. The goal's hypotheses are exactly (H₁) and the run predicate. Statements that only assert the existence of a good run, or bound $\theta^k_t$ instead of the cuts, are not formalizations of Theorem 2.1.

A complete development needs:

• Lipschitz continuity of a convex function on a compact subset of the relative interior of its domain;
• the existence of subgradients relative to an affine subspace;
• marginal-function convexity for extended-real functions.

All three are reusable well beyond this mission. Proofs of any milestone are welcome, as are proofs of the companion items.

Selected references

• P. Girardeau, V. Leclère, A. B. Philpott, On the Convergence of Decomposition Methods for Multistage Stochastic Convex Programs, Mathematics of Operations Research 40(1), 2015; author's version hal-01208295v1. https://doi.org/10.1287/moor.2014.0664, https://hal.science/hal-01208295
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52, 1991. https://doi.org/10.1007/BF01582895
• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Operations Research Letters 36(4), 2008. https://doi.org/10.1016/j.orl.2008.01.013
• A. Shapiro, Analysis of stochastic dual dynamic programming method, European Journal of Operational Research 209(1), 2011. https://doi.org/10.1016/j.ejor.2010.08.007
• J. E. Kelley, The cutting-plane method for solving convex programs, Journal of the SIAM 8(4), 1960. https://doi.org/10.1137/0108053

Who gains when a firm controls more decisions

A firm that sells differentiated products sets more than prices. It chooses quality levels (features, materials, reliability) and the ancillary services that come free with a product, such as a factory warranty or free maintenance for a fixed period. Wang, Ke and Cui (SSRN 3766191; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2020.0947) study the joint choice of price, quality and service duration when consumers choose according to the multinomial logit (MNL) model.

A firm allowed to make more decisions can never earn less: it may always ignore the extra instruments. The question this mission formalizes is what happens to consumers. A natural guess is that every new instrument lets the firm extract more of the consumers' surplus. Section 2.3 of the paper (Proposition 5) shows that under MNL demand this guess is wrong: consumer surplus also rises, so more control is a "win–win". The welfare measure is the logit consumer surplus of Anderson, de Palma and Thisse (Discrete Choice Theory of Product Differentiation, MIT Press, 1992).

The mission is the sixth of a series on the paper; each mission defines its own copy of the model in its own namespace.

Setting

There are $N$ products $i\in\mathcal N=\{1,\dots,N\}$. Product $i$ has a price $p_i$, a quality level $q_i$ and a service duration $t_i$, which must lie in a fixed interval $[t_s,t_l]$. The parameters are: $\alpha_i$, the consumers' sensitivity to quality; $s_i$, the utility of one unit of service time; $c_i>0$, so that producing one unit at quality $q_i$ costs $c_iq_i^2$; and $a_i,b_i$, so that service costs $a_i-b_iq_i$ per unit of time. The sign of $b_i$ is free: higher quality may make service cheaper ($b_i>0$), dearer ($b_i<0$), or leave it unchanged ($b_i=0$).

A consumer buys product $i$ with the MNL choice probability

$$d_i(\mathbf p,\mathbf q,\mathbf t;\mathcal N)=\frac{\exp(\alpha_iq_i-p_i+t_is_i)}{1+\sum_{j\in\mathcal N}\exp(\alpha_jq_j-p_j+t_js_j)},$$

where the $1$ is the outside option of buying nothing. With market size one, the firm's profit is

$$\Pi(\mathbf p,\mathbf q,\mathbf t;\mathcal N)=\sum_{i\in\mathcal N}\big[p_i-c_iq_i^2-t_i(a_i-b_iq_i)\big]\,d_i(\mathbf p,\mathbf q,\mathbf t;\mathcal N),$$

and the bracket is the markup of product $i$. Consumer surplus is

$$\mathrm{CS}(\mathbf p,\mathbf q,\mathbf t)=\log\Big(1+\sum_{i\in\mathcal N}\exp(\alpha_iq_i-p_i+t_is_i)\Big).$$

Three problems are compared, at the same pre-determined qualities $\mathbf q$ and durations $\mathbf t\in[t_s,t_l]^N$:

1. price only: maximize $\Pi(\cdot,\mathbf q,\mathbf t)$ over $\mathbf p\in\mathbb R^N$, with a maximizer $\mathbf p^\dagger$;
2. price and service: maximize $\Pi(\cdot,\mathbf q,\cdot)$ over $\mathbf p\in\mathbb R^N$ and $\mathbf t'\in[t_s,t_l]^N$, with a maximizer $(\mathbf p^\ddagger,\mathbf t^\ddagger)$;
3. price, quality and service, problem (4): maximize $\Pi$ over all three, with a maximizer $(\mathbf p^*,\mathbf q^*,\mathbf t^*)$.

Section 5.1 adds the manufacturer's short-term problem (10): qualities are fixed, and the firm also chooses which products $S\subseteq\mathcal N$ to offer.

Formalization targets

Goal: Proposition 5 (p. 13)

For every maximizer of each of the three problems,

$$\mathrm{CS}(\mathbf p^\dagger,\mathbf q,\mathbf t)\;\le\;\mathrm{CS}(\mathbf p^\ddagger,\mathbf q,\mathbf t^\ddagger)\;\le\;\mathrm{CS}(\mathbf p^*,\mathbf q^*,\mathbf t^*).$$

The inequalities are weak; equality holds, for instance, when the pre-determined $\mathbf q,\mathbf t$ are already optimal.

Milestones

1. Equation (17) (p. 26). For fixed $\mathbf q,\mathbf t$, the equation $r=\sum_i\exp(\alpha_iq_i-c_iq_i^2+t_i(s_i-(a_i-b_iq_i))-r-1)$ has a unique root $r^\dagger$; a price vector is optimal if and only if every markup equals $1+r^\dagger$; the optimal profit is $r^\dagger$.
2. Proposition 8 (p. 21). In problem (10) all products should be offered, an optimum uses durations $t_s$ or $t_l$ according to the sign of $b_i$ and the position of $q_i$, every optimal markup is $1+r^*$, and $r^*$ is the unique root of the corresponding equation.
3. Consumer surplus at an optimum (Online Supplement p. 1). If every markup is $1+r$ and the profit is $r$, then $\mathrm{CS}=\log(1+r)$.
4. Ordering of profits (Online Supplement p. 2): $r^\dagger\le r^\ddagger\le r^*$.

Significance

The result separates two effects that are usually conflated. More instruments raise profit; Proposition 5 says that under MNL demand the extra profit comes from serving more consumers (fewer choose the outside option), not from extracting more surplus from each. Proposition 8 states the corresponding structure for a firm whose product designs are already fixed: offer everything, use extreme service durations, and keep markups equal across products.

The paper proves these results; none is formalized. A machine-checked development produces the welfare comparison together with the price step of the MNL multi-product pricing problem (equal markups at every optimum, uniqueness of the optimal profit as a fixed point) as reusable statements, and pins down the boundary cases of Proposition 8 that the printed statement leaves implicit.

Difficulty

The ordering of profits is immediate from the nesting of feasible sets. The obstacle is translating it into consumer surplus: consumer surplus is not monotone in profit along arbitrary price vectors, and the argument needs that at every maximizer of each problem all markups are equal to $1+r$, with $r$ the optimal profit. That requires a global optimality analysis of the multi-product MNL pricing problem: the profit is not concave in prices, and both the uniqueness of the fixed point and the characterization of all maximizers (not only a stationary point) must be established. Comparing values $\log(1+r)$ with $r$ defined as the optimal profit, without linking them to the maximizers, proves nothing about consumer surplus.

Formalization scope

• Products are Fin N (0-based); $N$ is arbitrary and $N=0$ is allowed. The outside option is the $1$ in the denominator, not a product.
• Parameters $\alpha,a,b,c,s:\mathrm{Fin}\,N\to\mathbb R$; only $c_i>0$ and $t_s\le t_l$ are assumed throughout. No sign is imposed on $b_i$, $\alpha_i$, $a_i$ or $s_i$, and products are not assumed identical.
• Qualities range over $\mathbb R$, not the model's normalized range $[0,a_i/b_i)$, because the paper's joint optimum is computed over unconstrained qualities. Proposition 8(b) adds the model's bound $q_i\le a_i/b_i$ for $b_i>0$, without which the printed rule can fail.
• "Optimal" means a global maximizer over the stated feasible set. The goal quantifies over all maximizers of the three problems; their existence is not part of Proposition 5.
• The MNL formula and the log-sum consumer surplus are definitions; their derivation from Gumbel random utilities is cited, not formalized.
• Problem (10) is printed with $\Pi(\mathbf p,\mathbf q,\mathbf t;\mathcal N)$; the profit of the offer set $S$ is meant and is what is formalized.

A formalization in which the maximizers are given by the paper's closed-form prices, in which $r^\dagger,r^\ddagger,r^*$ are defined as optimal values and only $\log(1+r)$ is compared, or in which there is a single product, would make the goal trivial or different and is ruled out.

Contributions are welcome on the MNL price step (equation (17)), which is reusable for any multi-product logit pricing model, and on the per-product separation of the duration choice in Proposition 8.

Selected references

• R. Wang, C. Ke, S. Cui, Product Price, Quality and Service Decisions under Consumer Choice Models, Manufacturing & Service Operations Management, 2022; accepted manuscript SSRN 3766191. https://ssrn.com/abstract=3766191, https://doi.org/10.1287/msom.2020.0947
• S. P. Anderson, A. de Palma, J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992, ISBN 978-0-262-01128-0.
• D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, 1974, 105–142. https://eml.berkeley.edu/reprints/mcfadden/zarembka.pdf