Operations Research

Burn-in ovens as batch processing machines

In semiconductor manufacturing, finished chips go through burn-in: they are loaded on boards and held in an oven at high temperature to expose early failures. An oven holds a bounded number of boards, a load cannot be interrupted once started, and a chip may stay in the oven longer than its specified burn-in time but not shorter. Lee, Uzsoy and Martin-Vega (Oper. Res. 40(4), 1992) model the oven as a batch processing machine and give polynomial algorithms for several due-date objectives. The model has since become a standard one in scheduling theory; the survey of Potts and Kovalyov (2000) traces the batching literature that grew from it.

This mission formalizes the part of the paper's §3 on minimizing maximum tardiness when all jobs are available at time $0$ and processing times and due dates are agreeable. That is the problem the paper writes $1/B/T_{\max}$. The paper's own route is a feasibility test by dynamic programming, Algorithm DP2, which a bisection over due-date shifts turns into a $T_{\max}$ minimizer.

The batch machine

There are $n$ jobs $1,\dots,n$. Job $i$ has a processing time $p_i$ and a due date $d_i$, both natural numbers. The machine has capacity $B\ge 1$. A batch is a nonempty set of at most $B$ jobs processed together. It occupies the machine for the processing time of its longest job,

$$t(P)=\max_{i\in P}p_i .$$

A batch schedule of a job set $J$ is a sequence $S=(P_1,\dots,P_m)$ of pairwise disjoint batches covering $J$, processed in this order and back to back from time $0$. Batch $P_k$ and all of its jobs complete at $C(P_k)=t(P_1)+\dots+t(P_k)$. The makespan is $C_{\max}(S)=C(P_m)$, and the maximum tardiness is

$$T_{\max}(S)=\max_k\max_{i\in P_k}\max\{0,\,C(P_k)-d_i\}.$$

A schedule is feasible when $T_{\max}(S)=0$, that is, when every job meets its due date.

A sequence is in batch-EDD order (Definition 1) if no job in an earlier batch has a strictly later due date than a job in a later batch. Processing times and due dates are agreeable if $p_i<p_j$ implies $d_i\le d_j$. A schedule is consecutive when every batch is a block $\{i,i+1,\dots,k\}$ of indices and the blocks appear in increasing order.

Algorithm DP2 computes values $f(0),\dots,f(n)\in\mathbb N\cup\{\infty\}$:

$$f(0)=0,\qquad f(j)=\min_{\max\{1,\,j-B+1\}\le i\le j} f_i(j),\qquad f_i(j)=\begin{cases}f(i-1)+p_j,& f(i-1)+p_j\le d_i,\\ \infty,&\text{otherwise.}\end{cases}$$

Formalization targets

Goal: correctness of DP2

Index the jobs so that $d_1\le\dots\le d_n$ and $p_1\le\dots\le p_n$. Then for every $0\le j\le n$,

$$f(j)=\min\{\,C_{\max}(S) : S \text{ a batch schedule of jobs } 1,\dots,j,\ T_{\max}(S)=0\,\},$$

with $\min\emptyset=\infty$. The minimum ranges over all schedules: any batching, any order. This is the paper's reading of $f(j)$ as "the minimum completion time of jobs $1,\dots,j$ if they can be scheduled feasibly, and infinity otherwise".

Milestones

1. Lemma 3. With agreeable processing times and due dates, if a feasible schedule exists, then a feasible schedule in batch-EDD order exists.
2. Consecutive partition (justification of DP2). Under the index order above, if jobs $1,\dots,j$ can be scheduled feasibly, then some feasible schedule of minimum makespan is consecutive.
3. FBEDD. With equal processing times and due dates in index order, the Full-Batch EDD schedule $\{1,\dots,B\},\{B+1,\dots,2B\},\dots$ has $T_{\max}$ no larger than that of any batch schedule.

Significance

DP2 is the paper's feasibility test for $1/B/T_{\max}$ with agreeable data. With a bisection over the common shift of the due dates, it yields a polynomial algorithm for minimizing $T_{\max}$. A correct statement of what DP2 computes is therefore the core of that result. The same consecutive-partition structure underlies the paper's DP1 (release times, equal processing times) and DP3 (number of tardy jobs), which are separate missions of this series.

No machine-checked proof of any of these statements is known. The dynamic program's correctness is argued in the paper only by reference ("the justification of this algorithm is similar to that of algorithm DP1"), and the index order it needs is left implicit. A formal proof pins down exactly which ordering of the jobs makes the recursion correct.

Difficulty

The recursion charges $p_j$ for the last batch $\{i,\dots,j\}$ and checks only $d_i$. Both shortcuts rely on the jobs being sorted by due date and by processing time at the same time. Lemma 3's exchange argument sorts a feasible schedule by due date, but it does not by itself produce consecutive blocks of a fixed index order. With ties in due dates the indexing also has to be compatible with processing times. Without that, the recursion is wrong: for $B=2$, $p=(3,1)$, $d=(5,5)$ it gives $f(2)=1$, while every schedule takes at least $3$. The goal compares the DP with the optimum over all schedules, so the exchange arguments have to bridge arbitrary batchings and the consecutive ones the recursion enumerates. That bridge is the main step left to prove.

Formalization scope

• Jobs are Fin n (job $i$ of the paper is index $i-1$); jobs $1,\dots,j$ are jobsUpTo n j. Data are natural numbers; the paper assumes integral data (p. 769).
• A schedule is a List (Finset (Fin n)); validity requires nonempty batches of size at most $B$ inside the job set, pairwise disjoint, covering the set. Batches start as early as possible. Batch time is the maximum processing time in the batch.
• $\infty$ is ⊤ : ℕ∞, and the goal's minimum is the infimum in ℕ∞, which is ⊤ exactly when no feasible schedule exists. DP2 is defined by the printed recursion, not as an optimum.
• Explicit readings of loose phrases:
  • "jobs are indexed in increasing order of due dates" (p. 767) becomes Monotone d ∧ Monotone p for DP2 and its justification, and Monotone d for FBEDD;
  • "agreeable" (printed "$p_i\le p_j$ implies $d_i\le d_j$", which would force equal due dates for equal processing times) becomes the strict form $p_i<p_j\Rightarrow d_i\le d_j$, a weaker hypothesis;
  • "optimally solves" for FBEDD becomes "valid, and $T_{\max}$ at most that of every valid schedule";
  • "a consecutive partition problem" becomes the existence of a consecutive minimum-makespan feasible schedule.
• Not formalized: the $O(nB)$ and $O[nB\log_2(np_{\max})]$ running times, the bisection procedure, and the remark that $np_{\max}$ bounds $T_{\max}$.
• Trivializations ruled out: the goal's minimum ranges over all valid schedules, not only batch-EDD or consecutive ones (which would assume the milestones), and DP2 is the printed recursion, not a restatement of the optimum.
• Infrastructure needed: list-indexed schedules, exchange arguments on adjacent batches, and induction on prefix length for the recursion. The single-machine batch model is shared in spirit with missions 1 and 3 of this series. No published platform definition was reused, since nothing on batch machines exists yet.

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
• Y. Ikura, M. Gimple, Efficient scheduling algorithms for a single batch processing machine, Operations Research Letters 5(2), 61–65, 1986. https://doi.org/10.1016/0167-6377(86)90104-5
• C. N. Potts, M. Y. Kovalyov, Scheduling with batching: A review, European Journal of Operational Research 120(2), 228–249, 2000. https://doi.org/10.1016/S0377-2217(99)00153-8

Motivation

