Motivation

Controlled queueing systems (admission control, routing, service-rate selection) are naturally modelled as Markov decision chains whose state is a buffer content and therefore ranges over a countably infinite set. Linn Sennott's Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, DOI 10.1002/9780470317037) develops the dynamic programming theory for exactly this setting: countable state space, finite action sets, nonnegative and possibly unbounded costs, and value functions that are allowed to be infinite. The book's computational method, the approximating sequence method (ASM), replaces the infinite chain by a sequence of finite truncations and asks when optimal values and policies of the truncations converge to those of the original chain.

This mission is the first of a series on the book. It covers Chapter 3, finite horizon optimization, together with the model of Chapter 2 and three results from Appendices A and B that the chapter uses. The finite horizon theory is the entry point: it is where the book's general policy class, its extended-valued cost criteria and its approximating sequences are first used together.

Setting

A Markov decision chain $\Delta$ has a countable state space $S$; for each $i \in S$ a finite nonempty action set $A_i$; a finite cost $C(i,a) \ge 0$; and for each $a \in A_i$ a transition distribution $(P_{ij}(a))_{j \in S}$. A history at time $t$ is $h_t = (i_0, a_0, \dots, i_{t-1}, a_{t-1}, i_t)$, and a general policy $\theta$ chooses the action at time $t$ from a distribution $\theta(\cdot \mid h_t)$ on $A_{i_t}$: it may use the whole history and may randomize. Stationary policies $f$ ($f(i) \in A_i$) and deterministic Markov policies (a stationary policy for each time) are special cases.

Fix a finite terminal cost $F \ge 0$ and a discount factor $0 < \alpha \le 1$ ($\alpha = 1$ is the undiscounted case). The $n$ horizon expected discounted cost of $\theta$ from initial state $i$ is

$$v_{\theta,\alpha,n}(i) = \sum_{t=0}^{n-1} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i] + \alpha^n E_\theta[F(X_n) \mid X_0 = i],$$

and the value function is $v_{\alpha,n}(i) = \inf_\theta v_{\theta,\alpha,n}(i)$ over all general policies. Both may be $+\infty$. A policy is optimal for the $n$ horizon if it attains $v_{\alpha,n}(i)$ at every $i$. For $n \ge 1$ put $u_{\alpha,n}(i,a) = C(i,a) + \alpha \sum_j P_{ij}(a) v_{\alpha,n-1}(j)$ and let $B_i(\alpha,n)$ be the set of $a \in A_i$ minimizing it.

An approximating sequence $(\Delta_N)_{N \ge N_0}$ has finite nonempty state spaces $S_N$ increasing to $S$, the same actions and costs, and transition distributions $P_{ij}(a;N)$ on $S_N$ converging to $P_{ij}(a)$ as $N \to \infty$. Its value functions are $v^N_{\alpha,n}$. In an augmentation type approximating sequence, the probability $P_{ir}(a)$ of leaving $S_N$ to $r$ is redistributed over $S_N$ by an augmentation distribution $q_j(i,a,r,N)$. Assumption FH($\alpha$, $n$) requires $\limsup_N v^N_{\alpha,n}(i)$ to be finite and at most $v_{\alpha,n}(i)$ for every $i$. A stationary policy $e$ is a limit point of stationary policies $e^N$ if, along a subsequence, $e^{N_r}(i) = e(i)$ eventually for each $i$.

Formalization targets

Goal: Theorem 3.2.3

For fixed $n \ge 1$,

$$\Big(\forall i:\ \lim_{N\to\infty} v^N_{\alpha,n}(i) = v_{\alpha,n}(i) < \infty\Big) \iff \mathrm{FH}(\alpha,n),$$

and under either condition every limit point $e_n$ of stationary policies $e^N_n$ with $e^N_n(i) \in B^N_i(\alpha,n)$ satisfies $e_n(i) \in B_i(\alpha,n)$ for all $i \in S$.

Milestones

1. Proposition A.1.1: a probability average of $u$ is at least $\min u$, with equality iff the distribution is concentrated on the minimizers.
2. Theorem 3.1.2: the finite horizon optimality equation $v_{\alpha,n}(i) = \min_a u_{\alpha,n}(i,a)$, and the characterization of all optimal general policies.
3. Corollary 3.1.4: choosing $f_{n-t}(i) \in B_i(\alpha,n-t)$ yields an optimal deterministic Markov policy.
4. Proposition 2.5.6: the augmentation (2.19) defines an approximating distribution.
5. Lemma 3.2.2: $v^N_{\alpha,0} \to v_{\alpha,0}$ and $\liminf_N v^N_{\alpha,n} \ge v_{\alpha,n}$.
6. Propositions B.3 and B.5: sequences of stationary policies, for $\Delta$ or for $(\Delta_N)$, have limit points.
7. Propositions 3.3.1, 3.3.2 and 3.3.4: three sufficient conditions for FH($\alpha$, $n$), namely bounded costs, an augmentation sending excess probability to a finite set, and the augmentation inequality (3.20).

Significance

Theorem 3.1.2 is the finite horizon dynamic programming equation in the generality the rest of the book needs: the value function is an infimum over history-dependent randomized policies, and the equation holds with infinite values allowed. Its characterization of optimal policies is Bellman's principle of optimality in necessary-and-sufficient form. Corollary 3.1.4 shows that deterministic Markov policies suffice. The discounted chapter builds on these results, since its value function is the limit of finite horizon ones, and so does the value iteration algorithm of the average cost chapters.

