Operations Research

Motivation

Demand for many products is not stationary: it rises and falls with the economy, the season, a product's life cycle or a customer's state. Song and Zipkin (1993) (DOI 10.1287/opre.41.2.351) model this by a world-driven demand process: an exogenous Markov chain $A$ (the "state of the world") whose current state sets the rate of a Poisson demand stream. The model contains the classical stationary inventory model as the case of one world state, and it is a standard example of a Markov-modulated decision problem in operations research.

For stationary demand with a fixed order cost, optimal $(s, S)$ policies go back to Scarf (1960) for finite horizons and Iglehart (1963) for the infinite horizon; Veinott (1966) bounded the optimal parameters by quantities computed from the one-period cost alone. This mission formalizes the extension of both results to the fluctuating-demand model (§3.2 of the paper). A companion mission treats the linear order-cost case, in which a world-dependent basestock policy is optimal.

Setting

The world $A$ is a continuous-time Markov chain on a countable set $I$ with generator $(q_{ij})$, $q_i = -q_{ii} = \sum_{j\neq i} q_{ij}$, and bounded rates. While $A = i$, unit demands arrive at Poisson rate $\lambda_i$; shortages are backlogged. An order arrives after a random lead time $L$, independent of the world and the demand. The inventory position $x \in \mathbb Z$ is on-hand stock minus backorders plus stock on order.

Costs: a fixed cost $\bar K$ per order and a unit cost $\bar c$, both paid on arrival; a holding cost rate $h > 0$ and a penalty cost rate $p > 0$; a discount rate $\alpha > 0$. With $\tilde F_L(\alpha) = E[e^{-\alpha L}]$, the discounted costs are $c = \bar c\tilde F_L(\alpha)$ and $K = \bar K\tilde F_L(\alpha)$. If $D^i_L$ is the demand during a lead time from world state $i$ and $\hat C(x) = \max\{-px, hx\}$,

$$C(i, y) = E\big[e^{-\alpha L}\hat C(y - D^i_L)\big].$$

Uniformization at a rate $\mu \ge \sup_i q_i + \sup_i\lambda_i$ turns the problem into a discrete-time dynamic program with $\beta = 1/(\mu+\alpha)$, $\gamma = \beta\mu$ and the myopic cost $G^+(i, y) = (1-\gamma)cy + \beta C(i, y)$. For a terminal cost $W_0$ the $n$-stage costs satisfy the recursion (10):

$$W_n(i, x) = \min_{y\ge x}\{K\delta(y-x) + G_n(i, y)\},$$ $$G_n(i, y) = G^+(i, y) + \beta\lambda_i c + \beta\Big\{\lambda_i W_{n-1}(i, y-1) + \sum_{j\neq i} q_{ij}W_{n-1}(j, y) + (\mu - \lambda_i - q_i)W_{n-1}(i, y)\Big\},$$

where $\delta(z) = 1$ if $z > 0$ and $\delta(0) = 0$. Throughout, Assumption 1, $\alpha\bar c < p$, holds and $K > 0$. The terminal cost is the optimal cost $W_\infty$ of the linear model ($K = 0$); its $G_\infty$ is written $G_0$, and $y^*(i)$ is the smallest minimizer of $G_0(i, \cdot)$.

A function $f : \mathbb Z \to \mathbb R$ is $K$-convex (Definition 2) if $\frac{f(x)-f(x-b)}{b}a + f(x) \le f(x+a) + K$ for all $x$ and all integers $a, b > 0$. The $(r, S)$ policy with parameters $\{(r(i), S(i))\}$ orders up to $S(i)$ when $x \le r(i)$ and the world is in state $i$, and does not order otherwise. With $y^+(i)$ the smallest minimizer of $G^+(i,\cdot)$ and $y^+_{\min} = \min_i y^+(i)$, the paper defines

$$\begin{aligned} S^+(i) &= \min\{y \ge y^+(i) : G^+(i, y) - G^+(i, y^+(i)) > \gamma K\},\\ r^+(i) &= \max\{y < y^+(i) : G^+(i, y) - G^+(i, y^+(i)) > (1-\gamma)K\},\\ r^-(i) &= \max\{y < y^*(i) : G_0(i, y) - G_0(i, y^*(i)) > K\},\\ r^{--}(i) &= \max\{y < y^+_{\min} : G^+(i, y) - G^+(i, y^+_{\min}) > K\}. \end{aligned}$$

Formalization targets

Goal: Theorems 5(e) and 6

Let $S^*_n(i)$ be the smallest minimizer of $G_n(i,\cdot)$ and $r^*_n(i)$ the largest $y < S^*_n(i)$ with $G_n(i, y) > K + G_n(i, S^*_n(i))$. For every $i$ the sequence $(r^*_n(i), S^*_n(i))$ has limit points; for any choice of limit points $(r^*(i), S^*(i))$, the world-dependent $(r, S)$ policy with these parameters is optimal for the infinite-horizon discounted problem, and

$$y^*(i) \le S^*(i) < S^+(i),\qquad r^{--}(i) \le r^-(i) \le r^*(i) \le r^+(i).$$

Milestones

Lemma 4 (uniform bounds on the iterates); Theorem 3 ($K$-convexity of $G_n$, $W_n$ and optimality of an $(r, S)$ rule for each $n$-stage problem); Lemmas 5 and 6 (difference comparisons); Theorem 4 (the bounds above for every $n$); Theorem 5(a)–(d) (convergence of $W_n$, $G_n$, the $(r, S)$ property of limit points, and the optimality equation (2)).

Significance

The result shows that the classical $(s, S)$ structure survives Markov modulation of demand with an infinite world space and stochastic lead times: a stationary policy whose two parameters depend only on the current world state is optimal over the infinite horizon. The bounds of Theorem 6 locate those parameters in an interval computed from the myopic cost $G^+$ and the linear model alone, uniformly in the horizon.

The results are proved in the paper, except that Theorem 5 refers to Iglehart (1963) and Lemma 4 to Song's thesis. To our knowledge none of them has a machine-checked proof. A formalization would also produce reusable machinery: $K$-convexity on the integers, the Scarf-type inductive argument with a countable world state, and the passage from finite-horizon to infinite-horizon optimality for a nonnegative-cost Markov decision process with unbounded costs.

Difficulty

The one-period cost is unbounded in $x$ and the world space may be infinite, so the usual contraction argument for discounted dynamic programs does not apply. Convergence of $W_n$ needs the uniform bound of Lemma 4. Optimality of the limit policy needs a separate argument, because a pointwise limit of $(r, S)$ rules need not exist: the parameter sequences are only known to have limit points. The lower bounds $r^-$ and $r^{--}$ hold only because the terminal cost is the linear model's optimal cost, which makes the difference comparisons of Lemma 6 possible; the paper notes that Lemma 6 depends on this choice of $W_0$.

Formalization scope

