The OR Formalization Drive

Motivation

Decisions under uncertainty are often required to satisfy a constraint $\theta \in \Theta_\delta$ that depends on a random parameter $\delta$, and requiring it for every possible $\delta$ is usually too conservative or infeasible. The scenario approach replaces the unknown distribution of $\delta$ by $N$ independent samples (scenarios) and enforces only the sampled constraints; its generalization theorem (Campi and Garatti, 2008) bounds the probability that the resulting decision violates a fresh constraint.

Enforcing all $N$ sampled constraints can still be costly: a few unusual scenarios may dominate the solution. A practitioner therefore often discards $k$ of the sampled constraints, optimally, greedily or at random, and re-solves. The question is what guarantee survives: the removed constraints were chosen by looking at the data, so the solution is biased towards points of higher risk. Campi and Garatti (2011) answered it with a bound that holds for every removal procedure. This mission formalizes that answer as it is presented in Chapter 3, Section 3.3 and Chapter 5, Section 5.3 of the textbook Introduction to the Scenario Approach (Campi and Garatti, SIAM/MOS 2018), together with its explicit corollary, Theorem 1.2. Applications include chance-constrained control, portfolio selection and prediction, where discarding scenarios trades a controlled amount of risk for a better cost.

Setting

A decision $\theta$ ranges over $\mathbb R^d$ (in Lean, EuclideanSpace ℝ (Fin d)), with a closed convex domain $\Theta$ and a linear cost $c^{\mathsf T}\theta$. An uncertain parameter $\delta$ takes values in a measurable space $\Delta$ with probability $\mathbb P$, and each $\delta$ determines a closed convex constraint set $\Theta_\delta$. The violation probability of a decision is

$$V(\theta) = \mathbb P\{\delta \in \Delta : \theta \notin \Theta_\delta\}.$$

Given independent samples $\delta_1,\dots,\delta_N$ with joint law $\mathbb P^N$, the scenario program minimizes $c^{\mathsf T}\theta$ over $\theta \in \Theta \cap \bigcap_{i=1}^N \Theta_{\delta_i}$. For a set $I$ of indexes, the program without the constraints in $I$ minimizes the same cost over $\Theta \cap \bigcap_{i \notin I} \Theta_{\delta_i}$; its solution is written $\theta^*_I$. A removal procedure selects, as a function of the whole sample, a set of $k$ indexes, and $\theta^*_k$ denotes the solution of the program without them. The procedure is required to output a solution that violates exactly the $k$ removed constraints (with probability one): a removed constraint that turns out to be satisfied is reinstated and another is removed. Two standing assumptions are used throughout: Assumption 3.4, that $\Theta$ and every $\Theta_\delta$ are convex and closed, and Assumption 3.6, that for every sample size $m$ and every sample the scenario program has exactly one solution.

Formalization targets

Goal: Theorem 3.9

For $N \ge d$, under Assumptions 3.4 and 3.6, for every removal procedure and every $\varepsilon \in [0,1]$,

$$\mathbb P^N\{V(\theta^*_k) > \varepsilon\} \le \binom{k+d-1}{k} \sum_{i=0}^{k+d-1} \binom Ni \varepsilon^i (1-\varepsilon)^{N-i}.$$

The bound depends on the problem only through $d$, and on the removal procedure not at all. For $k = 0$ it is Theorem 3.7.

Milestones

1. Theorem 3.7 (no removal): $\mathbb P^N\{V(\theta^*) > \varepsilon\} \le \sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$, used for the program with the $N-k$ kept constraints.
2. Eq. (5.11): up to a zero probability set, the event $\{V(\theta^*_k) > \varepsilon\}$ is contained in the union over all $k$-element index sets $I$ of the events "$\theta^*_I$ violates all constraints in $I$ and $V(\theta^*_I) > \varepsilon$".
3. Eq. (5.13): for a fixed $I$, the probability of that event equals $\int_{(\varepsilon,1]} \alpha^k F_V(d\alpha)$, where $F_V$ is the law of $V(\theta^*_I)$.
4. Eq. (5.14) and Theorem 3.9 for $d = 2$: the book's complete proof in the plane.
5. Eqs. (3.15)–(3.17) and the conclusion of Section 3.3.1: with the explicit level $\varepsilon_k$ of (1.9), the right-hand side of (3.13) is at most $\beta$.
6. Theorem 1.2: with probability at least $1-\beta$, $V(\theta^*_k) \le \varepsilon_k$, where

$$\varepsilon_k = \frac{k}{N} + \left[\frac{\sqrt k}{N} + \frac{\sqrt k+1}{N}\left((d-1)\ln(k+d-1) + \frac{d-1}{\sqrt k} + \ln\frac1\beta\right)\right].$$

Significance

Theorem 3.9 certifies every constraint-removal heuristic at once. Since the guarantee is the same for optimal, greedy and random removal, a user may pick the removal strategy purely for cost, and may inspect several values of $k$ before choosing, paying only a union bound over the values tried (Section 3.3). Theorem 1.2 turns the bound into an explicit rate: when $k/N$ is held fixed, the violation exceeds the empirical risk $k/N$ by a margin of order $\ln N/\sqrt N$, only slightly worse than the $1/\sqrt N$ rate for estimating the probability of a fixed event. The result also shows that the violation after removal concentrates around the target level, which is the basis of the book's comparison between sampling-and-discarding and simply using fewer scenarios (Example 3.10).

Theorem 3.9 is proved in the literature for general $d$ (Campi and Garatti, 2011); the textbook proves it for $d = 2$. To our knowledge no part of the scenario approach has a machine-checked proof. A formal development would supply the first verified version of the removal bound, a Lean treatment of solution maps of random convex programs, and reusable combinatorial and binomial-tail estimates.

Difficulty

The removed set is chosen after seeing the data, so the kept constraints are not an independent sample and Theorem 3.7 cannot be applied to $\theta^*_k$ directly. The argument must pass through all $\binom Nk$ fixed index sets and account for the event that the removed constraints are violated; a plain union bound that ignores this event loses a factor $\binom Nk$ and does not give (3.13). For a fixed index set, the probability that the $k$ removed scenarios are all violated involves the distribution of $V(\theta^*_I)$, which is only known to be dominated by a Beta law, so a stochastic-domination argument for the increasing function $\alpha \mapsto \alpha^k$ is needed. In general dimension the combinatorial constant $\binom{k+d-1}{k}$ comes from a sharper counting than the two-dimensional computation of Section 5.3, and that argument is in the cited paper rather than in the book.

Formalization scope

Decisions live in EuclideanSpace ℝ (Fin d), samples of size $m$ are maps Fin m → Δ with law Measure.pi (fun _ => P) for a probability measure P, and the violation is the real number (P {δ | θ ∉ Θδ δ}).toReal. Events over samples are compared in ℝ≥0∞ with ENNReal.ofReal of the book's right-hand side. The removal procedure is an arbitrary map I : (Fin N → Δ) → Finset (Fin N) with (I ω).card = k, and θk is a map that, for every sample, solves the program without the constraints in I ω, and violates each of them with probability one. The following implicit hypotheses of the book are written as binders:

