Operations Research

Motivation

Many quantities in queueing, inventory and reliability models are additive functionals of a regenerative process: the total work processed by a server up to time $t$, the cost accumulated by an inventory policy, the time a machine spends broken. Each such quantity grows by independent, identically distributed amounts over the cycles between successive regeneration points. W. L. Smith called these cumulative processes in Regenerative stochastic processes (Proc. R. Soc. Lond. A, 1955), the paper that introduced the term "regenerative process" and laid out its limit theory. Long-run averages of such quantities are estimated by simulation and by statistical observation of real systems. Confidence intervals for these estimates, and the regenerative method of simulation output analysis, rest on the central limit theorem for cumulative processes. When several quantities are estimated at once (a ratio of two rewards, a vector of costs), they rest on its joint version for several cumulative processes driven by the same regenerations.

Timeline:

• 1949. Feller proves the central limit theorem for the renewal counting process.
• 1952. Anscombe proves that a central limit theorem survives replacing the number of summands by a random index $m_t$ with $m_t/\psi(t)\to 1$ in probability, without independence between the index and the summands (Anscombe, Proc. Camb. Phil. Soc. 48, 1952).
• 1955. Smith extends Anscombe's theorem to random vectors and deduces the univariate (Theorem 9, Corollary 9·1) and multivariate (Theorem 10) central limit theorems for cumulative processes (Smith 1955).

Setting

