Markov Chain

Linear programming for Markov decision problems

A Markov decision problem asks how to control a system that moves at random between finitely many states, where each decision changes the probabilities of the next move and incurs a cost. Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (Management Science 9(1):16–24) treats two criteria: the long-run average cost per period, and the total cost of driving the system into an absorbing state. Its Theorem 2 shows that, once attention is restricted to stationary procedures, each problem can be solved as a linear program over the state-action frequencies of the procedure. This mission formalizes that theorem, its supporting displays (3)–(10) and its Lemma on linear-fractional programs.

The linear programming formulation is now the standard computational and theoretical tool for constrained Markov decision processes, and its variables, the occupation measures, are the objects of most later work on that topic. Derman's paper is among the first to state it for the average-cost criterion. Manne (Linear Programming and Sequential Decisions, Management Science, 1960) gave an earlier average-cost formulation for an inventory model. The reduction of a ratio of linear functions to a linear program in Derman's Lemma is the transformation published in the same year by Charnes and Cooper (Programming with Linear Fractional Functionals, Naval Research Logistics Quarterly, 1962).

Setting

There are finitely many states $0, \dots, L$ and decisions $d_1, \dots, d_K$, all available in every state. Making decision $d_k$ in state $i$ sends the system to state $j$ with probability $q_{ij}(k) \ge 0$, where $\sum_j q_{ij}(k) = 1$, and costs $w_{ik}$.

A procedure of class $C'$ is stationary randomized: in state $i$ it makes decision $d_k$ with probability $D_{ik}$, where $D_{ik} \ge 0$ and $\sum_k D_{ik} = 1$, independently of the past and of the time. Under such a procedure the states form a Markov chain with transition probabilities $p_{ij} = \sum_k q_{ij}(k) D_{ik}$. Write $W_t$ for the expected cost at time $t$ when $X_0 = i$.

• Problem 1 (average cost): minimize $Q_R(i) = \limsup_{T\to\infty} \frac{1}{T}\sum_{t=0}^{T} W_t$. Here $w_{ik} > 0$, and Assumption A says that under every procedure of $C'$ all states belong to one class.
• Problem 2 (total cost): the state $L$ is absorbing under every decision and $w_{Lk} = 0$. Minimize $S_R(i) = \sum_{t=0}^{\infty} W_t$, the expected cost of reaching $L$. Assumption B says that under every procedure of $C'$, $L$ is reached from every state with probability one.

The state-action frequencies of a procedure $D \in C'$ with stationary distribution $\pi$ are $x_{jk} = \pi_j D_{jk}$. They satisfy the linear constraints

$$\text{(10)}\qquad x_{jk} \ge 0,\qquad \sum_k x_{jk} - \sum_{i}\sum_k x_{ik}\, q_{ij}(k) = 0 \ \ (j),\qquad \sum_j\sum_k x_{jk} = 1 .$$

For Problem 2, Derman adjoins a state $-1$ that restarts the chain uniformly on $0, \dots, L$ and is entered from $L$. The expected total cost then becomes a ratio of two linear functions of the frequencies of this augmented chain, (9).

Formalization targets

Goal: Theorem 2, pinned-down reading

The printed statement, "If Assumption A (B) holds, then problem 1 (2) can be formulated as a linear programming problem", is not a mathematical statement as it stands. The goal is the reading established by its proof (pp. 20–23).

Under Assumption A with $w > 0$, the program

$$\min \ \sum_{j,k} x_{jk} w_{jk} \quad \text{subject to (10)}$$

has an optimal solution. For every optimal $x^*$, every row sum $\sum_k x^*_{jk}$ is positive, and $D^*_{jk} = x^*_{jk}/\sum_k x^*_{jk}$ satisfies $Q_{D^*}(i) \le Q_D(i)$ for all $D \in C'$ and all $i$.

Under Assumption B with the Problem 2 costs, the linear program obtained from (9) by the Lemma's transformation, $\min \sum w_{jk} z_{jk}$ subject to (12), has an optimal solution. For every optimal $(z^*, z^*_{n+1})$ one has $z^*_{n+1} > 0$, and the procedure decoded from $x^* = z^*/z^*_{n+1}$ satisfies $S_{D^*}(i) \le S_D(i)$ for all $D \in C'$ and all $i$.

Milestones

In the order the proof uses them: the Cesàro limit and the unique positive stationary distribution of a one-class chain ((3), (5)); the taboo-probability identity (4); the formula (6) for $Q_R$; the cycle formula (7) for the averaged total cost; the remark that minimizing the average of the $S_R(i)$ minimizes each one; the correspondence between $C'$ and the solutions of (10); and the Lemma reducing a linear-fractional program under conditions (i) and (ii) to the linear program (12).

Significance

The theorem replaces a search over infinitely many randomized procedures by a single finite linear program. It also yields the structural fact that an optimal stationary procedure can be read off from any optimal solution. The variables $x_{jk}$ make constraints on long-run frequencies of actions expressible as linear constraints. That is the origin of the theory of constrained Markov decision processes, and of the dual linear programs whose variables are value functions. The Lemma is the classical linear-fractional reduction, used well beyond this setting.

All of these results are proved in the paper and in later textbooks (for example Puterman, Markov Decision Processes, 1994, §8.8 and §9.5). None of them has been formalized: Mathlib has Perron–Frobenius-type facts for irreducible matrices but no linear programming theory, no taboo probabilities and no Markov decision model. The mission produces machine-checked versions of the proof's chain of equalities and of the decoding step, written so that they can be reused for occupation-measure arguments.

Difficulty

Several steps fail in the naive argument. The correspondence between procedures and solutions of (10) needs every row sum $\sum_k x_{jk}$ to be positive. That uses Assumption A for a procedure obtained by completing the decoded rows arbitrarily, together with the uniqueness and positivity of the stationary distribution. Positivity of the stationary vector of an irreducible but possibly periodic chain, and the Cesàro (not ordinary) convergence of $P^t$, have no ready-made form in Mathlib. The total-cost identity (7) needs the regenerative identity (4), whose sums must first be shown to converge, and needs the augmented chain to be irreducible, which follows from Assumption B but is not assumed. Problem 2 needs one more step: a minimizer of the averaged total cost is optimal from every starting state, which uses the finiteness of all $S_R(i)$.

Formalization scope

States and decisions are finite Lean types S and Act. Probabilities and costs are real numbers, a procedure of $C'$ is a nonnegative real matrix with unit row sums, and the chain is chainMatrix q D. Assumption A is irreducibility (Matrix.IsIrreducible) of every such chain matrix. Assumption B is reachability of $L$ from every state; for a finite chain in which $L$ is absorbing, this is equivalent to absorption with probability one. $Q_R(i)$ is a real limsup of a bounded sequence, with the paper's sum over $t = 0, \dots, T$. $S_R(i)$ takes values in $[0, \infty]$. The paper requires $w_{ik} > 0$ on p. 17 and $w_{Lk} = 0$ in Problem 2. The formalization uses $w_{ik} > 0$ for $i \ne L$ in Problem 2, and keeps the two problems as separate implications. The adjoined state $-1$ is none : Option S, with the transition law that produces Derman's $p_{-1,i} = 1/(L+1)$, $p_{L,-1} = 1$ for every procedure. The published JewellMRP.InfiniteStep definitions of an ergodic matrix and of a stationary vector are reused.

The goal states optimality of the decoded procedure against every competitor in $C'$, for every optimal solution of the linear program, with existence of an optimal solution as a separate clause. A statement that only identifies feasible sets, or that only asserts that some optimal procedure exists, does not count as Theorem 2. Optimality over all history-dependent procedures is Theorem 1, a separate mission of this series.

Welcome contributions: the stationary-distribution facts for irreducible finite stochastic matrices (reusable across Markov chain work), a small linear-programming existence lemma (a linear function attains its minimum on a nonempty compact polytope), and the Lemma's transformation, which is self-contained.