• $d \ge 1$, $d \le N$, $k \le N$ and $\varepsilon \in [0,1]$;
• Assumption 3.6 for every $m$, including $m = 0$, and for every sample (not almost every);
• the removed constraints are violated with probability one (∀ᵐ ω ∂ℙ^N), the book's own hypothesis on p. 65, so (5.11) is an inclusion up to a null set as on the page; requiring the violation for every sample would be unsatisfiable for $1 \le k < N$ (on a sample with all $\delta_i$ equal a kept constraint coincides with a removed one) and would make the results vacuous;
• measurability, which the book glosses over (p. 33): the constraint relation $\{(\theta,\delta) : \theta \in \Theta_\delta\}$ is jointly measurable, the solution map of the scenario program with $m$ constraints is measurable for every $m$, and $\theta^*_k$ is measurable;
• for Theorem 1.2 and Section 3.3.1: $k \ge 1$ (formula (1.9) divides by $\sqrt k$), $N \ge 1$, $\beta \in (0,1)$; Section 3.3.1 additionally assumes $\varepsilon_k \le 1$, the range in which its chain of inequalities holds.

Theorem 1.2 is stated in the constraint formulation of Chapter 3, to which the book says it "straightforwardly generalizes" (p. 20), with the hypotheses of Theorem 3.9 from which Section 3.3.1 derives it. Eq. (5.14) and the closing display of Section 5.3 are stated for $d = 2$ only, as in the book.

A trivializing formalization is excluded: the removal procedure is universally quantified, the solutions are exact minimizers rather than arbitrary feasible points, and the event is the strict $V(\theta^*_k) > \varepsilon$; a statement for one fixed rule, or with $\theta^*_k$ unconstrained, would be a different theorem.

A complete development needs: product measures and Fubini over Fin N → Δ, reindexing of the kept constraints as a sample of size $N-k$, the Beta form of the binomial tail (the platform's binomial_upper_tail_eq_incomplete_beta is available), and stochastic domination for monotone integrands. Solution-map and violation infrastructure is shared with the sibling missions of this series. Contributions on any milestone, including the general-$d$ counting argument of the cited paper, are welcome.

Selected references

• M. C. Campi and S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018. https://doi.org/10.1137/1.9781611975444
• M. C. Campi and S. Garatti, A sampling-and-discarding approach to chance-constrained optimization: feasibility and optimality, Journal of Optimization Theory and Applications 148(2), 257–280, 2011. https://doi.org/10.1007/s10957-010-9754-6
• M. C. Campi and S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3), 1211–1230, 2008. https://doi.org/10.1137/07069821X
• G. C. Calafiore and M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5), 742–753, 2006. https://doi.org/10.1109/TAC.2006.875041

Motivation

Stochastic quasigradient (SQG) methods minimize an expectation $F(x)=E_\omega f(x,\omega)$ over a constraint set $X\subseteq\mathbb R^n$ when neither $F$ nor its gradient can be computed, only random vectors whose conditional mean is (close to) a subgradient. They are the workhorse of stochastic programming and, under the name stochastic gradient descent, of large-scale statistical learning. The classical convergence theory, going back to Robbins and Monro (1951) and to Ermoliev's quasi-Féjer analysis, asks the stepsizes to be chosen in advance with $\rho_s\to0$, $\sum\rho_s=\infty$, $\sum\rho_s^2<\infty$. Uryasev, in Chapter 18 of Numerical Techniques for Stochastic Optimization (Ermoliev and Wets, eds., 1988), points out that such programmed rules are slow in practice, and that practitioners want adaptive stepsizes computed on line from the observed directions.

Timeline:

• 1951: Robbins and Monro, stochastic approximation with programmed steps.
• 1976: Ermoliev, Methods of Stochastic Programming: the SQG projection method and its a.s. convergence through stochastic quasi-Féjer sequences.
• 1983: Mirzoakhmedov and Uryasev (Zh. Vychisl. Mat. i Mat. Fiz., cited as [7] in Ch. 18 and [14] in Ch. 17): Cesàro convergence of the weighted mean with $\rho_s\to0$ and $\sum\rho_s=\infty$ only, under the two measurability regimes. Chapter 17 states it as Theorem (ii); Chapter 18 as Theorem 1.
• 1988: Uryasev, Ch. 18, applies it to the adaptive rule (18.5) (Theorem 2).
• 1992: Polyak and Juditsky, averaging of iterates for smooth stochastic approximation, with optimal asymptotic variance.

Setting

Let $X\subseteq\mathbb R^n$ be nonempty, convex and compact, $C_1=\max_{x,y\in X}\|x-y\|$ its diameter, and $F$ convex on an open convex set $U\supseteq X$, with subdifferential $\partial F(x)$. The projection $\pi_X(y)$ is the point of $X$ nearest to $y$. On a probability space, the SQG method generates

$$x^{s+1}=\pi_X(x^s-\rho_s\xi^s),\qquad s=0,1,\dots\qquad(18.2)$$

from $x^0\in X$, where the direction $\xi^s$ is a stochastic quasigradient: $E(\xi^s\mid B_s)=F_x(x^s)+b^s$ with $F_x(x^s)\in\partial F(x^s)$, a bias $b^s$, and $B_s$ the $\sigma$-algebra induced by $(x^0,\dots,x^s,\xi^0,\dots,\xi^{s-1})$.

The adaptive stepsize rule of the chapter is, for fixed $a>1$, $\delta>0$ and $\rho_0>0$,

$$\rho_{s+1}=\rho_s\,a^{\langle\xi^{s+1},\,x^s-x^{s+1}\rangle-\delta\rho_s}\qquad(18.5).$$

The step grows when consecutive moves point the same way and shrinks otherwise. The weighted (Cesàro) averages are

$$\bar x^s=\sum_{\ell=0}^s\rho_\ell x^\ell\Big/\sum_{\ell=0}^s\rho_\ell\qquad(18.6).$$

The sequence $x^s$ is Cesàro convergent when $\bar x^s$ converges to the solution set.

Chapter 17 (Pflug) uses the same method for $f(x)=E_P\,q(x,\xi)$ over a closed convex $S\subseteq\mathbb R^k$, with $Y=\nabla q(X_n,\xi_n)$ from i.i.d. $\xi_n$ and stepsizes adapted to $\sigma(\xi_0,\dots,\xi_{n-1})$.

Formalization targets

Goal: Theorem 2 of Chapter 18

Under $\sup_s\|\xi^s\|<C_2$ (18.15), $\limsup\|b^s\|\le\bar b$ (18.16) and $\delta>C_2\limsup_s\inf_{h\in\partial F(x^s)}\|\xi^s-h\|$ (18.17), almost surely,

$$\limsup_{s\to\infty}\Big(F(\bar x^s)-\min_{x\in X}F(x)\Big)\le\bar b\,C_1,$$

and if $b^s\to0$ a.s., then $F(\bar x^s)\to\min_XF$ and all accumulation points of $\bar x^s$ are minimizers, almost surely.

Milestones