On a probability space $(\Omega, P)$, let $t_1, t_2, \dots$ be independent, identically distributed, non-negative random variables with $P\{t_1 = 0\} < 1$ (a renewal process), and $t_0 = 0$. The regeneration epochs are $T_k = t_0 + t_1 + \dots + t_k$ ($k \ge 0$), and $n_t$ is the number of epochs in $[0,t]$ (in Smith's words, the greatest $k$ with $T_{k-1} \le t$, where $T_{-1} = 0$). Write $\mu_r = E t_1^r$.

A real process $w_t$ with $w_0 = 0$ is a cumulative process if (C1) its cycle increments $y_n = \Delta_n w_t = w_{T_n} - w_{T_{n-1}}$, $n \ge 1$, are i.i.d., and (C2) with probability one its paths have bounded variation on every finite interval. The variation process $\tilde w_t = \int_0^t |\mathrm d w_t|$ has increments $\tilde y_n = \Delta_n \tilde w_t$. Moments are written $\kappa_r = E y_n^r$ and $\tilde\kappa_r = E \tilde y_n^{\,r}$.

$M$ cumulative processes $w^{(1)}_t, \dots, w^{(M)}_t$ are based on the same sequence of regeneration points when the cycle vectors $(t_n, y^{(1)}_n, \dots, y^{(M)}_n, \tilde y^{(1)}_n, \dots, \tilde y^{(M)}_n)$ are i.i.d. in $n$. Put $\kappa^{(i)}_1 = E y^{(i)}_1$. The covariance matrices are

$$a_{kl} = \operatorname{cov}(y^{(k)}_1, y^{(l)}_1), \qquad b_{kl} = \operatorname{cov}\Big(y^{(k)}_1 - \tfrac{\kappa^{(k)}_1}{\mu_1} t_1,\; y^{(l)}_1 - \tfrac{\kappa^{(l)}_1}{\mu_1} t_1\Big).$$

Formalization targets

Goal: Theorem 10

If $\mu_1 < \infty$ and $E(\tilde y^{(i)}_1)^2 < \infty$ for every $i$, then as $t \to \infty$

$$\left(\frac{w^{(i)}_t - \kappa^{(i)}_1 n_t}{(t/\mu_1)^{1/2}}\right)_{i=1}^M \xrightarrow{\ d\ } \mathcal N(0, a),$$

and if in addition $\mu_2 < \infty$,

$$\left(\frac{w^{(i)}_t - (\kappa^{(i)}_1/\mu_1)\,t}{(t/\mu_1)^{1/2}}\right)_{i=1}^M \xrightarrow{\ d\ } \mathcal N(0, b).$$

Milestones

• The renewal strong law $n_t/t \to 1/\mu_1$ almost surely (§5·3).
• Lemma 8: if $\mu_1 < \infty$ and $\tilde\kappa_p < \infty$, then $(w_{t+Z_t} - w_t)/t^{1/p} \to 0$ almost surely, where $Z_t = \sum_1^{n_t+1} t_i - t$.
• Theorem B (Anscombe): $P\{\sum_1^{m_t} y_i/(\sigma\psi(t)^{1/2}) \le \alpha\} \to \Phi(\alpha)$ for i.i.d. centred $y_i$ with variance $\sigma^2 > 0$ and $m_t/\psi(t) \to 1$ in probability.
• Its $M$-dimensional form (§5·4): $\psi(t)^{-1/2}\sum_1^{m_t} \mathbf y_j \xrightarrow{d} \mathcal N(0, a)$ for i.i.d. centred random vectors.
• Theorem 9: if $E y_1 = 0$ and $\operatorname{var} y_1 = \sigma^2 > 0$, then $P\{w_t/(\sigma(t/\mu_1)^{1/2}) \le \alpha\} \to \Phi(\alpha)$.
• Corollary 9·1: the univariate forms of both assertions of the goal, with normalisations $\sigma = (\kappa_2 - \kappa_1^2)^{1/2}$ and $\gamma = \operatorname{var}(y_1 - (\kappa_1/\mu_1)t_1)$.

Significance

Theorem 10 is the multivariate central limit theorem for regenerative processes. Its second assertion with $M = 2$ and the delta method gives the asymptotic normality of ratio estimators $w^{(1)}_t / w^{(2)}_t$, the basis of the regenerative method of simulation output analysis. With $w_t = n_t$, Corollary 9·1 recovers Feller's central limit theorem for renewal processes, which Smith points out (p. 9). The first assertion, with the random centring $\kappa_1 n_t$, needs only $\mu_1 < \infty$, which matters for heavy-tailed cycle lengths.

The results are classical and proved, and none of them is formalized. Mathlib has the central limit theorem for i.i.d. real sums with a deterministic number of terms and multivariate Gaussian laws, but no random-index central limit theorem, no renewal counting process and no regenerative process. A formal development would supply Anscombe's theorem (useful well beyond renewal theory, for sequential analysis and random sums), the renewal strong law and a reusable model of cumulative processes.

Difficulty

The obvious argument writes $w_t$ as the sum of the first $n_t$ cycle increments plus a remainder and applies the classical central limit theorem. This fails at two points. First, the number of summands $n_t$ is random and depends on the summands themselves (cycle lengths and rewards are typically dependent), so the classical theorem with a deterministic index does not apply and conditioning on $n_t$ destroys the i.i.d. structure. Anscombe's theorem is needed exactly for this; it requires control of the partial sums uniformly over a window of indices around $t/\mu_1$, not at a single index. Second, the remainder over the incomplete cycle at time $t$ must be shown negligible on the scale $\sqrt t$ using only a second moment of the cycle variation; Lemma 8 does this almost surely. For the vector statement, the scalar theorem must be lifted to convergence in distribution in $\mathbb R^M$ with a possibly degenerate covariance matrix, where the scalar theorem's hypothesis $\sigma > 0$ can fail along some directions.

Formalization scope

• Time is real; every limit is along $t \to \infty$ in $\mathbb R$. Processes are functions $w : \mathbb R \to \Omega \to \mathbb R$ (or a family indexed by Fin M); cycle lengths are a sequence $\mathbb N \to \Omega \to \mathbb R$ with $t_0 = 0$.
• $n_t$ is a natural number, the number of epochs $T_j \le t$; on the null event where infinitely many epochs are $\le t$ it is $0$. Finiteness is never assumed.
• $\tilde w_t$ is the total variation (eVariationOn) of the path on $[0,t]$, set to $0$ for all $t$ on paths of infinite variation, as Smith allows.
• Condition (C1) is read for the whole cycle vector $(t_n, y_n, \tilde y_n)$. No independence between components is assumed. Assuming the cycle length independent of the rewards, or the components independent, would make $a$ diagonal or force $b$ into a special form; that trivialization is ruled out.
• "Jointly normally distributed with covariance matrix $a$" is TendstoInDistribution to multivariateGaussian 0 a on EuclideanSpace ℝ (Fin M). The matrices $a$ and $b$ are defined as covariance matrices, hence positive semidefinite, so the limit is a genuine (possibly degenerate) Gaussian law and not Mathlib's Dirac fallback for non-PSD input.
• The scalar statements keep the paper's form: convergence of $P\{\cdot \le \alpha\}$ to $\Phi(\alpha) =$ cdf (gaussianReal 0 1) α for every real $\alpha$. The paper's implicit $\sigma > 0$ and $\gamma > 0$ are explicit hypotheses; without them the quotients are $0$ in Lean and the statements would be false.
• $\mu_1 < \infty$, $\mu_2 < \infty$ and $E\tilde y^2 < \infty$ are Integrable hypotheses, never encoded through the value of an integral.

Contributions welcome: a proof of Anscombe's theorem from Mathlib's central limit theorem; the renewal strong law from strong_law_ae; measurability lemmas for $n_t$ and $\tilde w_t$; the Cramér–Wold step.

Selected references

• W. L. Smith, Regenerative stochastic processes, Proc. R. Soc. Lond. A 232(1188):6–31, 1955. https://doi.org/10.1098/rspa.1955.0198
• F. J. Anscombe, Large-sample theory of sequential estimation, Proc. Cambridge Philos. Soc. 48, 600, 1952 (cited in Smith 1955, p. 31).
• W. Feller, Fluctuation theory of recurrent events, Trans. Amer. Math. Soc. 67, 98, 1949 (cited in Smith 1955, p. 31).
• J. L. Doob, Renewal theory from the point of view of the theory of probability, Trans. Amer. Math. Soc. 63, 422, 1948 (cited in Smith 1955, p. 31).

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

Motivation

Semiconductor burn-in tests hold several jobs in an oven at once. A production planner must decide which jobs share each oven run and in what order those runs take place. A job may become available only after earlier manufacturing steps, and a due date marks when its test should finish. The planning objective here is to minimize how many jobs finish after their due dates. Lee, Uzsoy, and Martin-Vega studied this batch scheduling problem and gave a dynamic program for the case of equal processing times and compatible release and due-date orders (Lee, Uzsoy, and Martin-Vega 1992, §4, pp. 770–771).

Setting

There are $n$ jobs and one batch processing machine with capacity $B\ge1$. Job $j$ has release time $r_j$, due date $d_j$, and processing time $p_j$. In the main problem every processing time equals a common value $p$. A batch is a nonempty set of at most $B$ jobs. Its processing time is the longest processing time among its members; it begins only after all its jobs have been released and the previous batch has finished. Processing is uninterrupted. A schedule is an ordered list of disjoint batches that covers every job. Each batch starts at the earliest time allowed by these conditions.

The completion time $C_j(S)$ of job $j$ in schedule $S$ is the completion time of its batch. A job is on time when $C_j(S)\le d_j$ and tardy when $d_j<C_j(S)$. Write $U(S)=\#\{j:d_j<C_j(S)\}$ and let $U^*$ be the minimum of $U(S)$ over all valid complete batch schedules. Tardy jobs still belong to a schedule and consume machine time. An on-time batch is one whose every member is on time.

For the structural lemmas, agreeable release times and due dates mean that $r_i<r_j$ implies $d_i\le d_j$. For the dynamic program, jobs are indexed so that both $r_j$ and $d_j$ are nondecreasing. A batch is in batch-EDD order relative to later batches when no job in it has a later due date than a job in a later batch. A batch of consecutive jobs contains exactly an index interval. These are the paper's Lemmas 4 and 5 and Definition 1 (pp. 767, 770).

Formalization targets

Structural optimal schedules

Lemma 4 asserts that some optimum has an initial list of wholly on-time batches in batch-EDD order, followed by batches containing only tardy jobs. Lemma 5 asserts that some optimum has every wholly on-time batch made of consecutive indexed jobs. These are existence statements about schedules of all jobs; neither restricts the feasible schedules over which $U^*$ is defined.

Correctness of Algorithm DP3

Let $f(i,j)$ be the table defined by Algorithm DP3 for the first $j$ jobs and a selected count $i$ of on-time jobs. Its boundary values are $f(0,j)=0$ and $f(i,j)=+\infty$ for $i>j$. For $1\le i\le j$, it takes the minimum of $f(i,j-1)$ and the eligible transitions that append a batch of $k$ jobs, $1\le k\le\min(B,i)$. A transition uses $\max\{f(i-k,j-k),r_j\}+p$ and is eligible when that completion time does not exceed $d_{j-k+1}$. The main target is

$$U^*=n-\max\{i\in\{0,\ldots,n\}:f(i,n)<+\infty\}.$$

The maximum includes zero, which is always feasible in the table. The printed range begins at one and has no value when every job is tardy. This is the corrected boundary reading of the displayed answer on p. 771 (source).

Unequal processing times

The paper also gives a variant for jobs available at time zero, with nondecreasing processing times and due dates. Its transition replaces the release-time maximum and common $p$ by $f(i-k,j-k)+p_j$. The corresponding correctness statement is a further milestone (p. 771).

Significance

The structural results connect the optimization over arbitrary complete batch schedules to the restricted arrangements represented by the table. DP3 correctness then identifies the number of tardy jobs from finite table entries, including instances with no on-time job. The variable-time extension covers the related case where each job has its own duration but all jobs are available together.

The paper proves these results informally; this mission leaves their Lean proofs open. A complete formalization would supply reusable definitions of batch schedules, release-limited completion times, tardy-job counts, and a finite dynamic program with an explicit infinite value. The machine-checked statements and the local instance check establish the interface for that work, while the structural and correctness theorems remain solver targets.

Difficulty

The objective ranges over every valid batching and every processing order. The table examines an indexed prefix and places the last on-time batch among consecutive jobs. Establishing that the table's choices preserve the full optimum requires the existence statements in Lemmas 4 and 5. Reordering jobs is delicate because delaying a batch can change release feasibility and can make an earlier on-time job late. Equal due dates also require care: a due-date order alone need not put the latest release of a proposed batch at its last index.

Formalization scope

Jobs use Fin n, with index zero representing the paper's job 1; the table's $j$ is a prefix length. Data and completion times are natural numbers, matching the paper's integer-data setting; $+\infty$ in the table is WithTop ℕ. The schedule model uses nonempty batches of cardinality at most $B$, pairwise disjointness, and complete coverage. A batch starts at the maximum of its latest release and the preceding completion time. This earliest-start convention is sufficient for minimizing the regular tardy-job objective. The empty job set is included: its empty schedule has zero tardy jobs.

The strict implication $r_i<r_j\Rightarrow d_i\le d_j$ makes the paper's loose “agreeable” condition precise without forcing equal due dates for tied release times. For the recurrence, both release times and due dates are nondecreasing in job index, including their ties. This ensures that $r_j$ is the last batch's latest release and $d_{j-k+1}$ its earliest due date. The variable-time version similarly indexes by nondecreasing processing times and due dates, so the last job gives the batch duration. The table uses a minimum over exactly the paper's range $1\le k\le\min(B,i)$, with an empty range giving $+\infty$. Zero is included in the final maximum. Tardy jobs are scheduled in the underlying optimum; defining the optimum as an on-time subset or defining the table as that optimum would erase the two structural claims.

This mission covers correctness only. The paper's $O(n^2B)$ running-time statement and the bisection procedure are outside the formalization because they would need a specified computational cost model. The paper's FBEDD remark for this objective is also excluded: a three-job instance contradicts it. Contributions to the open theorem proofs, schedule-existence facts, and reusable batch scheduling lemmas are welcome.

Selected references

• C.-Y. Lee, R. Uzsoy, and L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 1992, pp. 764–775. DOI: 10.1287/opre.40.4.764.

Why a one-sided market can have a core

Workers can form groups and produce an output that they divide through salaries. A group may object to a proposed allocation when it can pay all of its members at least as much and one member more. The central question is whether any allocation survives every such objection. Kelso and Crawford's 1982 paper gives a sufficient condition based on how an imaginary firm would demand workers as their salaries change. This is useful when production depends on combinations of workers, yet there is no actual employer side to the market.

The one-sided result belongs to a seven-mission series: 1, the salary-adjustment process; 2, continuous-salary core existence; 3, this one-sided theorem; 4, firm-optimality; 5, comparative statics; 6, returns to workers; and 7, the no-core example. Each mission can be read independently. None of Kelso and Crawford's results was on Prove2Me before this series. The paper itself notes that Theorem 3 is similar in spirit to Shapley's core-existence result but logically independent: Shapley's convex-game condition concerns second differences of a characteristic function, whereas this theorem uses a condition on input demand. Kelso and Crawford, footnote 3.

The market and its allocations

Let $W$ be a finite set of workers, with $m=|W|$. A coalition technology $v$ assigns a real output $v(C)$ to each worker set $C\subseteq W$. A one-sided allocation consists of a partition $P=(C_z)$ of all workers and one real salary $s_i$ for each worker. The parts of $P$ are disjoint and cover $W$. Each worker has a utility $\mu^i(s_i)$ that is continuous and strictly increasing in salary, so salary comparisons express the same preferences as utility comparisons.

The paper's individual rationality condition D1′ asks for nonnegative salaries and one aggregate resource constraint:

$$s_i\ge 0\quad(i\in W),\qquad \sum_{i\in W}s_i\le\sum_{C\in P}v(C).$$

It does not require each partition block to finance its own salaries. An improving coalition is a worker set $C$ with salaries $r_i\ge s_i$ for every $i\in C$, a strict inequality for at least one member, and $\sum_{i\in C}r_i\le v(C)$. A D1′ allocation is in the strict core D2′ when no improving coalition exists. The empty coalition cannot improve because it contains no member whose salary could rise. These are equations (12)–(15) on pages 1492–1493 of the source paper.

To state gross substitutes (GS), imagine $m+1$ identical firms, each with production $v$. At a salary vector $s:W\to\mathbb R$, a firm's profit from employing $C$ is $\pi(C;s)=v(C)-\sum_{i\in C}s_i$; a demanded set maximizes this profit over all worker subsets. GS says that if salaries rise coordinatewise from $s$ to $s'$, then for every demanded set at $s$ there is a demanded set at $s'$ containing all workers of the old set whose salaries stayed unchanged. The requirement is over all real salary vectors, as in the continuous market of Section 2.

Formalization targets

Goal: Theorem 3

Assume nonnegative marginal production (MP′), no free lunch (NFL), and GS for the identical fictitious firms:

$$v(C\cup\{i\})-v(C)\ge 0,\qquad v(\varnothing)=0,\qquad \operatorname{GS}(v).$$

The goal is the exact existence statement

$$\exists (P,s),\quad (P,s)\text{ is a one-sided strict-core allocation for }v.$$

Theorem 3 appears on page 1493 of Kelso and Crawford. Its two milestones are claims from the proof: every dummy firm has zero profit at a fictitious-market strict-core allocation, and that allocation induces a one-sided strict-core allocation. Mission 2 targets the paper's Theorem 2, which supplies existence of the fictitious-market allocation; this mission does not pose a duplicate specialized version of it.

What the result gives

The theorem ensures that workers can be partitioned and paid without any group being able to make at least one of its members strictly better off while preserving every member's prior salary. It turns a condition on a firm's reactions to wage increases into stability of a market containing no firms. The result also identifies a concrete boundary for the core-existence argument: the paper later constructs a market without GS that has no core allocation in its two-sided setting. Kelso and Crawford, Section 6.

The theorem is proved in the 1982 paper; this mission asks for machine-checked statements and proofs of its one-sided definitions, the two transfer claims, and Theorem 3. The local Lean files compile as open statements, and a concrete one-worker instance checks that MP′, NFL and GS can hold together. That local check is not a proof of Theorem 3. The definition of GS for a finite demand problem can be reused beyond this mission, but the dummy-firm construction and the one-sided D1′–D2′ predicates follow this paper's conventions.

Why the transfer is delicate

A strict-core allocation of a two-sided market controls coalitions containing a firm, while D2′ is expressed entirely through worker coalitions. The fictitious market has more firms than workers, which forces at least one firm to employ nobody. The proof must connect that observation to every firm's profit and then translate a one-sided improving coalition into a two-sided improvement. Individual rationality also has to preserve the paper's aggregate budget condition. Merely assigning each worker to a firm or showing nonnegative firm profits would leave these links unproved.

Formalization scope

Workers form an arbitrary finite type; the empty case is included. The fictitious firms have type Fin (m + 1), so their count is strictly greater than the worker count even when $m=0$. Salaries and output are real. In the fictitious market, every firm uses the same $v$, each worker's utility at every firm is $\mu^i(s)$, and reservation salary is zero, matching unemployment utility $\mu^i(0)$. The milestones retain arbitrary strictly increasing continuous functions $\mu^i$; Theorem 3 does not quantify over them because D1′ and D2′ compare salaries directly. Theorem 3's GS condition ranges over all real salary vectors, not a discrete salary grid.

Mathlib finite partitions contain nonempty parts. The paper permits empty indexed groups, but NFL makes them contribute zero output. The allocation model assigns every worker to one firm, and strict blocking allows any worker coalition, including the empty set, although strict improvement excludes that case. D1′ uses one total salary bound; a per-group bound would change the theorem. D2′ requires a strict gain in a worker's salary, not merely slack in the production budget. No vacuous regularity condition, fixed special technology, or restriction to a single worker is part of the mission goal.

Contributions are welcome on the finite partition interface, properties of profit-maximizing demand under GS, the zero-profit claim, and the transfer from fictitious firms to worker coalitions. The shared market and demand definitions are kept in their own module so they can be consolidated with the other missions of this paper.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6), 1982, pp. 1483–1504. DOI: 10.2307/1913392.
• L. S. Shapley, Cores of convex games, International Journal of Game Theory 1, 1971, pp. 11–26. DOI: 10.1007/BF01753431.

