Motivation

A branching random walk is the simplest model of a population that both reproduces and moves: every particle dies and leaves a random cloud of children displaced relative to it. Its extreme particles control the speed of travelling waves in reaction–diffusion equations (the KPP/Fisher equation), the free energy of directed polymers on trees, the cover and hitting times of random walks on trees, and the maxima of log-correlated fields such as the two-dimensional Gaussian free field. The basic quantity is the position of the leftmost particle at time $n$.

Timeline.

• 1974–1976: Hammersley, Kingman and Biggins prove the law of large numbers $M_n/n\to\gamma$ for the minimum.
• 1978–1983: Bramson shows that for branching Brownian motion the maximum, centred at $\sqrt2\,t-\frac{3}{2\sqrt2}\ln t$, converges in law (Bramson 1983). Lalley and Sellke (1987, Ann. Probab. 15) identify the limit as a Gumbel law randomly shifted by the limit of the derivative martingale.
• 2004: Biggins and Kyprianou prove that the derivative martingale of a branching random walk converges to a limit that is non-trivial in the boundary case (Adv. Appl. Probab. 36).
• 2009: Hu and Shi (arXiv:math/0702799) and Addario-Berry and Reed (Ann. Probab. 37) find the logarithmic correction: $M_n-\frac32\ln n$ is tight. Bramson and Zeitouni (2009) obtain tightness around the median under tail assumptions.
• 2013: Aïdékon proves convergence in law of $M_n-\frac32\ln n$ for general non-lattice branching random walks, the result this mission formalizes (arXiv:1101.1810, Ann. Probab. 41 (2013)).

Setting

Let $\mathcal L$ be a point process on $\mathbb R$: a random, possibly infinite, collection of points. Start one particle at $0$. At time $1$ it dies and leaves children at the points of $\mathcal L$; each particle of generation $n$ then dies and leaves children at the points of an independent copy of $\mathcal L$, translated to its own position. Vertices of the genealogical tree $\mathbb T$ (a Galton–Watson tree) are labelled by finite words $u=(i_0,\dots,i_{k-1})$; $|u|=k$ is the generation, $u_j$ the ancestor at generation $j$, and $V(u)$ the position.

The paper works in the boundary case

$$\mathbf E\Big[\sum_{|x|=1}1\Big]>1,\qquad \mathbf E\Big[\sum_{|x|=1}e^{-V(x)}\Big]=1,\qquad \mathbf E\Big[\sum_{|x|=1}V(x)e^{-V(x)}\Big]=0,\tag{1.1}$$

and assumes throughout that $\mathcal L$ is non-lattice and that

$$\mathbf E\Big[\sum_{|x|=1}V(x)^2e^{-V(x)}\Big]<\infty,\qquad \mathbf E\big[X(\ln_+X)^2\big]<\infty,\qquad \mathbf E\big[\tilde X\ln_+\tilde X\big]<\infty,\tag{1.3–1.4}$$

with $X=\sum_{|x|=1}e^{-V(x)}$ and $\tilde X=\sum_{|x|=1}V(x)_+e^{-V(x)}$. The objects of the main theorem are the minimum $M_n=\min\{V(x):|x|=n\}$ (with $\min\varnothing=+\infty$) and the derivative martingale

$$D_n=\sum_{|x|=n}V(x)e^{-V(x)},$$

which converges almost surely to a limit $D_\infty\ge0$, strictly positive on non-extinction. A standard example: two children with i.i.d. normal displacements of mean and variance $2\ln2$.

Formalization targets

Goal: Theorem 1.1

There is a constant $C^*\in(0,\infty)$ such that for every real $x$,

$$\lim_{n\to\infty}\mathbf P\Big(M_n\ge\tfrac32\ln n+x\Big)=\mathbf E\Big[e^{-C^*e^xD_\infty}\Big].$$

The constant is not specified numerically. It is the product $C_1c_0$ of the constants below.

Milestones, in the order the proof uses them

1. Many-to-one lemma (2.1): $\mathbf E_a[\sum_{|x|=n}g(V(x_1),\dots,V(x_n))]=\mathbf E_a[e^{S_n-a}g(S_1,\dots,S_n)]$ for a centred random walk $S$.
2. Renewal function (2.13): the renewal function $R$ of the strict descending ladder heights of $S$ satisfies $R(x)/x\to c_0>0$.
3. Corollary 3.2 and Proposition 1.2: for the walk killed below $0$, $e^z\,\mathbf P(M_n^{\rm kill}<\frac32\ln n-z)\to C_1$, uniformly for $z\in[A,\frac32\ln n-A]$.
4. Global minimum bound: $\mathbf P(\exists u\in\mathbb T: V(u)\le-y)\le e^{-y}$.
5. Corollary 3.5: $\mathbf P(M_n\le\frac32\ln n-y)\le(1+c_{10}(1+y))e^{-y}$.
6. Proposition 4.1: $\frac{e^z}{z}\mathbf P(M_n<\frac32\ln n-z)\to C_1c_0$, uniformly on the same window.
7. Derivative martingale: $D_n\to D_\infty$ a.s., $D_\infty\ge0$, $D_\infty>0$ a.s. on non-extinction.
8. (5.2): $\sum_{u\in\mathcal Z[A]}V(u)e^{-V(u)}\to D_\infty$ a.s. as $A\to\infty$, where $\mathcal Z[A]$ is the set of particles absorbed at level $A$.

Significance

The theorem identifies the limit law of the extreme particle: $M_n-\frac32\ln n$ converges in law, on the event of survival, to a Gumbel variable shifted by $-\ln(C^*D_\infty)$. It is the input for the study of the whole extremal process of the branching random walk seen from its leftmost particle (Madaule, J. Theoret. Probab., 2017), and it is the discrete-time counterpart of the Bramson and Lalley–Sellke results that later work on log-correlated fields takes as its template. The $\frac32$ correction and the role of the derivative martingale are the signature of the boundary case, and of log-correlated extremes generally.

The result is proved and published. It has not been formalized: Mathlib has no branching processes, no Galton–Watson trees with positions, no renewal theory, and no derivative martingale. This mission produces the first machine-checkable statement of the convergence-in-law theorem and of the intermediate results it rests on. A complete development would also give reusable formal versions of the many-to-one lemma and of renewal theory for ladder heights.

Difficulty

The first-moment computation through the many-to-one lemma gives the wrong centring. It predicts that the minimum sits near $\frac12\ln n$, because the expected number of particles below a level is dominated by rare realisations. The true centring $\frac32\ln n$ only appears after restricting to particles whose ancestral path stays above a barrier, and this restriction requires random-walk estimates (ballot theorems and local limit theorems for walks conditioned to stay positive) that hold uniformly in a window of starting points. A second difficulty is that the limit must be identified, not only shown to exist. Tightness and subsequence arguments do not give the factor $D_\infty$; the identification needs the precise tail $C_1c_0\,z\,e^{-z}$ of Proposition 4.1, with a known constant, and the almost-sure behaviour of the sum over the stopping line $\mathcal Z[A]$.

Formalization scope