All definitions live in the namespace SongZipkinFluct.FixedCost. Inventory positions and order-up-to levels are integers. The demand law $D^i_L$ is defined through uniformization at rate $\mu$, as an exact series representation of the Markov-modulated Poisson count, and the lead time is a probability law on $[0,\infty)$ independent of the rest. The standing conventions $h, p, \alpha > 0$, $\bar c, \bar K \ge 0$, $\mu > 0$ and $\mu \ge q^* + \lambda^*$ are hypotheses of the model. Assumption 1 and $\bar K > 0$ are hypotheses of each theorem.

The iterates $W_n$ are defined by the recursion (10), with the minimum written as an infimum over integers $y \ge x$. $W_\infty$ and $G_\infty$ are the suprema over $n$, which are finite and equal the limits by Lemma 4 and Theorem 3. Every minimizer and every extremal integer ($y^+$, $y^+_{\min}$, $y^*$, $S^*_n$, $r^*_n$, $S^+$, $r^+$, $r^-$, $r^{--}$) is passed through its defining property, never through sInf/sSup on $\mathbb Z$. The goal also asserts that all of them exist, so its hypotheses can be met. A limit point of an integer sequence is a value taken infinitely often.

Optimality is over all deterministic history-dependent feasible policies and from every initial state. Costs are valued in $[0,\infty]$, and a policy's cost is the supremum of its finite-horizon discounted costs in the uniformized problem (1). Restricting the comparison to $(r, S)$ or stationary policies would trivialize the goal and is ruled out. $K$-convexity is the integer version of Definition 2, not convexity over $\mathbb Z$-scalars.

Welcome contributions: $K$-convexity calculus on $\mathbb Z$, convergence of the uniformized demand series, Lemma 4, and an Iglehart-type limit argument for countable-state Markov decision processes with nonnegative costs.

Selected references

• J.-S. Song and P. Zipkin, Inventory Control in a Fluctuating Demand Environment, Operations Research 41(2):351–370, 1993. https://doi.org/10.1287/opre.41.2.351
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• A. F. Veinott, Jr., On the Optimality of (s, S) Inventory Policies: New Conditions and a New Proof, SIAM Journal on Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.

Motivation

A single stock of one product often serves customers of different importance: emergency and routine orders for spare parts, contract and spot customers, high- and low-priority patients for a blood bank. When stock runs low, the question is not only how much to order but how much of the remaining stock to hand to the less important customers now, and how much to hold back for more important demand that may still arrive. Stock rationing policies answer this question with critical rationing levels: demand of a class is served only while the stock stays above that class's level.

Topkis (1968) studied this problem as a finite-horizon dynamic program with $n$ demand classes, nonstationary costs and demands, and an arbitrary degree of backlogging. His Theorem 1 shows that, when each interval has either complete backlogging or none, a policy given by critical levels $\bar z_t^1 \ge \dots \ge \bar z_t^n$ is optimal. This mission concerns his Theorem 3, which treats the case of complete backlogging: the critical levels of a class do not depend on what happens in the classes below it.

Timeline. Veinott (1965) considered $n$ demand classes but imposed the policy with all critical levels equal to $0$. Topkis's 1966 report treated $n = 2$, partially duplicated independently by Evans (1968) and by Kaplan's 1966 report "Stock Rationing", in which, according to Topkis, the result of Theorem 3 was used implicitly. Topkis (1968) extended the analysis to $n$ classes and stated Theorem 3 explicitly.

Setting

A period is divided into $k$ intervals, indexed backwards: interval $t$ is followed by $t - 1$ further intervals, and interval $k$ is the first. There are $n$ demand classes; class $n$ is the most important. In interval $t$ a random demand vector $d_t = (d_t^1, \dots, d_t^n) \ge 0$ with law $\mu_t$ and finite means arrives; demands in different intervals are independent. Given the stock $z$ and the outstanding demand $B = b + d_t$ (backlog $b$ plus new demand), the decision is the vector $u$, $0 \le u \le B$, of demand left unsatisfied; the stock drops to $w = z - \mathbf 1 \cdot (B - u) \ge 0$. A penalty $p_t \cdot u$ and a holding cost $h_t(w)$ are charged, and the backlog carried into the next interval is $a_t u$, with $a_t = 1$ for complete backlogging. At the end of the period a salvage cost $g_0(z, b) = v_1(z) + v_2(z - \mathbf 1 \cdot b)$ is charged.

The standing assumptions are: $h_t$ convex and continuous on $[0,\infty)$; $v_1$ convex and continuous on $[0,\infty)$; $v_2$ convex and continuous on $\mathbb R$ with $\lim_{w \to -\infty} D^+ v_2(w) > -\infty$; and $0 \le p_t^1 \le \dots \le p_t^n$. The minimal expected cost satisfies the recursion (1):

$$f_t(z, B) = \inf_{\substack{0 \le u \le B \\ w = z - \mathbf 1\cdot(B-u) \ge 0}} \big[p_t \cdot u + h_t(w) + g_{t-1}(w, a_t u)\big], \qquad g_t(z, b) = \mathbb E\, f_t(z, b + d_t).$$

With $\delta_j$ the $j$-th unit vector, the critical rationing level $\bar z_t^j$ is $+\infty$ if $w \mapsto p_t^j w + h_t(w) + g_{t-1}(w, a_t w \delta_j)$ is strictly decreasing on $[0, \infty)$, and is the smallest minimizer of that function on $[0,\infty)$ otherwise. $D^+$ denotes a right derivative.

Formalization targets

Goal: Theorem 3

Assume $a_{t+1} = a_t = \dots = a_1 = 1$ and that the demands of different classes are independent in each interval. Fix a class $j$. Then for two instances of the model that differ only in the penalties $p_i^m$ of the classes $m \le j - 1$ and in the demand distributions of the classes $m \le j$,

(a) the marginal quantities

$$D_z^+ g_t(z, z\delta_j) \quad\text{and}\quad D_\varepsilon^+ g_t\big(w, \varepsilon(\delta_j - \delta_s) + b\big)\big|_{\varepsilon = 0} \quad (s > j,\ b^s > 0)$$

coincide, and

(b) the critical rationing levels $\bar z_{t+1}^j$ coincide.

Milestones

1. The claim in the proof of Theorem 3 (p. 173): for $j < s$ and $B^s > 0$, $D_\varepsilon^+ g_t(z, \varepsilon(\delta_j - \delta_s) + B)|_{\varepsilon=0}$ is independent of $B^1, \dots, B^j$.
2. Theorem 3 (a) on its own, from which the page derives (b).

Significance

The result. Theorem 3 reduces the size of the problem. Under complete backlogging, class 1 demand does not influence any critical rationing level, and the class-$j$ critical levels can be found from a problem with only the $n - j + 1$ classes $j, \dots, n$, with a degenerate demand distribution for class $j$. Since computing the levels requires tabulating functions of several variables, which Topkis calls prohibitive for large $n$, this is the observation that makes the levels of the most important classes computable.

