Queueing and Stochastic Networks

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

Linn Sennott's Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) studies Markov decision chains with countably many states, finite action sets and unbounded nonnegative costs. Its main computational device, the approximating sequence method (Definition 2.5.1, p. 28), replaces the countable state space $S$ by an increasing sequence of state spaces $S_N$ and the transition law out of each state by distributions $P_j(N)$ on $S_N$ that converge pointwise to the original law. Every convergence argument of that method has the same shape: a sum $\sum_{j\in S_N} P_j(N)\,u(j,N)$, an expected cost or value under the $N$-th approximating model, must be shown to converge to $\sum_{j\in S} P_j\,u(j)$, or at least to satisfy a one-sided bound in the limit.

Appendix A, Sections A.1–A.2 (pp. 270–278), collects the analysis results used for this. The author proves them for sums over countable sets rather than general integrals, so they need no measure theory, and the proofs of the discounted-cost and average-cost approximation theorems (Chapters 4 and 8) cite them. This mission formalizes that appendix section as a self-contained unit.

Setting

Let $S$ be a countable set and $(P_j)_{j\in S}$ a probability distribution on $S$: $P_j\ge 0$ and $\sum_j P_j=1$. Values of functions are extended reals in $[-\infty,\infty]$, with the convention $0\cdot\infty=0$. For $u:S\to[-\infty,\infty]$, the weighted sum is

$$\sum_{j\in S}P_j\,u(j)=\sum_{j\in S}P_j\,u^+(j)-\sum_{j\in S}P_j\,u^-(j),$$

which is well defined, in $(-\infty,\infty]$, whenever the negative parts have finite weighted sum. In Lean this is wsum P u.

A family of approximating distributions for $(P_j)$ consists of

1. an increasing sequence of subsets $S_0\subseteq S_1\subseteq\cdots$ of $S$ with $\bigcup_N S_N=S$;
2. for each $N$, a probability distribution $(P_j(N))_{j\in S_N}$ on $S_N$;
3. pointwise convergence $\lim_{N\to\infty}P_j(N)=P_j$ for every $j\in S$.

Since the sets increase to $S$, a fixed state $j$ lies in $S_N$ for every large $N$, so $\liminf_N u(j,N)$ and $\lim_N u(j,N)$ make sense for a function $u(j,N)$ defined only for $j\in S_N$. In Lean these three conditions are the structure ApproxDist P SN Q, with Q N j $=P_j(N)$.

Formalization targets

Goal: Theorem A.2.6 (Generalized Dominated Convergence Theorem), p. 278

Under the approximating-distribution hypotheses, let $u(j,N)$ and $w(j,N)$ be finite with $|u(j,N)|\le w(j,N)$ for $j\in S_N$, let $u(j,N)\to u(j)$ and $w(j,N)\to w(j)$ for every $j$, and assume

$$\lim_{N\to\infty}\sum_{j\in S_N}P_j(N)\,w(j,N)=\sum_{j\in S}P_j\,w(j)<\infty.$$

Then

$$\lim_{N\to\infty}\sum_{j\in S_N}P_j(N)\,u(j,N)=\sum_{j\in S}P_j\,u(j).$$

Milestones, in the book's order