• Point process. The law $L$ of $\mathcal L$ is a probability measure on configurations $(N,p)\in\mathbb N_\infty\times(\mathbb N\to\mathbb R)$, where the points are $p_i$ for $i<N$.
• Tree. Labels are List ℕ. The branching random walk is any family $(\xi_u)_{u}$ of independent measurable configurations of law $L$ on a probability space. Every theorem holds for every such realisation, and a canonical realisation exists (product space).
• Assumptions. Every expectation in (1.1), (1.3), (1.4) is a lower Lebesgue integral of a $[0,\infty]$-valued sum. The signed condition in (1.1) is "the expectations of $\sum V_+e^{-V}$ and $\sum V_-e^{-V}$ are equal and finite". Non-lattice means: there are no $a\in\mathbb R$ and $d>0$ with all points a.s. in $a+d\mathbb Z$.
• Which assumptions where. The goal and §§3–5 assume all of them. The many-to-one lemma and the global minimum bound assume only (1.1), and the derivative-martingale milestone drops non-lattice, as in Appendix A.
• Minima and limits. $M_n$ and $M_n^{\rm kill}$ are extended reals, $+\infty$ on an empty generation, so extinction lies in $\{M_n\ge\frac32\ln n+x\}$. $D_n$ is a real sum over generation $n$, absolutely summable almost surely, and $D_\infty$ is its pointwise limit. The expectation in the goal is a lower integral of $e^{-C^*e^xD_\infty}\in(0,1]$.
• Constants. $C^*$ is chosen before $x$. In Proposition 4.1, $C_1$ and $c_0$ are hypotheses tied to Proposition 1.2 and (2.13), not re-chosen. Corollaries 3.2 and 3.5 assert existence of their constants without Proposition 3.1 and Corollary 3.4.
• Not trivial. A formalization with a real-valued $M_n$ equal to $0$ on extinction, a $D_\infty$ never shown to be the limit, or a $C^*$ depending on $x$ would not be this theorem. The definitions above rule out each of these.

Out of scope: the spine-measure lemmas (Lemmas 2.3, 3.3, 3.8–3.10, 4.3), Propositions 2.1–2.2 cited from Lyons, and Appendices B–C. Contributions are welcome on all milestones. The many-to-one lemma and the renewal statement are independent of the rest and are natural first targets.

Selected references

• E. Aïdékon, Convergence in law of the minimum of a branching random walk, Ann. Probab. 41(3A) (2013) 1362–1426. arXiv:1101.1810, doi:10.1214/12-AOP750
• J. D. Biggins, A. E. Kyprianou, Measure change in multitype branching, Adv. Appl. Probab. 36 (2004) 544–581. Reference [7] of Aïdékon (2013), arXiv:1101.1810, p. 68
• M. Bramson, Convergence of solutions of the Kolmogorov equation to travelling waves, Mem. Amer. Math. Soc. 44, no. 285 (1983). doi:10.1090/memo/0285
• S. P. Lalley, T. Sellke, A conditional limit theorem for the frontier of a branching Brownian motion, Ann. Probab. 15 (1987) 1052–1061. Reference [21] of Aïdékon (2013), arXiv:1101.1810, p. 69
• Y. Hu, Z. Shi, Minimal position and critical martingale convergence in branching random walks, and directed polymers on disordered trees, Ann. Probab. 37 (2009) 742–789. arXiv:math/0702799
• L. Addario-Berry, B. Reed, Minima in branching random walks, Ann. Probab. 37 (2009) 1044–1079. Reference [1] of Aïdékon (2013), arXiv:1101.1810, p. 68
• R. Lyons, A simple path to Biggins' martingale convergence for branching random walk, in Classical and Modern Branching Processes, IMA Vol. Math. Appl. 84 (1997) 217–221. Reference [22] of Aïdékon (2013), arXiv:1101.1810, p. 69

Why the G/G/1 queue

The single-server queue with general interarrival times and general service times, written G/G/1 in Kendall's notation, is the model left when every distributional assumption is removed from the classical single-server queue. Customers arrive one at a time, wait in line in first-come, first-served order, and are served one at a time. Almost nothing about it can be computed in closed form. What survives is a recursion for the waiting times of successive customers and the integral equation of its steady state, due to Lindley (Lindley, 1952). Every exact and approximate treatment of the G/G/1 waiting time, including the bounds of the next chapter of the book, starts from that equation.

This mission is the eighth of a series formalizing Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651). It covers Chapter 6, "General Models and Theoretical Topics". The chapter also treats the G/E_k/1 characteristic equation (§6.1), the M/D/c queue (§6.3) and maximum-likelihood estimation for M/M/1 (§6.7), which appear here as further milestones.

Timeline. Lindley (1952) derived the recursion and the integral equation and showed that a limiting waiting-time distribution exists when the mean service time is smaller than the mean interarrival time. Loynes (1962) gave the stationary solution as a supremum over the past of a random walk, for stationary rather than independent inputs. Clarke (1957) derived the maximum-likelihood estimators for M/M/1, and Crommelin (1932) the M/D/c generating function. Chaudhry, Harris and Marchal (1990) located the roots of the G/E_k/1 characteristic equation.

Setting

The interarrival times $T^{(n)}$ are independent with common distribution $A$, the service times $S^{(n)}$ are independent with common distribution $B$, and the two sequences are independent. Both $A$ and $B$ are lifetime laws: probability distributions on $[0,\infty)$. The means are $\mathrm E[T]=1/\lambda$ and $\mathrm E[S]=1/\mu$, and the traffic intensity is $\rho=\lambda/\mu=\mathrm E[S]/\mathrm E[T]$.

The line delay $W_q^{(n)}$ of the $n$th customer satisfies Lindley's recursion

$$W_q^{(n+1)}=\max\bigl(0,\;W_q^{(n)}+S^{(n)}-T^{(n)}\bigr).$$

Write $U$ for the distribution of $S-T$ with $S\sim B$ and $T\sim A$ independent. Since $W_q^{(n)}$ is independent of $(S^{(n)},T^{(n)})$, one step of the recursion sends the distribution $\nu$ of $W_q^{(n)}$ to the distribution of $\max(0,W+U)$ with $W\sim\nu$ independent of $U$. A stationary delay distribution is a probability distribution $\nu$ that this step maps to itself; its CDF is $W_q(t)=\nu((-\infty,t])$.

Formalization targets

Goal: Lindley's equation (6.8)

If $\mathrm E[T]$ and $\mathrm E[S]$ are finite and $\rho<1$, then a stationary delay distribution exists, and the CDF of every stationary delay distribution satisfies

$$W_q(t)=\begin{cases}\displaystyle\int_{-\infty}^{t}W_q(t-x)\,dU(x) & (0\le t<\infty),\\ 0 & (t<0),\end{cases} \qquad U(x)=\int_{\max(0,x)}^{\infty}B(y)\,dA(y-x).$$

The goal consists of the existence statement and the equation together. The equation alone is close to unfolding one step of the recursion. Existence is what ties it to a queue in steady state.

Milestones

