Optimization

Motivation

Supply disruptions — fires, quality failures, capacity shortfalls at a supplier — are a first-order risk in manufacturing supply chains. A buying firm has two broad responses. It can dual source, splitting orders between suppliers so that one supplier's shortfall is partly covered by the other, or it can invest in process improvement at a single supplier (kaizen events, supplier development programmes) to make that supplier more reliable. Wang, Gilland and Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement? (M&SOM 12(3):489–510, 2010), build a two-stage newsvendor model that captures both levers and compare them analytically.

This mission formalizes the paper's analysis of the improvement lever on its own: the firm commits early to one supplier, decides how much effort to spend improving it, and then orders. The paper's Theorem 3 shows that, without committed costs, this improvement problem is a concave program with an explicit first-order condition, and its Corollary 2 derives how the optimal effort responds to costs, revenue and the chance that improvement succeeds. These are the facts the paper's later comparisons between improvement and dual sourcing rest on.

Setting

A firm sells one product over one season at unit revenue $r$, salvage value $v$ and unit penalty $p$ for unmet demand. Demand $X \ge 0$ has distribution function $F$ and finite mean. The firm orders $q \ge 0$ units from a supplier with design capacity $K > 0$, unit cost $c$ and committed cost $\eta \in [0,1]$: the firm pays $(\eta q + (1-\eta)y)c$ when $y$ units are delivered.

The supplier suffers a random capacity loss $\xi \ge 0$ and delivers $y = \min\{q, (K-\xi)^+\}$. The law of $\xi$ has a continuous distribution function $G(\cdot, a)$ that depends on the supplier's reliability index $a$; a larger index means a stochastically smaller loss, $G(\cdot, a) \le G(\cdot, a')$ for $a \le a'$. Demand and losses are independent.

With $\psi = -\eta c/(r+p-v)$ and $\varphi = (r+p-(1-\eta)c)/(r+p-v)$, the second-stage expected profit at index $a$ is

$$\Pi_2(q; a) = (r+p-v)\big(\psi q + \varphi\,\mathsf E[y] - \mathsf E[(y-X)^+]\big) - p\,\mathsf E[X],$$

and $\Pi_2^*(a) = \sup_{q \ge 0}\Pi_2(q; a)$ is its optimal value.

In the first stage the firm may improve the supplier from its initial index $a^0$. The paper reparametrizes effort by the target index: reaching index $a \ge a^0$ needs effort $z(a)$, where $z$ is convex and nondecreasing with $z(a^0) = 0$. Effort costs $m$ per unit and succeeds with probability $\theta$. The first-stage profit of early commitment is Eq. (7):

$$\Pi_1(a) = -m\,z(a) + \theta\,\Pi_2^*(a) + (1-\theta)\,\Pi_2^*(a^0), \qquad a \ge a^0 .$$

Formalization targets

Goal: Theorem 3

Assume $\eta = 0$ and that $a \mapsto G(\xi, a)$ is concave on $[a^0,\infty)$ for every $\xi$ (decreasing marginal reliability improvement). Then $\Pi_1$ is concave on $[a^0, \infty)$, and an optimal index $a^* > a^0$, with an optimal order $q^*$ at $a^*$, satisfies

$$\frac{m}{\theta}\,z'(a^*) = (r+p-v)\int_{K-q^*}^{K}\big(\varphi - F(K-\xi)\big)\,\frac{\partial G(\xi, a^*)}{\partial a}\,d\xi. \tag{8}$$

Milestones

1. Eq. (6), single-supplier instance with $\eta = 0$. For $0 < \varphi < 1$ the critical fractile $\hat q = \inf\{t : F(t) \ge \varphi\}$ maximizes $\Pi_2(\cdot\,; a)$ for every index $a$, and (with atomless demand) every positive optimal order satisfies the $\eta = 0$ instance of (6), $G(K-q^*,a)(\varphi - F(q^*)) = 0$.
2. Lemma 2(b), single-supplier instance. $\Pi_2^*(a)$ is increasing in $a$.
3. Corollary 2 (a), (b), (c), (e). The optimal reliability index, and so the optimal effort $z^* = z(a^*)$, is decreasing in $m$, increasing in $\theta$, decreasing in $c$ and increasing in $r$, each in the strong set order on the set of maximizers.

Significance

Theorem 3 turns the firm's improvement decision into a one-dimensional concave program, so that the first-order condition (8) characterizes the optimum and comparative statics are available. Corollary 2 is the managerial content: cheaper or more reliable improvement, a cheaper supplier and a more valuable product all justify more improvement effort. The paper's later results — when late commitment beats early commitment (§4.2.2) and when single sourcing with improvement beats dual sourcing (§5) — compare the optimal values these results describe.

The results are proved in the paper's online appendix; none of them has a machine-checked proof. A complete development provides formal proofs of the layer-cake representation of the random-capacity newsvendor profit, of its critical-fractile solution, and of the concavity and envelope arguments on top of it.

Difficulty

$\Pi_2^*$ is an optimal value, a supremum over order quantities, and suprema of concave functions are not concave in general. The obvious route — "$\Pi_2(q; a)$ is concave in $a$ for each $q$, hence so is the supremum" — fails, because $\Pi_2(q;a)$ is not concave in $a$ for a fixed $q$ beyond the critical fractile. Any argument has to control how the optimal order moves with $a$ under random capacity, where the delivered quantity is a minimum of the order and a random effective capacity. The first-order condition then requires differentiating an expectation of a non-smooth function of $(\xi, X)$ in the parameter of $\xi$'s law. Corollary 2 must be argued on the set of maximizers, since $\Pi_1$ is concave but not strictly concave.

Formalization scope