1. Chapter 17, Theorem (i): $\sum\rho_n=\infty$ and $\sum\rho_n^2<\infty$ a.s. imply $X_n\to x^*$ a.s.
2. Chapter 17, Theorem (ii): for convex $f$ and bounded $S$, $\rho_n\to0$ and $\sum\rho_n=\infty$ a.s. imply $\bar X_n\to x^*$ a.s.
3. Chapter 18, Theorem 1: for any stepsizes with $\rho_s>0$, $E\rho_s^2<\infty$, $\rho_s\to0$, $\sum\rho_s=\infty$ and measurability condition (1) or (2), $\limsup F(\bar x^s)-F(x^*)\le\bar bC_1$ a.s.
4. Chapter 18, Corollary: with $b^s\to0$, the accumulation points of $\bar x^s$ are solutions.
5. Eq. (18.18): $\|x^{s+1}-x^s\|\le\|\rho_s\xi^s\|\le\rho_sC_2$.
6. Proof of Theorem 2, step 1: the adaptive steps satisfy $\sum\rho_s=\infty$.
7. Proof of Theorem 2, step 2: under (18.17), $\rho_s\to0$.
8. End of step 2: $\rho_s\to0$ implies $\rho_{s+1}/\rho_s\to1$.

Significance

Theorem 2 is a convergence guarantee for a stepsize rule that is computed from the run itself. It needs no square summability of the steps, and it tolerates a nonvanishing bias at a cost linear in the bias. This is the regime of practical SQG codes; §18.4–18.5 of the chapter discuss implementation and numerical experiments. Theorem 1 isolates the reason: Cesàro convergence needs only $\rho_s\to0$ and $\sum\rho_s=\infty$. It also allows a stepsize that depends on the current direction, provided consecutive steps have ratio tending to $1$.

The volume proves none of the probabilistic results in full. Theorem 1 of Chapter 18 is cited from Uryasev's earlier report. Theorem 2 has an outline proof that reduces it to Theorem 1. Chapter 17 gives a sketch through the Robbins–Siegmund lemma. None of these results is formalized. The mission produces machine-checked statements of all of them, with the misprints of the page resolved, and it separates the pathwise part of the Theorem 2 argument (steps 1 and 2, which are deterministic) from the martingale part (Theorem 1).

Difficulty

The obvious route to a.s. convergence is the quasi-Féjer or Robbins–Siegmund argument. It controls $\|x^s-x^*\|^2$ and needs $\sum\rho_s^2\|\xi^s\|^2<\infty$, which is exactly what is not available here. The averaged analysis has to show that the martingale term $\sum_\ell\rho_\ell\langle\xi^\ell-E(\xi^\ell\mid B_\ell),x^*-x^\ell\rangle$ is $o(\sum_\ell\rho_\ell)$ almost surely, and that $\sum_\ell\rho_\ell^2\|\xi^\ell\|^2$ is $o(\sum_\ell\rho_\ell)$, when the stepsizes are themselves random. Under condition (2) of Theorem 1, $\rho_s$ is not even measurable with respect to the $\sigma$-algebra of the conditional expectation. So $E(\rho_s\xi^s\mid B_s)\ne\rho_sE(\xi^s\mid B_s)$, and the standard decomposition breaks. For the adaptive rule, the stepsizes are coupled to the iterates through the exponent. Neither $\sum\rho_s=\infty$ nor $\rho_s\to0$ is given, and both must be derived path by path.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Sequences are indexed from $0$. Chapter 17 is shifted by one against the page: its $X_n,\xi_n,\mathcal F_n$, $n\ge1$, become indices $n-1$. Conditional expectations are Mathlib's condExp with respect to the history $\sigma$-algebras of the definition file. Every $\limsup$ bound is written out as "for every $\varepsilon>0$, eventually $\dots\le\dots+\varepsilon$", or in (18.17) as a bound $L$ with $C_2L<\delta$. Expectations of squared norms are lower Lebesgue integrals. The deterministic proof steps (items 5 to 8) are stated for one sample path.

Readings of the page, each recorded in the item's Formalization Note:

• (18.17) prints $C_1$. The proof's estimate gives $(C_2C_s-\delta)\rho_s$, and only $C_2$ is invariant under rescaling of $\mathbb R^n$, so $C_2$ is stated.
• (18.5) has two forms that agree only without projection. The proof uses the second, $a^{\langle\xi^{s+1},x^s-x^{s+1}\rangle-\delta\rho_s}$, which is stated.
• (18.8) prints $F_s(x^s)$ for $F_x(x^s)$. (18.11) prints $E\rho_s^s$, read as $E\rho_s^2<\infty$.
• Theorem 2's "$F(x^s)-\min z\in XF(x)\to0$" is read as $F(\bar x^s)-\min_XF\to0$.
• The end of step 2 prints $\rho_{s+1}/\rho_s\to0$, read as $\to1$.
• Chapter 17, assumption (ii) prints $\|\nabla f(x)\|\le A+B\|x-x^*\|^2$. The proof uses $\|\nabla f(x)\|^2$, and the printed form makes part (i) false, so the squared form is stated. $\mathrm{Var}(Y_x)\le C$ is read as $E\|Y_x-EY_x\|^2\le C$.
• The Corollary adds lower semicontinuity of $F$ on $X$, without which it fails.
• $x^0\in X$ is assumed, and $\rho_0$ in Theorem 2 is a fixed positive number.

No explicit constants replace an O(·) or an unspecified "C": every constant appears in the book's statements.

A trivializing formalization states Theorem 2 for arbitrary stepsizes satisfying (18.10)–(18.13), which is Theorem 1 again. Here the stepsizes are tied to the iterates by (18.5), and the $\delta$ of (18.17) is the $\delta$ of the rule.

Needed infrastructure: a Robbins–Siegmund almost-supermartingale lemma, which Mathlib does not have; a strong law for martingale differences with random weights (Kronecker's lemma in its stochastic form); nonexpansiveness of the projection onto a closed convex set; and nonemptiness of the subdifferential of a finite convex function on an open set. The first two are reusable across stochastic approximation. Contributions of any of the milestones, or of these lemmas as separate theorems, are welcome.

Selected references

• G. Ch. Pflug, Stepsize Rules, Stopping Times and their Implementation in Stochastic Quasigradient Algorithms, in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer 1988, Ch. 17. https://doi.org/10.1007/978-3-642-61370-8
• S. Uryasev, Adaptive Stochastic Quasigradient Procedures, ibid., Ch. 18. https://doi.org/10.1007/978-3-642-61370-8
• Yu. Ermoliev, Stochastic Quasigradient Methods, ibid., Ch. 6. https://doi.org/10.1007/978-3-642-61370-8
• F. Mirzoakhmedov and S. P. Uryasev, Adaptive step size control for stochastic optimization algorithm, Zh. Vychisl. Mat. i Mat. Fiz. 23(6) (1983) 1314–1325 (in Russian); cited in the volume above, no online copy linked.
• H. Robbins and S. Monro, A Stochastic Approximation Method, Ann. Math. Statist. 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586
• H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press 1971, 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• B. T. Polyak and A. B. Juditsky, Acceleration of Stochastic Approximation by Averaging, SIAM J. Control Optim. 30 (1992) 838–855. https://doi.org/10.1137/0330046

Motivation

Service parts (spares for aircraft, machines, and networks) are typically managed item by item with a one-for-one replenishment policy, the $(s-1, s)$ policy: every unit withdrawn to meet a demand triggers an order for one replacement, so the inventory position stays at the stock level $s$. A firm stocking thousands of such items at one location has to choose all the stock levels together, trading a budget on inventory investment against a service measure. Chapter 3 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) sets up the three standard service measures (fill rate, ready rate, expected backorders), shows which of them have the convexity that optimization needs, and solves two multi-item stocking problems: minimum expected backorders under an investment budget, by Lagrangian relaxation justified by Everett's theorem, and maximum average fill rate, by a greedy marginal-analysis rule.

