Operations Research

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

A $T$-join of a graph $G$ is a set of edges $F$ such that exactly the vertices of a prescribed even set $T$ have odd degree in $F$. Minimum $T$-joins are a classical object of combinatorial optimization: they contain shortest paths ($|T|=2$), Chinese postman tours and perfect matchings as special cases, and their duality with $T$-cuts connects them to integral multiflows. Whether the minimum size $\tau(G,T)$ of a $T$-join equals the maximum number $\nu(G,T)$ of disjoint $T$-cuts has been studied extensively; equality always holds in bipartite graphs (Seymour 1981).

Sebő and Tannier (Math. Oper. Res. 2004) study the number of connected components of a minimum $T$-join, motivated by the observation that a minimum $T$-join with few components yields a large integral packing of $T$-cuts. Deciding whether some minimum $T$-join has at most $k$ components is NP-complete in general (their Theorem 5). This mission formalizes the opposite end, $k=1$: Theorem 6 characterizes exactly when a minimum $T$-join can be chosen connected, in terms of the shortest-path metric of $G$ restricted to $T$. The result first appeared in the authors' IPCO paper Connected joins in graphs (2001); the 2004 article derives it from its theory of isometric embeddings.

Setting

All graphs are finite, simple, undirected and connected. For vertices $x,y$ of $G$, $\mu_G(x,y)$ is the number of edges of a shortest $x$–$y$ path. For $T\subseteq V(G)$, $\mu_G|_T$ is the restriction of $\mu_G$ to pairs of vertices of $T$.

For an edge set $F\subseteq E(G)$, $\deg_F(v)$ is the number of edges of $F$ at $v$; $F$ is a $T$-join if $\deg_F(v)$ is odd exactly when $v\in T$. A minimum $T$-join has the fewest edges among all $T$-joins; a minimal one has no proper subset that is a $T$-join. $V(F)$ is the set of endpoints of edges of $F$; $F$ is connected (a tree) when the graph $(V(F),F)$ is connected (a tree), and $\mu_F$ is the distance in $(V(F),F)$.

An isometry from $(X,\mu)$ to $(Y,\nu)$ is a map $f$ with $\nu(f(x),f(y))=\mu(x,y)$ for all $x,y$. A metric $\mu$ on a finite set $X$ is a tree metric if there is a tree $A$ (unit edge lengths) and an isometry $g$ from $(X,\mu)$ to $A$; the pair $(A,g)$ is a realization. A realization is inclusionwise minimal if no proper subtree of $A$ contains $g(X)$. A tree $A$ is an $S$-join if its vertices of odd degree are exactly those of $S$.

Formalization targets

Goal: Theorem 6

For $G$ connected and $T$ nonempty of even cardinality,

$$\exists\,F\ \text{minimum connected }T\text{-join} \iff \begin{cases}\mu_G|_T \text{ is a tree metric, and for its minimal realization }(A,g),\ T':=g(T):\\ A \text{ is a } T'\text{-join},\\ \exists\,\varphi:V(A)\to V(G)\ \text{isometry with } \varphi(g(t))=t\ (t\in T).\end{cases}$$

The conditions are required of every minimal realization; all of them are isomorphic.

Milestones

1. (p. 389) A minimal $T$-join is the edge-disjoint union of $|T|/2$ paths pairing the vertices of $T$.
2. (p. 391) In every realization of $\mu$, the distance from $g(x)$ to the $g(y)$–$g(z)$ path equals $\tfrac12(\mu(x,y)+\mu(x,z)-\mu(y,z))$.
3. (p. 391) A tree metric has an inclusionwise minimal realization, unique up to an isomorphism respecting the realization maps.
4. (Lemma 2, p. 392) A connected $T$-join $F$ is minimum if and only if $F$ is a tree and $\mu_F=\mu_G$ on $V(F)$.
5. (p. 392) If $A$ is a $T'$-join and $\varphi$ an isometry from $A$ to $G$ extending $g^{-1}$, the image of $A$ under $\varphi$ is a $T$-join that is a tree with $\mu_F=\mu_G$ on $V(F)$.