• (6.9), the CDF of $U=S-T$ as a convolution of $B$ and $A$.
• The one-step convolution (p.285): $W_q^{(n+1)}(t)=\int_{-\infty}^{t}W_q^{(n)}(t-x)\,dU(x)$ for $t\ge0$.
• (6.10)–(6.12), the Wiener–Hopf form: $W_q^-(t)+W_q(t)=\int_{-\infty}^t W_q(t-x)\,dU(x)$ for all $t$, and $\bar W_q(s)=\bar W_q^-(s)/(A^*(-s)B^*(s)-1)$ for two-sided Laplace transforms.
• The G/E_k/1 root result (p.278): the characteristic equation $z^k=A^*[k\mu(1-z)]$ has exactly one root in $(0,1)$, one in $(-1,0)$ exactly when $k$ is even, and, when $A^*=[A_1^*]^k$, exactly $k$ distinct roots in the open unit disk.
• (6.18)–(6.20), the M/D/c generating function and $p_0$ in terms of the roots of $z^c=e^{-\lambda(1-z)}$.
• (6.33), the maximum-likelihood estimators $\hat\lambda=n_a/t$, $\hat\mu=n_c/t_b$ for M/M/1.

Significance

Lindley's equation characterizes the stationary G/G/1 waiting time without any distributional assumption. The M/M/1, M/G/1 and G/M/1 waiting-time distributions of earlier chapters are its special cases. The transform relation (6.12) reduces the G/G/1 delay to a factorization problem for $A^*(-s)B^*(s)-1$. The recursion and the equation are the starting point of Kingman's bound, of heavy-traffic approximations and of simulation of single-server systems.

All of these results are classical and proved. As far as a search of the platform shows, none of them is formalized. The platform's forward-coupling mission proves convergence to a stationary workload of a continuous-time queue that it assumes to exist. It proves neither the existence of a stationary law of Lindley's discrete recursion nor Lindley's equation. The mission therefore produces a machine-checked account of the G/G/1 recursion on distributions, a Loynes-type existence theorem for it, and the Wiener–Hopf transform identity. Its definitions (lifetime laws, the law of $S-T$, the law map of the recursion, two-sided transforms) are reusable for Kingman's bound in the next mission of the series.

Difficulty

The obvious route to existence is to iterate the recursion from $W_q^{(0)}=0$ and take a limit. The distributions of $W_q^{(n)}$ from zero increase stochastically, but a limit of CDFs need not be a probability distribution: mass can escape to infinity, and it does when $\rho>1$. Ruling this out under $\rho<1$ is the whole content of the existence half. It is a statement about the entire past of the input sequences, not about one step of the recursion, and the book asserts it without argument ("In the steady state ($\rho<1$) …", p.285).

The transform identity (6.12) needs the right strip of convergence, which the book does not state. $A^*(-s)$ is finite only where the interarrival time has an exponential moment.

Formalization scope

Distributions are Mathlib measures on $\mathbb R$. $A$ and $B$ are probability measures with no mass on $(-\infty,0)$, with integrable identity where means are used. $\rho<1$ is stated as $\mathrm E[S]/\mathrm E[T]<1$ with $\mathrm E[T]>0$. Independence is encoded by product measures: $U$ is the image of $B\otimes A$ under $(s,t)\mapsto s-t$, and one step of the recursion is the image of $\nu\otimes U$ under $(w,u)\mapsto\max(0,w+u)$. Stieltjes integrals over $(-\infty,t]$ are Lebesgue integrals over the closed half-line, so the atom $W_q(0)=q_0$ is counted. Transforms take complex arguments.

The closed forms carried by the statements are the following.

• (6.8), in both of the book's forms, $\int_{-\infty}^t W_q(t-x)\,dU(x)$ and $-\int_0^\infty W_q(y)\,dU(t-y)$.
• (6.9) as an integral against the law of $T+x$.
• $U^*(s)=A^*(-s)B^*(s)$ and (6.12), for $0<\operatorname{Re}s$ with $\int e^{(\operatorname{Re}s)x}\,dA(x)<\infty$. The division is stated only where $A^*(-s)B^*(s)\ne1$.
• (6.18) and (6.19) with the denominator $1-z^ce^{\lambda(1-z)}$ cleared on $|z|\le1$, and (6.20) for $c\ge2$. The roots $z_1,\dots,z_{c-1}$ are hypotheses: distinct, $\ne1$, and exhausting the roots in the closed disk.
• (6.33) as the unique maximizer of $-\lambda t-\mu t_b+n_a\ln\lambda+n_c\ln\mu$ over $\lambda,\mu>0$.

A stationary delay distribution is a fixed point of the law map of the recursion, not an arbitrary CDF assumed to satisfy (6.8). A statement of (6.8) for "any CDF with $W_q=W_q*U$ on $[0,\infty)$" would assume its own conclusion, and is excluded. The statement for M/D/c includes existence of a steady state under $\lambda<c$ as well as the formula for every steady state.

Not formalized: §6.1.1–6.1.2 (G/PH_k/1, quasi-birth–death processes), §6.4 (semi-Markov processes, whose limit theorems the book quotes without hypotheses), §6.5 (random-order and last-come service, series representations), §6.6 (design and control), and the rest of §6.7.

Contributions are welcome on the random-walk representation of the recursion, on the existence theorem under $\rho<1$, and on the transform identities. The first two are reusable for any single-server or storage model driven by a reflected random walk.

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
• D. V. Lindley, "The theory of queues with a single server", Mathematical Proceedings of the Cambridge Philosophical Society 48(2), 1952. https://doi.org/10.1017/S0305004100027638
• R. M. Loynes, "The stability of a queue with non-independent inter-arrival and service times", Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 1962. https://doi.org/10.1017/S0305004100036094
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.
• A. B. Clarke, "Maximum likelihood estimates in a simple queue", Annals of Mathematical Statistics 28(4), 1957. https://doi.org/10.1214/aoms/1177706796
• M. L. Chaudhry, C. M. Harris, W. G. Marchal, "Robustness of rootfinding in single-server queueing models", ORSA Journal on Computing 2(3), 1990. https://doi.org/10.1287/ijoc.2.3.273

Motivation

Most queueing models with a closed-form answer assume Poisson arrivals. In practice the times between arrivals are often far from exponential: scheduled appointments, batch releases from an upstream process, or arrivals timed by a machine cycle. The G/M/1 queue keeps the service side exponential and makes no assumption about the arrival stream beyond independent, identically distributed interarrival times. It is the standard counterpart of the M/G/1 queue, and its solution is the one used in teaching and in practice whenever the input is not Poisson (Gross, Shortle, Thompson & Harris, Fundamentals of Queueing Theory, 4th ed., Wiley 2008, §5.3.1, DOI 10.1002/9781118625651).

The answer has an unusually clean form. The number of customers that an arriving customer finds in the system is geometric, exactly as in the M/M/1 queue, with the traffic intensity $\rho$ replaced by a number $r_0$ that depends on the whole interarrival distribution through a single scalar equation. This mission is the seventh of a series formalizing the book chapter by chapter; it covers the G/M/1 half of §5.3 (printed pp.259–263).

Setting

Customers arrive at a single server. The interarrival times are independent with common law $A$, a probability distribution on $[0,\infty)$ with CDF $A(t)$ and finite mean $E[T] = 1/\lambda$, $\lambda > 0$. Service times are independent exponential random variables with rate $\mu > 0$, and the discipline is first come, first served.

