Optimization

Motivation

A mathematical program with complementarity constraints (MPCC, also called MPEC, mathematical program with equilibrium constraints) is a nonlinear optimization problem in which some pairs of constraint functions must be nonnegative with at least one of each pair equal to zero. Such constraints model equilibria inside an optimization problem: bilevel programs whose lower level is replaced by its optimality conditions, Stackelberg games, traffic and electricity market equilibria, contact problems in mechanics. See Luo, Pang and Ralph, Mathematical Programs with Equilibrium Constraints (Cambridge University Press, 1996), doi:10.1017/CBO9780511983658.

The complementarity constraints make the standard theory fail. At every feasible point the Mangasarian–Fromovitz constraint qualification is violated, so the Karush–Kuhn–Tucker conditions are not necessary for optimality, and standard NLP solvers lose their convergence guarantees. A common remedy is relaxation: replace the MPEC by a family of ordinary nonlinear programs depending on a parameter $t>0$, solve them for $t\downarrow0$, and study the limits of their stationary points.

The first relaxation scheme, and the reference point for all later ones, is due to Scholtes (Convergence properties of a regularization scheme for mathematical programs with complementarity constraints, SIAM J. Optim. 11 (2001), doi:10.1137/S1052623499361233). Scholtes showed that limits of stationary points of the relaxed programs are C-stationary when MPEC-LICQ holds at the limit. Hoheisel, Kanzow and Schwartz (Preprint 299, University of Würzburg, 2010; later Math. Program. 137 (2013), doi:10.1007/s10107-011-0488-5) compare five relaxation schemes and weaken the constraint qualification in each convergence theorem. For Scholtes' scheme, their Theorem 3.1 replaces MPEC-LICQ by the weaker MPEC-MFCQ. This mission formalizes that theorem.

Setting

The MPEC (1) is

$$\min f(x)\ \ \text{s.t.}\ \ g_i(x)\le0\ (i\le m),\ \ h_i(x)=0\ (i\le p),\ \ G_i(x)\ge0,\ \ H_i(x)\ge0,\ \ G_i(x)H_i(x)=0\ (i\le l),$$

with continuously differentiable $f,g_i,h_i,G_i,H_i:\mathbb R^n\to\mathbb R$ and feasible set $X$. For a point $x^*$ the paper uses the index sets $I_g=\{i\mid g_i(x^*)=0\}$, $I_{0+}=\{i\mid G_i(x^*)=0<H_i(x^*)\}$, $I_{00}=\{i\mid G_i(x^*)=H_i(x^*)=0\}$ and $I_{+0}=\{i\mid G_i(x^*)>0=H_i(x^*)\}$.

A standard nonlinear program has constraints $g_i\le0$, $h_j=0$. Its point $x$ satisfies the Mangasarian–Fromovitz constraint qualification (MFCQ) if the gradients $\nabla h_j(x)$ are linearly independent and some direction $d$ has $\nabla g_i(x)^Td<0$ for all active $i$ and $\nabla h_j(x)^Td=0$ for all $j$. A stationary point is the $x$-part of a KKT point: $x$ is feasible and there are $\lambda\ge0$, $\mu$ with $\lambda_ig_i(x)=0$ and $\nabla f(x)+\sum\lambda_i\nabla g_i(x)+\sum\mu_j\nabla h_j(x)=0$.

The tightened program TNLP$(x^*)$ keeps $g_i\le0$, $h_i=0$ and imposes $G_i=0,\ H_i\ge0$ on $I_{0+}$, $G_i\ge0,\ H_i=0$ on $I_{+0}$, and $G_i=H_i=0$ on $I_{00}$. MPEC-MFCQ holds at $x^*$ if MFCQ holds at $x^*$ for TNLP$(x^*)$.

A feasible $x^*$ is weakly stationary if there are multipliers $\lambda\in\mathbb R^m$, $\mu\in\mathbb R^p$, $\gamma,\nu\in\mathbb R^l$ with

$$\nabla f(x^*)+\sum_{i=1}^m\lambda_i\nabla g_i(x^*)+\sum_{i=1}^p\mu_i\nabla h_i(x^*)-\sum_{i=1}^l\gamma_i\nabla G_i(x^*)-\sum_{i=1}^l\nu_i\nabla H_i(x^*)=0,$$

$\lambda\ge0$, $\lambda_ig_i(x^*)=0$, $\gamma_i=0$ on $I_{+0}$ and $\nu_i=0$ on $I_{0+}$. It is C-stationary if such multipliers can be chosen with, in addition, $\gamma_i\nu_i\ge0$ for all $i\in I_{00}$.

Scholtes' relaxed program $R^S(t)$ replaces $G_i(x)H_i(x)=0$ by $G_i(x)H_i(x)\le t$ and keeps all other constraints of (1). The notation $\{t_k\}\downarrow0$ means a sequence of positive parameters decreasing to $0$.

Formalization targets

Goal: Theorem 3.1

Let $\{t_k\}\downarrow0$, let $x^k$ be a stationary point of $R^S(t_k)$, and let $x^k\to x^*$ with MPEC-MFCQ at $x^*$. Then

$$x^*\ \text{is a C-stationary point of the MPEC (1).}$$

No feasibility of $x^*$ is assumed; it is part of the conclusion.

Milestones

1. Remark 2.2: for a feasible point of a standard NLP, MFCQ holds if and only if the active inequality gradients together with all equality gradients are positive-linearly independent.
2. §2.2, pp. 6–7: MPEC-MFCQ written out explicitly, i.e. linear independence of $\nabla h_i$, $\nabla G_i$ ($I_{00}\cup I_{0+}$) and $\nabla H_i$ ($I_{00}\cup I_{+0}$), plus a direction $d$.
3. Proof of Theorem 3.2, p. 11: MPEC-MFCQ implies positive-linear independence of $\{\nabla g_i(x^*)\}_{I_g}\cup\{\{\nabla h_i\}\cup\{\nabla G_i\}_{I_{00}\cup I_{0+}}\cup\{\nabla H_i\}_{I_{00}\cup I_{+0}}\}$.
4. Proof of Theorem 3.1, p. 9: for large $k$, $I_g(x^k)\subseteq I_g$, $I_G(x^k)\subseteq I_{00}\cup I_{0+}$, $I_H(x^k)\subseteq I_{00}\cup I_{+0}$.
5. Proof of Theorem 3.1, pp. 10–11: under the goal's hypotheses, $x^*$ is weakly stationary.

