Markov Chain

Motivation

Controlled Markov processes with the average cost criterion model systems that run indefinitely, such as queues, inventories, maintenance and communication networks, where only the long-run cost per unit time matters. The standard route to an optimal stationary policy goes through the average cost optimality equation (ACOE). The ACOE is usually obtained by the vanishing discount method: solve the discounted problem for each discount factor $\beta<1$ and let $\beta\to1$. The method works only when the differences of discounted values stay bounded as $\beta\to1$. Conditions that guarantee this are therefore central in the survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993), §5).

This mission formalizes one such condition, due to Ross: if the mean return time to a fixed state is bounded uniformly over all stationary policies and initial states, the differential discounted value functions are bounded uniformly in the discount factor and the state.

Timeline. Derman (Management Sci. 9 (1962); survey reference [38]) and Derman–Veinott (Ann. Math. Statist. 38 (1967); survey reference [43]) introduced recurrence conditions of this kind for countable-state processes. Ross (Ann. Math. Statist. 39 (1968), survey reference [147]; Introduction to Stochastic Dynamic Programming, 1983, survey reference [150]) showed, for bounded costs, that under a Derman–Veinott type recurrence condition $h_\beta$ is bounded uniformly in $\beta$, and obtained a bounded solution of the ACOE by letting $\beta\uparrow1$ (survey, pp. 291 and 301). Later work replaced the condition with weaker ones (survey Assumptions 5.1–5.3) and with Sennott's conditions (survey Theorem 5.9).

Setting

The state space is $S=\{0,1,2,\dots\}$. In each state $i$, an action $a$ is chosen from a nonempty compact set $U(i)$ of a metric space $A$. The one-stage cost $c(i,a)$ is nonnegative and the next state is drawn from the transition law $P(\cdot\mid i,a)$. For fixed $i,j$, the maps $a\mapsto c(i,a)$ and $a\mapsto P(j\mid i,a)$ are continuous on $U(i)$. A policy $\pi\in\Pi$ chooses the action at time $t$ at random, given the whole history, and must choose from $U(X_t)$. A stationary deterministic policy $f\in\Pi_{SD}$ is a map $f:S\to A$ with $f(i)\in U(i)$. $P^\pi_i$ and $E^\pi_i$ denote the law and the expectation of the controlled process $(X_t,A_t)$ started at $i$.

For a discount factor $\beta\in(0,1)$, the discounted cost and the optimal discounted cost are

$$J_\beta(i,\pi)=E^\pi_i\Big[\sum_{t=0}^\infty\beta^t c(X_t,A_t)\Big],\qquad J^*_\beta(i)=\inf_{\pi\in\Pi}J_\beta(i,\pi).$$

A policy $f\in\Pi_{SD}$ is $\beta$-discount optimal if $J_\beta(i,f)=J^*_\beta(i)$ for all $i$. The differential discounted value function is

$$h_\beta(i)=J^*_\beta(i)-J^*_\beta(0),$$

measured relative to the fixed state $0$. The return time to $0$ is

$$\tau=\min\{t\ge1:\ X_t=0\},$$

with $\tau=\infty$ if the process never returns. Throughout, as in §5.1 of the survey, the cost is bounded: $c(i,a)\le M$ on admissible pairs.

Formalization targets

Goal: Theorem 5.3

If there is a constant $K>0$ with

$$E^f_i[\tau]<K\qquad\text{for all } f\in\Pi_{SD},\ i\in S, \tag{5.7}$$

then there is a constant $B$ such that

$$|h_\beta(i)|\le B\qquad\text{for all }\beta\in(0,1),\ i\in S.$$

This is the theorem as printed: it asserts only uniform boundedness and fixes no constant.

Milestones

1. Theorem 2.1 (iii): for every $\beta\in(0,1)$, a $\beta$-discount optimal $f_\beta\in\Pi_{SD}$ exists.
2. (5.8): for such an $f_\beta$, $J^*_\beta(i)\le M\,E^{f_\beta}_i[\tau]+J^*_\beta(0)\,E^{f_\beta}_i[\beta^\tau]$.
3. (5.9): $J^*_\beta(i)-\beta J^*_\beta(0)\le MK$.
4. Jensen step: $J^*_\beta(i)\ge J^*_\beta(0)\,E^{f_\beta}_i[\beta^\tau]\ge J^*_\beta(0)\,\beta^K$.
5. (5.10): $J^*_\beta(0)-J^*_\beta(i)\le(1-\beta^K)J^*_\beta(0)\le(1-\beta^K)\frac{M}{1-\beta}\le MK$.
6. Explicit bound: $|h_\beta(i)|\le MK$. This is stronger than the goal and is the constant the survey's argument yields.

Significance

The result. Theorem 5.3 verifies the hypothesis of the vanishing discount theorem (Theorem 5.2 of the survey) from a condition on the uncontrolled dynamics of stationary policies. Theorem 5.2 then gives a bounded solution $(\rho,h)$ of the ACOE, an average optimal stationary policy, and the limit $\lim_{\beta\to1}(1-\beta)J^*_\beta(i)=\rho$. Mean return times can often be estimated directly, for instance through Foster–Lyapunov drift arguments on queues, which makes (5.7) checkable in applications. The explicit bound $MK$ also controls the span of the relative value function.

Formalizing it. The result is proved in the literature; to our knowledge it has not been machine-checked. A formal proof needs discounted dynamic programming on a countable state space with compact action sets, the existence of optimal stationary policies (Theorem 2.1 (iii), which the survey cites without proof), and the strong Markov property of the controlled chain at a return time. All of these are reusable well beyond this mission.

Difficulty

The estimates (5.9) and (5.10) are elementary once (5.8) and the existence of $f_\beta$ are available. The weight lies elsewhere.

• Optimal stationary policies. The infimum defining $J^*_\beta$ ranges over all history-dependent randomized policies. Bringing it down to a single stationary deterministic policy requires the discounted optimality equation, a measurable selection of minimizers on compact action sets, and a verification argument against arbitrary policies.
• Restarting at $\tau$. (5.8) splits the discounted cost at the random time $\tau$. The tail must be identified with $\beta^\tau$ times the discounted cost from state $0$. This is the strong Markov property for the process built by the Ionescu-Tulcea theorem, applied at a stopping time that may be infinite.

Formalization scope

• The state space is ℕ; the action space is a metric space with its Borel $\sigma$-algebra. The model CMP carries compact nonempty $U(i)$, a nonnegative measurable cost, and continuity of $c(i,\cdot)$ and $P(j\mid i,\cdot)$ on $U(i)$, the standing assumptions of §5.
• Policies are history-dependent, randomized and admissible. The path measure is Mathlib's Kernel.trajMeasure. $J^*_\beta$ is an infimum over all such policies, not over Markov or stationary policies only.
• Costs are lower Lebesgue integrals in $[0,\infty]$. $h_\beta$ is the difference of the real parts of $J^*_\beta(i)$ and $J^*_\beta(0)$. This is exact here because bounded cost gives $J^*_\beta\le M/(1-\beta)<\infty$.
• Explicit choices:
  • The bounded-cost hypothesis $c\le M$ on admissible pairs is a binder of every §5.1 statement. It is the section's standing assumption, and without it the theorem is false.
  • $\tau$ counts from $t\ge1$ and takes values in $\mathbb N\cup\{\infty\}$, so (5.7) applies from $i=0$ and forces $\tau<\infty$ almost surely; $\beta^\tau=0$ on $\{\tau=\infty\}$.
  • The typo $\beta^n$ in (5.8) is read as $\beta^t$.
  • $K\ge1$ in (5.10) is not assumed; it follows from (5.7).
