Optimization

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.

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

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

Motivation

Manufacturers of computer hardware, software and automobiles routinely pay channel rebates to their retailers: a payment for each unit the retailer sells to end customers, either for every unit (a linear rebate) or only for units beyond a target (a target rebate). In the same industries manufacturers also accept returns, crediting the retailer for unsold stock. Both instruments are meant to make the retailer act in the interest of the whole supply chain. When the retailer's sales effort drives demand and cannot be written into a contract, the question is which of these instruments, alone or combined, can make the retailer choose the effort and the stock that maximize total chain profit.

T. A. Taylor, Supply Chain Coordination Under Channel Rebates with Sales Effort Effects, Management Science 48(8) (2002) (DOI 10.1287/mnsc.48.8.992.168), answers this in a newsvendor model with multiplicative effort. Its Theorem 2 shows that a target rebate combined with returns can coordinate. This mission formalizes the complementary negative result, the paper's Proposition 2: no single instrument suffices. It is related to the impossibility shown by Cachon and Lariviere for revenue sharing with retailer effort (Management Science 51(1), 2005), but concerns different instruments.

Setting

A retailer orders a quantity $Q \ge 0$ and exerts a sales effort $e \ge 0$ before demand is observed. Demand is $e\xi$, where $\xi$ is a random variable with a density $\varphi$ on $\mathbb R$ that vanishes on $(-\infty, 0)$ and is strictly positive on $[0, \infty)$ (Assumption A4), with finite mean. Write

$$\Phi(Q) = \int_0^Q \varphi(\xi)\,d\xi, \qquad \Gamma(Q) = \int_0^Q \xi\,d\Phi(\xi).$$

Effort costs $V(e)$, where $V(0) = 0$ and $V$ is strictly increasing and strictly convex on $[0, \infty)$ (Assumption A5; the paper declares all such properties strict). The retail price $p$, the manufacturer's unit cost $c$, the wholesale price $w$ and the salvage value $s$ satisfy $0 < c < w < p$ and $s < c$ (Assumption A1); $s$ may be negative.

The integrated channel earns

$$\Pi(Q, e) = -cQ + pE\min(Q, e\xi) + sE(Q - e\xi)^+ - V(e),$$

and $(\bar Q, \bar e)$ denotes a maximizer of $\Pi$ over $Q \ge 0$, $e \ge 0$. Under a contract with wholesale price $w$, rebate $u$ per unit sold beyond the target $T$, and return credit $b$ per unsold unit, the retailer earns

$$R(Q, e \mid T) = -wQ + pE\min(Q, e\xi) + uE(\min(Q, e\xi) - T)^+ + bE(Q - e\xi)^+ - V(e).$$

Returns alone is $u = 0$ with $b \in [s, w)$; a target rebate alone is $u > 0$, $T \ge 0$ with no returns, $b = s$ (the retailer salvages leftovers herself); a linear rebate alone is the case $T = 0$ of the latter. Channel coordination means that the retailer's optimal decisions under the contract are the integrated channel's $(\bar Q, \bar e)$.

Formalization targets

Goal: Proposition 2 (p. 1003)

For every $b \in [s, w)$, every $u > 0$ and every $T \ge 0$,

$$(\bar Q, \bar e) \notin \arg\max_{Q, e \ge 0} R(\cdot, \cdot \mid T)\ \text{ under } (u, b, T) = (0, b, 0),\ (u, s, 0),\ (u, s, T).$$

The three clauses are returns alone, a linear rebate alone, and a target rebate alone. The statement asserts that $(\bar Q, \bar e)$ is not among the retailer's maximizers at all, which is stronger than saying that the retailer's optimum is not exactly $\{(\bar Q, \bar e)\}$.

Milestones

1. §4.1, p. 999. An integrated optimum with $\bar e > 0$ satisfies $\bar Q = \bar e\,\bar Q_0$ with $\Phi(\bar Q_0) = (p - c)/(p - s)$, $V'(\bar e) = (p - s)\Gamma(\bar Q_0)$, and $\Pi(\bar Q, \bar e) = \bar e V'(\bar e) - V(\bar e)$.
2. Lemma 2, p. 1000. For every effort $e \ge 0$, the retailer's optimal orders under $(w, u, b, T)$ are $\{e\underline Q_0\}$, $\{e\underline Q_1\}$ or $\{e\underline Q_0, e\underline Q_1\}$ as $e <, >, = T/\tau$, where $\Phi(\underline Q_0) = (p - w)/(p - b)$, $\Phi(\underline Q_1) = (p + u - w)/(p + u - b)$ and $\tau$ is the indifference target of the quantity-only problem.
3. §4.3, p. 1001. For $T > 0$, no optimal pair of the retailer has effort exactly $T/\tau$.