The Lagrangian method goes back to Everett (Operations Research 1963); the search for the multiplier in one-constraint problems of this kind is Fox and Landi (Operations Research 1970); the compound Poisson $(s-1,s)$ model is Feeney and Sherbrooke (Management Science 1966). The same separable Lagrangian structure underlies the multi-echelon METRIC-type models later in the book.

Setting

A single item is stocked at one location, demand not met from stock is backordered, and customer orders arrive as a Poisson process of rate $\lambda > 0$. An order is for $j$ units with probability $u_j$, where $u_0 = 0$ and the mean order size $\bar u = \sum_j j u_j$ is finite (compound Poisson demand; simple Poisson demand is $u_1 = 1$). Resupply times have mean $\bar\tau > 0$. The steady-state probability that $x$ units are in resupply is

$$p(0 \mid \lambda\bar\tau) = e^{-\lambda\bar\tau}, \qquad p(x \mid \lambda\bar\tau) = \sum_{j \ge 1} e^{-\lambda\bar\tau}\frac{(\lambda\bar\tau)^j}{j!}\,u^{(j)}_x \quad (x \ge 1),$$

where $u^{(j)}_x$ is the probability that $j$ orders total $x$ units. In this mission $p(\cdot \mid \lambda\bar\tau)$ is the definition of the model, not a consequence of Palm's theorem. The mean lead-time demand is $\mu = \lambda\bar\tau\bar u$, and the book also writes $p(x \mid \mu)$.

For a stock level $s \in \{0, 1, 2, \dots\}$:

• the ready rate is $R(s) = \sum_{x \le s} p(x \mid \lambda\bar\tau)$;
• the expected backorders are $B(s) = \sum_{x > s}(x - s)\,p(x \mid \lambda\bar\tau)$;
• the expected on-hand inventory is $\sum_{x \le s}(s - x)\,p(x \mid \lambda\bar\tau)$;
• under simple Poisson demand the fill rate is $F(s) = \sum_{x < s} p(x \mid \lambda\bar\tau)$.

Forward differences are $\Delta f(s) = f(s+1) - f(s)$ and $\Delta^2 f(s) = \Delta f(s+1) - \Delta f(s)$; discrete convexity means $\Delta^2 f \ge 0$.

With $n$ items, unit costs $c_i > 0$ and budget $b$, Problem 4 (3.40) is

$$\min \sum_i B_i(s_i) \quad \text{s.t.} \quad \sum_i c_i\,[s_i - \mu_i + B_i(s_i)] \le b,\quad s_i \in \{0,1,\dots\}.$$

For a multiplier $\theta > 0$, the item-wise criterion defines $s_i^*(\theta)$ as the least $s$ with $\sum_{x \le s} p(x \mid \mu_i) \ge 1/(1 + \theta c_i)$, and $C(\theta) = \sum_i c_i\,[s_i^*(\theta) - \mu_i + B_i(s_i^*(\theta))]$.

Formalization targets

Goal: the Lagrangian stock levels solve Problem 4

For every $\theta > 0$, each $s_i^*(\theta)$ exists and

$$\sum_i c_i\,[s_i - \mu_i + B_i(s_i)] \le C(\theta) \ \Longrightarrow\ \sum_i B_i(s_i^*(\theta)) \le \sum_i B_i(s_i)$$

for every vector $s$ of nonnegative integer stock levels. That is, $s^*(\theta)$ is optimal for Problem 4 at budget $b = C(\theta)$. This is what the book asserts by combining Theorem 10 (p. 57, with the remark on p. 58) and the criterion of p. 61, and it is the basis of its bisection algorithm (p. 63). The goal fixes no numerical constant.

Milestones

1. Section 3.3, p. 53: $\Delta F(s) = p(s \mid \lambda\bar\tau)$ and $\Delta^2 F(s) = p(s \mid \lambda\bar\tau)\,(\lambda\bar\tau/(s+1) - 1)$, so under simple Poisson demand $F$ is discretely concave exactly on $s \ge \lfloor\lambda\bar\tau\rfloor$ (resp. $s \ge \lambda\bar\tau - 1$ for integer $\lambda\bar\tau$).
2. Section 3.3, p. 55: $\Delta B(s) = -(1 - R(s))$ and $\Delta^2 B(s) = p(s+1 \mid \lambda\bar\tau)$.
3. Theorem 10 (Everett), p. 57.
4. Section 3.4.2, p. 60: $E[\text{On-hand}] = s - \lambda\bar\tau\bar u + B(s)$.
5. Section 3.4.2, p. 61: the least $s$ with $R(s) \ge 1/(1+\theta c)$ minimizes $f(s) = (1 + \theta c)B(s) + \theta c s$.
6. Section 3.4.2, p. 61: $s^*(\theta)$ and $C(\theta)$ are nonincreasing in $\theta$.
7. Section 3.4.2, p. 63: at $\theta_{\max} = \max_i c_i^{-1}(1/p(0 \mid \mu_i) - 1)$ every $s_i^*(\theta_{\max}) = 0$.
8. Section 3.4.3, p. 65: every solution produced by the greedy marginal-analysis rule for Problem 5 (3.41), maximum average fill rate subject to $\sum_i c_i s_i \le b$ and $s_i \ge \lfloor\lambda_i\bar\tau_i\rfloor$, is optimal at the budget it uses.

Significance

The goal reduces a coupled integer program over thousands of items to one scalar search: for a fixed multiplier each item is solved by a single scan of its distribution function, and each multiplier yields a point on the exact efficient frontier of expected backorders against investment. Milestone 8 does the same for fill rates on the region where they are concave, and milestone 1 explains why that region, $s \ge \lfloor\lambda\bar\tau\rfloor$, is imposed in practice. Milestone 4 is the identity that turns an investment budget into the constraint of Problem 4.

All results are proved in the book (Theorem 10 with a complete proof; the others by short derivations, the greedy optimality by a sketch). None of them is formalized, as far as the platform shows: there is no Everett-type Lagrangian sufficiency theorem, no compound Poisson backorder function, and no discrete marginal-analysis optimality result. The mission produces a reusable layer for later chapters: the compound Poisson steady-state law with its backorder function, and the Lagrangian machinery the book reuses for multi-echelon systems.

Difficulty

The algebra of first differences is elementary; the difficulties are elsewhere. $B(s)$ is an infinite series whose convergence rests on the finiteness of the mean order size, and exchanging the difference with the sum, and identifying $\sum_x x\,p(x \mid \lambda\bar\tau)$ with $\lambda\bar\tau\bar u$, requires manipulating a doubly infinite sum over order counts and convolution powers. Existence of $s^*(\theta)$ requires that the compound Poisson probabilities sum to one. For milestone 8 the obvious argument ("greedy is optimal for concave separable objectives") fails for knapsack constraints with unequal costs at arbitrary budgets; it holds only at the budgets the greedy run generates, and only on the region where every $F_i$ is concave; dropping the floor constraints $s_i \ge \lfloor\lambda_i\bar\tau_i\rfloor$ makes it false.