Motivation

Two stationary random sequences can have identical distributions at each individual time while differing in their dependence across time. Comparing only their one-time marginals therefore misses a feature relevant to stochastic-process comparison. Ornstein's $\bar d$ measures the cost of matching two whole stationary processes: it minimizes the expected discrepancy at one time over joint laws that are themselves stationary. Kamae, Krengel, and O'Brien use stochastic order to replace that optimization over pairs of processes with an optimization over a single common lower process in Theorem 8 of their 1977 paper. This mission formalizes that identity and the stationary coupling results supporting it.

Setting

A two-sided path with values in a space $E$ is a sequence $\omega=(\omega^n)_{n\in\mathbb Z}$. The shift $T$ sends $\omega$ to the path whose coordinate $n$ is $\omega^{n+1}$. A probability law $P$ on paths is stationary, written $P\in\mathcal S_T$, when $P\circ T^{-1}=P$. A law $\nu$ on pairs of paths is jointly stationary, written $\nu\in\mathcal S_S$, when it is invariant under $S(\omega_1,\omega_2)=(T\omega_1,T\omega_2)$. Its first and second marginals are denoted $\nu_1$ and $\nu_2$. These are the objects defined at the start of Section 8.

When $E$ has a partial order, paths are ordered coordinatewise: $\omega_1\leq\omega_2$ means $\omega_1^n\leq\omega_2^n$ for every integer $n$. For probability laws on any such space, write $P\prec Q$ if $\int f\,dP\leq\int f\,dQ$ for every bounded, measurable, increasing real function $f$. Thus stochastic order compares laws through all bounded increasing observations, including observations that depend on several time coordinates. The paper introduces this order on a partially ordered Polish space whose order graph is closed and whose measurable sets are Borel sets in Section 1.