Theorem 3.2.3 is the finite horizon case of the approximating sequence method. It says exactly when finite truncations give the right answer, and it reduces the question to Assumption FH, for which Section 3.3 gives checkable conditions. The same structure (a lim inf inequality, a lim sup assumption, a limit point of optimal truncated policies) recurs for the discounted and the average cost criteria in later chapters.

The results are proved in the book. None of them is formalized: the platform has finite horizon dynamic programming only for Markov policies, abstract monotone mappings or finite reward-maximizing MDPs, and nothing on approximating sequences. A formalization contributes a Lean model of Markov decision chains with general policies and extended-valued criteria, which the later missions of the series restate and can merge with this one.

Difficulty

The obvious proof of the optimality equation conditions on the first action and state and then applies the induction hypothesis to the rest of the trajectory. With general policies the rest of the trajectory is governed by a continuation policy that depends on the first state and action, and the decomposition of the path law into a first step and a continuation must be proved from the definition of the process, not assumed. Infinite values also make the "only if" direction delicate: a strict inequality between expected costs becomes an equality once both sides are infinite.

For approximating sequences, the natural idea is to pass to the limit in the optimality equation of $\Delta_N$. This fails in general. Example 3.2.1 of the book has $\lim_N v^N_{1,2}(0) = 2 > 1 = v_{1,2}(0)$, because truncation moves probability onto states of high cost and dominated convergence is not available. Only the lim inf inequality holds for free, through a generalized Fatou lemma for approximating distributions. The lim sup side is exactly what Assumption FH supplies. The limit point argument then needs the compactness statement of Appendix B and the fact that a lim inf can be passed through a minimum over a finite set.

Formalization scope

The state space is a type S with [Countable S], the actions a type Act, and A i : Finset Act is nonempty. Costs are ℝ≥0, transition probabilities ℝ≥0∞ summing to 1 over S, and all values and expectations are in ℝ≥0∞, so infima over policies are lattice infima and +∞ is a genuine value. A history is the list of past state–action pairs, most recent first, with the current state, and a policy gives a distribution on A i for every history. Expectations are sums over histories of the path probabilities $\prod \theta(a_s \mid h_s) P_{i_s i_{s+1}}(a_s)$, which is the book's (2.6) and (2.9), not the dynamic programming recursion. The discount factor satisfies $0 < \alpha \le 1$ in every statement. An approximating sequence is indexed by $N \in \mathbb N$ with a start level $N_0$; its value functions are set to $0$ for the finitely many $N$ at which a given state is not yet in $S_N$, which does not affect limits.

The optimality equation must not be made definitional by defining $v_{\theta,\alpha,n}$ or $v_{\alpha,n}$ through the recursion (3.2). The policy class must not be restricted to deterministic Markov policies either, since that would make the characterization in Theorem 3.1.2 a different statement. Theorem 3.1.2(ii)(2) is stated with the guard $v_{\alpha,n}(i) < \infty$; the book omits it, and without it the "only if" direction is false (see the item's note).

A complete development needs the first-step decomposition of the path law under a general policy, the generalized Fatou lemma for approximating distributions (Proposition A.2.5, a milestone of the Appendix A mission of this series), and lim inf / lim sup manipulations in ℝ≥0∞. The model definitions are reusable by every later mission of the series. Contributions are welcome at every milestone, including proofs of the definitional sanity facts (for instance $v_{\theta,\alpha,0} = F$).

Selected references

• Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. https://doi.org/10.1002/9780470317037
• Martin L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994 (the standard reference for finite horizon dynamic programming with history-dependent randomized policies).
• Richard Bellman, Dynamic Programming, Princeton University Press, 1957.

Motivation

Control problems for queueing systems (admission control, routing, service rate selection, inventory replenishment) are naturally modelled as Markov decision chains with a countable state space, such as the number of customers in a buffer, and with costs that grow without bound in the state, such as holding costs proportional to queue length. The expected discounted cost criterion is the first infinite horizon criterion applied to such models, and it is also the tool through which the average cost criterion is treated later in the same book (Chapters 6–8 of Sennott's text reach average cost optimal policies through limits of discounted problems as the discount factor tends to one).

Classical treatments of discounted dynamic programming assume bounded costs, under which the dynamic programming operator is a contraction and has a unique bounded fixed point. That assumption fails for queueing models. This mission formalizes Chapter 4, Sections 4.1–4.4, of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999), which develops the discounted theory for nonnegative, possibly unbounded costs, where value functions may be infinite.

Timeline of the underlying theory:

• 1965. Blackwell (Ann. Math. Statist. 36) establishes the discounted theory with bounded rewards.
• 1966. Strauch (Ann. Math. Statist. 37) treats "negative" dynamic programming, the case of nonpositive rewards (equivalently nonnegative costs), with no boundedness assumption.
• 1977–1978. Bertsekas (SIAM J. Control Optim. 15) and Bertsekas and Shreve (Stochastic Optimal Control: The Discrete-Time Case) give the abstract monotone-mapping framework covering both cases.
• 1999. Sennott's text states the countable-state, finite-action, nonnegative-cost discounted theory in the form used for queueing control, with general history-dependent randomized policies.

Setting

A Markov decision chain $\Delta$ has a countable state space $S$; for each state $i$ a finite nonempty action set $A_i$; for each $a \in A_i$ a nonnegative finite cost $C(i,a)$ and a probability distribution $(P_{ij}(a))_{j \in S}$ of the next state. A policy $\theta$ chooses the action at time $n$ at random from a distribution $\theta(\cdot \mid h_n)$ on $A_{i_n}$ that may depend on the entire history $h_n = (i_0, a_0, \dots, a_{n-1}, i_n)$. A stationary policy $f$ always chooses $f(i) \in A_i$ in state $i$; for it one writes $C(i,f) = C(i,f(i))$ and $P_{ij}(f) = P_{ij}(f(i))$.

Fix a discount factor $\alpha \in (0,1)$. For an initial state $i$ and a policy $\theta$, the $n$-horizon cost with terminal cost zero and the infinite horizon discounted cost are

$$v_{\theta,\alpha,n}(i) = \sum_{t=0}^{n-1} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i], \qquad V_{\theta,\alpha}(i) = \sum_{t=0}^{\infty} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i],$$