Significance

Theorem 3.1 says that Scholtes' scheme, run to the limit, produces C-stationary points under a constraint qualification strictly weaker than the one in Scholtes' original result. MPEC-MFCQ is the natural assumption here: under it the KKT multipliers of the relaxed programs need not converge, and the theorem shows that a convergent subsequence of suitably modified multipliers still exists. The result is the first of a family of convergence theorems in the paper (the schemes of Lin–Fukushima, Kadrani–Dussault–Benchakroun and Steffensen–Ulbrich follow the same pattern) and the baseline against which those schemes are compared.

The theorem is proved in the paper; it is not open. To the extent a search of the Prove2Me catalog shows, no MPEC stationarity concept, MPEC constraint qualification or relaxation result has been formalized there, and Mathlib has no theory of constraint qualifications for nonlinear programs. The mission produces a machine-checked proof of Theorem 3.1 and, along the way, reusable statements of Definition 2.1, MFCQ, KKT points and the MFCQ/positive-linear-independence equivalence for general nonlinear programs.

Difficulty

The obvious argument takes a limit of the KKT multipliers of $R^S(t_k)$. That fails twice. First, under MPEC-MFCQ the multiplier sequence need not be bounded, so there may be nothing to take a limit of; boundedness has to be recovered from MPEC-MFCQ through positive-linear independence, a theorem of the alternative. Second, the multiplier $\delta^k$ of the product constraint $G_iH_i\le t_k$ multiplies $H_i\nabla G_i+G_i\nabla H_i$, which is not a multiplier of $\nabla G_i$ or $\nabla H_i$ alone; how it is redistributed depends on whether $i$ lies in $I_{0+}$, $I_{+0}$ or $I_{00}$, and the sign condition on $I_{00}$ comes from the support disjointness between $\delta^k$ and the multipliers of $G_i\ge0$, $H_i\ge0$, which uses $t_k>0$. Compactness, index-set bookkeeping along a subsequence and continuity of all gradients have to be combined.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), gradients are Mathlib's gradient, and $\nabla g(x)^Td$ is the inner product. Constraint indices are Fin m, Fin p, Fin l (0-based); $m,p,l$ may be $0$.
• The paper's standing assumption that all data are continuously differentiable (p. 1) is the explicit hypothesis P.IsC1 (ContDiff ℝ 1 for each function) of the goal and of milestones 4 and 5. Milestones 1–3 are pointwise linear algebra and assume no smoothness.
• "Stationary point of $R^S(t_k)$" is a KKT point of $R^S(t_k)$ viewed as a standard NLP with inequality constraints $g_i\le0$, $-G_i\le0$, $-H_i\le0$, $G_iH_i-t\le0$: feasibility, nonnegative multipliers and complementary slackness are included (p. 5).
• "$\{t_k\}\downarrow0$" is $t_k>0$ for all $k$, $(t_k)$ nonincreasing, and $t_k\to0$.
• Families of gradients are indexed families (repeated vectors count as dependent); in MPEC-MFCQ an index of $I_{00}$ contributes both $\nabla G_i$ and $\nabla H_i$. TNLP$(x^*)$ has constraints indexed by subtypes of the index sets; absent constraints are not padded by zero functions, which would make MPEC-MFCQ fail everywhere.
• Definition 2.3(a) is printed with two misprints ("$\mu_ih_i(x^*)$", "$i=1,\dots,l$" for the complementarity of $\lambda$); the formalization uses $\mu_i\nabla h_i(x^*)$ and $i=1,\dots,m$. C-stationarity requires feasibility and one multiplier tuple satisfying both the weak-stationarity conditions and the sign condition on $I_{00}$.
• A "stationary point" that is merely a feasible point or a critical point of $f$, or a C-stationarity whose sign condition refers to multipliers other than those of the weak-stationarity equation, would make the goal false or empty; neither reading is used. The hypotheses of the goal are jointly satisfiable (checked on the paper's Example 3.6 instance).
• Infrastructure needed: theorems of the alternative (Motzkin/Farkas) for finite families in $\mathbb R^n$, compactness of normalised multiplier sequences, continuity of gradients of $C^1$ maps. The NLP layer (positive-linear dependence, MFCQ, KKT points, Remark 2.2) is reusable for any constraint-qualification development. Contributions of proofs of the milestones, of general NLP lemmas, and of the goal are welcome.

Selected references

• T. Hoheisel, C. Kanzow, A. Schwartz, Theoretical and numerical comparison of relaxation methods for mathematical programs with complementarity constraints, Preprint 299, Institute of Mathematics, University of Würzburg, September 2010; published in Math. Program. 137 (2013) 257–288. doi:10.1007/s10107-011-0488-5
• S. Scholtes, Convergence properties of a regularization scheme for mathematical programs with complementarity constraints, SIAM J. Optim. 11 (2001) 918–936. doi:10.1137/S1052623499361233
• Z.-Q. Luo, J.-S. Pang, D. Ralph, Mathematical Programs with Equilibrium Constraints, Cambridge University Press, 1996. doi:10.1017/CBO9780511983658

Motivation

The capacitated vehicle routing problem (CVRP) asks for $K$ delivery routes from a depot that serve every client exactly once without exceeding a vehicle capacity, at minimum total length. It was introduced by Dantzig and Ramser in 1959 and is the reference problem of the vehicle routing literature: most exact methods for richer routing models (time windows, heterogeneous fleets, split deliveries) are first developed and benchmarked on it.

Exact CVRP algorithms are driven by the lower bound of a linear relaxation. Two families dominated before 2005. Branch-and-cut works with the edge variables $x_e$ and the rounded capacity inequalities (Lysgaard, Letchford and Eglese 2004, among others); its bound degrades as the number of vehicles grows. Lagrangean and column-generation methods work with q-routes, walks from the depot of bounded total demand that may revisit clients (Christofides, Mingozzi and Toth 1981). Fukasawa, Longo, Lysgaard, Poggi de Aragão, Reis, Uchoa and Werneck combine the two in one linear program over the intersection of the two polytopes, priced by column generation with every cut written on the edge variables. According to the abstract, the resulting branch-and-cut-and-price solves to optimality all instances from the literature with up to 135 vertices. The design is called robust because cuts are written on the edge variables $x$ and therefore never change the structure of the pricing problem.

This mission formalizes the formulation itself (§2 of the paper) and the two exact facts of its column generation (§3.1).

Setting

Let $G=(V,E)$ be an undirected graph on $V=\{0,1,\dots,n\}$. Vertex $0$ is the depot; $V_+=\{1,\dots,n\}$ are the clients, client $i$ having a positive demand $d_i$. Each edge has a length $\ell_e$. There are $K$ vehicles of capacity $C$, both positive integers.

A list of clients $r=(r_1,\dots,r_m)$ describes the closed walk $0\to r_1\to\cdots\to r_m\to 0$. Its edge incidence $q^e(r)$ is the number of times the walk traverses $e$ (a one-client walk $0\to j\to 0$ traverses $\{0,j\}$ twice); its load is $d_{r_1}+\cdots+d_{r_m}$, with repetitions.

• A CVRP route visits pairwise distinct clients with load at most $C$; a CVRP solution is a family $R=(R_1,\dots,R_K)$ of routes visiting every client exactly once. Its edge vector is $\chi(R)_e=\sum_kq^e(R_k)$.
• A q-route without 2-cycles is a walk of load at most $C$ that may revisit clients but contains no subpath $i\to j\to i$ with $i\ne 0$.

For $S\subseteq V$, $\delta(S)$ is the set of edges with one end in $S$, $x(\delta(S))=\sum_{e\in\delta(S)}x_e$, and $k(S)=\lceil d(S)/C\rceil$. The paper's constraints on $x\in\mathbb R^{E}$ and on weights $\lambda_j\ge 0$ of the q-routes $j$ are

$$\begin{aligned} &x(\delta(\{i\}))=2\ \ (i\in V_+)\ \ (1), && x(\delta(\{0\}))=2K\ \ (2), && x(\delta(S))\ge 2k(S)\ \ (S\subseteq V_+)\ \ (3),\\ &x_e\le 1\ \ (e\in E\setminus\delta(\{0\}))\ \ (4), && \textstyle\sum_jq^e_j\lambda_j=x_e\ \ (e\in E)\ \ (5), && \textstyle\sum_j\lambda_j=K\ \ (6). \end{aligned}$$

$P_1$ is $\{x\ge0:(1)\text{–}(4)\}$; $P_2$ is the set of $x\ge 0$ satisfying (1) together with some $\lambda\ge0$ satisfying (5), (6); the Explicit Master $P_3$ is the projection onto $x$ of the system (1)–(6) with one $\lambda$. The Dantzig–Wolfe Master (DWM) is the LP in $\lambda$ alone obtained by substituting (5) into (1)–(4), giving the rows (8)–(11), with objective (7) $\sum_j\sum_e\ell_eq^e_j\lambda_j$. The bounds are $L_i=\min_{x\in P_i}\ell^\top x$.

Formalization targets

Goal: the formulation theorem

For a loop-free graph with positive demands and capacity, and arbitrary lengths:

$$x\in P_3\cap\mathbb Z^{E}\iff x=\chi(R)\ \text{for a CVRP solution }R, \qquad P_3=\{Q\lambda:\lambda\ \text{DWM-feasible}\}, \qquad L_1,\,L_2\ \le\ L_3\ \le\ \mathrm{OPT},$$

with (7) equal to $\ell^\top Q\lambda$. The bounds are stated in lower-bound form: every lower bound of $\ell^\top x$ over $P_1$ or $P_2$ is one over $P_3$, and every lower bound over $P_3$ is at most the cost of every solution.

Milestones

1. $P_3=P_1\cap P_2$ (p. 5).
2. Every CVRP route is a q-route without 2-cycles (p. 2).
3. Validity of (1)–(4): $\chi(R)\in P_1$, with $\ell^\top\chi(R)$ the cost of $R$ (p. 4).
4. Validity of (5)–(6): $\chi(R)\in P_2$, with the routes of $R$ as columns (p. 4).
5. Every integer point of $P_1$ is $\chi(R)$ for a solution $R$ (p. 4).
6. Constraint (6) is implied by (2) and (5) (p. 5).
7. The DWM (8)–(11) is (1)–(4) on $x=Q\lambda$ (p. 5).
8. A generic cut $\sum_ea_ex_e\ge b$ becomes $\sum_j(\sum_ea_eq^e_j)\lambda_j\ge b$ (p. 5).
9. Every integer point of $P_2$ is $\chi(R)$ for a solution $R$ (p. 4).
10. The reduced cost of a column is $\sum_e\bar c_eq^e$ (§3.1, p. 6).
11. Scaling: a q-route for demands $\lceil d_v/g\rceil$ and capacity $\lfloor C/g\rfloor$ is a q-route for $(d,C)$ (§3.1, p. 7).

Significance

The formulation theorem is what makes the algorithm exact: integer points of $P_3$ are solutions, so branching on $x$ terminates at an optimum, and $P_3$ is a relaxation, so $L_3$ is a valid bound that dominates both classical bounds. The DWM description is what makes it computable: $P_3$ is optimized by column generation over q-routes, and milestones 8 and 10 show that any cut on $x$ can be added without changing the pricing problem, which remains a shortest q-route problem with edge costs $\bar c_e$.

The paper proves none of these claims formally; most are stated in a sentence, and milestone 9 is stated with "It can be shown" and no proof. To our knowledge none of them has a machine-checked proof. A formal development produces a library of walks, edge incidences, cut values and column families on a general graph that later missions on branch-cut-and-price (subset-row cuts, ng-routes, other routing variants) can import.

Difficulty

Most items are linear-algebra bookkeeping on finite sums, but they require a working theory of walks: edge incidences along a closed walk, the cut value of an incidence vector, and the fact that a walk from the depot crosses every client set an even number of times. The integrality statements (milestones 5 and 9 and goal part 1) are the hard part: an integer vector satisfying degree constraints need not come from routes through the depot, and the statements must exclude every other structure. For $P_2$ there are no capacity cuts at all, so the capacity of the routes must be recovered from the columns, and the paper states this case without proof. The obvious reduction "an integer point of $P_2$ is an integer combination of q-routes" fails: $\lambda$ may be fractional even when $x$ is integral.

Formalization scope

Vertices are Fin (n+1) with depot 0; edges are Sym2 (Fin (n+1)); the graph is an edge set E assumed loop-free where needed. Edge vectors are functions on all unordered pairs that vanish off E, which encodes $x\in\mathbb R^{|E|}$. Demands $d$, $K$ and $C$ are natural numbers; positive demands, $K>0$ and $C>0$ (the paper's standing assumptions, p. 1) are carried by the integrality statements and the goal, while $\ell\ge0$ is used by no statement and is omitted. Loads count repeated visits. The cut value $x(\delta(S))$, the demand $d(S)$ and $k(S)=\lceil d(S)/C\rceil$ are the published definitions LysgaardCVRP.Shrink.cut, .demand and .roundedCapacityBound. The matrix $Q$ is replaced by finitely supported weights on client lists ranging over all q-routes without 2-cycles. $L_1,L_2,L_3$ and OPT are never real infima, since $P_3$ is empty for infeasible instances.

Three trivializations are ruled out by construction: $P_3$ is defined from the Explicit Master display, not as $P_1\cap P_2$; a CVRP solution is defined by its routes, not as an integer point of a polytope; and the columns are not a fixed finite list, which would turn $P_2$ into a restricted master.

The strictness of "CVRP routes $\subsetneq$ q-routes" (p. 2) depends on the instance and is not stated. Contributions of reusable lemmas on walks and cut values of incidence vectors are welcome, as are proofs of any milestone.

Selected references

• R. Fukasawa, H. Longo, J. Lysgaard, M. Poggi de Aragão, M. Reis, E. Uchoa and R. F. Werneck, Robust branch-and-cut-and-price for the capacitated vehicle routing problem, Mathematical Programming 106 (2006); accepted manuscript. https://doi.org/10.1007/s10107-005-0644-x
• N. Christofides, A. Mingozzi and P. Toth, Exact algorithms for the vehicle routing problem, based on spanning tree and shortest path relaxations, Mathematical Programming 20 (1981). https://doi.org/10.1007/BF01589353
• J. Lysgaard, A. N. Letchford and R. W. Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Mathematical Programming 100 (2004). https://doi.org/10.1007/s10107-003-0481-8
• G. B. Dantzig and J. H. Ramser, The truck dispatching problem, Management Science 6 (1959). https://doi.org/10.1287/mnsc.6.1.80

Motivation

Firms that buy from unreliable suppliers have two broad ways to protect themselves against supply disruptions: dual sourcing, which splits the order between two suppliers so that a shortfall at one is cushioned by the other, and process improvement, which invests in a supplier's operations so that it fails less often. 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-period model in which the uncertainty is in the supplier's capacity, not in a proportional yield.

Real supply bases are rarely symmetric. Suppliers differ in cost, reliability and capacity because of their history or location, and the paper (p. 501) cites evidence that global sourcing has widened those differences. This mission formalizes the paper's analytical answer to one question this raises: as two otherwise identical suppliers drift apart in unit cost, which strategy gains? The paper's answer (Theorem 7, p. 502) is that the advantage of single sourcing with improvement over dual sourcing grows with the cost gap.

Setting

A firm sells one product over one season with unit revenue $r$, salvage value $v$ and penalty $p$ per unit of unmet demand; demand $X \ge 0$ has a known law with finite mean. Supplier $i \in \{1, 2\}$ has unit cost $c_i$, committed-cost fraction $\eta_i \in [0, 1]$ and design capacity $K_i > 0$. Its realized capacity loss $\xi_i \ge 0$ has a continuous distribution $G_i(\cdot, a_i)$ indexed by a reliability index $a_i$; a larger index means a stochastically smaller loss: $a \le a'$ implies $G_i(t, a) \le G_i(t, a')$ for all $t$. Losses are independent of each other and of demand.

An order $q_i \ge 0$ delivers $y_i = \min\{q_i, (K_i - \xi_i)^+\}$ and costs $(\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)^+,$$

the second-stage expected profit is $\Pi_2(q; a) = \mathbb E[\pi(q)]$, and $\Pi_2^*(a) = \sup_{q \ge 0}\Pi_2(q; a)$.

• Dual sourcing (DS) orders from both suppliers at their initial indices: $\Pi^*_{DS} = \Pi_2^*(a_1^0, a_2^0)$.
• Single sourcing with improvement (SSI) commits to one supplier $i$, spends $m_i z_i(a)$ to try to raise its index to $a \ge a_i^0$ (success probability $\theta_i$), and orders only from it. With $\Pi_2^*(a_i)$ the single-supplier optimal value, its profit is $\Pi_1(a_i) = -m_i z_i(a_i) + \theta_i \Pi_2^*(a_i) + (1-\theta_i)\Pi_2^*(a_i^0)$ (Eq. (7)), and $\Pi^*_{SSI} = \max_i \sup_{a \ge a_i^0} \Pi_1(a)$.
• Heterogeneity. For suppliers identical except in cost, $c_1 = c - \Delta_c$ and $c_2 = c + \Delta_c$ with $0 \le \Delta_c < c$; $\Delta_c$ is the cost heterogeneity parameter. The committed-cost parameter $\Delta_\eta$ is defined in the same way.

In Lean these objects are MitigateSupplyRisk.Heterogeneity.Model (with Pi2, Pi2star, PiDS, Pi1single, PiSSI, Pi1) and SymData (with costModel Δ and etaModel Δ).

Formalization targets

Goal: Theorem 7 (p. 502)

For suppliers identical except in unit cost,

$$\Delta_c \mapsto \Pi^*_{SSI}(\Delta_c) - \Pi^*_{DS}(\Delta_c) \quad\text{is nondecreasing on } [0, c).$$

The statement fixes no parameter values and no particular distribution; it asserts only the direction of the effect.

Milestones

1. Theorem 6(a) (p. 501): $\Pi^*_{SSI}$ is nondecreasing in $\Delta_c$ on $[0, c)$ and in $\Delta_\eta$ on $[0, \min\{\eta, 1-\eta\}]$.
2. Theorem 6(b) (p. 501): $\Pi^*_{DS}$ is nondecreasing in $\Delta_c$ and in $\Delta_\eta$ on the same ranges.
3. Lemma 5 (p. 504): the combined-strategy profit $\Pi_1(a)$ of Eq. (5), which improves one or both suppliers before dual sourcing, is submodular on $[a_1^0, \infty) \times [a_2^0, \infty)$:

$$\Pi_1(a \vee b) + \Pi_1(a \wedge b) \le \Pi_1(a) + \Pi_1(b).$$

Significance

Theorem 7 turns a strategy comparison into a comparative-statics statement: once SSI is preferred at some cost gap, it stays preferred at every larger gap, so the preference switches at most once along a cost-heterogeneity path. Theorem 6 shows separately that both strategies benefit from heterogeneity, which is immediate for a single-sourcing strategy but not for dual sourcing, where one supplier improves and the other deteriorates. Lemma 5 is the structural fact the paper uses for the combined strategy: improvement efforts at the two suppliers are substitutes.

The results are proved in the paper's online appendix, which this formalization does not use. To our knowledge none of them has a machine-checked proof. A formal development would supply reusable pieces: an expected-profit model for random capacity with integrable profits, envelope and convexity arguments for suprema of affine families, and monotone comparative statics for single- and dual-supplier newsvendor problems.

Difficulty

$\Pi^*_{SSI}$ and $\Pi^*_{DS}$ are both nondecreasing in $\Delta_c$ (Theorem 6), so the goal compares the growth rates of two optimal values. Neither has a closed form. Both are suprema of families affine in $\Delta_c$, so they are convex but may have kinks, and an optimal improvement level need not exist when the index set $[a^0, \infty)$ is unbounded. The comparison concerns orders at different cost levels and under different strategies, so it needs a link between the dual-sourcing order from the cheaper supplier and the single-sourcing order and its response to improvement. Evaluating each side at a fixed optimizer does not give it, because the two optimizers move with $\Delta_c$. For Lemma 5, submodularity of $\Pi_2(q; a)$ in $a$ for each fixed $q$ does not pass to the supremum over $q$ by itself.

Formalization scope

• Representation. Suppliers are indexed by Fin 2. Each $G_i(\cdot, a)$ is the cdf of a measure ν i a on ℝ. Expectations are Bochner integrals against the product of the two loss laws and the demand law. The integrand is bounded by a constant times $1 + |x|$, so the integrals are genuine.
• Optimal values. Optimal values are real suprema over $q \ge 0$ and $a \ge a_i^0$. Under the standing assumptions every such set is nonempty and bounded above by $(r + |v|)(K_1 + K_2)$, so no supremum takes Lean's default value. $\Pi^*_{SSI}$ is the early-commitment value and maximizes over the choice of supplier; it does not fix supplier 1.
• Standing assumptions (fields of Model.Standing and SymData.Standing):
  • the demand is a probability law on $[0, \infty)$ with finite mean;
  • each loss law is a continuous probability law on $[0, \infty)$, stochastically decreasing in the index;
  • $\eta_i \in [0, 1]$, $K_i > 0$, $\theta_i \in [0, 1]$, $m_i \ge 0$;
  • $z_i$ is convex and nondecreasing on $[a_i^0, \infty)$ with $z_i(a_i^0) = 0$.
• Disclosed readings.
  • $r \ge 0$, $p \ge 0$ and $c_i \ge 0$ ($c > 0$ in the heterogeneity statements, so that $c_1 > 0$) are the paper's readings of revenue, penalty and cost.
  • $v < r + p$ is implicit in the paper's Eq. (2), which divides by $r + p - v$.
  • The effort function $z_i(a)$ is taken as the primitive, as on p. 493. This presumes that every index $a \ge a_i^0$ is reachable.
  • $\Delta_\eta$ ranges over $[0, \min\{\eta, 1-\eta\}]$, the reading of "analogously" (p. 501) that keeps both committed costs in $[0, 1]$.
• Weak monotonicity. "Increasing" is weak (p. 492) and is stated as MonotoneOn.
• Corrections. No printed slip is corrected in this mission.
• Not formalized. Theorem 7 is stated without $\eta = 0$ and without concavity of $G$ in $a$, as on the page. The $\Delta_K$ and $\Delta_a$ clauses of Theorem 6 are not formalized, because the paper does not pin down how the improvement function depends on an initial index that differs between suppliers. Theorem 8 is also left out.
• Non-trivialization. Both values are recomputed as optimal values of the model at every $\Delta_c$. Defining them by a formula, fixing an optimizer at $\Delta_c = 0$, or hard-coding supplier 1 as the single source would trivialize the goal, and none of these is done.

Contributions are welcome at every level: integrability and boundedness lemmas for $\Pi_2$, convexity of the optimal values in $\Delta$, the symmetry argument behind Theorem 6(b), and monotone comparative statics of single-supplier orders in the reliability index.

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
• J. Hazra, B. Mahadevan, Impact of supply base heterogeneity in electronic markets, European Journal of Operational Research 174(3):1580–1594, 2006 (cited on p. 501 of the paper for the growth of supply-base heterogeneity).

Motivation

Many objective functions in engineering and statistics are nonsmooth and nonconvex: the spectral abscissa of a parametrized matrix, the largest eigenvalue of a symmetric matrix function, the $H_\infty$ norm of a closed-loop system, or a maximum of finitely many smooth functions. Such functions are typically differentiable almost everywhere, yet their minimizers usually sit exactly where the gradient fails to exist. Gradient descent then zig-zags or stalls, and bundle methods, which are designed for convex functions, lose their guarantees.

Burke, Lewis and Overton (SIAM J. Optim. 15 (2005) 751–779) proposed the gradient sampling (GS) algorithm: at each iterate, sample gradients at random nearby points, take the element of least norm in their convex hull, and search along its negative. The method needs nothing beyond gradients at points of differentiability, and it has since become a standard tool for nonsmooth, nonconvex minimization (Burke, Curtis, Lewis, Overton, Simões, 2020). This mission formalizes the paper's convergence theory.

Timeline. Goldstein (1977) introduced the $\epsilon$-subdifferential of a Lipschitz function and a conceptual descent method built on it. Clarke's generalized gradient (Clarke 1983) supplied the stationarity notion. Burke, Lewis and Overton (2005) made Goldstein's idea implementable by random sampling and proved almost-sure convergence to Clarke $\epsilon$-stationary points for a fixed sampling radius. Kiwiel (2007) revisited the analysis and proved convergence for a modified version of the algorithm.

Setting

Let $f:\mathbb R^n\to\mathbb R$ be locally Lipschitz, and let $D\subseteq\mathbb R^n$ be an open dense set on which $f$ is continuously differentiable. Write $\mathbb B$ for the closed Euclidean unit ball, and fix $\tilde x$ such that the level set $\mathcal L=\{x: f(x)\le f(\tilde x)\}$ is compact.

The Clarke subdifferential $\bar\partial f(x)$ is the convex hull of all limits $\lim_i\nabla f(x+h_i)$ with $h_i\to0$ and $f$ differentiable at each $x+h_i$. For $\epsilon>0$ define

$$G_\epsilon(x)=\operatorname{cl}\operatorname{conv}\nabla f\big((x+\epsilon\mathbb B)\cap D\big),\qquad \rho_\epsilon(x)=\operatorname{dist}\big(0\mid G_\epsilon(x)\big),$$

and the Clarke $\epsilon$-subdifferential $\bar\partial_\epsilon f(x)=\operatorname{cl}\operatorname{conv}\bigcup_{\|y-x\|\le\epsilon}\bar\partial f(y)$. A point is Clarke $\epsilon$-stationary if $0\in\bar\partial_\epsilon f(x)$, and Clarke stationary if $0\in\bar\partial f(x)$.

The GS algorithm. Fix $x^0\in\mathcal L\cap D$, $\gamma,\beta\in(0,1)$, $\epsilon_0>0$, $\nu_0\ge0$, $\mu\in(0,1]$, $\theta\in(0,1]$ and a sample size $m\ge n+1$. At iteration $k$:

1. Draw $u^{k1},\dots,u^{km}$ independently and uniformly from $\mathbb B$ and set $x^{kj}=x^k+\epsilon_k u^{kj}$. If some $x^{kj}\notin D$, stop. Otherwise let $G_k=\operatorname{conv}\{\nabla f(x^k),\nabla f(x^{k1}),\dots,\nabla f(x^{km})\}$.
2. Let $g^k$ be the least-norm element of $G_k$. If $\nu_k=\|g^k\|=0$, stop. If $\|g^k\|\le\nu_k$, set $t_k=0$, $\nu_{k+1}=\theta\nu_k$, $\epsilon_{k+1}=\mu\epsilon_k$ and go to step 4. Otherwise keep $\nu_{k+1}=\nu_k$, $\epsilon_{k+1}=\epsilon_k$ and set $d^k=-g^k/\|g^k\|$.
3. Let $t_k$ be the largest $\gamma^s$, $s\in\{0,1,2,\dots\}$, with $f(x^k+\gamma^s d^k)<f(x^k)-\beta\gamma^s\|g^k\|$.
4. If $x^k+t_kd^k\in D$, set $x^{k+1}=x^k+t_kd^k$. Otherwise pick any $\hat x^k\in x^k+\epsilon_k\mathbb B$ with $\hat x^k+t_kd^k\in D$ and $f(\hat x^k+t_kd^k)<f(x^k)-\beta t_k\|g^k\|$, and set $x^{k+1}=\hat x^k+t_kd^k$.

With $\nu_0=0$ and $\mu=1$ the radius stays fixed, $\epsilon_k=\epsilon_0=\epsilon$: this is fixed-radius mode.

Formalization targets

Goal: Theorem 3.4 (p. 760)

In fixed-radius mode, with probability $1$, either the algorithm stops at some iteration $k_0$ with $\rho_\epsilon(x^{k_0})=0$, or it runs forever and there is a subsequence $J$ with

$$\rho_\epsilon(x^k)\xrightarrow[k\in J]{}0,\qquad 0\in\bar\partial_\epsilon f(\bar x)\ \text{ for every cluster point }\bar x\text{ of }\{x^k\}_{k\in J}.$$

The theorem asserts nothing about $\|g^k\|$ along $J$; the authors list $\|g^k\|\to_J0$ as an open question.

Milestones

The milestones follow the paper's argument: the minimax characterization of the search direction (Lemma 2.1), the line-search descent estimate and the descent property of the iterates (§2), the almost-sure absence of a Step 1 stop, upper semicontinuity of $\rho_\epsilon$ and the uniform covering of Lemma 3.2(iv)–(v), Lebourg's mean value theorem (Theorem 3.3), the representation $\bar\partial f(x)=\bigcap_{\epsilon>0}G_\epsilon(x)$, the estimate of Lemma 3.1, the inclusion $G_\epsilon(x)\subseteq\bar\partial_\epsilon f(x)$, and the closed graph of $\bar\partial_\epsilon f$.

Companions

Well-posedness of the algorithm (every sample realization admits a run), Corollary 3.5(1) (the $C^1$ case: $\|g^k\|\to0$), Corollary 3.6 (Clarke $\epsilon_j$-stationary points with $\epsilon_j\downarrow0$ cluster at Clarke stationary points, and with a unique stationary point in $\mathcal L$ the sets $C_j$ converge to it in the Hausdorff sense), Corollary 3.7 (with a unique stationary point in $\mathcal L$, small $\epsilon$ forces the run near it), and Theorem 3.8 (the variable-radius mode with $\nu_0>0$).

Significance

Theorem 3.4 is the first convergence guarantee for a practical method on general locally Lipschitz, nonconvex functions that uses only gradients at points of differentiability. It holds for a fixed sampling radius, the setting where most of the work is, and Corollaries 3.6–3.7 and Theorem 3.8 transfer it to radii decreasing to zero, which is how the method is used in practice. Later gradient sampling variants and their analyses start from these results.

The results are proved on paper; no machine-checked proof of them is known. A formalization would make the probabilistic structure precise, which the paper leaves informal (see Formalization scope), and would certify the hypotheses under which the theorem holds. Already the statements record two such corrections.

Difficulty

The natural argument, "$f(x^k)$ decreases and $\mathcal L$ is compact, so the steps $t_k\|g^k\|$ tend to zero, hence $\|g^k\|\to0$", fails: $t_k$ can go to zero while $\|g^k\|$ stays bounded away from zero. The difficulty is to show that, on the event $\inf_k\rho_\epsilon(x^k)>0$, the random samples land infinitely often in a configuration whose sampled hull nearly realizes $\rho_\epsilon$ at a fixed nearby point, uniformly over a compact set of iterates, and that the failed trial step at such an iteration contradicts the Armijo rule. The iterates depend on all past samples, so independence across iterations cannot be used directly.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\nabla f$ is Mathlib's gradient, the Clarke subdifferential is the published ClarkeGradients.Shared.generalizedGradient, and $\operatorname{dist}(0\mid C)$ is Metric.infDist 0 C. Local Lipschitz continuity is Mathlib's LocallyLipschitz; continuous differentiability on $D$ is ContDiffOn ℝ 1 f D.
• A run is a predicate IsGSRun on the iterates, radii, tolerances, step lengths, least-norm vectors, directions and a stopping index $\tau\in\mathbb N\cup\{\infty\}$, imposing Steps 0–4 up to $\tau$. "$\max\gamma^s$" is the least admissible $s$, and the Armijo and (2) inequalities are strict.
• A random run (IsRandomGSRun) lives on a probability space with a filtration $(\mathcal F_k)$: the samples are uniform on $\mathbb B$, independent within an iteration, and independent of $\mathcal F_k$, while $x^k,\epsilon_k,\nu_k$ are $\mathcal F_k$-measurable. The Step 4 choice may use the past and extra randomness but never future samples. "With probability 1" is ∀ᵐ. The paper's event $\mathcal E$, the realizations that hit every positive-measure subset of $\mathbb B^m$ infinitely often, is not used, because no sequence has that property.
• Added hypothesis $\operatorname{vol}(D^c)=0$. An open dense set can have a complement of positive measure, and then Step 1 stops with positive probability, so Theorem 3.4 would fail. Every probabilistic statement, and the two inclusions $\bar\partial f(x)\subseteq G_\epsilon(x)$, $\bar\partial_{\epsilon_1}f(x)\subseteq G_{\epsilon_2}(x)$ (which fail without it), carry this hypothesis.
• Trivializing encodings are ruled out. The run predicate is satisfiable for every sample realization (a companion statement), so the goal is not vacuous. The Step 4 choice cannot anticipate future samples. The conclusion is almost sure, not sure.
• Reusable infrastructure: the Clarke $\epsilon$-subdifferential and its closed graph, Lebourg's mean value theorem for the published Clarke subdifferential, Lemma 2.1 (a finite-dimensional minimax identity), and a conditional Borel–Cantelli argument for adaptively placed targets. Contributions to any of these are welcome, as are proofs of the companion corollaries.

Selected references

• J. V. Burke, A. S. Lewis, M. L. Overton, A robust gradient sampling algorithm for nonsmooth, nonconvex optimization, SIAM J. Optim. 15(3) (2005) 751–779. https://doi.org/10.1137/030601296
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983; reprinted SIAM Classics in Applied Mathematics 5, 1990. https://doi.org/10.1137/1.9781611971309
• A. A. Goldstein, Optimization of Lipschitz continuous functions, Math. Programming 13 (1977) 14–22. https://doi.org/10.1007/BF01584320
• K. C. Kiwiel, Convergence of the gradient sampling algorithm for nonsmooth nonconvex optimization, SIAM J. Optim. 18(2) (2007) 379–388. https://doi.org/10.1137/050639673
• J. V. Burke, F. E. Curtis, A. S. Lewis, M. L. Overton, L. E. A. Simões, Gradient sampling methods for nonsmooth optimization, in Numerical Nonsmooth Optimization, Springer, 2020. https://arxiv.org/abs/1804.11003

Motivation

Firms that buy from unreliable suppliers can protect themselves in two ways: they can spread orders across several suppliers, or they can invest in improving a supplier's reliability, for example through supplier-development programmes or joint process-improvement projects. Wang, Gilland and Tomlin (MSOM 12(3):489–510, 2010) compare the two strategies in a newsvendor model with random supplier capacity.

This mission formalizes one part of that comparison: single sourcing with improvement, in which improvement efforts may fail. The firm must then decide when to choose its supplier. Under early commitment it picks one supplier, invests in it, and buys from it whatever the outcome. Under late commitment it invests in both suppliers, observes which efforts succeeded, and only then buys from the better one. Empirical work on supplier development documents both practices and the reluctance of suppliers whose improvement efforts previously failed (Handfield et al. 2000, as cited by Wang et al. 2010, p. 496; Krause et al. 2007). The question is how much the option to postpone the choice is worth.

Setting

A firm sells a single product over one season. It earns a unit revenue $r\ge 0$, salvages leftovers at $v$, and pays a penalty $p\ge 0$ per unit of unmet demand, with $v<r+p$. Demand $X$ is nonnegative with finite mean.

Supplier $i\in\{1,2\}$ has design capacity $K_i>0$, unit cost $c_i\ge 0$ and committed-cost fraction $\eta_i\in[0,1]$. Its capacity loss $\xi_i\ge 0$ has a continuous distribution $G_i(\cdot,a_i)$ that depends on a reliability index $a_i$; a higher index means a stochastically smaller loss. An order $q_i\ge 0$ delivers $y_i=\min\{q_i,(K_i-\xi_i)^+\}$. The firm pays $(\eta_iq_i+(1-\eta_i)y_i)c_i$, and the realized profit of single sourcing from $i$ is

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

The second-stage expected profit is $\Pi_2(q_i;a_i)=\mathsf E[\pi(q_i)]$, and $P_i(a_i)=\Pi_2^*(a_i)=\sup_{q_i\ge 0}\Pi_2(q_i;a_i)$ is its optimal value.

Improvement. Supplier $i$ starts at index $a_i^0$. Effort to reach index $a_i\ge a_i^0$ costs $m_iz_i(a_i)$, where $z_i$ is convex and increasing with $z_i(a_i^0)=0$. The effort succeeds with probability $\theta_i$; on failure the index stays at $a_i^0$.

• Early commitment to supplier $i$ yields

$$\Pi_{1i}^E(a_i)=-m_iz_i(a_i)+\theta_iP_i(a_i)+(1-\theta_i)P_i(a_i^0),$$

and $\Pi_1^{*E}=\max_i\sup_{a_i\ge a_i^0}\Pi_{1i}^E(a_i)$.

• Late commitment yields $\Pi_1^L(a_1,a_2)$: the improvement costs, plus, for each of the four success/failure outcomes, its probability times $\max\{P_1(\cdot),P_2(\cdot)\}$ at the realized indices (Eq. (9)). $\Pi_1^{*L}$ is its supremum over $a_1\ge a_1^0$, $a_2\ge a_2^0$.

Formalization targets

Goal: Theorem 5

Let the suppliers be identical except for their unit costs, $c_1\le c_2$, with common $\theta\in(0,1)$, $m$, $z$ and $a^0$, and let $a_2^{*E}$ be an optimal early-commitment index of supplier 2. Then

$$\bigl[P_2(a_2^{*E})-P_1(a_1^0)\bigr]^+>\frac{m\,z(a_2^{*E})}{\theta(1-\theta)}\quad\Longrightarrow\quad\Pi_1^{*L}>\Pi_1^{*E}.$$

Milestones, in the paper's order

1. Lemma 2(b), single-supplier instance: $P_i$ is increasing in the index.
2. Theorem 4(a), cost-only instance: if the suppliers differ only in unit cost, the cheaper one is preferred with and without improvement, so $i^*=j^*$.
3. §4.2.2: late commitment weakly dominates early commitment, $\Pi_1^{*E}\le\Pi_1^{*L}$.
4. Lemma 4: $a_i^{*L}\le a_i^{*E}$, in the form valid for non-unique optimizers.
5. §4.2.2: $\Pi_1^{*L}=\Pi_1^{*E}$ if $P_i(a_i^{*E})<P_j(a_j^0)$ for some $i$.
6. Corollary 3(a): strict superiority of late commitment at $c_1=\hat c_1$ persists for every $c_1\in[\hat c_1,c_2]$.

Significance

The results identify when the flexibility of postponing supplier selection has value. Late commitment never hurts. It has no value when one supplier dominates the other, even after the other's improvement. For suppliers that differ only in cost, Theorem 5 gives a checkable sufficient condition for strict value. The condition weighs the gain from switching in the outcome "the costlier supplier improves, the cheaper one does not", which has probability $\theta(1-\theta)$, against the cost of improving the costlier supplier. Together with Lemma 4 the results say that keeping the choice open lowers the reliability target but can raise expected profit. Corollary 3(a) says this value is easiest to obtain when costs are close.

The paper's proofs are in an online appendix that is not used here, and none of these statements has a machine-checked proof. The mission produces formal versions of the statements, with the hypotheses that the printed versions leave implicit made explicit (see Formalization scope), and invites proofs of them.

Difficulty

The late-commitment profit (9) is a probability-weighted sum of maxima of two optimal-value functions. It is "neither concave nor unimodal" (p. 498), so first-order conditions do not characterize its optimum, and optimizers need not be unique.

• Order of the arguments. The comparison results rest on the monotonicity of $P_i$ (Lemma 2(b)). That is a statement about a supremum of expectations under a stochastically ordered family of capacity-loss laws, and must be established before the first-stage results can use it.
• Theorem 5 and Corollary 3(a) compare two suprema, neither of which is assumed to be attained. Strictness has to survive passing to the supremum.
• Corollary 3(a) is a comparative-statics statement in $c_1$. Both $\Pi_1^{*L}$ and $\Pi_1^{*E}$ decrease as $c_1$ grows, so nothing pointwise orders their difference.

Formalization scope

Everything is in the namespace MitigateSupplyRisk.LateCommit, with one definition module Model.

• Model. The demand law is a probability measure $\mu$ on $\mathbb R$ with $\mu(-\infty,0)=0$ and finite mean; no density is assumed. Capacity losses are a family $a\mapsto\nu_a$ of atomless probability measures on $[0,\infty)$, ordered by $\nu_a(-\infty,t]\le\nu_{a'}(-\infty,t]$ for $a\le a'$. Loss and demand are independent (a product measure).
• Optimal values. $\Pi_2$ is the Bochner integral of the realized profit (1). Every optimal value is a sSup over the feasible set. The sign conventions $r,p,c_i\ge 0$, $v<r+p$ make these sets bounded above, so no supremum is a junk value, and no optimum is assumed to be attained.
• Effort. The effort function $z$ is taken as the primitive on $[a^0,\infty)$, which presumes that every index is reachable.
• Identical suppliers. "Identical except for unit costs" means that the two suppliers share the same Supplier record (committed cost, capacity, loss family) and the same Improvement record ($a^0,\theta,m,z$).
• Notation in (9). The paper writes $\Pi_2^*$ for both suppliers in (9); the Lean writes $P_1$ and $P_2$.
• Added or reread hypotheses:
  • Theorem 5 assumes $0<\theta<1$. The printed condition divides by $\theta(1-\theta)$, and Lean's $x/0=0$ would otherwise turn it into $[\cdot]^+>0$, under which the conclusion is false at $\theta=1$.
  • Lemma 4 is stated for arbitrary maximizers: $\max\{a_i^L,a_i^E\}$ is again an early maximizer. This reduces to the printed inequality when the early optimizer is unique.
  • Lemma 2(b) and Theorem 4(a) are the single-supplier and cost-only instances of the paper's statements.
  • Optimizers $a_i^{*E}$ appear as hypotheses (IsMaxOn), never as claims.
• Not trivially true. A statement in which $\Pi_1^{*L}$ or $\Pi_1^{*E}$ is a junk supremum, or in which Theorem 5's condition degenerates at $\theta\in\{0,1\}$, would be trivially true or false; the bounded feasible sets and the hypothesis $0<\theta<1$ exclude both.
• Not formalized: Theorem 4 for other attributes and Theorem 4(b), Lemma 3, and Corollary 3(b), whose printed form needs hypotheses the page does not pin.

Proofs of the milestones are welcome. A reusable lemma, that the supremum of expectations is monotone under first-order stochastic dominance of the loss, would serve the other missions of this series too.

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
• R. B. Handfield, D. R. Krause, T. V. Scannell, R. M. Monczka, Avoid the pitfalls in supplier development, Sloan Management Review, 2000, pp. 37–49 (cited from the reference list of Wang et al. 2010, https://doi.org/10.1287/msom.1090.0279).
• D. R. Krause, R. B. Handfield, B. B. Tyler, The relationships between supplier development, commitment, social capital accumulation and performance improvement, Journal of Operations Management 25(2):528–545, 2007. https://doi.org/10.1016/j.jom.2006.05.007
• B. Tomlin, On the value of mitigation and contingency strategies for managing supply chain disruption risks, Management Science 52(5):639–657, 2006. https://doi.org/10.1287/mnsc.1060.0515

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.