The Lean development lives in the namespace MitigateSupplyRisk.Improvement. Model bundles $r, v, p, c, \eta, K$, a demand law $\mu$ and the family $\nu(a)$ of loss laws; $F$ and $G(\cdot,a)$ are their cdf. Expectations are Bochner integrals over $\nu(a)$ and over the product $\nu(a)\otimes\mu$. Model.Assumptions collects the standing assumptions of §3: $0 \le \eta \le 1$, $K > 0$, $v < r+p$ (implicit in the paper's division by $r+p-v$), a nonnegative integrable demand, nonnegative atomless losses, and the stochastic order in $a$. Demand needs no density. Effort bundles $\theta, m, a^0, z$ with $\theta \in [0,1]$, $m \ge 0$ and $z$ convex, nondecreasing on $[a^0,\infty)$, $z(a^0) = 0$; taking $z$ as primitive assumes every index $a \ge a^0$ is reachable. $\Pi_2^*$ is a real supremum and $\Pi_1$ is built from it, never from the critical fractile. Every statement about $\Pi_2^*$ carries $\eta = 0$ or $c \ge 0$, which makes the supremum finite. "Optimal" always means a maximizer over the whole feasible set, and "increasing" is weak throughout, as on p. 492 of the paper.

The paper's proofs are in an online appendix that was not used here. Deviations from the page, each disclosed in the item's Formalization Note:

• Eq. (8) omits the factor $r+p-v$ on its right side; it is correct as printed only when $r+p-v = 1$, which holds in all of the paper's numerical examples. The goal states the corrected identity, multiplied by $\theta$.
• $\partial^2 G/\partial a^2 \le 0$ is read as concavity of $G(\xi,\cdot)$ on $[a^0,\infty)$.
• (8) is the first-order condition at an interior optimum $a^* > a^0$; differentiability of $z$ and of $G(\xi,\cdot)$ at $a^*$ is assumed explicitly.
• Corollary 2 is stated in the strong set order on the argmax, (c) and (e) in the setting $\eta = 0$ of Theorem 3, and (b) with $c \ge 0$. Corollary 2(d), on the committed cost $\eta$, is not stated, because Theorem 3's setting fixes $\eta = 0$.
• Lemma 2(b) and Eq. (6) are the single-supplier instances of the paper's dual-sourcing statements, which the paper applies to single sourcing on p. 496.

A trivializing formalization is ruled out: $\Pi_1$ is built from the supremum $\Pi_2^*$ (not from $\Pi_2$ at a fixed order), the supremum is finite under the stated hypotheses, and every expectation is of an integrable function, so no statement holds through a junk value.

Reusable beyond this mission: the random-capacity newsvendor objects (delivered quantity, expected profit, layer-cake representation) and a Topkis-type monotone comparative statics lemma on a chain. Contributions of either, and proofs of the milestones in any order, are welcome.

Selected references

• Y. Wang, W. Gilland, B. Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement?, Manufacturing & Service Operations Management 12(3):489–510, 2010. https://doi.org/10.1287/msom.1090.0279
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
• R. B. Handfield, D. R. Krause, T. V. Scannell, R. M. Monczka, Avoid the Pitfalls in Supplier Development, Sloan Management Review 41(2):37–49, 2000.

Motivation

The Lasso fits a linear model by least-norm regression with an $\ell^1$ penalty, and its most used property is that it returns sparse coefficient vectors: many features receive weight exactly zero. Most sparsity guarantees for the Lasso are statistical. They assume a generative model and an incoherence or irrepresentability condition on the design, and conclude that the support is recovered (Tropp 2006; Zhao and Yu 2006).

Xu, Caramanis and Mannor (arXiv:0811.1790v1, 2008; IEEE Trans. Inf. Theory 56(7), 2010) show that the Lasso's $\ell^1$-regularized regression problem is exactly a robust regression problem in which each feature column is perturbed independently within a norm ball (their Theorem 1; mission 1 of this series). Section IV of the paper uses this robust view to give a sparsity criterion that needs no generative model: a feature gets zero weight if some allowable perturbation makes it irrelevant. This mission formalizes that criterion, Theorem 5, together with the more general Theorem 5′ it specializes, and the geometric consequence Theorem 6.

Setting

Fix integers $n, m$. The data are the features $a_1,\dots,a_m \in \mathbb R^n$, the columns of a matrix $A$, and a response $b \in \mathbb R^n$. For $x\in\mathbb R^m$, $Ax = \sum_i x_i a_i$. A disturbance $\Delta A = (\delta_1,\dots,\delta_m)$ perturbs column $i$ to $a_i + \delta_i$.

Given radii $c_1,\dots,c_m \ge 0$, the feature-wise uncoupled uncertainty set is

$$\mathcal U = \{(\delta_1,\dots,\delta_m) \mid \|\delta_i\|_2 \le c_i,\ i = 1,\dots,m\}.$$

For a set $\mathcal V$ of disturbances, the robust objective is

$$R_{A,\mathcal V}(x) = \max_{\Delta A\in\mathcal V}\|b - (A+\Delta A)x\|_2,$$

and the robust regression problem is $\min_{x\in\mathbb R^m} R_{A,\mathcal V}(x)$. It has a solution supported on $I \subseteq \{1,\dots,m\}$ if some minimizer $x^*$ has $x^*_j = 0$ for all $j \in I^c = \{1,\dots,m\}\setminus I$.

For a disturbance $\Delta A$, $\Delta A^I$ agrees with $\Delta A$ on the features in $I$ and is zero elsewhere, and $\mathcal U^I = \{\Delta A^I \mid \Delta A \in \mathcal U\}$. Given numbers $l_j$ for $j\notin I$, the enlarged set of Theorem 5′ is

$$\tilde{\mathcal U} = \{(\delta_1,\dots,\delta_m) \mid \|\delta_i\|_2 \le c_i,\ i \in I;\ \|\delta_j\|_2 \le c_j + l_j,\ j\notin I\}.$$

In Lean these are uncertaintySet c, restrictedSet c I, enlargedSet c l I, robustObjective a b V x, IsRobustSolution and HasSolutionSupportedOn, all in the namespace RobustRegLasso.Sparsity.

Formalization targets

Goal: Theorem 5 (p. 8)

If there is a disturbance $\Delta\tilde A^{I^c}\in\mathcal U$ that is zero on the features in $I$ and such that

$$\min_{x\in\mathbb R^m}\Big\{\max_{\Delta\tilde A^I\in\mathcal U^I}\|b-(A+\Delta\tilde A^{I^c}+\Delta\tilde A^I)x\|_2\Big\}$$

has a solution supported on $I$, then $\min_x R_{A,\mathcal U}(x)$ has a solution supported on $I$.

Milestones (proof order)

1. First display of the proof of Theorem 5′ (p. 9). If $x^*_j = 0$ off $I$ and $\tilde a_i = a_i$ on $I$, then $R_{A,\tilde{\mathcal U}}(x^*) = R_{A,\mathcal U}(x^*) = R_{\tilde A,\mathcal U}(x^*)$, and also $R_{\tilde A,\tilde{\mathcal U}}(x^*) = R_{A,\mathcal U}(x^*)$.
2. Second display of the proof of Theorem 5′ (p. 9). If $\|a_j-\tilde a_j\|_2 \le l_j$ off $I$ and $a_i = \tilde a_i$ on $I$, then $\{A+\Delta A \mid \Delta A\in\mathcal U\}\subseteq\{\tilde A+\Delta A\mid\Delta A\in\tilde{\mathcal U}\}$, hence $R_{\tilde A,\tilde{\mathcal U}} \ge R_{A,\mathcal U}$ pointwise.
3. Theorem 5′ (pp. 8–9). If $x^*$ minimizes $R_{A,\mathcal U}$ and $x^*_j = 0$ off $I$, then $x^*$ minimizes $R_{\tilde A,\tilde{\mathcal U}}$ for every $\tilde A$ with $\|\tilde a_j - a_j\|_2\le l_j$ off $I$ and $\tilde a_i = a_i$ on $I$.
4. Theorem 6, conclusion corrected (p. 10). With $c_i = c$ for all $i$: if every unit $v\in\operatorname{span}(\{a_i, i\in I\}\cup\{b\})$ has $v^\top a_j\le c$ for all $j\notin I$, then some optimal solution of $\min_x R_{A,\mathcal U}(x)$ vanishes off $I$.

Theorem 5 is Theorem 5′ applied to the perturbed matrix $A + \Delta\tilde A^{I^c}$ with radii $c_j = 0$ off $I$, $l_j = c_j$ and $\tilde A = A$.

Significance

The result separates sparsity from statistics. Theorem 5 asks only that the features outside $I$ can be made irrelevant by a perturbation within the uncertainty budget; it involves no noise model and no probability. Theorem 6 turns this into an incoherence-type condition: features that lie within $c$ of being orthogonal to the response and to the relevant features receive zero weight. Because the robust problem over $\mathcal U$ is the $\ell^1$-regularized regression $\min_x \|b-Ax\|_2 + \sum_i c_i|x_i|$ (Theorem 1), these are sparsity statements about that Lasso-type problem. The same argument gives the paper's further results on angular separation and nearly dependent features, which it defers to a companion report.

These results are proved in the paper; none of them has a machine-checked proof on Prove2Me or, to our knowledge, elsewhere. The mission formalizes the known proof. It also records a correction: Theorem 6 as printed claims that every optimal solution vanishes off $I$, which is false (a two-dimensional counterexample is in the milestone's statement); the proof gives existence of one such solution, and that is what is posed.

Difficulty

The proof of Theorem 5′ is short, and the work is in the bookkeeping. The obvious attempt treats "max" as a real supremum and compares values directly; it has to know that each uncertainty set is nonempty and that the residual is bounded on it, and the enlarged set $\tilde{\mathcal U}$ is nonempty only because $l_j \ge \|\tilde a_j - a_j\|_2 \ge 0$. The two equalities of the first display require reassigning the columns outside $I$ of a disturbance (to zero, or to a feasible value) without changing the residual at $x^*$, which works only because $x^*_j = 0$ there. The specialization of Theorem 5′ to Theorem 5 changes the radius vector and the base matrix at the same time, and needs $\mathcal U^I$ to coincide with the feature-wise set whose radii are $c_i$ on $I$ and $0$ off it. Theorem 6 additionally needs the equivalence of the robust problem with an $\ell^1$-regularized problem, an orthogonal projection onto a span, and the existence of a minimizer of a coercive (or, for $c = 0$, least-squares) objective.

Formalization scope

• Features are a family a : Fin m → EuclideanSpace ℝ (Fin n); a disturbance is δ : Fin m → EuclideanSpace ℝ (Fin n); $A+\Delta A$ is the family a + δ. Index sets are Finset (Fin m) (0-based). The loss is the $\ell^2$ norm, as stated in the paper (which remarks that any norm works).
• "max" over a set of disturbances is the supremum in EReal (⨆ δ ∈ V). With nonnegative radii every set used is nonempty and bounded, so the value is a finite, attained real number; no junk value of a real sSup can make a statement vacuous. "Optimal solution" means a minimizer of this objective over all of $\mathbb R^m$; existence of a minimizer is assumed where the paper assumes it (Theorem 5′) and concluded where the paper concludes it (Theorems 5, 6).
• Radii $c_i \ge 0$ are hypotheses (the paper's standing convention). $l_j \ge 0$ is not assumed: it follows from $\|\tilde a_j - a_j\|_2 \le l_j$.
• Corrected printed typos: $I\subseteq\{1,\dots,n\}$ on p. 8 is read with $m$; the inequality after "For an arbitrary $x'$" is posed with $A$ and $\tilde A$ exchanged, as the inclusion and the final display require; Theorem 6's "any optimal solution" becomes "some optimal solution", and "$I\subset$" becomes $I\subseteq$.
• The robust objective is the supremum over the set, never its closed form $\|b-Ax\|_2+\sum_i c_i|x_i|$; with that definition the problem would no longer be a robust problem and Theorems 5 and 5′ would be about a different function.
• The definitions here restate objects of mission 1 of this series (the set (2) and $Ax$). The interpretation through a generative model (p. 9) and the results deferred to the companion report are not formalized. Contributions of proofs of any milestone, and of a local proof of Theorem 1 for use in Theorem 6, are welcome.

Selected references

• H. Xu, C. Caramanis, S. Mannor, Robust Regression and Lasso, arXiv:0811.1790v1, 2008; IEEE Transactions on Information Theory 56(7), 2010. https://arxiv.org/abs/0811.1790v1, https://doi.org/10.1109/TIT.2010.2048503
• R. Tibshirani, Regression shrinkage and selection via the lasso, Journal of the Royal Statistical Society B 58(1), 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
• J. A. Tropp, Just relax: convex programming methods for identifying sparse signals in noise, IEEE Transactions on Information Theory 52(3), 2006. https://doi.org/10.1109/TIT.2005.864420
• P. Zhao, B. Yu, On model selection consistency of Lasso, Journal of Machine Learning Research 7, 2006. https://jmlr.org/papers/v7/zhao06a.html
• L. El Ghaoui, H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM Journal on Matrix Analysis and Applications 18(4), 1997. https://doi.org/10.1137/S0895479896298130

Motivation

Firms that buy from unreliable suppliers face two broad remedies: spread orders across several suppliers (dual sourcing), or invest in making a supplier more reliable (process improvement). Wang, Gilland and Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement? (M&SOM 12(3):489–510, 2010), compare the two in a single newsvendor model in which suppliers deliver less than ordered because of random capacity losses. This mission covers the first half of that comparison: the pure dual-sourcing strategy, in which the firm improves nobody and only chooses how much to order from each of two suppliers.

A single-supplier random-capacity model was studied by Ciarallo, Akella and Morton (Management Science 40(3), 1994); in that model, as the paper notes, the firm never orders more than demand to hedge against capacity shortfall. Dada, Petruzzi and Schwarz (M&SOM 9(1), 2007) studied several unreliable suppliers but gave only necessary conditions for optimal orders. The paper states necessary and sufficient conditions for two suppliers (its Theorem 1) and, for deterministic demand, a closed-form optimal order in each of six demand regions (Theorem 2). Its proofs are in an online appendix.

Setting

A product sells at unit revenue $r$, is salvaged at $v$, and unmet demand costs $p$ per unit, with $v < r + p$. Two suppliers $i = 1, 2$ have unit cost $c_i \ge 0$, committed-cost fraction $\eta_i \in [0, 1]$ and design capacity $K_i > 0$. Supplier $i$ suffers a random capacity loss $\xi_i \ge 0$ whose continuous distribution function $G_i(t, a_i)$ depends on a reliability index $a_i$: a larger index makes the loss stochastically smaller, $G_i(\cdot, a) \le G_i(\cdot, \hat a)$ for $a \le \hat a$. The losses are independent of each other and of demand $X \ge 0$, which has distribution function $F$.

For an order vector $q = (q_1, q_2) \ge 0$, supplier $i$ delivers $y_i = \min\{q_i, (K_i - \xi_i)^+\}$ and is paid $(\eta_i q_i + (1 - \eta_i) y_i) c_i$. The realized profit is

$$\pi(q) = -\sum_i (\eta_i q_i + (1-\eta_i) y_i) c_i + r \min\Big\{x, \sum_i y_i\Big\} + v\Big(\sum_i y_i - x\Big)^+ - p\Big(x - \sum_i y_i\Big)^+,$$

and the second-stage expected profit is $\Pi_2(q; a) = \mathbb E_{\xi(a), X}[\pi(q)]$. With $\psi_i = -\eta_i c_i/(r+p-v)$ and $\phi_i = (r + p - (1-\eta_i)c_i)/(r+p-v)$ this is the paper's Eq. (3). The optimal value is $\Pi_2^*(a) = \sup_{q \ge 0} \Pi_2(q; a)$, and an optimal procurement vector is a $q \ge 0$ attaining it.

Formalization targets

Goal: Theorem 2 (corrected)

Let demand be deterministic, $X = x \ge 0$, let $\eta = 0$, let $0 < \phi_i < 1$, let each $G_i$ be strictly increasing on a support $[0, b_i]$ with $b_i \le K_i$, and let $\phi_1 G_1(K_1) \ge \phi_2 G_2(K_2)$. With $A_1 = G_1^{-1}(\phi_2)$, $A_2 = G_2^{-1}(\phi_1)$, $B = G_1^{-1}(\tfrac{\phi_2}{\phi_1}G_2(K_2))$ and $S = K_1 + K_2$, an optimal vector is

$$q^* = \begin{cases} (x, 0) & 0 \le x \le K_1 - B \quad (\Omega_1)\\ (x - q_2^*, q_2^*),\ \phi_1 G_1(K_1 - x + q_2^*) = \phi_2 G_2(K_2 - q_2^*) & x \le S - (A_1 + A_2) \quad (\Omega_2)\\ (x - K_2 + A_2,\ x - K_1 + A_1) & x \le S - \max(A_1, A_2) \quad (\Omega_3)\\ (x - K_2 + A_2, K_2) \text{ if } A_1 \ge A_2, \text{ else } (K_1, x - K_1 + A_1) & x \le S - \min(A_1, A_2) \quad (\Omega_4)\\ (K_1, K_2) & \text{otherwise} \quad (\Omega_5 \cup \Omega_6).\end{cases}$$

In $\Omega_3$–$\Omega_5$ the firm orders more in total than demand: the quantity hedge.

Milestones

1. Lemma 1: $\Pi_2(q; a)$ is submodular in $q$, $\Pi_2(q \vee q') + \Pi_2(q \wedge q') \le \Pi_2(q) + \Pi_2(q')$.
2. Theorem 1: with a demand density, some optimal $q^*$ has, for each $i$, $q_i^* \in \{0, K_i\}$ or $\nabla_{q_i}\Pi_2(q^*; a) = 0$.
3. Eq. (6): for $0 < q_i < K_i$, $\nabla_{q_i}\Pi_2 = (r+p-v)\big(\psi_i + G_i(K_i - q_i)(\phi_i - \mathbb E[F(q_i + y_j)])\big)$, which vanishes at an optimal $q$.
4. Lemma 2(b): $\Pi_2^*(a)$ is increasing in each $a_i$.
5. Corollary 1 (after the goal): as either index increases, the hedge region $\Omega_3 \cup \Omega_4 \cup \Omega_5$ and the hedge size $[q_1^* + q_2^* - x]^+$ shrink; $\Omega_1$ expands in $a_1$ and contracts in $a_2$.

Significance

Theorem 2 is the paper's explicit description of how a buyer splits orders between two unreliable suppliers: single sourcing when capacity is ample, dual sourcing at total order equal to demand, then deliberate over-ordering, and finally ordering full capacity. The quantity hedge is the paper's main qualitative finding for dual sourcing, since, as the paper notes, over-ordering of this kind does not occur with one random-capacity supplier. Corollary 1 says how this hedge responds to reliability, which is the comparison with process improvement that the rest of the paper builds on; Lemma 2(b) is the value of reliability used there.

None of these results has a machine-checked proof, and the paper's proofs are in an online appendix not used here. A formalization would also settle the printed statement, which contains a slip (below) that a formal proof must avoid.

Difficulty

$\Pi_2$ is submodular but not jointly concave in $q$, so the usual route (concavity plus first-order conditions) is not available, and the paper invokes unimodality instead. Under deterministic demand $\Pi_2$ is not differentiable on the line $q_1 + q_2 = x$, where the $\Omega_1$ and $\Omega_2$ optima sit, so Theorem 1 cannot simply be specialized to Theorem 2: optimality there needs one-sided arguments. In every region the claim is global optimality over all $q \ge 0$, including orders above the design capacities, and the feasible set is unbounded.

Formalization scope

Suppliers are indexed by Fin 2 (index 0 is supplier 1). The capacity losses are a family of probability measures $\nu_i(a)$ on $\mathbb R$ without atoms and with $\nu_i(a)((-\infty, 0)) = 0$, and $G_i(t, a)$ is their distribution function. $\Pi_2$ is the Bochner integral of $\pi$ against $\nu_1(a_1) \otimes \nu_2(a_2) \otimes \mu$ for a demand law $\mu$. Every theorem assumes $\mu$ is a probability measure on $[0, \infty)$ with finite mean. Deterministic demand is $\mu = \delta_x$. Theorem 1 and Eq. (6) add $\mu \ll$ Lebesgue (the paper's density). "Optimal" means a global maximizer over $q \ge 0$, and "increasing" is weak, as the paper declares. Added standing hypotheses: $K_i > 0$, $v < r + p$, and $r, p, c_i \ge 0$, which bound $\pi$ above so that $\Pi_2^*$ is a genuine supremum. $G_i^{-1}$ is the generalized inverse $\inf\{t \ge 0 : G_i(t) \ge u\}$.

Corrections to the printed Theorem 2, each disclosed in its item:

• the $\min$ and $\max$ in the bounds of $\Omega_3$, $\Omega_4$, $\Omega_5$ are swapped back (as printed, $\Omega_4$ is empty and the $\Omega_3$ formula can exceed $K_1$);
• $G_i(K_i) = 1$ is added, through the support hypothesis (without it the $\Omega_1$ claim is false);
• $0 < \phi_i < 1$ and strict increase of $G_i$ on its support are added.

Theorem 1's "$q_i^* = K$" is read as $K_i$. Lemma 2(a) is not formalized: optimal orders are not unique and no reading of "$q_i^*$ is increasing" was found that is both faithful and safely true.

Stating Theorem 2 as "$q^*$ satisfies the first-order conditions", or optimality only within a region's face, would trivialize it; the statement requires $\Pi_2(q; a) \le \Pi_2(q^*; a)$ for every $q \ge 0$. Proofs need integrals of piecewise-linear functions of independent variables, differentiation under the integral sign, and facts about generalized inverses of continuous distribution functions. Lemma 1 and the generalized-inverse facts are reusable beyond this mission; proofs of any milestone are welcome.

Selected references

• Y. Wang, W. Gilland, B. Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement?, Manufacturing & Service Operations Management 12(3):489–510, 2010. https://doi.org/10.1287/msom.1090.0279
• F. W. Ciarallo, R. Akella, T. E. Morton, A Periodic Review, Production Planning Model with Uncertain Capacity and Uncertain Demand — Optimality of Extended Myopic Policies, Management Science 40(3):320–332, 1994. https://doi.org/10.1287/mnsc.40.3.320
• M. Dada, N. C. Petruzzi, L. B. Schwarz, A Newsvendor's Procurement Problem when Suppliers Are Unreliable, Manufacturing & Service Operations Management 9(1):9–32, 2007. https://doi.org/10.1287/msom.1060.0126

Motivation

Monotone variational inequalities (v.i.) cover convex minimization, convex–concave saddle-point problems, Nash equilibria of convex games and complementarity problems. Matrix games and other large saddle-point problems are typical cases. At large scale, first-order methods that use only values of the operator and simple auxiliary minimizations are the practical tool. The paper's introduction (pp. 229–231) contrasts this with the black-box lower bound of order $1/\epsilon^2$ evaluations for nonsmooth Lipschitz minimization, and with Nesterov's smoothing method (2005), which reaches $O(1/t)$ for structured saddle-point objectives. The paper states that its $O(1/t)$ complexity estimate is new, to the author's knowledge, even in the Euclidean case, where the scheme is Korpelevich's extragradient method of 1976.

A. Nemirovski, Prox-Method with Rate of Convergence O(1/t) for Variational Inequalities with Lipschitz Continuous Monotone Operators and Smooth Convex-Concave Saddle Point Problems, SIAM J. Optim. 15(1):229–251, 2004 (doi:10.1137/S1052623403425629), introduced what is now called the mirror-prox method. It showed that two prox steps per iteration give an ergodic error of order $1/N$ when the operator is Lipschitz continuous, and that the bound holds in an arbitrary norm, adapted to the geometry of the feasible set by a distance-generating function. The method and its analysis underlie later work on smooth saddle-point problems, including Nesterov's dual extrapolation and Juditsky–Nemirovski–Tauvel's stochastic mirror-prox (2011).

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$, not necessarily Euclidean. Dual vectors $\xi$ act on $z\in E$ by $\langle\xi,z\rangle$, and the conjugate norm is $\|\xi\|_*=\max_{\|z\|\le1}\langle\xi,z\rangle$. Let $Z\subseteq E$ be nonempty, convex and compact.

The operator $F$ maps $Z$ to dual vectors and satisfies (2.1): it is $L$-Lipschitz, $\|F(z)-F(z')\|_*\le L\|z-z'\|$, and monotone, $\langle F(z)-F(z'),z-z'\rangle\ge0$, for all $z,z'\in Z$. A solution of the v.i. is a point $z_*\in Z$ with $\langle F(z),z_*-z\rangle\le0$ for all $z\in Z$. The accuracy of a candidate $\bar z\in Z$ is

$$\epsilon(\bar z)=\max_{u\in Z}\langle F(u),\bar z-u\rangle .$$

The distance-generating function $\omega:Z\to\mathbb R$ is continuously differentiable on $Z$ and strongly convex with modulus $\alpha>0$ in the form (2.2): $\langle\omega'(z)-\omega'(w),z-w\rangle\ge\alpha\|z-w\|^2$. The prox-mapping is

$$P_z(\xi)=\operatorname*{argmin}_{w\in Z}\big[\omega(w)+\langle\xi-\omega'(z),w\rangle\big],$$

and the constant $\Theta(z_0)=\max_{z\in Z}[\omega(z)-\omega(z_0)-\langle\omega'(z_0),z-z_0\rangle]$ measures how far $Z$ extends from the starting point $z_0$ in the geometry of $\omega$.

The basic implementation fixes the stepsize $\gamma=\alpha/(\sqrt2L)$ (3.2). At step $t$ it computes $w_{t,1}=P_{z_{t-1}}(\gamma F(z_{t-1}))$ and checks the test (3.4),

$$\langle\gamma F(a),a-b\rangle+\omega(z_{t-1})+\langle\omega'(z_{t-1}),b-z_{t-1}\rangle-\omega(b)\le0,$$

for $(a,b)=(z_{t-1},w_{t,1})$. If the test passes, $w_t=z_{t-1}$ and $z_t=w_{t,1}$. Otherwise $w_t=w_{t,1}$ and $z_t=P_{z_{t-1}}(\gamma F(w_{t,1}))$. The output after $N$ steps is the average $z^N=\frac1N\sum_{t=1}^Nw_t$ of the points $w_t$.

Formalization targets

Goal: Theorem 3.2 (p. 239), variational-inequality form

For every run of the basic implementation, (3.4) holds at every step, so two inner iterations always suffice, and for every $N\ge1$

$$\epsilon(z^N)\le\frac{\sqrt2\,\Theta(z_0)\,L}{\alpha N}.\tag{3.9}$$

Milestones, in the order of the proof

1. Lemma 2.1 (2.5), p. 232: $H_u(P_z(\xi))-H_u(z)\le\langle\xi,u-P_z(\xi)\rangle+[\omega(z)+\langle\omega'(z),P_z(\xi)-z\rangle-\omega(P_z(\xi))]$, and the bracket is $\le0$. Here $H_u(z)=\Omega(\omega'(z))-\langle\omega'(z),u\rangle$ and $\Omega$ is the Legendre transform of $\omega|_Z$.
2. (2.15), p. 235: one step of the relaxed conceptual prox-method satisfies $\langle\gamma_tF(w_t),w_t-u\rangle\le H_u(z_{t-1})-H_u(z_t)+\epsilon_t$.
3. Proposition 2.2(ii), p. 234: $\epsilon(z^N)\le(\Theta(z_0)+\sum_t\epsilon_t)/\sum_t\gamma_t$ for the relaxed method (2.11).
4. Lemma 3.1 (3.7.a), p. 238: $\|w-z_+\|\le\alpha^{-1}\gamma\|\xi-\eta\|_*$.
5. Lemma 3.1 (3.7.c), p. 238: $\delta\le\epsilon$.
6. Lemma 3.1 (3.7.d), p. 238: $\epsilon\le\alpha^{-1}\gamma^2\|\xi-\eta\|_*^2-\frac\alpha2[\|w-z\|^2+\|w-z_+\|^2]$.
7. The display of the proof of Theorem 3.2, p. 239: with $\gamma=\alpha/(\sqrt2L)$, the second inner iterate always passes (3.4).

Lemma 2.1 (2.4), Lemma 3.1 (3.7.b) and Remark 2.3 are also stated as companion theorems.

Significance

The theorem gives an $O(1/N)$ bound for monotone Lipschitz v.i. and for smooth convex–concave saddle points at a cost of two operator evaluations and two prox problems per step. With a distance-generating function adapted to $Z$, the paper derives rates that are, in its words, nearly dimension-independent under favorable circumstances, for matrix games, eigenvalue minimization and the Lovász capacity number (§5). In the Euclidean case $\omega=\frac12\|\cdot\|_2^2$ the method is Korpelevich's extragradient method, so the theorem also gives an ergodic $O(1/N)$ rate for that method.

The result is proved in the paper; no machine-checked proof of it is known. The platform has a formalized statement of mirror prox for minimization of a smooth convex function (Bubeck's Theorem 4.4), which uses a mirror map on an open set and a function-value gap. It does not cover operators, the v.i. accuracy measure or a prox-mapping over a compact set. This mission produces the general v.i. version, with an arbitrary norm and a distance-generating function defined only on $Z$.

Difficulty

The algebra of each step is short. The work is in three places. First, the first-order optimality conditions of the constrained prox problems, (2.6) and (3.8), must be derived when $\omega'$ is only a derivative within $Z$, and $Z$ may have empty interior. Second, (3.7.d) needs the function-value form of strong convexity, $\omega(w)\ge\omega(z)+\langle\omega'(z),w-z\rangle+\frac\alpha2\|w-z\|^2$, which must be derived from the monotonicity form (2.2) along segments of $Z$. Third, the telescoping of (2.15) uses the identity $\Omega(\omega'(z))=\langle\omega'(z),z\rangle-\omega(z)$ for $z\in Z$, and the passage from the weighted sum to the average uses monotonicity of $F$.

The natural first idea is to prove that the inner map $w\mapsto P_z(\gamma F(w))$ is a contraction, observation (3.1), and iterate it to a fixed point. That gives only a geometric number of inner steps, not two. The two-step bound comes from Lemma 3.1, which decouples the two prox steps and compares them through strong convexity.

Formalization scope

Dual vectors are continuous linear functionals E →L[ℝ] ℝ on a finite-dimensional normed space E, and $\|\cdot\|_*$ is the operator norm. This is equivalent to the paper's Euclidean space with a second norm. $Z$ is assumed convex, compact and nonempty in every item. $\omega$ has a derivative within $Z$ that is continuous on $Z$, and (2.2) is assumed in the monotonicity form. The prox-mapping is the relation "$v\in U$ minimizes $\omega(y)+\langle\xi-\omega'(z),y\rangle$ over $U$". $\Omega$ and $\Theta$ are suprema over the image of $Z$, which are maxima under these assumptions. The paper's indices are kept: z 0 is $z_0$, and step $t+1$ goes from z t to w (t+1) and z (t+1).

Disclosed choices: $L>0$ and $N\ge1$ are hypotheses, because (3.2) and (3.9) divide by them. The termination test (2.8) is not modelled, so runs never stop; this only adds runs. The basic implementation's inner loop is cut at $s=2$, which is what the goal's first claim justifies. The bound on $\epsilon(z^N)$ is stated for every $u\in Z$, which is equivalent to the bound on the maximum. Items that use only monotonicity of $F$, or no property of $F$, do not assume the rest of (2.1).

The goal quantifies over every run, and a sorry-free sanity file exhibits a run on $Z=[0,1]$, so the run relation is not empty. The average is over the $w_t$, not the $z_t$. The suprema are taken over compact nonempty $Z$ with continuous $\omega$, so they are not junk values. The saddle-point form (3.10), the bound (2.14) and Theorems 4.1–4.2 are not posed.

Useful contributions: optimality conditions for minimizers of functions differentiable within a convex set; the function-value form of strong convexity derived from (2.2); and the Legendre-transform identity. All three are reusable for other mirror-descent and prox-method analyses.

Selected references

• A. Nemirovski, Prox-Method with Rate of Convergence O(1/t) for Variational Inequalities with Lipschitz Continuous Monotone Operators and Smooth Convex-Concave Saddle Point Problems, SIAM J. Optim. 15(1):229–251, 2004. https://doi.org/10.1137/S1052623403425629
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12:747–756, 1976.
• Yu. Nesterov, Dual extrapolation and its applications to solving variational inequalities and related problems, Math. Program. 109:319–344, 2007. https://doi.org/10.1007/s10107-006-0034-z
• A. Juditsky, A. Nemirovski, C. Tauvel, Solving variational inequalities with stochastic mirror-prox algorithm, Stochastic Systems 1(1):17–58, 2011. https://doi.org/10.1214/10-SSY011
• S. Bubeck, Convex Optimization: Algorithms and Complexity, Found. Trends Mach. Learn. 8(3–4):231–357, 2015, §4.5. https://doi.org/10.1561/2200000050

Motivation

A retailer that carries several substitutable products, such as brands of the same item, loses part of a customer's demand when the preferred product is out of stock, but not all of it: some customers buy another product instead. How much of each product to stock then depends on the stocking levels of the others. When all products are managed by one company, the stocking problem is a joint optimization; when each product is managed by a separate firm, it is a game, and each firm ignores the effect of its stock-outs on its competitors.

A common view in the inventory literature is that competition drives inventories up for every product. Mahajan and van Ryzin and Lippman and McCardle demonstrated it in special cases (Lippman & McCardle, Operations Research 1997; Mahajan & van Ryzin, Columbia working paper 1999, published in Operations Research 2001). Netessine and Rudi (SSRN 303779, 2002, later published in Operations Research, 2003) study the general model with $n$ products, an arbitrary continuous joint demand distribution, and arbitrary substitution fractions. They show that the common view fails in general: some products may be stocked more under centralized management (Proposition 6(i)), but at least one product is always stocked no less under competition (Proposition 6(ii)). This mission formalizes Proposition 6(ii) and the centralized first-order analysis on which it rests.

Setting

There are $n \ge 1$ products, indexed $i = 1,\dots,n$, sold in a single period. Product $i$ is stocked at $Q_i \ge 0$ units at unit cost $c_i$, sold at unit price $r_i$, and salvaged at unit value $s_i$, with $r_i > c_i > s_i > 0$. Write $u_i = r_i - c_i$ (the underage cost) and $o_i = c_i - s_i$ (the overage cost).

The first-choice demand vector $D = (D_1,\dots,D_n)$ is random, with a known continuous joint law on the positive orthant. A fraction $a_{ij} \in [0,1]$ of the unmet demand for product $i$ switches to product $j$, with $a_{ii} = 0$ and $\sum_j a_{ij} < 1$; a customer whose second choice is also out of stock is lost. The effective demand for product $i$ is

$$D^s_i = D_i + \sum_{j \ne i} a_{ji}\,(D_j - Q_j)^+, \qquad x^+ = \max(0,x).$$

Under centralized management a single company maximizes the expected profit

$$\pi(Q) = \mathbb E \sum_i \Big[r_i \min(D^s_i, Q_i) - c_i Q_i + s_i (Q_i - D^s_i)^+\Big]$$

over all $Q \ge 0$; a maximizer is written $Q^c$. Under competition firm $i$ chooses $Q_i \ge 0$ to maximize

$$\pi_i(Q) = \mathbb E\big[u_i D^s_i - u_i (D^s_i - Q_i)^+ - o_i (Q_i - D^s_i)^+\big],$$

given the other firms' quantities; a Nash equilibrium $Q^d \ge 0$ is a vector at which no firm gains by changing its own quantity. In the Lean development these objects are Model, Ds, centralProfit, IsCentralOptimal, firmProfit, IsBestResponse and IsNash in the namespace DemandSubstitution.Comparison.

Formalization targets

Goal: Proposition 6(ii)

For every optimal centralized stocking vector $Q^c$ and every Nash equilibrium $Q^d$,

$$\exists\, i:\quad Q^c_i \le Q^d_i .$$

The statement quantifies over all optima and all equilibria; it asserts neither existence nor uniqueness of either.

Milestones

1. The underage/overage form (1): $\pi = \mathbb E\sum_i [u_i D^s_i - u_i (D^s_i - Q_i)^+ - o_i (Q_i - D^s_i)^+]$.
2. The derivative of one substitution term: for $j \ne i$, $\partial\,\mathbb E(D^s_j - Q_j)^+/\partial Q_i = -a_{ij}\Pr(D^s_j > Q_j, D_i > Q_i)$.
3. The partial derivative (8) of $\pi$ with respect to $Q_i$.
4. Proposition 1, the centralized optimality condition (7):

$$\Pr(D_i < Q^c_i) - \Pr(D_i < Q^c_i < D^s_i) + \sum_{j\ne i}\frac{u_j+o_j}{u_i+o_i}\,a_{ij}\Pr(D^s_j < Q^c_j, D_i > Q^c_i) = \frac{u_i}{u_i+o_i}.$$

5. The comparison $\Pr(D^{sc}_i < Q^c_i) \le \Pr(D^{sd}_i < Q^d_i)$, where $D^{sc}$ and $D^{sd}$ are the effective demands at $Q^c$ and $Q^d$.

Significance

Proposition 6(ii) bounds how far competition can depart from the centralized solution in the downward direction: it can never make every product understocked. Together with Proposition 6(i), it shows that neither "competition overstocks everything" nor its opposite holds in general, and it is the step from which the symmetric case, Proposition 6(iii) (every product is stocked at least as much under competition), follows. The centralized condition (7) and the derivative (8) are of independent use: they give the first-order conditions of the multi-product newsvendor with stock-out substitution for an arbitrary number of products and an arbitrary continuous demand law, obtained without Leibniz-rule integration over polyhedral regions.

The results are proved in the paper; none of them has a machine-checked proof. A formal proof requires differentiating an expectation of piecewise-linear functions of the demand under the integral sign, and handling the measure-zero boundaries where those functions have kinks. That machinery is reusable for other multi-product newsvendor models.

Difficulty

The centralized profit is not concave in general for three or more products (the paper's own example, pp. 3–5), so the optimum cannot be characterized as the unique solution of first-order conditions: the argument must work with an arbitrary maximizer and use only the necessary condition at an interior coordinate. The derivative (8) must be justified as a two-sided derivative of an integral whose integrand is not differentiable on hyperplanes in demand space; the paper's difference quotient argument leaves the boundary terms implicit. Finally, the obvious comparison of the two first-order conditions yields only an inequality between probabilities; turning it into an inequality between stocking levels requires the distribution function of $D^s_i$ to be strictly increasing, and an optimal $Q^c_i$ may be zero, where (7) does not hold.

Formalization scope

Products are Fin n (0-based). The model data and the standing assumptions $r_i > c_i > s_i > 0$, $a_{ij} \in [0,1]$, $a_{ii} = 0$, $\sum_j a_{ij} < 1$ are fields of a structure Model n. The demand law is a probability measure $\mu$ on $\mathbb R^n$ that is absolutely continuous with respect to Lebesgue measure, is concentrated on the open positive orthant, and has integrable coordinates (IsDemandLaw). Expectations are Bochner integrals and probabilities are μ.real of sets with the strict and weak inequalities exactly as printed. Derivatives are two-sided HasDerivAt in one coordinate, the others held fixed through Function.update.

Three hypotheses are pinned relative to the page and disclosed in the statements:

• NeZero n in the goal: for $n = 0$ "at least one $i$" is false.
• HasPositiveDensity μ in the goal: a Lebesgue density strictly positive on the open positive orthant. The paper's last step uses strict monotonicity of the distribution function of $D^s_i$ without stating it.
• $Q^c_i > 0$ in Proposition 1 and in the probability comparison: (7) is an equality only at an interior coordinate. The goal carries no such hypothesis.

The centralized optimum is a maximizer of $\pi$ over nonnegative vectors and the Nash equilibrium is the no-profitable-deviation property over nonnegative quantities. Defining either by its first-order condition ((7) or (10)) would turn the propositions into definitions and is ruled out. Stating the goal for one chosen optimum or equilibrium is ruled out as well: it holds for every pair.

Contributions welcome: differentiation of expectations of piecewise-linear functions under absolutely continuous laws; null-set lemmas for $\{D^s_j = Q_j\}$; Fermat's rule at a coordinate-wise interior maximizer; the Nash condition (10) of the competitive game, which milestone 5 needs and which is also posed in the companion mission on equilibrium existence.

Selected references

• S. Netessine and N. Rudi, Centralized and Competitive Inventory Models with Demand Substitution, Simon School Working Paper OP 02-01, University of Rochester, April 2002, SSRN 303779. https://doi.org/10.2139/ssrn.303779 (journal version: Operations Research 51(2), 2003; this mission cites the working paper's numbering)
• S. A. Lippman and K. F. McCardle, The competitive newsboy, Operations Research 45(1), 54–65, 1997.
• S. Mahajan and G. van Ryzin, Inventory competition under dynamic consumer choice, Columbia University working paper, 1999 (cited by Netessine & Rudi as [8]); published in Operations Research, 2001.

Motivation

Obstacle problems, contact problems and control-constrained optimal control problems lead, after discretization, to complementarity systems of the form "find $y \le \psi$ and $\lambda \ge 0$ with $Ay + \lambda = f$ and $\lambda_i(y_i - \psi_i) = 0$". The primal-dual active set strategy solves such systems by guessing which constraints are active, solving one linear system, and updating the guess. It is widely used because each iteration is a single linear solve and, in practice, it terminates after few iterations.

Hintermüller, Ito and Kunisch (SIAM J. Optim. 13(3), 2002; authors' version hal-01660511v1) showed that the strategy is a semismooth Newton method applied to a reformulation of the complementarity system with a max-function. This gives local superlinear convergence. For global convergence, from arbitrary initial data, the paper gives three sufficient conditions on the matrix $A$: the M-matrix case (Theorem 3.2), the condition of Theorem 3.3 treated in this mission, and small perturbations of M-matrices (Theorem 3.4). Theorem 3.3 is the one that goes beyond sign patterns: it covers P-matrices whose blocks satisfy a norm bound and a cone condition, with the sum of the components of $y$ serving as a merit function.

Setting

Fix $n \ge 0$, a matrix $A \in \mathbb{R}^{n \times n}$, vectors $f, \psi \in \mathbb{R}^n$ and a parameter $c > 0$. Vectors are ordered componentwise. The problem is

$$Ay + \lambda = f, \qquad \lambda - \max\big(0, \lambda + c(y - \psi)\big) = 0, \tag{3.1}$$

with the maximum taken componentwise. In the paper's notation the matrix is $A$ and the index sets are calligraphic: $\mathcal{A}$ (active) and $\mathcal{I}$ (inactive).

A P-matrix is a square matrix all of whose principal minors are positive. For an index set $\mathcal{I} \subseteq \{1,\dots,n\}$ with complement $\mathcal{A}$, $A_{\mathcal{I}}$ is the principal submatrix of $A$ on $\mathcal{I}$, and $A_{\mathcal{I}\mathcal{A}}$ is the submatrix with rows in $\mathcal{I}$ and columns in $\mathcal{A}$. For a P-matrix every $A_{\mathcal{I}}$ is invertible.

The primal-dual active set algorithm starts from an arbitrary pair $(y^0, \lambda^0)$. Given $(y^k, \lambda^k)$ it sets

$$\mathcal{A}_k = \{ i : \lambda^k_i + c(y^k_i - \psi_i) > 0 \}, \qquad \mathcal{I}_k = \{ i : \lambda^k_i + c(y^k_i - \psi_i) \le 0 \},$$

and determines $(y^{k+1}, \lambda^{k+1})$ from

$$Ay^{k+1} + \lambda^{k+1} = f, \qquad y^{k+1} = \psi \text{ on } \mathcal{A}_k, \qquad \lambda^{k+1} = 0 \text{ on } \mathcal{I}_k .$$

For a rectangular matrix $B$, $B_+$ is the matrix of the positive parts $\max(0, b_{ij})$ of its entries, and $\|\cdot\|_1$ is the matrix norm subordinate to the one-norms, i.e. the maximal absolute column sum. Thus $\|B_+\|_1 = \max_j \sum_i \max(0, b_{ij})$.

Formalization targets

Goal: Theorem 3.3

If $A$ is a P-matrix and for every partition of $\{1, \dots, n\}$ into disjoint sets $\mathcal{I}$ and $\mathcal{A}$

$$\big\|(A_{\mathcal{I}}^{-1} A_{\mathcal{I}\mathcal{A}})_+\big\|_1 < 1 \qquad\text{and}\qquad \sum_{i \in \mathcal{I}} (A_{\mathcal{I}}^{-1} v)_i \ge 0 \ \text{ for all } v \ge 0,$$

then for every solution $x^* = (y^*, \lambda^*)$ of (3.1) and every run of the algorithm, $x^k = (y^k, \lambda^k) \to x^*$.

Milestones

The proof in the paper passes through the following claims, in order: the sign facts $\lambda^k_{\mathcal{I}_k} \le 0$ and $y^k_{\mathcal{A}_k} \ge \psi_{\mathcal{A}_k}$ for $k \ge 1$; the update formula on the inactive set derived from the Newton system (3.3); inequality (3.6); inequality (3.7),

$$\sum_{i=1}^n (y^{k+1}_i - y^k_i) \le -\|y^k - \psi\|_{1,\mathcal{A}_k} + \big\|(A_{\mathcal{I}_k}^{-1} A_{\mathcal{I}_k\mathcal{A}_k})_+\big\|_1 \, \|y^k - \psi\|_{1,\mathcal{A}_k};$$

and the fact that a repeated active set yields a solution of (3.1).

Companion statements

Existence of a run from every initial pair when $A$ is a P-matrix; Remark 3.3 (an M-matrix satisfies the conditions of Theorem 3.3); and the stronger conclusion of the proof, that every run reaches $x^*$ after finitely many steps.

Significance

Theorem 3.3 gives global convergence of the primal-dual active set strategy for a class of matrices that is not restricted to M-matrices, and identifies $\mathcal{M}(y) = \sum_i y_i$ as a merit function under its two conditions. The paper points out that the result applies to discretizations of control-constrained optimal control problems, where the system matrix is generally not an M-matrix, and Remark 3.3 shows that the M-matrix case falls under it.

The result is proved on paper; none of it has been machine-checked. A formal development would produce a checked global convergence theorem for a semismooth Newton method, together with reusable statements about principal blocks of P-matrices and the subordinate one-norm of a positive part. The step from "the merit function does not increase" to convergence is the part of the paper's argument that a formal proof has to make fully precise (see below).

Difficulty

The obvious route is the paper's: show that $\sum_i y^k_i$ decreases strictly until the active set repeats, conclude that no active set can recur, and use finiteness of the set of possible active sets. The inequalities (3.6) and (3.7) give only a non-strict decrease. The paper's assertion "$< 0$, unless $y^{k+1} = y^k$" does not follow from them as written: the right-hand side of (3.7) vanishes when $y^k = \psi$ on $\mathcal{A}_k$, and the cone condition permits $\sum_{i \in \mathcal{I}} (A_{\mathcal{I}}^{-1}\lambda^k_{\mathcal{I}})_i = 0$ with $\lambda^k_{\mathcal{I}} \neq 0$. A complete proof has to exclude cycling among active sets at equal merit value by a further argument. That is the central difficulty of this mission, and the reason the strict part of (3.7) is not stated as a milestone.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ; index sets are Finset (Fin n) and blocks are submatrices along the subtype inclusion. The P-matrix predicate is the published definition RobinsonSR.Schur.IsPMatrix (every nonempty principal minor is positive). The algorithm is encoded as a relation between consecutive iterates, and a run is an infinite sequence related step by step with arbitrary initial data; the stopping option of the algorithm is not modelled. The solution of (3.1) enters as a hypothesis: for a P-matrix it exists and is unique, so no assumption beyond the paper is made. Convergence is convergence of $(y^k, \lambda^k)$ in $\mathbb{R}^n \times \mathbb{R}^n$. The parameter $c > 0$ is the paper's standing assumption.

Conventions committed to:

• both conditions of Theorem 3.3 range over every index set, including $\mathcal{I} = \emptyset$ and $\mathcal{I} = \{1,\dots,n\}$;
• $\|B_+\|_1$ is the maximal column sum of the positive part, computed as a supremum in $\mathbb{R}_{\ge 0}$, and equals $0$ for a matrix with no columns;
• the cone condition is $\sum_{i\in\mathcal{I}}(A_{\mathcal{I}}^{-1}v)_i \ge 0$ for $v \ge 0$, not entrywise nonnegativity of $A_{\mathcal{I}}^{-1}$;
• the milestones on the iterates hold from $k = 1$ on, as in the paper.

The goal does not assume a decrease of the merit function or finite termination; a formalization that adds either as a hypothesis would be trivial and is ruled out. The run-existence companion shows that the hypothesis "let $(y^k,\lambda^k)$ be a run" can be met, so the goal is not vacuous.

A complete development needs: invertibility of principal blocks of a P-matrix, the block form of one step, the elementary estimate of $\sum_i (B x)_i$ by $\|B_+\|_1 \sum_j x_j$ for $x \ge 0$, and an argument that excludes cycling. Proofs of any milestone, of the companion statements, or of the goal through an argument other than the paper's are welcome.

Selected references

• M. Hintermüller, K. Ito, K. Kunisch, The primal-dual active set strategy as a semismooth Newton method, SIAM J. Optim. 13(3):865–888, 2002. https://doi.org/10.1137/S1052623401383558 ; authors' version https://hal.science/hal-01660511v1
• A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, Academic Press, 1979 (SIAM Classics reprint 1994). https://doi.org/10.1137/1.9781611971262