Operations Research

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

An arbitrator who must choose among collective options for a group of players usually does not know the players' private characteristics. The arbitrator can only ask, and a player who expects to profit from a false answer may give one. Before designing any procedure, the arbitrator therefore needs to know which expected-payoff allocations can be reached at all once strategic misreporting is taken into account.

Myerson (1979) answers this for Bayesian collective choice problems with finitely many types. Restricting attention to mechanisms that simply ask each player for their type, and that make honest answers optimal, loses nothing: every expected-payoff allocation that any mechanism can produce in equilibrium is already produced honestly by such a direct mechanism, and conversely. This is the revelation principle in the form used throughout Bayesian mechanism design. It is what makes incentive-compatibility constraints the starting point for auction design, bilateral trade, and the bargaining solution in the second half of the same paper.

Timeline. Gibbard (1973) gave the dominant-strategy form of the principle. Rosenthal (Review of Economic Studies, 1978) studied arbitration of two-party disputes under uncertainty; Myerson notes that Theorem 2 could be derived as a corollary of Rosenthal's Theorem 3. Dasgupta, Hammond and Maskin (1979) gave general Bayesian implementation results in the same year. Myerson's Theorem 2 states the principle as an equality of interim payoff sets over all finite response sets. Myerson (1982) later extended it to principal–agent problems with moral hazard.

Setting

A Bayesian collective choice problem $(C,A_1,\dots,A_n,U_1,\dots,U_n,P)$ has a nonempty finite set of players $i$, a nonempty finite set $A_i$ of types for each player, a nonempty finite set $C$ of collective choices, utilities $U_i(c,\alpha)$ depending on the choice and on the true type profile $\alpha=(\alpha_1,\dots,\alpha_n)$, and a probability distribution $P$ on type profiles. With $R_i(a_i)=\sum_{\beta:\beta_i=a_i}P(\beta)$ the marginal of type $a_i$, a player of type $a_i$ assigns the conditional probability $P_i(\alpha\mid a_i)=P(\alpha)/R_i(a_i)$ to profiles with $\alpha_i=a_i$, and $0$ to the others.

A choice mechanism on response sets $S_1,\dots,S_n$ (nonempty finite sets of possible answers) is a function $\pi(c\mid s)\ge0$ with $\sum_{c}\pi(c\mid s)=1$ for every response profile $s$. On the standard response sets $S_i=A_i$, the payoff of type $a_i$ who reports $b_i$ while the others are honest is

$$Z_i(\pi,b_i\mid a_i)=\sum_\alpha\sum_{c}P_i(\alpha\mid a_i)\,\pi(c\mid\alpha_{-i},b_i)\,U_i(c,\alpha).$$

The mechanism is Bayesian incentive-compatible if $Z_i(\pi,a_i\mid a_i)\ge Z_i(\pi,b_i\mid a_i)$ for all $i,a_i,b_i$. Its honest allocation is the vector $V(\pi)$ with coordinates $V_i(\pi\mid a_i)=Z_i(\pi,a_i\mid a_i)$, indexed by the disjoint union of the $A_i$. The incentive-feasible set is

$$F^*=\{V(\pi):\pi\text{ a Bayesian incentive-compatible choice mechanism on the standard response sets}\}.$$

On general response sets, a response plan $\sigma_i(s_i\mid a_i)$ is a probability distribution over $S_i$ for each type $a_i$. Plans $\sigma=(\sigma_1,\dots,\sigma_n)$ give type $a_i$ the payoff

$$W_i(\pi,\sigma\mid a_i)=\sum_\alpha\sum_s\sum_c P_i(\alpha\mid a_i)\Big(\prod_{j}\sigma_j(s_j\mid\alpha_j)\Big)\pi(c\mid s)\,U_i(c,\alpha).$$

They form a response-plan equilibrium for $\pi$ if no type $a_i$ of any player gains by switching to any other response plan $\sigma_i'$. The equilibrium-feasible set $F^{**}$ collects $W(\pi,\sigma)$ over all choice mechanisms $\pi$, on all nonempty finite response sets, and all response-plan equilibria $\sigma$ for $\pi$.

