The OR Formalization Drive

Motivation

The newsvendor problem is the basic single-period inventory model: a decision maker orders $q$ units before a random demand $D$ is observed, pays $b>0$ per unit of unmet demand and $h>0$ per unit left over, and minimizes the expected cost $C(q)=E[b(D-q)^+ + h(q-D)^+]$. When the distribution of $D$ is known, the optimal order is the $b/(b+h)$ quantile of $D$. In practice the distribution is unknown and only a sample of past demands is available; the standard data-driven order is the sample average approximation (SAA), the $b/(b+h)$ quantile of the empirical distribution.

R. Levi, G. Perakis and J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights (Operations Research 63(6), 2015), ask how many samples guarantee that the SAA order is $\epsilon$-optimal with high probability. Levi, Roundy and Shmoys (2007) gave a distribution-free bound. Levi, Perakis and Uichanco show that, asymptotically in $\epsilon$, the right measure of difficulty is a single scalar of the demand law, the weighted mean spread at the critical quantile, and that for the class of log-concave demand distributions (normal, uniform, exponential, logistic, Laplace and many others used in inventory theory) this scalar is bounded below by $\min(b,h)/(b+h)$. That uniform bound turns a distribution-dependent sample-size guarantee into one that holds for every log-concave demand, and is markedly tighter than the distribution-free one.

This mission formalizes the bound (Proposition 2) and the chain of lemmas the paper uses to prove it. The source is the authors' accepted manuscript of the paper (MIT DSpace), cited by its own page numbers.

Setting

Fix costs $b>0$, $h>0$ and the critical ratio $\beta=b/(b+h)\in(0,1)$. A demand law is given by a probability density $f:\mathbb R\to\mathbb R$: measurable, nonnegative, with $\int f=1$. Its cdf is $F(t)=\int_{(-\infty,t]}f$, and its $\beta$ quantile is

$$q^*=\inf\{q : F(q)\ge \beta\}.$$

The absolute mean spread (AMS, Definition 1) at $t$ is the gap between the conditional means above and below $t$,

$$\Delta(t)=E(D\mid D\ge t)-E(D\mid D\le t)=\frac{\int_{[t,\infty)}x f(x)\,dx}{1-F(t)}-\frac{\int_{(-\infty,t]}x f(x)\,dx}{F(t)},$$

and the weighted mean spread (WMS, Definition 2) is $\Delta(q^*)f(q^*)$.

A density is log-concave (Definition 3) if $\log f$ is concave on its support. Equivalently, $f(x)^a f(y)^{1-a}\le f(ax+(1-a)y)$ for all $x,y$ and $a\in[0,1]$; this form allows $f$ to vanish outside an interval.

For a log-concave $f$ and a point $t$ with $f(t)>0$, the number $\gamma_1$ is a supergradient of $\log f$ at $t$, written $\gamma_1\in\partial\log f(t)$, if $\log f(x)\le\log f(t)+\gamma_1(x-t)$ for all $x$ with $f(x)>0$. The paper splits the class $\mathbb L$ of log-concave densities into the subclasses $\mathbb L_{q^*,\gamma_0,\gamma_1}$ of densities with quantile $q^*$, $f(q^*)=\gamma_0$ and $\gamma_1\in\partial\log f(q^*)$, and minimizes the AMS over each subclass (problem (11)). The minimizer is the truncated exponential density

$$\tilde f(x)=\gamma_0e^{\gamma_1(x-q^*)}\ \text{ on }[\underline x,\overline x],\qquad \underline x=q^*+\tfrac1{\gamma_1}\log\!\big(1-\tfrac{\gamma_1}{\gamma_0}\beta\big),\quad \overline x=q^*+\tfrac1{\gamma_1}\log\!\big(1+\tfrac{\gamma_1}{\gamma_0}(1-\beta)\big),$$