Selected references

• C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• A. Charnes and W. W. Cooper, Programming with Linear Fractional Functionals, Naval Research Logistics Quarterly 9(3–4):181–186, 1962. https://doi.org/10.1002/nav.3800090303
• K. L. Chung, Markov Chains with Stationary Transition Probabilities, Springer, 1960. https://doi.org/10.1007/978-3-642-49686-8
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Why restrict to stationary procedures

A Markov decision process with finitely many states and decisions is the basic model of sequential decision making under uncertainty: inventory replacement, machine maintenance, queue control and pursuit problems all fit it. Its computational methods (Howard's policy iteration, 1960; Manne's linear programming formulation, 1960) search only over stationary procedures, which use the same decision every time the system is in the same state. A controller, however, may also remember the whole past and randomize. Whether such procedures can do better is a genuine question: as Derman puts it, "a proof is required before a procedure optimal over $C'$ can be considered as the optimal procedure."

Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (Management Science 9(1):16–24) answers it for two criteria, the long-run average cost and the total cost until absorption, by showing that a deterministic stationary procedure is optimal against all procedures. This mission formalizes that theorem, Theorem 1, together with the steps of its proof.

Timeline. Karlin (1955) gives the existence of a discount-optimal procedure used here; Howard (1960) and Manne (1960) solve the average-cost problem over stationary procedures; Wagner (1960) shows by linear programming that an optimal average-cost procedure can be taken deterministic and stationary; Derman (1962) proves the reduction for both criteria by the functional equation approach; Blackwell (1962) strengthens the discounted side to procedures optimal for all discount factors close to $1$.

Setting

The system is observed at times $t = 0, 1, \dots$ in one of finitely many states $0, \dots, L$. After each observation one of $K$ decisions $d_1, \dots, d_K$ is made; every decision is available in every state. If the system is in state $i$ and decision $d_k$ is made, it moves to state $j$ with probability $q_{ij}(k) \ge 0$, where $\sum_j q_{ij}(k) = 1$, and a cost $w_{ik}$ is incurred.

A procedure $R$ chooses decision $d_k$ at time $t$ with probability $D_k(X_0, \Delta_0, \dots, X_t)$, which may depend on the whole history of states $X_s$ and decisions $\Delta_s$. The class of all procedures is $C$. The class $C'$ consists of the stationary randomized procedures, for which this probability is a number $D_{ik}$ depending only on the current state $i$. The class $C''$ consists of the deterministic stationary procedures, those of $C'$ with $D_{ik} \in \{0, 1\}$, that is, maps $f$ from states to decisions; $C''$ is finite.

Started from $X_0 = i$, a procedure $R$ incurs the expected cost $W_t$ at time $t$. The criteria are

$$Q_R(i) = \limsup_{T \to \infty} \frac1T \sum_{t=0}^{T} W_t \quad\text{(Problem 1)}, \qquad S_R(i) = \sum_{t=0}^{\infty} W_t \in [0, \infty] \quad\text{(Problem 2)},$$

and, for a discount factor $0 < \alpha < 1$, the auxiliary discounted cost $V_R(i, \alpha) = \sum_{t \ge 0} \alpha^t W_t$. Problem 1 assumes $w_{ik} > 0$. Problem 2 assumes that state $L$ is absorbing under every decision and that $w_{Lk} = 0$, so $S_R(i)$ is the expected cost of driving the system from $i$ into $L$.

Formalization targets

Goal: Theorem 1

There are procedures $R_1, R_2 \in C''$ such that, for every state $i$,

$$Q_{R_1}(i) = \min_{R \in C} Q_R(i) \quad\text{(Problem 1)}, \qquad S_{R_2}(i) = \min_{R \in C} S_R(i) \ \ (\text{possibly } \infty) \quad\text{(Problem 2)}.$$

One procedure serves every initial state, and the minimum is over all of $C$.

Milestones, in the order of the proof

1. The functional equation: $V_i = \min_{R \in C} V_R(i, \alpha)$ satisfies $V_i = \min_{D_i} \sum_k D_{ik}\,(w_{ik} + \alpha \sum_j q_{ij}(k) V_j)$, the minimum over randomizations $D_i$ being attained.
2. For each $\alpha \in (0,1)$ some $R_\alpha \in C''$ minimizes $V_R(i, \alpha)$ over $C$.
3. One $R^* \in C''$ is $\alpha_v$-discount optimal along a sequence $\alpha_v \to 1$.
4. $\lim_{v} (1 - \alpha_v) V_{R^*}(i, \alpha_v) = Q_{R^*}(i)$ for a stationary $R^*$ (published).
5. The Abelian inequality $Q_R(i) \ge \limsup_{\alpha \to 1^-} (1 - \alpha) V_R(i, \alpha)$ for every $R \in C$ (published).
6. Theorem 1 (1) itself (published, as part of Sennott's Proposition 6.2.3).
7. $S_R(i) = \lim_{\alpha \to 1^-} V_R(i, \alpha)$ for every $R \in C$, finite or not.

Significance

Theorem 1 is what makes finite optimization possible for these problems: once $C''$ is known to contain an optimal procedure, the search runs over finitely many maps, and the linear programs of the paper's §3 (the next mission of this series) and of Manne describe the whole problem rather than a restriction of it. Part (2) is a total-cost result without any assumption that the absorbing state is reached; it holds even when every procedure has infinite cost from some state, which separates it from the stochastic shortest path theory that assumes properness.

Part (1) is available on the platform as part of Sennott's Proposition 6.2.3 (stated there, not yet proved), and it is referenced here rather than restated. Part (2), the functional equation for history-dependent procedures and the Abel-limit identity for the total cost have no statement on the platform; to our knowledge none has a machine-checked proof.

Difficulty

The obvious argument compares an arbitrary procedure with stationary ones state by state, but a history-dependent randomized procedure does not induce a Markov chain, so no transition matrix is available for it. The comparison has to pass through the discounted problem, where an optimal stationary procedure exists for each $\alpha$, and then let $\alpha \to 1$. Two limit exchanges are needed: for the average cost, an Abelian inequality valid for every procedure plus a Markov chain limit theorem for the stationary one; for the total cost, monotone convergence in $[0, \infty]$, which must work when the limit is infinite. The discount-optimal procedure depends on $\alpha$, and the finiteness of $C''$ is what yields a single procedure along a sequence $\alpha_v \to 1$.

Formalization scope

The model is the published SennottDP.AvgFinite.Model (a Markov decision chain with finite action sets, nonnegative costs in $\mathbb R_{\ge 0}$ and transition probabilities in $[0, \infty]$) with finite nonempty types of states and decisions and every action set equal to the whole decision type. Derman's class $C$ is its Policy (history-dependent, randomized); $C''$ is StationaryPolicy. $W_t$ is expCost, $V_R(i, \alpha)$ is discCost, and $Q_R(i)$ is avgCost $= \limsup_n \frac1n \sum_{t<n} W_t$, which has the same value as Derman's normalization because $W_t$ is bounded. $S_R(i)$ is a new definition, a sum in $[0, \infty]$. Every discount factor is restricted to $(0, 1)$ explicitly. "Minimum over $C$" is stated as an inequality against every policy, with the optimal procedure chosen before the initial state.

Problems 1 and 2 enter as separate implications with their own cost hypotheses; the page's "$w_{ik} > 0$" is read as $w_{ik} > 0$ for $i \ne L$ in Problem 2, since $w_{Lk} = 0$ there. A formalization that compares only against stationary procedures, or that states the total cost as a real series (whose divergent values default to $0$), is ruled out: the competitors are all policies and $S_R(i)$ lives in $[0, \infty]$.

A complete development needs the discounted Bellman equation for history-dependent policies, the selection of a deterministic minimizer, and Abelian theorems for nonnegative series. These are reusable across the platform's dynamic programming missions, and proofs of the referenced Sennott propositions are welcome contributions in their own right.

Selected references

• C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
• S. Karlin, The Structure of Dynamic Programming Models, Naval Research Logistics Quarterly 2(4):285–294, 1955. https://doi.org/10.1002/nav.3800020408
• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• H. M. Wagner, On the Optimality of Pure Strategies, Management Science 6(3):268–269, 1960. https://doi.org/10.1287/mnsc.6.3.268
• D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Propositions 6.1.1, 6.2.2, 6.2.3. https://doi.org/10.1002/9780470317037

Motivation

Average cost control of queues rests on a small amount of Markov chain theory: when does a chain with costs have a well defined long-run average cost, and how can that be checked for a concrete model with an unbounded state space? Appendix C of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037) collects this material for countable state spaces and packages it in one hypothesis, the $z$ standard chain. Chapters 7–10 of the book verify this hypothesis for the Markov chains induced by stationary policies in admission, routing and service-rate control models, and use its consequences to prove existence of average cost optimal policies.