Alan S. Manne's Linear Programming and Sequential Decisions (Management Science 6(3), 1960, pp. 259–267) is the first formulation of an infinite-horizon, average-cost sequential decision problem as a linear program. The illustration is a single-item inventory problem, but the construction, with unknowns indexed by a state and a decision and constraints expressing statistical equilibrium, became the standard state–action frequency linear program of Markov decision processes. Later LP approaches to average-cost Markov decision processes, including constrained ones, build on it.

Timeline of the LP approach to average-cost problems:

• 1960 — Manne: the inventory model as a linear program in the joint probabilities of (stock level, production quantity); mixed strategies allowed; the decision rule is read off as a conditional probability.
• 1960 — H. M. Wagner, in a companion note in the same issue, shows that an optimal solution consisting of pure strategies exists.
• 1962 — C. Derman (Management Science 9(1), 1962) gives the general finite-state, finite-action version, assuming every stationary randomized rule yields an irreducible chain.
• 1960 — F. d'Epenoux (Revue Française de Recherche Opérationnelle 4, No. 14; English translation 1963) treats the discounted criterion by linear programming, as Manne's closing note records.

Setting

A positive integer $T$ bounds inventory accumulation; the stock levels are $0,1,\dots,T$. At the start of a month the initial stock $i$ is observed and a production quantity $j$ is chosen; the available stock is $k=i+j$. The month's demand $n\in\{0,1,2,\dots\}$ is independent of everything else and has law $p_n$. Backlogs are excluded, so the terminal stock is $t=\max(0,k-n)$, which becomes the next initial stock. A finite set $A$ of admissible pairs $(i,j)$, all with $i+j\le T$ and containing $(i,0)$ for every $i\le T$, lists the decisions available at each stock level. Costs are three arbitrary real functions: $C_1(i)$ of the initial stock, $C_2(j)$ of the production quantity, and $C_3(n-k)$ of the shortage level.

A stationary randomized decision rule $q(j\mid i)$ is a conditional probability of producing $j$ at stock $i$, supported on admissible pairs. It makes the initial stock a Markov chain. A statistical equilibrium of $q$ is a stationary distribution $y=(y_0,\dots,y_T)$ of that chain: the law $y'$ of the terminal stock equals the law $y$ of the initial stock, (2). The expected monthly cost (1) of $q$ in the equilibrium $y$ is

$$\mathcal EC_1(i)+\mathcal EC_2(j)+\mathcal EC_3(n-k),$$

the expectation taken under the joint law $y_i\,q(j\mid i)\,p_n$ of (initial stock, production, demand).

The linear program has one unknown $x_{ij}$ per admissible pair, the joint probability of (initial stock $i$, production $j$). Its constraints are $x_{ij}\ge0$, (4) $\sum_{i,j}x_{ij}=1$, and the equilibrium equations

$$\text{(8.t)}\qquad \sum_j x_{tj}=\sum_{\substack{i,j,n:\\ i+j-n=t}}p_nx_{ij}\qquad(t=1,\dots,T),$$

and its objective (9) is $\sum_{i,j}c_{ij}x_{ij}$ with the cost coefficients (10)

$$c_{ij}=C_1(i)+C_2(j)+\sum_np_nC_3(n-i-j).$$

The companion equation (8.0) for $t=0$ has right-hand side $\sum_{i+j-n\le0}p_nx_{ij}$ and is omitted from the constraints. A feasible $x$ is decoded into $y_i=\sum_jx_{ij}$ and $q(j\mid i)=x_{ij}/y_i$.

Formalization targets

The paper labels no theorem or lemma. The goal is assembled from §1 (third paragraph), §3 (N.B.), §4 (last two paragraphs), §5 and §7 (3), and every milestone is cited by section, display, table or footnote.

Goal: an LP optimum gives an optimal stationary rule

Assume $\sum_np_n|C_3(n-i-j)|<\infty$ for every admissible pair. Then the linear program has an optimal solution, and for every optimal solution $x^*$, with decoding $(q^*,y^*)$, $q^*$ is a stationary randomized rule, $y^*$ is a statistical equilibrium of $q^*$, and

$$\mathrm{Cost}(q^*,y^*)=\sum_{i,j}c_{ij}x^*_{ij}\le \mathrm{Cost}(q,y)$$

for every stationary randomized rule $q$ and every statistical equilibrium $y$ of $q$.

Milestones

1. (7): under a rule in a distribution $y$, the law of the terminal stock is the right-hand side of (7)/(8) evaluated at $x_{ij}=y_iq(j\mid i)$.
2. (8.0)–(8.T): a rule in statistical equilibrium yields a point satisfying $x\ge0$, (4) and all of (8.0)–(8.T).
3. (8.0) is redundant: (4) and (8.1)–(8.T) imply (8.0).
4. §3, N.B.: every feasible $x$ equals $y_iq(j\mid i)$ for its decoding $(q,y)$, with $y$ an equilibrium of $q$.
5. (10): the expected monthly cost (1) under the joint law $x_{ij}p_n$ equals $\sum c_{ij}x_{ij}$.
6. Table 1: the cost coefficients of the §6 example ($T=3$, $p=(2/3,0,1/3)$, $C_1(i)=i$, $C_2(j)=3j$, $C_3(m)=\max[0,6m]$, $j\in\{0,1\}$) are $4,5,3,4,2,5,3$.
7. Table 2, footnote 3: $x_{01}=1/3$, $x_{11}=2/9$, $x_{20}=4/9$ is optimal with cost $31/9$; the do-nothing solution costs $4$.
8. Footnote 5: the implicit prices $-7/3,-13/3,-11/3$ of (8.1)–(8.3), with $31/9$ on (4), are an optimal dual solution.

Significance

The result turns an infinite-horizon control problem into a finite linear program. Equilibrium joint laws of (state, decision) under stationary randomized rules are exactly the feasible points of a polytope, and the average cost is linear on it. Consequences include computability by the simplex method; an economic reading of the dual variables (Manne's footnote 5 interprets them as the relative advantage of starting at a given stock level, related to Bellman's functional equation); and, in later work, the treatment of side constraints, which dynamic programming handles poorly.

The result is classical and proved in the paper (largely by inspection of the definitions). It has not been formalized. The formalization adds three things. First, a precise statement of what is optimized when the chain of a rule is not irreducible: the paper's §7 (3) concedes that a "decomposable" optimum makes the equilibrium depend on initial conditions, and the goal resolves this by optimizing over (rule, equilibrium) pairs. Second, an explicit treatment of the stock levels the equilibrium never visits, where the paper's quotient $x_{ij}/\sum_jx_{ij}$ is undefined. Third, a machine-checked numerical example whose LP is derived from the general definitions, not entered by hand. Derman's later irreducible-case version exists on the platform as a separate open statement; this mission covers Manne's irreducibility-free version on state-dependent action sets.

Difficulty

Each step is elementary; the work is bookkeeping across three descriptions of the same object. The equilibrium is defined through the transition kernel of the controlled chain, the LP through the displayed sums over $(i,j,n)$ with conditions $i+j-n\le0$ and $i+j-n=t$, and the cost through the joint law of three variables. Identifying them needs a reindexing of the admissible pairs by stock level, the interchange of a finite sum with an infinite sum over demands, and $\sum_np_n=1$. The naive argument "the LP constraints are the equilibrium equations, so the LP optimum is the optimal rule" skips two points. The constraints omit (8.0), so equilibrium at stock level $0$ must be recovered from (4) and the bound $i+j\le T$. And the decoding fails at unvisited stock levels unless a default action is supplied. Existence of an LP optimum requires compactness of the feasible polytope, not just its nonemptiness.

Formalization scope

All statements live in the namespace ManneLP.Equilibrium. Conventions:

• Stock levels and production quantities are natural numbers; a model carries $T>0$, the admissible set $A$ (a Finset (ℕ × ℕ) with $i+j\le T$ and every $(i,0)\in A$), a demand law $p:\mathbb N\to\mathbb R$ with $p_n\ge0$ and HasSum p 1, and costs $C_1,C_2:\mathbb N\to\mathbb R$, $C_3:\mathbb Z\to\mathbb R$. The shortage level $n-i-j$ is an integer; no convexity, sign or monotonicity of the costs is assumed.
• The admissible set is a parameter: §6 imposes a capacity limit $j\le1$. Reading of the page: $i+j\le T$ is how §2's requirement $\max(0,k-n)\le T$ holds whatever the demand; $(i,0)\in A$ (producing nothing is possible) is implicit in §2.
• The terminal stock is computed by truncated subtraction in $\mathbb N$, which equals $\max(0,k-n)$. Sums over demands are tsums; the demand is not assumed bounded. The goal and the cost identity assume the expected shortage cost at each admissible pair is finite (absolutely summable), which the page takes for granted.
• A statistical equilibrium is a stationary distribution of the chain of the rule, defined from the transition probabilities, not from (8). The expected monthly cost is defined from the joint law of (stock, production, demand), not as $\sum c_{ij}x_{ij}$. The LP constraint set omits (8.0), exactly as the page does.
• The decoded rule uses the default action $j=0$ at stock levels with $\sum_jx_{ij}=0$; any admissible default would do.
• Table 2's $x_{30}=\varepsilon$ is the paper's device against degeneracy; the example's solution has $x_{30}=0$. Footnote 5 prints no price for (4); $31/9$ is the price forced by equal objectives, and the dual optimum is not claimed unique.

Trivializing formalizations are ruled out: equilibrium is not defined as (8) (which would make milestone 2 vacuous), (8.0) is not a constraint (which would make milestone 3 vacuous), the cost is not defined as $\sum c_{ij}x_{ij}$ (which would make milestone 5 and the goal's cost clause definitional), and the optimality comparison ranges over all rules and all of their equilibria, not over irreducible chains or pure rules.

Contributions welcome: proofs of the milestones and the goal; computations of the §6 example from the general definitions; reusable lemmas on stationary distributions of finite stochastic matrices and on the existence of LP optima over compact polytopes.

Selected references

• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3), 259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• H. M. Wagner, On the Optimality of Pure Strategies, Management Science 6(3), 268–269, 1960. https://doi.org/10.1287/mnsc.6.3.268
• C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1), 16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
• F. d'Epenoux, A Probabilistic Production and Inventory Problem, Management Science 10(1), 98–108, 1963 (translation of the 1960 French paper). https://doi.org/10.1287/mnsc.10.1.98

Motivation

Maximum likelihood estimates, least-squares fits and sample-average approximations of stochastic programs solve $0 = \bar f^\nu(x)$, where $\bar f^\nu$ averages a random integrand over $\nu$ observations. Their classical asymptotic theory rests on the implicit function theorem and needs a smooth, unconstrained problem.

When the estimate is constrained to a set, for example a nonnegativity constraint, a simplex or a polyhedron, the first-order conditions become a generalized equation

$$0 \in f(z, x) + N(x),$$

where $N$ is a multifunction such as the normal cone of the constraint set. The same form describes optimality conditions of stochastic programs and variational inequalities. Aitchison and Silvey (1958) treated equality-constrained maximum likelihood. Huber (1967) allowed nonsmooth estimating functions but required an open parameter domain. Dupačová and Wets (1988) and Shapiro (1989) derived limit laws for solutions of stochastic programs under smoothness of the expected gradient. King and Rockafellar (1993) gave a general theory that needs neither smoothness of the expected map nor single-valuedness of $N$: the limit law of the normalized error is the image of a Gaussian under a contingent derivative, a positively homogeneous and generally nonlinear map, so the limit is generally not normal.

Setting

Let $Z$ be a separable Banach space with norm $\|\cdot\|$, and let $|\cdot|$ be the Euclidean norm on $\mathbb R^n$ and $\mathbb R^m$. A multifunction $G : Z \rightrightarrows \mathbb R^n$ assigns a set $G(z) \subseteq \mathbb R^n$ to each $z$. Its graph is $\operatorname{gph} G$ and its inverse is $G^{-1}(x) = \{z \mid x \in G(z)\}$.

For sets $A_t$ indexed by $t \downarrow 0$, the upper limit $\limsup A_t$ consists of the points $x$ with $x = \lim x_k$, $x_k \in A_{t_k}$ for some $t_k \downarrow 0$, and the lower limit of the points reachable along every such sequence. The contingent derivative of $G$ at $(z, x) \in \operatorname{gph} G$ is the multifunction $DG(z|x)$ with

$$\operatorname{gph} DG(z|x) = \limsup_{t \downarrow 0} t^{-1}\big[\operatorname{gph} G - (z,x)\big].$$