and the value functions are $v_{\alpha,n}(i) = \inf_\theta v_{\theta,\alpha,n}(i)$ and $V_\alpha(i) = \inf_\theta V_{\theta,\alpha}(i)$, infima over all policies. All of these lie in $[0,\infty]$. A policy is discount optimal if $V_{\theta,\alpha} = V_\alpha$. The discount optimality equation is

$$W(i) = \min_{a \in A_i} \Big\{ C(i,a) + \alpha \sum_j P_{ij}(a) W(j) \Big\}, \qquad i \in S. \tag{4.9}$$

With $W = V_\alpha$, $B_i(\alpha)$ denotes the set of actions attaining the minimum at $i$.

Formalization targets

Goal: Theorem 4.1.4

$V_\alpha$ solves (4.9); every $W : S \to [0,\infty]$ solving (4.9) satisfies $V_\alpha \le W$; and every stationary policy $f_\alpha$ with

$$C(i,f_\alpha) + \alpha \sum_j P_{ij}(f_\alpha) V_\alpha(j) = \min_a \Big\{ C(i,a) + \alpha \sum_j P_{ij}(a) V_\alpha(j) \Big\} \quad \text{for all } i$$

is discount optimal. No boundedness of costs and no finiteness of $V_\alpha$ is assumed.

Milestones

In attack order: Lemma 4.1.1 ($v_{\theta,\alpha,n} \uparrow V_{\theta,\alpha}$); Proposition 4.1.2 (a supersolution of the one-policy equation dominates $v_{e,\alpha,n} + \alpha^n E_e[W(X_n)]$ and $V_{e,\alpha}$); Corollary 4.1.3 (a supersolution of the optimality inequality dominates $V_{f,\alpha} \ge V_\alpha$); then, beyond the goal, Corollary 4.1.5 ($\alpha^n E_{f_\alpha}[V_\alpha(X_n) \mid X_0 = i] \to 0$ where $V_\alpha(i) < \infty$), Proposition 4.2.2 and Corollary 4.2.4 (conditions under which a solution of (4.9) equals $V_\alpha$), Proposition 4.3.1 ($v_{\alpha,n} \uparrow V_\alpha$, and limit points of finite horizon optimal stationary policies are discount optimal) and Proposition 4.4.1 (optimal policies are exactly those concentrated on the sets $B_{i}(\alpha)$ along histories of positive probability).

Significance

Theorem 4.1.4 is the foundation for everything in the book that concerns discounted costs: it produces an optimal stationary deterministic policy, identifies $V_\alpha$ among the many solutions of (4.9) (Example 4.2.1 of the book gives a one-parameter family of finite solutions), and underlies value iteration (Proposition 4.3.1) and the approximating-sequence method of Sections 4.6–4.7. The average cost results of Chapters 6–8 are proved from it by letting $\alpha \to 1$. Proposition 4.4.1 describes the full set of optimal policies, including randomized and history-dependent ones.

These are known results with published proofs. The contribution of this mission is a machine-checked development of the discounted theory for countable state spaces with unbounded costs and infinite values, over the general policy class. Related statements on the platform (the monotone-mapping propositions of Bertsekas 1977 in the MonotoneDP missions, and bounded-cost or finite-state discounted results) use different models and are open; no machine-checked proof of the present statements is known to this mission.

Difficulty

The contraction argument that settles the bounded case is unavailable: with unbounded costs the operator in (4.9) has many fixed points, and $V_\alpha$ can equal $+\infty$ at some states, so neither uniqueness of fixed points nor subtraction of values is available. The optimality equation compares the infimum over all history-dependent randomized policies with a one-step minimum, so the general policy class and the law of the process under it must be handled directly; restricting attention to Markov or stationary policies begs the question. Every limit exchange (monotone limits of finite horizon costs, the passage to limit points of policies in Proposition 4.3.1) takes place in $[0,\infty]$, where finite-valued arguments do not transfer verbatim.

Formalization scope

The Lean development lives in the namespace SennottDP.Discounted. Conventions:

• The state space is a type S with [Countable S]; actions form a type Act and A i : Finset Act is nonempty. Costs are ℝ≥0; transition probabilities are ℝ≥0∞ with ∑' j, P i a j = 1 for a ∈ A i.
• A history at time $n$ is a pair Fin (n+1) → S, Fin n → Act; a policy assigns to every history a distribution on the action set of its last state. The probability of a history is the product of the policy and transition probabilities; expectations are ℝ≥0∞ sums over histories, so no integrability conditions arise.
• All values ($v_{\theta,\alpha,n}$, $V_{\theta,\alpha}$, $v_{\alpha,n}$, $V_\alpha$, and the competing solutions $W$) are ℝ≥0∞-valued; $0 \cdot \infty = 0$. The discount factor is α : ℝ≥0 with 0 < α and α < 1. Terminal costs are zero.
• $V_\alpha$ and $v_{\alpha,n}$ are infima over the type of all general policies. Defining them over stationary policies only would make the optimality of $f_\alpha$ a tautology; that formalization is ruled out.
• Proposition 4.4.1: the book states the equivalence without a finiteness assumption, but its necessity argument needs $V_\alpha < \infty$, and necessity fails otherwise. Sufficiency is stated in general and necessity under $V_\alpha < \infty$ everywhere.

Useful infrastructure, reusable by the later missions of this series (approximating sequences, average cost): the shift of a general policy after its first step, the Chapman–Kolmogorov identity for the history law, and the computation $E_f[W(X_{n+1})] = E_f[\sum_j P_{X_n j}(f) W(j)]$ for stationary policies. Contributions of such lemmas, and proofs of any milestone, are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999, Chapter 4. https://doi.org/10.1002/9780470317037
• D. Blackwell, Discounted dynamic programming, Annals of Mathematical Statistics 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
• R. E. Strauch, Negative dynamic programming, Annals of Mathematical Statistics 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM Journal on Control and Optimization 15 (1977), 438–464. https://doi.org/10.1137/0315031
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Optimal control of queueing systems leads to Markov decision problems whose state space is countably infinite (buffer contents, numbers of customers) and whose costs are unbounded (holding costs grow with the queue). Such a problem cannot be solved on a computer as it stands. The standard remedy is to truncate: solve a finite problem on the states $\{0,1,\dots,N\}$ and hope that its value and its optimal policy approximate those of the original problem as $N$ grows. Linn Sennott's approximating sequence method (ASM) makes this hope precise. For the expected discounted cost criterion, Sections 4.6–4.7 of Sennott's book (Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999) identify a single condition, Assumption DC($\alpha$), that is necessary and sufficient for convergence of the truncated values, and give checkable sufficient conditions for it.

The method matters because naive truncation can fail. The book's Example 4.6.1 has a chain whose value at state $0$ is finite, yet a natural truncation produces values $V^N_\alpha(0)\ge \alpha N^2/((1-\alpha)[N(1-\alpha)+\alpha])\to\infty$. How the probability that would leave the truncated set is redistributed decides whether the computation is meaningful.

Earlier truncation schemes (Fox 1971; White 1980, 1982; Hernández-Lerma 1986; Cavazos-Cadena 1986; Whitt 1978–79; see the bibliographic notes on p. 81 of the book and Puterman 1994) require bounded rewards or pass directly to an algorithm. The ASM instead produces a sequence of finite Markov decision chains that can be studied in their own right; the material of Sections 4.6–4.7 is presented in the book as new.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$; for each state $i$ a finite nonempty action set $A_i$; nonnegative finite costs $C(i,a)$; and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a)=1$. A policy $\theta$ chooses the action at time $t$ at random from a distribution $\theta(\cdot\mid h_t)$ on $A_{i_t}$ that may depend on the entire history $h_t=(i_0,a_0,\dots,i_{t-1},a_{t-1},i_t)$. A stationary policy $f$ always chooses $f(i)\in A_i$ in state $i$. Fix a discount factor $\alpha\in(0,1)$. The discounted cost of $\theta$ and the discounted value function are

$$V_{\theta,\alpha}(i)=\sum_{t\ge0}\alpha^tE_\theta[C(X_t,A_t)\mid X_0=i],\qquad V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i),$$

both in $[0,\infty]$, the infimum over all policies. A policy is discount optimal if $V_{\theta,\alpha}=V_\alpha$.

An approximating sequence $(\Delta_N)_{N\ge N_0}$ consists of finite nonempty sets $S_N$ increasing to $S$ and, for $i\in S_N$ and $a\in A_i$, probability distributions $P_{ij}(a;N)$ on $S_N$ with $P_{ij}(a;N)\to P_{ij}(a)$ as $N\to\infty$. The finite MDC $\Delta_N$ has state space $S_N$ and the same actions and costs; $V^N_\alpha$ is its value function and $f^N_\alpha$ a stationary policy attaining the minimum in its discount optimality equation

$$V^N_\alpha(i)=\min_{a\in A_i}\Big\{C(i,a)+\alpha\sum_{j\in S_N}P_{ij}(a;N)V^N_\alpha(j)\Big\},\qquad i\in S_N.$$

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the excess probability $P_{ir}(a)$, $r\notin S_N$, according to augmentation distributions $q_j(i,a,r,N)$ on $S_N$: $P_{ij}(a;N)=P_{ij}(a)+\sum_{r\notin S_N}P_{ir}(a)q_j(i,a,r,N)$.

Assumption DC($\alpha$): for every $i\in S$, $W_\alpha(i):=\limsup_{N}V^N_\alpha(i)<\infty$ and $W_\alpha(i)\le V_\alpha(i)$.

Formalization targets

Goal: Theorem 4.6.3

The following are equivalent:

$$\text{(i)}\ \lim_{N\to\infty}V^N_\alpha(i)=V_\alpha(i)<\infty\ \ (i\in S);\qquad \text{(ii)}\ \text{Assumption DC}(\alpha).$$