Formalization scope

Stock levels are natural numbers; probabilities, rates, costs and multipliers are reals. The compound Poisson law is a structure with fields $\lambda, \bar\tau > 0$, an order-size distribution $u$ with $u_0 = 0$, $u_j \ge 0$, $\sum_j u_j = 1$, and summable $j u_j$ (the finite mean is added: without it $B$ is infinite). Expected on-hand inventory is the finite sum $E[(s - X)^+]$. Items are indexed by an arbitrary finite type (nonempty where a maximum over items is taken).

Pinnings and deviations, each stated in the item's Formalization Note:

• $\theta > 0$ and $c > 0$. The book allows $\theta \ge 0$ in (3.38); at $\theta = 0$ the threshold $1$ is never reached and $f = B$ has no minimizer.
• Theorem 10 without convexity and for an arbitrary set $S$: the book assumes $f, g$ convex, but its proof does not use it and the applications are to integer vectors (labelled generalization).
• $B$'s identities for compound Poisson demand. The book derives them under simple Poisson demand and uses them for compound demand on p. 61; strict convexity and strict decrease are stated only for simple Poisson demand, as in the book.
• Optimality is always against every feasible vector, never an infimum; the greedy procedure is a relation on sequences, covering every tie-breaking rule.
• Problem 5 keeps the constraints $s_i \ge \lfloor\lambda_i\bar\tau_i\rfloor$.

A trivializing formalization is ruled out: the goal is stated for the book's own backorder function $B$ built from the compound Poisson law, not for an arbitrary convex function nor for a $B$ defined through its differences.

Welcome contributions: summability and normalization lemmas for the compound Poisson law, a general discrete Lagrangian lemma for separable objectives, and proofs of the milestones in any order.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Chapter 3, pp. 47–65. https://doi.org/10.1007/b138879
• H. Everett III, Generalized Lagrange multiplier method for solving problems of optimum allocation of resources, Operations Research 11(3):399–417, 1963. https://doi.org/10.1287/opre.11.3.399
• B. L. Fox and D. M. Landi, Searching for the multiplier in one-constraint optimization problems, Operations Research 18(2):253–262, 1970. https://doi.org/10.1287/opre.18.2.253
• G. J. Feeney and C. C. Sherbrooke, The (s−1, s) inventory policy under compound Poisson demand, Management Science 12(5):391–411, 1966. https://doi.org/10.1287/mnsc.12.5.391

Motivation

Spare-parts inventory models for repairable items rest on Palm's theorem: if demands arrive as a Poisson process with constant rate $\lambda$ and each demanded unit spends an independent, identically distributed resupply time with mean $\bar\tau$ in the pipeline, the number of units in resupply is Poisson with mean $\lambda\bar\tau$ in steady state. Stock levels, backorders and fill rates are all computed from that distribution.

Both assumptions fail in practice. Military flying programmes ramp up and down within weeks, repair shops close for periods, and commercial parts distribution centres see demand that varies by day of the week. Chapter 9 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) extends Palm's theorem to a nonstationary Poisson demand process with time-dependent resupply-time distributions, gives the compound (multi-unit order) version, and uses the result to compute, at any time $t$, the distribution of units in repair at the depot of a two-echelon system.

Timeline: Palm (1938) proved the stationary result for telephone traffic; Feeney and Sherbrooke (1966) extended it to compound Poisson demand; Hillestad and Carrillo (RAND, 1980) and Crawford (RAND, 1981) developed the time-dependent extensions, summarized by Carrillo (RAND, 1989). The chapter presents these results.

Setting

A single item is stocked at one location, and every demand is for one unit.

• Demand rate $\lambda(s) \ge 0$, integrable on bounded intervals, with mean function $m(t) = \int_0^t \lambda(s)\,ds$.
• Demand process: a nonstationary Poisson process with mean function $m$, with $N(0) = 0$. $N(t)$ counts demands in $[0,t]$ and $T_0 < T_1 < \cdots$ are the demand epochs.
• Resupply times: a unit demanded at time $s$ is resupplied within $w$ time units with probability $G_s(w)$. Resupply times are nonnegative, have finite expectations, are independent from unit to unit, and are independent of the demand process.
• $X(t)$ is the number of units in resupply at time $t$: demands in $[0,t]$ whose resupply is not complete at $t$.

The mean of $X(t)$ is

$$\alpha(t) = \int_0^t \bigl(1 - G_s(t-s)\bigr)\lambda(s)\,ds.$$

In the compound version (Section 9.2), orders arrive as above and each order is for $Q \ge 1$ units, with a time-stationary law $u_j = P(Q = j)$. All units of an order share its resupply time, $Y(t)$ counts units demanded in $[0,t]$, and $u^{(n)}_k$ is the $n$-fold convolution of $(u_j)$.

In the two-echelon version (Section 9.3), base $i$ has failure rate $\lambda_i$. A failure is repaired at the base with probability $r_i$ and at the depot otherwise. Depot repair of a failure occurring at time $u$ takes a deterministic time $D(u)$ with $D(t) + t \ge D(s) + s$ for $s < t$ (no crossing). Write $\tilde t = \inf\{u \ge 0 : D(u) + u > t\}$.

Formalization targets

Goal: Theorem 13 (p. 216)

For every $t \ge 0$,

$$P\{X(t) = k\} = e^{-\alpha(t)}\frac{\alpha(t)^k}{k!}, \qquad k = 0,1,2,\dots$$

This is an exact statement at each finite time, not a limit. With constant $\lambda$ and $G_s = G$ it reduces to the finite-time step of Palm's theorem.

Milestones

1. $E[N(t)] = m(t)$ (Section 9.1, p. 216).
2. Theorem 12 (p. 216): given $N(t) = n$, the epochs $T_0, \dots, T_{n-1}$ are distributed as the order statistics of $n$ i.i.d. variables with distribution function $F(x) = m(x)/m(t)$ on $[0,t)$.
3. The binomial step of the proof of Theorem 13 (pp. 216–217): $P\{X(t) = k \mid N(t) = n\} = \binom nk p^k(1-p)^{n-k}$, with $p = \int_0^t (1 - G_s(t-s))\lambda(s)/m(t)\,ds$.
4. Section 9.2 (p. 218): $E[Y(t)] = m(t)E[Q]$ and $\operatorname{Var}[Y(t)] = m(t)E[Q^2]$.
5. Theorem 14 (p. 218): $P[X(t) = k] = \sum_{n\ge1} u^{(n)}_k e^{-\alpha(t)}\alpha(t)^n/n!$ for $k \ge 1$, and $e^{-\alpha(t)}$ at $k = 0$.
6. Section 9.3.2 (p. 221): $P\{X_0(t) = k\} = e^{-m_0(\tilde t,t)} m_0(\tilde t,t)^k/k!$ with $m_0(\tilde t,t) = \int_{\tilde t}^t \sum_i \lambda_i(u)(1-r_i)\,du$.

A plain supporting item states that $N(t)$ is Poisson with mean $m(t)$, the factor the proof of Theorem 13 uses.

Significance