Let $X_n$ be the number of customers in the system just before the $n$th arrival. Between two arrivals the server completes a Poisson number of services (truncated by the number present), so $\{X_n\}$ is a Markov chain on $\{0,1,2,\dots\}$. Its transition probabilities are built from

$$b_k = \int_0^\infty \frac{e^{-\mu t}(\mu t)^k}{k!}\,dA(t) \qquad (k \ge 0),$$

the probability of exactly $k$ completions during one interarrival time (Eq. (5.50)): $p_{i0} = 1 - \sum_{k=0}^{i} b_k$, $p_{ij} = b_{i+1-j}$ for $1 \le j \le i+1$, and $p_{ij} = 0$ otherwise (Eq. (5.51)). A stationary arrival-point distribution is a probability vector $q = \{q_n\}$ with $qP = q$ and $qe = 1$ (Eq. (5.52)); $q_n$ is the long-run probability that an arrival finds $n$ customers present.

The characteristic equation of the chain is

$$z = \beta(z), \qquad \beta(z) = \sum_{n \ge 0} b_n z^n ,$$

where $\beta$ is the probability generating function of $\{b_n\}$ (Eq. (5.55)). Equivalently $z = A^*[\mu(1-z)]$ (Eq. (5.56)), where $A^*(s) = \int_0^\infty e^{-sx}\,dA(x)$ is the Laplace–Stieltjes transform of the interarrival law. The traffic intensity is $\rho = \lambda/\mu$.

Formalization targets

Goal: Eq. (5.60), the geometric arrival-point law

If $\rho = \lambda/\mu < 1$, there is a number $r_0$ with $0 < r_0 < 1$ and $r_0 = \beta(r_0)$, it is the only complex root of $z = \beta(z)$ in the open unit disk, and

$$q_n = (1 - r_0)\, r_0^{\,n} \qquad (n \ge 0)$$

is a stationary arrival-point distribution and the only one. The root is part of the conclusion, not an assumption.

Milestones

1. Eqs. (5.51)–(5.53): for a probability vector $q$, $qP = q$ is equivalent to $q_i = \sum_{k\ge0} q_{i+k-1}b_k$ ($i \ge 1$) and $q_0 = \sum_{j\ge0} q_j\bigl(1 - \sum_{k=0}^{j} b_k\bigr)$.
2. p.261: $0 < b_0 < 1$, $b_n > 0$ for all $n$, $\beta(1) = 1$, and $\beta'(1) = \sum_n n b_n = \mu/\lambda$.
3. Eq. (5.56): $\beta(z) = A^*[\mu(1-z)]$ for $|z| \le 1$.
4. Eq. (5.58), Figure 5.2: $z = \beta(z)$ has at most one root in $(0,1)$, and one exists if and only if $\lambda/\mu < 1$.
5. p.262: when $\lambda/\mu < 1$, $z = \beta(z)$ has exactly one root with $|z| < 1$.
6. Eq. (5.59): successive substitution $z^{(k+1)} = \beta(z^{(k)})$ from any $0 < z^{(0)} < 1$ converges to $r_0$.
7. Eq. (5.61): $L^{(A)} = r_0/(1-r_0)$ and $L_q^{(A)} = r_0^2/(1-r_0)$.
8. Eq. (5.62): $W_q(t) = 1 - r_0 e^{-\mu(1-r_0)t}$ and $W(t) = 1 - e^{-\mu(1-r_0)t}$ for $t \ge 0$.
9. Eq. (5.63): $W_q = r_0/(\mu(1-r_0))$ and $W = 1/(\mu(1-r_0))$.

Significance

The result. Equation (5.60) reduces the analysis of a queue with arbitrary renewal input to one scalar root. Every arrival-point performance measure of the M/M/1 queue then carries over with $\rho$ replaced by $r_0$: the mean number found by an arrival, the mean queue found by an arrival, and the full distributions of line delay and system time seen by arrivals (Eqs. (5.61)–(5.63)). The same root drives the multiserver G/M/c analysis later in §5.3 and the relation between arrival-point and time-average probabilities in §6.3. The result also illustrates a point the book stresses: $q_n$ is the distribution seen by arrivals, and it equals the time-average distribution $p_n$ only when the input is Poisson.

Formalizing it. The mathematics is classical (the embedded-chain method goes back to Kendall, 1953) and fully proved in the textbook literature; nothing here is open. To our knowledge none of it has a machine-checked proof: the platform had no G/M/1, embedded-chain, or Rouché-type statement when this mission was drafted. The work is to formalize the known argument, which touches analytic facts about power series with nonnegative coefficients, a mixture-of-Poisson computation, a counting of roots in the unit disk, and the uniqueness of the stationary law of an irreducible countable chain.

Difficulty

Locating a real root in $(0,1)$ is a one-variable question. The hard step is excluding every other complex root inside the unit disk: a real-variable argument says nothing about complex roots, and the book's route relies on Rouché's theorem, which Mathlib does not have. A second point is uniqueness of the stationary vector: showing that the geometric vector solves $qP = q$ does not show that no other probability vector does, and the goal asserts both. Computing $\sum_n n b_n = \mu/\lambda$ requires interchanging a sum with the integral against $A$, which is where the finite mean of the interarrival law enters.

Formalization scope

The interarrival law is a measure A : Measure ℝ with IsProbabilityMeasure A, A (Set.Iio 0) = 0, integrable identity, and ∫ x ∂A = 1/λ (the structure IsInterarrivalLaw). Every theorem also assumes $\lambda > 0$ and $\mu > 0$. The integrals defining $b_k$ and $A^*$ are over $[0,\infty)$, closed at $0$. The generating function $\beta$ takes complex arguments; real roots are written with the real-to-complex coercion. A stationary vector is a function q : ℕ → ℝ with $q_n \ge 0$, HasSum q 1, and HasSum (fun i => q i * p i j) (q j) for every $j$.

The explicit closed forms the statements carry are: the transition matrix (5.51); the equations (5.53); $\beta(z) = A^*[\mu(1-z)]$ (5.56); $\beta'(1) = \mu/\lambda$; $q_n = (1-r_0)r_0^n$ (5.60); $r_0/(1-r_0)$ and $r_0^2/(1-r_0)$ (5.61); $1 - r_0e^{-\mu(1-r_0)t}$ and $1 - e^{-\mu(1-r_0)t}$ (5.62); $r_0/(\mu(1-r_0))$ and $1/(\mu(1-r_0))$ (5.63). The waiting-time CDFs are defined as in §2.2.5 of the book: $W_q(t) = q_0 + \sum_{n\ge1} q_n \Pr\{n \text{ completions in} \le t\}$ with the Erlang type-$n$ CDF, and $W(t)$ likewise with $n+1$ completions. The means in (5.63) are $\int_0^\infty [1 - W_q(t)]\,dt$ and $\int_0^\infty [1 - W(t)]\,dt$.

A trivializing formalization would take "$r_0 \in (0,1)$ solves $z = \beta(z)$" as a hypothesis of the goal, which turns (5.60) into a geometric-series check; here existence, location and uniqueness of the root, and uniqueness of the stationary vector, are all conclusions.