For real-valued paths, $\omega^0$ is the value at time zero. If the time-zero values under stationary laws $P$ and $Q$ are integrable, define Ornstein's distance by

$$\bar d(P,Q)=\inf_{\substack{\nu\in\mathcal S_S\\\nu_1=P,\,\nu_2=Q}} \int |\omega_1^0-\omega_2^0|\,\nu(d\omega_1,d\omega_2).$$

The stationary constraint on $\nu$ is part of the definition. It asks for a matching of the full processes, even though the cost is evaluated at one coordinate. The paper notes that this formula is equivalent to Ornstein's original definition for the processes considered here on p. 910.

Formalization targets

The ordered special case is Lemma 3: if $P\prec Q$, then

$$\bar d(P,Q)=\int\omega^0\,Q(d\omega)-\int\omega^0\,P(d\omega).$$

The main target is Theorem 8, equation (18). For stationary real process laws $P,Q$ with finite first moments at time zero,

$$\bar d(P,Q)= \int\omega^0\,P(d\omega)+\int\omega^0\,Q(d\omega) -2\sup_{\substack{R\in\mathcal S_T\\R\prec P,\,R\prec Q}} \int\omega^0\,R(d\omega).$$

The supremum ranges over stationary laws of whole paths, ordered on the full coordinatewise path space. The milestone list includes Theorem 7's stationary monotone coupling, Lemmas 2 and 3, and three claims made inside the proof of Theorem 8: the triangle inequality $\bar d(P,Q)\le\bar d(P,R)+\bar d(R,Q)$, which the paper asserts without proof ("since $\bar d$ is a distance"), the attainment of the infimum defining $\bar d$, and the fact that the law of the coordinatewise minimum of an optimal stationary coupling lies below both $P$ and $Q$. These are the statements from the paper that delimit the target.