Theorem 13 gives the full distribution of the pipeline at every instant. Time-dependent expected backorders, $\sum_{x > s(t)} (x - s(t)) P\{X(t) = x\}$, and fill rates $P\{X(t) < s(t)\}$ follow from it, so stock levels can be planned against a surge or a repair outage without a steady-state approximation. Theorem 14 does the same for multi-unit orders. The depot result feeds the base-level convolution of Section 9.3.3, which in turn gives time-dependent performance measures for a two-echelon system.

These results are proved in the literature, and the chapter reproduces the proofs of Theorems 13 and 14. It cites Theorem 12 without proof ("similar to the one given in Chapter 3"). No machine-checked version of any of them is known, and neither Mathlib nor this platform has a Poisson process, stationary or not, a thinning theorem, or an order-statistics theorem. The formal content of this mission therefore includes the construction and the first distributional facts of the nonstationary Poisson process.

Difficulty

The algebra of the proof is a Poisson mixture of binomials and is short. The difficulty is Theorem 12 and its use. The obvious argument treats "the $n$ demands in $[0,t]$" as $n$ independent draws from $F$ and assigns each an independent resupply time with law $G_{\text{draw}}$. Making this rigorous requires identifying the conditional joint law of the epochs given $N(t) = n$. The resupply time of the $j$-th demand is not independent of its epoch: its law depends on the epoch. So it must be shown that, after conditioning, the marks attached to sorted epochs behave like marks attached to unsorted i.i.d. draws. The book's constant-rate argument (Chapter 3) uses the uniform density $n!/t^n$ on the simplex. Here the density involves $\lambda$, which may vanish on intervals, and $m$ need not be invertible.

Formalization scope

• Demand process. The nonstationary Poisson process is constructed, not postulated. With i.i.d. exponential(1) gaps and unit-rate points $\Gamma_k = A_0 + \cdots + A_k$, the $k$-th demand occurs at $T_k = \inf\{s \ge 0 : m(s) \ge \Gamma_k\}$, and $N(t) = \#\{k : \Gamma_k \le m(t)\}$.
• Resupply times. Resupply times are $\rho(T_k, U_k)$ for a jointly measurable $\rho \ge 0$ and i.i.d. marks $U_k$ independent of the gaps, with $G_s(w) = \nu\{\rho(s,\cdot) \le w\}$. Every measurable family $G_s$ arises this way, and joint measurability makes $\alpha(t)$ a genuine integral. Independence of resupply times from the demand process is not written in Theorem 12 or 13 but is used in the proof; it is part of the model.
• Pinnings and conventions.
  • "$\lambda$ integrable" is read as integrable on bounded intervals.
  • Time is $t \ge 0$.
  • Theorem 12 assumes $m(t) > 0$, since $F$ is $0/0$ otherwise, and sets $F = 0$ on $(-\infty,0)$.
  • Conditional probabilities are written as joint probabilities.
  • $E[Y(t)]$ is stated in $[0,\infty]$; the variance identity assumes $E[Q^2] < \infty$.
  • $\tilde t$ is an infimum over $u \ge 0$, and $D \ge 0$.
  • Counts are cardinalities, and are $0$ on the null event where they would be infinite.
• Corrections. Theorem 14's printed sum starts at $n = 1$, which gives $P[X(t) = 0] = 0$. The statement keeps the book's formula for $k \ge 1$ and adds $P[X(t) = 0] = e^{-\alpha(t)}$. The depot's Poisson demand stream with rate $\sum_i \lambda_i(1-r_i)$ is generated from the bases' processes and independent repair-location choices, not assumed.
• Not stated.
  • Eqs. (9.1)–(9.2), the FCFS depot backorders owed to base $i$: the derivation on p. 221 is informal, and (9.1) prints the exponent $s_0(t-1)$ for $s_0(t)-1$.
  • The base analysis of Section 9.3.3.
  • The compound law of $Y(t)$ on p. 217, which has the same $n = 0$ omission.
• Trivialization ruled out. $X(t)$ is computed from the demand epochs and resupply times, not defined by its law, and resupply times cannot depend on the demand epochs except through the prescribed $G_s$. Either shortcut would make the goal empty or false.
• Infrastructure. The time-changed Poisson construction, its count law, the order-statistics property and marked thinning are reusable well beyond this chapter: in queueing ($M_t/G_t/\infty$), in reliability, and in the stationary Palm mission of this series. Contributions of these general lemmas are welcome.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Chapter 9, pp. 215–222. https://doi.org/10.1007/b138879
• C. Palm, "Analysis of the Erlang traffic formulae for busy-signal arrangements", Ericsson Technics 5, 1938, 39–58.
• G. J. Feeney and C. C. Sherbrooke, "The (s−1, s) inventory policy under compound Poisson demand", Management Science 12(5), 1966, 391–411. https://doi.org/10.1287/mnsc.12.5.391
• R. J. Hillestad and M. J. Carrillo, Models and techniques for recoverable item stockage when demand and the repair processes are nonstationary — Part I: Performance measurement, Report N-1482-AF, RAND Corporation, 1980.
• G. B. Crawford, Palm's theorem for nonstationary processes, Report R-2750-RC, RAND Corporation, 1981.
• M. J. Carrillo, Generalizations of Palm's theorem and Dyna-METRIC's demand and pipeline variability, Report R-3698-AF, RAND Corporation, 1989.

Motivation

The solution concept of von Neumann and Morgenstern — today usually called a stable set — was the first general answer to the question of what a rational outcome of a many-player cooperative game should be. It was introduced in Theory of Games and Economic Behavior (1944), and Chapter VI of that book states it exactly (§30) and then tests it on the smallest nontrivial case: the essential zero-sum three-person game (§32). The complete determination of all solutions of that game, (32:A)–(32:B) on p. 288, is the book's first full answer to "what are all the solutions of a given game?", and it is the result that made visible the two features every later discussion of stable sets has had to address: a game can have many solutions, and a solution can be an infinite set of imputations that discriminates against one player.

Stable sets remain an active topic in cooperative game theory: Lucas (1968) showed that some games have no stable set, and the literature on existence, uniqueness and structure (for example Shapley 1971 on convex games, whose core is the unique stable set) builds on the definitions formalized here.

Setting

A zero-sum $n$-person game with players $I = \{1, \dots, n\}$ is described by its characteristic function $v(S)$, a real number for each set $S \subseteq I$ of players, satisfying (25:3:a)–(25:3:c):

$$v(\ominus) = 0,\qquad v(-S) = -v(S),\qquad v(S \cup T) \geqq v(S) + v(T)\ \text{ for } S \cap T = \ominus .$$

An imputation is a vector $\vec\alpha = \{\alpha_1, \dots, \alpha_n\}$ with $\alpha_i \geqq v((i))$ for each player and $\sum_i \alpha_i = 0$ (30:1), (30:2). A set $S$ is effective for $\vec\alpha$ if $\sum_{i \in S} \alpha_i \leqq v(S)$ (30:3). An imputation $\vec\alpha$ dominates $\vec\beta$, $\vec\alpha \succ \vec\beta$, if some nonempty set $S$ is effective for $\vec\alpha$ and $\alpha_i > \beta_i$ for all $i \in S$ (30:4). A solution is a set $V$ of imputations such that no element of $V$ dominates another element of $V$ (30:5:a) and every imputation outside $V$ is dominated by some element of $V$ (30:5:b).