Significance

Theorem 6 turns the existence of a connected minimum $T$-join, a question about all $T$-joins of $G$, into conditions on the finite metric $\mu_G|_T$ alone plus one isometric embedding of a tree into $G$. Tree metrics can be recognized and their minimal realization constructed efficiently (Buneman 1974), and the embedding problem is the one solved in §2 of the paper, since $T'$ contains all leaves of $A$. The authors deduce that connected minimum $T$-joins can be found in polynomial time, which contrasts with the NP-completeness of the same question for $k$ components. A consequence stated in the paper: if the minimal realization of $\mu_G|_T$ is not a $T'$-join, then no minimum $T$-join is connected.

The result is proved in the paper. No machine-checked version of Theorem 6, of Lemma 2, or of the uniqueness of minimal tree realizations is known to exist; Mathlib has graph distances, trees and walks, but neither $T$-joins nor tree metrics. The mission produces these definitions and a formal proof of the characterization; the complexity consequence is out of scope.

Difficulty

The central difficulty is in the necessity direction. A connected minimum $T$-join $F$ is itself a minimal realization of $\mu_G|_T$ (Lemma 2), so $F$ satisfies the conditions; but the conditions concern the minimal realization, and transferring them from $F$ to an arbitrary minimal realization requires that minimal realizations are unique up to a label-preserving isomorphism. That uniqueness (milestone 3) is the step where the obvious approach stops: it is a statement about all trees realizing a metric, not about the graph $G$.

Formalization scope

• Graphs are SimpleGraph V with [Fintype V] [DecidableEq V]; G.Connected is a hypothesis of every statement about $G$ (SimpleGraph.dist is $0$ on unreachable pairs). Distances are natural numbers (SimpleGraph.dist).
• Edge sets are Finset (Sym2 V). Connectivity, the tree property and $\mu_F$ refer to the graph with edge set $F$ induced on $V(F)$, not on all of $V$.
• "Minimum" is "$|F|\le|F'|$ for every $T$-join $F'$", never an infimum over $\mathbb N$.
• A realization is a tree on Fin N together with a map $g:X\to$ Fin N; this avoids quantifying over a universe. A tree metric must satisfy $\mu(x,y)=0\Rightarrow x=y$.
• "The unique minimal realization" is encoded by quantifying over all inclusionwise minimal realizations. A goal that only asks for some minimal realization satisfying the conditions is a different, weaker statement (its necessity half needs no uniqueness) and is not this mission's target.
• $T\neq\emptyset$ is added: for $T=\emptyset$ the minimum $T$-join is empty and its connectivity is only a convention.
• "$f$ is the inverse of $g$ and $\varphi$ extends $f$" is encoded as $\varphi(g(t))=t$. Isometries preserve all distances, not only adjacency.
• Halving and subtraction (milestone 2) are multiplied out.

Reusable beyond this mission: the $T$-join vocabulary, the path decomposition of minimal $T$-joins, and tree metrics with the uniqueness of minimal realizations. Contributions to any milestone are welcome, as are alternative proofs of milestone 3.

Selected references

• András Sebő, Eric Tannier, On Metric Generators of Graphs, Mathematics of Operations Research 29(2):383–393, 2004. https://doi.org/10.1287/moor.1030.0070
• András Sebő, Eric Tannier, Connected joins in graphs, Integer Programming and Combinatorial Optimization (IPCO 2001), Lecture Notes in Computer Science 2081, 383–395, 2001. https://doi.org/10.1007/3-540-45535-3
• Peter Buneman, A note on the metric properties of trees, Journal of Combinatorial Theory, Series B 17:48–50, 1974. https://doi.org/10.1016/0095-8956(74)90047-1
• Paul Seymour, On odd cuts and plane multicommodity flows, Proceedings of the London Mathematical Society 42:178–192, 1981. https://doi.org/10.1112/plms/s3-42.1.178