and zero elsewhere (display (12)), with AMS $z^*_{q^*,\gamma_0,\gamma_1}$ in closed form.

The Lean development uses the names IsPdf, cdfOf, quantileOf, ams, IsLogSupergradient, tildeF and zStar for these objects, in the namespace DataDrivenNV.WMS.

Formalization targets

Goal: Proposition 2

For every log-concave density $f$,

$$\Delta(q^*)\,f(q^*)\ \ge\ \frac{\min(b,h)}{b+h}.$$

The statement has no further hypothesis: no moment condition, no continuity, no restriction on $\gamma_0,\gamma_1$.

Milestones, in the order of the paper's proof

1. Lemma 1: at the quantile, $-\frac{b+h}{h}\le\frac{\gamma_1}{\gamma_0}\le\frac{b+h}{b}$.
2. Lemma 2: $f(x)\le\gamma_0e^{\gamma_1(x-t)}$ for every $x$.
3. Lemma 3 (Domination Lemma): a density dominated on the support of another, with the same mass left of $t$, has the larger AMS at $t$.
4. Proposition 1: $\tilde f$ belongs to $\mathbb L_{q,\gamma_0,\gamma_1}$ and minimizes the AMS there.
5. The closed form: $\Delta_{\tilde f}(q)=z^*_{q,\gamma_0,\gamma_1}=\frac{\gamma_0}{\gamma_1^2}\big[(\frac{b+h}{h}+\frac{\gamma_1}{\gamma_0})\log(1+\frac{\gamma_1}{\gamma_0}\frac{h}{b+h})+(\frac{b+h}{b}-\frac{\gamma_1}{\gamma_0})\log(1-\frac{\gamma_1}{\gamma_0}\frac{b}{b+h})\big]$.
6. Lemma 4: three elementary inequalities in $\beta\in(0,1)$ and $\eta\in(-\frac1{1-\beta},\frac1\beta)$.

Significance

The proposition is what makes the paper's log-concave sample-size bound (Theorem 4) parameter-free: the probability that the biased SAA order is $\epsilon$-optimal is, asymptotically, at least $1-2\exp(-\frac14N\epsilon\,\Delta(q^*)f(q^*))$ (Theorem 3), and Proposition 2 replaces the unknown $\Delta(q^*)f(q^*)$ by $\min(b,h)/(b+h)$. A manager who only knows that demand is log-concave can then size a sample without estimating any parameter of the law.

The result is proved in the paper; nothing about it is open. As far as is known it has no machine-checked proof. Formalizing it produces a checked lower bound for an inventory-theory quantity together with reusable facts about log-concave densities on the line: exponential envelopes from a supergradient, the quantile-and-slope constraints of Lemma 1, and the comparison of conditional means behind the Domination Lemma.

Difficulty

The definitions are elementary, but the proof passes through an infinite-dimensional optimization problem over a class of densities. The obvious first step, "the AMS is minimized by the most concentrated density", has no direct meaning without fixing the density value and the slope of $\log f$ at the quantile; after fixing them, one needs the envelope of Lemma 2, a stochastic comparison (Lemma 3) and an explicit integral of a truncated exponential. The Domination Lemma as printed is false (a density whose support has a gap to the right of $t$ is a counterexample), so it is formalized under the hypothesis that the dominating density is positive exactly on an interval around $t$, which is how Proposition 1 uses it. The case $\gamma_1=0$ (uniform minimizer) and the two boundary values of $\gamma_1/\gamma_0$ (one-sided exponential minimizers) are not covered by the closed form (12) and must be handled separately in a proof of the goal. Finally, Lemma 1 rests on the monotonicity of the failure rate $f/(1-F)$ and the reversed hazard rate $f/F$ of log-concave laws, which must be proved from log-concavity.

Formalization scope