Formalization targets

Goal: Theorem 2

$$F^{**}=F^*.$$

Both inclusions are asserted for every Bayesian collective choice problem. $F^{**}\subseteq F^*$ says equilibrium behaviour under any mechanism can be replicated honestly by an incentive-compatible direct mechanism. $F^*\subseteq F^{**}$ says honest reporting is itself an equilibrium of every incentive-compatible mechanism.

Milestones (the steps of the paper's proof)

1. For any choice mechanism $\pi$ and response plans $\sigma$, the induced direct mechanism $\pi'(c\mid\alpha)=\sum_s\pi(c\mid s)\prod_i\sigma_i(s_i\mid\alpha_i)$ is a choice mechanism and $V(\pi')=W(\pi,\sigma)$.
2. If $\sigma$ is a response-plan equilibrium for $\pi$, then $\pi'$ is Bayesian incentive-compatible.
3. If $\pi'$ is a Bayesian incentive-compatible choice mechanism, the honest plans $\sigma_i'(b_i\mid a_i)=\mathbf 1[b_i=a_i]$ form a response-plan equilibrium for $\pi'$, and $W(\pi',\sigma')=V(\pi')$.

Significance

The result. Theorem 2 reduces a search over all communication protocols, an unbounded family of response sets and mixed reporting behaviours, to a finite system of linear inequalities in $\pi$ on a fixed finite domain. Combined with Theorem 1 of the paper, which shows $F^*$ is a nonempty compact convex set, it justifies applying a bargaining solution to $F^*$ rather than to some larger, ill-defined set of attainable outcomes. The same reduction underlies the use of incentive constraints in optimal auctions, bilateral trade and correlated-type mechanism design.

Formalizing it. The result is classical and its proof is short, but it is a statement about all finite response sets at once, and the equality of two sets of payoff vectors is sensitive to the conventions: which plans are allowed as deviations, where the conditioning happens, and whether the induced mechanism is a genuine probability distribution. A machine-checked version pins these down. To our knowledge no formal proof of this finite Bayesian revelation principle exists. The platform has related, unproved items in other models: MechanismDesign.Robust.revelation_principle (Börgers, Prop. 10.2, on a countable Harsanyi type space with PMF lotteries; one inclusion, outcome equivalence) and single-agent, quasi-linear and dominant-strategy revelation principles from the same book. None of them is the statement here.

Difficulty

The mathematics consists of finite sums, but the bookkeeping is the obstacle. Milestone 1 requires exchanging a sum over response profiles with a product over players and using that each plan sums to one. Milestone 2 requires recognizing a lie $b_i$ in $\pi'$ as a particular whole response plan in $\pi$: the plan that, at every type, behaves as type $b_i$ would. Because $P_i(\alpha\mid a_i)$ vanishes off $\alpha_i=a_i$, only its value at $a_i$ matters. For milestone 3, a mixed deviation from honesty has to be bounded by the best pure misreport, a convex-combination argument over $A_i$. Identifying the $F^{**}$ side of the goal also needs instances on an existentially chosen family of types.

Formalization scope

All objects live in MyersonBargaining.Revelation. Players form a nonempty finite type ι; types A i, choices C and response sets S i are nonempty finite types in Type. Mechanisms and plans are real-valued functions with the probability constraints as predicates (IsChoiceMechanism, IsResponsePlan), event first and condition second: π c s, σ i s a. Allocation vectors are functions on Σ i, A i. The paper's loose phrases are read as follows:

• "probability distribution" means nonnegativity and sum one;
• (3) divides by $R_i(a_i)$, so the problem requires $R_i(a_i)>0$; individual profiles may have probability zero;
• the consistent (common-prior) reading of (3)–(4) is formalized, not the subjective reading the paper permits on p. 63;
• "for every possible alternative response plan" in (14) ranges over all mixed response plans, compared type by type;
• "$\pi$ is a choice mechanism" in (15) ranges over all nonempty finite response sets, with an explicit existential over the family S : ι → Type and its instances;
• "incentive-compatible mechanism" means a choice mechanism satisfying (6).