Two characteristic functions $v, v'$ are strategically equivalent if $v'(S) = v(S) + \sum_{k\in S}\alpha^0_k$ for constants with $\sum_k \alpha^0_k = 0$ (27:1), (27:2). Every $v$ is strategically equivalent to exactly one reduced function $\bar v$ (27:A); the game is inessential if $\bar v \equiv 0$ and essential otherwise (27.3).

For three players, an essential game in reduced form with the unit chosen so that $\gamma = 1$ has

$$\text{(32:1)}\qquad v(S) = 0,\ -1,\ 1,\ 0 \quad\text{when } S \text{ has } 0, 1, 2, 3 \text{ elements},$$

and its imputations are the points of the fundamental triangle $\alpha_1, \alpha_2, \alpha_3 \geqq -1$, $\alpha_1 + \alpha_2 + \alpha_3 = 0$.

Formalization targets

Goal: the complete list of solutions, (32:A) + (32:B)

For the game (32:1), a set $V$ is a solution if and only if either

$$V = \bigl\{\{-1, \tfrac12, \tfrac12\},\ \{\tfrac12, -1, \tfrac12\},\ \{\tfrac12, \tfrac12, -1\}\bigr\}\qquad\text{(32:6), (32:B)}$$

or, for some player $i$ and some $c$ with

$$-1 \leqq c < \tfrac12 \qquad\text{(32:8)},$$

$V$ is the set of all imputations with $\alpha_i = c$ ((32:7), (32:7*), (32:7**), (32:A)). Both directions are part of the goal.

Milestones

For general $n$ (§31): domination is irreflexive (31:K); an inessential game has exactly one imputation and an essential game infinitely many (31:I); solutions are never empty (31:J); in an essential game every imputation is dominated by one it does not dominate (31:L); an undominated imputation exists iff the game is inessential (31:M); a one-element solution exists iff the game is inessential, and it is then the only solution (31:P); strategic equivalence induces an isomorphism of imputations, effective sets, domination and solutions (31:Q).

For the three-person game (§32): domination is the coordinate condition (32:4) on two of the three players; two mutually undominated imputations agree in one coordinate (32:5); the set (32:6) is a solution (32:B); every set (32:7) with $c$ in the range (32:8) is a solution (32:A).

Significance

The goal is the first complete classification of the stable sets of a game. It shows that solutions are not unique and need not be finite: next to the symmetric three-point solution there is a one-parameter family, for each of the three players, of solutions that fix that player's payoff at $c$ and let the other two bargain freely. The book's interpretation of these "discriminatory" solutions (§33) as standards of behaviour is one of the lasting ideas of the theory. The general-$n$ results of §31 fix the trivial case completely: an inessential game has a unique, one-point solution, so every essential game has only solutions with at least two elements and an empty core. (31:Q) justifies working with reduced forms throughout the later chapters.

The results are proved in the book; none has a machine-checked proof on the platform as of this writing. The existing stable-set definitions on the platform concern feasible payoff vectors $a(N) \leqq v(N)$ of a superadditive game, not imputations of a zero-sum game, so this mission also provides the book's definitions in the form every later chapter of the series (decomposition, simple games, general games) uses.

Difficulty

The "if" direction of the goal is a finite case analysis per set, but (30:5:b) must be checked for every imputation outside the set, with the dominating element chosen as a function of it. The "only if" direction is the substance: from an arbitrary solution — a possibly infinite, a priori unstructured subset of the triangle — one must derive that it is exactly one of the listed sets. The book's argument is geometric (Figures 54–60) and leans on pictures of dominated regions; the delicate points are the exclusion of the limiting position $c = \tfrac12$, where a single point of the triangle stays undominated, and the proof that a solution with two points on a horizontal line and one point off it must be exactly (32:6). The endpoint $c = -1$ is included and must be handled; the endpoint $c = \tfrac12$ is excluded and must be refuted.

Formalization scope

Players are Fin n (the book's player $i$ is index $i-1$; for three players $1, 2, 3$ are 0, 1, 2), coalitions are Finset (Fin n), characteristic functions are Finset (Fin n) → ℝ, imputations are vectors Fin n → ℝ. The domination relation is defined on all vectors but every statement restricts it to imputations; solutions are sets of imputations and (30:5:b) quantifies over imputations only.

Standing hypotheses instantiated in the statements:

• every general-$n$ result of §31 assumes that $v$ satisfies (25:3:a)–(25:3:c) (IsCharFunction v), the book's standing assumption for "a zero-sum $n$-person game";
• "inessential" is the book's definition (reduced form identically $0$, 27.3.1), not the criterion (27:B); "essential" is its negation;
• the three-person results are stated for the reduced form (32:1) with $\gamma = 1$ exactly, as in §32; the transfer to arbitrary essential three-person games via (31:Q) and the choice of unit is not part of the goal;
• the range of $c$ is the half-open interval (32:8).

Domination requires all three clauses of (30:4): dropping "$S$ not empty" makes every imputation dominate every other through $S = \ominus$ and turns the goal into a statement about the empty solution; the definitions keep all three. The general-$n$ statements carry the characteristic-function hypotheses because without them a set function with no imputation has the empty set as a vacuous solution.

The dimension claim "an $(n-1)$-dimensional continuum" in (31:I) is not formalized; only "infinitely many imputations" is. Contributions welcome: proofs of the milestones, a proof of the transfer of the goal to all essential three-person games through (31:Q), and reusable lemmas on domination via two-element coalitions.

Selected references

• J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd edition, 1953), §§25–27, 30–32. https://doi.org/10.1515/9781400829460
• W. F. Lucas, A game with no solution, Bulletin of the American Mathematical Society 74 (1968), 237–239. https://doi.org/10.1090/S0002-9904-1968-11901-9
• L. S. Shapley, Cores of convex games, International Journal of Game Theory 1 (1971), 11–26. https://doi.org/10.1007/BF01753431

Motivation

Average cost Markov decision chains model systems that run indefinitely and are judged by their long-run cost per step: admission and routing control in queues, inventory replenishment, machine maintenance. For a finite state space the classical tool is the average cost optimality equation (ACOE)

$$J + h(i) = \min_{a \in A_i}\Big\{C(i,a) + \sum_j P_{ij}(a)\,h(j)\Big\},$$

whose solution gives both the minimum average cost $J$ and an optimal stationary policy. To be useful the equation has to be solved numerically, and the method used in practice is value iteration: compute the minimum $n$-horizon costs $v_n$ and extract $J$ and $h$ from their growth. This mission formalizes Sections 6.4–6.6 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037): when the minimum average cost is constant, the ACOE holds, any solution of it is optimal, and value iteration converges, provided the optimal policies are aperiodic. When they are not, a transformation of the model makes them so.

Related classical work includes Blackwell's discrete dynamic programming (1962) and Schweitzer–Federgruen's analysis of undiscounted value iteration (1977); Sennott's treatment derives the ACOE from the discounted value function $V_\alpha$ as $\alpha \to 1^-$, which is the route that extends to countable state spaces in later chapters of the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a finite state space $S$; in each state $i$ a finite nonempty action set $A_i$; nonnegative costs $C(i,a)$; and transition probabilities $P_{ij}(a)$. A policy $\theta$ may use the whole history and randomize; a stationary policy $e$ always chooses $e(i) \in A_i$ in state $i$ and induces a Markov chain with transitions $P_{ij}(e) = P_{ij}(e(i))$.