Significance

The identity expresses a distance defined through stationary joint distributions using only stationary laws below both inputs in stochastic order. It therefore links a coupling cost to an order-theoretic optimization. In the ordered case, Lemma 3 evaluates the distance directly from the difference of means. The authors point out that the general formula replaces an infimum over laws on a product path space by a supremum over laws on one path space on p. 911.

The 1977 results are proved on paper; these mission statements are open Lean proof targets. A completed formalization would supply reusable definitions for stationary path laws, stationary couplings, stochastic order on path spaces, and $\bar d$, together with checked statements about their interaction. It would also make the closed-order and first-moment conditions explicit at every point where a subsequent result uses them. The separate mission for Theorem 1 contains the general coupling characterization that the paper invokes in Theorem 7.

Difficulty

The cost in $\bar d$ inspects only time zero, but admissibility of a coupling involves every time coordinate at once. An arbitrary coupling of the time-zero marginals need not extend to a stationary coupling of the two processes. The stationary-coupling existence statement must preserve both full path marginals and the coordinatewise order. On the optimization side, taking an infimum in the real numbers is justified only after the coupling class is shown nonempty and its costs are finite; attaining the infimum requires more than those two facts. These are the obstacles made explicit by Theorem 7 and the proof of Theorem 8.

Formalization scope