Formalizing it. The theorem is proved in the paper by a short sketch that points to two case formulas, (16) and (17), to Theorem 1 (c), and to an interchange of expectation and right derivative. A machine-checked proof would supply the induction, the case analysis and the interchange in full. No formalization of any part of Topkis's paper is known: the result is proved on paper, not formalized.

Difficulty

The obvious argument is an induction on $t$ showing that $g_t$ itself does not depend on the lower classes. It fails: $g_t$ does depend on the penalties and demands of every class, since lower-class demand is still served and penalized. Only certain directional derivatives are invariant, and these derivatives depend on the critical levels of every class $l \ge j$ and on the optimal rationing decision, which themselves change from one instance to the other unless the invariance is already known for the previous interval. The derivatives are one-sided, may be $-\infty$ at the boundary, and must be passed through an expectation.

Formalization scope

The Lean development, in namespace TopkisRation.Backlog, fixes these conventions:

• classes are Fin n (class $j$ of the paper is index $j-1$); intervals are natural numbers counted backwards; vectors are ordered pointwise;
• $f_t$ is defined by the recursion (1), with sInf for the infimum and the Bochner integral for $\mathbb E$, and every statement restricts to $z \ge 0$, $b \ge 0$;
• $D^+$ is an extended-real right derivative (a liminf of difference quotients); $D_z^+ g_t(z, z\delta_j)$ is the derivative along the ray in which the stock and the class-$j$ backlog move together;
• $\bar z_t^j$ takes values in $\mathbb R \cup \{+\infty\}$ and is specified by a predicate (smallest minimizer, or $+\infty$ for a strictly decreasing function), never by a real sInf;
• the limit in (B) is read as "$D^+ v_2$ is bounded below";
• independence of the classes in interval $i$ is independence of the coordinate maps under $\mu_i$.

"Does not depend on" is stated with two instances $M$, $M'$ that agree on every datum the conclusion uses except the freed ones: the same $k$, $v_1$, $v_2$, the same $h_i$ and the same $p_i^m$ for $m \ge j$ in intervals $i \le t+1$, and the same class-$m$ marginal law for $m > j$ in every interval. The penalty of class $j$ itself is not freed. Data of intervals beyond $t+1$ and the ordering cost are unconstrained. Part (b) is stated for arbitrary critical levels of the two instances; existence of critical levels is part of the paper's §1 and is not assumed away, so (b) is not vacuous. The goal does not assume the p. 173 claim, the case formulas (16)–(17), or Theorem 1. Encoding "does not depend" as "is a function of the remaining data" is ruled out.

Needed infrastructure: one-sided derivatives of convex functions and their monotone limits, interchange of right derivative and expectation for convex integrands, and the convexity and rationing-policy results of §1 (Theorem 1, Lemma 2). These are reusable for the other missions of this series. Contributions welcome: proofs of the milestones, a formal version of (16)–(17), and the existence of critical levels.

Selected references

• D. M. Topkis, Optimal ordering and rationing policies in a nonstationary dynamic inventory model with n demand classes, Management Science 15(3):160–176, 1968. https://doi.org/10.1287/mnsc.15.3.160
• A. F. Veinott Jr., Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13(5):761–778, 1965. https://doi.org/10.1287/opre.13.5.761
• R. V. Evans, Sales and restocking policies in a single item inventory system, Management Science 14(7):463–472, 1968. https://doi.org/10.1287/mnsc.14.7.463
• A. Kaplan, Stock Rationing, report, December 1966 (reference [4] of Topkis 1968).

Motivation

A firm that holds a single stock of one product often faces demand from several classes of customers that differ in importance: emergency and routine orders for spare parts, contract and spot customers, high- and low-priority users of a military supply system. When stock runs low it can pay to refuse a less important demand now in order to keep stock for a more important demand that may arrive later. Veinott (Operations Research 13 (1965), 761–778) studied a dynamic inventory model with several demand classes but required the specific policy that serves every class whenever stock is available. Topkis (Management Science 15 (1968), 160–176) treated the dynamic version, in which demands arrive over the intervals of a period between two procurements, and showed that the optimal rationing policy has a simple form described by one critical rationing level per class and interval.

This mission concerns how those critical levels move over time. The paper's Theorem 2 gives a condition under which, without backlogging, the levels are monotone in the interval index, so that rationing is at least as strict early in the period as late in it. It is the second of four missions on the paper; the first establishes the critical-level policy itself (Theorem 1).

Setting

A period is divided into $k$ intervals, indexed backwards: interval $t$ has $t-1$ intervals after it, so interval $k$ is the first and interval 1 the last. There are $n$ demand classes, class $n$ the most important. At the start of interval $t$ the demand vector $d_t = (d_t^1,\dots,d_t^n)$ is observed; demands of different intervals are independent, and each class has a finite mean. With backlog $b$ and stock $z$, one decides the vector $u$ of outstanding demand left unsatisfied, $0 \le u \le B = b + d_t$, using $\mathbf 1\cdot(B-u)$ units of stock, so the stock at the end of the interval is $w = z - \mathbf 1\cdot(B-u) \ge 0$. A fraction $a_t \ge 0$ of the unsatisfied demand is carried as backlog $a_t u$ into the next interval: $a_t = 1$ is complete backlogging, $a_t = 0$ none.

The costs are a penalty $p_t\cdot u$ with $0 \le p_t^1 \le \dots \le p_t^n$ (Assumption (C)), a holding cost $h_t(w)$ continuous and convex on $[0,\infty)$ (Assumption (A)), and a salvage cost $v_1(z) + v_2(z - \mathbf 1\cdot b)$ at the end of the period, with $v_1$, $v_2$ convex and continuous and $D^+v_2$ bounded below (Assumption (B)). Here $D^+$ denotes the right derivative. The optimal costs satisfy the recursion (1)

$$f_t(z,B) = \inf_{0\le u\le B,\ w = z-\mathbf 1\cdot(B-u)\ge 0}\bigl[p_t\cdot u + h_t(w) + g_{t-1}(w, a_t u)\bigr],\qquad g_t(z,b) = \mathbb E f_t(z, b+d_t),$$

with $g_0(z,b) = v_1(z) + v_2(z-\mathbf 1\cdot b)$.

With $\delta_j$ the $j$-th unit vector, the critical rationing level $\bar z_t^j\in[0,\infty]$ is $+\infty$ if $\varphi_t^j(w) = p_t^j w + h_t(w) + g_{t-1}(w, a_t w\delta_j)$ is strictly decreasing on $[0,\infty)$, and the smallest minimizer of $\varphi_t^j$ on $[0,\infty)$ otherwise. Under the paper's Theorem 1 the rationing level policy $u^j = (B^{(j)} - z + \bar z_t^j)^+\wedge B^j$, with $B^{(j)} = \sum_{i\ge j}B^i$, is optimal: class $j$ is served from stock only while the stock stays at or above $\bar z_t^j$.