For a policy $\theta$ and initial state $i$: $v_{\theta,n}(i)$ is the expected cost of the first $n$ steps, $V_{\theta,\alpha}(i)$ the expected $\alpha$-discounted cost, and $J_\theta(i) = \limsup_n v_{\theta,n}(i)/n$ the average cost. The value functions are the infima over all policies: $v_n$, $V_\alpha$ and the minimum average cost $J(i)$. A policy is average cost optimal if $J_\theta \equiv J$.

Section 6.2 of the book provides a stationary policy $f$ that is $\alpha$ discount optimal for all $\alpha$ close to $1$ (a Blackwell optimal policy), and Section 6.3 builds from it a relative value function $w^*$. For a distinguished state $z$ put

$$h_\alpha(i) = V_\alpha(i) - V_\alpha(z), \qquad h(i) = \lim_{\alpha\to1^-} h_\alpha(i), \qquad d_n(i) = h(i) + nJ - v_n(i).$$

For a distinguished state $x$ the finite horizon relative value function is $r_n(i) = v_n(i) - v_n(x)$.

A positive recurrent class $R$ of a Markov chain is aperiodic if $P^{(n)}_{ij} \to \pi_j$ for $i, j \in R$, where $\pi$ is the steady state distribution. Assumption OPA ("optimal policies are aperiodic") requires every positive recurrent class of every average cost optimal stationary policy to be aperiodic. The aperiodicity transformation $\Delta^*$ with $0<\tau<1$ keeps states and actions, scales costs by $\tau$, and sets $P^*_{ij}(a) = \tau P_{ij}(a)$ for $j \ne i$, $P^*_{ii}(a) = \tau P_{ii}(a) + (1-\tau)$.

Formalization targets

Goal: convergence of value iteration (Proposition 6.6.3)

If $J(i) \equiv J$ and Assumption OPA holds, then for any distinguished state $x$

$$\lim_{n\to\infty}[v_n(x) - v_{n-1}(x)] = J, \qquad \lim_{n\to\infty} r_n(i) =: r(i) \text{ exists},$$

$(J, r)$ solves the ACOE, and every limit point of the finite horizon optimal stationary policies is average cost optimal.

Milestones

1. Proposition 6.4.1: unichain structure, bounded $|V_\alpha(i) - V_\alpha(z)|$, or pairwise reachability imply $J(i) \equiv J$, with the implication diagram (6.26).
2. Theorem 6.4.2: under $J(i) \equiv J$, $h$ exists, solves the ACOE (6.31), yields optimal policies, $|d_n| \le L$ and $v_n/n \to J$.
3. Proposition 6.5.1: any finite solution $(F, r)$ of the ACOE (or of the inequality (6.36)) gives $J \equiv F$ and optimal policies, and differs from $h$ by constants on recurrent classes.
4. Lemma 6.6.2: on an aperiodic positive recurrent class of an optimal policy, $d_n$ converges to a constant.
5. Lemma 6.6.5 and Proposition 6.6.6: $\Delta^*$ has the same recurrent classes and steady states, all of them aperiodic, costs scaled by $\tau$; value iteration on $\Delta^*$ produces a solution $(J^*/\tau, r^*)$ of the ACOE of $\Delta$.

Significance

The ACOE with constant $J$ is the standard certificate of optimality for finite average cost models, and Proposition 6.5.1 is what allows any numerical solution of it to be trusted. Proposition 6.6.3 is the correctness theorem of the value iteration algorithm (VIA 6.6.4 of the book), and Proposition 6.6.6 removes its one extra hypothesis at the price of a model transformation. Chapter 8 of the book runs this algorithm on a sequence of finite truncations to compute optimal policies for countable-state queueing models, so these results are the base of the book's computational method.

All results in this mission are proved in the book; none has a machine-checked proof. Existing formalizations on the platform treat average reward models under a unichain hypothesis with a single action set type; this mission assumes only a constant minimum average cost (multichain models allowed) and uses the general policy class throughout.

Difficulty

The ACOE itself is not the obstacle; convergence of $v_n(x) - v_{n-1}(x)$ is. Theorem 6.4.2 bounds $d_n$ but does not make it converge, and Example 6.6.1 of the book (a two-state periodic chain) shows that without aperiodicity $v_n(x) - v_{n-1}(x)$ oscillates. The naive argument, passing to the limit in the finite horizon optimality equation, assumes the limits exist, which is exactly what is in question. Chain structure is the obstruction: a multichain optimal policy has several recurrent classes, and the Cesàro-type convergence that suffices for the ACOE itself is weaker than the pointwise convergence value iteration needs. The policy statement is also delicate, since the finite horizon minimizers $f_n$ need not converge.

Formalization scope

• The state type S is finite ([Fintype S]); actions are a type Act with per-state nonempty Finset action sets. Costs are in ℝ≥0, transition probabilities in ℝ≥0∞, and all value functions are defined in [0,∞] as infima over all history-dependent randomized policies, then converted to ℝ (they are finite for finite $S$).
• $J$ constant is stated as $J(i) = J$ for all $i$, with $J \in \mathbb R_{\ge 0}$. The relative value $h$ is defined as the limit $\alpha \to 1^-$ of $h_\alpha$, not taken as an arbitrary solution of the ACOE; Theorem 6.4.2(i) asserts the limit exists. The Blackwell optimal policy $f$ enters as a hypothesis: any stationary policy discount optimal on an interval $(\alpha_0,1)$.
• min_a is Finset.inf' over $A_i$. Limit points of policy sequences follow Definition B.1 (a subsequence agreeing eventually in every state). Finite horizon optimal policies $f_n$ are any minimizers of $v_n(i) = \min_a\{C(i,a) + \sum_j P_{ij}(a) v_{n-1}(j)\}$.
• Aperiodicity of a class is the book's definition ($P^{(n)}_{ij} \to \pi_j$ on the class), with $\pi_j = 1/m_{jj}$. Assumption OPA quantifies over average cost optimal stationary policies only, not over all stationary policies.
• A trivializing formalization is ruled out: $h$, $r_n$, $d_n$ and $v_n$ are computed from the model, not free functions constrained by the ACOE, and the ACOE conclusions are equalities of real numbers with the minimum over the actual action sets.
• The model, criteria and Markov chain definitions restate those of mission IV of this series in their own namespace; they are reusable for any finite average cost result. Contributions of general Markov chain facts (convergence of $P^{(n)}$ on aperiodic classes, Cesàro limits $\frac1n\sum_t P^{(t)}$) are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, Wiley, 1999. https://doi.org/10.1002/9780470317037
• D. Blackwell, Discrete dynamic programming, Annals of Mathematical Statistics 33 (1962), 719–726. https://doi.org/10.1214/aoms/1177704593
• P. J. Schweitzer and A. Federgruen, The asymptotic behavior of undiscounted value iteration in Markov decision problems, Mathematics of Operations Research 2 (1977), 360–381. https://doi.org/10.1287/moor.2.4.360
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887