Motivation

In a linearly parameterized bandit, the expected rewards of many arms are driven by a small number of unknown parameters. Each arm is a vector $u \in \mathbb R^r$, and its expected reward is the inner product $u'Z$ with an unknown parameter vector $Z$. Problems of this kind arise in marketing and revenue management, where each product is described by $r$ features (price, popularity, …) and the expected revenues of thousands of products are, to a good approximation, linear in a few unknown feature weights. Pulling one arm then reveals information about all of them, and a good policy has to exploit this correlation.

Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, 2010) studied this model with unbounded, sub-Gaussian noise and a prior on $Z$. They proved an $\Omega(r\sqrt T)$ lower bound, a matching policy for smooth arm sets, and the Uncertainty Ellipsoid (UE) policy for arbitrary arm sets. This mission formalizes their Theorem 4.2: when the set of arms is finite, the regret of UE grows like $\log T$, within a constant factor of the Lai–Robbins lower bound for the classical multi-armed bandit (Lai and Robbins, 1985).

Timeline.

• 1985: Lai and Robbins prove that, for independent arms, the regret of any uniformly good policy grows at least like $\log T$, and give policies attaining it.
• 2002: Auer, Cesa-Bianchi and Fischer give the finite-time UCB1 analysis (doi:10.1023/A:1013689704352), whose pull-count argument the UE analysis adapts. Auer, in the same year, studies linear payoffs with confidence bounds (JMLR 3).
• 2010: Rusmevichientong and Tsitsiklis treat unbounded sub-Gaussian noise with an anytime policy (UE), and prove the $\log T$ regret and $\log^2 T$ Bayes-risk bounds for finitely many arms formalized here.

Setting

Let $r \ge 2$ and let $\mathcal U_r \subset \mathbb R^r$ be a finite, nonempty set of arms. Fix $z \in \mathbb R^r$, the value of the unknown parameter. Playing arm $u$ in period $t$ yields the reward $X_t = u'z + W_t$. The noise $W_t$ is drawn afresh in each period from a law $\nu_u$ that depends only on the arm played, independently of the past. A policy chooses the arm $U_{t+1}$ of period $t+1$ as a function of the history $H_t = (U_1, X_1, \dots, U_t, X_t)$. The regret given $Z = z$ is

$$\mathrm{Regret}(z, T, \psi) = \sum_{t=1}^T \mathbb E\Big[\max_{v \in \mathcal U_r} v'z - U_t'z \,\Big|\, Z = z\Big],$$

and for a prior $\mu$ of $Z$ the Bayes risk is $\mathrm{Risk}(T, \psi) = \mathbb E_{Z \sim \mu}[\mathrm{Regret}(Z, T, \psi)]$. The gap of arm $u$ is $\Delta^u(z) = \max_{v \in \mathcal U_r} v'z - u'z$, and $N^u(z, T)$ is the number of periods among the first $T$ in which $u$ is played.

Assumption 1.