Under either, every limit point of $(f^N_\alpha)_{N\ge N_0}$ (a stationary $f$ with $f^{N_r}(i)=f(i)$ eventually along a subsequence, for each $i$) is discount optimal for $\Delta$.

Milestones

• Lemma 4.6.2: $\liminf_N V^N_\alpha\ge V_\alpha$ for every approximating sequence.
• Proposition 4.7.1: bounded costs imply DC($\alpha$).
• Lemma 4.7.2: taboo probabilities of avoiding $S-S_N$ converge to the $t$-step transition probabilities.
• Lemma 4.7.3: for the first passage time $T_i(N)$ out of $S_N$ under a stationary policy, $E[\alpha^{T_i(N)}]\to0$.
• Proposition 4.7.4: if $V_\alpha<\infty$ and the ATAS sends excess probability to a finite set, DC($\alpha$) holds.
• Corollary 4.7.5: the case of a single distinguished state $z$, with the relative form of the optimality equation for $\Delta_N$.
• Proposition 4.7.6: if $V_\alpha<\infty$ and the augmentation distributions satisfy $\sum_{j\in S_N}q_j(i,a,r,N)v_{\alpha,n}(j)\le v_{\alpha,n}(r)$ for all $n\ge0$, then $V^N_\alpha\le V_\alpha$ on $S_N$.

Significance

Theorem 4.6.3 turns the question "does truncation work?" into the verification of one inequality between a lim sup and the true value, and it delivers both the value and an optimal stationary policy from finite computations. Propositions 4.7.4–4.7.6 give conditions that hold in the queueing models of the book with unbounded holding costs, and Corollary 4.7.5 supplies the computational form used for the inventory model of Chapter 5. The discounted theory is also the stepping stone to the average cost ASM of Chapter 8, which is built on discounted approximations.

All results are proved in the book. None of them is formalized: the platform has no statement about approximating sequences or state truncation of countable-state MDPs, and Mathlib has no Markov decision processes. The mission produces machine-checked versions of the convergence theorem and its sufficient conditions, for general history-dependent randomized policies and $[0,\infty]$-valued costs.

Difficulty

The value functions are infima over uncountably many history-dependent policies and may be infinite, so no contraction argument applies: costs are unbounded and $V_\alpha$ is only the minimal nonnegative solution of its optimality equation. Passing to the limit in $N$ inside $\sum_{j\in S_N}P_{ij}(a;N)V^N_\alpha(j)$ is an interchange of limit and infinite sum under a moving probability measure, with no dominating function in general; Example 4.6.1 shows that the interchange genuinely fails. The upper bound of Proposition 4.7.4 requires comparing $\Delta_N$ with $\Delta$ along a coupled first passage out of $S_N$, which needs the taboo-probability estimates of Lemmas 4.7.2–4.7.3. The obvious idea of bounding $V^N_\alpha$ by $\sup C/(1-\alpha)$ works only for bounded costs (Proposition 4.7.1).

Formalization scope

The state type S is countable ([Countable S]); actions live in a type Act, with a finite nonempty Finset of admissible actions per state. Costs are ℝ≥0, transition probabilities and all value functions are ℝ≥0∞, so infima over policies are lattice infima and $+\infty$ is a legitimate value. A general policy is a function of the history, encoded as the list of past state–action pairs (most recent first) and the current state; the expected cost at time $t$ is the $[0,\infty]$-valued sum over histories. $V_\alpha$ is the infimum over all such policies; a stationary policy enters as the policy putting mass one on $f(i)$. The discount factor is α : ℝ≥0 with $0<\alpha<1$ (the chapter's standing assumption). $\Delta_N$ is an MDC on the subtype $S_N$; $V^N_\alpha(i)$ is extended by $0$ when $N<N_0$ or $i\notin S_N$, a convention that affects finitely many $N$ for each fixed $i$ and hence no limit in $N$. Limits, lim sups and lim infs are along Filter.atTop in ℝ≥0∞. Taboo probabilities and the first passage quantity $E[\alpha^{T}]=\sum_{n\ge1}\alpha^nP(T=n)$ (so $\alpha^\infty=0$) are defined combinatorially from the transition probabilities.

A trivializing formalization is ruled out: $V_\alpha$ is not an infimum over stationary policies only (which would make optimality of limit points close to definitional), DC($\alpha$) keeps both of its conditions, and statement (i) of the goal includes finiteness of $V_\alpha$.

A complete development needs the minimality of $V_\alpha$ among nonnegative solutions of the discount optimality equation (Theorem 4.1.4, chunk II of this series), Fatou-type lemmas for sums against converging distributions (Appendix A, chunk XI), and compactness of stationary policies (Proposition B.5). Contributions of these as reusable lemmas about countable-state MDCs are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Sections 4.6–4.7, pp. 73–81. https://doi.org/10.1002/9780470317037
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Why average cost on finite state spaces

Controlled queues, inventories and communication links are run for a long time, and the quantity an operator usually cares about is the long-run average cost per period rather than a discounted total. The average cost criterion is harder to work with than the discounted one: its value is a $\limsup$ of Cesàro means, it is not given by a contraction, and for general (history dependent, randomized) policies the limit need not exist. Chapter 6 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) treats the case of a finite state space, where the strongest results hold: an average cost optimal policy exists, can be taken stationary, and can be obtained as a limit of discount optimal policies as the discount factor tends to one.