Densities are functions ℝ → ℝ with IsPdf f (measurable, nonnegative everywhere, integrable, total integral 1); the law of $D$ is never introduced separately. Log-concavity is the published definition ConvexOptimization.LogConcaveOn Set.univ f (power form, zeros allowed). Concavity of Real.log ∘ f is not used, because Real.log 0 = 0 would treat $\log f$ as $0$ off the support. The quantile is an sInf; for $\beta\in(0,1)$ its defining set is nonempty and bounded below. The AMS is the difference of two ratios of integrals. At the quantile both denominators are positive, and the goal and Proposition 1 assume no integrability of $xf(x)$, since log-concave densities have exponential tails. The value $f(q^*)$ is taken pointwise; $q^*$ lies in the interior of the support, where a log-concave density is continuous.

Conventions and disclosed departures from the page:

• "$\gamma_1\in\partial\log f$, the set of all subgradients" is read as the superdifferential of the concave $\log f$ on $\{f>0\}$.
• Lemma 3 carries three added hypotheses: $f_2$ vanishes outside some $[l,u]\ni t$ and is positive on $(l,u)$; $0<F_1(t)<1$; and $xf_1(x)$, $xf_2(x)$ are integrable. The first repairs the printed statement; the other two are the conditions under which Definition 1 makes sense for general densities.
• Proposition 1 and the closed form of $z^*$ are stated for $\gamma_1\neq0$ and $\gamma_1/\gamma_0$ strictly inside the interval of Lemma 1, where (12) is a finite interval.
• The goal has no such restriction.

Assumption 1 of the paper (monotonicity of $f$ beyond $q^*$) and the continuity assumption of §3 are hypotheses of Theorems 3–4 only and are not used here. A formalization in which $f(q^*)$ or $\Delta(q^*)$ takes a junk value (a non-integrable $xf(x)$, a zero denominator) would make the goal trivially true or false; the hypotheses above exclude this, and no statement assumes the conclusion of another.

Contributions welcome: proofs of the milestones in any order; general lemmas on log-concave densities on $\mathbb R$ (exponential tails, integrability of moments, monotone hazard rates, continuity in the interior of the support); and the boundary cases of problem (11).

Selected references

• R. Levi, G. Perakis, J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights, Operations Research 63(6):1294–1306, 2015. Authors' accepted manuscript, MIT DSpace. https://doi.org/10.1287/opre.2015.1422
• R. Levi, R. O. Roundy, D. B. Shmoys, Provably Near-Optimal Sampling-Based Policies for Stochastic Inventory Control Models, Mathematics of Operations Research 32(4):821–839, 2007. https://doi.org/10.1287/moor.1070.0272

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

Motivation

A many-server queue in which customers arrive at the epochs of a renewal process and are served for exponential times is the basic model of a telephone exchange, a call centre, or a bank of identical machines. Its continuous-time queue-length process is not Markovian unless the arrivals are Poisson, so Erlang's birth–death formulas for M/M/s do not apply. In 1953 D. G. Kendall showed how to analyse such systems by the method of the imbedded Markov chain: observe the system only at the arrival epochs, where the number of customers present does form a Markov chain, and read the equilibrium behaviour off that chain (Kendall 1953).

Timeline:

• Erlang (1908–1929) treated M/M/s, where the queue length is itself Markovian.
• Kendall (1951) treated M/G/1 by a chain imbedded at departure epochs.
• W. L. Smith (Kendall's ref. [19]) observed that for a single server, under restrictions on the input law, exponential service gives an exponential waiting time apart from an atom at zero.
• Kendall (1953), this paper, treated GI/M/s for every input law and every number of servers $s$, and showed that Smith's restrictions are unnecessary.
• Foster (1953) gave the criterion for ergodicity of a denumerable chain through a summable invariant vector, which is the step Kendall's argument relies on.

Setting

Customers arrive with independent inter-arrival times of law $A$ on $[0,\infty)$ and mean $a$, $0<a<\infty$. There are $s\ge 1$ servers and a single queue served first come, first served. Service times are independent of one another and of the input, negative-exponential with mean $b$, $0<b<\infty$. The relative traffic intensity is $\rho=b/(sa)$.

The state of the imbedded chain at an arrival epoch is the number $i\in\{0,1,2,\dots\}$ of persons found ahead (waiting or in service) by the arriving customer. Its transition matrix $P=[p_{ij}]$ of eq. (8) is given in three blocks, written with the death-process probabilities $[n\mid m]=\int_0^\infty\binom{m}{n}(1-e^{-u/b})^n e^{-(m-n)u/b}\,dA(u)$ of (9)–(10), the probabilities $\{n\mid s;m\}$ of (11)–(12), and the Poisson probabilities $(n\mid s)=\int_0^\infty e^{-su/b}(su/b)^n/n!\,dA(u)$ of (13)–(14):

$$p_{ij}=\begin{cases}(i+1-j\mid s) & j\ge s,\ j\le i+1,\\ [\,i+1-j\mid i+1\,] & i<s,\ j<s,\ j\le i+1,\\ \{s-j\mid s;\,i-s+1\} & i\ge s,\ j<s,\\ 0 & j>i+1.\end{cases}$$

The key function is

$$F(\lambda)=\int_0^\infty e^{-(1-\lambda)su/b}\,dA(u).$$

The queue size met by an arrival is $Q=\max(i-s,0)$. The waiting time $w$ is, given $i$, the sum of $k=\max(i-s+1,0)$ independent exponential variables of mean $b/s$.

Formalization targets

Goal: Theorem IV (p. 350)

When $\rho<1$ the chain has a limiting distribution $\pi$, and with $\lambda$ the root of $F(\lambda)=\lambda$ in $(0,1)$ and $c=b/(s(1-\lambda))$,

$$\Pr(Q=n\mid Q>0)=(1-\lambda)\lambda^{n-1}\ (n\ge1),\qquad \Pr(w>t\mid w>0)=e^{-t/c}\ (t\ge0),$$

with both conditioning events of positive probability. The goal fixes no constant beyond those the theorem names: $\lambda$ and $c$ are determined by $A$, $b$ and $s$.

Milestones

• The matrix is stochastic (p. 349), and the chain is irreducible and aperiodic (p. 347).
• The coefficients $(n\mid s)$ are positive, sum to one and have mean $1/\rho$; $F(\lambda)=\sum_n (n\mid s)\lambda^n$; for $\rho<1$ the equation $F(\lambda)=\lambda$ has a unique root in $(0,1)$ (p. 348–349).
• For the trial vector $x=[\mu_0,\dots,\mu_{s-2},1,\lambda,\lambda^2,\dots]$ (15): the invariance equations for $j\ge s$ are equivalent to $F(\lambda)=\lambda$; those for $1\le j\le s-1$ determine the $\mu$'s; the one for $j=0$ follows from the row sums (pp. 348–349).
• A nonnull absolutely summable invariant vector makes the chain ergodic, and normalized it is the limiting distribution (p. 348).
• Theorem I: for $\rho<1$ the chain is irreducible and ergodic, and $\pi_j=C\lambda^{j-(s-1)}$ for $j\ge s-1$.
• Theorem II: $\Pr(Q=0)=\alpha=\dfrac{\sum\mu+1+\lambda}{\sum\mu+1/(1-\lambda)}$ and $\Pr(w=0)=\beta=\dfrac{\sum\mu+1}{\sum\mu+1/(1-\lambda)}$.
• Theorem III: $E(Q)=(1-\alpha)/(1-\lambda)$ and $E(w)/b=(1-\beta)/(s(1-\lambda))$.
• Eq. (27): for M/M/s the root is $\lambda=\rho$.

Significance

Theorem IV says that, whatever the input law and the number of servers, the part of the equilibrium waiting-time law away from zero is exponential and the part of the queue-size law away from zero is geometric, both governed by the single number $\lambda$. All equilibrium quantities of GI/M/s (Theorems II–III and the delay distribution) then reduce to computing $\lambda$ from a one-dimensional equation and the finitely many $\mu$'s from a triangular linear system. This is the standard textbook treatment of G/M/c queues and the template for many later matrix-geometric results.

The results are proved in the paper, partly by appeal to Feller's theory of denumerable chains and to "tedious but elementary" verifications. None of them is machine-checked. The mission formalizes the paper's chain of argument: the explicit transition matrix, its stochasticity, the reduction of the invariance equations, the passage from a summable invariant vector to the limiting distribution, and the computation of the laws of $Q$ and $w$ from it. The single-server special cases are posed separately on the platform (QueueingFundamentals.GM1.arrival_point_geometric, GM1.waiting_time_cdf, GM1.arrival_point_means, GM1.mean_waiting_times, FosterQueues.GIM1.gim1_classification); they do not cover $s\ge2$.

Difficulty

The obvious route is to guess the geometric tail and check it against the balance equations. For $j\ge s$ this works, but the rows $i\ge s$ of the block $\mathbf B$ involve the convolution integral (11), and the equations for $j<s$ couple the geometric tail to the boundary terms $\mu_0,\dots,\mu_{s-2}$. Showing these are solvable, and that the row sums of the three-block matrix equal one, requires handling (11) explicitly. The second obstacle is the limit theorem itself: an invariant vector does not, by itself, give $p^n_{ij}\to\pi_j$. That step needs Feller's dichotomy for irreducible aperiodic denumerable chains, which Mathlib does not provide. Finally, the conditional waiting-time law requires summing an Erlang mixture with geometric weights in closed form.

Formalization scope

The queue process itself is not formalized. The chain is defined by its transition matrix (8)–(14), and $w$ by the Erlang mixture of p. 349, as the paper derives both by a modelling argument. A chain is any TransitionMatrix P of the published Markov-chain vocabulary with P.p = gimsMatrix s A b; states are $0$-based. "Ergodic" is Feller's: Aperiodic ∧ PositiveRecurrent. The limiting distribution is asserted as Tendsto (P.stepProb n i j) atTop (𝓝 (π j)) for all $i,j$, not as a stationary vector. The input law satisfies the published IsInterarrivalLaw A a⁻¹ (a probability measure carried by $[0,\infty)$, integrable, mean $a$), and $(n\mid s)$ is the published serviceProb A (s/b) n. Conditional laws are stated multiplied out, together with positivity of the conditioning probabilities. Every series identity is stated with HasSum.

Trivializing formalizations are ruled out: $\lambda$ is tied to $F(\lambda)=\lambda$ on $(0,1)$ rather than free; $\pi$ is the limiting distribution of $P$, asserted to exist, not a probability vector handed to the statement; the conditioning events are asserted to have positive probability; the matrix is the GI/M/s matrix, not the GI/M/1 one; and the $\mu$'s of Theorems II–III are characterized by the invariance equations, never defined from $\pi$.

A complete development needs: Feller's limit theorem for irreducible aperiodic positive recurrent chains (reusable well beyond this mission), Foster's sufficiency criterion (referenced, open), Fubini for the stochastic-matrix identities, parametric interval integrals for the block $\mathbf B$, and Erlang distribution functions. Contributions to the general Markov-chain milestones are as welcome as those specific to GI/M/s.

Selected references

• D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Ann. Math. Statist. 24(3), 338–354, 1953. https://doi.org/10.1214/aoms/1177728975
• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24(3), 355–360, 1953. https://doi.org/10.1214/aoms/1177728976
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, Wiley, 1950, ch. 15.
• W. L. Smith, On the distribution of queueing times, Proc. Cambridge Philos. Soc. 49, 449–461, 1953 (cited by Kendall as "to be published", ref. [19]).
• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.3.

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

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