The product in (12) is printed with $\sigma_j(s_j\mid a_j)$; it is formalized with $\alpha_j$, as the paper's own induced mechanism on p. 66 uses. Milestone 1 is stated for arbitrary response plans, not only for equilibria. Section 6's numerical example is not formalized.

A trivializing formalization is ruled out explicitly: fixing $S_i=A_i$ in $F^{**}$, restricting deviations to pure plans, or stating only $F^{**}\subseteq F^*$ would each change the theorem, and none is done.

A complete development needs finite sums over dependent product types (Fintype.piFinset, Finset.prod_univ_sum), Function.update on dependent families, and nothing beyond Mathlib. The two definition modules (the model and the response-plan objects) are reusable by any finite Bayesian mechanism-design formalization. Proofs of any milestone, alternative proofs via Rosenthal's argument, and cleaner restatements as lemmas about stochastic matrices are welcome.

Selected references

• Roger B. Myerson, Incentive compatibility and the bargaining problem, Econometrica 47(1), 61–73, 1979. https://doi.org/10.2307/1912346
• Robert W. Rosenthal, Arbitration of two-party disputes under uncertainty, Review of Economic Studies 45(3), 1978 (cited in the source as reference [8], "forthcoming").
• Allan Gibbard, Manipulation of voting schemes: a general result, Econometrica 41(4), 587–601, 1973. https://doi.org/10.2307/1914083
• Partha Dasgupta, Peter Hammond, Eric Maskin, The implementation of social choice rules: some general results on incentive compatibility, Review of Economic Studies 46(2), 185–216, 1979. https://doi.org/10.2307/2297045
• Roger B. Myerson, Optimal coordination mechanisms in generalized principal–agent problems, Journal of Mathematical Economics 10(1), 67–81, 1982. https://doi.org/10.1016/0304-4068(82)90006-4

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

Motivation

Burn-in is the final reliability test of integrated circuits: boards loaded with chips are held in an oven at elevated temperature for a minimum specified time, so that marginal devices fail before shipment. An oven holds several boards at once, and a load may stay in the oven longer than its specification but never shorter. Lee, Uzsoy and Martin-Vega (Oper. Res. 40(4), 1992) model such an oven as a batch processing machine and study the resulting scheduling problems. Burn-in is often the bottleneck of the test stage, which is why throughput (makespan) and due-date performance on several ovens in parallel are of practical interest.

This mission covers the paper's makespan result for parallel ovens. On ordinary identical parallel machines, Graham (SIAM J. Appl. Math. 17, 1969) proved that the LPT rule (list the jobs longest first and give each to the machine that frees up first) has worst-case ratio $4/3 - 1/(3m)$ on $m$ machines. The paper shows that the same factor holds for batch machines once the jobs are first grouped into full batches of the longest jobs.

Setting

There are $n$ jobs with processing times $p_j > 0$, all available at time $0$, and $m \ge 1$ identical batch processing machines. Each machine processes up to $B \ge 1$ jobs at the same time. A batch is a set of at most $B$ jobs processed together; once started it cannot be interrupted or joined, and its batch time is that of its longest job,

$$p(P) = \max_{j \in P} p_j .$$

A schedule forms the jobs into disjoint nonempty batches covering all jobs, assigns each batch to a machine, and runs every machine's batches back to back from time $0$. The makespan is the largest machine load, the total batch time on a machine. The problem of minimizing it is written $P/B/C_{\max}$, and $C^*$ denotes its optimal value, over every way of forming batches (any sizes up to $B$, any grouping) and every assignment. For $B = 1$ it is the classical problem $P//C_{\max}$.

Algorithm BLPT.

1. Rank the jobs in nonincreasing order of processing time and cut the ranked list into successive groups of $B$ jobs, the last possibly smaller.
2. Order these batches in nonincreasing order of batch time and assign each in turn to a machine with least current load.