The Lean path space is $\mathbb Z\to E$, with Mathlib's product topology, Borel measurable structure, and coordinatewise order. The shift sends coordinate $n$ to the old coordinate $n+1$. For Theorem 7, $E$ carries the paper's standing assumptions: it is Polish, its order is a closed partial order, and its measurable structure is Borel. Measurability of quantified functions is explicit, following the paper's convention that sets and functions under discussion are measurable. Theorem 8 and its Section 8 milestones specialize to $E=\mathbb R$.

The real-valued definition of $\bar d$ takes the infimum over jointly stationary probability couplings with the specified full path marginals. Under the target's finite-first-moment hypotheses, the product coupling makes this class nonempty, every displayed cost is integrable, and costs are bounded below by zero. The goal states the supremum with an explicit finite least upper bound. It considers common lower laws with an integrable time-zero coordinate: such laws give the finite values intended by the paper, and this restriction does not remove the optimal value. These choices exclude totalized integrals and default real infima or suprema from supplying a spurious identity. Theorem 7's support condition is concentration on the closed set of ordered path pairs.

Reusable contributions include general facts about stationary measures on countable products, measurable coordinatewise order and meet maps, and stationary coupling compactness. The target specifically requires the order to test bounded increasing functions on the full path space; replacing it with a comparison of time-zero marginals would give a different claim. Likewise, dropping the joint stationarity constraint from the definition of $\bar d$ would turn it into the Kantorovich (Wasserstein-1) distance of the time-zero marginals, a different and in general smaller quantity; the formalization keeps that constraint. The source is the published Annals of Probability version; throughout this mission printed page $=$ PDF page $+898$.

