Motivation

Almost every model in queueing theory is analysed through a Markov chain. The number of customers in an M/M/c queue is a continuous-time birth–death chain; the number left behind by departing customers of an M/G/1 queue is a discrete-parameter chain on $\{0,1,2,\dots\}$ (the imbedded Markov chain); networks of queues are chains on vectors of queue lengths. Before any steady-state formula (Erlang's formulas, the Pollaczek–Khintchine formula, product forms) can be used, one has to know that the chain has a steady state at all: that it is positive recurrent, so that a stationary distribution exists and equals the limiting distribution.

Chapter 1 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), collects the two ingredients the rest of the book stands on: the Poisson process with its exponential interarrival times (§§1.7–1.8), and the classification theory of discrete-parameter Markov chains (§1.9), ending with Foster's criterion (Theorem 1.2), a sufficient condition for positive recurrence in terms of a drift inequality. The criterion goes back to F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24 (1953) (DOI 10.1214/aoms/1177728976), and is the ancestor of the Foster–Lyapunov method used for stability of queueing networks and stochastic systems.

This mission is the first of a series formalizing the book chapter by chapter.

Setting

A homogeneous discrete-parameter Markov chain on $\{0,1,2,\dots\}$ is given by a transition matrix $P=\{p_{ij}\}$ with $p_{ij}\ge0$ and $\sum_j p_{ij}=1$ for every $i$. The $m$-step transition probabilities $p_{ij}^{(m)}$ are the entries of $P^m$.

The first-passage probability $f_{ij}^{(n)}$ is the probability that the chain started in $i$ enters $j$ for the first time at step $n\ge1$; for $i=j$ it is the probability of first return at step $n$. The return probability is $f_{jj}=\sum_{n\ge1}f_{jj}^{(n)}$ and the mean recurrence time is $m_{jj}=\sum_{n\ge1}n f_{jj}^{(n)}\in[0,\infty]$. A state is positive recurrent if $f_{jj}=1$ and $m_{jj}<\infty$; the chain is positive recurrent if every state is.

The chain is irreducible if for every pair of states $(i,j)$ some $p_{ij}^{(n)}$ is positive, and aperiodic if for every state $k$ the greatest common divisor of $\{n\ge1:p_{kk}^{(n)}>0\}$ is $1$. A stationary distribution is a probability vector $\pi$ with $\pi=\pi P$, i.e. $\pi_j=\sum_i\pi_i p_{ij}$ for every $j$.

For the Poisson part, $T_0,T_1,\dots$ are independent interarrival times, each exponentially distributed with rate $\lambda>0$; the arrival epochs are $S_n=T_0+\dots+T_{n-1}$, and $N(t)=\#\{n\ge1:S_n\le t\}$ counts the arrivals in $[0,t]$.

Formalization targets

Goal: Theorem 1.2 (Foster's criterion)

An irreducible, aperiodic chain is positive recurrent if there exist $x_j\ge0$ with

$$\sum_{j=0}^\infty p_{ij}x_j\le x_i-1\quad(i\ne0),\qquad\sum_{j=0}^\infty p_{0j}x_j<\infty .$$

Milestones: the Markov chain theorems

• Theorem 1.1(a). In an irreducible, positive recurrent chain, $\pi_j=1/m_{jj}$ is a stationary distribution, and it is the only one.
• Theorem 1.1(c). If moreover the chain is aperiodic and all moments of $\pi$ are finite, then $\lim_{m\to\infty}p_{ij}^{(m)}=\pi_j$ for all $i,j$.

Milestones: the Poisson process and the exponential distribution

• Eqs. (1.11)–(1.14). The unique solution of $p_0'=-\lambda p_0$, $p_n'=-\lambda p_n+\lambda p_{n-1}$ with $p_0(0)=1$, $p_n(0)=0$ is $p_n(t)=(\lambda t)^n e^{-\lambda t}/n!$.
• Eq. (1.15). With exponential interarrival times,

$$\Pr\{N(t)\le n\}=\int_t^\infty\frac{\lambda(\lambda x)^n}{n!}e^{-\lambda x}dx=\sum_{i=0}^n\frac{(\lambda t)^ie^{-\lambda t}}{i!}.$$

• Eq. (1.16). Given $N(L)=k$, the arrival epochs have density $k!/L^k$ on $\{0<t_1<\dots<t_k<L\}$.
• Eq. (1.17) and its converse (p.21). The exponential law satisfies $\Pr\{T\le t_1\mid T\ge t_0\}=\Pr\{0\le T\le t_1-t_0\}$, and it is the only continuous distribution on $[0,\infty)$ that does.
• Nonhomogeneous Poisson law (p.22). With a continuous rate $\lambda(t)$ the forward equations have the unique solution $p_n(t)=e^{-m(t)}m(t)^n/n!$, $m(t)=\int_0^t\lambda(s)\,ds$.

Significance

Foster's criterion reduces positive recurrence, a statement about return times, to exhibiting one test function $x$ with negative drift outside a single state. In the book it is the tool that establishes the existence of steady state for imbedded chains of the M/G/1 and G/M/1 queues (Chapter 5); its generalizations are the standard stability proofs for queueing networks. Theorem 1.1 then supplies what positive recurrence buys: the stationary distribution exists, is unique, equals $1/m_{jj}$, and is the limit of the transition probabilities. The Poisson results justify the "Markovian" arrivals and services of Chapters 2–4.

All of these results are classical and proved in the literature; the book states Theorems 1.1 and 1.2 without proof. The Prove2Me platform already holds machine-checked versions of related Markov chain theorems in other missions (Levin–Peres–Wilmer's and Durrett's countable-chain convergence theorems), stated with different definitions and hypotheses. What this mission adds is a formal development in the book's own terms — first-passage probabilities $f_{jj}^{(n)}$, mean recurrence times $m_{jj}$, gcd periodicity — on which the later missions of the series (imbedded chains, birth–death processes) can build, together with a formal proof of Foster's criterion, which is not on the platform.

Difficulty

For Foster's criterion the natural first step, taking expectations of the drift inequality along the chain, only shows that the expected value of $x$ decreases while the chain stays away from $0$. Turning that into a bound on the expected return time to $0$ requires an optional-stopping or telescoping argument over a random time, with the value $x$ possibly unbounded, and a separate argument that positive recurrence of state $0$ propagates to all states of an irreducible chain. The book's hypotheses include aperiodicity, which the argument does not use.

For Theorem 1.1, identifying the stationary distribution with $1/m_{jj}$ requires relating the matrix powers $P^n$ to the first-passage probabilities (a renewal decomposition), and uniqueness over countably many states needs care with infinite sums. For the Poisson results, the difficulty is measure-theoretic: the distribution of the sum of $n+1$ exponential variables, and conditioning on the event $\{N(L)=k\}$ for the order-statistics property.

Formalization scope

States are natural numbers; the transition matrix is a real function $p:\mathbb N\times\mathbb N\to\mathbb R$ with nonnegative entries and rows summing to one (as a convergent series). The return probability and the mean recurrence time are valued in $[0,\infty]$, so null recurrence ($m_{jj}=\infty$) is representable. Irreducibility is the per-pair notion. Stationary equations are stated componentwise with convergent series.

In Foster's criterion the series $\sum_j p_{ij}x_j$ are required to converge for every $i$, which is the book's condition $\sum_j p_{0j}x_j<\infty$ together with the finiteness implicit in the inequalities for $i\ne0$; $x$ is real-valued and nonnegative. Dropping the convergence requirement would let a divergent row series (whose Lean sum is $0$) satisfy the inequality vacuously; allowing $x_j=\infty$ would make the hypothesis trivially satisfiable. Neither is permitted.

The closed forms stated explicitly are: $\pi_j=1/m_{jj}$ (Theorem 1.1(a), with both existence and uniqueness), the Poisson probabilities $(\lambda t)^ne^{-\lambda t}/n!$ (1.14), the Erlang tail integral and the Poisson CDF (1.15), the density $k!/L^k$ (1.16), and $e^{-m(t)}m(t)^n/n!$ for the nonhomogeneous law. Equations (1.14) and the nonhomogeneous law are stated as "solves the equations with the initial conditions if and only if equals the closed form", so both existence and uniqueness are asserted.

The Poisson results use random variables on a probability space, with Mathlib's expMeasure for the exponential law and cond for conditional probability. The derivation of the forward equations from the $o(\Delta t)$ axioms of §1.7 is not formalized; the Poisson law is reached from the equations and, separately, from exponential interarrival times.

Not formalized: Theorem 1.1(b) and the word "ergodic" in 1.1(c), which rest on the book's informal notion of ergodicity; Theorem 1.3, whose phrase "for Theorem 1.1 to be valid" for a continuous-time chain is not pinned down.

The Markov chain definitions are reusable by every later mission that studies an imbedded chain. Contributions welcome: proofs of the milestones, and supporting lemmas (Chapman–Kolmogorov, renewal decomposition of $p_{jj}^{(n)}$, class properties of recurrence).

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Annals of Mathematical Statistics 24 (1953), 355–360. https://doi.org/10.1214/aoms/1177728976

Motivation

Queueing control problems (admission control, routing, service rate selection) are naturally modelled as Markov decision chains with a countably infinite state space and unbounded costs, for instance a holding cost that grows with the queue length. For such models the long-run average cost criterion is often the relevant one, and the central question is whether an optimal stationary policy exists and can be computed from an average cost optimality equation (ACOE). Chapter 7 of Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037) develops a verifiable set of conditions, the (SEN) assumptions, under which an average cost optimality inequality (ACOI) holds and yields an optimal stationary policy. The inequality may be strict (Example 7.3.1), and an optimal policy may induce a Markov chain without positive recurrent states.