Significance

Proposition 2 is the converse half of the paper's main message. Together with Theorem 2 it says that the combination of a target rebate with returns is the minimal coordinating scheme among those considered: each ingredient alone fails, under general demand and general effort cost, not only in a parametric example. The proposition also frames the paper's remark that a linear rebate combined with returns coordinates only at $u = w - c$ and $b = s + w - c$, which leaves the manufacturer no profit.

The result is proved in the paper; nothing in this mission is open mathematics. No part of it has been machine-checked before. The formal development adds a precise account of what the paper's argument needs: the existence and interiority of the integrated optimum, the differentiability of the effort cost, and a full characterization of the retailer's optimal order for a general positive density, which the paper states but proves only for the quantity-only case.

Difficulty

The obvious route compares first-order conditions, but neither problem is globally smooth. The retailer's profit in $Q$ has an upward kink at $Q = T$, so it is concave only piecewise and its maximizer is decided by a comparison of two local maxima, not by a first-order condition. Consequently the retailer's value as a function of effort, $A(e \mid T) = \max_Q R(Q, e \mid T)$, switches branch at $e = T/\tau$ and is neither concave nor differentiable there. Showing that $(\bar Q, \bar e)$ is not a retailer optimum therefore requires the global order characterization (Lemma 2) in place of a local condition, a separate argument for the knife-edge effort $T/\tau$, and differentiability of expectations such as $E\min(Q, e\xi)$ in the effort level under only a finite-mean assumption. The paper's own proof cites Lemma 1 where Lemma 2 with $b = s$ is needed.

Formalization scope

The density form of A4 is literal: a measurable $\varphi$, zero on negatives, positive on $[0, \infty)$, integrating to one, with $\xi\varphi(\xi)$ integrable. The law of $\xi$ is Lebesgue measure with density $\varphi$; the law of $e\xi$ is its image under $x \mapsto ex$. The expectations $E\min(Q, e\xi)$ and $E(Q - e\xi)^+$ are the published CachonCoord.Newsvendor.expSales and expLeftover of that image law; the rebate term is the integral of $\max(\min(Q, x) - T, 0)$. Critical fractiles $\Phi^{-1}(\cdot)$ and the threshold $\tau$ are stated by their defining equations, never as inverse functions. "Optimal" means a maximizer over $Q \ge 0$ (and $e \ge 0$).

Two hypotheses are pinned relative to the page and disclosed in each statement. The effort cost carries a derivative $V'$ with $V$ differentiable at every $e > 0$: the paper writes $(\partial/\partial e)V$ in every first-order condition without stating it, and without it a kink of $V$ at $\bar e$ could let both the channel and the retailer stop at $\bar e$. The integrated optimum is a hypothesis, as the paper assumes its existence in words, and it is required to have $\bar e > 0$, as the paper's optimum is interior. Without $\bar e > 0$ the channel would sell nothing, and a degenerate statement would follow.

A trivializing reading is ruled out: the goal does not say that the retailer's first-order conditions fail at $(\bar Q, \bar e)$, nor that her optimum is not unique; it says that $(\bar Q, \bar e)$ is not a retailer maximizer.

Needed infrastructure: differentiation under the integral of $E\min(Q, e\xi)$ and $E(\min(Q, e\xi) - T)^+$ in $e$, strict monotonicity of $\Phi$ and $\Gamma$ on $[0, \infty)$, and the piecewise-concavity analysis of the newsvendor with a target rebate. These pieces are reusable for the sibling missions of this paper and for other effort-dependent newsvendor models. Proofs of the milestones and of supporting lemmas on these expectations are welcome.

Selected references

• T. A. Taylor, Supply Chain Coordination Under Channel Rebates with Sales Effort Effects, Management Science 48(8):992–1007, 2002. https://doi.org/10.1287/mnsc.48.8.992.168
• G. P. Cachon, M. A. Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, Management Science 51(1):30–44, 2005. https://doi.org/10.1287/mnsc.1040.0215
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science 11, 2003. https://doi.org/10.1016/S0927-0507(03)11006-7