$C(\mathrm{BLPT})$ is the resulting makespan.

For the optional lateness result, each job also has a due date $d_j \ge 0$. The maximum lateness of a schedule is $L_{\max} = \max_j (C_j - d_j)$, $L$ is its value under BLPT, $L^*$ its optimum and $d_{\max} = \max_j d_j$.

Formalization targets

Goal: Proposition 3 (p. 773)

$$C(\mathrm{BLPT}) \le \left(\frac43 - \frac1{3m}\right) C^* .$$

It is claimed for every run of BLPT, whatever order the algorithm gives to equal processing times and equal batch times.

Milestones

1. Proposition 2 (p. 772). With the jobs re-indexed longest first, some optimal schedule has batches of consecutive jobs, all full except possibly the one containing the last job. In other words, its batches are exactly the groups formed in Step 1 of BLPT.
2. The reduction (§5, p. 772). $C^*$ equals the optimal makespan of $P//C_{\max}$ on the aggregate jobs $p(B_1), \dots, p(B_{\lceil n/B\rceil})$.
3. Graham's LPT bound, as quoted (p. 772). For jobs $q_0 \ge \dots \ge q_{M-1} \ge 0$ on $m$ machines, list scheduling in that order has makespan at most $(4/3 - 1/(3m))$ times the optimum.
4. Proposition 5 (p. 773, further result).

$$\frac{L - L^*}{L^* + d_{\max}} \le \left(\frac13 - \frac1{3m}\right) + \frac{d_{\max}}{L^* + d_{\max}} .$$

Significance

Proposition 3 gives a constant-factor guarantee for a strongly NP-hard problem. The guarantee does not depend on $B$, whereas arbitrary batch list scheduling only gets $B + 1 - 1/m$ (Proposition 1 of the same paper). For one machine the factor is $1$, so BLPT is then exact. Proposition 2 is a structural statement: it fixes the batch composition of an optimal schedule before any assignment decision. It turns the batch problem into an ordinary parallel-machine problem, so other results for $P//C_{\max}$ transfer as well. Proposition 5 carries the guarantee over to maximum lateness, measured relative to $L^* + d_{\max}$ because $L^*$ may be negative.

All results are proved in the paper, Proposition 3 by a one-line appeal to Proposition 2 and Graham. This mission produces machine-checked versions of the reduction and the bound. Graham's LPT bound itself is not formalized anywhere on the platform. Its proof here is a reusable result about the published list-scheduling definitions, independent of batching.

Difficulty

The obvious argument is "batch as in Step 1, then apply Graham". It has two gaps. First, $C^*$ ranges over all batchings, and an optimal schedule need not use full batches or consecutive jobs. The exchange argument behind Proposition 2 has to move jobs between batches, possibly on different machines, without increasing any machine's load. Ties among equal processing times also have to be handled, since the claim is made for every longest-first ranking. Second, Graham's bound is not on the platform and has to be proved. It is a finite combinatorial statement, but its known proofs are not short. Proposition 5 additionally needs the bound for sub-instances formed by a prefix of the batches.

Formalization scope

Jobs are Fin n, 0-based. Processing times are real, p : Fin n → ℝ with 0 < p j; due dates (Proposition 5 only) are d : Fin n → ℝ with 0 ≤ d j. A batching is a list of nonempty, pairwise disjoint Finsets of size at most B covering every job. The batch time is the maximum of p over the batch.

Machine loads, assignments, the per-batching optimum and list scheduling reuse the published definitions NumStochOpt.ListScheduling.ListSchedule (firstAvailable, lsLoads, listMakespan) and NumStochOpt.ListScheduling.Makespan (machineLoad, makespan, optMakespan) from the Rinnooy Kan–Stougie mission, applied to the sequence of batch times (padded with zeros beyond the last batch, which these definitions never read). $C^*$ is the infimum of optMakespan over all valid batchings, never only over the consecutive ones of Step 1, which would assume Proposition 2.