$G$ is proto-differentiable when this upper limit equals the lower limit, and semi-differentiable when $t^{-1}[G(z + t w') - x] \to DG(z|x)(w)$ as $t \downarrow 0$ and $w' \to w$. A single-valued $g$ is B-differentiable at $z$ when $t^{-1}[g(z + tw') - g(z)] \to Dg(z)(w)$ in the same sense.

The deterministic problem is $0 \in f(z, x) + N(x)$ with $f : Z \times \mathbb R^n \to \mathbb R^m$, data $z$ and solution map $J(z)$. At a reference pair $(z^*, x^*)$ set $F = f(z^*, \cdot) + N$. The analytical assumptions M.1–M.4 are as follows. $f$ is jointly continuous and B-differentiable in each variable, with the $z$-derivative $D_z f(z^*, x^*)$ strong (uniform in $x$ near $x^*$). $N$ is closed and proto-differentiable. $F$ is subinvertible: $0 \in F(x^*)$, and a closed-graph, convex-valued selection of $F^{-1}$ near $0$ passes through $x^*$. The contingent derivative $DF^{-1}(0|x^*)$ is at most single-valued.

The statistical problem has i.i.d. random elements $s_1, s_2, \dots$ of a measurable space $S$ and an integrand $f : U \times S \to \mathbb R^m$ on a compact neighborhood $U$ of $x^*$. It satisfies the probabilistic assumptions P.1–P.4: continuity in $x$, measurability in $s$, a finite second moment at one point, and a Lipschitz bound $|f(x_1,s) - f(x_2,s)| \le a(s)|x_1 - x_2|$ with $E a(s_1)^2 < \infty$. The M-estimate $x^\nu$ is a measurable solution of

$$0 \in \bar f^\nu(x) + N(x), \qquad \bar f^\nu(x) = \frac1\nu\sum_{i=1}^\nu f(x, s_i),$$

and the true equation is $0 \in Ef(x) + N(x)$ with $F = Ef + N$.

Formalization targets

Goal: Theorem 2.7 (asymptotic distribution of M-estimates)

Under P.1–P.4 on a compact neighborhood $U$ of $x^*$, B-differentiability of $Ef$ at $x^*$, and M.2–M.4 for $F = Ef + N$, every sequence of measurable solutions $x^\nu$ of (2.5) with $x^\nu \to x^*$ almost surely satisfies

$$\sqrt\nu\,[x^\nu - x^*] \xrightarrow{\ \mathcal D\ } DF^{-1}(0|x^*)(-w^*), \qquad w^* \sim \mathcal N\big(0, \operatorname{cov} f(x^*, s_1)\big).$$

The goal fixes the limit law completely: the map is the contingent derivative of $F^{-1}$, and the Gaussian has the covariance of the integrand at $x^*$.

Milestones

• Theorem 2.4 gives bounds in probability, $P\{|x^\nu - x^*| > \delta\} \le P\{\alpha\lambda\|z^\nu - z^*\| > \delta\}$. Its proof uses the upper-Lipschitz property $U \cap F^{-1}(y) \subseteq x^* + \lambda|y|B$ (a display of the proof).
• Theorem 2.6 is the abstract limit theorem: if $\tau_\nu^{-1}[z^\nu - z^*] \to_{\mathcal D} w$, then $\tau_\nu^{-1}[x^\nu - x^*] \to_{\mathcal D} DF^{-1}(0|x^*)(-D_z f(z^*,x^*)(w))$. Its proof uses two displays: semi-differentiability of the localized solution map, with $DJ(z^*|x^*)(w) = DF^{-1}(0|x^*)(-D_z f(z^*,x^*)(w))$, and a Lipschitz bound $|x - x^*| \le \lambda\|z - z^*\|$ on $U \cap J(z)$.
• Proposition A1, Corollary A2 and Theorem A3 concern the space $C_m(U)$ under P.1–P.4. The integrand and the empirical means are random elements of $C_m(U)$, and $\sqrt\nu(\bar f^\nu - Ef)$ converges in distribution to a Gaussian element of $C_m(U)$.

The three displays (Theorem 2.4's upper-Lipschitz inclusion, and Theorem 2.6's semi-differentiability and Lipschitz bound) are statements the paper cites from King and Rockafellar, Sensitivity analysis for nonsmooth generalized equations ([12]: Proposition 2.1, Theorem 4.1, Remark 4.3). They are cited results, not this paper's own, and are milestones because the proofs of Theorems 2.4 and 2.6 rest on them.

Significance

Theorem 2.7 gives the limit law of constrained and nonsmooth M-estimates in a form that can be computed. When $N$ is the normal cone of a polyhedron, $DF^{-1}(0|x^*)$ is piecewise linear, and the limit is the solution of a random linear complementarity or quadratic problem driven by a Gaussian vector. This underlies the asymptotic theory of sample-average approximation in stochastic programming, where the paper applies it to stochastic programs (§3) and to piecewise linear-quadratic tracking problems (§4). Theorem 2.6 separates the deterministic sensitivity analysis from the probability, so any data sequence with a known limit law yields a limit law for the solutions.

The result is proved in the paper modulo the cited theorems of [12] and [11], but none of it is machine-checked. Mathlib has the real-valued i.i.d. central limit theorem, Gaussian measures on Banach spaces and convergence in distribution. It has no multivariate or Banach-space central limit theorem, no contingent derivatives and no set-valued implicit function theorem. Formalizing the mission produces these, along with a checked version of the cited sensitivity results.

Difficulty

The classical argument linearizes $F$ at $x^*$, inverts the Jacobian and applies the delta method. Here $F$ is set-valued and its derivative is only positively homogeneous. There is no Jacobian to invert, and the solution map need not be differentiable or even single-valued away from $x^*$. The replacement for the implicit function theorem is the semi-differentiability of the localized solution map under M.1–M.4. Proving it means controlling both the upper and the lower set limits of difference quotients of solution sets, and subinvertibility is what supplies existence of nearby solutions.

The probabilistic side cannot work coordinate by coordinate either. The estimate solves an equation in the whole function $\bar f^\nu$, so convergence of $\bar f^\nu$ at finitely many points is not enough. The central limit theorem must hold in the sup norm on $C_m(U)$, which requires tightness of the empirical process, and only then can the deterministic sensitivity result be composed with it.

Formalization scope

Points live in EuclideanSpace ℝ (Fin n), and $Z$ is a real normed space with [CompleteSpace Z] [SeparableSpace Z] where the paper says "separable Banach". Set limits are Kuratowski limits along filters ($t \downarrow 0$ is 𝓝[>] 0, and $(t,w') \to (0^+,w)$ is the product filter). The contingent derivative is defined by (2.2) alone. M.4's printed sum formula equals it under M.1, and this is not assumed. "B-differentiable" is read as the limit (2.4). Products carry Lean's max norm. $s_1$ is s 0, empirical means sum over Finset.range ν, and (2.5) is required for $\nu \ge 1$. $F = Ef + N$ is empty off $U$. Convergence in distribution is Mathlib's TendstoInDistribution, with the limit on its own probability space. The law of $w^*$ is fixed through linear functionals: $\langle\ell, w^*\rangle \sim \mathcal N(0, \operatorname{Var}\langle\ell, f(x^*,s_1)\rangle)$. In Appendix A1–A3 the integrand is S → C(↥U, Rn m) with the Borel σ-algebra, and "Gaussian" is IsGaussian.

Explicit choices relative to the printed text:

1. The paper states that an almost surely convergent sequence of solutions "converges to the point $x^*$" (Theorems 2.6 and 2.7). This is false when the true equation has a second solution: $f(z,x) = x^2 - x - z$, $N \equiv \{0\}$, $z^* = x^* = 0$ satisfies M.1–M.4 with $J(0) = \{0, 1\}$. The formalization assumes $x^\nu \to x^*$ almost surely instead.
2. $0 \in F(x^*)$ (presupposed by $DF^{-1}(0|x^*)$) is explicit in Theorem 2.4 and the upper-Lipschitz display.
3. The threshold for "all sufficiently small $\delta$" in Theorem 2.4 is chosen with $U$ and $\lambda$, before the random elements.
4. Proposition A1 and Corollary A2 carry P.1–P.4, as stated or inherited on the Appendix page, though their measurability conclusions use only P.1.
5. In the limit theorems, the single-valued map $DF^{-1}(0|x^*)$ is a function $L$ whose values lie in the contingent derivative at every point.

The conclusion of the goal names its limit: the image of the stated Gaussian under a map $L$ whose values lie in the contingent derivative of $F^{-1}$. A statement asserting only that $\sqrt\nu(x^\nu - x^*)$ converges in distribution to some limit, or replacing $DF^{-1}(0|x^*)$ by a linear map, is a different and weaker theorem. A sorry-free check confirms that the goal's hypotheses can all be met (a degenerate instance with $f(x,s) = x$, $N \equiv \{0\}$).

A complete development needs Kuratowski set convergence and contingent derivatives (reusable across set-valued analysis), a central limit theorem in $C(K)$ for Lipschitz-indexed processes (reusable for empirical-process theory), and a continuous-mapping argument for random closed sets. Contributions to any of these layers are welcome, as are proofs of the cited [12] statements.

Selected references

• A. J. King and R. T. Rockafellar, Asymptotic theory for solutions in statistical estimation and stochastic programming, Mathematics of Operations Research 18(1) (1993). https://doi.org/10.1287/moor.18.1.148
• A. J. King and R. T. Rockafellar, Sensitivity analysis for nonsmooth generalized equations, Mathematical Programming 55 (1992) 193–212. https://doi.org/10.1007/BF01581199
• A. J. King, Generalized delta theorems for multivalued mappings and measurable selections, Mathematics of Operations Research 14(4) (1989) 720–736. https://doi.org/10.1287/moor.14.4.720
• J. Dupačová and R. J.-B. Wets, Asymptotic behavior of statistical estimators and of optimal solutions of stochastic optimization problems, Annals of Statistics 16(4) (1988) 1517–1549. https://doi.org/10.1214/aos/1176351052
• A. Shapiro, Asymptotic properties of statistical estimators in stochastic programming, Annals of Statistics 17(2) (1989) 841–858. https://doi.org/10.1214/aos/1176347146
• P. J. Huber, The behavior of maximum likelihood estimates under nonstandard conditions, Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1 (1967) 221–233. https://projecteuclid.org/euclid.bsmsp/1200512988
• A. Araujo and E. Giné, The Central Limit Theorem for Real and Banach Valued Random Variables, Wiley, 1980.

Motivation

A partially observed Markov decision process (POMDP) models a controller that cannot see the state of the system it controls. It sees only noisy observations, and so it acts on a belief: a probability vector over the hidden states. Machine maintenance, medical screening, quality control and search problems all have this form. The dynamic program of a POMDP lives on the simplex of beliefs, a continuum, so computing exact optimal policies is expensive even when the state, action and observation sets are small. Structural results reduce that cost. A value function that is monotone in the belief, or a policy known to dominate a cheap reference policy, shrinks the space a computation must search. Such results also explain the model: they say when one belief is "better" than another.

W. S. Lovejoy, Some Monotonicity Results for Partially Observed Markov Decision Processes (Operations Research 35(5):736–743, 1987), provides such results by ordering beliefs with the monotone likelihood ratio (MLR) order instead of first-order stochastic dominance.

Timeline. Smallwood and Sondik (1973) set out the finite POMDP and its piecewise-linear value functions. White (1979, 1980) obtained monotone policies and values for machine replacement, for single-stage problems, and for the completely observed and completely unobserved extremes, all under first-order stochastic dominance. Albright (1979) treated the two-state case, where the usual orders coincide. Whitt (1979, 1982) developed the likelihood-ratio orders and showed that they are preserved by Bayesian updating. Lovejoy (1987) combined these into general monotonicity results for finite POMDPs, and the MLR order has since become the standard tool for structural results in POMDPs.

Setting

Let $S=\{1,\dots,n\}$ (states) and $O=\{1,\dots,m\}$ (observations) carry their natural orders, and let $A$ be a finite, completely ordered action set. For a finite chain $X$, $\Pi(X)$ is the set of probability vectors on $X$. For $\pi,\pi'\in\Pi(X)$, $\pi\ge_s\pi'$ (first-order stochastic dominance) means $\sum_{i\ge q}\pi_i\ge\sum_{i\ge q}\pi'_i$ for every $q$. $\pi\ge_r\pi'$ (MLR order) means $\pi_i\pi'_{i'}\ge\pi_{i'}\pi'_i$ whenever $i\ge i'$. For matrices $f,g$ on $X\times Y$, $f\ge_{tp}g$ means $f(x\vee x',y\vee y')\,g(x\wedge x',y\wedge y')\ge f(x,y)\,g(x',y')$ for all pairs, and $f$ is TP₂ if $f\ge_{tp}f$.

In each period the decision maker in state $s_t=i$ chooses $a\in A$ and receives the reward $g(i,a)$. The state moves to $j$ with probability $p^a_{ij}$ (matrix $P^a$), and an observation $k$ arrives with probability $r^a_{jk}$ (matrix $R^a$, with row $r^a(j)\in\Pi(O)$), generated by the new state $j$ and the action $a$. The paper assumes $r^a_{jk}>0$ throughout. The discount factor is $\beta\ge 0$. From a belief $\pi$, the observation $k$ has probability $\sigma(k;\pi,a)=\sum_{i,j}\pi_i p^a_{ij}r^a_{jk}$, and the posterior is the Bayes update $T_j(\pi,a,k)=\sum_i\pi_ip^a_{ij}r^a_{jk}/\sigma(k;\pi,a)$. With

$$h(\pi,a,V)=\sum_{i}\pi_i g(i,a)+\beta\sum_{k}\sigma(k;\pi,a)\,V(T(\pi,a,k)),$$

a finite horizon $N$ with salvage value $g_s$ gives the optimal values $V^*_{N+1}(\pi)=\sum_i\pi_ig_s(i)$ and $V^*_t(\pi)=\max_a h(\pi,a,V^*_{t+1})$. For $N=\infty$ and $0<\beta<1$, $V^*$ is the bounded solution of $V^*(\pi)=\max_a h(\pi,a,V^*)$. The myopic actions are $\alpha(\pi)=\operatorname{argmax}_a\sum_i\pi_ig(i,a)$.

Formalization targets

Goal: Proposition 2 (myopic lower bound)

Under (a) $g_s$ nondecreasing, (b) $g(\cdot,a)$ nondecreasing, (c) $P^a\ge_{tp}P^{a'}$ for $a\ge a'$, (d) $r^a(j)\ge_r r^a(j')$ for $j\ge j'$, (e) $r^a(j)\ge_s r^{a'}(j)$ for $a\ge a'$, and (f) $r^a_{jk}r^{a'}_{j'k}\ge r^{a'}_{jk}r^a_{j'k}$ for $a\ge a'$, $j\ge j'$: for every $t\le N$ (finite horizon), or for the infinite horizon with $0<\beta<1$, and every $\pi\in\Pi(S)$,

$$\forall\,\delta^*(\pi)\ \exists\,\alpha(\pi)\le\delta^*(\pi),\qquad \forall\,\alpha(\pi)\ \exists\,\delta^*(\pi)\ge\alpha(\pi),$$

where $\delta^*(\pi)$ ranges over the maximizers of $a\mapsto h(\pi,a,V^*_{t+1})$ (resp. $h(\pi,a,V^*)$).

Milestone: Proposition 1 (MLR-monotone values)

Under (a)–(d) with every $P^a$ TP₂: $\pi\ge_r\pi'$ in $\Pi(S)$ implies $V^*_t(\pi)\ge V^*_t(\pi')$ for $t=1,\dots,N+1$, and, without (a), $V^*(\pi)\ge V^*(\pi')$ for $N=\infty$.

Supporting milestones

The ordering facts behind both propositions: MLR implies stochastic dominance (§1), Lemma 1.1 (characterization of $\ge_s$), Lemma 1.3 (TP₂ prediction preserves $\ge_r$), Lemma 1.2 (the Bayes update is MLR-monotone in the observation, the prior and the action), the stochastic monotonicity of $\sigma$ in the belief (proof of Proposition 1) and in the action (Lemma 2.3), the comparison of $h$-increments with myopic increments (proof of Proposition 2), and Lemma 2.2 (dominated increments order maximizer sets).

Significance

The result. Proposition 2 makes the myopic policy, which solves a one-stage problem, a lower bound on an optimal policy for every belief and every period. In a search over policies, actions below $\alpha(\pi)$ can be discarded. When $g$ also has isotone differences, $\alpha$ is nondecreasing, and the optimal policy is bounded below by a monotone function that is easy to compute. Proposition 1 gives MLR-monotone value functions, the input to many later structural results for POMDPs. Lemma 1.2 records the fact behind it: Bayesian updating respects the MLR order, while first-order stochastic dominance does not survive conditioning.

Formalizing it. These results are proved on paper. This mission produces machine-checked proofs, together with a reusable finite-POMDP layer (belief update, observation probabilities, Bellman operator, finite- and infinite-horizon values) and a library of the stochastic orders on finite chains. One statement in the paper is wrong: the printed "only if" direction of Lemma 1.2(1) is false. The mission states only the direction that is true and used.

Difficulty

The obvious induction on $t$ for Proposition 1 needs $k\mapsto V(T(\pi,a,k))$ to be nondecreasing and $\sigma(\pi,a)$ to increase with $\pi$. Both need a belief order that conditioning preserves. Under first-order stochastic dominance the posterior is not monotone in the prior, and the paper's counterexample (p. 740) shows that the induction then fails. The MLR order repairs this, but proving that the prediction step preserves it (Lemma 1.3) requires a total-positivity composition argument (Karlin–Rinott, Theorem 2.4) on product lattices. For Proposition 2 the difficulty is to compare continuation values across actions: the observation distribution and the posterior both change with the action, and two separate orderings (Lemma 2.3 and Lemma 1.2(3)) must be combined before the maximizer comparison applies. The infinite-horizon parts additionally need the Bellman fixed point characterized well enough to pass monotonicity to the limit.

Formalization scope

Everything is finite, so all probabilities and expectations are finite sums and no measure theory is involved. States, observations and actions are finite nonempty types with a LinearOrder (any finite chain is isomorphic to $\{1,\dots,n\}$). $\Pi(X)$ is Mathlib's stdSimplex ℝ X. The orders $\ge_s,\ge_r,\ge_{tp}$ are plain relations (StochGE, MLRGE, TPGE) with the larger argument first, and every statement assumes simplex membership explicitly. The standing assumptions (stochastic rows of $P^a$ and $R^a$, $r^a_{jk}>0$, $\beta\ge0$) are fields of the structure POMDP. $V^*_t$ is computed by recursion (3) counted in steps to go, Vstar gs N t = valueToGo gs (N+1-t). The infinite-horizon $V^*$ is any function bounded on $\Pi(S)$ that solves the Bellman equation there. For $0<\beta<1$ such a function exists and is unique on $\Pi(S)$, by contraction. The equivalence between recursion (3) and the optimum over history-dependent strategies is cited by the paper from the literature and is not part of this mission. Maximizer sets (argmaxSet) carry the "for all $\delta^*$ / there exists $\alpha$" quantifiers. Both halves of each part of Proposition 2 are $\forall\exists$ statements.

The goal is not to be read with $V^*_{t+1}$ or $V^*$ replaced by an arbitrary, or an arbitrary nondecreasing, value function. That reading would reduce Proposition 2 to Lemma 2.2 plus a hypothesis. The goal quantifies only over the value functions of recursion (3) and over bounded Bellman solutions.

A complete development needs finite total-positivity composition (Mathlib's four functions theorem is the natural starting point), Abel summation for Lemma 1.1, and a contraction argument for the infinite horizon. The order library and the finite POMDP layer are reusable beyond this paper. Proofs of any milestone are welcome, as are alternative arguments for Lemma 1.3.

Selected references

• W. S. Lovejoy, Some Monotonicity Results for Partially Observed Markov Decision Processes, Operations Research 35(5):736–743, 1987. https://doi.org/10.1287/opre.35.5.736
• R. D. Smallwood and E. J. Sondik, The Optimal Control of Partially Observable Markov Processes over a Finite Horizon, Operations Research 21(5):1071–1088, 1973. https://doi.org/10.1287/opre.21.5.1071
• W. Whitt, A Note on the Influence of the Sample on the Posterior Distribution, Journal of the American Statistical Association 74:424–426, 1979.
• W. Whitt, Multivariate Monotone Likelihood Ratio and Uniform Conditional Stochastic Order, Journal of Applied Probability 19:695–701, 1982.
• S. Karlin and Y. Rinott, Classes of Orderings of Measures and Related Correlation Inequalities. I. Multivariate Totally Positive Distributions, Journal of Multivariate Analysis 10(4):467–498, 1980. https://doi.org/10.1016/0047-259X(80)90065-2
• C. White, Optimal Control-limit Strategies for a Partially Observed Replacement Problem, International Journal of Systems Science 10:321–331, 1979 (the machine-replacement model of §5).
• S. C. Albright, Structural Results for Partially Observable Markov Decision Processes, Operations Research 27(5):1041–1053, 1979. https://doi.org/10.1287/opre.27.5.1041

Motivation

Labor markets match workers to firms, and the terms of each match (the salary) are negotiated along with the match itself. A firm's output depends on the whole team it hires, so a firm cares about sets of workers, not individual workers one at a time. Kelso and Crawford (1982) asked when such a market has a stable outcome, the core, in which no firm and group of workers can agree on terms that all of them prefer, and when a simple decentralized auction finds one.

Their answer is the gross-substitutes condition: raising some workers' salaries never makes a firm withdraw an offer from a worker whose salary has not risen. Under it, an ascending process in which firms make offers and workers reject all but their favorite reaches a core allocation. This condition became the standard hypothesis for the existence of Walrasian equilibrium with indivisible goods (Gul and Stacchetti 1999), it is the hypothesis behind matching with contracts (Hatfield and Milgrom 2005), and the process is the ancestor of ascending auction designs.

Timeline.

• 1962: Gale and Shapley, deferred acceptance for one-to-one and many-to-one matching without money.
• 1971: Shapley and Shubik, the assignment game: one-to-one matching with transferable utility; the core is nonempty and is the set of solutions of a dual linear program.
• 1981: Crawford and Knoer, a salary-adjustment process for one-to-one matching with money, converging to the core.
• 1982: Kelso and Crawford, many-to-one matching with money and production complementarities; existence of the core under gross substitutes via the salary-adjustment process (Theorem 1, the target of this mission).

Setting

There are finitely many workers $i \in W$ and firms $j \in F$, with at least one firm. Worker $i$'s utility of working for firm $j$ at salary $s$ is $u^i(j; s)$, strictly increasing and continuous in $s$. Firm $j$'s gross product from hiring the set $C \subseteq W$ is $y^j(C)$, and its profit at the salary vector $s^j = (s_{1j},\dots,s_{mj})$ is

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

$M^j(s^j)$ is the set of profit-maximizing $C$. Each pair has a starting salary $\sigma_{ij}$. The assumptions (p. 1486) are (MP) $y^j(C \cup \{i\}) - y^j(C) - \sigma_{ij} \ge 0$ for $i \notin C$; (NFL) $y^j(\emptyset) = 0$; and (GS): if $C \in M^j(s^j)$ and $\tilde s^j \ge s^j$, some $\tilde C \in M^j(\tilde s^j)$ contains $\{i \in C : \tilde s_{ij} = s_{ij}\}$.

In the discrete market with unit $\delta > 0$, firm $j$ may pay worker $i$ only $\sigma_{ij} + k\delta$, $k = 0, 1, 2, \dots$. An allocation sends each worker $i$ to a firm $f(i)$ at a salary $s_{if(i)}$; it is individually rational (D1) if $s_{if(i)} \ge \sigma_{if(i)}$ and every firm's profit is nonnegative. It is a (discrete) core allocation (D3) if it is individually rational, pays permitted salaries, and no firm $j$, set $C$ and permitted salaries $r^j$ satisfy $u^i(j; r_{ij}) > u^i(f(i); s_{if(i)})$ for all $i \in C$ and $\pi^j(C; r^j) > \pi^j(C^j; s^j)$.

The salary-adjustment process (pp. 1488–1489), verbatim:

R1. Firms begin facing a set of permitted salaries $s_{ij}(0) = \sigma_{ij}$. Permitted salaries at round $t$, $s_{ij}(t)$, remain constant, except as noted below. In round zero, each firm makes offers to all workers; this is costless by (MP).

R2. On each round, each firm makes offers to the members of one of its favorite sets of workers, given the schedule of permitted salaries $s^j(t) \equiv [s_{1j}(t), \dots, s_{mj}(t)]$. That is, firm $j$ makes offers to the members of $C^j[s^j(t)]$, where $C^j[s^j(t)]$ maximizes $\pi^j[C; s^j(t)]$. Firms may break ties between sets of workers however they like, with the following exception: Any offer made by firm $j$ in round $t - 1$ that was not rejected must be repeated in round $t$. By (GS), the firm sacrifices no profits in doing this, since (by R4) other workers' permitted salaries cannot have fallen, and the salary of a worker who did not reject an offer remains constant.

R3. Each worker who receives one or more offers rejects all but his or her favorite (taking salaries into account), which he or she tentatively accepts. Workers may break ties at any time however they like.

R4. Offers not rejected in previous periods remain in force. If worker $i$ rejected an offer from firm $j$ in round $t - 1$, $s_{ij}(t) = s_{ij}(t - 1) + 1$; otherwise $s_{ij}(t) = s_{ij}(t - 1)$. Firms continue to make offers to their favorite sets of workers, taking into account their permitted salaries.

R5. The process stops when no rejections are issued in some period. Workers then accept the offers that remain in force from the firms they have not rejected.

Formalization targets

Goal: Theorem 1 (p. 1489)

"The salary-adjustment process R1–R5 converges in finite time to a discrete core allocation in the discrete market for which it is defined." Formally, under the assumptions above:

$$\Big(\exists \text{ a run}\Big)\ \wedge\ \forall \rho \text{ run}:\ \Big(\exists T:\ \rho \text{ issues no rejections in round } T\Big)\ \wedge\ \Big(\forall T \text{ such rounds},\ \text{outcome}_\rho(T) \text{ is a discrete core allocation}\Big).$$

Milestones, in the paper's order

1. R2 is well defined: a run exists (each firm has a favorite set containing its unrejected offers).
2. Lemma 1: every worker has at least one offer in every period.
3. Lemma 2: after finitely many rounds every worker has exactly one offer and the process stops.
4. Lemma 3: the allocation at a stopping round is individually rational.
5. Lemma 4: the allocation at a stopping round is a discrete core allocation.

Significance

Theorem 1 gives the existence of a core allocation in every discrete market satisfying (MP), (NFL) and (GS), with no convexity of production and arbitrary complementarity within the limits of (GS). It is the step from which the paper derives the existence of a strict core allocation of the continuous market (Theorem 2, by letting the unit shrink), and with additional no-ties assumptions the firm-optimality of the process's outcome (Theorem 4) and the comparative statics of entry and exit (Theorem 5).

The result is proved in the paper and has been reproved in more general settings; it has no machine-checked proof known to us. Nothing of this paper was on Prove2Me before this series. Related platform work, credited but not reused: the Gale–Shapley deferred-acceptance development (GS62CollegeAdmissions.*, proved), the no-money ancestor of this process; and the Shapley–Shubik assignment game (AssignmentGame.CoreLP), whose core the process approximates when production is additively separable. Neither states anything about this process. This mission is mission 1 of a series of seven on the paper: 2 (strict core of the continuous market), 3 (one-sided coalition formation), 4 (firm-optimality), 5 (comparative statics), 6 (gross substitutes and decreasing returns), 7 (a market without a core). Each states its own model.

Difficulty

The process is quantified over all tie-breakings, so no single computation settles it; the statements are about every sequence of rounds consistent with R1–R5. Two points carry the content. First, R2 imposes a constraint that may not be satisfiable: a firm must repeat its unrejected offers and choose a profit-maximizing set. Without (GS) no such set need exist and the process is not defined. Second, the core property at the stopping round compares the outcome with coalitions using salaries the process never reached; the comparison is with salaries on the discrete grid only, and it is false if coalitions may use salaries below $\sigma_{ij}$ or off the grid. Termination is not automatic either: the process may continue after a round without rejections, salaries are real numbers, and no bound on the number of rounds is given.

Formalization scope

Lean representation, in namespace KelsoCrawford.Process:

• Market W F carries u, y, σ; workers and firms are finite types, with [Nonempty F] (the paper's $n \ge 1$; with no firms and some worker no run exists).
• Allocation assigns every worker to a firm (no unemployment, as in the paper's $f$).
• (GS) is GrossSubstitutesOn (M.y j) (M.gridVectors δ j) for each firm: the discrete (GS), since the paper notes that a discrete market may satisfy (GS) while its continuous version does not.
• The core is D3 with permitted salaries M.grid δ $= \{\sigma_{ij} + k\delta : k \in \mathbb N\}$.
• A Run records salaries, offers and tentative choices per round; IsRun is R1–R4, Stopped is R5's "no rejections", outcome is R5's allocation.

Explicit readings of the paper's phrases:

• "converges in finite time" = every run has a round without rejections; no bound on that round is claimed;
• "to a discrete core allocation" = at every round without rejections, the allocation read off is in the discrete core;
• the unit $1$ of R4 is a parameter $\delta > 0$ (same theorem in rescaled units);
• $\sigma_{ij}$ is data; its defining relation $u^i(j;\sigma_{ij}) = u^i(0;0)$ is not assumed (a more general statement).

The existence of a run is part of the goal: without it, statements about all runs would be vacuous. Fixing a tie-breaking rule would turn the statements into claims about a single run and is ruled out; so are the strict core D2 (false here because of ties at the grid) and an integer grid below $\sigma_{ij}$ (false for improving coalitions). Proofs of the milestones and reusable infrastructure for ascending processes 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/1913320
• D. Gale and L. S. Shapley, College admissions and the stability of marriage, American Mathematical Monthly 69(1), 1962, 9–15. https://doi.org/10.2307/2312726
• 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

Motivation

For problems with inequality constraints only, F. John (1948) showed that every minimizer admits nonnegative multipliers $(\bar u_0, \bar u_1, \dots, \bar u_m) \ne 0$, one of which belongs to the objective. The Kuhn–Tucker conditions (1951) are the stronger statement in which the objective's multiplier can be taken equal to one; they need a constraint qualification.

Problems arising in practice mix equalities and inequalities. Fritz John's theorem does not cover them, and the obvious reduction, writing each equality $h_j(x) = 0$ as the two inequalities $h_j(x) \le 0$ and $-h_j(x) \le 0$, destroys the content of the conditions: every feasible point then satisfies them with $\bar u_0 = 0$. O. L. Mangasarian and S. Fromovitz (1967) proved a version of Fritz John's conditions that treats equalities directly and stays informative, and from it derived the constraint qualification now known as the Mangasarian–Fromovitz constraint qualification (MFCQ). MFCQ is the standard regularity assumption in the convergence theory of sequential quadratic programming, interior-point and augmented-Lagrangian methods, and in the stability theory of parametric programs.

Timeline.

• 1939, W. Karush (master's thesis) and 1951, H. W. Kuhn and A. W. Tucker: multiplier conditions with $\bar u_0 = 1$ for inequality constraints, under a constraint qualification.
• 1948, F. John: the multiplier rule with $\bar u_0 \ge 0$ for inequality constraints, no qualification needed.
• 1967, Mangasarian and Fromovitz (this paper): the multiplier rule for equalities and inequalities together, and the qualification (3.4)–(3.6).

Setting

Let $E^n$ be $n$-dimensional Euclidean space, and let $\theta, g_1, \dots, g_m, h_1, \dots, h_k : E^n \to \mathbb R$ be functions with continuous first partial derivatives on $E^n$. The program is

$$\text{minimize } \theta(x) \quad \text{subject to} \quad g_i(x) \le 0,\ i \in M = \{1,\dots,m\}, \qquad h_j(x) = 0,\ j \in K = \{1,\dots,k\}. \tag{1.1}$$

The feasible set is $S = \{x \in E^n : g_i(x) \le 0,\ i \in M,\ h_j(x) = 0,\ j \in K\}$. A point $\bar x$ is a solution of (1.1) if $\bar x \in S$ and $\theta(\bar x) \le \theta(x)$ for all $x \in S$. The active set at $\bar x$ is $\bar M = \{i \in M : g_i(\bar x) = 0\}$. The gradient of $f$ at $\bar x$ is $\nabla f(\bar x)$, and $y'z$ denotes the inner product.

The generalized Fritz John conditions hold at $\bar x$ if there are $\bar u = (\bar u_0, \bar u_1, \dots, \bar u_m)$ and $\bar v = (\bar v_1, \dots, \bar v_k)$ with

$$\bar u_0 \nabla\theta(\bar x) + \sum_{i=1}^m \bar u_i \nabla g_i(\bar x) + \sum_{j=1}^k \bar v_j \nabla h_j(\bar x) = 0, \qquad \sum_{i=1}^m \bar u_i g_i(\bar x) = 0, \qquad \bar u \ge 0, \qquad (\bar u, \bar v) \ne 0 .$$

The Kuhn–Tucker conditions are the same system with $\bar u_0 = 1$ and no nontriviality requirement.

Formalization targets

Goal: the generalized Fritz John necessary conditions (p. 41)

If $\bar x$ is a solution of (1.1), then there exist $\bar u \in E^{m+1}$ and $\bar v \in E^k$ with

$$\bar u_0 \nabla\theta(\bar x) + \sum_{i=1}^m \bar u_i \nabla g_i(\bar x) + \sum_{j=1}^k \bar v_j \nabla h_j(\bar x) = 0, \quad \sum_{i=1}^m \bar u_i g_i(\bar x) = 0, \quad \bar u \ge 0, \quad (\bar u, \bar v) \ne 0. \tag{2.9–2.12}$$

No regularity of the constraints is assumed. The nontriviality requirement covers $\bar u_0$, the $\bar u_i$ and the $\bar v_j$ together.

Milestones

1. Motzkin's transposition theorem (p. 39): for real matrices $A, B, C$ with $A$ nonempty, exactly one of $y'A < 0,\ y'B \le 0,\ y'C = 0$ and $Az_1 + Bz_2 + Cz_3 = 0,\ z_1 \ge 0,\ z_1 \ne 0,\ z_2 \ge 0$ is solvable.
2. Lemma 1 (pp. 39–40): if $f_i(\bar x) = 0$, $h_j(\bar x) = 0$ at some $\bar x$ in an open set $D$, no $x \in D$ has $f_i(x) < 0$ for all $i$ and $h_j(x) = 0$ for all $j$, and the $\nabla h_j(\bar x)$ are linearly independent, then no $y$ has $y'\nabla f_i(\bar x) < 0$ and $y'\nabla h_j(\bar x) = 0$.
3. Lemma 2 (p. 40): under the same assumptions, without independence, there are $\bar r \ge 0$ and $\bar s$, not both zero, with $\sum \bar r_i \nabla f_i(\bar x) + \sum \bar s_j \nabla h_j(\bar x) = 0$.
4. $D$ is open (p. 41): $D = \{x : g_i(x) < 0,\ i \in M \setminus \bar M\}$ is open.
5. The reduction (pp. 41–42): at a solution $\bar x$ of (1.1), $\bar x \in D$ and the system $\theta(x) - \theta(\bar x) < 0$, $g_i(x) < 0$ ($i \in \bar M$), $h_j(x) = 0$ has no solution in $D$.

Companion results

• Corollary (p. 43): the generalized Fritz John conditions hold at any feasible point satisfying (2.27) or (2.28).
• The generalized constraint qualification (pp. 43–44): at a solution, $\bar y'\nabla g_i(\bar x) < 0$ ($i \in \bar M$), $\bar y'\nabla h_j(\bar x) = 0$ and independent $\nabla h_j(\bar x)$ imply the Kuhn–Tucker conditions.
• The splitting remark (p. 38): after splitting equalities, every feasible point satisfies Fritz John's original conditions.

Significance

The theorem is a multiplier rule for smooth programs with both kinds of constraints and no assumption on the constraints. It has two direct consequences in the paper. First, it yields MFCQ, the condition (3.4)–(3.6) under which the Kuhn–Tucker conditions hold at every solution. MFCQ is weaker than linear independence of all active gradients (LICQ), and it is equivalent to boundedness of the Kuhn–Tucker multiplier set (Gauvin, 1977). Second, the corollary identifies feasible non-minimizers at which the conditions hold anyway.

The result is classical and its proof is in every nonlinear-programming textbook. Mathlib has the equality-constrained Lagrange multiplier rule for a local extremum (IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt) and the implicit function theorem, and Prove2Me has a formalized Fritz John theorem for inequality constraints only. To our knowledge no machine-checked proof of the mixed equality–inequality Fritz John rule, of MFCQ, or of Motzkin's transposition theorem in this form exists. The formalization would provide the standard multiplier rule and qualification on which a formal theory of nonlinear programming builds.

Difficulty

With inequalities alone, John's theorem follows from the observation that if $\bar x$ is a minimizer, no direction $y$ strictly decreases $\theta$ and every active $g_i$ to first order; Motzkin's (or Gordan's) theorem then produces the multipliers. With equalities the first step fails: a direction with $y'\nabla h_j(\bar x) = 0$ is tangent to the equality manifold but generally leaves it, so a first-order descent direction does not yield a feasible point with smaller objective. Lemma 1 is precisely the claim that it does when the $\nabla h_j(\bar x)$ are independent, and it needs a curve inside $\{h = 0\}$ along which the strict inequalities persist: the implicit function theorem, applied on an open set, with care that the curve stays in $D$. The linearly dependent case must be handled separately, and it is the only place the multipliers $\bar v$ can be nonzero with $\bar u = 0$.

Formalization scope

$E^n$ is EuclideanSpace ℝ (Fin n), the inner product $y'z$ is inner ℝ y z, and $\nabla f(\bar x)$ is Mathlib's gradient f xbar. "Continuous first partial derivatives on $E^n$", the standing assumption of §1, is ContDiff ℝ 1 (equivalent in finite dimension) and is a hypothesis of the goal, the corollary and the constraint qualification; Lemma 1 and Lemma 2 use ContDiffOn ℝ 1 · D on an open set $D$, as on the page. Indices $i \in M$ and $j \in K$ are Fin m and Fin k, 0-based; $m = 0$ and $k = 0$ are allowed. The multiplier vector $\bar u \in E^{m+1}$ is split into u0 : ℝ and u : Fin m → ℝ, and $(\bar u, \bar v) \ne 0$ is "u0 ≠ 0, or some u i ≠ 0, or some v j ≠ 0". A solution of (1.1) is a global minimizer over $S$, as the proof on p. 42 uses. In Motzkin's theorem a matrix is the family of its columns, and "either … or …, but never both" is Xor. In Lemma 2, "the assumptions of Lemma 1" exclude the proviso (2.5) of linear independence, which the proof of Lemma 2 treats separately.

The goal does not assume linear independence of the $\nabla h_j(\bar x)$, does not mention $D$ or Lemma 1, and requires $(\bar u, \bar v) \ne 0$ with $\bar u_0$ included; a formalization that drops $\bar u_0$ from the nontriviality condition is false at $m = k = 0$, and one that requires $\bar u_0 \ne 0$ is the Kuhn–Tucker statement, false without a qualification.

A complete development needs Motzkin's (or Gordan's) theorem of the alternative, which is reusable well beyond this mission, and the implicit function theorem on open sets in Euclidean space with a $C^1$ curve argument. Proofs of any milestone are welcome, as is a proof of the goal by another route.

Selected references

• O. L. Mangasarian and S. Fromovitz, The Fritz John necessary optimality conditions in the presence of equality and inequality constraints, J. Math. Anal. Appl. 17 (1967), 37–47. https://doi.org/10.1016/0022-247X(67)90163-1
• F. John, Extremum problems with inequalities as subsidiary conditions, in Studies and Essays Presented to R. Courant on his 60th Birthday, Interscience, New York, 1948, 187–204.
• H. W. Kuhn and A. W. Tucker, Nonlinear programming, Proc. Second Berkeley Symposium on Mathematical Statistics and Probability, University of California Press, 1951, 481–492.
• J. Gauvin, A necessary and sufficient regularity condition to have bounded multipliers in nonconvex programming, Math. Programming 12 (1977), 136–138. https://doi.org/10.1007/BF01593777
• O. L. Mangasarian, Nonlinear Programming, McGraw-Hill, 1969; reprinted SIAM Classics in Applied Mathematics 10, 1994. https://doi.org/10.1137/1.9781611971255