Formalization targets

Goal: Theorem 2 (p. 170)

Let $1\le t$, $t+1\le k$, $a_{t+1} = a_t = 0$, and $a_i\in\{0,1\}$ for $i\le t$. If

$$p_{t+1}^j + \lim_{z\to\infty}D^+h_{t+1}(z) \le p_t^j, \qquad\text{then}\qquad \bar z_t^j \le \bar z_{t+1}^j .$$

Milestones

1. Lemma 5 (p. 168). For $b\le\bar b$: $D_z^+g_t(z,\bar b)\le D_z^+g_t(z,b)$.
2. Lemma 6 (p. 168). For $z\le\bar z$ and $y\ge 0$: $g_t(\bar z,b)-g_t(z,b)\le g_t(\bar z+\mathbf 1\cdot y,b+y)-g_t(z+\mathbf 1\cdot y,b+y)$.
3. (12) (p. 170). If $b=0$ or $a_t=1$, for small $\varepsilon>0$ and every $d\ge0$, the difference quotients of $f_t(\cdot,b+d)$, $f_t(\cdot,b)$ and $h_t+g_{t-1}(\cdot,b)$ at $z$ are ordered.
4. Lemma 7 (p. 169). If $a_t = 1$ or $b = 0$: $D_z^+g_t(z,b)\le D^+h_t(z)+D_z^+g_{t-1}(z,b)$.

Significance

The result says that, in intervals without backlogging, the stock reserved against a class is never larger late in the period than early in it, provided the class's penalty in the earlier interval plus the eventual marginal holding cost does not exceed its penalty in the later interval. Together with Theorem 1 it reduces the dynamic rationing problem to a family of one-dimensional critical numbers with a known order in both the class and the time index. The paper's example on p. 170 shows that the analogous monotonicity fails with backlogging, so the hypothesis $a_{t+1} = a_t = 0$ is essential.

The paper's proofs are complete but informal: they interchange expectation and right-derivative limits, and rest on Lemma 2 (convexity and attainment) and Theorem 1 (c). No part of this paper has been machine-checked. This mission produces formal statements of Theorem 2 and the three lemmas it rests on; contributions that formalize the known proofs, or that settle whether the extra hypothesis on earlier backlogging fractions (below) can be dropped, are equally in scope.

Difficulty

The central difficulty is Lemma 7, the comparison of the marginal value of stock in two consecutive intervals. The value functions are defined through an infimum and an expectation, so they are convex but not differentiable, and the minimizer in (1) changes regime each time the stock crosses a critical level; differentiating (1) directly is not available. Right derivatives may also be $-\infty$ at $z = 0$, and statements about them have to survive an interchange of expectation and a one-sided limit. The lemma depends on the optimal policy of Theorem 1, which is the subject of the first mission of this series. The claim of Lemma 7 is false when $a_t = 0$ and $b\ne0$ (p. 168), so no argument can ignore the case split.

Formalization scope

• Classes are Fin n (paper class $j$ is index $j-1$); intervals are natural numbers counted backwards; vectors are Fin n → ℝ with the pointwise order.
• $f_t$ and $g_t$ are defined by the recursion (1) with sInf and the Bochner integral, and every statement restricts to $z\ge0$, $b\ge0$, where the paper's Lemma 2 (proved in the first mission of the series) makes the infimum finite and attained and the integrand integrable.
• $D^+$ is an extended-real liminf of right difference quotients, never a real derivWithin, which would return $0$ where the right derivative is $-\infty$. Sums of right derivatives are taken in EReal.
• The standing assumptions (A), (B), (C), $a_t\ge0$, and probability laws on $[0,\infty)^n$ with finite means are bundled in Model.Standing; (B)'s limit condition is read as "$D^+v_2$ is bounded below".
• Critical levels are values in WithTop ℝ satisfying the defining predicate (strictly decreasing ⇒ $+\infty$, otherwise the smallest minimizer); the theorem holds for any such choice. Their existence is a milestone of the first mission; a sanity check exhibits a model in which all hypotheses of Theorem 2 hold with $\bar z_t^j = \bar z_{t+1}^j = 0$.
• The penalty hypothesis is stated for all $z\ge0$ instead of as a limit; these agree because $D^+h_{t+1}$ is nondecreasing.
• Disclosed addition: Theorem 2 is stated with $a_i\in\{0,1\}$ for all $i\le t$, the hypothesis of Lemma 7 that its proof uses; the printed statement names only $a_{t+1}=a_t=0$. The hypothesis on $a_i$ in Lemmas 5–7 is required only for $i\le t$.
• A formalization in which the goal assumes Lemma 7's inequality, or any property of $D^+g_t$, would be trivial and is excluded: those facts appear only as milestones.

Selected references

• D. M. Topkis, Optimal ordering and rationing policies in a nonstationary dynamic inventory model with n demand classes, Management Science 15(3) (1968), 160–176. https://doi.org/10.1287/mnsc.15.3.160
• A. F. Veinott, Jr., Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13(5) (1965), 761–778. https://doi.org/10.1287/opre.13.5.761

Motivation

A single server shared by several classes of jobs must decide, at every moment, which class to work on. When each class $k$ incurs a linear delay cost $c_k$ per unit of waiting time and needs mean service time $1/\mu_k$, the classical $c\mu$ rule (serve the waiting class with the largest $c_k\mu_k$) minimizes expected cost in many settings, from the M/G/1 queue to discrete-time models (Buyukkoc, Varaiya and Walrand, Adv. Appl. Probab. 1985). Linear costs are a strong restriction: in telecommunications, manufacturing and service systems the penalty for delay often grows faster than linearly, and with convex costs the static priority order of the $c\mu$ rule is no longer optimal.

Van Mieghem (Ann. Appl. Probab. 1995) proposed the generalized $c\mu$ rule: with nondecreasing convex delay costs $C_k$ and marginal costs $c_k = C_k'$, serve the class with the largest index $\mu_k c_k(\cdot)$ evaluated at its current delay or workload. The paper proves that, in heavy traffic, this dynamic index policy is asymptotically optimal among all scheduling policies, including policies whose scaled workloads do not converge. This mission formalizes that result and the chain of propositions it rests on.

Setting