Motivation

Two-stage stochastic linear programs model decisions taken before uncertainty is revealed (a first-stage plan $x$) followed by a corrective recourse action once it is. The classical model needs the full probability distribution of the uncertain data. In practice usually only estimates of a few moments are available, and the computed plan can be sensitive to the distribution that is assumed. The minimax (distributionally robust) approach replaces the single distribution by a class of distributions sharing given moments and optimizes against the worst member of the class. Bertsimas, Doan, Natarajan and Teo (Math. Oper. Res. 35(3), 2010) combine this with risk aversion, through a piecewise-linear disutility of the second-stage cost, and show which instances become semidefinite programs.

Besides the optimal value, the worst-case distribution itself is of practical interest: the paper proposes it as a natural distribution for stress-testing a first-stage solution (§4). This mission concerns the case where the right-hand side of the second stage is random, and formalizes the paper's construction of a worst-case distribution that is a genuine member of the moment class.

Setting

A first-stage decision $x\in\mathbb R^n$ is feasible if $x\in X=\{x : Ax=b,\ x\ge 0\}$. Given a recourse matrix $W\in\mathbb R^{r\times d}$, a technology matrix $T\in\mathbb R^{r\times n}$, a constant cost vector $q\in\mathbb R^d$ and a realized right-hand side $h\in\mathbb R^r$, the second-stage cost is the optimal value of the dual of the recourse linear program,

$$\mathcal Q(h,x)=\max_{p}\ (h-Tx)'p\quad\text{s.t.}\quad W'p\le q .$$

Risk aversion enters through the disutility $\mathbb U(t)=\max_{k=1,\dots,K}(\alpha_k t+\beta_k)$ with $\alpha_k\ge 0$. The right-hand side $\tilde h$ is random; its distribution is only known to lie in the moment class