• (a) Every $\nu_u$ has mean zero and $\mathbb E[e^{xW}] \le e^{x^2\sigma_0^2/2}$ for all $x$.
• (b) Every arm has norm at most $\bar u$, and $\mathcal U_r$ contains $r$ linearly independent arms $b_1, \dots, b_r$ with $\lambda_{\min}(\sum_k b_kb_k') \ge \lambda_0$.

The UE policy first plays $b_1, \dots, b_r$. It then forms the least squares estimate $\widehat Z_t = C_t\sum_{s\le t}U_sX_s$ with $C_t = (\sum_{s \le t} U_sU_s')^{-1}$, and plays an arm maximizing $v'\widehat Z_t + R^v_t$. The uncertainty radius is

$$R^v_t = \alpha\sqrt{\log t}\sqrt{\min\{r\log t, |\mathcal U_r|\}}\,\sqrt{v'C_tv},$$

with $\alpha = 4\sigma_0\kappa_0^2$ and $\kappa_0 = 2\sqrt{1 + \log(1 + 36\bar u^2/\lambda_0)}$. Ties are broken arbitrarily.

Formalization targets

Goal: Theorem 4.2

There are constants $a_6, a_7 > 0$ depending only on $\sigma_0, \bar u, \lambda_0$ such that for all $T \ge r+1$ and $z$,

$$\mathrm{Regret}(z, T, \mathrm{UE}) \le a_6|\mathcal U_r|\,\|z\| + a_7|\mathcal U_r|\sum_{u \in \mathcal U_r}\min\Big\{\frac{\log T}{\Delta^u(z)}, T\Delta^u(z)\Big\}.$$

If moreover each $\Delta^u(Z)$ has a point mass at $0$ and a density bounded by $M_0$ on $\mathbb R_+$, there are $a_8, a_9 > 0$ depending only on $\sigma_0, \bar u, \lambda_0, M_0$ with

$$\mathrm{Risk}(T, \mathrm{UE}) \le a_8|\mathcal U_r|\,\mathbb E\|Z\| + a_9|\mathcal U_r|^2\log^2 T.$$

The constants are left unspecified, as in the paper. Their existence, uniformly in $r$ and in the arm set, is the content.

Milestones

• Theorem B.1 and Theorem B.2: Chernoff-type deviation bounds for adaptive least squares, with factors $t^{5|\mathcal U_r|}$ and $t^{r\kappa_0^2}$.
• Lemma B.6: the radius $R^u_t$ is exceeded with probability at most $1/t^2$.
• The pull-count bound of App. B.3: $\mathbb E[N^u(z,T)] \le 6 + 4\alpha^2|\mathcal U_r|\log T/\Delta^u(z)^2$ for every suboptimal arm.
• The regret decomposition $\mathrm{Regret} = \sum_u\Delta^u(z)\,\mathbb E[N^u(z,T)]$.
• The risk bound $\mathbb E[\min\{\log T/\Delta^u(Z), T\Delta^u(Z)\}] \le (M_0+1)\log T + M_0\log^2 T$.

Significance

The result. For a fixed finite arm set, Theorem 4.2 shows that a single anytime policy, which does not know $T$, has regret $O(\log T)$ for every parameter and Bayes risk $O(\log^2 T)$. It does this with unbounded noise and correlated arms. The dependence on the problem enters only through the gaps $\Delta^u(z)$ and the number of arms. The companion result for general compact arm sets (Theorem 4.1) gives only $\tilde O(r\sqrt T)$. The finite case shows that the same policy adapts to the easier problem.

Formalizing it. The theorem is proved on paper. As far as is known, it has no machine-checked proof. The platform's finite-armed bandit library (Lattimore–Szepesvári) has the regret decomposition and UCB pull-count bounds for independent arms, e.g. BanditAlgorithm.bandit_regret_decomposition. Those statements live in a different model and do not apply to correlated linear rewards with a least squares estimator. This mission adds:

• self-normalized deviation bounds for adaptively collected least squares estimates, under per-arm sub-Gaussian noise;
• a pull-count analysis that runs through a matrix-valued confidence radius;
• the Bayes-risk integration under a density condition.

Difficulty

The arms are chosen adaptively, so the design matrix $\sum_s U_sU_s'$ is random and depends on the noise. Applied with the realized $C_t$, the classical Chernoff bound for a fixed weighted sum of independent noises is not valid. The obvious union bound over arms does not apply either: the event concerns the random matrix $C_t$, not one arm. In the pull-count bound, the radius of arm $u$ must be controlled through the number of times $u$ was played, although $C_t$ mixes all arms, and the Gram matrix of the other arms may be singular.

Formalization scope

• Space. $\mathbb R^r$ is EuclideanSpace ℝ (Fin r), so $\|\cdot\|$ is Euclidean. The source is arXiv:0812.3465v2; its printed page numbers equal the PDF's.
• Model.
  • The arm set is a finite nonempty Set, and $|\mathcal U_r|$ is its ncard. Theorem B.2 and Lemma B.6, which the paper states for any compact arm set, are stated for compact nonempty arm sets, as printed.
  • The noise is a Markov kernel $u \mapsto \nu_u$.
  • The law of the history given $Z = z$ is built period by period, with fresh noise from $\nu_{U_{t+1}}$. This is the paper's model: noises independent of each other and of $Z$, identically distributed in $t$, mean zero.
  • Policies are deterministic and history-dependent, with measurable selection rules. The paper uses this measurability implicitly.
  • Regret is $T\max_v v'z - \mathbb E[\sum_t U_t'z]$.
  • Assumption 1(a) is an mgf bound written with a lower integral, so the exponential moments are finite. Assumption 1(b) writes $\lambda_{\min} \ge \lambda_0$ as $\lambda_0\|x\|^2 \le \sum_k (b_k'x)^2$.
  • A UE run is any measurable policy that plays $b_1, \dots, b_r$ first and then an arg max of (7). The theorems hold for every tie-breaking rule.
• Constants. They are quantified before $r$, the arm set, the noise, the policy, $T$, $z$ and the prior, so they cannot depend on any of these.
• Corrections and added hypotheses.
  • The pull-count bound is stated for arms with $\Delta^u(z) > 0$. As printed, it divides by a zero gap for an optimal arm.
  • The risk part assumes $\mathbb E\|Z\| < \infty$ and concludes the integrability of the regret.
• Conventions.
  • An optimal arm contributes $\min\{\log T/0, 0\} = 0$, the paper's reading and Lean's value.
  • The density condition says that, on $(0,\infty)$, the law of $\Delta^u(Z)$ is at most $M_0$ times Lebesgue measure.
• No trivializing reading. The regret is never a junk-valued integral that makes the bound free: the integrand is bounded and measurable, and a junk value would only raise the regret. The width $\min\{r\log t, |\mathcal U_r|\}$ uses the true cardinality, so the radius is not zero.
• Contributions welcome. Reusable pieces are the history-measure construction, Chernoff bounds for adaptive designs, and the deviation bounds of Theorems B.1–B.2, which the companion mission on general compact arm sets also needs.

Selected references

• P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, arXiv:0812.3465v2, 24 Feb 2010. https://arxiv.org/abs/0812.3465
• T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• P. Auer, Using confidence bounds for exploitation–exploration trade-offs, JMLR 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• V. H. de la Peña, M. J. Klass, T. L. Lai, Self-normalized processes: exponential inequalities, moment bounds and iterated logarithm laws, Annals of Probability 32, 2004. https://doi.org/10.1214/009117904000000397

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

Let $G$ be a connected graph and $T$ a set of vertices of even cardinality. A $T$-join is a set of edges $F$ in which exactly the vertices of $T$ have odd degree. A $T$-cut is a cut $\delta(X)$ with $|X\cap T|$ odd. Write $\tau(G,T)$ for the minimum size of a $T$-join and $\nu(G,T)$ for the maximum number of pairwise disjoint $T$-cuts. Every $T$-cut meets every $T$-join, so $\nu(G,T)\le\tau(G,T)$. When equality holds is a central question of combinatorial optimization because of its links to integral multiflows. Seymour (1981) proved equality for all $T$ in bipartite graphs. Middendorf and Pfeiffer (1998) showed that deciding equality is NP-complete.

Korach and Penn (1992) proved that a minimum $T$-join $F$ with $k$ connected components satisfies

$$\tau(G,T)-k+1\ \le\ \nu(G,T)\ \le\ |F|.$$

So a minimum $T$-join with few components certifies a large packing of $T$-cuts, and a connected one certifies $\nu=\tau$. Sebő and Tannier (Math. Oper. Res. 2004) therefore study the problem MTSC: given $G$, $T$ and an integer $k$, is there a minimum $T$-join with at most $k$ connected components? They show it can be solved in polynomial time for $k=1$ and is NP-complete in general (their Theorem 5). The hardness proof reduces three-dimensional matching (3DM) to MTSC. This mission formalizes the correctness of that reduction.

Setting

Three-dimensional matching. An instance consists of three pairwise disjoint sets $W$, $X$, $Y$, each of cardinality $q$, and a set of triples $H\subseteq W\times X\times Y$. A matching is a subset $M\subseteq H$ in which every element of $W\cup X\cup Y$ occurs in exactly one triple.

The graph $G$. Take a further set $Z$ of $q$ points and put $T:=W\cup X\cup Y\cup Z$, so $|T|=4q$. The graph $G$ has as vertices the points of $T$, the triples of $H$, and one new vertex $p_{ab}$ for every unordered pair $\{a,b\}$ of distinct points of $T$. Its edges are:

1. $a\,p_{ab}$ and $p_{ab}\,b$ for every such pair, so any two points of $T$ are joined by a path of length 2;
2. $hw$, $hx$, $hy$ and $hz$ for every $h=(w,x,y)\in H$ and every $z\in Z$.

There are no other edges. In Lean, $G$ is gadget q H and $T$ is gadgetT q H.

$T$-joins and components. For $F\subseteq E(G)$ and a vertex $v$, $\deg_F(v)$ is the number of edges of $F$ at $v$. $F$ is a $T$-join (IsTJoin) if $\deg_F(v)$ is odd exactly for $v\in T$. It is a minimum $T$-join (IsMinTJoin) if no $T$-join of $G$ is smaller. The connected components of $F$ are those of the graph $(V(F),F)$, where $V(F)$ is the set of endpoints of edges of $F$. Their number is numComponents F.

Formalization targets

Goal: the Claim in the proof of Theorem 5 (p. 391)

$$\exists\,F \text{ minimum } T\text{-join of } G \text{ with at most } q \text{ components}\quad\iff\quad \exists\,M\subseteq H \text{ a matching.}$$

This statement is quantified over every $q$ and every $H$, and it is the full mathematical content of the reduction.

Milestones (p. 391, in the order the proof uses them)

1. Every $T$-join $F$ of $G$ has $|F|\ge 4q$, with equality iff each $t\in T$ lies in exactly one edge of $F$.
2. If $M$ is a matching, $Z$ can be indexed as $\{z_m: m\in M\}$, and for every such indexing $\bigcup_{m=(w,x,y)\in M}\{mw,mx,my,mz_m\}$ is a minimum $T$-join with exactly $q$ components.
3. Every minimum $T$-join $F$ has $|F|=4q$, and each $t\in T$ lies in exactly one edge of $F$.
4. Every minimum $T$-join has at least $q$ components. It has exactly $q$ iff each component contains a vertex of $H$ and exactly one vertex of each of $W$, $X$ and $Y$.

Significance

The result. The Claim shows that minimizing the number of components of a minimum $T$-join is NP-hard. A Korach–Penn certificate for a large packing of $T$-cuts therefore cannot in general be found by optimizing the component count. This sets the $k=1$ case, which Sebő and Tannier solve in polynomial time through isometric embeddings of tree metrics, apart from the general case.

Formalizing it. The Claim is proved in the paper, in one paragraph. No machine-checked version is known, and the platform has no $T$-join library. The mission produces a reusable vocabulary for $T$-joins, minimum $T$-joins and the components of an edge set, together with a checked proof that a concrete gadget is correct. One sentence of the published argument is false as written (see Difficulty); a formal proof settles the conclusion independently of it.

Difficulty

The direction from a matching to a $T$-join is a direct verification. The converse has to control an arbitrary minimum $T$-join: its size, the shape of each of its components, and how the components meet $W$, $X$ and $Y$. A first reading of the printed proof suggests that every vertex outside $T$ that carries edges of $F$ is adjacent to at most one vertex of each of $W$, $X$, $Y$. This is false for the inner vertex of a path joining two vertices of the same class, and the construction joins every pair of points of $T$, including pairs inside $W$. Such components really occur in minimum $T$-joins, so the count of components has to cover them as well. The stated conclusion (at least $q$ components, with equality only in the matching-like configuration) remains true.

On the Lean side, the components of an edge set are not the components of the graph with that edge set on all vertices: there every untouched vertex would be a component, and the Claim would become false.

Formalization scope

• 3DM. $W$, $X$, $Y$ are three copies of $\{0,\dots,q-1\}$ (Fin q), so their disjointness holds by construction. $H$ and $M$ are finite sets of triples in Fin q × Fin q × Fin q. IsMatching q M requires each element of each class to be the corresponding coordinate of exactly one triple of $M$, and $M\subseteq H$ is a separate hypothesis. A covering-only or at-most-one version would be a different problem.
• The graph. Its vertex type has three kinds of vertices: $T$-vertices $(i,j)$ with class $i\in\{0,1,2,3\}$ ($W,X,Y,Z$), one midpoint per non-diagonal unordered pair of $T$-vertices, and one vertex per element of $H$. The adjacency is exactly the two bullets of p. 390. The graph is fixed by the definition, not described by properties.
• $T$-joins. Edges are unordered pairs (Sym2) and $F$ is a Finset of edges of $G$. Parity uses $\deg_F$. Minimality is "$|F|\le|F'|$ for all $T$-joins $F'$", never an infimum on $\mathbb N$.
• Components. A component of $F$ is a component of the graph with edge set $F$ that contains an endpoint of an edge of $F$. Isolated vertices are never counted, and the empty edge set has $0$ components.
• The degenerate case $q=0$ is included: the graph is empty, $F=\emptyset$ is a minimum $T$-join with $0$ components, and $M=\emptyset$ is a matching.
• Not formalized. Membership of MTSC in NP, polynomial-time computability of the construction, and NP-completeness itself. The platform has no complexity-theory substrate. The Claim is the mathematical statement those rest on.
• Ruled out. The Claim must not be weakened to "exactly $q$ components" or to minimality among $T$-joins with few components, and components must not be counted on the whole vertex type. Each of these changes the statement.

Contributions welcome: proofs of the milestones, general lemmas on $T$-joins (a $T$-join in a graph where $T$ is independent has at least $|T|$ edges), and lemmas on the components of an edge set, which are reusable well beyond this mission.

Selected references

• A. Sebő, E. Tannier, On Metric Generators of Graphs, Mathematics of Operations Research 29(2):383–393, 2004. https://doi.org/10.1287/moor.1030.0070
• E. Korach, M. Penn, Tight integral duality gap in the Chinese postman problem, Mathematical Programming 55:183–191, 1992.
• P. D. Seymour, On odd cuts and plane multicommodity flows, Proceedings of the London Mathematical Society 42:178–192, 1981.
• M. Middendorf, F. Pfeiffer, On the complexity of the edge-disjoint path problem, Combinatorica (cited by Sebő and Tannier as 1998, vol. 8, pp. 103–116) — NP-completeness of deciding $\nu=\tau$.
• M. R. Garey, D. S. Johnson, Computers and Intractability, W. H. Freeman, San Francisco, 1979 — NP-completeness of 3DM.
• A. Frank, A survey on T-joins, T-cuts, and conservative weightings, in Combinatorics, Paul Erdős is Eighty, Vol. 2, 1996, pp. 213–252.
• Related platform item, not reused: UnrelatedSched.ThreeHalves.ThreeDimMatching (Lenstra–Shmoys–Tardos) encodes 3DM with an indexed family of triples and the covering form of a matching, a different encoding from the paper's set $H$ with "exactly one".

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.