There are $d$ job classes. In the $n$th system, the $i$th class-$k$ job arrives after an interarrival time $u^n_{k,i}>0$ and needs service $v^n_{k,i}\ge 0$. $A^n_k(t)$ counts class-$k$ arrivals in $[0,t]$ and $S^n_k(x)$ counts class-$k$ completions within $x$ units of server time. A policy is an allocation $T^n=(T^n_k)$, where $T^n_k(t)$ is the time in $[0,t]$ spent on class $k$. From it come the headcount $N^n_k = A^n_k - S^n_k\circ T^n_k$, the workload $W^n_k(t) = V^n_k(A^n_k(t)) - T^n_k(t)$ (work present in class $k$), the class-FIFO delay $\tau^n_k(t)=\inf\{s\ge0: W^n_k(t)\le T^n_k(t+s)-T^n_k(t)\}$ of a job arriving at $t$, and the cumulative cost $J^n(t)=\sum_k\sum_{i\le A^n_k(t)} C^n_k(\tau^n_{k,i})$. Feasible policies are continuous, nondecreasing and work conserving.

The $n$th system runs on $[0,n]$ and is studied at the diffusion scale: $\tilde W^n_k(t)=W^n_k(nt)/\sqrt n$, $\tilde N^n_k$, $\tilde\tau^n_k$ likewise, and $\tilde J^n(t)=J^n(nt)/n$. Arrival and service processes expand as $A^n(nt)=n\bar A^n(t)+\sqrt n\,\tilde A^n(t)+o(\sqrt n)$ and $S^n(nt)=n\bar S^n(t)+\sqrt n\,\tilde S^n(t)+o(\sqrt n)$. Assumption 1 asks that these terms converge, with rates $\lambda=\bar A^{*\prime}>0$, $\mu=\bar S^{*\prime}>0$, and that the system is in heavy traffic: $\sqrt n(R^n_+-e)\to\tilde c^*$, where $R^n_k=(\bar S^n_k)^{-1}\circ\bar A^n_k$ and $\rho_k=\lambda_k/\mu_k$ is the traffic intensity. Assumption 2 asks that the costs scale, $C^n(\sqrt n\,\cdot)\to C^*(\cdot)$, and Assumption 3 that $C^*$ be strictly convex and $\mathcal C^1$.

The scaled total workload has a policy-independent limit $\tilde W^*_+=\varphi(\tilde L^*_++\tilde c^*)$, with $\varphi$ the one-dimensional reflection map. The key static problem splits a total $y$ among classes:

$$g\circ y(t)=\arg\min_{x\in\mathbb R^d_+,\ \sum_k x_k=y(t)}\ \sum_k\lambda_k(t)\,C^*_k\Big(\frac{x_k}{\rho_k(t)}\Big). \tag{43}$$

Formalization targets

Goal: Proposition 7

Under Assumptions 1–3, for feasible policies with

$$\max_{k,l}\Big\|\mu_kc^*_k\Big(\frac{\tilde W^n_k}{\rho_k}\Big)-\mu_lc^*_l\Big(\frac{\tilde W^n_l}{\rho_l}\Big)\Big\|\to0, \tag{51}$$

the costs and delays converge,

$$\tilde J^n\to\tilde J^*=\sum_k\int\lambda_kC^*_k\Big(\frac{[g\circ\tilde W^*_+]_k}{\rho_k}\Big)dt,\qquad \tilde\tau^n\to\frac{g\circ\tilde W^*_+}{\rho}. \tag{52–53}$$

Milestones