The tools are Lyapunov functions in the sense of Foster (1953): a nonnegative function on the states whose expected one-step change is negative away from a finite set. Foster's criterion for positive recurrence, and its refinements bounding expected first passage times and costs, are the standard way to verify stability of queueing networks (Meyn and Tweedie, Markov Chains and Stochastic Stability, 1993/2009).

Setting

A Markov chain $\Gamma$ on a countable set $S$ is given by transition probabilities $P_{ij}\ge 0$ with $\sum_j P_{ij}=1$. $X_t$ is the state at time $t$ and $P^{(t)}_{ij}$ the $t$-step transition probability ($P^{(0)}_{ij}=\delta_{ij}$). State $i$ leads to $j$ if $P^{(t)}_{ij}>0$ for some $t\ge0$; states that lead to each other communicate, which partitions $S$ into communicating classes.

For a nonempty $G\subseteq S$ the first passage time from $i$ is $T_{iG}=\min\{t\ge1: X_t\in G\}$ given $X_0=i$, and $m_{iG}=E[T_{iG}]\in[0,\infty]$; $m_{ij}$ is the case $G=\{j\}$ and $m_{ii}$ the expected return time. The taboo probability $_G P^{(t)}_{ik}$ is the probability of going from $i$ to $k$ in $t$ steps without visiting $G$ at the intermediate times, and $_G u_{ik}$ is the expected number of visits to $k$ at times $0\le t<T_{iG}$. A state is transient if $P(T_{ii}<\infty)<1$ and positive recurrent if $m_{ii}<\infty$; a positive recurrent class is a communicating class of positive recurrent states. The steady state probability is $\pi_j=(m_{jj})^{-1}$ (zero when $m_{jj}=\infty$).

Each state carries a finite cost $C(i)\ge0$. The expected average cost over $[0,n-1]$ from $i$ is

$$J^{(n)}_i=\frac1n\,E\Big[\sum_{t=0}^{n-1}C(X_t)\,\Big|\,X_0=i\Big]=\frac1n\sum_{t=0}^{n-1}\sum_j P^{(t)}_{ij}C(j),$$

$c_{iG}$ is the expected cost $E[\sum_{t=0}^{T_{iG}-1}C(X_t)\mid X_0=i]$ of a first passage (defined when $m_{iG}<\infty$), and $J_R=\sum_{j\in R}\pi_jC(j)$ is the average cost on a positive recurrent class $R$. The chain is $z$ standard (Definition C.2.5) if for a distinguished state $z$

$$m_{iz}<\infty\quad\text{and}\quad c_{iz}<\infty\qquad\text{for all } i\in S.$$

Formalization targets

Goal: Proposition C.2.6

If $\Gamma$ is $z$ standard, then $S$ is the union of a positive recurrent class $R\ni z$ and a set of transient states, $J_R<\infty$, and

$$\lim_{n\to\infty}J^{(n)}_i=J_R\qquad\text{for every } i\in S.$$

The statement fixes no constants: it asserts that the average cost exists, is finite, and does not depend on the initial state.

Milestones

1. Proposition C.1.2: $\pi$ is the unique stationary distribution of a positive recurrent class, and $\pi_j=e_{ij}/m_{ii}=\pi_ie_{ij}$.
2. Proposition C.1.4: the first-step equations (C.2)–(C.4) for taboo probabilities, visit counts and $m_{iG}$; $\sum_{i\in G}\pi_im_{iG}=1$ for $G$ inside a positive recurrent class; $m_{ij}<\infty$ within such a class.
3. Proposition C.1.5: if $\sum_jP_{ij}[y(j)-y(i)]\le-\epsilon$ off $G$, then $m_{iG}\le y(i)/\epsilon$.
4. Corollary C.1.6: the same with $G=\{z\}$ and $\sum_jP_{zj}y(j)<\infty$ makes $z$ positive recurrent.
5. Proposition C.2.1: on a positive recurrent class, $J^{(n)}_i\to J_R=c_{ii}/m_{ii}$.
6. Proposition C.2.2: $c_{iG}=\sum_kC(k)\,{}_Gu_{ik}$, the first-step equation (C.13), and $J_R=\sum_{i\in G}\pi_ic_{iG}$.
7. Proposition C.2.3 and Corollary C.2.4: the cost drift condition $\sum_jP_{ij}[r(j)-r(i)]\le-C(i)$ off a finite set bounds $c_{iG}\le r(i)+Fm_{iG}$, and gives $c_{zz}<\infty$.
8. Remark C.2.7: the hypotheses of C.1.6 and C.2.4 together imply the chain is $z$ standard; so do irreducibility, positive recurrence and finite average cost.

Significance

Proposition C.2.6 is what makes the $z$ standard hypothesis useful: an average cost criterion that is a genuine limit, finite, and independent of the initial state, even for chains with transient states and unbounded state spaces. Every average cost optimality result of the book that works with a stationary policy's induced chain (the (SEN) and (BOR) assumption sets, the approximating-sequence method, the continuous-time chapter) calls on this proposition or on the Lyapunov criteria of Remark C.2.7 to establish its hypotheses for queueing models.

All results of the mission are classical and proved in the literature; parts are stated in the book without proof and referred to Chung (1967), Grassmann et al. (1985) and renewal theory. None of them has been machine-checked in this form as far as the platform and Mathlib show: Mathlib has kernels and Ionescu-Tulcea trajectories but no countable-state Markov chain classification, no first passage calculus, and no Foster–Lyapunov criterion. Existing platform results on countable chains (the Levin–Peres–Wilmer series) treat irreducible chains without costs. A complete development here produces a reusable library of first passage identities, Foster–Lyapunov bounds for times and costs, and average cost limits on reducible chains.

Difficulty

The Lyapunov bounds (C.1.5, C.2.3) are telescoping arguments, but they require a clean handling of truncated passages and of sums that may be infinite: (C.7) is an inequality between possibly divergent series, and the step "iterate $n$ times and let $n\to\infty$" must be made rigorous for $[0,\infty]$-valued expectations.

The central difficulty is part (iii) of the goal for transient initial states. On the class $R$, the limit of $J^{(n)}_i$ is a renewal reward theorem over successive returns to $z$; from a transient state the first cycle has a different law, so a delayed renewal reward argument is needed, and it has to cover the case where costs are unbounded. The obvious approach, bounding $J^{(n)}_i$ between $J_R$ and the average over the first $n$ steps of the chain started in $z$, fails because $P^{(t)}_{ij}$ need not converge (periodic classes) and because finite $c_{iz}$ does not bound individual cost terms. Proposition C.1.2's uniqueness and the Kac-type identity of C.1.4(iv) likewise need the full cycle decomposition of a positive recurrent class.

Formalization scope