• Proposition A.1.3: $\liminf$ commutes with a minimum over a finite nonempty set; $\lim$ does too when all limits exist.
• Proposition A.1.5: $\liminf_N\sum_{j\in G}u(j,N)\ge\sum_{j\in G}\liminf_N u(j,N)$ for finite $G$ and $u>-\infty$, when the right side has no indeterminate form.
• Proposition A.1.7: the same inequality for countable sums of $[0,\infty]$-valued terms.
• Proposition A.1.8: the same, with the left sum over $S_N$ increasing to $S$.
• Proposition A.1.10: $\liminf u_n\le\liminf w_n/n\le\limsup w_n/n\le\limsup u_n$ for $w_n=\sum_{k<n}u_k$.
• Proposition A.2.1 (Fatou's lemma): $\liminf_N\sum_jP_j u(j,N)\ge\sum_jP_j\liminf_N u(j,N)$ for $u\ge -L$.
• Theorem A.2.3 (dominated convergence, with a convergent dominating sequence $w(j,N)$) and Corollary A.2.4 (fixed dominating function).
• Proposition A.2.5 (generalized Fatou's lemma):

$$\liminf_{N\to\infty}\sum_{j\in S_N}P_j(N)\,u(j,N)\ \ge\ \sum_{j\in S}P_j\,\liminf_{N\to\infty}u(j,N)\qquad(u\ge -L\text{ on }S_N).$$

• Corollary A.2.7: bounded convergence under approximating distributions.

Significance

The results. Proposition A.2.5 and Theorem A.2.6 are the two limit interchanges the approximating sequence method needs. The generalized Fatou inequality gives the lower bound on limits of value functions of the approximating models, and the generalized dominated convergence theorem identifies the limit of expected costs when a dominating function is available. Corollary A.2.7 gives the bounded case, and Proposition A.1.3 moves limits inside the minimization of an optimality equation. Proposition A.1.10 compares Cesàro averages with the sequence itself, which the average-cost chapters use.

Formalizing them. All statements are classical and proved in the book. A.1.7, A.2.1, A.2.3 and A.2.4 are, after translation, instances of Mathlib's Fatou lemma (MeasureTheory.lintegral_liminf_le) and dominated convergence theorem for a discrete measure. The mission states them in the book's discrete, extended-real form so later chapters can cite them by number. The versions in which the distribution and its support change with $N$ (A.2.5–A.2.7) are not in Mathlib in this form; the generalized dominated convergence theorem appears in the measure-theoretic literature (Royden, Real Analysis, Ch. 4) but has no Lean formalization. None of these statements has been formalized for this book.

Difficulty

For the generalized results, Mathlib's Fatou lemma and dominated convergence theorem do not apply directly: they fix one measure, while here both the weights $P_j(N)$ and the support $S_N$ change with $N$. The dominating function $w(j,N)$ also changes with $N$ and is not integrable uniformly in $N$; only the convergence of its expectations is assumed. For small $N$, $\sum_{j\in S_N}P_j(N)w(j,N)$ may even be infinite, and then $\sum_{j\in S_N} P_j(N)u(j,N)$ has no value.

A second difficulty is bookkeeping in the extended reals. Lower limits may be $\pm\infty$, products use $0\cdot\infty=0$, and a sum with a $+\infty$ term and a $-\infty$ term is undefined. The inequality of Proposition A.1.5 holds only when that indeterminate form is excluded. The bound $u\ge -L$ in A.2.1 and A.2.5 cannot be dropped: Examples A.1.9 and A.2.2 of the book show the inequalities fail without it.

Formalization scope

• Types. $S$ is any type with [Countable S]. Probabilities are ℝ≥0∞-valued with ∑' j, P j = 1, and $P_j(N)$ is Q N j. Extended-real values are EReal, and nonnegative extended values (A.1.7, A.1.8) are ℝ≥0∞. Limits and lower and upper limits are along atTop in ℕ. The book's $N\ge N_0$ convention (Remark A.1.2) needs nothing extra, since only large $N$ matter.
• Sums over $S_N$ are sums over $S$ of (SN N).indicator (Q N) times the function. Values of $u(j,N)$ and $P_j(N)$ for $j\notin S_N$ never enter any statement, and the hypotheses on $u$ ($u\ge -L$, $|u|\le w$) are imposed only on $S_N$, as in the book.
• Weighted sums are wsum, the difference of the weighted positive and negative parts, each in [0,∞]. When both are infinite the book's sum is undefined and wsum returns $-\infty$. Every sum used in a hypothesis or conclusion is defined, except possibly for finitely many $N$ in limit statements, where it does not matter.
• Limits of $u(j,N)$ and $w(j,N)$ are taken in EReal, since the book allows extended-real limits (p. 271). The hypotheses force them to be finite wherever $P_j>0$.
• Ruled out. Statements in which wsum returns its junk value $-\infty$ could make an inequality trivial. Every left-hand side here is a lower limit of sums whose negative parts are bounded, or a limit of eventually defined sums, so no statement holds only because of that junk value. Real-valued tsum with its junk value $0$ is not used anywhere.
• Welcome contributions. A proof of A.1.7 from lintegral_liminf_le for the counting measure, and lemmas relating wsum to Mathlib's tsum and to integrals against Measure.sum (fun j => P j • dirac j), can be reused by the other missions of this series.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999, Appendix A, pp. 270–278. https://doi.org/10.1002/9780470317037
• H. L. Royden, Real Analysis, 3rd ed., Macmillan, 1988, Chapter 4 (Fatou's lemma, generalized Lebesgue convergence theorem).
• The Mathlib Community, The Lean Mathematical Library, CPP 2020, https://doi.org/10.1145/3372885.3373824 (MeasureTheory.lintegral_liminf_le, MeasureTheory.tendsto_integral_of_dominated_convergence).

Motivation

In the theory of Markov decision chains two cost criteria dominate: the discounted cost, in which a cost incurred at time $n$ is weighted by $\alpha^n$ for a discount factor $\alpha \in (0,1)$, and the average cost, the long-run cost per unit time. A standard route to average cost optimal policies is to solve the discounted problem and let $\alpha \to 1^-$. That route needs a precise link between the two criteria for a single sequence of expected costs $u_0, u_1, u_2, \dots \ge 0$: the discounted cost multiplied by $1-\alpha$ on one side, the running average on the other. Appendix A.4 of Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) supplies this link as Theorem A.4.2, and the book invokes it whenever it passes from discounted to average cost (for instance in Chapter 6, where it is applied to $u_n = E_\theta[C(X_n, A_n)]$).

The result belongs to classical summability theory.

• Abelian direction. Convergence of averages implies convergence of the power-series (Abel) means: a consequence of Abel's and Frobenius's theorems on power series (19th century).
• Tauber (1897). The first converse, under a growth condition on the terms.
• Hardy and Littlewood (1914). The converse for Cesàro means of nonnegative terms, the "Hardy–Littlewood Tauberian theorem".
• Karamata (1930). A short proof of that converse by polynomial approximation, reproduced in Titchmarsh, The Theory of Functions (1939, pp. 227–229). The book follows this proof.
• Widder (1941). The continuous-time (Laplace transform) version.
• Sennott (1986b). A proof of the discrete statement, cited by the book as its source for Theorem A.4.2.

Setting

Let $u_0, u_1, u_2, \dots$ be nonnegative terms $u_n \in [0, \infty]$ with $u_0 < \infty$. For $\alpha \in [0, \infty)$ the power series

$$U(\alpha) = \sum_{n=0}^{\infty} \alpha^n u_n \in [0, \infty]$$

always has a sum, possibly $+\infty$, because its partial sums increase. Its radius of convergence is $R = (\limsup_{n} u_n^{1/n})^{-1} \in [0,\infty]$. The partial sums are $w_n = \sum_{k=0}^{n-1} u_k$ for $n \ge 1$. Two ways of averaging the sequence are compared:

• the Cesàro means $w_n / n$, as $n \to \infty$;
• the Abel means $(1-\alpha) U(\alpha)$, as $\alpha \to 1^-$ (from below).

For the constant sequence $u_n \equiv B$ both equal $B$. In the Lean development these are U, radius, w, cesaroMean and abelMean in the namespace SennottDP.Tauberian, all valued in ℝ≥0∞. The proof also uses the function $r$ of Fig. A.1, equal to $0$ on $(0, e^{-1})$ and to $1/x$ on $[e^{-1}, 1)$.

Formalization targets

Goal: Theorem A.4.2

$$\liminf_{n\to\infty} \frac{w_n}{n} \le \liminf_{\alpha\to 1^-} (1-\alpha)U(\alpha) \le \limsup_{\alpha\to 1^-} (1-\alpha)U(\alpha) \le \limsup_{n\to\infty} \frac{w_n}{n}, \tag{A.28}$$

and the following are equivalent: (i) all terms in (A.28) are equal and finite; (ii) $\lim_n w_n/n$ exists and is finite; (iii) $\lim_{\alpha \to 1^-} (1-\alpha)U(\alpha)$ exists and is finite.

No growth or boundedness condition on $u_n$ is assumed: nonnegativity is the only Tauberian condition.

Milestones

1. Remark A.3.3: the geometric series. $R = 1$, $U(\alpha) = B/(1-\alpha)$ and $B\sum_n n\alpha^n = B\alpha/(1-\alpha)^2$.
2. Remark A.3.1: inside the radius of convergence, $U$ is differentiable term by term, and the derived series has the same radius.
3. Eq. (A.31): $\big(\sum \alpha^n\big) U(\alpha) = \sum_n \alpha^n w_{n+1} = U(\alpha)/(1-\alpha)$.
4. Eq. (A.28): the Abelian inequalities on their own.
5. Eq. (A.26): $\int_0^1 r = 1$.
6. Lemma A.4.1: continuous $s^* \le r \le s$ with integrals within $\varepsilon$ of $1$.
7. Eqs. (A.35)–(A.36): if the Abel means tend to $L < \infty$, then $(1-\alpha)\sum_n \alpha^n u_n f(\alpha^n) \to L\int_0^1 f$ for $f(x) = x^k$.
8. The same statement for every $f$ continuous on $[0,1]$.
9. The same statement for $f = r$.
10. Example A.5.1: a $0/1$ block sequence with $\liminf w_n/n = 1/2$ and $\limsup w_n/n = 2/3$ (Choice One) or $1$ (Choice Two), for which the middle inequality of (A.28) is strict.

Significance

The result itself. Theorem A.4.2 lets every statement about $\lim_{\alpha\to1^-}(1-\alpha)V_\alpha$ for a discounted value be read as a statement about long-run average cost, and conversely. The strict cases of Example A.5.1 show why the book must work with $\liminf$ and $\limsup$ rather than limits: average costs of policies need not exist as limits, even for bounded costs.

Formalizing it. Mathlib contains Abel's theorem for convergent series (Mathlib/Analysis/Complex/AbelLimit.lean) and Cesàro convergence of convergent sequences, but no Tauberian theorem. The pinned checkout has no file mentioning "Tauberian", and neither does the platform. The mathematics has been proved since 1914. Formalizing it here adds:

• a machine-checked Hardy–Littlewood–Karamata theorem for nonnegative $[0,\infty]$-valued sequences;
• the $\liminf$/$\limsup$ comparison (A.28) with infinite values allowed;
• a reusable component for the average cost chapters of this series.

Difficulty

The Abelian inequalities (A.28) follow from rearranging the series. The converse (iii) ⇒ (ii) does not: the first idea, recovering $w_n/n$ from $(1-\alpha)U(\alpha)$ at $\alpha = 1 - 1/n$, fails, because knowing $U$ near $1$ controls only weighted averages of all the $u_k$, not a sharp truncation. Some positivity argument is unavoidable, since the converse fails for signed sequences (for example $u_n = (-1)^n n$). The sharp truncation at $n \approx (-\ln\alpha)^{-1}$ corresponds to the discontinuous weight $r$. Passing from polynomial weights to the jump function $r$ requires uniform approximation together with the nonnegativity of the $u_n$ at every step.

The infinite values add bookkeeping. A single $u_{n_0} = \infty$ makes every term of (A.28) infinite, and $R < 1$ forces $U(\alpha) = \infty$ on $(R,1)$.

Formalization scope

Conventions the statements commit to:

• Values. Terms $u : \mathbb{N} \to [0,\infty]$ (ℝ≥0∞) with $u_0 \ne \infty$. $U$, the Abel means, $w_n$ and the Cesàro means are ℝ≥0∞-valued, with ℝ≥0∞ sums (no summability side conditions).
• Limits. $\liminf$ and $\limsup$ are those of the complete lattice $[0,\infty]$, never real liminf. "Exists and is finite" means convergence in $[0,\infty]$ to some $L \ne \infty$.
• Discount factor. $\alpha \in \mathbb{R}_{\ge 0}$, and $\alpha \to 1^-$ is the filter 𝓝[<] 1.
• Index $n = 0$. $n \to \infty$ is atTop on $\mathbb{N}$; the value $w_0/0 = 0$ is irrelevant.
• The equivalence is List.TFAE.
• The function $r$. Its value at the jump is $r(e^{-1}) = e$ (Fig. A.1).
• Continuity. In Lemma A.4.1 and in the continuous-weight step, continuity is required on the closed interval $[0,1]$, which is what the Weierstrass approximation step uses. The book writes "$(0,1)$".
• Finite terms. Remark A.3.1 is stated for finite terms, which the book's discussion of the radius presumes.

A trivializing formalization is ruled out. Real-valued $\liminf$/$\limsup$ would make (A.28) hold by junk values on unbounded sequences; hypotheses such as boundedness of $u_n$ would replace the theorem by an easier special case; and a definition of "exists and is finite" allowing $L = \infty$ would make (ii) hold for $u_n = n$. None of these is used. As sanity checks: for $u_n \equiv 1$ all four terms of (A.28) equal $1$, and for $u_n = n$ all equal $\infty$ and (i)–(iii) all fail.

A complete development needs:

• Cauchy products of $[0,\infty]$-valued power series;
• the Weierstrass approximation theorem, which Mathlib has (polynomialFunctions.topologicalClosure);
• interval integrals of step-like functions;
• $\liminf$/$\limsup$ manipulation along 𝓝[<] 1.

Reusable beyond this mission: the ℝ≥0∞ power-series toolkit and the Karamata argument for general continuous weights (milestone 8). Contributions welcome: proofs of any milestone, and alternative proofs of (iii) ⇒ (ii).

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix A.3–A.5, pp. 279–287. https://doi.org/10.1002/9780470317037
• E. C. Titchmarsh, The Theory of Functions, 2nd ed., Oxford University Press, 1939, pp. 227–229 (Karamata's proof).
• J. Karamata, "Über die Hardy–Littlewoodschen Umkehrungen des Abelschen Stetigkeitssatzes", Mathematische Zeitschrift 32 (1930), 319–320.
• G. H. Hardy and J. E. Littlewood, "Tauberian theorems concerning power series and Dirichlet's series whose coefficients are positive", Proc. London Math. Soc. (2) 13 (1914), 174–191.
• D. V. Widder, The Laplace Transform, Princeton University Press, 1941.
• L. I. Sennott, "A new condition for the existence of optimum stationary policies in average cost Markov decision processes — unbounded cost case", Proc. 25th IEEE Conference on Decision and Control, Athens, 1986, pp. 1719–1721 (cited by the book as Sennott 1986b).
• T. M. Liggett and S. A. Lippman, "Short notes: Stochastic games with perfect information and time average payoff", SIAM Review 11 (1969), 604–607. https://doi.org/10.1137/1011093