Lemma 1 and Proposition 2 (jumps (33)–(34), first-order allocation (27), total workload (32), boundedness, equivalences (35)); Proposition 3 ($\mu_k\tilde W^n_k-\tilde N^n_k\to0$); Proposition 4 (Little's law); Proposition 5 (converging policies); uniqueness and continuity of $g$ (§4.1); the Kuhn–Tucker characterization (46)–(50); and Proposition 6, the lower bound

$$\liminf_n\tilde J^n(t)\ge\tilde J^*(t)\qquad\text{for every feasible policy sequence.}\tag{44}$$

Proposition 6 is what makes Proposition 7 an optimality statement; it is a separate milestone and not part of the goal.

Significance

The result. Proposition 7 identifies a simple, myopic index rule that is optimal at the diffusion scale for every time simultaneously, for arbitrary convex delay costs and nonstationary rates. It extends the $c\mu$ rule beyond linear costs, links it to the "hug the optimal workload curve" policies of heavy-traffic control, and shows that the instantaneous allocation problem (43) is all that matters asymptotically. Later work on Brownian control of multiclass queues and on convex-cost scheduling (Mandelbaum and Stolyar 2004) builds on this.

Formalizing it. The paper's proofs are short and informal at several points, and the formalization makes these points explicit: the domain of every uniform limit, the policy class, and the reading of $\mu$. No part of this paper has a machine-checked proof. A completed mission would give a verified heavy-traffic analysis of a multiclass single-server queue at the sample-path level, the first on the platform with a deterministic diffusion scaling and an explicit reflection map.

Difficulty

The obvious route is to show that $\tilde W^n$ converges and then pass to the limit in the cost. That fails for the lower bound: Proposition 6 must cover policies whose class workloads never converge (polling-type policies), so it cannot use compactness of $\tilde W^n$ and must instead compare the cost of an arbitrary split of $\tilde W^n_+$ with the optimal split, locally in time. For the goal, (51) controls only the indices, so the convergence of $\tilde W^n$ must be extracted from (51) through the inverse marginal costs, the convergence of the total workload, and the Kuhn–Tucker conditions of (43). Delay convergence then needs a uniform control of $\tilde T^n$ over windows of length $O(n^{-1/2})$, and cost convergence needs the convergence of the costs $C^n$ applied to delays of order $\sqrt n$.

Formalization scope

Lean namespace GenCMu.HeavyTraffic. The development is deterministic and works one sample path at a time; the stochastic version (Proposition 8) is not part of this mission. Conventions committed to:

• Classes are Fin d; job indices start at $1$; every "→" between functions is uniform convergence ((11)), on $[0,1]$ unless stated; $\liminf$ is written as "eventually $\ge$ bound $-\varepsilon$".
• The scaled processes are defined exactly, with $\bar T^n=\bar L^n=R^n$ ((69), (75)); the inverse in (14) is the generalized inverse on $[0,1]$.
• The $o(n^{1/2})$ terms of (12)–(13) are uniform in $t$. The trends converge in $\mathcal C^1$, not only in $\mathcal C$. Without this, $\bar A^n,\bar S^n$ can oscillate on the $n^{-1/2}$ scale and (33)–(34) and Proposition 3 fail. The service expansion holds on server time $[0,2n]$, so that for $d=1$ in heavy traffic the service times of jobs arriving before $n$ are covered.
• $\mu_k$ in (20), (36), (41), (46)–(51) is $\mu_k(R^*_k(t))$, the service rate in real time, so $\rho_k=\lambda_k/\mu_k(R^*_k)$.
• (38) is uniform on compacts. Assumption 3's interior clause is imposed where $\tilde W^*_+(t)>0$. At $\tilde W^*_+(t)=0$ no point of $\Omega=\{0\}$ is interior, and the literal clause would make the goal vacuous.
• For the heavy-traffic limit and goal, feasible policies satisfy F1 (without adaptedness), F2–F4, $W_k\ge0$, work conservation (used by $W^n_+=\varphi(X^n)$), and every job finishes. Proposition 6 uses a broader cost-admissible class that permits idleness with work waiting. Class-FIFO is built into the delay (9).
• The delays of jobs arriving near the horizon depend on post-horizon service. We require the allocation on every bounded diffusion-scale window after $n$ to advance at the first-order rates $\rho_k(1)$. This explicit boundary hypothesis keeps Propositions 2, 4, 5, and 7 on the paper's full $[0,1]$.
• Lemma 1 additionally assumes a common Lipschitz bound on the first-order partial-sum trends. Uniform convergence alone permits jumps of order $\sqrt n$; the bound repairs that omission. Uniqueness of the solution of (43) is stated under strict convexity: "convex increasing" (p. 820) does not give it. (35) is stated without the implication from $\tilde\tau^n$ back to $\tilde W^n$, which fails in the uniform topology.
• $\tilde J^*$ integrates the optimal value of (43), so Proposition 6 needs no choice of minimizer.

A trivializing formalization is ruled out: no theorem assumes the convergence of $\tilde W^n$ or $\tilde W^n_+$, the uniqueness of minimizers, or the lower bound, and the joint satisfiability of all hypotheses has been checked in Lean for $d=1$.

Needed infrastructure: sample-path reflection-map estimates, counting/partial-sum inversion with uniform $o(\sqrt n)$ errors, parametric convex optimization (Berge's theorem for (43)), and Riemann-sum arguments for the lower bound. The reflection-map and inversion lemmas are reusable beyond this mission. Contributions to any milestone are welcome. The definitions are frozen, so a proof that needs a different definition should be raised in the discussion.

Selected references

• J. A. Van Mieghem, Dynamic Scheduling with Convex Delay Costs: The Generalized cμ Rule, Ann. Appl. Probab. 5(3) (1995) 809–833. https://doi.org/10.1214/aoap/1177004706
• C. Buyukkoc, P. Varaiya, J. Walrand, The cμ rule revisited, Adv. Appl. Probab. 17 (1985) 237–238.
• J. M. Harrison, Brownian Motion and Stochastic Flow Systems, Wiley, 1985 (reflection map).
• D. L. Iglehart, W. Whitt, Multiple channel queues in heavy traffic. I, Adv. Appl. Probab. 2 (1970) 150–177.
• A. Mandelbaum, A. L. Stolyar, Scheduling flexible servers with convex delay costs: heavy-traffic optimality of the generalized cμ-rule, Oper. Res. 52(6) (2004) 836–855. https://doi.org/10.1287/opre.1040.0156

Motivation

Weighted voting models assign a coalition a win when its combined vote reaches a quota. The Shapley value measures a player's contribution by averaging the change it makes when added to every possible predecessor coalition. This is straightforward to define for a finite list of voters, but a voting body may contain a few major holders and a very large population of individually small holders. A calculation made for a finite approximation should then have a stable meaning as the small holdings are divided more finely. Milnor and Shapley's oceanic game gives that question a precise form and asks whether its major-player values agree with the limits of finite weighted majority games. Milnor and Shapley, RAND RM-2649 (1961).

The question matters whenever a finite voting model is used to represent a diffuse electorate or ownership base. Without a continuity result, the measured power of a major voter could depend on how an otherwise identical mass of minor votes was artificially split. The memo's Theorem 1 establishes the required stability under an explicit small-weight condition. The result is a known theorem from the 1961 memorandum; the task here is its Lean formalization, including the mathematical objects that make its statement meaningful.

Setting

Fix a finite set $M=\{1,\ldots,m\}$ of major players, with nonnegative weights $w_i$. The ocean is a continuum of individually insignificant voters represented by the unit interval $I=[0,1]$, with total weight $\alpha>0$. A coalition's vote is its major-player weight plus $\alpha$ times the Lebesgue measure of its oceanic part. It wins when that vote reaches a quota $c\ge0$. The formal development uses Fin m for $M$ and real weights; the underlying voting rule is the one in §2 of the memorandum. Milnor and Shapley, §2.

To assign a value to a major player, insert each major player independently and uniformly into the ordered ocean. A position vector $x=(x_1,\ldots,x_m)$ lies in the cube $I^m$. Write $P(t)=\{j\in M:x_j<t\}$ and $w(S)=\sum_{j\in S}w_j$. Major player $i$ is pivotal when the predecessor weight is below the quota and adding $i$ reaches it, in the memo's weak-boundary form

$$w(P(x_i))+\alpha x_i\le c\le w(P(x_i))+w_i+\alpha x_i.$$

The oceanic major-player value $\phi_i$ is the probability of this event. Since the insertion positions are uniform, it is also the $m$-dimensional Lebesgue volume of the corresponding set $A_i\subseteq I^m$. Equalities at boundary positions have zero volume. Milnor and Shapley, (2.3)–(2.4), pp. 4–5.

At stage $\ell$, the finite approximation has the same $m$ major players, followed by $n_\ell$ minor players with nonnegative weights $a_{j,\ell}$. Its quota and major weights are $c_\ell$ and $w_{i,\ell}$. A coalition has value one if its weight is at least $c_\ell$, and zero otherwise. The finite-game value $\phi_{i,\ell}$ is the Shapley value of that coalition function. The published Shapley-value definition is reused for this general finite-game object; only the quota game and its oceanic limit are defined for this mission. Milnor and Shapley, Appendix (A.1), (A.4).

Formalization targets

Theorem 1: continuity of major-player values

The principal target says that if quotas and major weights converge, the total minor weight tends to $\alpha$, and every minor weight becomes small, then each major-player value converges:

$$c_\ell\to c,\quad w_{i,\ell}\to w_i,\quad \sum_j a_{j,\ell}\to\alpha>0,\quad \max_j a_{j,\ell}\to0 \quad\Longrightarrow\quad \phi_{i,\ell}\to\phi_i.$$

This is Theorem 1, equations (3.1)–(3.2), of the memorandum. Its conclusion refers to the pivotal-probability definition of $\phi_i$ above. Milnor and Shapley, Theorem 1, p. 6.

Supporting statements

The milestone list follows three statements present in the source: equation (3.4) partitions $A_i$ by the predecessor set $S$; equations (3.5)–(3.6) give the volume of each part as a one-variable integral with clamped endpoints; and Appendix (A.1)–(A.3) states the finite-game limit as a sum of those integrals. Their shared expression is

$$L_i(c,w,\alpha)=\sum_{S\subseteq M\setminus\{i\}}\int_{[0,1]\cap[(c-w(S)-w_i)/\alpha,(c-w(S))/\alpha]} t^{|S|}(1-t)^{m-|S|-1}\,dt.$$

The appendix's limit statement concerns $L_i$; Theorem 1 concerns $\phi_i$. Both are separate targets in the formalization. Milnor and Shapley, §3 and Appendix.

Significance

The theorem makes the major-player value independent of a particular fine division of the minor vote, provided the total minor weight and the other parameters converge as stated. The same oceanic game can therefore stand for many finite approximating sequences. The integral expression also gives a precise comparison point between finite Shapley values and the geometric definition by pivotal volume. Milnor and Shapley, §1 and Theorem 1.

The mathematical result is proved in the cited memorandum, and its appendix recapitulates a limit theorem from the preceding work in the series. The formalization work is to state and prove these known claims over Lean's finite index types, Lebesgue measure, integrals, and limits. Reusable components include the quota-game characteristic function and the interface between a finite Shapley value and a changing number of minor players. The mission does not claim that the historical theorem is open, nor that these target statements already have machine-checked proofs.

Difficulty

The number of minor players changes with $\ell$, so the finite Shapley sum does not have a fixed set of coalitions. Merely taking a limit term by term in that sum does not justify its limit: the number and weights of the terms also change. The condition that the largest minor weight tends to zero controls a triangular family of games, while the oceanic definition is a measure of a geometric pivotal event. Matching the two descriptions requires care at the quota boundaries and at intervals that may be empty. These are the central issues represented by the appendix milestone and by equations (3.4)–(3.6). Milnor and Shapley, §3 and Appendix.

Formalization scope

The Lean model uses Fin m for major players and Fin (n l) for minor players at stage $l$, concatenated with majors first. It uses a real-valued quota characteristic function, the published finite Shapley-value definition, and product Lebesgue volume on the cube $[0,1]^m$ for uniform insertion positions. The predecessor relation is strict, $x_j<x_i$, exactly as in §2; the complementary cell relation is weak. The pivotal inequalities follow (2.4), and the oceanic value is defined from their volume. Defining it as $L_i$ would make the comparison demanded by Theorem 1 empty, so that equality remains a theorem-level obligation.

The source defines oceanic games with $c\ge0$, $w_i\ge0$, and $\alpha>0$. The finite approximants are read as weighted majority games with nonnegative weights; that condition is explicit in Lean. No sign condition is imposed on the stage quotas $c_\ell$, since (3.2) states none (only the limit satisfies $c\ge0$). The statement does not impose the footnote's upper bound $c\le w(M)+\alpha$ because Theorem 1 only concerns major-player values, which are zero in a null game. An empty minor list is permitted at an early stage. Rather than taking the maximum of an empty list, Lean says that for each $\varepsilon>0$, all minor weights are eventually at most $\varepsilon$; with nonnegative weights this is the paper's vanishing-maximum condition. A positive limiting ocean weight also excludes an eventually empty minor population.

The integral in (A.3) is a set integral over the stated intersection of closed intervals, so an empty intersection contributes zero. For (3.5), the endpoints are clamped to $[0,1]$. The condition $S\subseteq M\setminus\{i\}$ ensures $m-|S|-1$ is nonnegative before it is represented as a natural-number exponent. Contributions that strengthen the measure-theoretic partition, the cell-volume computation, or the varying-population finite limit are within scope; a proof may use other intermediate lemmas while keeping the sourced target statements unchanged.

Selected references

• John W. Milnor and Lloyd S. Shapley, Values of Large Games, II: Oceanic Games, RAND Research Memorandum RM-2649, 1961. RAND publication page.
• Lloyd S. Shapley and Norman Shapiro, Values of Large Games, I: A Limit Theorem, RAND Research Memorandum RM-2648, 1960. RAND publication page.

Motivation

Two-stage stochastic programming with recourse models a decision taken in two steps: a first-stage decision $x_1$ is fixed before a random outcome $s$ is observed, and a recourse decision $x_2(s)$ is taken afterwards, once $s$ is known. The model goes back to Dantzig (1955) and Beale (1955) and is the basic template of stochastic optimization in operations research: capacity planning before demand is known, production before prices are revealed, reservoir management before inflows are observed.

When the outcome space is not finite, the recourse is a function $x_2(\cdot)$, and the problem must specify the class of functions it ranges over. Rockafellar and Wets (Pacific J. Math. 62 (1976) 173–195) develop the duality theory of the convex case with recourse functions that are measurable and essentially bounded ($\mathcal L^\infty$), the setting in which the dual multipliers and their interpretation as prices become available. Their §3 asks whether that restriction loses anything: whether minimizing over $\mathcal L^\infty$ recourses gives the same first-stage problem as minimizing, scenario by scenario, the best attainable second-stage cost.

Setting

Let $(S,\Sigma,\sigma)$ be a probability space. The data are closed convex nonempty sets $C_1\subseteq\mathbb R^{n_1}$, $C_2\subseteq\mathbb R^{n_2}$, finite convex functions $f_{10},f_{1i}$ on $\mathbb R^{n_1}$ ($i=1,\dots,m_1$), and functions $f_{20}(s,x_1,x_2)$, $f_{2i}(s,x_1,x_2)$ ($i=1,\dots,m_2$), finite and jointly convex in $(x_1,x_2)$ for each $s$, and measurable in $s$ for each $(x_1,x_2)$, summable for $i=0$ and bounded for $i\ge1$. These are the paper's standing assumptions.

With $X=\mathbb R^{n_1}\times\mathcal L^\infty_{n_2}$, the essential objective of the problem $\mathbf P$ is

$$f(x_1,x_2)=F_1(x_1,0)+\int_S F_2\big(s,x_1,x_2(s),0\big)\,\sigma(ds),$$

where $F_1(x_1,u_1)=f_{10}(x_1)$ if $x_1\in C_1$ and $f_{1i}(x_1)\le u_{1i}$ for all $i$, and $+\infty$ otherwise, and $F_2(s,x_1,x_2,u_2)=f_{20}(s,x_1,x_2)$ if $x_2\in C_2$ and $f_{2i}(s,x_1,x_2)\le u_{2i}$ for all $i$, and $+\infty$ otherwise. Integrals of extended-real functions follow the paper's convention (2.4): the ordinary integral (real or $-\infty$) when the integrand is majorized by a summable function, and $+\infty$ otherwise.

Two first-stage problems are compared:

• the first-stage problem induced by $\mathbf P$ minimizes $J(x_1)=\inf_{x_2\in\mathcal L^\infty_{n_2}}f(x_1,x_2)$;
• the intrinsic first-stage problem $\mathbf Q$ minimizes $j(x_1)=F_1(x_1,0)+\int_S q(s,x_1)\,\sigma(ds)$, where $q(s,x_1)=\inf_{x_2\in\mathbb R^{n_2}}F_2(s,x_1,x_2,0)$ is the optimal recourse cost in scenario $s$.

The hypothesis of the general result uses $\rho(s,x_1)=\inf\{|x_2|\mid F_2(s,x_1,x_2,0)<+\infty\}$, the Euclidean distance from the origin to the feasible recourses ($+\infty$ if there are none), and calls $x_1$ intrinsically feasible when $j(x_1)<+\infty$. A normal convex integrand $h$ on $S\times\mathbb R^n$ is lower semicontinuous, convex and proper in $z$ for each $s$, with a measurability condition given by a sequence of measurable functions dense in each $\operatorname{dom}h(s,\cdot)$.

Formalization targets

Goal: Theorem 2 (p. 187)

If $C_2$ is bounded, then for every $x_1\in\mathbb R^{n_1}$

$$j(x_1)=J(x_1)=\inf_{x_2\in\mathcal L^\infty_{n_2}}f(x_1,x_2),\qquad \inf\mathbf Q=\inf\mathbf P,$$

the two first-stage problems have the same minimizers, and the infimum over $x_2\in\mathcal L^\infty_{n_2}$ is attained for each $x_1$.

Theorem 1 (p. 186)

If $\rho(\cdot,x_1)$ is essentially bounded for every intrinsically feasible $x_1$, then $j(x_1)=J(x_1)$ for all $x_1$, $\inf\mathbf Q=\inf\mathbf P$, and the minimizers coincide. Boundedness of $C_2$ is a special case of this hypothesis.

Milestones

• (2.1): $F(x,u)=F_1(x_1,u_1)+\int_S F_2(s,x_1,x_2(s),u_2(s))\,\sigma(ds)$ (p. 180);
• Proposition 1: for a normal convex integrand, $\inf_{z\in\mathcal L^p_n}\int_S h(s,z(s))\,\sigma(ds)=\int_S\inf_z h(s,z)\,\sigma(ds)$ whenever the left side is not $+\infty$ (p. 181);
• Proposition 2: $F_2$ is a normal convex integrand (p. 182);
• Proposition 4: $q(\cdot,x_1)$ is measurable (p. 185);
• (3.5)–(3.6): $j\le f$, hence $\inf\mathbf Q\le\inf\mathbf P$ (p. 186);
• the feasible-recourse multifunction (3.10) is measurable, $\rho$ is measurable, and the nearest feasible point is a measurable selection (p. 187);
• Theorem 1 (p. 186);
• with $C_2$ bounded, the argmin multifunction of $F_2(s,x_1,\cdot,0)$ is nonempty, compact, measurable and has a measurable selection (p. 188).

The Corollary of Theorem 2 (p. 188), that $x_1$ minimizes $\mathbf Q$ iff some $(x_1,x_2)$ minimizes $\mathbf P$, is included as a further statement.

Significance

The theorem justifies the modelling choice behind the paper's duality theory: when the second-stage constraint set is bounded, restricting recourse to essentially bounded measurable functions changes neither the optimal value nor the optimal first-stage decisions, and an optimal recourse function exists for every first stage. The duality theory of the companion mission (Theorem 3 of the same paper) is developed in that $\mathcal L^\infty$ setting, so the two results together describe the problem completely in the bounded case. Proposition 1, the interchange of infimum and integral for normal integrands, is a basic tool of stochastic programming and of the calculus of variations, used well beyond this paper.

The results are proved in the 1976 paper, relying on Rockafellar's earlier work on normal integrands and measurable selections. None of them has a machine-checked proof. Mathlib has the Lebesgue and Bochner integrals, $\mathcal L^p$ spaces and the measurable-selection prerequisites in partial form; it has no normal integrands, no extended-real integral convention of this kind, and no interchange theorem. A formal development produces those as reusable components.

Difficulty

The inequality $j\le J$ is immediate. The reverse inequality requires, from the pointwise infima $q(s,x_1)$, a single recourse function $x_2(\cdot)$ that is measurable, essentially bounded and nearly optimal in almost every scenario. Choosing a near-minimizer separately for each $s$ gives no measurability at all: the content is a measurable choice, and that needs the normality of $F_2$ and the measurability of the multifunctions of feasible and of optimal recourses. Essential boundedness is a second, independent obstacle: without a bound on $\rho$ every feasible recourse may be unbounded, and the infimum over $\mathcal L^\infty$ can then exceed $j$. Attainment in Theorem 2 needs, in addition, compactness of the argmin sets, which comes from the boundedness of $C_2$ and lower semicontinuity.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ; indices $i=1,\dots,m$ are Fin m; $\mathcal L^\infty_n$ and $\mathcal L^p_n$ are Mathlib's Lp (Fin n → ℝ) p σ, so recourse functions are almost-everywhere classes and the second-stage constraints hold almost surely. $\sigma$ is a probability measure in every theorem. All extended-real quantities ($F$, $F_1$, $F_2$, $f$, $J$, $q$, $j$, $\rho$, $\inf\mathbf P$, $\inf\mathbf Q$) take values in EReal, and every infimum is the complete-lattice infimum, so an empty infimum is $+\infty$. The integral convention (2.4) is the published definition DupacovaWets.Consistency.expect: $+\infty$ when the positive part has infinite integral (for a measurable function, exactly when it has no summable majorant), and otherwise the difference of the lower Lebesgue integrals of the positive and negative parts. $|\cdot|$ in $\rho$ is the Euclidean length, not the sup norm. "Gives the minimum" is "has value $\le$ the value at every point". Measurability of a multifunction is the published definition DupacovaWets.Consistency.IsMeasurableMultifunction ($\{s\mid\Gamma(s)\cap K\ne\emptyset\}$ measurable for every closed $K$). The standing assumptions are fields of the structure Problem.

The integral of an extended-real function must not be replaced by a Bochner integral of its real part, which would turn $\pm\infty$ values into $0$ and make $j$ meaningless; and the infima must not be real sInf, which returns $0$ on unbounded sets.

Reusable beyond this mission: the notion of a normal convex integrand on a finite-dimensional space, and Proposition 1. Contributions of measurable-selection infrastructure (Kuratowski–Ryll-Nardzewski type theorems, measurability of distance functions of closed-valued multifunctions) are welcome as supporting lemmas. The mission "Stochastic Convex Programming: Basic Duality 1" formalizes the duality theorem of the same paper on the same model.

Selected references

• R. T. Rockafellar and R. J.-B. Wets, Stochastic convex programming: basic duality, Pacific Journal of Mathematics 62(1) (1976) 173–195. https://doi.org/10.2140/pjm.1976.62.173
• R. T. Rockafellar, Measurable dependence of convex sets and functions on parameters, Journal of Mathematical Analysis and Applications 28 (1969) 4–25. https://doi.org/10.1016/0022-247X(69)90104-8
• R. T. Rockafellar, Integrals which are convex functionals, Pacific Journal of Mathematics 24(3) (1968) 525–539. https://doi.org/10.2140/pjm.1968.24.525
• G. B. Dantzig, Linear programming under uncertainty, Management Science 1(3–4) (1955) 197–206. https://doi.org/10.1287/mnsc.1.3-4.197