Explicit readings of the paper's phrases:

• "rank jobs in decreasing order" is any list of all jobs that is nonincreasing in p;
• the batches of Step 1 are List.toChunks B of that list;
• "order the batches in nonincreasing order of $p(B_k)$" is any permutation of those chunks that is nonincreasing in batch time;
• every statement is quantified over both choices;
• "assign them to the machines as they become free" is least-loaded list scheduling with the published lowest-index tie rule. With no idle time, the machine that becomes free first is a least-loaded one, and the tie rule does not change the multiset of loads;
• "$1/3m$" is $1/(3m)$;
• "optimal solution" in Proposition 2 is a valid batching with an assignment whose makespan equals $C^*$, and "consecutive, all full except the one containing the highest indexed job" is "equal, up to order, to the chunks of the ranked list";
• schedules on each machine run in list order without idle time, and every processing order is a reordering of the list. For $L^*$ this covers every semi-active schedule.

Proposition 5 adds the hypothesis $d_j \ge 0$, which the paper's proof uses but does not print. It also makes $L^* + d_{\max}$ positive, so the printed ratios are well defined. Running times and the paper's other algorithms are out of scope.

A statement with $C^*$ restricted to consecutive batches, a sorry-free bound obtained from a degenerate $m = 0$ or empty-job reading, or a BLPT fixed to one convenient tie-break would trivialize or weaken the goal and is ruled out by the statements as posed. Welcome contributions: Graham's LPT bound on the published list-scheduling definitions (reusable for any $P//C_{\max}$ work), the exchange lemma behind Proposition 2, and the permutation invariance of optMakespan under reordering of items.

Selected references

• C.-Y. Lee, R. Uzsoy, L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 764–775, 1992. https://doi.org/10.1287/opre.40.4.764
• R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. https://doi.org/10.1137/0117039
• A. H. G. Rinnooy Kan, L. Stougie, Stochastic Integer Programming, Ch. 8 of Y. Ermoliev, R. J.-B. Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer, 1988 (source of the reused list-scheduling definitions). https://doi.org/10.1007/978-3-642-61370-8

Motivation

Multistage decision problems under uncertainty are often modelled by a finite set of scenarios: each scenario $s$ fixes one possible future, and for it a deterministic problem can be solved. What makes the problem stochastic is the requirement that decisions may depend only on information available at the time they are taken. Rockafellar and Wets (WP-87-119, 1987; journal version Math. Oper. Res. 16 (1991) 119–147) proposed the progressive hedging algorithm, which solves the scenario problems separately with a penalty and a price term and blends their solutions step by step into a single policy that respects the information constraints. The method is a standard decomposition scheme of stochastic programming and is implemented in solver libraries such as PySP and mpi-sppy.

For convex problems the paper proves convergence through the theory of the proximal point algorithm. Many practical scenario models are not convex (integer-like penalties, nonconvex costs). For that case the paper proves one result, Theorem 6.1: the algorithm cannot be expected to find a global minimum, but whenever it converges, its limit is a stationary point. This mission formalizes that result.

Setting

Let $S$ be a finite set of scenarios with probabilities $p_s>0$, $\sum_s p_s=1$. A decision is a vector $x=(x_1,\dots,x_T)\in\mathbb R^n$, split into blocks $x_t$ taken at times $t=1,\dots,T$. For each scenario there is a scenario subproblem

$$(P_s)\qquad\text{minimize } f_s(x)\ \text{over } x\in C_s\subseteq\mathbb R^n .$$

Throughout, every $C_s$ is nonempty and closed, every $f_s$ is locally Lipschitz, and the sets $\{x\in C_s\mid f_s(x)\le\alpha\}$ are bounded.