The results go back to D. Blackwell, "Discrete dynamic programming", Ann. Math. Statist. 33 (1962), who showed that for finite states and actions some stationary policy is discount optimal for all discount factors close to one. Such a policy is now called Blackwell optimal. Sennott's Chapter 6 derives average cost optimality of this policy and the multichain average cost optimality equation from it, in the notation used throughout the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$, a finite nonempty action set $A_i$ in each state $i$, nonnegative finite costs $C(i,a)$, and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a) = 1$. A policy $\theta$ chooses the action at time $t$ from a distribution $\theta(\cdot \mid h_t)$ on $A_{i_t}$ that may depend on the whole history $h_t = (i_0,a_0,\ldots,i_t)$. A stationary policy $f$ always chooses a fixed action $f(i) \in A_i$ in state $i$.

With $X_t, A_t$ the state and action at time $t$ and $X_0 = i$, define

• the discounted cost $V_{\theta,\alpha}(i) = \sum_{t \ge 0} \alpha^t E_\theta[C(X_t,A_t)]$ for $0<\alpha<1$, and the discounted value function $V_\alpha(i) = \inf_\theta V_{\theta,\alpha}(i)$;
• the $n$ horizon cost $v_{\theta,n}(i) = \sum_{t=0}^{n-1} E_\theta[C(X_t,A_t)]$;
• the average cost $J_\theta(i) = \limsup_n v_{\theta,n}(i)/n$, its $\liminf$ version $J^*_\theta(i)$, and the minimum average cost $J(i) = \inf_\theta J_\theta(i)$.

All infima range over all general policies, and every quantity may equal $+\infty$. A policy is $\alpha$ discount optimal if $V_{\theta,\alpha} = V_\alpha$, and average cost optimal if $J_\theta = J$.

For a stationary policy $f$ on a finite state space, the induced Markov chain splits into positive recurrent classes $R_1,\ldots,R_K$ and transient states. With $p_k(i)$ the probability of reaching $R_k$ from $i$, distinguished states $z_k \in R_k$, and $W_\alpha(i) = \sum_k p_k(i) V_\alpha(z_k)$, the relative value function is $w_\alpha(i) = V_\alpha(i) - W_\alpha(i)$.

Formalization targets

Goal: Proposition 6.2.3

For an MDC with a finite state space there are $\alpha_0 \in (0,1)$ and one stationary policy $f$ such that $f$ is $\alpha$ discount optimal for every $\alpha \in (\alpha_0,1)$, $f$ is average cost optimal, and

$$J(i) = \lim_{\alpha\to 1^-} (1-\alpha) V_\alpha(i) = \lim_{n\to\infty} \frac{v_{f,n}(i)}{n}, \qquad i \in S.$$

Milestones

1. Proposition 4.5.3. For finite $S$ and stationary $e$, $\alpha \mapsto V_{e,\alpha}(i)$ is a finite, continuous, rational function on $(0,1)$.
2. Proposition 6.1.1. For every policy on a countable state space,

$$J^*_\theta(i) \le \liminf_{\alpha\to1^-}(1-\alpha)V_{\theta,\alpha}(i) \le \limsup_{\alpha\to1^-}(1-\alpha)V_{\theta,\alpha}(i) \le J_\theta(i),$$

with three equivalent conditions for equality. 3. Proposition 6.2.2. For finite $S$ and stationary $e$, $J_e(i) = \lim_{\alpha\to1^-}(1-\alpha)V_{e,\alpha}(i) = \lim_n v_{e,n}(i)/n$. 4. Proposition 4.5.1, Proposition 4.5.4, Corollary 4.5.5. The power series structure of $V_{\theta,\alpha}$ in $\alpha$; monotonicity and left continuity of $V_\alpha$; continuity under bounded costs. 5. Theorem 6.3.1. For the policy $f$ of the goal, $\lim_{\alpha \to 1^-} w_\alpha(i) = w(i)$ exists, and

$$J(i) + w(i) = C(i,f) + \sum_j P_{ij}(f) w(j) \ \ge\ \min_{a} \Big\{C(i,a) + \sum_j P_{ij}(a) w(j)\Big\},$$

together with the limit identities (i)–(iii) and the optimality criterion (v). 6. Proposition 6.3.3. $V_\alpha(i) = J(i)/(1-\alpha) + w^*(i) + \varepsilon_\alpha(i)$ with $\varepsilon_\alpha(i) \to 0$ as $\alpha \to 1^-$.

Significance

The goal says that on a finite state space nothing is gained by randomizing or by remembering the past when minimizing average cost, and that the minimum average cost is the vanishing-discount limit of the discounted value function. This justifies computing average cost optimal policies through discounted problems and value iteration, the route taken in the rest of Chapter 6 and, via approximating sequences, for countable state spaces in Chapters 7 and 8. Theorem 6.3.1 supplies an optimality equation without any unichain or communication assumption. The book's Example 6.3.2 shows that the inequality in that equation can be strict, and that a stationary policy attaining the minimum need not be optimal.

The results are classical and proved in the book. No machine-checked version of them is known to exist. The platform has average-reward results for unichain finite MDPs with Markov policies (the Puterman series) and an average-cost optimality equation under recurrence assumptions (the Bertsekas series). Neither covers existence of a Blackwell optimal policy against the class of all history dependent randomized policies, or the multichain equation. A formal development also yields reusable infrastructure: the law of a controlled process under a general policy, first passage quantities of finite chains, and the Abelian inequality between Abel and Cesàro means of a nonnegative sequence.

Difficulty