The chain is a structure MC S with P : S → S → ℝ≥0∞ and ∑' j, P i j = 1, over a countable type S; costs are C : S → ℝ≥0. Probabilities and expectations are ℝ≥0∞-valued sums over finite paths Fin (t+1) → S, so every quantity is defined without summability side conditions and may be $\infty$. The first passage time is $T_{iG}\ge1$; $m_{iG}$ is the expectation of $T_{iG}$ from its law (and $\infty$ when $P(T_{iG}<\infty)<1$), not defined by the recursion (C.4), so that (C.4) is a theorem. $_Gu_{ik}$ counts visits at times $0\le t<T_{iG}$. $c_{iG}$ is computed over first passage paths and is used only when $m_{iG}<\infty$, as in the book. $\pi_j$ is $(m_{jj})^{-1}$, which the book states equals the Cesàro limit $\lim_nQ^{(n)}_{jj}$. $J^{(n)}_i$ is meaningful for $n\ge1$, and limits are taken in $[0,\infty]$. The drift conditions $\sum_jP_{ij}[y(j)-y(i)]\le-\epsilon$ and $\sum_jP_{ij}[r(j)-r(i)]\le-C(i)$ are written in the equivalent additive form $\sum_jP_{ij}y(j)+\epsilon\le y(i)$, which is equivalent for finite $y$ and makes the case $\sum_jP_{ij}y(j)=\infty$ fail, as it does in the book.

A trivializing formalization, such as defining $m_{iG}$ or $c_{iG}$ by the equations (C.4) or (C.13), defining $J_R$ as the limit of $J^{(n)}_i$, or allowing a $z$ standard chain whose return time or return cost to $z$ is infinite, is ruled out: $z$ standard requires $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$ including $z$, and each quantity is defined from path probabilities.

Needed infrastructure: path-sum manipulation in $[0,\infty]$ (first-step and last-step decompositions), the ratio limit / renewal reward theorem for a positive recurrent class, and the delayed version for transient starts. The first passage calculus and the Lyapunov bounds are reusable by the book's other chapters on average cost, which state the $z$ standard property for policy-induced chains. Contributions of lemmas on path sums and of an independent renewal reward library are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix C, pp. 292–302. doi:10.1002/9780470317037
• K. L. Chung, Markov Chains with Stationary Transition Probabilities, 2nd ed., Springer, 1967. doi:10.1007/978-3-642-62015-7
• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Annals of Mathematical Statistics 24 (1953), 355–360. doi:10.1214/aoms/1177728976
• S. P. Meyn and R. L. Tweedie, Markov Chains and Stochastic Stability, 2nd ed., Cambridge University Press, 2009. doi:10.1017/CBO9780511626630
• D. P. Heyman and M. J. Sobel, Stochastic Models in Operations Research, Vol. I, McGraw-Hill, 1982.

Motivation

Howard's finite Markovian decision process (MDP) models a controller who, at each instant, observes the state of a system, chooses a decision, collects a reward and moves to a random next state with known transition probabilities. Howard's policy-iteration algorithm computes an optimal policy, and the model has been applied to inventory control, equipment replacement, quality control and marketing. Its weak point is the requirement that every transition probability be known exactly: in applications these numbers are estimated and are hard to measure.

Satia and Lave (Operations Research 21(3), 1973) relax this requirement. In their game-theoretic formulation, the controller knows only a set of admissible probability rows for every state–decision pair, and nature chooses the rows adversarially. This is the model now called a robust MDP with (s,a)-rectangular uncertainty, studied later by Iyengar (Math. Oper. Res. 2005) and Nilim and El Ghaoui (Oper. Res. 2005), who reprove and extend the dynamic-programming results for it. The paper gives a policy-iteration algorithm for the max-min criterion and proves that it terminates at an optimal policy. This mission formalizes that part of the paper (pp. 728–732).

Timeline:

• 1953: Shapley introduces stochastic games (PNAS 39).
• 1960: Howard, Dynamic Programming and Markov Processes, policy iteration for known transitions.
• 1973: Satia and Lave, max-min and max-max policy iteration for uncertain transitions (dynamic-programming equations and optimality of pure stationary policies cited from Satia's 1968 Stanford thesis).
• 2005: Iyengar; Nilim and El Ghaoui, robust dynamic programming under rectangular uncertainty.

Setting

There are finitely many states $i$ and, in state $i$, a finite nonempty set $D_i$ of decisions $k$. A transition $i\to j$ under decision $k$ earns reward $r^k_{ij}$; rewards are discounted by $\beta$ with $0\le\beta<1$. For every pair $(i,k)$ there is a nonempty, closed, convex set $S_i^k$ of probability rows $p=(p_1,\dots,p_N)$, $p_j\ge0$, $\sum_j p_j=1$. Nature's choice is a matrix $P\in S$: one row $p_i^k\in S_i^k$ for every pair.

A pure stationary policy $A=(A_1,\dots,A_N)$ selects $A_i\in D_i$. Under $P$ its present value $v^A(P)$ is the unique solution of equations (5),

$$v_i^A=\sum_j p^{A_i}_{ij}\big(r^{A_i}_{ij}+\beta v_j^A\big).$$

Nature's minimum is $\underline v_i(A)=\inf_{P\in S}v_i^A(P)$, and the max-min return of criterion (2) is $\bar v_i=\max_A\underline v_i(A)$. A policy is max-min optimal if $\underline v(A)=\bar v$ in every state.

The algorithm alternates two routines. Phase 1 (nature's policy evaluation) fixes $A$, computes $v^A$ from the current rows, replaces each row at $A_i$ by a minimizer of $\sum_j p_j(r^{A_i}_{ij}+\beta v^A_j)$ over $S_i^{A_i}$ (6), and stops when the minima reproduce $v^A$. Phase 2 (policy improvement) chooses in each state a decision $B_i$ maximizing the test quantity (7),

$$t_i^k(v)=\min_{p\in S_i^k}\sum_j p_j\big(r^k_{ij}+\beta v_j\big),$$

at $v=\underline v(A)$, keeping $A_i$ on ties; if $B=A$ the algorithm terminates.

Formalization targets

Goal: Proposition 5 with Proposition 3

Along every run $A^0,A^1,\dots$ of Phase 2 steps,

$$\underline v(A^n)\le\underline v(A^{n+1})\ \ \forall n,\qquad \exists\,n<\#\{\text{policies}\}:\ A^{n+1}=A^n,\ \ \underline v(A^n)=\bar v,$$

and the terminal policy attains the solution of the equations (4) and is $\varepsilon$-optimal for every $\varepsilon>0$.

Milestones

• Eq. (5): the present-value equations have a unique solution.
• $[I-\beta P]^{-1}$ is nonnegative with diagonal at least 1 for stochastic $P$ (proof of Proposition 5).
• Proposition 1: equations (4), with randomized decisions and mixed choices of nature, have a unique solution, and it is the max-min return.
• Proposition 2: a pure stationary policy attains it.
• A non-final Phase 1 iteration lowers nature's value weakly everywhere and strictly somewhere (proof of Proposition 4).
• Proposition 4: Phase 1 comes within $\varepsilon$ of nature's optimum after finitely many iterations.
• Proposition 3: at termination no pure stationary policy is better.
• Each policy change strictly improves the max-min return (proof of Proposition 5).

Significance

The goal certifies a complete algorithm for the max-min problem: it computes a policy that is optimal against the worst admissible transition probabilities, in all states at once, in finitely many improvement steps. Propositions 1 and 2 show that the dynamic-programming equations (4) characterize the max-min value and that neither side gains from randomization. The known-transition case (every $S_i^k$ a single row) recovers Howard's policy iteration.

On the platform, Howard-type policy iteration for known transitions has been formalized (the Bertsekas Dynamic Programming and Optimal Control missions); nothing with uncertain transitions exists. The results of this paper are proved in the literature (Satia's thesis, and in greater generality by Iyengar and by Nilim and El Ghaoui); none has a machine-checked proof. This mission produces the first formal robust-MDP model and robust policy-iteration theorem on the platform.

Difficulty

The obvious argument copies Howard's improvement lemma. It fails at two points. First, the value of a policy is itself the result of an inner optimization by nature, so comparing two policies requires comparing two different worst-case transition matrices; the matrix $P^{*B}$ minimizing against $B$ is not the one minimizing against $A$. Second, the proof of Proposition 4 as printed shows only that nature's values decrease and converge; that the limit is nature's optimum, over a continuum of admissible rows, needs a separate argument. Finally, Proposition 1 involves randomized strategies and probability measures on the uncertainty sets, and reducing them to pure strategies is the content of Propositions 1 and 2, not a definitional convenience.

Formalization scope

States are a finite type S (nonemptiness is not needed: every statement is unchanged in meaning at $N=1$ and trivially true at $N=0$), decisions a family D : S → Type* of finite nonempty types. The model fixes these conventions and readings:

• $0\le\beta<1$ (not printed; every return is an infinite discounted sum) and nonempty $S_i^k$ (not printed; Phase 1 presupposes a feasible row) are added standing hypotheses; closedness and convexity are the paper's.
• The present value is $[I-\beta P^A]^{-1}$ applied to the one-step rewards; the Eq. (5) milestone proves it is the unique solution of (5).
• "min over $p_i^k\in S_i^k$" in (2) is an infimum over the nonempty type of admissible choices $P\in S$, bounded below; "max over all policies" is a maximum over pure stationary policies, with randomization handled in (4).
• In (4), $\tau$ ranges over probability vectors on $D_j$ and $\alpha$ over probability measures on row vectors with $\alpha(S_j^k)=1$; the missing integral sign and unmatched brace of the printed display are corrected.
• "Optimal" = equal to the max-min return in every state; "$\varepsilon$-optimal" = within $\pm\varepsilon$ in every state (p. 731); "$\varepsilon$-optimal for nature" = within $\varepsilon$ of nature's minimum.
• "Terminates" = Phase 2 returns the same policy; "a finite number of iterations" is stated with the explicit bound "fewer than the number of policies".
• Phase 1 is taken exact in Phase 2 (the proofs of Propositions 3 and 5 use exact minimizers); the Phase 1 stopping test is printed without $\Sigma$ and the sum is formalized.
• Retention rule: Phase 2 keeps $A_i$ when it is already a maximizer. It is not printed, but it is Howard's rule and Proposition 5 is false without it.
• Proposition 5's "$\varepsilon$-optimal … in a finite number of iterations" is formalized as exact termination at an optimal policy, which implies the printed claim for every $\varepsilon$.

Equation (4) must not be collapsed to $\max_k\min_{p\in S_j^k}$ in its definition: that would make Proposition 2 true by definition. Similarly, the Phase 2 relation always has a successor and algorithm runs exist from every policy, so the goal is not vacuous.

Needed infrastructure: Neumann series for $I-\beta P$ with stochastic $P$, monotonicity of policy evaluation, existence of minimizers of linear functions on compact subsets of the simplex, and the contraction argument for the robust Bellman operator. These are reusable for any robust or known-transition MDP development. Proofs of any milestone, alternative arguments for Propositions 1 and 2, and extensions to the max-max criterion are welcome.

Selected references

• J. K. Satia and R. E. Lave, Jr., Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3), 728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• L. S. Shapley, Stochastic Games, PNAS 39(10), 1095–1100, 1953. https://doi.org/10.1073/pnas.39.10.1095
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2), 257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• A. Nilim and L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5), 780–798, 2005. https://doi.org/10.1287/opre.1050.0216