Out of scope for this mission: the M/G/c and M/G/∞ results of §5.2 and the multiserver G/M/c analysis of §5.3.2. Reusable pieces include a Rouché-type or fixed-point counting lemma for power series with nonnegative coefficients summing to one, and the uniqueness of stationary laws for irreducible chains on $\mathbb N$. Contributions of either kind are welcome.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.3.1, pp.259–263. https://doi.org/10.1002/9781118625651
• D. G. Kendall, "Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain", Annals of Mathematical Statistics 24(3), 1953, 338–354. https://doi.org/10.1214/aoms/1177728975

Motivation

The M/G/1 queue is the single-server queue with Poisson arrivals and an arbitrary service-time distribution. It is the first queueing model beyond the birth–death family in which exact formulas survive. It is also the model a practitioner reaches for when service times are measured and visibly not exponential: repair times, transmission times of variable-length packets, machining times. Its central result is the Pollaczek–Khintchine formula, first obtained by Pollaczek (1930) and Khintchine (1932). It expresses the stationary queue in terms of the service distribution, and it shows that the mean wait grows linearly in the squared coefficient of variation of service. That makes variability, and not only load, a measurable driver of congestion.

The textbook treatment followed here is Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory, 4th ed. (Wiley 2008), §5.1. It derives the result through Kendall's (1953) imbedded Markov chain of system sizes at departure epochs. It then obtains the transforms of the waiting times and the busy-period functional equation of Takács (1962).

Setting

Customers arrive in a Poisson stream of rate $\lambda > 0$. Service times $S$ are independent with distribution $B$, a probability distribution on $[0,\infty)$ with mean $\mathrm E[S]$, and the discipline is first-come first-served. The traffic intensity is $\rho = \lambda\,\mathrm E[S]$.

Let $X_n$ be the number of customers the $n$th departing customer leaves behind. The number of arrivals during one service time equals $i$ with probability

$$k_i = \int_0^\infty \frac{e^{-\lambda t}(\lambda t)^i}{i!}\,dB(t),$$

and $(X_n)$ is a Markov chain on $\{0,1,2,\dots\}$ whose transition matrix $P$ has first row $(k_0,k_1,k_2,\dots)$ and, for $i \ge 1$, entries $p_{ij} = k_{j-i+1}$ for $j \ge i-1$ and $0$ otherwise. A stationary distribution is a probability vector $\pi$ with $\pi P = \pi$. Its generating function is $\Pi(z) = \sum_i \pi_i z^i$, and that of the arrivals per service is $K(z) = \sum_i k_i z^i$, for complex $|z| \le 1$. The Laplace–Stieltjes transform of a distribution $F$ on $[0,\infty)$ is $F^*(s) = \int_0^\infty e^{-st}\,dF(t)$. In the Lean development these are arrivalProb, transitionMatrix, IsStationaryDist, pgf, utilization and lst in the namespace QueueingFundamentals.MG1.

Formalization targets

Goal: the Pollaczek–Khintchine transform formula (5.15)–(5.16)

If $\mathrm E[S] < \infty$ and $\rho < 1$, the chain has a stationary distribution, and every stationary distribution satisfies $\pi_0 = 1-\rho$ and

$$\Pi(z) = \frac{(1-\rho)(1-z)K(z)}{K(z)-z}, \qquad |z| \le 1,\ z \ne 1,$$

with $K(z) \ne z$ at each such $z$. It leaves the service distribution completely general.

Milestones

1. The stationary equations (5.12): $\pi_i = \pi_0 k_i + \sum_{j=1}^{i+1}\pi_j k_{i-j+1}$.
2. The transform (5.14), $\Pi(z) = \pi_0(1-z)K(z)/(K(z)-z)$, with $\pi_0$ free and no condition on $\rho$.
3. Ergodicity (§5.1.4): a unique stationary distribution exists if and only if $\rho < 1$.
4. The departure-point mean (5.7): $L^{(D)} = \rho + (\rho^2+\lambda^2\sigma_B^2)/(2(1-\rho))$.
5. $K(z) = B^*[\lambda(1-z)]$ (5.32).
6. The system-wait transform (5.29), (5.33): $\Pi(z) = W^*[\lambda(1-z)]$ and $W^*(s) = (1-\rho)sB^*(s)/(s-\lambda[1-B^*(s)])$.
7. The line-wait transform (5.34): $W_q^*(s) = (1-\rho)s/(s-\lambda[1-B^*(s)])$.
8. The busy-period equation (5.37): $G^*(s) = B^*[s+\lambda-\lambda G^*(s)]$.
9. The mean busy period: $\mathrm E[X] = 1/(\mu-\lambda)$ with $\mu = 1/\mathrm E[S]$.

Significance

The transform formula determines the whole stationary departure-point distribution from the service distribution. Its derivatives at $z = 1$ give every moment of the system size, including the mean-value formula (5.7). Combined with the transform identity (5.32), it gives the waiting-time transforms (5.33)–(5.34). Those in turn give the classical geometric-series representation of the line-wait distribution through the residual service time. The busy-period equation is the starting point for busy-period moments and for the M/G/1 analysis of priority and vacation models later in the book.

All results here are classical and proved in the literature. As far as a search of the platform shows (2026-09-28), none is machine-checked: there is no M/G/1 queue, imbedded departure-point chain, Laplace–Stieltjes transform of a service distribution, or busy-period equation on Prove2Me. Mathlib has Poisson distributions and measure convolution but no generating-function theory for countable Markov chains, no Laplace–Stieltjes transform, and no identity theorem in the form these statements need. The mission produces a checked statement of the Pollaczek–Khintchine formulas that later queueing developments (vacations, priorities, M/G/1-type chains) can build on.

Difficulty

Turning the stationary equations into (5.14) is formal power-series algebra. The difficulties lie elsewhere. First, the formula must hold for complex $z$ on the closed disk, which needs the non-vanishing of $K(z)-z$ away from $z = 1$. That fact fails for $\rho > 1$, where $K$ has a fixed point inside the disk. Second, (5.15) evaluates $\pi_0$ from $\Pi(1) = 1$ by a limit at the point where the formula is $0/0$, and this uses $K'(1) = \rho$, an interchange of sum and integral. Third, the existence half of the goal requires positive recurrence of a chain with unbounded jumps. The book obtains it from Foster's criterion, which is not in Mathlib. Fourth, the waiting-time and busy-period transforms are stated for all real $s > 0$, while the generating-function route reaches only $s = \lambda(1-z) \in (0, 2\lambda]$. Extending the identity requires either analyticity arguments or a direct derivation. A formal proof of (5.14) alone does not touch any of these.

Formalization scope

The service distribution is a Measure ℝ with IsProbabilityMeasure B and B (Set.Iio 0) = 0; no density is assumed. The arrival rate is lam : ℝ with 0 < lam. Stationarity is IsStationaryDist P π: nonnegative entries, HasSum π 1, and HasSum (fun i => π i * P i j) (π j) for every j. That is global balance on ℕ, as the book writes it. Generating functions take a complex argument with ‖z‖ ≤ 1; transforms take a complex argument, and the waiting-time and busy-period statements use real s. The mean and variance of B are Bochner integrals, and every statement that uses them assumes Integrable. The mean busy period assumes 0 < E[S], so that $\mu = 1/\mathrm E[S]$ is the book's service rate.