A policy is a map $X:S\to\mathbb R^n$. Policies form a space $\mathcal E$ with inner product $\langle X,Y\rangle=\sum_s p_s X(s)\cdot Y(s)$ and norm $\|X\|=\langle X,X\rangle^{1/2}$. For each time $t$ the scenarios are partitioned into bundles $A\in\mathcal A_t$ of scenarios indistinguishable at time $t$. A policy is implementable, $X\in\mathcal N$, when each $X_t$ is constant on every bundle of $\mathcal A_t$; it is admissible, $X\in\mathcal C$, when $X(s)\in C_s$ for all $s$. The aggregation operator $J$ replaces $X_t(s)$ by its conditional expectation over the bundle of $s$; $K=I-J$, and $\mathcal M=\{W\mid JW=0\}=\mathcal N^\perp$. With $F(X)=\sum_s p_s f_s(X(s))$ the problem is

$$(P)\qquad\text{minimize } F(X)\ \text{over } X\in\mathcal C\cap\mathcal N .$$

Progressive hedging with parameter $r>0$ keeps $X^\nu\in\mathcal C$ and $W^\nu\in\mathcal M$. It sets $\hat X^\nu=JX^\nu$, computes $X^{\nu+1}(s)$ for every $s$ from

$$(P^\nu_s)\qquad\text{minimize } f_s(x)+x\cdot W^\nu(s)+\tfrac12 r|x-\hat X^\nu(s)|^2\ \text{over } x\in C_s ,$$

and updates $W^{\nu+1}=W^\nu+rKX^{\nu+1}$. In the nonconvex case, $X^{\nu+1}(s)$ is only required to be $\delta$-locally optimal: optimal among the points of $C_s$ within Euclidean distance $\delta$ of it, for a fixed $\delta>0$.

$\partial g(x)$ denotes Clarke's generalized gradient of a locally Lipschitz $g$ and $N_C(x)$ Clarke's normal cone to a closed set $C$.

Formalization targets

Goal: Theorem 6.1

If $X^\nu\to X^*$ and $W^\nu\to W^*$, then $X^*\in\mathcal N\cap\mathcal C$, $W^*\in\mathcal M$ and

$$-W^*(s)\in\partial f_s(X^*(s))+N_{C_s}(X^*(s))\qquad\text{for all } s\in S;$$

moreover $X^*$ is a local minimizer of $(\tilde P)$, which is (P) with $f_s$ replaced by $\tilde f_s(x)=f_s(x)+\tfrac12 r|x-X^*(s)|^2$, and $-W^*(s)\in\partial\tilde f_s(X^*(s))+N_{C_s}(X^*(s))$.

Milestones

1. (6.4)–(6.5): each $X^{\nu+1}$ is optimal for $(P^\nu)$, minimize $F(X)+\langle X,W^\nu\rangle+\tfrac12 r\|X-\hat X^\nu\|^2$ over $\mathcal C$, on the $\|\cdot\|$-ball of radius $\delta'=\delta\min_s p_s^{1/2}$.
2. $W^*\in\mathcal M$, $KX^\nu\to0$ and $X^*\in\mathcal N$.
3. (6.6): $X^*$ is locally optimal for $(P^*)$, minimize $F(X)+\langle X,W^*\rangle+\tfrac12 r\|X-X^*\|^2$ over $\mathcal C$.
4. $X^*$ is locally optimal for $F(X)+\tfrac12 r\|X-X^*\|^2=E\{\tilde f_s(X(s))\}$ over $\mathcal C\cap\mathcal N$.
5. (6.2): $\partial\tilde f_s(X^*(s))=\partial f_s(X^*(s))$, from $\partial\tilde f_s(x)=\partial f_s(x)+r(x-X^*(s))$.
6. Theorem 4.1: at a local minimizer of (P) satisfying the constraint qualification "the only $W\in\mathcal M$ with $-W(s)\in N_{C_s}(X^*(s))$ for all $s$ is $W=0$", some $W^*\in\mathcal M$ satisfies the conditions above; in the convex case these conditions imply global optimality.

Significance