The obvious argument picks, for each $\alpha$, a stationary discount optimal policy $f_\alpha$ and lets $\alpha \to 1$. Finiteness of the set of stationary policies gives one policy that is optimal along some sequence $\alpha_n \to 1$, but not on an interval. Excluding infinite switching between two policies requires the analytic structure of $\alpha \mapsto V_{f,\alpha}(i)$ (Proposition 4.5.3), which in turn rests on matrix inversion of $I - \alpha P$. Passing from the discounted criterion to the average one requires an Abelian inequality for nonnegative series whose terms may be infinite (Proposition 6.1.1), and comparison against general policies rules out any argument that works only within stationary or Markov policies. For Theorem 6.3.1 the difficulty is the multichain structure: the relative value function has to be assembled class by class from first passage times and costs, and its limit must be identified.

Formalization scope

• States form a type S; [Countable S] for Section 4.5 and Proposition 6.1.1, [Fintype S] from Section 6.2 on, as in the book. Actions form a type Act with A i : Finset Act nonempty. Costs are in ℝ≥0, transition probabilities in ℝ≥0∞.
• A general policy is a function of the list of past state-action pairs (most recent first) and the current state, giving a distribution on A i. Stationary policies embed as degenerate policies. The law of the process is built from this data, and every infimum ranges over all general policies.
• $V_{\theta,\alpha}$, $V_\alpha$, $v_{\theta,n}$, $J_\theta$, $J^*_\theta$, $J$ are in ℝ≥0∞, so $+\infty$ is represented. $\alpha \to 1^-$ is the filter 𝓝[<] 1. On a finite state space these quantities are finite. The real valued objects of Section 6.3 ($w_\alpha$, $w$, $w^*$, equation (6.6)) are therefore formed with toReal, and this switch from ℝ≥0∞ to ℝ happens only in Theorem 6.3.1 and Proposition 6.3.3.
• The objects of Section 6.3 ($p_k$, $m_{i|k}$, $c_{i|k}$, $\pi_s$, $W_\alpha$) are defined from $f$. The distinguished states are a hypothesis quantified over.
• A trivializing formalization would take the infimum over stationary policies only, let the optimal policy depend on $\alpha$, or state rationality as an equation p/q without requiring $q \ne 0$. Each is excluded here: $J$ and $V_\alpha$ are infima over all general policies, one pair $(\alpha_0,f)$ is quantified before all $\alpha$, and the denominator is required to be nonzero on $(0,1)$.

Useful infrastructure includes rational functions of one real variable and their finitely many sign changes, the resolvent $(I-\alpha P)^{-1}$ of a stochastic matrix, the Abelian inequality for $[0,\infty]$-valued sequences, and renewal-reward identities for finite chains. Contributions of general lemmas on these topics are welcome, as are proofs of individual milestones.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, 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
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

In a discrete-time queue the service of a customer lasts a random number $Y$ of slots. When such a system is modelled as a Markov decision chain (Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, DOI 10.1002/9780470317037, Chapter 9), the state must record how much service is still owed, and the controller only observes that a service has lasted $s$ slots and is not yet finished. The relevant random quantity is then the residual life $Y_s$: the remaining service time given that $s$ slots have elapsed without completion. Verifying the book's average cost assumptions for such a model requires bounds on expected first passage times and costs, and these reduce to moment bounds on $Y$ and on the residual lives $Y_s$.

Section 9.2 isolates a single condition that makes those bounds available: the expected remaining service time is bounded uniformly in the elapsed time. The concept of mean residual life comes from reliability theory, where $Y$ is the lifetime of a component and $E[Y_s]$ is its expected remaining lifetime at age $s$. This mission formalizes Section 9.2 of the book, together with the moment computation for batch arrivals (Lemma 9.5.2) that the same verification uses.

Setting

Let $Y$ be a random variable with values in $\{1,2,3,\dots\}$ and distribution $u_y = P(Y = y)$, $y \ge 1$. Write $F(y) = P(Y \le y)$ and $F^*(y) = P(Y > y) = 1 - F(y)$ for $y \ge 0$, so $F(0) = 0$ and $F^*(0) = 1$. The $k$-th moment is

$$E[Y^k] = \sum_{y \ge 1} y^k u_y \in [0,\infty].$$

For $s \ge 0$ with $F^*(s) > 0$, the residual life $Y_s$ has distribution

$$P(Y_s = y) = P(Y = s + y \mid Y > s) = \frac{u_{s+y}}{F^*(s)}, \qquad y \ge 1,$$

with $Y_0 = Y$; its tail is $F^*_s(y) = F^*(s+y)/F^*(s)$, and $E[Y_s]$ is the mean residual lifetime.

The distribution of $Y$ has bounded mean residual lifetimes (BMRL-$U$, Definition 9.2.4) if there is a finite constant $U$ with

$$E[Y_s] \le U \qquad \text{for every } s \ge 0 \text{ with } F^*(s) > 0,$$

and it is BMRL if it is BMRL-$U$ for some $U$.

Three families appear by name: the geometric distribution $\mathrm{geo}(\mu)$ of the number of Bernoulli($\mu$) trials to the first success, $P(Y=y) = \mu(1-\mu)^{y-1}$; the negative binomial $\mathrm{neg\,bin}(\mu, r)$ of the number of trials to the $r$-th success, $P(Y = y) = \binom{y-1}{r-1}\mu^r(1-\mu)^{y-r}$ for $y \ge r$; and the truncated Poisson $\mathrm{trun\,Pois}(\lambda)$, $P(Y=y) = \frac{e^{-\lambda}}{1-e^{-\lambda}}\frac{\lambda^y}{y!}$ for $y \ge 1$.