Closed forms carried by the statements: $\pi_0 = 1-\rho$ (5.15); $(1-\rho)(1-z)K(z)/(K(z)-z)$ (5.16); $\pi_0(1-z)K(z)/(K(z)-z)$ (5.14); $\rho + (\rho^2+\lambda^2\sigma_B^2)/(2(1-\rho))$ (5.7); $B^*[\lambda(1-z)]$ (5.32); $(1-\rho)sB^*(s)/(s-\lambda[1-B^*(s)])$ (5.33); $(1-\rho)s/(s-\lambda[1-B^*(s)])$ (5.34); $B^*[s+\lambda-\lambda G^*(s)]$ (5.37); $1/(\mu-\lambda)$ for the mean busy period.

The waiting-time distribution $W$ enters through the book's FCFS relation $\pi_n = \frac1{n!}\int(\lambda t)^n e^{-\lambda t}\,dW(t)$, and $W_q$ through $W = W_q * B$; both are hypotheses, as in the book. The busy-period distribution $G$ enters through the equation (5.36) in CDF form, with $n$-fold convolutions built from Mathlib's Measure.conv.

The goal is not the algebraic consequence of (5.12) for an arbitrary sequence: $\pi$ must be a probability vector, $\pi_0$ is determined as $1-\rho$, and the existence of a stationary distribution is part of the conclusion, so the statement cannot hold vacuously. The departure-point/time-average equality (§5.1.3, via PASTA) is not formalized.

Useful infrastructure, reusable beyond this mission: generating functions of stationary distributions on ℕ, Poisson mixtures, Laplace–Stieltjes transforms of measures on $[0,\infty)$, and a Foster-type drift criterion for countable chains. Contributions proving any milestone, or those tools, are welcome.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.1. https://doi.org/10.1002/9781118625651
• D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Annals of Mathematical Statistics 24 (1953) 338–354. https://doi.org/10.1214/aoms/1177728975
• 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
• L. Takács, Introduction to the Theory of Queues, Oxford University Press, 1962.
• F. Pollaczek, Über eine Aufgabe der Wahrscheinlichkeitstheorie, Mathematische Zeitschrift 32 (1930) 64–100. https://doi.org/10.1007/BF01194620

Motivation

Networks of queues model systems in which a job visits several service stations in turn: jobs in a computer system alternating between CPU and disks, machines cycling between operation and repair, parts routed through a job shop. In a closed network no job enters or leaves; a fixed population of $N$ customers circulates among $k$ nodes. Closed networks are the standard model of multiprogrammed computer systems and of machine-repair and finite-source systems, and they are the setting of chapter 4 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, doi:10.1002/9781118625651).

The chapter's results form a short line of computational ideas:

• Jackson (1957, 1963) showed that open networks of exponential servers with Markovian routing have a product-form steady state; Gordon and Newell (1967) gave the closed-network version, (4.15)–(4.18) of the book.
• Buzen (1973) gave a convolution recursion for the normalizing constant $G(N)$ and for marginal distributions, (4.19)–(4.22).
• Reiser and Lavenberg (1980) introduced mean-value analysis (MVA), which computes mean queue lengths, waiting times and throughputs population by population without ever forming $G(N)$, (4.23)–(4.25); the book presents it following Bruell and Balbo (1980).
• The book closes the section with a recursion for the full marginal distributions, (4.26), which it proves from the product form (pp.207–209).

This mission formalizes that line, ending at (4.26).

Setting

A closed Jackson network has nodes $i = 1, \dots, k$, each with a single server whose service times are exponential with rate $\mu_i > 0$. A customer finishing service at node $i$ moves to node $j$ with probability $r_{ij}$; the routing matrix $R = (r_{ij})$ has nonnegative entries and rows summing to one, and it is irreducible: every node can be reached from every other. The state is $\bar n = (n_1, \dots, n_k)$, the number of customers at each node, with $n_1 + \cdots + n_k = N$; this state space is finite.

The steady-state distribution $p_{\bar n}$ is the probability vector on the state space that solves the flow-balance equations (4.14),

$$\sum_{j=1}^{k}\sum_{\substack{i=1\\ i\ne j}}^{k} \mu_i r_{ij}\, p_{\bar n;i^+j^-} = \sum_{i=1}^{k}\mu_i(1-r_{ii})\,p_{\bar n},$$

where $\bar n;i^+j^-$ has one more customer at $i$ and one fewer at $j$, and terms with a negative subscript or with $\mu_i$ at an empty node vanish. The traffic equations (4.16) are $\mu_i\rho_i = \sum_j \mu_j r_{ji}\rho_j$; they determine $\rho = (\rho_1, \dots, \rho_k)$ up to a positive factor. The normalizing constant is

$$G(N) = \sum_{n_1+\cdots+n_k=N}\rho_1^{n_1}\cdots\rho_k^{n_k},$$

and more generally, with $f_i(n) = \rho_i^{\,n}/a_i(n)$ for $c_i$-server nodes ((4.13)), $G(N) = \sum \prod_i f_i(n_i)$ and Buzen's function $g_m(n) = \sum_{n_1+\cdots+n_m=n}\prod_{i\le m} f_i(n_i)$.

For each population $N$ write $p_i(n, N) = \Pr\{N_i = n\}$ for the marginal distribution at node $i$, $\bar P_i(n; N) = \Pr\{N_i \ge n\}$, $L_i(N)$ for the mean number at node $i$, and

$$\lambda_i(N) = \Pr\{\text{server busy at node } i\}\cdot\mu_i$$

for the throughput of node $i$.

Formalization targets

Goal: the marginal recursion (4.26)

For every node $i$,

$$p_i(0,0) = 1, \qquad p_i(n, N) = \frac{\lambda_i(N)}{\mu_i}\,p_i(n-1, N-1) \quad (n, N \ge 1).$$

It involves only the steady-state distributions and quantities computed from them; it holds for every irreducible routing matrix and every choice of rates.

Milestones

1. Product form (4.14)–(4.16). For any positive solution $\rho$ of (4.16), a probability distribution solves (4.14) if and only if $p_{\bar n} = G(N)^{-1}\rho_1^{n_1}\cdots\rho_k^{n_k}$.
2. Buzen's algorithm (4.19)–(4.21). $G(N) = g_k(N)$, $g_m(n) = \sum_{i=0}^{n} f_m(i)\,g_{m-1}(n-i)$, $g_1 = f_1$, $g_m(0) = 1$.
3. Marginal at the last node (4.22). $p_k(n) = f_k(n)\,g_{k-1}(N-n)/G(N)$ for $0 \le n \le N$.
4. Complementary marginal (p.208). $\bar P_i(n_i; N) = \rho_i^{\,n_i}G(N-n_i)/G(N)$.
5. Mean-value analysis (4.23)–(4.25). $L_i(0) = 0$; $L_i(N) = \lambda_i(N)W_i(N)$ with $W_i(N) = (1 + L_i(N-1))/\mu_i$; and for $v$ solving $v_i = \sum_j v_j r_{ji}$ with $v_l = 1$, $\lambda_l(N) = N/\sum_i v_iW_i(N)$ and $\lambda_i(N) = \lambda_l(N)v_i$.

Significance