Selected references

• T. Kamae, U. Krengel, and G. L. O'Brien, Stochastic Inequalities on Partially Ordered Spaces, The Annals of Probability 5(6), 899–912, 1977. DOI: 10.1214/aop/1176995659.

Motivation

Labour markets match workers to firms that hire teams: a firm's output depends on the whole set of workers it employs, while each worker holds one job. A salary agreement is stable when no firm and group of workers can renegotiate among themselves to the benefit of all of them. Shapley and Shubik (1971) showed that such stable outcomes exist when each firm hires at most one worker and utility is transferable; Crawford and Knoer (1981) extended this to general utilities, still one-to-one. Kelso and Crawford (1982) let firm size be endogenous and identified the condition under which existence survives: workers must be gross substitutes for every firm. Their condition later became the standard assumption for existence of Walrasian equilibrium with indivisible goods (Gul and Stacchetti, 1999) and the basis of matching with contracts (Hatfield and Milgrom, 2005).

This mission is the second of a seven-mission series on the paper: 1, the salary-adjustment process; 2, existence of a strict core with continuous salaries (this mission); 3, one-sided coalition formation; 4, the firm-optimal allocation; 5, comparative statics; 6, gross substitutes versus nonincreasing returns; 7, a market with no core. Each mission is self-contained. Nothing of this paper was on Prove2Me before this series.

Setting

There is a finite set $W$ of $m$ workers and a nonempty finite set $F$ of firms. Worker $i$'s utility of working for firm $j$ at salary $s\in\mathbb R$ is $u^i(j;s)$, strictly increasing and continuous in $s$. Firm $j$'s gross product when it hires the set $C\subseteq W$ is $y^j(C)$, and its profit at the salary vector $s^j=(s_{ij})_{i\in W}$ is

$$\pi^j(C;s^j)=y^j(C)-\sum_{i\in C}s_{ij}.$$

The reservation salary $\sigma_{ij}$ is defined by $u^i(j;\sigma_{ij})=u^i(0;0)$, worker $i$'s utility of unemployment. Section 2 of the paper assumes, for every firm $j$:

• (MP) $y^j(C\cup\{i\})-y^j(C)-\sigma_{ij}\ge0$ whenever $i\notin C$;
• (NFL) $y^j(\emptyset)=0$;
• (GS) if $C$ maximizes $\pi^j(\cdot\,;s^j)$ and $\tilde s^j\ge s^j$ componentwise, then some maximizer $\tilde C$ of $\pi^j(\cdot\,;\tilde s^j)$ contains every $i\in C$ with $\tilde s_{ij}=s_{ij}$.

An allocation assigns each worker $i$ to a firm $f(i)$ at salary $s_{if(i)}$; firm $j$ hires $C^j=\{i:f(i)=j\}$. It is individually rational (D1) if $s_{if(i)}\ge\sigma_{if(i)}$ and $\pi^j(C^j;s^j)\ge0$ for all $i,j$. A firm $j$, a set $C$ and salaries $r_{ij}$ improve upon it if $u^i(j;r_{ij})\ge u^i(f(i);s_{if(i)})$ for $i\in C$ and $\pi^j(C;r^j)\ge\pi^j(C^j;s^j)$, with at least one inequality strict; they strictly improve upon it if all are strict. A strict core allocation (D2) is an individually rational allocation no coalition improves upon; a core allocation (D3) is one no coalition strictly improves upon. In the continuous market coalitions may use any real salaries; in the discrete market of unit $\delta>0$ all salaries lie on the grids $\sigma_{ij}+\delta\mathbb N$.

Formalization targets

Goal: Theorem 2

Under regular utilities, (MP), (NFL), the reservation-salary relation and (GS) on all real salary vectors,

$$\exists\,(f;s)\ \text{individually rational that no firm–worker coalition can improve upon (D2).}$$

The goal fixes no grid, no constant and no particular technology.

Milestones, in the order of the paper's proof

1. Every discrete market has a core (p. 1490): for every $\delta>0$, if (GS) holds on grid salary vectors, a discrete core allocation (D3) exists.
2. The gains are bounded above zero (p. 1491, eqs. (8)–(11)): if the continuous market has no strict core allocation, there is $H>0$ such that every individually rational allocation admits a coalition that leaves its workers no worse off and raises its firm's profit by at least $H$.
3. A fine grid inherits the improvement (pp. 1491–1492): with such an $H$, every individually rational grid allocation of unit $0<\delta<H/(m+1)$ can be strictly improved upon in the discrete market.