• Theorem 2.1 is stated in the survey for Borel models under Assumptions 2.1–2.3. Here it is posed in the countable model, where those assumptions follow from the §5 continuity and compactness assumptions.
• The goal's bound $B$ is quantified before $\beta$ and $i$. A per-$\beta$ or per-state bound would be trivial, since every $h_\beta(i)$ is a finite number.
• Welcome contributions include discounted dynamic programming on countable state spaces, the strong Markov property for trajMeasure, and return-time estimates.

Selected references

• A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2) (1993) 282–344. https://doi.org/10.1137/0331018
• C. Derman, On sequential decisions and Markov chains, Management Sci. 9 (1962) 16–24. https://doi.org/10.1287/mnsc.9.1.16
• C. Derman, A. F. Veinott Jr., A solution to a countable system of equations arising in Markovian decision processes, Ann. Math. Statist. 38 (1967) 582–584 (cited as [43] in the survey, https://doi.org/10.1137/0331018).
• S. M. Ross, Non-discounted denumerable Markovian decision models, Ann. Math. Statist. 39 (1968) 412–423 (cited as [147] in the survey, https://doi.org/10.1137/0331018).
• S. M. Ross, Introduction to Stochastic Dynamic Programming, Academic Press, 1983 (cited as [150] in the survey, https://doi.org/10.1137/0331018).

Why average cost is a control problem

A controller acting over an indefinite horizon must decide whether a lower cost today is worth a higher cost later. Average cost measures the expected expenditure per stage as the horizon grows. It is appropriate when operation has no natural terminal date, but its limiting definition makes it difficult to compute an optimal policy directly. Discounted cost assigns less weight to distant stages and has a more direct optimality equation. Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus survey these criteria for controlled Markov processes and state a condition under which solving one discounted problem yields a solution to an average-cost problem (Arapostathis et al., 1993, §5.1).

The condition is a common lower bound on the one-step probability of moving to a distinguished state. Ross's reduction, reported as Theorem 5.6 of the survey, uses that bound to define a new transition law and a specific discount factor. The survey's theorem states the reduction informally; its proof specifies the transformed law, the optimality equation and the resulting average-cost policy. Those claims are the targets of this mission (Arapostathis et al., 1993, pp. 303–304).

Controlled process and criteria

The state space is $S=\{0,1,2,\ldots\}$. In state $i$, the controller may choose an action $a$ from a nonempty compact set $U(i)$ in a metric action space. Choosing $a$ incurs the one-stage cost $c(i,a)\ge0$ and moves the state to $j$ with probability $P(j\mid i,a)$. The cost is measurable, and for each fixed $i,j$ its value and $P(j\mid i,a)$ vary continuously with $a$ on $U(i)$. Section 5 imposes these state and continuity conventions; §5.1 additionally assumes the costs are bounded (Arapostathis et al., 1993, pp. 284–288, 299, 301).

An admissible policy $\pi$ chooses a probability law for the next action from the entire observed history, and assigns probability one to admissible actions. A stationary deterministic policy is a map $f$ with $f(i)\in U(i)$; it always takes action $f(i)$ in state $i$. These are distinct classes. Let $J_N(i,\pi)$ be expected cost over the first $N$ stages from $i$, and let $J_\beta(i,\pi)$ be expected cost when stage $t$ is weighted by $\beta^t$, where $0<\beta<1$. The average-cost criterion is $J(i,\pi)=\limsup_{N\to\infty}J_N(i,\pi)/N$. The optimal values $J^*(i)$ and $J_\beta^*(i)$ are infima over all admissible policies, including randomized and history-dependent ones (Arapostathis et al., 1993, pp. 285–287).

The average cost optimality equation, or ACOE, asks for a scalar $\rho$ and a real function $h$ such that, for each state $i$,

$$\rho+h(i)=\min_{a\in U(i)}\left\{c(i,a)+\sum_{j\in S}P(j\mid i,a)h(j)\right\}.$$

The minimum is attained. The survey's verification theorem identifies $\rho$ with the optimal average cost when the terminal contribution of $h(X_t)$ vanishes after division by $t$ (Arapostathis et al., 1993, p. 299, (5.1), Theorem 5.1).

Formalization targets

The reduction

Assume that $P(0\mid i,a)\ge\alpha$ on every admissible state-action pair for a single constant $0<\alpha<1$. The transformed process $\widetilde M$ has the same admissible actions and costs and has transition probabilities

$$\widetilde P(j\mid i,a)=\frac{P(j\mid i,a)-\alpha\mathbf1_{\{j=0\}}}{1-\alpha}.$$

Write $\widetilde J^*_{1-\alpha}$ for its discounted value at discount factor $1-\alpha$. The goal states that this value is finite, a stationary deterministic discounted-optimal policy exists, and every such policy is average-cost optimal for the original process. It also identifies a constant optimal average cost for every initial state:

$$J^*(i)=\alpha\widetilde J^*_{1-\alpha}(0),\qquad i\in S.$$

The goal does not assume the average optimality that it asserts. It requires the transformed law to satisfy the displayed formula at every admissible state-action pair (Arapostathis et al., 1993, Theorem 5.6 and proof, pp. 303–304).

Supporting targets

The milestones establish that the transformed law gives a controlled Markov process, that the discounted problem has an optimal stationary deterministic policy, and that the transformed discounted value satisfies the original ACOE with $\rho=\alpha\widetilde J^*_{1-\alpha}(0)$. The final milestone is the ACOE verification theorem needed to identify the average cost. The source gives the first two discounted claims through Theorem 2.1 and writes out the transformed equation in the proof of Theorem 5.6 (Arapostathis et al., 1993, pp. 289, 299, 304).

What the result supplies

The theorem replaces an average-cost optimization problem by one discounted problem with a prescribed discount factor and transition law. It yields a stationary deterministic policy that is optimal even when compared with every history-dependent randomized policy, and it shows that the optimal average cost is independent of the initial state. Without the common return probability, neither this particular law nor this fixed discount factor follows from the survey's argument (Arapostathis et al., 1993, Theorem 5.6).

The survey reports this as a known result of Ross rather than an open conjecture. The formalization work is to give the path measures, value functions, transformed process and verification result machine-checkable meanings. The Lean declarations here are open theorem statements awaiting proofs; compiling a statement with sorry does not establish the mathematical theorem. The policy and cost definitions can also support the other countable-state missions drawn from §5.

Difficulty

The transformed probabilities have to form a measurable stochastic kernel, preserve the action continuity assumptions and yield a controlled process with the original feasible actions and costs. The discounted value must be finite and uniformly bounded before its real form can enter the ACOE. A simple comparison of numerical optimal values is insufficient: a policy chosen in the transformed model must be shown optimal for the original model against the full policy class. The verification theorem also requires control of the terminal expectation of $h(X_t)$ for arbitrary admissible policies, rather than only the stationary policies named in its printed condition (Arapostathis et al., 1993, pp. 299–300, 304).

Formalization scope

Lean uses $\mathbb N$ for the countable state space and Mathlib probability kernels for the transition and randomized decision rules. Strategic path measures are constructed from those kernels. Nonnegative expected costs and their infima live in $[0,\infty]$, so an unbounded integral cannot silently become a finite real value. The transformed discounted value is converted to a real only in conclusions that also assert its finiteness. The ACOE uses real sums with explicit summability and an attained minimum. The model requires a Borel metric action space, nonempty compact action sets, measurable costs, and coordinatewise action continuity of the transition probabilities.

The source's §5.1 bounded-cost assumption is explicit in the goal and its discounted milestones. The displayed transformation needs $\alpha<1$; the paper's theorem sentence gives only $\alpha>0$, so the case $\alpha=1$ is excluded from this version. The paper prints (5.2) for stationary deterministic policies, but the proof uses it for all admissible policies to compare with $J^*$; the verification milestone takes the stronger, proof-supported hypothesis. Expectations in that condition are explicitly integrable. The converse part of Theorem 5.1 is not used and is outside this mission.

The transformed process is represented by another CMP constrained to have exactly the source's action sets, admissible costs and transition formula. A milestone poses its existence. This representation keeps the definition layer free of an unproved stochastic-kernel construction. The discount-optimal policy conclusion ranges over every stationary deterministic policy attaining the transformed discounted value, while the values themselves take infima over all admissible policies. Definitions of admissible path laws and the verification theorem are reusable contributions; proofs of the transformed kernel, stationary discounted existence and ACOE identity are welcome.

Selected references

• A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh and S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM Journal on Control and Optimization 31(2), 282–344, 1993. DOI: 10.1137/0331018.

Motivation

A controller often cannot see the state of the system it steers. It sees only measurements that are noisy functions of that state. In operations research this happens in machine maintenance and inspection, in queues observed only partially, and in inventory systems with inexact stock records. In control engineering it is the usual case. The question is what the controller should base its decisions on. The full record of past measurements is the obvious choice, but that record grows with time, so a law that uses it is a function on a space whose dimension grows with the horizon.

K. J. Åström's 1965 paper Optimal Control of Markov Processes with Incomplete State Information answered this question for finite Markov chains. The answer is that the conditional distribution of the hidden state given the measurements is a sufficient statistic. The problem with incomplete information is equivalent to a problem with complete information whose state is that distribution. This is the model now called a partially observable Markov decision process (POMDP), and the conditional distribution is now called the belief state.

Timeline. For linear systems with quadratic cost and Gaussian noise, the separation theorem of Joseph and Tou (1961) and Gunckel and Franklin (1963) says that the optimal control is a fixed function of the conditional mean of the state. Åström (1965) proved the reduction for finite-state Markov chains with arbitrary costs, with the conditional distribution as the new state. Smallwood and Sondik (1973) showed that for finite horizons the value function is piecewise linear and concave in the belief, which made exact computation possible. Bertsekas and Shreve (1978) and Bäuerle and Rieder (2011) gave the reduction for general Borel models.

Setting

The hidden state $x_t$, $t = 1, \dots, N$, takes values in a finite set $S$. The controls $u = (u_1, \dots, u_r)$ range over a compact nonempty set $U \subset \mathbb R^r$. The state moves by the transition probabilities $p_{ij}(u, t) = P\{x_t = j \mid x_{t-1} = i\}$, which are continuous in $u$. The state is observed through outputs $y_t$ in a finite set $Y$, with $q_{ij} = P\{y_t = j \mid x_t = i\}$, conditionally independent given the states. The law of $x_1$ is $p^1$. An instantaneous cost $g(u, i, t)$, continuous in $u$, is paid at each time.

A control law chooses $u(t) = c(\eta_1, \dots, \eta_t, t) \in U$ from the outputs observed so far, $\eta(t) = (\eta_1, \dots, \eta_t)$. With $u(t)$ moving $x_t$ to $x_{t+1}$, a law determines the joint law of $(x_1, \dots, x_N, y_1, \dots, y_N)$ and the expected cost

$$EL = E \sum_{t=1}^N g(u(t), x_t, t). \tag{2.6}$$

Problem P.1 is to find an admissible law minimizing (2.6).

The conditional state distribution is $w_i(t) = P\{x_t = i \mid \eta(t)\}$. It is updated by Bayes' rule: with $z^j(u, w)_i = \sum_s q_{ij}\, p_{si}(u, t+1)\, w_s$ and $\|z\| = \sum_i |z_i|$, the output $\eta_{t+1} = j$ gives $w(t+1) = z^j(u(t), w(t)) / \|z^j(u(t), w(t))\|$, and $\|z^j\|$ is the probability of that output. The cost-to-go $V_k(w)$ is the minimal expected cost of the steps $k, \dots, N$ when $x_k$ has distribution $w$, with $V_{N+1} = 0$. Problem P.2 controls the process $w(t)$ directly: a law chooses $u(t)$ from $w(1), \dots, w(t)$ to minimize $E\sum_{t=1}^N \sum_i g(u(t), i, t)\, w_i(t)$.

Formalization targets

Goal: Theorem 3

P.1 has a solution if and only if P.2 has one. For every solution $(V, c^0)$ of the functional equation

$$V_k(w) = \min_{u \in U} \Big\{ \sum_i g(u, i, k)\, w_i + \sum_j V_{k+1}\Big(\frac{z^j(u, w)}{\|z^j(u, w)\|}\Big) \|z^j(u, w)\| \Big\}, \qquad V_{N+1} = 0, \tag{3.28}$$

with $c^0(w, k)$ attaining the minimum, the law

$$u(t) = c^0(w(t), t)$$

is optimal for P.1 and for P.2, among all admissible laws of each, and both minimal values equal $E_{\eta_1} V_1(w(1))$.

Milestones

1. (3.20)–(3.25): the conditional distributions obey the Bayes recursion, and $\|z^j\| = P[y_{t+1} = j \mid \eta(t)]$.
2. Theorem 1: the cost-to-go satisfies (3.28) with the minimum attained, and an optimal Markov law attains it.
3. Theorem 2: a solution of (3.28) gives an optimal law for P.1 with value (3.29).
4. Lemma 1: under $u(t) = c(w(t), t)$, $\{w(t)\}$ is a Markov process with transition probabilities $P(y, \Gamma, u) = \sum_{k \in K} \|z^k(u, y)\|$.
5. Proof of Theorem 3: the integral against this kernel is the sum in (3.28).

Significance

The result. Theorem 3 replaces a minimization over functions of ever longer measurement records with a recursion over a fixed space, the probability simplex over the states. Every exact and approximate POMDP algorithm starts from it: value iteration on beliefs, the piecewise-linear representation of Smallwood and Sondik, point-based methods. It also splits the controller in two. A filter computes $w(t)$ in real time, and the function $c^0$ can be computed off-line. This is the decomposition the paper draws on p. 189, and it extends the linear-quadratic separation theorem to arbitrary finite chains.

Formalizing it. The theorem is proved. The platform has the reduction in Bäuerle and Rieder's discounted Borel model with an observable state component and rewards in extended reals. It does not have Åström's model: finite chains, time-dependent transition matrices, an unobservable state, costs, and laws of the raw output history. This mission formalizes Åström's statements as he gives them. The cost (2.6) is defined from the joint law of states and outputs, and the comparison classes are all laws of the outputs (P.1) and all laws of the distribution history (P.2). The finite setting makes every expectation a finite sum, so a complete development needs no measure theory.

Difficulty

The obvious argument is backward induction on the conditional distributions. The difficulty is that $w(t)$ depends on the controls already used, so it is not given in advance: the state of the reduced problem is produced by the law being optimized. It has to be shown that the expected cost of an arbitrary law of the outputs, computed from the joint law, splits as the reduced recursion says. In particular, laws that use more of the record than $w(t)$ must gain nothing. Restricting the comparison class to laws of the form $c(w(t), t)$ assumes this conclusion.

A second difficulty is attainment. "Min" in (3.28) and "has a solution" presuppose that minima over $U$ are attained, which needs continuity of $V_{k+1}$ on the simplex. The weights $\|z^j(u, w)\|$ can vanish, and then the update $z^j/\|z^j\|$ is undefined.

Formalization scope

States and outputs are finite types, St and Obs, with the chain given by the structure Model. Controls are Fin r → ℝ, and $U$ is compact and nonempty. The law $p^1$ of $x_1$ is the datum in place of the paper's law of $x_0$, since no control $u(0)$ exists. The transition from $x_t$ to $x_{t+1}$ uses $u(t)$ and the matrix $p(u(t), t+1)$. Times $1, \dots, N$ are indexed by Fin N as $0, \dots, N-1$.

The norm $\|\cdot\|$ is the $\ell^1$ norm l1, not Mathlib's sup norm. Conditional distributions are ratios of path sums, condState, and are claimed only on output histories of positive probability. When $\|z^j\| = 0$ the update is the zero vector and is always multiplied by $0$.

The cost-to-go costToGo is an infimum over admissible tail laws. Its index set is nonempty and the costs are bounded below, so the real infimum is a true infimum. It is never defined through (3.28), since that would make Theorem 1 circular. The P.2 functional sums branch by branch over the outputs, with weights $\|z^j\|$. "Given by Theorem 1" is read as "$c^0(w, k) \in U$ attains the minimum in (3.28)" (IsSolution328).

The goal is not the bare equivalence of solvability. In this compact, continuous, finite setting both problems always have solutions, so that sentence alone is trivially true. The goal also requires the law $c^0(w(t), t)$ to be optimal in both problems, against every admissible law, with equal minimal values.

Reusable beyond this mission are the finite POMDP model, the joint path law, the Bayes filter and the belief-MDP kernel. Welcome contributions include proofs of the milestones, the continuity of $V_k$ on the simplex, and existence of solutions of (3.28).

Selected references

• K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10(1):174–205, 1965. https://doi.org/10.1016/0022-247X(65)90154-X
• R. D. Smallwood and E. J. Sondik, The optimal control of partially observable Markov processes over a finite horizon, Operations Research 21(5):1071–1088, 1973. https://doi.org/10.1287/opre.21.5.1071
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978, Chapter 10. https://web.mit.edu/dimitrib/www/soc.html
• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5. https://doi.org/10.1007/978-3-642-18324-9
• P. D. Joseph and J. T. Tou, On linear control theory, Transactions of the AIEE, Part II 80(4):193–196, 1961. https://doi.org/10.1109/TAI.1961.6371743

Motivation

Many control problems in queueing, inventory and communication systems run indefinitely, and the quantity of interest is the long-run cost per unit time rather than a discounted total. The average cost criterion is harder to analyse than the discounted one: the discounted dynamic programming operator is a contraction, while the average cost problem has no contraction, and on an infinite state space its behaviour depends on the recurrence structure of the controlled chain. The survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993)) organises the theory around the average cost optimality equation (ACOE) and the conditions under which it has a solution.

Timeline (as recorded in the survey's §3 and §5). Derman studied the ACOE and characterized optimal stationary policies by its solutions (Derman, On sequential decisions and Markov chains, Management Sci. 1962; Denumerable state Markovian decision processes — average cost criterion, Ann. Math. Statist. 1966). Taylor introduced a vanishing discount argument for a replacement problem (Ann. Math. Statist. 1965). Ross extended it to general countable models, showing that uniformly bounded differential discounted value functions yield a bounded solution of the ACOE (Ann. Math. Statist. 1968, two papers; Introduction to Stochastic Dynamic Programming, 1983). Sennott replaced the uniform bound by one-sided bounds and obtained the average cost optimality inequality (Oper. Res. 1989). The survey presents Ross's result as Theorem 5.2, following the 1983 book; this mission formalizes it.

Setting

A controlled Markov process on the countable state space $S=\{0,1,2,\dots\}$ consists of a metric space $\mathbf A$ of actions; for each state $i$ a nonempty compact set $U(i)\subseteq\mathbf A$ of admissible actions; a cost $c(i,a)\ge0$; and transition probabilities $P(j\mid i,a)$. For fixed $i,j$, the maps $a\mapsto c(i,a)$ and $a\mapsto P(j\mid i,a)$ are continuous on $U(i)$.

An admissible policy $\pi$ chooses, at each time $t$, a probability distribution on $U(X_t)$ that may depend on the whole past $(X_0,A_0,\dots,X_t)$. The class of all of them is $\Pi$, and $\Pi_{SD}$ is the class of stationary deterministic policies, maps $f$ with $f(i)\in U(i)$. Each initial state $i$ and policy $\pi$ define a law $P^\pi_i$ of the trajectory, with expectation $E^\pi_i$. For a discount factor $0<\beta<1$,

$$J_\beta(i,\pi)=E^\pi_i\sum_{t=0}^\infty\beta^tc(X_t,A_t),\qquad J(i,\pi)=\limsup_{N\to\infty}\frac1N E^\pi_i\sum_{t=0}^{N-1}c(X_t,A_t),$$

and $J^*_\beta(i)=\inf_{\pi\in\Pi}J_\beta(i,\pi)$, $J^*(i)=\inf_{\pi\in\Pi}J(i,\pi)$. The differential discounted value function is $h_\beta(i)=J^*_\beta(i)-J^*_\beta(0)$. A pair $(\rho,h)$, $\rho\in\mathbb R$, $h:S\to\mathbb R$, solves the ACOE if

$$\rho+h(i)=\min_{a\in U(i)}\Big\{c(i,a)+\sum_{j\in S}P(j\mid i,a)h(j)\Big\},\qquad i\in S.\tag{5.1}$$

In the Lean development these objects are CMP, Policy, StationaryPolicy, pathMeasure, discCost, avgCost, discValue ($J^*_\beta$), optAvg ($J^*$), hRel ($h_\beta$) and ACOE.

Formalization targets

Goal: Theorem 5.2 (p. 301)

Assume $J^*_\beta(i)<\infty$ for all $\beta\in(0,1)$ and $i\in S$, and that there is $K>0$ with $|h_\beta(i)|\le K$ for all such $\beta$ and $i$. Then there are $\rho\in\mathbb R$, a bounded $h:S\to\mathbb R$ and a sequence $\beta_n\in(0,1)$, $\beta_n\to1$, with

$$(\rho,h)\text{ solves (5.1)},\qquad h(i)=\lim_{n\to\infty}h_{\beta_n}(i),\qquad \lim_{\beta\uparrow1}(1-\beta)J^*_\beta(i)=\rho\qquad(i\in S).$$

The goal does not assert that $\rho$ is the optimal average cost; that follows from Theorem 5.1 and Remark 5.1(a), which are milestones.

Milestones

1. Lemma 2.1 (p. 289): the dynamic programming map $T(v)(i)=\inf_{a\in U(i)}\{c(i,a)+\sum_jP(j\mid i,a)v(j)\}$ satisfies $T(v+k)=T(v)+k$ and is monotone.
2. Theorem 2.1 (i), (iii) (p. 289), in the countable model: $J^*_\beta=T_\beta J^*_\beta$ and a $\beta$-discount optimal $f\in\Pi_{SD}$ exists.
3. Equation (5.6) (p. 301): $(1-\beta)J^*_\beta(0)+h_\beta(i)=\min_{a\in U(i)}\{c(i,a)+\beta\sum_jP(j\mid i,a)h_\beta(j)\}$.
4. Theorem 5.1 (p. 299): a solution of (5.1) with $\lim_t\frac1tE^\pi_ih(X_t)=0$ gives $\rho=J(i,f)=J^*(i)$ for a minimizing selector $f$; minimizing selectors are average optimal; conversely, an average optimal $f$ with an irreducible positive recurrent chain is a minimizing selector.
5. Remark 5.1(a) (p. 300): a bounded solution of (5.1) satisfies the growth condition of Theorem 5.1.

Significance

Theorem 5.2 is the template of the vanishing discount method. Under its hypothesis the average cost problem has a bounded solution of the ACOE, so (through Theorem 5.1) the optimal average cost is a constant $\rho$ independent of the initial state, it is attained by a stationary deterministic policy, and it is the Abelian limit of the scaled discounted values. Recurrence conditions on the controlled chain, such as uniformly bounded mean return times to a fixed state (Theorem 5.3 of the survey), are verified by checking the hypothesis of Theorem 5.2; the later results of §5 refine its conclusion under weaker hypotheses.

The theorem itself is classical. What this mission adds is a machine-checked statement and, eventually, proof, on a model with history-dependent randomized policies, compact action sets and unbounded costs, together with the supporting verification theorem (Theorem 5.1) and the discounted optimality equation. To our knowledge none of these results has been formalized in Lean; Mathlib has the Ionescu-Tulcea construction of the path measure but no controlled Markov processes.

Difficulty

The obvious argument fixes a sequence $\beta_n\uparrow1$, extracts a pointwise convergent subsequence of the bounded functions $h_{\beta_n}$ and of the bounded numbers $(1-\beta_n)J^*_{\beta_n}(0)$, and passes to the limit in (5.6). Two steps resist this. First, the limit of a minimum over $U(i)$ is not in general the minimum of the limits: the convergence of $a\mapsto\sum_jP(j\mid i,a)h_{\beta_n}(j)$ must be shown to be uniform on the compact set $U(i)$, which requires more than pointwise continuity of each $P(j\mid i,\cdot)$. Second, the subsequential limit $\rho$ could depend on the subsequence, so part (iii), a limit along all $\beta\uparrow1$, needs an independent identification of $\rho$, here as the optimal average cost through Theorem 5.1, which in turn needs the comparison with arbitrary history-dependent policies. The discounted optimality equation behind (5.6) also has to be established for unbounded costs, where $J^*_\beta$ is not the unique fixed point of $T_\beta$.

Formalization scope

The state space is ℕ; state 0 is the reference state of $h_\beta$. Policies are history-dependent randomized stochastic kernels with the admissibility constraint $\pi_t(U(x_t)\mid h_t)=1$, and $J^*$, $J^*_\beta$ are infima over all of them. Costs are lower Lebesgue integrals with values in $[0,\infty]$, built from Mathlib's Kernel.trajMeasure. The following choices make implicit hypotheses explicit:

• Finiteness of $J^*_\beta$. The paper's bound $|h_\beta|\le K$ presupposes finite values; the goal assumes $J^*_\beta(i)<\infty$, and (5.6) assumes it for its $\beta$.
• Convergent series in the ACOE. A solution of (5.1) requires every series $\sum_jP(j\mid i,a)h(j)$, $a\in U(i)$, to converge, and the minimum to be attained.
• (5.2) over all policies. The paper prints the growth condition of Theorem 5.1 for $\pi\in\Pi_{SD}$, but its conclusion $\rho=J^*(i)$ concerns all policies, and the proof uses the condition for arbitrary $\pi$. It is stated for every $\pi\in\Pi$, with integrability of $h(X_t)$ explicit.
• Theorem 2.1 is cited without proof in the survey for Borel models; in the countable model its Assumptions 2.2–2.3 follow from the continuity assumptions of §5. Only parts (i) and (iii) are stated.
• Lemma 2.1 is stated for functions bounded below (on discrete ℕ these are the lower semicontinuous functions bounded below), with convergent series.
• Irreducible, positive recurrent (converse of Theorem 5.1): every state is reached with positive probability from every state, and every state has finite expected return time.

A formalization in which $J^*$ is an infimum over stationary policies only, in which the ACOE is an inequality or holds for one fixed action, or in which $h_\beta$ is computed from $+\infty$ values through a junk conversion, would trivialize the goal; all three are excluded by the definitions above.

A complete development needs the Ionescu-Tulcea path measure for history-dependent policies, the discounted optimality equation for nonnegative unbounded costs, Scheffé-type uniform convergence on compact action sets, and the martingale identity behind Theorem 5.1. The model file is reusable by the other missions of this series and by any countable-state average cost result; proofs of the milestones are welcome independently of the goal.

Selected references

• A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2) (1993) 282–344. https://doi.org/10.1137/0331018
• C. Derman, On sequential decisions and Markov chains, Management Sci. 9 (1962) 16–24 (reference [38] of the survey).
• C. Derman, Denumerable state Markovian decision processes — average cost criterion, Ann. Math. Statist. 37 (1966) 1545–1553 (reference [39]).
• H. M. Taylor, Markovian sequential replacement processes, Ann. Math. Statist. 36 (1965) 1677–1694 (reference [177]).
• S. M. Ross, Non-discounted denumerable Markovian decision models, Ann. Math. Statist. 39 (1968) 412–423, and Arbitrary state Markovian decision processes, Ann. Math. Statist. 39 (1968) 2118–2122 (references [147], [148]).
• S. M. Ross, Introduction to Stochastic Dynamic Programming, Academic Press, New York, 1983 (reference [150]).
• L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Oper. Res. 37 (1989) 626–633 (reference [156]).

Motivation

A single-server queue in which customers arrive according to a renewal process and are served in exponentially distributed times is the system GI/M/1. Observed just before successive arrivals, its queue length is a Markov chain on $\{0, 1, 2, \dots\}$, the imbedded chain introduced by D. G. Kendall (Kendall 1953, Ann. Math. Statist. 24, pp. 338–354). Whether this chain settles into a statistical equilibrium, keeps returning to the empty state without one, or drifts off to infinity is the first question asked about the queue, and every later quantity (stationary queue lengths, waiting-time distributions) presupposes the answer.

F. G. Foster's 1953 paper (Foster 1953) answers it for GI/M/1 and for M/G/1 by a different route from Kendall's direct analysis: it first proves general criteria, stated in terms of solutions of linear equations and inequalities in the transition matrix, for a countable Markov chain to be ergodic, recurrent or transient, and then checks them on the two queueing matrices. The criteria are of independent use; one of them (Theorem 2 of the paper) is now known as Foster's criterion, the starting point of the drift (Lyapunov-function) method for stability of Markov chains and queueing networks.

Timeline. Kendall (1951, J. Roy. Statist. Soc. B 13) studied queue-length processes directly, including a recurrence argument for M/G/1 that Foster's §3 reproduces; Kendall (1953) introduced the imbedded-chain method and, for GI/M/1, proved by it that $\rho < 1$ is sufficient for ergodicity (Foster 1953, p. 359); Foster (1953) proved the full classification, ergodic iff $\rho < 1$ and recurrent iff $\rho \le 1$, by the general criteria. This mission treats the GI/M/1 half; a companion mission treats M/G/1.

Setting

A transition matrix on the states $\{0, 1, 2, \dots\}$ is an array $[p_{ij}]$ of nonnegative reals whose rows sum to $1$. For a state $j$, $f_{jj}$ is the probability that the chain started at $j$ returns to $j$ at some later step. The chain is recurrent if $f_{jj} = 1$ for every $j$, transient if $f_{jj} < 1$ for every $j$, and ergodic (recurrent-nonnull, positive recurrent) if moreover every mean recurrence time $\sum_n n f^{(n)}_{jj}$ is finite. Foster's general theorems concern an irreducible chain (every state reachable from every state), assumed aperiodic for simplicity.

The GI/M/1 chain is described by a sequence $a = (a_n)_{n \ge 0}$ of positive numbers with $\sum_n a_n = 1$: $a_n$ is the probability that exactly $n$ services are completed between two arrivals. With the tails $\alpha_i = \sum_{j \ge i+1} a_j$,

$$[p_{ij}] = \begin{bmatrix} \alpha_0 & a_0 & 0 & 0 & \cdots \\ \alpha_1 & a_1 & a_0 & 0 & \cdots \\ \alpha_2 & a_2 & a_1 & a_0 & \cdots \\ \vdots & \vdots & \vdots & \vdots & \end{bmatrix},$$

that is $p_{i0} = \alpha_i$, $p_{ij} = a_{i+1-j}$ for $1 \le j \le i+1$, and $p_{ij} = 0$ for $j > i+1$. In Lean this matrix is gim1Matrix a. The traffic parameter $\rho$ is defined through its inverse,

$$\rho^{-1} = \sum_{n=1}^{\infty} n\, a_n \in (0, \infty],$$

the mean number of service completions per interarrival interval (rhoInv a, and rho a $= \rho$).

Formalization targets

Goal: the classification of GI/M/1 (§4, p. 359)

$$\text{the chain is ergodic} \iff \rho < 1, \qquad \text{the chain is recurrent} \iff \rho \le 1 .$$

Together: ergodic for $\rho < 1$, recurrent-null for $\rho = 1$, transient for $\rho > 1$. The statement carries no constants and leaves the sequence $a$ free apart from positivity and normalization.

Milestones

1. Theorem 7 (p. 358): for a probability distribution $\{p_n\}$ with $p_0 > 0$, the equation $\sum_{n \ge 0} z^n p_n = z$ has a root in $(0, 1)$ iff $\sum_{n\ge1} n p_n > 1$.
2. Theorem 1, sufficiency (p. 355): a nonnull solution of $\sum_i x_i p_{ij} = x_j$ with $\sum_i |x_i| < \infty$ makes the system ergodic.
3. Theorem 1, necessity (p. 355): in an ergodic system every nonnegative solution of $\sum_i x_i p_{ij} \le x_j$ has $\sum_i x_i < \infty$.
4. Theorem 4 (pp. 356–357): the system is transient iff $\sum_j p_{ij} y_j = y_i$ ($i \ne 0$) has a bounded nonconstant solution.

Milestones 2–4 are stated for a general irreducible aperiodic chain.

Significance

The classification tells exactly when the GI/M/1 queue is stable: the stationary distribution of the imbedded chain, which is geometric, exists precisely in the ergodic case $\rho < 1$, and for $\rho > 1$ the queue grows without bound. Theorems 1 and 4 are general tools, reusable for any countable chain: Theorem 1 characterizes ergodicity by summable invariant vectors, Theorem 4 characterizes transience by bounded harmonic functions off one state. Theorem 7 is the extinction criterion of branching processes and recurs throughout applied probability.

All of these results are proved in the literature (Foster 1953; Feller's textbook for Theorem 7 and a version of Theorem 4). As far as a search of the platform shows, none of them has a machine-checked proof; the platform holds related special cases for the G/M/1 queue with a specific interarrival law (QueueingFundamentals.GM1.unique_root_unit_interval, open), but not the general lemma or the classification. A formalization would provide the general criteria as reusable library results and the first verified stability classification of a non-Markovian queue's imbedded chain.

Difficulty

The matrix is explicit, but none of the three properties is a finite computation: ergodicity and recurrence are statements about return times over all horizons, so each direction must go through an existence or nonexistence statement about infinite systems of equations. For the converse directions the obvious argument fails: exhibiting a candidate solution such as $x_i \equiv 1$ shows nothing until it is known that ergodicity forces every such solution to be summable, and showing that no bounded nonconstant solution of (7) exists when $\rho < 1$ requires control of all solutions, not of one. The general criteria themselves rest on limit theorems for $p_{ij}^{(n)}$ and on interchanging infinite sums, and the infinite-mean case $\sum n a_n = \infty$ has to be carried along everywhere.

Formalization scope

• The Markov-chain vocabulary is the published definition QueueingFundamentals_Foundations_MarkovChain: TransitionMatrix (entries p, nonnegativity, rows summing to $1$ via HasSum), returnProb, meanRecurrenceTime, Irreducible, Aperiodic, PositiveRecurrent. "Ergodic" is PositiveRecurrent. IsRecurrent and IsTransient are defined state by state from returnProb; their complementarity for irreducible chains is a theorem, not a definition.
• States are indexed from $0$, as in the paper. The goal quantifies over every TransitionMatrix whose entries equal gim1Matrix a; such a matrix exists for every admissible $a$ (rows sum to $1$), so the statement is not vacuous.
• $\rho^{-1}$ and $\rho$ live in $[0, \infty]$ (ℝ≥0∞), with $\infty^{-1} = 0$: an infinite mean gives $\rho = 0$, and that chain is ergodic.
• The goal does not assume irreducibility or aperiodicity: they follow from $a_n > 0$. Milestones 2–4 carry them, as the paper's standing assumptions (§1).
• Every infinite series appearing in a hypothesis is required to converge (HasSum or Summable), so that a divergent series cannot satisfy an equation or inequality vacuously. In Theorem 1's sufficiency half the $x_i$ may be of either sign. In Theorem 7 the distribution is renamed $q$ to avoid a clash with $p_{ij}$.
• Ruled out as trivializing: defining $\rho$ by a real inverse of a real series, defining "ergodic" as the existence of a summable invariant vector (which is Theorem 1's condition), or stating the goal over a matrix that need not exist.
• Not included: the paper's explicit description of the solutions of (7) for $\rho \ge 1$ via the generating function $(1 - z)\{A(z) - z\}^{-1}$, and the M/G/1 half (Theorems 2, 3, 5), which is the companion mission. Contributions welcome: proofs of the general criteria (reusable for any countable chain), of Theorem 7, and lemmas on the GI/M/1 matrix such as irreducibility and aperiodicity.

Selected references

• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24 (1953), 355–360. https://doi.org/10.1214/aoms/1177728976
• D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Ann. Math. Statist. 24 (1953), 338–354 (the paper immediately preceding Foster's in the same issue).
• D. G. Kendall, Some problems in the theory of queues, J. Roy. Statist. Soc. B 13 (1951), 151–185.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, Wiley, 1950.

Motivation

The neutral theory of molecular evolution holds that much of the genetic variation observed at the molecular level is caused by selectively neutral mutations rather than by selection. To test it against data one needs the distribution of allele frequencies that a neutral model predicts, and in practice that distribution has to be compared with a sample from the population, never with the whole population. Ewens (Ewens 1972) derived the equilibrium distribution of allele counts under the infinite alleles model, now called the Ewens sampling formula; it underlies classical tests of neutrality and appears throughout combinatorics and probability as the law of the cycle type of an Ewens-distributed random permutation and of the Chinese restaurant process.

Chapter 7 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) obtains the infinite alleles model as a limit of the reversible migration processes of Chapters 2 and 6, and uses reversibility to answer questions about allele ages and fixation. The mission formalizes the finite, combinatorial results of that chapter.

Timeline. Kimura and Crow (1964) introduced the infinite alleles model. Ewens (1972) found its equilibrium sampling distribution (7.6). Kingman (1978, J. London Math. Soc.) characterized the consistency of random partitions under sampling, the property Theorem 7.1 asserts for the Ewens family. Kelly (1979, Chapter 7) derived (7.6) as a limit of reversible migration processes, and the consistency and the allele-age results from the reversibility of a labelled population process.

Setting

A population consists of $M\ge2$ individuals, each carrying an allelic type. Its description is $\mathbf M=(M_1,\dots,M_M)$, where $M_i$ is the number of allelic types carried by exactly $i$ individuals, so that

$$\sum_{i=1}^{M} iM_i=M. \qquad (7.3)$$

For a real parameter $\nu>0$, the Ewens distribution on descriptions is

$$\pi_M(\mathbf M)=\binom{\nu+M-1}{M}^{-1}\prod_{i=1}^{M}\Big(\frac{\nu}{i}\Big)^{M_i}\frac{1}{M_i!}, \qquad (7.6)$$

where $\binom{x}{k}=x(x-1)\cdots(x-k+1)/k!$ is the binomial coefficient for real $x$. In the infinite alleles model, individuals die at rate $\mu$, each death is followed by the birth of an offspring of a uniformly chosen survivor, and the offspring is a mutant of an entirely new type with probability $u$; then (7.6) is the equilibrium distribution with $\nu=(M-1)u/(1-u)$ (7.5).

A random sample of size $1\le m\le M$ without replacement is a uniformly random $m$-element subset of the $M$ labelled individuals, each of the $\binom Mm$ subsets being equally likely; the sample has a description in the same sense.

The number $j$ of individuals carrying one given allele performs a random walk on $\{0,\dots,M\}$ with intensities

$$q(j,j-1)=\mu\frac jM\Big(\frac{M-j}{M-1}+\frac{j-1}{M-1}u\Big),\qquad q(j,j+1)=\mu\frac{M-j}{M}\frac{j}{M-1}(1-u). \qquad (7.8)$$

An allele is quasi-fixed when it is the only allele present ($j=M$).

Formalization targets

Goal: consistency under sampling (Theorem 7.1)

If $M\ge2$ and the population description is distributed as $\pi_M$, then a random sample of size $1\le m\le M$ drawn without replacement has description $\mathbf m$ with probability $\pi_m(\mathbf m)$, the same $\nu$ being used for both sizes:

$$\sum_{\mathbf M}\pi_M(\mathbf M)\,P\big(\text{sample has description }\mathbf m\mid\text{population has description }\mathbf M\big)=\pi_m(\mathbf m).$$

Milestones

1. (7.6) is a distribution: $\pi_M(\mathbf M)>0$ and $\sum_{\mathbf M}\pi_M(\mathbf M)=1$ (Exercise 7.1.3).
2. Theorem 7.1 for $m=M-1$, the case the book's proof establishes first.
3. Corollary 7.5, the identity of its proof: the probability that a uniformly chosen individual's allele is carried by exactly $i$ individuals is

$$\sum_{\mathbf M}\frac{iM_i}{M}\pi_M(\mathbf M)=\frac{\nu}{M}\binom{\nu+M-1}{i}^{-1}\binom Mi. \qquad (7.9)$$

4. Theorem 7.9: the probability $Q$ that the walk (7.8) started at $1$ reaches $M$ before $0$ satisfies

$$Q^{-1}=\sum_{i=0}^{M-1}\binom{M-1}{i}^{-1}\binom{\nu+M-1}{i}.$$

Significance

The results. Consistency under sampling is what makes the Ewens formula usable as a statistical model: the predicted distribution for an observed sample does not depend on the unknown population size, only on $\nu$. Kelly deduces from it the sufficiency of the number of alleles in a sample for $\nu$ and the heterozygosity $\nu/(\nu+1)$ (Exercises 7.1.5, 7.1.8). The formula (7.9) gives the equilibrium frequency of the oldest allele, and Theorem 7.9 gives the quasi-fixation probability from which the mean time between quasi-fixations follows (Corollary 7.10).

Formalizing them. All four results are classical and proved; none has a machine-checked proof on the platform or in Mathlib as of this writing. The mission produces a reusable formal Ewens distribution over integer partitions, a definition of sampling without replacement by counting labelled subsets, and an absorption probability for an explicit birth–death walk. Proofs independent of Kelly's process argument are welcome.

Difficulty

The book's proof of Theorem 7.1 is a process argument: in a population whose size fluctuates between $M-1$ and $M$, a drop in size acts as a random deletion, and the truncated equilibrium (7.7) restricted to each size gives $\pi_{M-1}$ and $\pi_M$. Turning that into a statement about finite sets requires the equilibrium of a truncated reversible process, which is not available here, so a formal proof must either build that process or find a direct combinatorial route. A direct route has to relate, for each description of the sample, the number of $m$-subsets of a labelled population with a given description to products of binomial coefficients, and sum the result against (7.6); the bookkeeping over partitions is where the work lies. Theorem 7.9 needs a solution of the first-step equations of a non-symmetric walk and the identification of that solution with a hitting probability defined as a limit.

Formalization scope

• Descriptions of $n$ individuals are integer partitions Nat.Partition n, with $M_i$ the multiplicity of the part $i$; the product in (7.6) runs over $i=1,\dots,n$. The real binomial coefficient is the published definition AppliedComb.GenFun.binomReal.
• The population is Fin M with allelic types Fin M → ℕ; the description of a labelled set is computed from the labelling. The sampling probability is $\binom Mm^{-1}$ times the number of $m$-subsets whose restricted labelling has the given description. It is not defined by a formula on descriptions, and a definition that removed individuals one at a time in proportion to class sizes (the book's proof route) is ruled out as a definition because it presupposes the reduction the proof must supply.
• The goal and Corollary 7.5 quantify over an arbitrary choice of labelling for each population description. They assume $M\ge2$, as required by the chapter's rule that a parent is chosen among the other $M-1$ individuals; the goal also assumes $1\le m\le M$. Because $\pi_M>0$, this forces the conditional sampling law to depend on the population only through its description. Types are natural numbers, so every description is realized and the hypothesis is never vacuous.
• The quasi-fixation probability is defined through the jump chain of (7.8): the limit of the probabilities of reaching $M$ within $n$ jumps without reaching $0$. The theorem assumes $M\ge2$, $\mu>0$, $0<u<1$ and $\nu=(M-1)u/(1-u)$.
• Corollary 7.5 is formalized as the identity of its proof. The identification of the oldest allele's frequency with that of a randomly chosen individual uses allele ages and the reversibility of the labelled process (Theorem 7.2) and is not formalized. Theorem 7.2 itself, whose state space orders the allele labels within each class, and the allele-age results (Corollaries 7.3, 7.4, 7.7, 7.8, Theorem 7.6, Corollary 7.10, Theorem 7.11) are not part of the mission.

Contributions of general partition and sampling lemmas (counting subsets with a given description, the generating function identity $(1-x)^{-\nu}=\prod_j e^{\nu x^j/j}$) are reusable beyond this mission.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979, Chapter 7. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• W. J. Ewens, The sampling theory of selectively neutral alleles, Theoretical Population Biology 3 (1972), 87–112. https://doi.org/10.1016/0040-5809(72)90035-4
• J. F. C. Kingman, The representation of partition structures, Journal of the London Mathematical Society (2) 18 (1978), 374–380. https://doi.org/10.1112/jlms/s2-18.2.374
• M. Kimura and J. F. Crow, The number of alleles that can be maintained in a finite population, Genetics 49 (1964), 725–738. https://doi.org/10.1093/genetics/49.4.725

Motivation

Many queues observed at well-chosen instants are Markov chains on the nonnegative integers. For the single-server queue with Poisson arrivals and general service times (M/G/1), D. G. Kendall showed in 1951 that the number of customers left behind at successive departure epochs is such a chain, the imbedded Markov chain (Kendall 1951; Kendall 1953). Whether the queue settles into a steady state, keeps returning to empty without settling, or grows without bound is then a question about this chain: is it ergodic, null recurrent, or transient?

F. G. Foster's 1953 paper (doi:10.1214/aoms/1177728976) answers this question by first proving general criteria for an irreducible chain on $\{0,1,2,\dots\}$, stated as solvability conditions for linear inequalities in the transition matrix, and then applying them to the M/G/1 and GI/M/1 chains. Theorem 2 of the paper is the drift condition now known as Foster's criterion, the starting point of the Lyapunov-function method for the stability of queues and stochastic networks (Meyn and Tweedie 2009). This mission is the M/G/1 half of the paper.

Timeline:

• 1951–1953, Kendall. Introduces the imbedded chains of M/G/1 and GI/M/1 and obtains most of their classification by direct methods.
• 1953, Foster. Derives the classification from general criteria: Theorem 2 (ergodicity), Theorems 4–6 (transience and recurrence).
• 1950s onward. The criteria become the standard tools (Feller's text; later the drift conditions of Meyn and Tweedie).

Setting

A Markov chain on the states $\{0,1,2,\dots\}$ is given by a transition matrix $P=[p_{ij}]$: $p_{ij}\ge0$ and $\sum_j p_{ij}=1$ for every row $i$. Write $f_{ij}^{(n)}$ for the probability that the chain started in $i$ first reaches $j$ (for $i=j$, first returns to $j$) at step $n\ge1$. The chain is irreducible if every state can be reached from every other, and aperiodic if for every state the return times have greatest common divisor $1$. A state $j$ is recurrent if $f_{jj}=\sum_n f_{jj}^{(n)}=1$ and transient if $f_{jj}<1$; a recurrent state is ergodic (positive recurrent, "recurrent-nonnull") if in addition its mean recurrence time $\sum_n n f_{jj}^{(n)}$ is finite. The mean first-passage time from $i$ to $j$ is $\mu_{ij}=\sum_{n\ge1} n f_{ij}^{(n)}\in[0,\infty]$.

The M/G/1 matrix is built from a sequence $k_0,k_1,\dots$ of positive numbers summing to one ($k_n$ is the probability of $n$ arrivals during one service):

$$[p_{ij}] = \begin{bmatrix} k_0 & k_1 & k_2 & \cdots \\ k_0 & k_1 & k_2 & \cdots \\ 0 & k_0 & k_1 & \cdots \\ 0 & 0 & k_0 & \cdots \\ \vdots & \vdots & \vdots & \end{bmatrix},$$

that is, $p_{0j}=k_j$ and, for $i\ge1$, $p_{ij}=k_{j-i+1}$ when $j\ge i-1$ and $0$ otherwise. The traffic intensity is

$$\rho=\sum_{n=1}^{\infty}n\,k_n\in[0,\infty],$$

the mean number of arrivals per service.

Formalization targets

Goal: the M/G/1 classification (§3, p. 358)

$$\text{the chain is ergodic}\iff\rho<1,\qquad\text{the chain is recurrent}\iff\rho\le1 .$$

The goal leaves $k$ arbitrary apart from positivity and normalization; in particular $\rho=\infty$ is allowed and falls in the transient case.

Milestones (the paper's general theorems and the step of §3 they feed)

1. Theorem 2 (drift criterion): a nonnegative solution of $\sum_j p_{ij}y_j\le y_i-1$ ($i\ne0$) with $\sum_j p_{0j}y_j<\infty$ makes the system ergodic. Already posed on the platform and referenced here.
2. Theorem 3: in an ergodic system the mean first-passage times $d_j=\mu_{j0}$ are finite and satisfy $\sum_{j\ge1}p_{ij}d_j=d_i-1$ ($i\ne0$), $\sum_{j\ge1}p_{0j}d_j<\infty$.
3. §3 display: for the ergodic M/G/1 chain, $\mu_{i,i-1}=\mu_{10}$ and $\mu_{i0}=i\mu_{10}$ ($i\ne0$).
4. Theorem 5: a solution of $\sum_j p_{ij}y_j\le y_i$ ($i\ne0$) with $y_i\to\infty$ makes the system recurrent.
5. Theorem 7: for a probability distribution $\{p_n\}$ with $p_0>0$, $\sum_n z^np_n=z$ has a root in $(0,1)$ iff $\sum_{n\ge1}np_n>1$.
6. Theorem 4: the system is transient iff $\sum_j p_{ij}y_j=y_i$ ($i\ne0$) has a bounded nonconstant solution.

Significance

The result. The classification is the stability theorem for the M/G/1 queue: for $\rho<1$ the departure-epoch queue length has a stationary distribution, which is what the Pollaczek–Khinchine formula describes; for $\rho=1$ the queue empties infinitely often but has no steady state; for $\rho>1$ it grows without bound. The general criteria behind it (Theorems 2, 4, 5) apply to any chain on the nonnegative integers and are reused in the companion GI/M/1 mission and throughout queueing and Markov-chain stability theory.

Formalizing it. All results here are proved on paper (Kendall and Foster, 1951–1953, with Theorems 3 and 7 classical lemmas from Feller). None of them is known to have a machine-checked proof against a Lean development of countable-state Markov chains. The mission produces such proofs on the published discrete-chain vocabulary (transition matrices, first-passage probabilities, return probabilities, positive recurrence), together with the general Foster criteria as reusable theorems. Theorem 2 is already posed as an open platform theorem and is reused here.

Difficulty

The queue-specific part of the argument is short once the general criteria are available; the weight of the mission is in those criteria. They relate qualitative properties of an infinite chain (ergodicity, recurrence, transience) to solvability of infinite systems of linear inequalities, and this needs limit behaviour of the $n$-step probabilities $p_{ij}^{(n)}$ and of hitting probabilities of state $0$, none of which follows from finite-state arguments. Two further points resist the naive approach. The converse directions (ergodic $\Rightarrow\rho<1$, recurrent $\Rightarrow\rho\le1$) need exact identities for mean first-passage times, not just bounds, and these must be handled in $[0,\infty]$ because the means may be infinite. And the boundary case $\rho=1$ (null recurrence) separates the two equivalences: an argument that only compares the mean drift $\rho-1$ with $0$, such as a law of large numbers for the increments, cannot tell recurrence from transience there.

Formalization scope

• The chain is the published QueueingFundamentals.Foundations.TransitionMatrix (entries P.p i j, rows summing to $1$ as a HasSum), with its firstPassage, returnProb, Irreducible, Aperiodic and PositiveRecurrent. "Ergodic" is P.PositiveRecurrent; aperiodicity is the paper's standing assumption and is not folded into it a second time.
• States are indexed from $0$, as in the paper; "$i\ne0$" is i ≠ 0.
• The M/G/1 matrix is a function mg1Matrix k : ℕ → ℕ → ℝ; the goal and the §3 display quantify over every TransitionMatrix P with P.p = mg1Matrix k. Such a P exists for every admissible k (checked in a sorry-free local file for $k_i=2^{-(i+1)}$).
• $\sum_n k_n=1$ is added as the meaning of "stochastic matrix"; §3 writes only $k_i>0$.
• $\rho$ and all mean first-passage times are extended nonnegative reals ($[0,\infty]$), so divergent means are $\infty$, never $0$. Theorem 7's mean is also taken in $[0,\infty]$.
• Recurrent means $f_{jj}=1$ for every state $j$; transient means $f_{jj}<1$ for every state. For irreducible chains these are complementary, which is a theorem, not a definition.
• The general Theorems 3, 4 and 5 assume irreducibility and aperiodicity, the paper's standing assumption of §1. The goal does not assume them: they follow from $k_i>0$.
• Every series in a hypothesis carries its convergence (Summable or HasSum); Theorem 3's equation (6) is written as $d_i=1+\sum_{j\ge1}p_{ij}d_j$ in $[0,\infty]$ together with finiteness of the $d_j$, $j\ne0$.
• Theorem 7's distribution is renamed $q$ in Lean to avoid a clash with $p_{ij}$. Theorem 1 of the paper (§2) and Theorem 6 are not targets of this mission.

Ruled out: $\rho$ as a real tsum (which is $0$ for a divergent series and would call a heavy-tailed chain ergodic); defining "ergodic" or "recurrent" through the existence of Lyapunov or drift functions (which would make the criteria tautological); a goal over a matrix $P$ that need not exist.

Contributions welcome: proofs of the general criteria (Theorems 2–5) on the published chain vocabulary, the limit theorem $p_{ij}^{(n)}\to\pi_j$ for irreducible aperiodic chains, first-step analysis for hitting times, and Theorem 7 as a lemma on probability generating functions; all of these are reusable beyond this mission.

Selected references

• F. G. Foster, On the stochastic matrices associated with certain queuing processes, The Annals of Mathematical Statistics 24(3), 355–360, 1953. https://doi.org/10.1214/aoms/1177728976
• D. G. Kendall, Some problems in the theory of queues, Journal of the Royal Statistical Society B 13(2), 151–185, 1951. https://doi.org/10.1111/j.2517-6161.1951.tb00093.x
• D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, The Annals of Mathematical Statistics 24(3), 338–354, 1953. https://doi.org/10.1214/aoms/1177728975
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, Wiley, 1950.
• S. Meyn and R. L. Tweedie, Markov Chains and Stochastic Stability, 2nd ed., Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511626630