Sections 7.4 and 7.5 answer two practical questions: when is the ACOI in fact an equation, and how can (SEN) be checked in a concrete model? The answer culminates in the (BOR) assumptions, which require only one well-behaved stationary policy and the finiteness of a set of low-cost states.

According to the book's bibliographic notes (p. 163): the (BOR) assumptions modify a line of development due to Borkar (SIAM J. Control Optim. 22, 1984, and 27, 1989; monograph 1991) and are weaker than his original conditions; the proof that (BOR) implies (SEN) is from Cavazos-Cadena and Sennott (Oper. Res. Letters 11, 1992), and the version of (BOR) used here is from Sennott (Prob. Eng. Inform. Sci. 7, 1993). Proposition 7.5.5 and the (CAV*) assumptions go back to Cavazos-Cadena (Kybernetika 25, 1989); Proposition 7.5.3 and Corollary 7.5.4 to Sennott (Oper. Res. 37, 1989).

Setting

A Markov decision chain consists of a countable state space $S$, finite nonempty action sets $A_i$, nonnegative finite costs $C(i,a)$ and transition probabilities $P_{ij}(a)$. A policy $\theta$ may use the whole history and randomize. For $\alpha\in(0,1)$ the discount value function is $V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i)$, the infimum of $\sum_t\alpha^tE_\theta[C(X_t,A_t)\mid X_0=i]$; the average cost of $\theta$ is $J_\theta(i)=\limsup_n\frac1nE_\theta[\sum_{t<n}C(X_t,A_t)\mid X_0=i]$ and the minimum average cost is $J(i)=\inf_\theta J_\theta(i)$. All of these lie in $[0,\infty]$.

For a distinguished state $z$ the relative value is $h_\alpha(i)=V_\alpha(i)-V_\alpha(z)$. The (SEN) assumptions are: (SEN1) $(1-\alpha)V_\alpha(z)$ is bounded on $(0,1)$; (SEN2) $h_\alpha\le M$ for a finite function $M\ge0$; (SEN3) $h_\alpha\ge-L$ for a finite constant $L\ge0$. Under (SEN), $J=\lim_{\alpha\to1^-}(1-\alpha)V_\alpha(i)$ is a finite constant, and a limit function $h$ is a pointwise limit of $h_{\beta_n}$ along some $\beta_n\to1^-$. The ACOI and ACOE read

$$J+h(i)\ \ge\ (\text{resp. }=)\ \min_{a\in A_i}\Big\{C(i,a)+\sum_jP_{ij}(a)h(j)\Big\},\qquad i\in S.$$

For a nonempty set $G$ the first passage time is $T=\min\{n\ge1:X_n\in G\}$. The class $\Re(i,G)$ consists of the policies that, from $i$, enter $G$ with probability one in finite expected time $m_{iG}(\theta)$; $\Re^*(i,G)$ adds a finite expected first passage cost $c_{iG}(\theta)=E_\theta[\sum_{t<T}C(X_t,A_t)]$. A (randomized) stationary policy $d$ is $z$ standard if the Markov chain it induces has $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$; it then has a single positive recurrent class $R_d\ni z$ and a finite constant average cost $J_d$.

Formalization targets

Goal: Theorem 7.5.6

Assume (BOR): (BOR1) a $z$ standard policy $d$ exists; (BOR2) for some $\varepsilon>0$ the set $D=\{i: C(i,a)\le J_d+\varepsilon\text{ for some }a\}$ is finite; (BOR3) every $i\in D-R_d$ can be reached from $z$ by some $\theta_i\in\Re^*(z,i)$. Then (SEN) holds and every limit function satisfies the ACOE; every average cost optimal stationary policy $e$ has a positive recurrent state in

$$D(e)=\{i: C(i,e)\le J+\varepsilon\},$$

at most $|D(e)|$ positive recurrent classes and no null recurrent class; and a policy realizing the minimum in the ACOE satisfies $e\in\Re^*(i,D(e)\cap R(e))$ for every $i$.

Milestones

• Lemma 7.4.1: $h_\alpha(i)\le c_{iz}(\theta_i)$ for $\theta_i\in\Re^*(i,z)$, hence (SEN2).
• Lemma 7.4.2: $h(i)\le c_{iG}(\theta)-Jm_{iG}(\theta)+E_\theta[h(X_T)]$ for $\theta\in\Re(i,G)$ under an integrability condition.
• Theorem 7.4.3: four sufficient conditions for equality in the ACOI at a state.
• Lemma 7.5.2: $J_d=(1-\alpha)\sum_{i\in R}\pi_i(d)V_{d,\alpha}(i)$ for a $z$ standard $d$.
• Proposition 7.5.3: a $z$ standard policy gives (SEN1–2).
• Corollary 7.5.4: on $S=\{0,1,\dots\}$, increasing $V_\alpha$ plus a $0$ standard policy gives (SEN), with nonnegative increasing limit functions.
• Proposition 7.5.5: an optimal stationary policy has a positive recurrent state of cost at most $J+\varepsilon$, reachable from $i$, when (7.33) holds.
• Corollaries 7.5.9 and 7.5.10: the (CAV) and (CAV*) conditions imply (BOR).

Significance

Theorem 7.5.6 reduces the verification of the ACOE for a queueing model to three checks that do not involve the discount value function: exhibit one stationary policy with finite mean return times and costs to a fixed state (typically a stable "serve at maximal rate" policy), check that low costs occur on a finite set (automatic when the holding cost grows without bound, Corollaries 7.5.9–7.5.10), and check reachability of finitely many states. Its conclusions go beyond existence: optimal stationary policies induce chains with positive recurrent classes located in a known finite set, and ACOE-realizing policies reach them in finite expected time and cost. This is what makes value iteration and approximating-sequence methods in later chapters of the book applicable to these models.

The results are proved in the book. The present mission produces machine-checked statements of the first passage calculus for general (history-dependent, randomized) policies, of (SEN) and limit functions, and of the chain of implications from (CAV*) to the ACOE. No machine-checked version of these statements is known.

Difficulty

The obvious approach to the ACOE is to pass to the limit $\alpha\to1^-$ in the discount optimality equation. Exchanging this limit with $\sum_jP_{ij}(a)h_\alpha(j)$ requires a dominating function, and (SEN2) only gives a pointwise bound $M$ whose expectation may be infinite; Fatou's lemma then yields only the inequality. Obtaining equality requires tracking first passages to sets and showing that the discrepancy $\Phi$ vanishes along them, which in turn needs finiteness of $c_{iG}$ that is not assumed but has to be derived. On the recurrence side, the average cost criterion is a limit superior of Cesàro averages over a countable state space, and mass can escape to infinity; the finiteness of the set $D$ is what prevents an optimal policy from spending its time in transient or null recurrent states, and turning that into positive recurrence requires the renewal-type identities of Appendix C.

Formalization scope

States form a countable type $S$; action sets are nonempty Finsets; costs are in ℝ≥0; transition probabilities are ℝ≥0∞-valued with row sums one on admissible actions. Policies are general: a history is a state sequence and an action sequence, and all probabilities and expectations (hitting probabilities, $m_{iG}$, $c_{iG}$, $P_\theta(X_T=j)$, $Q^{(n)}_{ij}$) are computed from the history probabilities of the process. $V_\alpha$, $J_\theta$, $m_{iG}$ and $c_{iG}$ take values in $[0,\infty]$; $m_{iG}=\infty$ when $G$ is missed with positive probability; the first passage time satisfies $T\ge1$. $h_\alpha$ and $\sum_jP_{ij}(a)h(j)$ are in the extended reals, with the book's convention that a function bounded below has an expectation in $(-\infty,+\infty]$. Limit functions are real valued. Positive recurrence, communicating classes and steady state probabilities $\pi_j=(m_{jj})^{-1}$ are the notions for the chain induced by a (randomized) stationary policy. $J_d$ is the average cost of $d$ from $z$.

A formalization in which the ACOE is asserted for some convenient function instead of every limit function, or in which $|D(e)|$ is a natural-number cardinality that vanishes on infinite sets, would trivialize part of the goal; the statements quantify over all limit functions and use Set.encard.