Motivation

A Markov decision problem models a system that is observed once per period and controlled by choosing an action: the action earns an immediate income and determines the probabilities of the next state. Inventory control, machine replacement, queue admission and many reinforcement-learning benchmarks are of this form. With future income discounted by a factor $\beta<1$, Howard (Dynamic Programming and Markov Processes, 1960) showed how to compute an optimal policy by policy improvement. The undiscounted problem ($\beta=1$) is harder, because total income is typically infinite.

David Blackwell's Discrete Dynamic Programming (Ann. Math. Statist. 33 (1962) 719–726) treats $\beta=1$ as a limit of $\beta<1$. Its Theorem 5 shows that some stationary policy is optimal simultaneously for all discount factors sufficiently close to $1$. Such policies are now called Blackwell optimal, and the result is the base of sensitive discount optimality (Veinott, 1969) and of the standard textbook treatment of average-reward problems (Puterman, Markov Decision Processes, 1994, Ch. 10).

Timeline. Howard (1960): policy iteration for discounted and average-reward finite problems. Blackwell (1962): Theorem 5 (Blackwell optimal stationary policies exist) and the characterization of nearly optimal stationary policies (Theorem 4, the subject of the companion mission). Miller and Veinott (Ann. Math. Statist. 40 (1969) 366–370), Veinott (Ann. Math. Statist. 40 (1969) 1635–1660): Laurent expansions of $V_\beta$ in $1-\beta$ and $n$-discount optimality.

Setting

There are finitely many states $s$ and a finite set $A$ of actions, every action available in every state. In state $s$, action $a$ yields income $i(s,a)\in\mathbb R$ (any sign) and moves the system to state $s'$ with probability $q(s'\mid s,a)$; each $q(\cdot\mid s,a)$ is a probability vector.

A decision rule is a function $f$ from states to actions; $F$ is the finite set of decision rules. A policy is a sequence $\pi=\{f_n,\ n=1,2,\dots\}$ in $F$: on day $n$, in state $s$, action $f_n(s)$ is used. Policies are deterministic and Markov but may change with time. The policy $(f,\pi)$ uses $f$ on day $1$ and then follows $\pi$; $f^{(\infty)}$ uses $f$ every day and is called stationary.