Theorem 6.1 is the paper's only guarantee outside convexity. It says that progressive hedging, run with local solvers on nonconvex scenario subproblems, cannot converge to a point that fails the first-order conditions, and that the limiting price system $W^*$ is a Lagrange multiplier for the nonanticipativity constraint $X\in\mathcal N$. It needs no constraint qualification, unlike the general necessary condition of Theorem 4.1: the multiplier is produced by the algorithm. This is the basis for using progressive hedging as a heuristic for nonconvex and mixed-integer stochastic programs.

The result is proved in the paper; to our knowledge it has not been machine-checked. A complete formalization would give checked statements of the scenario model ($J$, $K$, $\mathcal N$, $\mathcal M$ with the weighted inner product), of the algorithm with inexact local subproblem solutions, and of Clarke's optimality conditions for problems with separable structure. The convex convergence theory of the same paper is the subject of the companion mission Scenarios and Policy Aggregation in Optimization Under Uncertainty 1.

Difficulty

The local optimality of $X^{\nu+1}(s)$ is relative to a ball centred at the iterate, which moves. Passing to the limit requires a radius that is uniform in $\nu$ and in the norm of $\mathcal E$; this is what $\delta'$ provides, and it only covers points strictly inside the limiting ball: a point of $\mathcal C$ at distance exactly $\delta'$ from $X^*$ may lie outside every ball around the iterates. The step from local optimality to the multiplier condition uses Clarke's necessary condition for minimization over a closed set and the sum rule for a Lipschitz function plus a smooth one; neither is in Mathlib. Theorem 4.1 needs, in addition, a calculus rule for normal cones of an intersection under a qualification condition, and the transfer of Clarke's objects between $\mathcal E$ with the weighted inner product and the individual scenario spaces.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). A policy is a function S → EuclideanSpace ℝ (Fin n). The weighted inner product and norm of $\mathcal E$ are explicit definitions (ip, pnorm); Lean's built-in norm on policies (the sup norm) is used only for topological notions: convergence of the iterates and "locally optimal" without a radius, which do not depend on the norm. The radii $\delta'$ are in the weighted norm, the radius $\delta$ in the Euclidean norm of $\mathbb R^n$. Time blocks are a monotone map from coordinates to periods; bundles are the classes of a setoid on $S$ for each period. The standing assumptions are fields of the model structure, so every theorem carries them. Indices are 0-based and sequences are indexed by $\nu=0,1,2,\dots$; the run starts from $X^0\in\mathcal C$ and $W^0\in\mathcal M$. Theorem 4.1 is stated in its decomposed form (4.4), scenario by scenario.

Clarke's generalized gradient and normal cone are the published platform definitions ClarkeGradients.Shared.generalizedGradient (convex hull of limits of gradients) and ClarkeGradients.FlowInvariance.normalCone (closure of the cone generated by the generalized gradient of the distance function); for locally Lipschitz functions and closed nonempty sets these are the objects the paper uses.

Formalizations that trivialize the statement are excluded: Theorem 6.1 carries no convexity hypothesis and no constraint qualification, the $\delta'$-balls are not measured in the sup norm, and the run predicate is satisfiable (the model files come with a sanity check exhibiting a run).

Useful infrastructure, reusable beyond this mission: Clarke's necessary condition for local minimization of a Lipschitz function over a closed set, the sum rule with a $C^1$ function, products of normal cones, and basic facts about $J$ (an orthogonal projection onto $\mathcal N$ for the weighted inner product). Contributions of any of these are welcome.

Selected references

• R. T. Rockafellar and R. J.-B. Wets, Scenarios and policy aggregation in optimization under uncertainty, IIASA Working Paper WP-87-119, 1987. https://pure.iiasa.ac.at/id/eprint/2933/
• R. T. Rockafellar and R. J.-B. Wets, Scenarios and policy aggregation in optimization under uncertainty, Mathematics of Operations Research 16(1), 119–147, 1991. https://doi.org/10.1287/moor.16.1.119
• F. H. Clarke, Generalized gradients and applications, Transactions of the AMS 205, 247–262, 1975. https://doi.org/10.1090/S0002-9947-1975-0367131-6
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983. https://doi.org/10.1137/1.9781611971309