$$\mathcal P=\{P : \mathbb E_P[\tilde h]=\mu,\ \mathbb E_P[\tilde h\tilde h']=Q\},$$

and the worst-case expected disutility is $\hat Z(x)=\sup_{P\in\mathcal P}\mathbb E_P[\mathbb U(\mathcal Q(\tilde h,x))]$.

The standing assumptions are: complete recourse, $\{Ww : w\ge 0\}=\mathbb R^r$; a nonempty dual polyhedron $\{p : W'p\le q\}$; $Q\succ\mu\mu'$; and (Assumption 5) the extreme points $p_1,\dots,p_N$ of the dual polyhedron are known. Under these, the paper introduces the semidefinite program (16): over symmetric blocks indexed by pairs $(k,i)$,

$$\hat Z_{DD}(x)=\max\ \sum_{k=1}^K\sum_{i=1}^N\big(\alpha_k p_i'v_k^i+v_{k0}^i(\beta_k-\alpha_k p_i'Tx)\big) \ \ \text{s.t.}\ \ \sum_{k,i}\begin{pmatrix}V_k^i & v_k^i\\ (v_k^i)' & v_{k0}^i\end{pmatrix}=\begin{pmatrix}Q&\mu\\ \mu'&1\end{pmatrix},\ \ \begin{pmatrix}V_k^i & v_k^i\\ (v_k^i)' & v_{k0}^i\end{pmatrix}\succeq 0 .$$

From a point of (16) the paper builds the mixed distribution $P_m(x)$, which with probability $v_{k0}^i$ draws a normal vector with mean $v_k^i/v_{k0}^i$ and covariance $(V_k^iv_{k0}^i-v_k^i(v_k^i)')/(v_{k0}^i)^2$.

Formalization targets

Goal: Theorem 3.3 (p. 590)

For every $x\in X$ there is $P\in\mathcal P$ with

$$\mathbb E_{P'}\big[\mathbb U(\mathcal Q(\tilde h,x))\big]\le \mathbb E_{P}\big[\mathbb U(\mathcal Q(\tilde h,x))\big]=\hat Z(x)=\hat Z_{DD}(x)\qquad\forall P'\in\mathcal P,$$

where the common value is the attained maximum of (16), and the expected disutility is integrable under every member of $\mathcal P$.

Milestones (proof of Theorem 3.3, pp. 590–591)

1. $\mathbb U(\mathcal Q(h,x))=\max_{k,i}\big(\alpha_k(h-Tx)'p_i+\beta_k\big)$ for every $h$.
2. Every $P\in\mathcal P$ yields a feasible point of (16) of equal value; hence $\hat Z(x)\le\hat Z_{DD}(x)$.
3. (16) has an optimal solution whose blocks have $v_{k0}^i>0$ or vanish.
4. For such a feasible point, $P_m(x)\in\mathcal P$.
5. $\mathbb E_{P_m(x)}[\mathbb U(\mathcal Q(\tilde h,x))]$ is at least the objective value of (16) at that point.

Significance

The result. Theorem 3.3 shows that, once the dual extreme points are known, the worst case over the moment class is attained, and by an explicit finite mixture of normal distributions read off an optimal solution of a semidefinite program. This contrasts with the random-objective case of the same paper (Theorem 2.2), where the bound is in general only approached by a sequence of distributions. The extremal distribution gives a concrete stress-test scenario for a candidate first-stage plan, and the identity $\hat Z(x)=\hat Z_{DD}(x)$ certifies the value of the inner worst-case problem without appeal to strong duality for the moment problem.

Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. A formal proof needs a measure-theoretic treatment of conditional moments on the cells of a piecewise-linear maximum, the existence of optima of a bounded semidefinite program, and moment computations for multivariate normal mixtures. These pieces are reusable well beyond this paper, for instance in other moment-based distributionally robust models.

Difficulty

The obvious route goes through moment-problem duality: dualize $\sup_{P\in\mathcal P}$, reformulate the semi-infinite constraint as linear matrix inequalities, and dualize again. That route only gives the inequality chain up to a duality gap and says nothing about attainment over $\mathcal P$. The proof here avoids strong duality, but it must show two separate things: every distribution in $\mathcal P$ maps to a feasible point of (16) without loss of value (this needs a measurable choice of the maximizing pair and the conditional moments on each cell), and the optimal point of (16) maps back to a distribution in $\mathcal P$ whose value is at least the optimum. The second step fails on blocks with zero weight $v_{k0}^i=0$, where no normal component can be formed; those blocks have to be removed from an optimal solution first.

Formalization scope

The Lean development works on $\mathbb R^r$ as Fin r → ℝ, with measures in place of the paper's densities. The moment class reuses the published definitions MomentDRO.Conf.HasSecondMoments, meanVec and secondMomentAbout P 0 (uncentred second moment). $\mathcal Q(h,x)$, $\hat Z(x)$ and $\hat Z_{DD}(x)$ are real sSups; every theorem that uses them states the relevant maximum or bound explicitly, so no statement depends on the junk value of an empty or unbounded supremum. Bordered matrices are Matrix.fromBlocks over Fin r ⊕ Fin 1 and $\succeq 0$ is Matrix.PosSemidef. The normal components are Mathlib's multivariateGaussian, transported from EuclideanSpace ℝ (Fin r); the mixture weights are ENNReal.ofReal $v_{k0}^i$.

Readings of the page:

• As printed, Assumption 2 (complete recourse) and Assumption 3 "for all $q$" are mutually inconsistent when $r\ge 1$. The formalization uses complete recourse and nonemptiness of $\{p : W'p\le q\}$ at the one constant $q$ of §3.
• Assumption 1 is not used and is dropped; $x\in X$ is kept as in the statement.
• "Without loss of generality $v_{k0}^i>0$" is read as: some optimal solution has every block either with $v_{k0}^i>0$ or zero.
• The printed "$V_k^iv_{k0}$", "$v_{k0}^2$" and "with probability $v_{k0}$" are read with the superscript $i$.

The goal asserts that a maximizer over $\mathcal P$ exists, not only an equation between suprema: an equation such as $\mathbb E_P[\cdot]=\hat Z(x)$ alone could hold through a junk value and is ruled out as the target. No strong-duality hypothesis is assumed, since the proof does not need one. Contributions welcome: the measurable argmax selection, compactness of the feasible set of (16), and second-moment computations for Gaussian mixtures.

Selected references

• D. Bertsimas, X. V. Doan, K. Natarajan, C.-P. Teo, Models for Minimax Stochastic Linear Optimization Problems with Risk Aversion, Mathematics of Operations Research 35(3):580–602, 2010. https://doi.org/10.1287/moor.1100.0445
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• J. Dupačová, The minimax approach to stochastic programming and an illustrative application, Stochastics 20(1):73–88, 1987. https://doi.org/10.1080/17442508708833436