The product form reduces a $\binom{N+k-1}{N}$-state Markov chain to the constants $G(0), \dots, G(N)$, and Buzen's recursion computes them in $O(kN^2)$ operations. Mean-value analysis goes further and avoids $G(N)$, whose magnitude can overflow or underflow for large populations; it is the method used in capacity planning of computer systems. The recursion (4.26) extends MVA from means to full marginal distributions, so a single pass over $N$ yields every nodal distribution.

All of these results are classical and proved in the literature; the book proves (4.26) itself. What the mission adds is a machine-checked development of them from the global balance equations: the product form with its uniqueness, the convolution identities, the marginal formulas, and the correctness of the MVA iteration as stated by the book, all over one shared definition layer. A search of the platform on 2026-09-28 found no formal statement of Buzen's algorithm or of MVA. The platform has Kelly's closed migration process theorem (KellyStochasticNetworks.closed_migration_equilibrium), which shows that the unnormalized product form satisfies the equilibrium equations under Kelly's conventions; the normalization, uniqueness and everything downstream of the product form are new here.

Difficulty

The combinatorial identities (Buzen's recursion, the tail marginal) are reindexings of finite sums over compositions of $N$; in Lean the work is in bijections between the state spaces $\{n_1+\cdots+n_k = N\}$ for different $k$ and $N$. The substantive step is uniqueness in the product-form theorem: the global balance equations have a one-dimensional solution space only because the chain on the $N$-customer states is irreducible on the population level, which is a property of the network chain and not of the routing matrix alone. The goal and MVA also need a positive solution of the traffic equations, which is not among the hypotheses and has to come from irreducibility of $R$. The book's own intuitive derivation of MVA via the arrival theorem is not the route the statements require; they are stated in terms of the steady-state distributions alone.

Formalization scope

Nodes are Fin k (book node $i$ is index $i-1$); states are n : Fin k → ℕ with ∑ i, n i = N, collected in a Finset, and all sums are finite. A distribution is a real function on $\mathbb N^k$ that is nonnegative, vanishes off the $N$-customer states and sums to one there. The balance equations are (4.14) verbatim with the book's boundary convention (p.188), not detailed balance. All results except Buzen's algorithm and (4.22) are for single-server nodes, as in the book; (4.13)'s multiserver factor $a_i(n)$ enters only (4.19)–(4.22).

Closed forms instantiated in the statements: the product form $G(N)^{-1}\prod_i\rho_i^{n_i}$ ((4.15)); $G(N)$ as the explicit sum (4.18)/(4.19); $a_i(n)$ from (4.13); $g_m$ from (4.20); $p_k(n) = f_k(n)g_{k-1}(N-n)/G(N)$ ((4.22)); $\bar P_i(n;N) = \rho_i^nG(N-n)/G(N)$ (p.208); $W_i(N) = (1+L_i(N-1))/\mu_i$ ((4.23)); $\lambda_l(N) = N/\sum_i v_iW_i(N)$ (MVA step (iii)(b)).

Two trivializing formalizations are ruled out: $\lambda_i(N)$ in (4.26) and (4.24) is the throughput computed from the steady-state distribution, not a free constant (which would make (4.26) a definition); and $g_m$ is defined by the sum (4.20), so the recursion (4.21) is a theorem rather than rfl. The product-form statement is an equivalence, so it asserts both that the product form is a steady state and that it is the only one.

Needed infrastructure: bijections between compositions of $N$ into $k$ and $k-1$ parts, uniqueness of stationary distributions of irreducible finite continuous-time chains (stated directly via the balance equations), and existence of positive solutions of $v = vR$ for irreducible stochastic $R$. The last two are reusable beyond this mission. Contributions welcome: proofs of the milestones in any order, and helper lemmas on these three points.

Not formalized: open Jackson networks (4.11) and Burke's theorem (4.5)–(4.6), multiclass networks (§4.2.1), the multiserver recursion (4.27) and cyclic queues (§4.4).

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §4.3, pp.195–209. https://doi.org/10.1002/9781118625651
• J. R. Jackson, "Jobshop-like queueing systems", Management Science 10(1), 1963. https://doi.org/10.1287/mnsc.10.1.131
• W. J. Gordon, G. F. Newell, "Closed queuing systems with exponential servers", Operations Research 15(2), 1967. https://doi.org/10.1287/opre.15.2.254
• J. P. Buzen, "Computational algorithms for closed queueing networks with exponential servers", Communications of the ACM 16(9), 1973. https://doi.org/10.1145/362342.362345
• M. Reiser, S. S. Lavenberg, "Mean-value analysis of closed multichain queuing networks", Journal of the ACM 27(2), 1980. https://doi.org/10.1145/322186.322195
• S. C. Bruell, G. Balbo, Computational Algorithms for Closed Queueing Networks, North-Holland, 1980.

Motivation

In many service systems a customer who finds every server busy does not join a queue. A caller who hears a busy signal hangs up and redials later; a request rejected by a saturated server is resent after a timeout; an aircraft that cannot land circles and tries again. These retrial queues are the subject of a substantial literature in telephone traffic engineering, computer networks and call-centre design, surveyed in the monograph of Falin and Templeton (1997) and the bibliography of Artalejo (1999). Their analysis is harder than that of ordinary queues: the blocked customers form an orbit whose size is part of the state, so even the simplest model is a two-dimensional Markov chain, and explicit stationary distributions are rare.

This mission is the fourth of a series formalizing Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008). Its goal is the explicit stationary distribution of the single-server retrial queue, Eq. (3.57) of §3.5.1, one of the few retrial models solvable in closed form. Chapter 3 of the book treats Markovian queues that are not birth–death processes: bulk arrivals, bulk service, Erlang phases, priority disciplines and retrials. The milestones also collect three capstone formulas from the chapter's other sections: the bulk-input queue, the partial-batch bulk-service queue, and Cobham's formula for nonpreemptive priorities (Cobham, 1954).

Setting

In the $M/M/1$ retrial queue customers arrive according to a Poisson process with rate $\lambda$ and are served one at a time by a single server, with exponential service times of mean $1/\mu$. An arrival that finds the server busy enters the orbit and stays there for an exponential time with mean $1/\gamma$, after which it tries again; each customer in orbit retries independently. No customer leaves because of impatience. With $N_s(t) \in \{0,1\}$ the number in service and $N_o(t)$ the number in orbit, the pair is a continuous-time Markov chain on states $\{i, n\}$, $i \in \{0,1\}$, $n \in \{0,1,2,\dots\}$. Writing $p_{i,n}$ for the steady-state probability of $\{i,n\}$, the rate-balance equations are

$$\begin{aligned} (\lambda + n\gamma)p_{0,n} &= \mu p_{1,n}, && n \ge 0, && (3.47)\\ (\lambda+\mu)p_{1,n} &= \lambda p_{0,n} + (n+1)\gamma p_{0,n+1} + \lambda p_{1,n-1}, && n \ge 1, && (3.48)\\ (\lambda+\mu)p_{1,0} &= \lambda p_{0,0} + \gamma p_{0,1}. && && (3.49) \end{aligned}$$

Following the book's convention (§1.9, and the footnote on p.118), a steady-state solution is a nonnegative solution of these equations whose total mass $\sum_n (p_{0,n} + p_{1,n})$ equals $1$. The traffic intensity is $\rho = \lambda/\mu$, and the partial generating functions are $P_0(z) = \sum_n z^n p_{0,n}$ and $P_1(z) = \sum_n z^n p_{1,n}$.