For Lemma 9.5.2, batches of customers arrive in each slot; the batch sizes $X_1, X_2, \dots$ are independent with common distribution $p_j$, mean $\lambda = \sum_j j p_j$ and second moment $\lambda^{(2)} = \sum_j j^2 p_j$, and $X(s) = X_1 + \dots + X_s$ is the number of arrivals in $s$ slots.

Formalization targets

Goal: Proposition 9.2.5

If the distribution of $Y$ is BMRL, then

$$E[Y^k] < \infty \qquad \text{for every } k.$$

The goal fixes no constant: it asserts only that a uniform first-moment bound on the residual lives forces every moment of $Y$ to be finite.

Milestones

1. Proposition 9.2.1. $E[Y] = \sum_{y=0}^\infty F^*(y)$ and, for $k \ge 2$,

$$E[Y^k] = 1 + \sum_{z=0}^{k-1}\binom{k}{z}\left[\sum_{y=1}^\infty y^z F^*(y)\right]. \tag{9.4}$$

2. Remark 9.2.2. For $k \ge 2$, $E[Y^k] < \infty$ if and only if $\sum_y y^{k-1}F^*(y) < \infty$.
3. Proposition 9.2.3. For a positive integer $k$, $E[Y^k] < \infty$ implies $E[Y_s^k] < \infty$ for all $s \ge 0$.
4. Proposition 9.2.6. The geometric ($0<\mu<1$), negative binomial ($0<\mu<1$, $r \ge 2$) and truncated Poisson ($\lambda > 0$) distributions are BMRL.
5. Lemma 9.5.2. Under $\lambda^{(2)} < \infty$,

$$E[X(s)] = \lambda s, \qquad E[(X(s))^2] = \lambda^{(2)}s + \lambda^2 s(s-1). \tag{9.25}$$

Significance

The result itself. Proposition 9.2.5 turns a condition that is easy to check for concrete service distributions, and natural for services (a service whose expected remaining duration grows without bound as it goes on is undesirable), into the moment bounds that the average cost analysis consumes. With Proposition 9.2.6 it shows that the most common unbounded service distributions on $\{1,2,\dots\}$ have finite moments of all orders; with Lemma 9.5.2 it supplies the linear and quadratic growth of expected arrivals and their second moments that the verification of the (WAC) assumptions for the batch-arrival queue of Example 9.3.1 needs (Section 9.5). Every bounded distribution is BMRL as well (the book's Problem 9.3).

Formalizing it. All results here are proved in the book; none has a machine-checked proof on the platform or in Mathlib, which has geometric and Poisson distributions but no residual lives, negative binomial or truncated Poisson laws. A complete development gives a reusable tail-sum calculus for moments of $\mathbb N$-valued random variables in $[0,\infty]$, a residual-life construction for discrete distributions, and the BMRL property of three standard families. The platform's mean residual life order (the "Stochastic Orders II" mission, Shaked–Shanthikumar) compares two variables; BMRL is a uniform bound on one variable's residual lives and is not an order, so none of that material states these results.

Difficulty

BMRL controls only first moments, of the conditional laws $Y_s$; the goal asks for moments of every order of $Y$ itself. Bounding $E[Y^k]$ by expanding $E[Y_s]$ for each fixed $s$ gives nothing, because each single bound is compatible with a heavy tail: the uniformity in $s$ is essential. The residual lives are also only defined where $P(Y > s) > 0$, so every argument must handle distributions with bounded support separately. Proposition 9.2.6 requires explicit control of ratios of tail sums for three families; for the negative binomial and truncated Poisson the tails have no closed form.

Formalization scope

• $Y$ is represented by its law, a function $u : \mathbb N \to [0,\infty]$ with $\sum_y u_y = 1$ and $u_0 = 0$ (IsDistOnPos). $F^*$, moments and residual-life moments are ℝ≥0∞-valued series; an infinite moment is $+\infty$ and "finite" means $< \infty$. No Bochner integral is used, so a finite-moment conclusion cannot hold vacuously through an integrability default.
• The residual life $Y_s$ is defined by (9.7) and is used only where $F^*(s) > 0$; BMRL-$U$ is required exactly at those $s$, and $U$ is a finite nonnegative real. A formalization requiring the bound at every $s$ with a junk value of $E[Y_s]$ where $F^*(s) = 0$ is ruled out: the definitions never divide by $F^*(s) = 0$ in a used position, and bounded distributions remain BMRL.
• The geometric and negative binomial laws count trials (support starting at $1$ and $r$), not failures as Mathlib's geometricPMF does.
• Lemma 9.5.2 is stated on a probability space with measurable, mutually independent (iIndepFun) batch sizes of common law $p$, expectations as lower Lebesgue integrals, and only assumption (BA1), $\lambda^{(2)} < \infty$, which is the part of the book's (BA) that concerns arrivals.
• Welcome contributions: the tail-sum identity (9.4) and its reindexing lemmas, the residual-life tail formula (9.8) and moment formula (9.9), each as a separate lemma; and proofs that the three named families are probability distributions on their supports.

Selected references

• Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999, Section 9.2 (pp. 202–206) and Section 9.5 (pp. 214–215). DOI 10.1002/9780470317037
• Moshe Shaked and J. George Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Section 2.A (the mean residual life order). DOI 10.1007/978-0-387-34675-5

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.