For $f\in F$, $r(f)$ is the vector $(i(s,f(s)))_s$ and $Q(f)$ the Markov matrix $(q(s'\mid s,f(s)))_{s,s'}$. With $Q_0(\pi)=I$ and $Q_n(\pi)=Q(f_1)\cdots Q(f_n)$, the return of $\pi$ at discount factor $0\le\beta<1$ is

$$V_\beta(\pi)=\sum_{n=0}^\infty \beta^n\,Q_n(\pi)\,r(f_{n+1}),$$

a vector indexed by the initial state. Vectors are compared coordinatewise; $w_1>w_2$ means $w_1\ge w_2$ and $w_1\ne w_2$.

A policy $\pi^*$ is $\beta$-optimal if $V_\beta(\pi^*)\ge V_\beta(\pi)$ for every policy $\pi$. Following §4 of the paper, a policy is optimal if it is $\beta$-optimal for all $\beta$ sufficiently near $1$.

Formalization targets

Goal: Theorem 5

There exist a decision rule $f$ and $\beta_0<1$ such that

$$V_\beta(f^{(\infty)})\ \ge\ V_\beta(\pi)\qquad\text{for all }\beta\in(\beta_0,1)\text{ and all policies }\pi.$$

One $f$ and one $\beta_0$ serve every competing policy and every $\beta\in(\beta_0,1)$.

Milestones

1. The composition rule $V_\beta(f,\pi)=L(f)V_\beta(\pi)$, with $L(f)w=r(f)+\beta Q(f)w$, and its $N$-fold version (§2).
2. Theorem 1: if $V_\beta(f,\pi^*)\le V_\beta(\pi^*)$ for all $f\in F$, then $\pi^*$ is $\beta$-optimal.
3. Theorem 2: if $V_\beta(f,\pi)>V_\beta(\pi)$ then $V_\beta(f^{(\infty)})>V_\beta(\pi)$.
4. Theorem 3 (policy improvement): if no action improves $f^{(\infty)}$ by one step, $f^{(\infty)}$ is $\beta$-optimal; otherwise switching to improving actions gives $g^{(\infty)}>f^{(\infty)}$.
5. Corollary: for each fixed $\beta\in[0,1)$ some stationary policy is $\beta$-optimal.
6. Each coordinate of $V_\beta(f^{(\infty)})$ is a rational function of $\beta$ on $[0,1)$ with nonvanishing denominator.
7. Some $f^*$ is $\beta$-optimal for a set of $\beta$'s having $1$ as a limit point.
8. If $V_\beta(f^{*(\infty)})\ge V_\beta(g^{(\infty)})$ for a set of $\beta$'s accumulating at $1$, then it holds for all $\beta$ near $1$.

Significance

The result. Theorem 5 shows that the infinitely many discounted problems near $\beta=1$ share a common optimal stationary policy. Such a policy is also optimal for the long-run average criterion, which settles the existence of average-optimal stationary policies in finite models without any recurrence assumption. It also justifies computing undiscounted solutions as limits of discounted ones, and it is the first case of the sensitive optimality criteria developed later.

Formalizing it. The theorem is classical and proved in the paper and in the textbooks; there is no machine-checked proof of it in Blackwell's model on the platform. A related open item, SennottDP.AvgFinite.prop_6_2_3_blackwell_optimal, states the textbook version for nonnegative costs and randomized history-dependent policies; the present mission is Blackwell's own formulation with incomes of either sign and deterministic Markov policies. A complete development also yields a verified policy improvement theorem (Theorem 3) and the rationality of discounted values in $\beta$, both reusable for any finite-state discounted model.

Difficulty

The Corollary gives, for each $\beta$, some optimal stationary policy, and $F$ is finite, so one $f^*$ is $\beta$-optimal for infinitely many $\beta$ accumulating at $1$. The obvious argument stops there: optimality on a sequence of $\beta$'s says nothing about the $\beta$'s in between, and a pointwise limit argument cannot produce a whole interval $(\beta_0,1)$. The step that fails is passing from "frequently" to "eventually", and it needs structural information about how $V_\beta$ depends on $\beta$, not just continuity. A second difficulty is the comparison class: optimality must hold against all time-dependent policies, not only the finitely many stationary ones, so the final step has to bring the Corollary back in for every $\beta$ near $1$.

Formalization scope

States and actions are finite nonempty Lean types St, Act; decision rules are functions St → Act and policies are sequences ℕ → St → Act, indexed from $0$ (π 0 is Blackwell's $f_1$). Incomes are real-valued with no sign restriction. The law of motion law s a s' $=q(s'\mid s,a)$ satisfies the published predicate IsTransitionKernel. $Q_n(\pi)$ is the ordered matrix product and $V_\beta(\pi)$ is the tsum of the series, which converges absolutely for $0\le\beta<1$; every statement at a fixed $\beta$ assumes $0\le\beta<1$, and nothing is stated for $\beta\ge1$. Vector inequalities are coordinatewise, and the strict order is "$\ge$ and $\ne$", not coordinatewise strict. "$\beta$ sufficiently near $1$" is "there is $\beta_0<1$ such that for every $\beta\in(\beta_0,1)$". The paper's §4 phrase $V_\beta(\pi)=U(\beta)$ is encoded as $\beta$-optimality, so no supremum over policies appears.

The word "optimal" has two meanings in the paper: at one fixed $\beta$ (§3, the Corollary) and for all $\beta$ near $1$ (§4, Theorem 5). The Lean development keeps them apart as IsBetaOptimal β and IsOptimal. A statement of Theorem 5 at a single $\beta$, with "there exists $\beta$", for a set of $\beta$'s accumulating at $1$, or against stationary policies only would be a different and weaker theorem; the goal rules all of these out.

Needed infrastructure: summation and shifting of the discounted series, Neumann series $(I-\beta Q)^{-1}=\sum_n\beta^nQ^n$ for stochastic $Q$, Cramer's rule to express $(I-\beta Q)^{-1}r$ as a ratio of polynomials in $\beta$, and the fact that a nonzero polynomial has finitely many roots. The policy improvement theorem and the rationality lemma are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

• D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• R. A. Howard, Dynamic Programming and Markov Processes, Technology Press and Wiley, 1960.
• A. F. Veinott Jr., Discrete Dynamic Programming with Sensitive Discount Optimality Criteria, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999 (Proposition 6.2.3, Blackwell optimality for finite models). https://doi.org/10.1002/9780470317037

Motivation

A manufacturer that makes one product to stock faces random demand, can produce at most $b$ units per period, and can store at most $U$ units. The classical result without the production limit is that a base-stock policy is optimal: raise inventory to a fixed level $\bar y$ each period. With a production limit, the natural modification is to produce up to $\bar y$ when that is possible and to produce at full capacity otherwise. Federgruen and Zipkin (1986) proved that this modified base-stock (critical-number) policy is optimal under the long-run average-cost criterion, for discrete demand with a general convex cost. Production-capacity models of this type are standard in operations management texts, and the result underlies the computational and comparative-static work that followed, starting with Part II of the same paper, which treats discounted costs.

Timeline.

• 1950s–60s: optimality of base-stock (critical-number) policies for uncapacitated periodic-review models; see Heyman and Sobel's Stochastic Models in Operations Research, Vol. II (1984).
• 1986: Federgruen and Zipkin, Part I (average cost, MOR 11(2):193–207) and Part II (discounted cost, MOR 11(2):208–215) establish the capacitated case. Part I handles the unbounded state space with a general average-cost theory for countable-state Markov decision processes by Federgruen, Schweitzer and Tijms (1983).

Setting

Time is divided into periods $t = 0, 1, \dots$. The demands $D_0, D_1, \dots$ are independent copies of a random variable $D$ with values in $\{0, 1, 2, \dots\}$ and probability mass function $p(j)$; write $\mu = E(D)$ and $P(j) = \Pr\{D \le j\}$. At the start of period $t$ the inventory is an integer $x_t$ (negative values are backorders). The decision maker raises it to

$$y_t \in Y(x_t) = \{y \in \mathbb Z : x_t \le y \le x_t + b,\ y \le U\},$$

pays the expected one-period cost $G(y_t)$, and demand is subtracted: $x_{t+1} = y_t - D_t$. The order cost per unit is set to zero, as in the paper; this loses no generality because every policy with finite average cost has the same average order cost.

The standing assumptions are: $G \ge 0$ is convex and $G(y) \to \infty$ as $|y| \to \infty$ (Assumption 1); the characteristic function of $D$ is analytic at the origin (Assumption 2), and $0 < \mu$; $G(y) \le A + B|y|^\rho$ for some positive integer $\rho$ (Assumption 3); $b > \mu$ and $P(b) < 1$ (Assumption 4). The smallest global minimizer of $G$ is $\bar y^\infty$, and $U \ge \bar y^\infty$.

A Markov policy is a sequence $\pi = (\pi_0, \pi_1, \dots)$ of maps with $\pi_t(x) \in Y(x)$. The critical-number policy with critical number $\bar y$ is $\delta[\bar y](x) = \max(x, \min(\bar y, x + b))$. A stationary policy $\delta$ is strongly optimal with average cost $g$ if, from every initial state $x \le U$, its average cost $t^{-1}E\{\sum_{i<t} G(y_i)\}$ converges to $g$, while every Markov policy has lim-inf average cost at least $g$ from every initial state.

The analysis uses the operators $Rv(y) = G(y) + E\,v(y - D)$ and $Sv(x) = \min_{y \in Y(x)} Rv(y)$, and the optimality equation

$$g + v(x) = Sv(x),\qquad x \le U. \tag{6}$$

For an interval $\iota = [l, u]$, $H_\iota v(x)$ is the largest expected sum of $v(y_t)$, over policies forced to produce at capacity below $l$ and to produce nothing above $u$, until the inventory first returns to $\iota$.

Formalization targets

Goal: Theorem 1 (p. 202)

There exist $g^*$, $v^*$ and $y^* \ge \bar y^\infty$ such that $(g^*, v^*)$ solves (6), $v^*$ is convex with global minimizer $y^*$, and

$$\delta^* = \delta[y^*] \text{ is strongly optimal with average cost } g^*.$$

The $y^*$ in the optimality claim is the minimizer constructed in part (a).

Milestones

• Lemma 2(a)–(c) (pp. 196–197): a normal-tail inequality and two series estimates.
• Lemma 3 (p. 198): if $v(x) = O(|x|^q)$ then $H_\iota v(x) = O(|x|^{q+3})$.
• Corollary 1 (p. 200): $H_\iota 1 = O(|x|^3)$ and $H_\iota G = O(|x|^{\rho+3})$, both finite.
• Corollary 2 (p. 201): $(t+1)^{-1}P[\delta_{0t}]\cdots P[\delta_{tt}](H_\iota 1 + H_\iota G)(x) \to 0$.
• Lemma 4 (p. 201): reachability of every state in $[L, U - D_-]$ under some policy that produces at capacity below $L$.
• Lemma 5 (p. 202): $S$ and $Q$ preserve the class $V$ of convex functions of growth $O(|x|^{\rho+3})$ that are nonincreasing below $\bar y^\infty$.

Significance

The result. Theorem 1 reduces an infinite-state average-cost control problem to a one-parameter search over critical numbers. The paper then evaluates the average cost of $\delta[\bar y]$ by a renewal formula, proves it convex in $\bar y$ (Theorem 2), and in §5 extends optimality to unlimited storage. The strong form of optimality matters: it compares with every Markov policy from every starting state, and it compares lim-infs, not only lim-sups.

Formalizing it. The theorem has a published proof, but no machine-checked one, and its proof relies on external results that are themselves unformalized: the countable-state average-cost theory of Federgruen, Schweitzer and Tijms, a fixed-point theorem on a compact convex subset of a product space, and a large-deviation estimate quoted from Feller. A formal development produces reusable infrastructure: expected first-passage sums for integer-valued random walks with a reflecting control, polynomial moment bounds for them, and the convexity-preservation argument for capacitated value iteration.

Difficulty

The state space is unbounded below, so the finite-state theory of average-cost Markov decision processes does not apply, and the one-period cost is unbounded. The obvious approach, letting the discount factor tend to one in the discounted problem, needs uniform bounds on relative value functions. Those bounds come from the expected cost until the inventory returns to a fixed interval, and with capacity limits that expectation must be controlled with growth $O(|x|^{\rho+3})$ uniformly over a class of policies. This is the content of Lemma 3, whose proof combines a large-deviation estimate for the demand sums with a renewal-type recursion. A second obstacle is strong optimality: comparing with policies whose lim-inf average cost is smaller requires that the relative value function grows sublinearly along every admissible trajectory (Corollary 2).

Formalization scope

All objects are in the namespace FedergruenZipkin.AvgCost, defined in one file. States $x, y$ and the capacity $U$ are integers; demands are natural numbers with a real probability mass function p; $b$ is a positive natural number. Convexity on $\mathbb Z$ is the second-difference inequality. Expectations of a real function are series $\sum_j p(j)\,v(y-j)$; expected policy costs and hitting sums are $[0,\infty]$-valued and need no integrability side condition. Feasibility and all properties of value functions are required only on states $x \le U$, which are the only states visited. Assumption 2 is stated literally, as real-analyticity of $\theta \mapsto \sum_j p(j)e^{i\theta j}$ at $0$. The order cost is zero, as in the paper. $\bar y^\infty$ is a parameter characterised as the least minimizer of $G$, not an infimum.

"Strongly optimal" has no displayed definition in the paper; it is read from eq. (7) in the proof of Theorem 1(b): convergence of the average cost of $\delta^*$ to $g^*$ from every state, together with a lim-inf lower bound for every Markov (memoryless, possibly nonstationary) policy from every state. The class is neither widened to history-dependent policies nor narrowed to stationary ones. The goal additionally records that $E\,v^*(y-D)$ converges, that $v^*$ has growth $O(|x|^{\rho+3})$, and that $g^* \ge 0$; all three follow from the paper's proof.

A trivializing reading is ruled out: the existence of $g$, $v$ and $y^*$ is one existential, so $y^*$ cannot be decoupled from the solution of (6), and strong optimality includes the convergence of $\delta^*$'s own average cost to $g^*$, so $g = 0$ does not satisfy it vacuously.

Not posed: Lemma 1 (quoted from Feller, and replaceable by a Chernoff bound); the renewal formulas (10)–(11) and Theorem 2; and §5 (unlimited storage). Useful contributions include a formal theory of expected hitting sums for skip-free-upward random walks, and a proof of Lemma 3 by any route.

Selected references

• A. Federgruen and P. Zipkin, An Inventory Model with Limited Production Capacity and Uncertain Demands I. The Average-Cost Criterion, Mathematics of Operations Research 11(2):193–207, 1986. https://doi.org/10.1287/moor.11.2.193
• A. Federgruen and P. Zipkin, An Inventory Model with Limited Production Capacity and Uncertain Demands II. The Discounted-Cost Criterion, Mathematics of Operations Research 11(2):208–215, 1986. https://doi.org/10.1287/moor.11.2.208
• A. Federgruen, P. J. Schweitzer and H. C. Tijms, Denumerable Undiscounted Semi-Markov Decision Processes with Unbounded Rewards, Mathematics of Operations Research 8(2):298–314, 1983. https://doi.org/10.1287/moor.8.2.298
• D. P. Heyman and M. J. Sobel, Stochastic Models in Operations Research, Vol. II, McGraw-Hill, 1984.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.

Motivation

Service parts supply chains are often limited by a capacitated resource, such as a production line or a repair shop, instead of by lead times alone. Once capacity binds, the classical tools for setting stock levels (Palm's theorem and the Poisson distribution of units in resupply) no longer apply, and the quantity that determines how much stock is needed is the shortfall: the amount by which the end-of-period inventory falls below its target because capacity was insufficient. Chapter 8 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) builds its tactical planning models for capacity-limited systems on the distribution of this random variable, and on a continuous-time repair queue in which item counts are geometric.

The shortfall recursion is the Lindley recursion of queueing theory (Lindley 1952), so its stationary law is the law of the maximum of a random walk with negative drift. The exponential tail of that maximum goes back to Cramér's work on ruin probabilities; for capacitated production–inventory systems it was stated by Glasserman (1997), whose theorem the book quotes as Theorem 11. Glasserman and Tayur (1995) used the shortfall to optimize base-stock levels in multi-echelon capacitated systems, and Roundy and Muckstadt (2000) studied the mass-exponential approximation that the theorem motivates.

Setting

A single item is produced in periods $n = 1, 2, \dots$ of an infinite horizon; at most $c$ units can be produced per period. The demand of period $n$ is $D_n$; the demands are nonnegative, independent and identically distributed, with generic demand $D$ and $E[D] < c$ (the standing assumption of Section 8.1.1).

Under the modified $(s-1, s)$ policy with target level $s$, the facility observes $D_n$ and produces $\min\{c, s - I_{n-1} + D_n\}$ units, where $I_n$ is the end-of-period net inventory and $I_0 = s$. The shortfall $V_n = s - I_n$ satisfies $V_0 = 0$ and

$$V_n = \left[V_{n-1} + D_n - c\right]^+ . \tag{8.1}$$

With the random walk $S_n = \sum_{k=1}^{n} (D_k - c)$ ($S_0 = 0$), the stationary shortfall is

$$V = \sup_{n \ge 0} S_n .$$

A law on $\mathbb R$ is lattice if it is concentrated on a progression $a + d\mathbb Z$ with $d > 0$.

In the discrete case ($c$ and $D$ integer valued) $(V_n)$ is a Markov chain on $\{0, 1, 2, \dots\}$ with transition probabilities $p_{ij}$ (p. 185). In the repair model of Section 8.3.1, reparable units of item $i$ arrive at rate $\lambda_i$, $\lambda = \sum_i \lambda_i$, a single exponential server repairs at rate $\mu > \lambda$, $N$ is the number of units in repair and $N_i$ the number of item-$i$ units, and $\eta_i = \lambda_i/(\mu - \lambda + \lambda_i)$.

Formalization targets

Goal: Theorem 11, corrected (p. 191)

Assume $E[e^{\alpha D}] < \infty$ for all $\alpha < \delta$, with $\delta > 0$; $P[D > c] > 0$; the law of $D$ is non-lattice; and $E[e^{-\alpha(c-D)}] = 1$ has a root in $(0, \delta)$. Then there are $\beta > 0$ and $\alpha > 0$ with

$$\frac{P\{V > v\}}{\beta e^{-\alpha v}} \to 1 \quad (v \to \infty), \qquad \alpha \text{ the unique positive root of } E\left[e^{-\alpha(c - D)}\right] = 1 .$$

The constant $\beta$ is left unspecified, as in the book.

Milestones, in attack order

1. Eq. (8.1): under the modified policy, $s - I_n = V_n$ for every $n$, independently of $s$.
2. Section 8.1.1: $V < \infty$ almost surely, $P\{V_n > v\} \to P\{V > v\}$ for every $v$, and the law of $V$ is stationary for (8.1).
3. Eq. (8.2): for $v > 0$, $P\{V_n > v\} = P\{D_n > v + c\} + E_D[1(d \le v + c)\, P\{V_{n-1} > v + c - d\}]$.
4. Theorem 11, second sentence: $E[e^{-\alpha(c-D)}] = 1$ has at most one positive root.
5. Section 8.1.2: with integer demand, $(V_n)$ is a Markov chain with transition probabilities $p_{ij}$.
6. Section 8.1.2: $\pi_i = \lim_n P\{V_n = i\}$ exists and solves $\pi\mathcal P = \pi$, $\sum_i \pi_i = 1$, $\pi_i \ge 0$.
7. Section 8.3.1: if $N$ is geometric with parameter $\lambda/\mu$ and $N_i$ given $N = j$ is binomial$(j, \lambda_i/\lambda)$, then $P[N_i = j] = (1 - \eta_i)\eta_i^j$.
8. Section 8.3.1: $\sum_{j > s} p_i(j) = \eta_i^{s+1}$, and the smallest cost-minimising stock level is the smallest $s$ with $\eta_i^{s+1} \le h_i/(h_i + b)$.

Significance

The exponential tail is the justification the book gives for approximating the shortfall by a mass-exponential law (an atom at zero plus an exponential tail), from which target stock levels and fill rates are computed in closed form. The decay rate $\alpha$ depends only on the demand law and the capacity, so the theorem also says how the stock needed for a given service level grows as utilization approaches one. The discrete-chain milestones justify the exact computation of the shortfall distribution behind the book's Table 8.1 and Figures 8.3–8.8. The geometric law of $N_i$ reduces the multi-item repair problem to independent newsvendor problems with an explicit solution.

The asymptotics of the random-walk maximum are proved in the literature (Cramér–Lundberg theory, Feller Vol. II, XII.5; Asmussen, Applied Probability and Queues, XIII.5); no machine-checked proof is known to exist. Mathlib has neither the Lindley recursion, nor ladder-height decompositions, nor the key renewal theorem for non-lattice laws. The printed Theorem 11 is not correct as stated (see Formalization scope), so the mission also records a corrected statement.

Difficulty

The central step of the goal is the passage from the random walk to an exact asymptotic. An exponential change of measure (Esscher tilt) with the root $\alpha$ turns $P\{V > v\}$ into an expectation under a law with positive drift, but it only yields the upper bound $P\{V > v\} \le e^{-\alpha v}$ (Lundberg's inequality); it does not show that $e^{\alpha v}P\{V > v\}$ converges, nor that the limit is positive. Convergence needs a renewal theorem for the overshoot of the tilted walk, which fails for lattice laws. That is why the non-lattice hypothesis cannot be dropped. For the milestones, the existence of the stationary law needs the reversal argument that identifies the law of $V_n$ with that of $\max_{k \le n} S_k$, plus the strong law of large numbers to show $V < \infty$ from $E[D] < c$.

Formalization scope

• Model. Demands are real, nonnegative, measurable, i.i.d. (iIndepFun plus IdentDistrib with $D_1$), integrable, with $E[D] < c$; these are fields of ShortfallModel. Periods are numbered from $1$ as in the book (demand 0 is an unused i.i.d. copy). The discrete case is a separate structure with $\mathbb N$-valued demand and capacity.
• Stationary shortfall. The book's "stationary distribution ... Let $V$ represent this random variable" is pinned to $V = \sup_{n \ge 0} S_n$, taken in $[0, \infty]$ and converted to a real number; milestone 2 proves that it is the limit law of $V_n$ from $V_0 = 0$ and a stationary law of (8.1). The discrete $\pi_i$ is pinned to $\lim_n P\{V_n = i\}$.
• Corrections to Theorem 11. The printed theorem is false. For integer demand $P\{V > v\}$ is a step function, and no $\beta e^{-\alpha v}$ is asymptotic to it. If $E[e^{\alpha D}]$ is finite only for $\alpha < \delta$, the equation $E[e^{-\alpha(c-D)}] = 1$ may have no root in $(0,\delta)$. The goal therefore adds two labelled hypotheses: a non-lattice demand law, and a root in $(0, \delta)$. The mass-exponential demand of Section 8.1.3 (an atom at $0$ plus a density) is non-lattice. The approximation $\beta \approx e^{-2(.583)(c-E(D))/\sigma}$ is not stated.
• Repair model. The M/M/1 queue is not built. The geometric law of $N$ (asserted on p. 202) and the binomial split of $N$ (quoted from Chapter 3) enter milestone 7 as hypotheses, exactly as the page's proof uses them. The stability condition $\lambda < \mu$, not written on the page, is a hypothesis. "The optimal $s_i$" is read as the smallest minimiser of the cost.
• Ruled out. Stating Theorem 11 with $\alpha$ or $\beta$ allowed to depend on $v$, with $\beta = 0$ (the ratio would be a division by zero, which Lean evaluates to $0$), or for a $V$ postulated to have an exponential tail proves nothing. Here $\beta, \alpha$ are quantified before $v$, both are asserted positive, and $V$ is constructed from the demands.
• Not formalized. The mass-exponential approximations (8.3)–(8.4), the Roundy–Muckstadt refinement, the fill-rate formula $\eta(s)$ (a definition, whose steady-state identity needs uniform integrability the book does not discuss), the random-capacity chain on p. 186, and the monotonicity of $s_i$ in $\mu$.
• Reusable infrastructure. Welcome: the Lindley recursion and its reversal identity, the Loynes existence theorem, Lundberg's inequality, and a non-lattice renewal theorem. All of these are needed well beyond this mission, in queueing (GI/G/1 waiting times) and ruin theory.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Chapter 8. https://doi.org/10.1007/b138879
• P. Glasserman, Bounds and asymptotics for planning critical safety stocks, Operations Research 45(2), 244–257, 1997. https://doi.org/10.1287/opre.45.2.244
• P. Glasserman and S. Tayur, Sensitivity analysis for base-stock levels in multiechelon production-inventory systems, Management Science 41(2), 263–281, 1995 (the book's reference [97]). https://doi.org/10.1287/mnsc.41.2.263
• R. O. Roundy and J. A. Muckstadt, Heuristic computation of periodic-review base stock inventory policies, Management Science 46(1), 104–109, 2000. https://doi.org/10.1287/mnsc.46.1.104.15131
• D. V. Lindley, The theory of queues with a single server, Mathematical Proceedings of the Cambridge Philosophical Society 48(2), 277–289, 1952. https://doi.org/10.1017/S0305004100027638
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971, Chapter XII.
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003, Chapter XIII. https://doi.org/10.1007/b97236