The other models of the mission use the same convention. In the bulk-input queue $M^{[X]}/M/1$, batches arrive at rate $\lambda$ with batch-size probabilities $c_n = \Pr\{X = n\}$, $n \ge 1$, and batch-size generating function $C(z) = \sum_n c_n z^n$. In the partial-batch bulk-service queue $M/M^{[K]}/1$, single arrivals come at rate $\lambda$ and the server serves up to $K$ customers together in an exponential time of mean $1/\mu$. In the nonpreemptive priority queue there are $r$ classes with rates $\lambda_k$ and $\mu_k$, loads $\rho_k = \lambda_k/\mu_k$ and cumulative loads $\sigma_k = \rho_1 + \cdots + \rho_k$.

Formalization targets

Goal: the stationary distribution (3.57)

For $\lambda, \mu, \gamma > 0$ and $\rho < 1$, the numbers

$$p_{0,n} = (1-\rho)^{(\lambda/\gamma)+1}\frac{\rho^n}{n!\,\gamma^n}\prod_{i=0}^{n-1}(\lambda+i\gamma), \qquad p_{1,n} = (1-\rho)^{(\lambda/\gamma)+1}\frac{\rho^{n+1}}{n!\,\gamma^n}\prod_{i=1}^{n}(\lambda+i\gamma)$$

form a steady-state solution of (3.47)–(3.49), and every steady-state solution equals them.

Milestones on the retrial queue

The generating functions satisfy (3.50)–(3.52) on $(-1,1)$, including the separable equation

$$P_0'(z) = \frac{\lambda\rho}{\gamma(1-\rho z)}P_0(z),$$

their closed form is (3.55),

$$P_0(z) = (1-\rho z)\left(\frac{1-\rho}{1-\rho z}\right)^{(\lambda/\gamma)+1}, \qquad P_1(z) = \rho\left(\frac{1-\rho}{1-\rho z}\right)^{(\lambda/\gamma)+1},$$

and the mean orbit size is (3.58), $L_o = \frac{\rho^2}{1-\rho}\cdot\frac{\mu+\gamma}{\gamma}$.

Milestones from the rest of Chapter 3

The bulk-input generating function (3.3), $p_0 = 1 - \rho$ with $\rho = \lambda\mathrm E[X]/\mu$, and the mean (3.4); the unique root $r_0 \in (0,1)$ of $\mu r^{K+1} - (\lambda+\mu)r + \lambda = 0$ and the geometric law $p_n = (1-r_0)r_0^n$ (3.9); and Cobham's formula (3.41)/(3.43), the unique solution of the linear system (3.40).

Significance

The closed form (3.57) makes every performance measure of the $M/M/1$ retrial queue explicit. The server is busy a fraction $\rho$ of the time, exactly as without retrials. The mean orbit size (3.58) is the $M/M/1$ mean queue length multiplied by $(\mu+\gamma)/\gamma$, and the mean time in orbit (3.59) follows from Little's law. These formulas quantify the cost of retrials against an ordinary queue and are the reference case against which approximations for multi-server retrial systems are checked.

The results are classical and proved in the book, partly through exercises (Problems 3.39–3.41). None of them is formalized in any proof assistant, as far as the platform's catalogue shows: there is no retrial, bulk or priority queue on Prove2Me. The mission produces machine-checked statements and, once solved, proofs of the chapter's main closed forms. It also produces a small reusable layer: generating functions of probability sequences on the closed unit disc, and the "probability solution of the balance equations" pattern for chains with countable state spaces.

Difficulty

The derivation in the book is formal. It differentiates power series term by term, divides by $1 - z$, integrates $\ln P_0$, and fixes the constant by setting $z = 1$, without justifying any of these steps. A formal proof has to show that the series converge and are differentiable on $(-1,1)$, that the differential equation determines $P_0$ up to a constant, and that the values at $z = 1$ are the limits of the values inside the disc (Abel's theorem). The uniqueness half of the goal is the hardest part. The book never proves it; it follows from the ODE argument only once every step is shown to hold for an arbitrary probability solution. Verifying that (3.57) solves (3.47)–(3.49) is only the easy half. The same pattern recurs in the bulk-input queue, where $z = 1$ is a removable singularity of (3.3). In the bulk-service queue the root $r_0$ is only characterized as the unique root in $(0,1)$, so existence and uniqueness of the root are part of the claim.

Formalization scope

A steady-state solution is a pair p0 p1 : ℕ → ℝ (resp. one sequence p : ℕ → ℝ) that is pointwise nonnegative, has total mass $1$ as a HasSum, and solves the book's balance equations exactly as printed, global balance and not detailed balance. Every "the steady-state solution is X" is stated with both halves: X is a steady-state solution, and every steady-state solution equals X. Stating only that (3.57) solves (3.47)–(3.49), without normalization or uniqueness, would be a trivializing formalization. So would taking $r_0$ as a given root in (3.9), or taking the $W_q^{(i)}$ in (3.41) as numbers assumed to satisfy it. None of these is used. The closed forms instantiated are (3.52), (3.55), (3.57), (3.58), (3.3), (3.4), (3.9), (3.41) and (3.43), each written out in full, with the real power $(1-\rho)^{(\lambda/\gamma)+1}$ as Real.rpow.

The conventions are as follows. The retrial generating functions take real arguments, on $(-1,1)$ for the differential equations and on $[-1,1]$ for the closed form. The bulk-input generating function takes complex arguments with $|z| \le 1$, $z \ne 1$, because (3.3) is $0/0$ at $z = 1$. The condition $\rho < 1$ is a hypothesis of every retrial statement. For the bulk-service queue the book's unnamed condition is stated as $\lambda < K\mu$. For bulk input, $\mathrm E[X] < \infty$ is assumed throughout, and the mean (3.4) is asserted under the further condition $\mathrm E[X^2] < \infty$, which it requires. For Cobham's formula only the algebraic content is formalized; the mean-value argument that yields (3.40) and (3.42) is not.

Needed infrastructure: power series of summable nonnegative sequences on the closed unit disc (convergence, term-by-term differentiation, Abel continuity), the binomial series $(1 - x)^{-a} = \sum_n \frac{a(a+1)\cdots(a+n-1)}{n!}x^n$ for real $a$, and uniqueness of invariant probability vectors for irreducible chains. All of this is reusable beyond the mission. Proofs of any milestone, of the easy half of the goal, or of the needed series facts are welcome contributions.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §§3.1, 3.2.0.1, 3.4.2, 3.5.1. https://doi.org/10.1002/9781118625651
• G. I. Falin, J. G. C. Templeton, Retrial Queues, Chapman & Hall, 1997. https://doi.org/10.1007/978-1-4899-2977-8
• J. R. Artalejo, Accessible bibliography on retrial queues, Mathematical and Computer Modelling 30 (1999) 1–6. https://doi.org/10.1016/S0895-7177(99)00128-4
• A. Cobham, Priority assignment in waiting line problems, Journal of the Operations Research Society of America 2 (1954) 70–76. https://doi.org/10.1287/opre.2.1.70