A complete development needs: history-dependent policies and their path laws on countable spaces; first passage decompositions (strong Markov property at $T$); Abelian limits of $\sum_t\alpha^tP(T=t)$; Fatou and dominated convergence for series; and the renewal reward theorem for positive recurrent classes (Appendix C of the book). The first passage and Markov chain layer is reusable beyond this mission. Proofs of individual milestones, and sharper statements of the Appendix C facts they use, 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. doi:10.1002/9780470317037
• V. S. Borkar, "On minimum cost per unit time control of Markov chains", SIAM J. Control Optim. 22 (1984), 965–978.
• V. S. Borkar, "Control of Markov chains with long-run average cost criterion: the dynamic programming equations", SIAM J. Control Optim. 27 (1989), 642–657.
• V. S. Borkar, Topics in Controlled Markov Chains, Pitman Research Notes in Mathematics 240, Longman, 1991.
• R. Cavazos-Cadena, "Weak conditions for the existence of optimal stationary policies in average Markov decision chains with unbounded costs", Kybernetika 25 (1989), 145–156.
• R. Cavazos-Cadena and L. I. Sennott, "Comparing recent assumptions for the existence of average optimal stationary policies", Oper. Res. Letters 11 (1992), 33–37.
• L. I. Sennott, "The average cost optimality equation and critical number policies", Prob. Eng. Inform. Sci. 7 (1993).
• L. I. Sennott, "Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs", Operations Research 37 (1989), 626–633. doi:10.1287/opre.37.4.626
• K. L. Chung, Markov Chains with Stationary Transition Probabilities, 2nd ed., Springer, 1967.

Motivation

Queueing control problems (admission control, routing, service-rate selection, flow control) are naturally posed as Markov decision chains with a denumerably infinite state space, such as the number of customers in a buffer, and are usually judged by their long-run average cost per unit time. When the state space is finite, Chapter 6 of Sennott's book shows that an average cost optimal stationary policy always exists. On a countable state space this fails: Section 7.1 of the book gives examples in which no average cost optimal policy exists, and one in which no stationary policy comes within a given distance of the minimum average cost. The question addressed by this mission is under which verifiable conditions on the discounted value functions a countable-state model has a constant minimum average cost and an optimal stationary policy.

Timeline, following the book's bibliographic notes (p. 163). The book names Taylor (1965) and Derman (1966) as earlier pivotal work and Ross (1968), and his 1983 textbook, as the direct predecessor. Sennott (1989, Operations Research 37) weakened Ross's assumptions to cover models with unbounded costs, and proved the main result of Section 7.2; the (SEN) assumptions of Chapter 7 are the cleaner version of Sennott (1993). Cavazos-Cadena (1991) gave the example, adapted as Example 7.3.1 of the book, showing that under these assumptions the optimality inequality can be strict. The weaker (H*) assumptions of Section 7.7 appear, in a slightly different form, in Sennott (1995). Part (iv) of Theorem 7.2.3 is new in the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$, for each state $i$ a finite nonempty action set $A_i$, a nonnegative finite cost $C(i,a)$, and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a) = 1$. A policy $\theta$ chooses the action at time $n$ at random according to a distribution that may depend on the whole history $(X_0, A_0, \dots, X_n)$; a stationary policy $f$ always chooses $f(i) \in A_i$ in state $i$.

For an initial state $i$, the $n$-horizon cost is $v_{\theta,n}(i) = \sum_{t=0}^{n-1} E_\theta[C(X_t,A_t) \mid X_0 = i]$, the average cost is $J_\theta(i) = \limsup_{n} v_{\theta,n}(i)/n$, and the minimum average cost is $J(i) = \inf_\theta J_\theta(i)$ over all policies. A policy is average cost optimal if $J_\theta \equiv J$. For $\alpha \in (0,1)$ the discounted value function is $V_\alpha(i) = \inf_\theta \sum_{t \ge 0} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i]$. All these quantities lie in $[0,\infty]$.

Fix a distinguished state $z$ and put $h_\alpha(i) = V_\alpha(i) - V_\alpha(z)$. The (SEN) assumptions are:

• (SEN1) $(1-\alpha)V_\alpha(z)$ is bounded for $\alpha \in (0,1)$;
• (SEN2) there is a nonnegative finite function $M$ with $h_\alpha(i) \le M(i)$ for all $i$ and $\alpha$;
• (SEN3) there is a nonnegative finite constant $L$ with $-L \le h_\alpha(i)$ for all $i$ and $\alpha$.

A limit function $h$ is a pointwise limit of $h_{\beta_n}$ along some sequence $\beta_n \to 1^-$. If $f_\alpha$ is a stationary policy realizing the discount optimality equation $V_\alpha(i) = \min_a \{C(i,a) + \alpha\sum_j P_{ij}(a)V_\alpha(j)\}$, a limit point $f$ is a stationary policy with $f_{\beta_n}(i) = f(i)$ for large $n$, for each $i$, along some $\beta_n \to 1^-$.

Formalization targets

Goal: Theorem 7.2.3

Under (SEN), there is a finite constant $J = \lim_{\alpha\to1^-}(1-\alpha)V_\alpha(i)$ independent of $i$; limit functions exist, satisfy $-L \le h \le M$ and the average cost optimality inequality (ACOI)

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

every stationary policy realizing the minimum is average cost optimal with $J_e \equiv J$ and $E_e[h(X_n)]/n \to 0$; every limit point of discount optimal stationary policies is average cost optimal and satisfies the corresponding inequality for an associated limit function; and the average cost of any optimal policy is a limit, not only a limit supremum.

Milestones

• Proposition 7.1.1: finitely many initial transitions with finite cost do not change $J_\theta$.
• Lemma 7.2.1: a bounded-below solution $(J,h)$ of the ACOI inequality for a stationary $e$ gives $J_e \le J$.
• Proposition B.6: a sequence of functions squeezed between $-L$ and $M$ on a countable set has a pointwise convergent subsequence.
• Proposition 7.2.4: (SEN) does not depend on the choice of $z$.
• Proposition 7.7.1: (SEN) $\Rightarrow$ (H*) $\Rightarrow$ (H).
• Proposition 7.7.2: the conclusions of Theorem 7.2.3 hold under (H), with a state-dependent lower bound $L(i)$.

Significance

Theorem 7.2.3 is the existence theorem the rest of Chapter 7 builds on (p. 128): the ACOE results of Section 7.4, the (BOR) and (CAV) sufficient conditions of Section 7.5, and the worked queueing models of Section 7.6 all work under (SEN) and invoke it. It justifies computing an average cost optimal policy for a queueing model as a limit of discount optimal policies, and it shows that the minimum average cost is the Abelian limit of the normalized discounted value.

The results are proved in the book and in Sennott (1989, 1993, 1995), but none of them has a machine-checked proof: Mathlib has no Markov decision processes, and the platform's average cost results concern finite state spaces or Borel models with different assumptions. The formalization produces a general-policy, countable-state MDC development with extended-real values, reusable by the later missions of this series.

Difficulty

On a finite state space the relative value functions are bounded and the Abelian limit $(1-\alpha)V_\alpha$ can be controlled directly. Here $h_\alpha$ is bounded above only by a function $M$ that may be unbounded, so passing to the limit in the discounted optimality equation $\sum_j P_{ij}(a)h_\alpha(j)$ cannot use dominated convergence, and in general only an inequality survives in the limit; Example 7.3.1 shows that the inequality in the ACOI can be strict. Showing that a policy realizing the ACOI is optimal requires control of $E_e[h(X_n)]/n$ for a function $h$ that is unbounded above, and part (iv) requires comparing the limit inferior and limit superior of Cesàro averages for an arbitrary, possibly history-dependent optimal policy.

Formalization scope

The state space is any countable type ([Countable S]); actions form a type with finite nonempty Finset action sets; costs are ℝ≥0; transition probabilities, costs over time and value functions are ℝ≥0∞. Policies are general: randomized and history dependent, with histories encoded as finite state and action sequences and the process law built by an explicit recursive product. Finite horizon costs have terminal cost $0$, as the chapter prescribes.

The relative value $h_\alpha(i) = V_\alpha(i) - V_\alpha(z)$ is computed in EReal, never through a truncated real subtraction: a state with $V_\alpha(i) = \infty$ gives $h_\alpha(i) = +\infty$, so (SEN2) cannot hold through a junk value, and (SEN1) is a bound by a finite constant that itself forces $V_\alpha(z) < \infty$. Sums $\sum_j P_{ij}(a)h(j)$ and expectations $E[h(X_n)]$ of real functions are extended reals, computed as positive part minus negative part; they are never Bochner integrals and never default to $0$ when not summable. The limit $\alpha \to 1^-$ is the filter 𝓝[<] 1. Limit functions and limit points follow Definition 7.2.2 literally, over arbitrary sequences $\alpha_n \to 1^-$ in $(0,1)$, and the (SEN), (H), (H*) sets are predicates carrying their witnesses $M$ and $L$.