Significance

Theorem 2 gives existence of a stable assignment of workers to firms with salaries, for arbitrary technologies under which workers are gross substitutes, without any convexity or divisibility of labour. Because the core and the competitive equilibrium coincide in this model when salaries are divisible (p. 1487), it is also an existence theorem for competitive equilibrium in a market with indivisible workers; the example of mission 7 shows that it fails without (GS). The Shapley–Shubik assignment game is the special case $u^i(j;s)=a_{ij}+s$, $y^j(C)=\sum_{i\in C}b_{ij}$ with at most one worker per firm.

The result has been proved since 1982; it has not been machine-checked. Prove2Me holds a formalization of the Shapley–Shubik assignment game (AssignmentGame.CoreLP), whose core-existence theorem is a different model and is not yet proved, and Murota's gross-substitutes axioms for demand on $\mathbb Z^n$, which concern one price per good rather than firm-specific salary vectors over sets of workers. Neither supplies this market or Theorem 2.

Difficulty

Discrete core allocations exist at every unit $\delta$, so the natural first idea is to take a sequence of them as $\delta\to0$ and pass to a limit. A limit of discrete core allocations need only be a core allocation of the continuous market in the weak sense D3, and a coalition that improves upon the limit may need salaries off every grid; nothing in the discrete statements controls how much a coalition gains, so the blocking coalitions of the continuous market may vanish on the grids. The required control has to be uniform over all individually rational allocations, which form an infinite set, while each blocking comparison involves the utilities of several workers and a nonadditive technology. A second obstacle is in the paper's notation: the gain (8) uses the salary $\rho_{ij}$ with $u^i(j;\rho_{ij})=u^i[f(i);s_{if(i)}]$, which need not exist when $u^i(j;\cdot)$ is bounded.

Formalization scope

Workers and firms are arbitrary finite types; every theorem assumes at least one firm (the paper's $n\ge1$), since with no firm and some worker no allocation exists. Salaries, utilities, outputs and profits are real numbers. An allocation has no unemployment, as in D1. The reservation salaries $\sigma$ are data, and the paper's definition of $\sigma_{ij}$ enters as the hypothesis $u^i(j;\sigma_{ij})=u^i(k;\sigma_{ik})$; it is assumed on the goal and on milestones 2 and 3, where the discretization step needs every improving salary to be at least $\sigma_{ij}$. Milestone 1 assumes neither this relation nor continuous (GS). The standing assumptions of p. 1486, which Theorem 2's sentence does not repeat, are hypotheses of the goal.

Explicit readings of the paper's phrases: "continuous market" means coalitions may use any real salary; "bounded above zero" is one $H>0$ valid for every individually rational allocation, stated without $\rho_{ij}$ by quantifying over admissible coalition salaries; "the unit of measurement smaller than $H/(m+1)$" is $0<\delta<H/(m+1)$ with $m=|W|$ and the division in $\mathbb R$; the discrete market's salaries are $\sigma_{ij}+\delta k$, $k\in\mathbb N$, the paper's integer salaries starting at $\sigma_{ij}$ (R1, R4) with a general unit.

Trivializing formalizations are ruled out: the goal assumes (GS) on all real vectors rather than on one grid (a stronger theorem the paper does not prove), its conclusion is the strict core D2 rather than the weaker core D3, and its hypotheses are satisfiable (a one-worker, one-firm market satisfies all of them).

A complete development needs finite optimization over sets of workers, a compactness argument over the individually rational salary schedules of each assignment, and the existence of discrete core allocations (the existence form of Theorem 1, mission 1). Proofs of the milestones, of the equivalence of D2 and D3 in the continuous market, and lemmas on finite demand correspondences reusable across the series are welcome.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job Matching, Coalition Formation, and Gross Substitutes, Econometrica 50(6), 1982, 1483–1504. https://doi.org/10.2307/1913392
• V. P. Crawford and E. M. Knoer, Job Matching with Heterogeneous Firms and Workers, Econometrica 49(2), 1981, 437–450. https://doi.org/10.2307/1912751
• L. S. Shapley and M. Shubik, The Assignment Game I: The Core, International Journal of Game Theory 1, 1971, 111–130. https://doi.org/10.1007/BF01753437
• F. Gul and E. Stacchetti, Walrasian Equilibrium with Gross Substitutes, Journal of Economic Theory 87(1), 1999, 95–124. https://doi.org/10.1006/jeth.1999.2531
• J. W. Hatfield and P. R. Milgrom, Matching with Contracts, American Economic Review 95(4), 2005, 913–935. https://doi.org/10.1257/0002828054825466