A development that bounds only $h_\alpha$ as a free function, rather than the one built from the infimum over all policies, or that quantifies only over stationary policies in $J(i)$, proves a different and weaker theorem and does not count.

Needed infrastructure: the law of the controlled process under a general policy, monotone and Fatou-type limit interchanges for countable sums, the Abelian inequality $\limsup(1-\alpha)\sum\alpha^t c_t \le \limsup \frac1n\sum_{t<n}c_t$ (Proposition 6.1.1 of the book), and the existence and optimality of discount optimal stationary policies (Theorem 4.1.4). The MDC layer and these two results are shared with other missions of the series; contributions to them are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Chapter 7 (pp. 127–166) and Appendix B. https://doi.org/10.1002/9780470317037
• L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Operations Research 37 (1989) 626–633. https://doi.org/10.1287/opre.37.4.626
• L. I. Sennott, The average cost optimality equation and critical number policies, Probability in the Engineering and Informational Sciences 7 (1993). (Cited in the book's bibliography, p. 321.)
• L. I. Sennott, Another set of conditions for average optimality in Markov control processes, Systems & Control Letters 24 (1995) 147–151. (Cited in the book's bibliography.)
• R. Cavazos-Cadena, A counterexample on the optimality equation in Markov decision chains with the average cost criterion, Systems & Control Letters 16 (1991) 387–392. (Cited in the book's bibliography.)
• S. M. Ross, Non-discounted denumerable Markovian decision models, Annals of Mathematical Statistics 39 (1968) 412–423. (Cited in the book's bibliography.)
• H. M. Taylor, Markovian sequential replacement processes, Annals of Mathematical Statistics 36 (1965) 1677–1694. (Cited in the book's bibliography.)
• E. A. Feinberg and Y. Liang, On the optimality equation for average cost Markov decision processes and its validity for inventory control; formalized on Prove2Me in the mission of the same name (Borel state spaces, a different model).

Motivation

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

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

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

Setting

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

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

The mean of $X(t)$ is

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

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

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

Formalization targets

Goal: Theorem 13 (p. 216)

For every $t \ge 0$,

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Strassen's Theorems and the Stochastic Ordering of Queues

Background

Chapters 1–3 of Baccelli and Brémaud's Elements of Queueing Theory compute exact quantities: Palm identities, stability criteria, PASTA, Pollaczek–Khinchin. Chapter 4 asks a different question. When you cannot compute a queue, can you at least say it is better than another one?

That requires an order on distributions. The chapter builds a family of them — integral orders — by choosing a class ℒ of test functions and declaring F ≤_ℒ G when ∫f dF ≤ ∫f dG for all f ∈ ℒ. Three matter: {i} the non-decreasing functions, giving the strong (stochastic) order; {cx} the convex functions, giving the convex order; and their intersection {icx}.

The goal

An integral order compares two distributions that need not live on the same probability space, and that is both its convenience and its difficulty. Strassen's theorems say each of these orders is secretly a statement about a coupling.

Theorem 4.2.2 (p.278), Strassen's ≤_cx theorem:

F ≤_cx G   ⟺   ∃ X ~ F, Y ~ G on one space with  E[Y | X] = X  a.s.
F ≤_icx G  ⟺   the same with  E[Y | X] ≥ X  a.s.

The convex order holds exactly when G is a martingale dilation of F — obtained by spreading each point out without moving its conditional mean. That is what makes the order usable: comparison results for queues become induction arguments on a coupling instead of analytic manipulations of convolutions of c.d.f.'s.

Its companion Theorem 4.2.1 is the ≤_st version, where the coupling is the simpler X ≤ Y a.s. In dimension one both are explicit — take X = F⁻¹(U), Y = G⁻¹(U) for a uniform U. In dimension n there is no such formula, and that is why these are Strassen's theorems. The book attributes both to Strassen (1965) and proves neither.

Why FIFO is optimal

§4.1 is a different kind of comparison: not between two queues, but between two service disciplines for the same queue. The order there is majorization ≺, which compares how spread out two vectors of the same total are.

The answer is that FIFO minimizes E⁰[f(V)] for every convex f (Property 4.1.3), and the proof is an interchange argument. Under any non-preemptive discipline that uses no information on the service times, customer k effectively receives service σ_{γ(k)} for some permutation γ; Lemma 4.1.3 shows the same queue is produced by FIFO fed with that reordered input, and that the reordering does not change the law of the input. Lemma 4.1.4 passes to the limit, which needs ρ < 1. Lemmas 4.1.1 and 4.1.2 then do the combinatorics: undoing one inversion of γ makes the waiting-time vector less spread out, so the identity permutation — FIFO — is extremal.

Feller's paradox, and what survives it

§4.4 compares time-stationary queues, and opens with a warning. T_n[P⁰] ≤_i T̃_n[P̃⁰] for every n does not imply T_n[P] ≤_i T̃_n[P̃]: Example 4.4.1, "Feller's paradox revisited", exhibits a Poisson process and a renewal process where the Palm order holds and the stationary one fails. The order does not pass from the Palm probability to the stationary one.

For ≤_cx it does. Lemma 4.4.1 is why: it expands E_P[f(N[0,x))] as a series of second differences of f against Palm expectations, and a convex f makes every coefficient non-negative. Lemma 4.4.2 handles the S-orders, built by dividing Palm integrals by the mean cycle length, and shows that the normalisation does not hide the comparison it normalises by.

Formalization scope

• Orders. ≤_i, ≤_cx, ≤_icx on distributions on ℝⁿ are integral orders over the book's test classes (§4.2.1), with the page's qualification that only test functions with well-defined integrals count. Majorization ≺ is (4.1.2) with increasing reorderings of both vectors.
• Strassen. Both theorems are stated as equivalences, with the coupling existential over the probability space. Theorem 4.2.2 carries both clauses — E[Y | X] = X for ≤_cx, E[Y | X] ≥ X for ≤_icx, as conditional expectations given σ(X) — and assumes both distributions integrable; Theorem 4.2.1 has no integrability hypothesis. A one-directional statement (the Jensen half) is not the theorem.
• The queue of §4.1.3 is constructed: a GI/GI input (i.i.d. inter-arrival and service times, independent), a single work-conserving server started empty, and any non-preemptive discipline whose choices are measurable in the information the book's σ-field 𝒢_t carries (arrivals, service times of customers already started) plus external randomisation. FIFO is one such discipline. The interchange permutations γ_n and their limit γ are built from the schedule as on pp.268–270; Lemma 4.1.4 assumes ρ = E[σ₀]/E[τ₀] < 1.
• Lemma 4.4.1 is stated with the exact second-difference series and assumes that series converges absolutely; the page states it for all f, which fails for heavy-tailed counts and sparse f.
• The S-orders test against {I-ℒ} — primitives ∫_0^t f(u, x) du of test functions — and apply only to distributions whose first coordinate is a.s. positive with a finite mean.

What this mission provides

None of it exists. Mathlib has no stochastic order, no convex order, no increasing-convex order, no majorization, no Schur-convexity and no Strassen theorem; the platform returns zero hits for q=stochastic ordering. Everything in this chapter is new substrate — and §§4.1–4.2 need nothing from Palm calculus, so this mission can be read on its own.

PASTA and the Formulas of Palm Calculus

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds Palm calculus. Chapter 2 settles when a queue has a stationary regime. Chapter 3 is called simply Formulas, and it is what the first two chapters were for: it computes.

The pattern is always the same. A quantity of interest is observed two ways — from a clock fixed in time, and from an arriving customer — and Palm calculus converts between them. Little's law, the Pollaczek–Khinchin formula and the rate conservation principle are all instances.

The goal

Theorem 3.3.1 (p.211) is the one that says when the two views coincide.

This classical result of queueing theory states, in rough terms, that if the arrival point process is Poisson, operational characteristics of the system computed just before arrival times and at arbitrary times are the same (Poisson Arrivals See Time Averages). Some care must be exercised in the application of this principle, and we now give a precise statement, in the θ_t-framework.

E⁰_A[f(Z(0))] = E[f(Z(0))]                                                            (3.3.1)

for every F_t-predictable, flow-compatible {Z(t)} and every non-negative measurable f, whenever A admits the constant F_t-intensity λ; and, under ergodicity,

lim_N (1/N) Σ_{n=1}^N f(Z(T_n)) = lim_T (1/T) ∫_0^T f(Z(s)) ds .                       (3.3.2)

The "some care" is the word predictable. PASTA is false without it: an arrival that changes the state it then observes does not see the time average, and that is exactly what predictability — measurability for the F_t-predictable σ-field, generated by the sets (a,b] × A with A ∈ F_a — rules out.

The hypothesis is the constant F_t-intensity, not "A is Poisson". By Watanabe's theorem the two are equivalent, but that equivalence is a remark on the page and not part of this theorem.

Why it earns its place: Pollaczek–Khinchin

§3.4 derives formulas from conservation equations. Applying the rate conservation principle of Chapter 1 to Y(t) = e^{iuW(t)} in a GI/GI/1/∞ queue gives Takács' formula

iu E[e^{iuW(0)}] = λ E⁰_A[e^{iuW(0−)}] (E[e^{iuσ_0}] − 1) + iu(1 − ρ) ,                (3.4.44)

an identity between a stationary expectation and a Palm expectation of the workload just before an arrival. One substitution turns it into a closed form — and that substitution is PASTA. When the arrivals are Poisson, E⁰_A[e^{iuW(0−)}] = E[e^{iuW(0)}], and

E[e^{iuW(0)}] = iu(1 − ρ) / ( iu − λ(Ψ_σ(u) − 1) ) ,                                   (3.4.45)

the Pollaczek–Khinchin characteristic function formula. The most quoted formula in single-server queueing theory is one application of this mission's goal theorem.

The rest of the chapter

§3.1 carries Little's formula to fluid queues. Lemma 3.1.1 is the set identity that turns the fluid workload into an integral against the arrival measure — the same two instants described from the server's side and from the arrivals' side.

§3.2 applies Campbell's formula to rare events. Lemma 3.2.1 gives a closed form, in a countable-state Markov chain, for the mean time to make an excursion to a rare set and return; its two expressions count the same cycle rate from the two ends. Theorem 3.2.1 generalizes Keilson's asymptotic equivalence to a stationary θ_t-compatible process, replacing cycles by thinnings of the entrance processes of two disjoint sets.

§3.5 applies the stochastic intensity integration formula to a superposition of on-off fluid sources. Lemma 3.5.1 identifies a conditional expectation with a Palm expectation through Papangelou's theorem — the mean workload while a source is idle equals the mean workload that source sees when it wakes. Lemma 3.5.2 measures the gap between the two Palm expectations of the workload taken with respect to a source's start process and its fluid process.

What this mission provides

Nothing here is on the platform or in Mathlib. The nearest platform item, queueing_general_littles_law, is Stidham's deterministic sample-path law; its own docstring disclaims probability, expectation, stationarity, ergodicity and FIFO. Baccelli's L = λW is the Palm identity for a stationary ergodic marked point process, derived from the inversion formula (1.2.25) — an identity between an expectation under P and a Palm expectation under P⁰_N, not a pathwise limit. Different framework, different hypotheses, and neither implies the other.

Mathlib has filtrations and adapted processes but no predictability in the form this chapter needs, and no stochastic intensity.

Formalization scope

• PASTA carries both displays. (3.3.1) is an equality in [0, ∞] for every non-negative measurable f. (3.3.2) asserts that, P-almost surely, both averages converge in [0, ∞] to one common limit, so both limits exist. Predictability is measurability for the predictable σ-field P(F_t) of p.55. The concrete form Z(t,ω) = v(t, θ_t ω) of (1.8.1) is not used as the hypothesis, because for a general history it is strictly weaker. The hypothesis is the constant F_t-intensity, E[A(a,b] | F_a] = λ(b − a), and not "A is Poisson".
• Takács (3.4.44) and Pollaczek–Khinchin (3.4.45) are stated for every real u, and for u ≠ 0 respectively. Their hypotheses are the page's: σ_n is independent of W(T_n−) under P⁰_A, E⁰_A[e^{iuσ_0}] = E[e^{iuσ_0}], P(W(0) = 0) = 1 − ρ, and ρ < 1. The workload is a measurable, flow-compatible solution of Lindley's equation. (3.4.45) adds PASTA's hypotheses for {W(t−)}, and it asserts that its denominator is non-zero.
• Lemma 3.2.1 asserts both closed forms of E_α R. The chain is irreducible, F is non-empty, and hitting times are counted from time 0.
• Theorem 3.2.1 asserts the equality in (3.2.43), the convergence to 1, and E⁰_{F_n(→A)}[τ(F_n)] · Λ_n → 1. Its hypotheses are the section's standing ones: P is flow-invariant, {X(t)} is flow-compatible, and A and every F_n are regular and disjoint.
• Lemmas 3.5.1 and 3.5.2 are stated for the full on-off model of §3.5.3. The on-off point processes are independent, their on periods, off periods and fluid functions are i.i.d. and independent, P⁰_{A^i} is the Palm probability of the random measure A^i, and the workload is the stationary solution of the fluid-queue equation. Lemma 3.5.1 is an identity in [0, ∞]. Lemma 3.5.2 assumes that E⁰_{A^i}[W(0)] and the expectation defining C_i are finite.

A formalization that makes Palm probability an opaque measure with the formulas as axioms, or that weakens predictability to adaptedness, trivializes this mission or makes it false, and is out of scope.

Stationary Regimes of Stochastic Recurrences

Background

Chapter 2 of Baccelli and Brémaud's Elements of Queueing Theory asks when a queue has a stationary regime. §§2.1–2.4 answer it for the single-server and multiserver queues by Loynes' monotone construction. §§2.5 and 2.11 answer it for the general object those constructions are instances of: a stochastic recurrence

W_{n+1} = h(W_n, ξ_n),

driven by a sequence {ξ_n} compatible with an ergodic shift θ. Two questions arise, and this mission is about both.

Exact sampling, and what "exact" means

§2.5.3 treats the finite-state case. An ergodic transition matrix on E = {1, …, r} has a stationary law π, and the classical way to sample it is to run the chain and wait. That gives a sample whose law converges to π and is never equal to it.

Coupling from the past (Propp and Wilson, 1996) does better. Run one chain from every state, all sharing a single array {ξ_k(i)} of i.i.d. uniforms indexed by time and current state, started further and further in the past. Once two chains meet they stay together, so eventually all r coalesce before time 0 — and Theorem 2.5.1 says the common value they reach has the distribution π exactly. Theorem 2.5.2 makes it practical: if the updating function preserves a partial order with a least and a greatest state, and a single uniform sequence drives every chain, the two extremal chains funnel all the others and their coalescence suffices.

Neither theorem is a statement about a program. Each says that a random variable is almost surely finite, and that another has a distribution equal to π.

Renovating events: sufficient, and then necessary

§2.5.4 treats the general case, through Borovkov's idea. An event A_n is renovating of length m when, on it, W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}) — the sequence's value m steps ahead forgets where it came from. Theorem 2.5.3 turns a condition on how often renovating events occur into the existence of a finite stationary solution Z with Z ∘ θ = h(Z, ξ), and into strong backwards coupling: W_n ∘ θ^{-n} is not merely convergent to Z but equal to it after a finite random index.

Corollary 2.5.1 makes the limit independent of the initial condition — one stationary regime, reached from every starting point. Theorem 2.5.4 is the converse: for ℝ₊^K-valued recurrences with a constant initial condition, strong backwards coupling produces renovating events. So the method characterises stability rather than merely detecting it.

The saturation rule

§2.11 treats the multidimensional case, where the state is a vector and the natural models are monotone and homogeneous. Theorem 2.11.1, due to Crandall and Tartar, is the key that unlocks it: under homogeneity, monotone and non-expansive are the same property. That is what puts these models within reach of Kingman's subadditive ergodic theorem, and Theorem 2.11.2 collects the payoff — asymptotic growth rates γ̄ and γ_ exist, both almost surely and in L¹, and do not depend on the initial condition.

The goal

Queueing folklore has a rule of thumb for the stability of an open network: saturate the queues fed by the external stream, measure the departure intensity µ of the saturated system, and declare the network stable when λ < µ. The book is careful that this saturation rule "does not hold for all systems".

Theorem 2.11.3 (p.166), "the main result on the stability region", proves it for Monotone-Homogeneous-Separable networks:

If lim Z_{[-n,0]} → ∞ a.s., then λ γ(0) ≥ 1.    If λ γ(0) > 1, then lim Z_{[-n,0]} → ∞ a.s.

Here γ(c) is the growth rate of the network fed by the scaled process cN, so c = 0 places every arrival at the origin: γ(0) is exactly the saturated system's rate, and µ = γ(0)⁻¹.

Two implications, with a gap between ≥ 1 and > 1 that the book leaves open — as it leaves open the critical case ρ = 1 of Loynes' theorem. Closing it would assert more than is proved.

What this mission provides

Nothing here is on the platform or in Mathlib. There is no coupling from the past, no theory of renovating events, and no Crandall–Tartar theorem. Order/Hom/* has monotone maps and Topology/MetricSpace/* has LipschitzWith 1, which is the right ambient notion for non-expansiveness in the sup-norm, but the equivalence between them under homogeneity is absent.

Formalization scope

• The standing assumptions of §2.5.1 (p.104) are part of every §2.5.4 statement: (P⁰, θ) is ergodic and {ξ_n} is compatible with θ. The relation Z ∘ θ = h(Z, ξ) holds P⁰-a.s.
• Theorem 2.5.4 is stated for {W_n^{[C]}}, the sequence its proof on p.119 builds the renovating events for. The page prints {W_n^{[0]}} in the conclusion, and that version is false. Corollary 2.5.1 uses the renovating condition of (2.5.14), W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}), where the page prints W_n.
• Theorem 2.11.2 carries all four limits, a.s. and in expectation, for every integrable ℝ^K-valued random initial condition Y, under the book's linear lower bound E[X_n^{[0]}] > −Cn.
• The goal is stated on the Palm space of a stationary ergodic marked point process: T_0 = 0, T_n ∘ θ = T_{n+1} − T_1, ξ_n ∘ θ = ξ_{n+1}, E⁰τ_n = λ^{-1}, E⁰Z_n < ∞. The map X satisfies (2.11.16) (it depends only on the points and marks in the index window) and the four framework assumptions for every point process. γ(0) is the a.s. limit of Z_{[-n,-1]}(0·N)/n. Dropping the marks would reduce the theorem to deterministic service, and dropping the link between the points and θ makes the second implication false. Neither is done.
• Stating only one of the goal's two implications, or collapsing them into an equivalence, would be a different theorem. Both implications are stated, with the gap between ≥ 1 and > 1 left open.

The Loynes Stability Theorem and Coupling

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds a calculus for stationary queues. Chapter 2 asks the prior question: when is there a stationary queue at all?

The G/G/1/∞ queue is one server at unit rate, infinite waiting room, fed by a stationary marked point process {(T_n, σ_n)} — arrival epochs and required service times. Its workload W(t), the service still owed by the server, obeys Lindley's equation between arrivals:

W(t) = (W(T_n−) + σ_n − (t − T_n))⁺,    t ∈ [T_n, T_{n+1}).                          (2.1.6)

Nothing in that equation says a solution exists on the whole line, let alone a stationary one. The answer is a sharp criterion in the traffic intensity ρ = λE⁰_A[σ_0].

The goal

Theorem 2.1.1 (p.80), which the book calls "the fundamental result of stability". Under ρ < 1 there is a unique finite workload process on all of ℝ, compatible with the flow, and it is given explicitly by the Loynes supremum

W(0) = sup_{n ≤ 0} ( T_n + Σ_{i=n}^{0} σ_i )⁺ ,                                      (2.1.12)

with W(T_n−) = 0 for infinitely many negative and infinitely many positive n (2.1.13). If ρ > 1 there is no finite stationary workload process at all.

Each half earns its place. The supremum is what "the Loynes construction" means: look back from the origin, take the work brought by customers n, …, 0 less the time −T_n since elapsed, and maximise over how far back you look. The ρ > 1 half is what turns ρ < 1 from a sufficient condition into a criterion. The critical case ρ = 1 is an explicit non-result in the book — there "may or may not" be a stationary workload — and is deliberately absent from the statement.

The route, and what it produces on the way

§2.2 proves the theorem by Loynes' monotone scheme on the Palm space, and two of its steps are worth stating in their own right.

Lemma 2.2.1 (p.87) is the uniqueness engine: a non-negative, a.s. finite Z with Z − Z∘θ ∈ L¹(P⁰) has E⁰[Z − Z∘θ] = 0. Applied to the difference of two stationary solutions, it forces that difference to be invariant, and ergodicity then forces it to be zero.

Theorem 2.2.1 (p.90) runs the argument backwards. Its section is titled "Queueing Proof of the Ergodic Theorem", and it is exactly that: the queueing construction yields the pointwise ergodic theorem, in the ratio form

lim_n ( Σ_{i=0}^n σ∘θ^{-i} ) / ( Σ_{i=0}^n τ∘θ^{-i} ) = E⁰[σ]/E⁰[τ],    P⁰-a.s.

Mathlib has the mean (von Neumann) ergodic theorem and no pointwise one, so this is absent substrate rather than a restatement.

Three extensions

The multiserver queue (§2.3). With s servers and the least-loaded-server rule, the state is the ordered workload vector obeying the Kiefer–Wolfowitz recurrence, and the criterion becomes E⁰[σ] < s E⁰[τ] (Theorem 2.3.1, p.93). Here uniqueness fails: p.94 exhibits a two-point space with a whole interval of stationary solutions. What survives is that the solution set is bracketed — M_∞ is minimal, and V^∞_∞ is the largest finite solution (Theorem 2.3.2, p.95).

Coupling (§2.4). Theorem 2.4.1 (p.99) is what "reaches the stationary regime" means: if a sequence couples with a θ-compatible one, then the law of its whole shifted trajectory converges in variation to the stationary trajectory's. The proof is one inequality, |P̃_{X,k} − P̃_{Z,k}| ≤ P(N > k), and the finiteness of the coupling time.

The fluid queue (§2.7). Theorem 2.7.1 (p.131) replaces customers by two θ_t-compatible random measures, the arrivals A and the service capacity C, and recovers the Loynes supremum W(t) = sup_{u ≤ t}(A_{u,t} − C_{u,t}) under λ < µ — as the minimal solution, the book claiming no uniqueness here.

Formalization scope

• ρ = λE⁰_A[σ_0] takes values in [0, ∞], so an input with E⁰_A[σ_0] = ∞ has ρ = ∞ and falls under the non-existence half rather than being read as ρ = 0.
• The explicit formulas are carried: the Loynes supremum (2.1.12) with the boundedness of its set as a conclusion, the construction points (2.1.13), the ratio limit E⁰[σ]/E⁰[τ] of Theorem 2.2.1, the threshold s E⁰[τ] of Theorem 2.3.1, and the fluid supremum (2.7.7).
• Identities between random variables hold almost surely, as in the book: the workload equations, (2.1.12)–(2.1.13), (2.7.7), and the solutions of (2.3.2). A statement "for every sample point" would be false, because on a null invariant set of sample paths no finite solution exists.
• Uniqueness in Theorem 2.1.1 is among measurable, θ_t-compatible workload processes; maximality in Theorem 2.3.2 is among measurable finite solutions; the coupling time of Theorem 2.4.1 is a random variable. A formalization that dropped the explicit supremum, or the ρ > 1 half, would trivialize the goal and is ruled out.

What this mission provides

None of it is on the platform or in Mathlib. The nearest platform item, single_server_queueing_convergence_of_subcritical, presupposes a stationary workload and proves two-time finite-dimensional convergence to it; Theorem 2.1.1 constructs that workload, proves it unique, gives it in closed form, and adds the non-existence half. Different conclusion, different generality, different Mathlib revision.

Ergodicity and Stochastic Intensity

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory has two halves. The first builds Palm calculus from the Matthes definition of P⁰_N and reaches the Swiss army formula. This mission is the second: §§1.6, 1.8 and 1.9, which supply the two things the rest of the book runs on.

Ergodic theory, quoted

§1.6 states, in its own words, "the ergodic theory results to be used later in this book". Five of them, and the book proves none: Birkhoff's pointwise ergodic theorem in discrete (Theorem 1.6.1) and continuous time (Theorem 1.6.4), Kingman's sub-additive ergodic theorem (Theorem 1.6.2), and the extremal characterizations of ergodicity in both settings (Theorems 1.6.3 and 1.6.5) — ergodicity is exactly the impossibility of splitting an invariant probability into two distinct ones.

They are quoted, but they are not decoration. Kingman's theorem is what produces the asymptotic growth rates of Theorem 2.11.2 and the constant γ(c) on which the saturation rule rests. Birkhoff's theorem is what makes the time average in PASTA's (3.3.2) a well-defined object, and what the fluid Loynes theorem invokes for lim_{u→−∞}(A_{u,0} − C_{u,0}) = −∞.

None of the three analytic ones exists in Mathlib. Analysis/InnerProductSpace/MeanErgodic is the mean (von Neumann, L²) theorem, not almost-everywhere convergence, and there is no sub-additive ergodic theorem at all. The platform has neither.

Predictability, and why PASTA can be stated

§1.8 introduces the stochastic intensity: a point process N admits the (P, F_t)-intensity {λ(t)} when E[N(a,b] 1_A] = E[(∫_a^b λ(t)dt) 1_A] for A ∈ F_a. Around it sits the notion of a predictable process — one measurable with respect to the strict past.

Theorem 1.8.1 is the structural fact that makes predictability usable. For the internal history of a marked point process, every predictable process has the concrete form

Z(t, ω) = v(t, θ_t ω),    v(t, ·) F_{0−}-measurable.                                   (1.8.1)

That is why mission IV can take this form as PASTA's hypothesis rather than constructing a predictable σ-field: Theorem 1.8.1 says nothing is lost.

The goal

Theorem 1.8.2 (p.61), §1.8.4, Watanabe's characterization of Poisson processes. For a history F_t = F_t^N ∨ G and a G-measurable, locally integrable {λ(t)}, if N admits the F_t-intensity {λ(t)} then N is a G-conditional Poisson process:

E[ e^{iuN(a,b]} | G ∨ F^N_a ] = exp{ (e^{iu} − 1) ∫_a^b λ(t) dt } .                    (1.8.12)

A stochastic intensity that carries no information beyond G forces the process to be Poisson conditionally on G, with the compensator as the parameter — and the conditional characteristic function is the exact Poisson one, not an approximation. With G trivial and λ constant this is the ordinary Poisson process, which is the equivalence Remark 3.3.1 of Chapter 3 invokes to explain the name PASTA. The book: "This result plays a role in queueing theory, especially for proving that some streams in a queueing network are or are not Poissonian."

Palm probability meets stochastic intensity

§1.9 asks whether the stochastic intensity is the same under P and under P⁰_N — whether the two probabilities describe the same dynamics. Theorem 1.9.1 says yes, on ℝ₊: the same process {λ(t)} serves both.

Theorem 1.9.2 is Papangelou's theorem, and it is the deepest statement of the section: N admits a stochastic intensity if and only if P⁰_N ≪ P on F_{0−}, and then λ(t) = (μ ∘ θ_t)λ with μ the Radon–Nikodým derivative. A dynamic property and a static one turn out to be the same thing.

Theorem 1.9.3 is Mecke's characterization: N is Poisson exactly when P ≡ P⁰_N on F_{0−}. The view from a point of the process and the view from a deterministic instant agree on the strict past precisely when the process has no memory. It follows in one line from the two theorems before it.

What this mission provides

Four of the five missions in this series import the Chapter 1 substrate; this one adds the two pieces they need from its second half — ergodic theory and the stochastic intensity. Nothing here is on the platform, and Mathlib has filtrations and adapted processes but no predictability in this form, no stochastic intensity, no pointwise ergodic theorem and no Kingman.

Formalization scope

Every result is stated in the book's strength, with the book's standing definitions as binders. A discrete flow is a bijective, measurable, P⁰-preserving map (p.46); a continuous flow is jointly measurable in (t, ω) (p.3, clause (a)). A history compatible with the flow satisfies θ_t F_s = F_{s−t} (p.57), and an F_t-intensity is a non-negative, measurable, locally integrable, adapted process (p.58). The limits of Theorems 1.6.1, 1.6.2 and 1.6.4 are asserted to exist; Kingman's constant h̄ lies in ℝ ∪ {−∞} and is identified with inf_n (1/n) E⁰[h_n], the means being extended reals so that E⁰[h_n] = −∞ is not read as 0. Theorems 1.6.3, 1.6.5, 1.9.2 and 1.9.3 are equivalences, and Theorem 1.9.2 carries the closed form λ(t) = (μ ∘ θ_t)λ with μ = dP⁰_N/dP on F_{0−}. The goal's conclusion is the exact conditional characteristic function (1.8.12); a formalization that only asserted some conditional Poisson law, or conditioned on G alone, would not be this theorem.

The Swiss Army Formula of Palm Calculus

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds the calculus that the rest of the book runs on. Its subject is the relation between two ways of looking at the same stationary system: from a clock fixed in time, and from a customer arriving into it. The two are not the same — the interval a random instant falls into is longer than a typical interval, a fact every queueing student meets as the inspection paradox — and the object that makes the difference precise is the Palm probability P⁰_N.

The chapter defines P⁰_N by the Matthes definition in terms of counting,

λ t P⁰_N(A) = E[ Σ_{n ∈ ℤ} 1_A(θ_{T_n}) 1_{(0,t]}(T_n) ],                          (1.2.1)

and everything else is a theorem about it. That ordering is deliberate here too: P⁰_N is carried in the formalization as a predicate satisfying (1.2.1), not as a measure constructed to make Mecke's formula true. If it were the latter, Mecke's formula would be a definition and the inversion formula and the goal theorem would inherit that emptiness.

From (1.2.1) the chapter derives, in order: that P⁰_N is invariant under the point shift (1.2.16); Mecke's formula (1.2.17), which the literature also knows as the generalized Campbell formula; the inversion formula of Ryll-Nardzewski and Slivnyak (1.2.25), which runs back from P⁰_N to P; the mean-value formulas (1.3.2)–(1.3.3); the Neveu exchange formula (1.3.4), which relates two point processes stationary for the same flow; and the Miyazawa rate conservation principle (1.3.10), which balances the drift of a process between its jumps against the rate at which it jumps.

The goal

§1.3.7 then collects all of them into one identity. Its name is the book's own:

Depending on which blade is selected, a Swiss army knife transforms itself into various useful tools. The formula obtained in this subsection is called the Swiss army formula of Palm calculus because it contains the main formulas of this theory, as well as some new ones.

Theorem 1.3.1 (p.29). For arrivals {T_n} with counting measure A and intensity λ_A, departures {τ_n} with counting measure D — not assumed ordered — sojourn times W_n = τ_n − T_n ≥ 0 forming a sequence of marks of A, the number in system {X(t)} with X(b) − X(a) = A((a,b]) − D((a,b]), a non-decreasing corlol integrator {B(t)} and a non-negative process {Z(t)}, all compatible with a measurable flow under which P is invariant:

λ_A E⁰_A [ ∫_(0,W_0] Z(s) dB(s) ] = (1/t) E [ ∫_(0,t] X(s−) Z(s) dB(s) ].              (1.3.28)

Selecting the blade Z ≡ 1, B(t) = t turns it into λ_A E⁰_A[W_0] = E[X(0)] — Little's law, here in its full stationary-ergodic form rather than as a deterministic sample-path identity. Other choices give the inversion formula, the Miyazawa conservation principle and the rate conservation law.

The local meaning of P⁰_N

One milestone stands slightly apart. Theorem 1.5.1 (p.45) is what licenses the whole reading of P⁰_N as "what an arriving customer sees":

lim_{t→0} sup_{A ∈ F} | P⁰_N(A) − P(θ_{T_1} ∈ A | T_1 ≤ t) | = 0.                       (1.5.3)

The supremum is inside the limit. The convergence is uniform over every measurable event, which is what Dobrushin's estimate of §1.5.1 buys and what a pointwise limit would not give.

What this mission provides

Nothing in this chapter exists on the platform or in Mathlib: not stationary marked point processes, not Palm probability, not the Campbell measure. Four of the five missions in this series import the vocabulary built here, and the two definition items — the substrate of §§1.1–1.2 and the setting of §1.3.7 — are as much of the deliverable as the theorems are.

Formalization scope

• The flow {θ_t} is a one-parameter group with (t, ω) ↦ θ_t ω jointly measurable (p.5 (a)); a point process is its strictly increasing points {T_n}_{n ∈ ℤ} with T_0 ≤ 0 < T_1, infinitely many on each side (Hypothesis 1.1.1), with finite non-null intensity λ = E[N((0,1])].
• P⁰_N is characterized by (1.2.1) for every t > 0, which determines it uniquely; nothing is axiomatized. A formalization that introduced P⁰_N as any measure satisfying Mecke's formula would make the milestones and the goal trivial and is ruled out.
• Every "for all non-negative measurable" formula (Mecke, inversion, mean-value, Neveu, Wald, the goal) is stated in [0, ∞] with lower Lebesgue integrals, for all such functions, not only bounded or integrable ones.
• Three hypotheses the book uses without listing them are explicit: the Swiss army formula assumes the integrator {B(t)} is θ_t-compatible (the proof uses it, and without it the identity fails); it is stated for t > 0, the only values at which 1/t and (0, t] give it content; and the Miyazawa principle assumes Y'(0) ∈ L¹(P), which its E[Y'(0)] presupposes.
• Theorem 1.5.1 keeps the supremum over all events inside the limit (one δ for every A).

Motivation

Countable-state Markov chains are the standard model of queues with unbounded buffers, but any numerical computation of their long-run behaviour works on a finite state space. The usual remedy is truncation: restrict the chain to a finite set $S_N$ and redistribute the probability of leaving $S_N$ back into it. Whether the steady state probabilities and average costs of the truncated chains converge to those of the original chain depends on how that probability is redistributed. Gibson and Seneta studied this question for the stationary distributions of chains without costs (Gibson and Seneta, J. Appl. Prob., 1987). Sennott extended it to chains with costs and expected first passage costs (Sennott, Adv. Appl. Prob. 29, 1997; ZOR Math. Meth. Oper. Res. 45, 1997), and used it as the basis of the approximating sequence method for average-cost Markov decision chains (Sennott, 1999, Chapter 8). This mission covers Appendix C, Sections C.4–C.5 of the 1999 book, the Markov-chain results that the book's average-cost approximation theorems use.

Setting

A Markov chain with costs $\Gamma$ on a denumerable state space $S$ has transition probabilities $P_{ij}$ with $\sum_jP_{ij}=1$ and a finite nonnegative cost $C(i)$ at each state. For a set $G\subseteq S$ and a start $i$, $T_{iG}\ge 1$ is the first passage time to $G$. The taboo probability ${}_GP^{(t)}_{ik}$ is the probability of moving from $i$ to $k$ in $t$ steps with no intermediate state in $G$. The expected visits ${}_Gu_{ik}$ count the visits to $k$ at times $0\le t<T_{iG}$. The mean first passage time is $m_{iG}=E[T_{iG}]$, infinite when $G$ is missed with positive probability. The first passage cost is $c_{iG}=E\big[\sum_{t<T_{iG}}C(X_t)\big]$. A state $i$ is positive recurrent when $m_{ii}<\infty$, and the steady state probability is $\pi_i=m_{ii}^{-1}$. On a positive recurrent class $R$ the average cost is $J_R=\sum_{j\in R}\pi_jC(j)$. The chain is $z$ standard when $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$. Such a chain has one positive recurrent class $R\ni z$ with $J_R<\infty$, and every other state is transient.

An approximating sequence (AS) $(\Gamma_N)_{N\ge N_0}$ consists of increasing nonempty finite sets $S_N$ with $\bigcup_NS_N=S$ and, for each $N$, a chain $\Gamma_N$ on $S_N$ with the same costs and transition probabilities $P_{ij}(N)\to P_{ij}$. The quantities of $\Gamma_N$ are written $m_{iG}(N)$, $c_{iG}(N)$, $\pi_i(N)$ and $J(i)(N)$. An AS is conforming (for a $z$ standard $\Gamma$) if, for large $N$, $\Gamma_N$ is unichain with $z$ in its positive recurrent class, and $m_{iz}(N)\to m_{iz}$ and $c_{iz}(N)\to c_{iz}$ for all $i$. It is conforming on $R$ if $\pi_i(N)\to\pi_i$ and $J(i)(N)\to J_R$ on $R$.

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the probability of each excluded target $r\notin S_N$ according to an augmentation distribution $q_\cdot(i,r,N)$ on $S_N$:

$$P_{ij}(N)=P_{ij}+\sum_{r\in S-S_N}P_{ir}\,q_j(i,r,N),\qquad j\in S_N.$$

It sends excess probability to $G$ if every $q_\cdot(i,r,N)$ is concentrated on $G$.

Formalization targets

Goal: Proposition C.5.2

For a $z$ standard chain $\Gamma$ and a finite nonempty $G\subseteq S$,

$$\text{every ATAS that sends excess probability to } G \text{ is conforming},$$

and if $G\subseteq R$ it is also conforming on $R$. No rate of convergence and no constants are involved, and $G$ need not contain $z$.

Milestones

1. Proposition C.4.2: for fixed $t$, $\lim_N{}_GP^{(t)}_{ik}(N)={}_GP^{(t)}_{ik}$; also $\liminf_N{}_Gu_{ik}(N)\ge{}_Gu_{ik}$ and $\liminf_Nm_{iG}(N)\ge m_{iG}$.
2. Proposition C.4.3: $\pi_i(N)\to0$ off the positive recurrent states, and along subsequences $\pi_i(N_s)\to b\pi_i$ on a class, with $0\le b\le1$.
3. Proposition C.4.5: $\liminf_Nc_{iG}(N)\ge c_{iG}$.
4. Proposition C.4.6: on a positive recurrent class, convergence of $\pi$, of $m_{zz}$ and of all $m_{iG}$ are equivalent. Given these, convergence of $J(i)$, of $c_{zz}$ and of all $c_{iG}$ are equivalent.
5. Proposition C.4.9: conformity implies $\pi_i(N)\to\pi_i$ for all $i$, and that the constant average costs $J(N)$ of $\Gamma_N$ converge to $J_R$.

Further results

6. Proposition C.5.3: an ATAS is conforming when, for $N\ge N^*$, the augmentation distributions satisfy $\sum_{j\ne z}q_j(i,r,N)m_{jz}\le m_{rz}$ and $\sum_{j\ne z}q_j(i,r,N)c_{jz}\le c_{rz}$.
7. Corollary C.5.4: for a $0$ standard chain on $\{0,1,2,\dots\}$ with an upper Hessenberg transition matrix, truncated to $S_N=\{0,\dots,N\}$ with the excess sent to $N$, the ATAS is conforming.

Significance

The result. Conformity is the hypothesis under which the book's approximating sequence method works for average-cost queueing control (Chapter 8). The method computes optimal policies for finite truncations and passes to the limit. That argument needs the first passage times and costs to a distinguished state to converge along the chains induced by fixed policies. Propositions C.5.2 and C.5.3 turn this analytic requirement into conditions on the truncation scheme that can be checked in practice: send the overflow to a fixed finite set, or to states from which reaching $z$ is no more expensive. Examples C.4.4 and C.4.7 of the book show that an arbitrary approximating sequence can fail. The limit of the steady state probabilities can be a strict multiple $b\pi$ with $b<1$. First passage costs can converge to the wrong value even when the steady state probabilities converge.

Formalizing it. The results are proved in the book, some in abbreviated form ("the proof for the costs is similar and is omitted"). The Prove2Me library had no statement on truncation or augmentation of countable Markov chains when this mission was drafted (September 2026). A formalization supplies the omitted cost arguments, makes the passage between $\liminf$ bounds and limits in $[0,\infty]$ explicit, and produces a reusable library of first passage quantities for countable chains.

Difficulty

The lower bounds of Propositions C.4.2 and C.4.5 are the routine part. The difficulty is the matching upper bound: in $\Gamma_N$, a first passage that leaves $S_N$ is restarted elsewhere, which can lengthen it without bound. Taking limits termwise in the first passage equation $m_{iz}(N)=1+\sum_{j\ne z}P_{ij}(N)m_{jz}(N)$ fails, because no dominating function is available and mass can escape to infinity. Example C.4.4 exhibits exactly this. Unichain structure is also not automatic: $\Gamma_N$ may have several recurrent classes, or a recurrent class not containing $z$, and ruling this out is part of the conclusion rather than an assumption.

Formalization scope

The Lean development works in SennottDP.ChainASM. A chain is a structure MC S with P : S → S → ℝ≥0∞, ∑' j, P i j = 1 and C : S → ℝ≥0. Theorems assume [Countable S] [Infinite S], matching the book's denumerable state space. Taboo probabilities, expected visits, $m_{iG}$, $c_{iG}$, $\pi_j=(m_{jj})^{-1}$ and $J_R=\sum_{j\in R}\pi_jC(j)$ are defined as sums in $[0,\infty]$. $m_{iG}=\sum_{t\ge0}P(T_{iG}>t)$ is infinite whenever $G$ is missed with positive probability. The average cost $J(i)$ is the $\limsup$ of the Cesàro cost averages.

An AS is a structure carrying $N_0$, the finite sets $S_N$ (as Finset S) and $P_{ij}(N)$. $\Gamma_N$ is built as an MC on the subtype of $S_N$, and a set $G$ is read in $\Gamma_N$ as $G\cap S_N$. Quantities of $\Gamma_N$ are lifted to functions of $N$ and of states of $S$ with the value $0$ where they are undefined ($N<N_0$ or a state outside $S_N$). For fixed states this affects finitely many $N$, and all statements are limits, $\liminf$s or eventual equalities. All convergence is in $[0,\infty]$. The conformity predicate includes the standing assumption that $\Gamma$ is $z$ standard. The positive recurrent class $R$ of a $z$ standard chain is the communicating class of $z$.

A trivializing formalization is excluded: the AS of Example C.4.4, whose positive recurrent class $\{N\}$ excludes $z=0$, is not conforming under these definitions. The ATAS predicate requires the augmentation distributions to be probability distributions and to reproduce $P_{ij}(N)$ exactly by (C.27).

A complete development needs first passage decompositions for countable chains, the renewal-reward identity $J_R=c_{zz}/m_{zz}$, and dominated and Fatou-type limit theorems for sums (the book's Appendix A). The first passage library and the lifted-quantity conventions can be reused by the average-cost approximation chapters. Contributions of intermediate lemmas are welcome, especially the finite-state unichain facts of Section C.3 and the identities of Propositions C.1.4 and C.2.2.

Proposition C.5.5 (lower Hessenberg chains, from Gibson and Seneta) is stated in the book without proof and without naming the distinguished state, and is not included.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix C, Sections C.4–C.5. https://doi.org/10.1002/9780470317037
• L. I. Sennott, "The computation of average optimal policies in denumerable state Markov decision chains", Advances in Applied Probability 29 (1997) 114–137 (cited in the book as Sennott 1997a).
• L. I. Sennott, "On computing average cost optimal policies with application to routing to parallel queues", ZOR Mathematical Methods of Operations Research 45 (1997) 45–62 (cited in the book as Sennott 1997b).
• D. Gibson and E. Seneta, "Augmented truncations of infinite stochastic matrices", Journal of Applied Probability (1987).