Probability

Motivation

Thompson Sampling (TS) is the oldest heuristic for the stochastic multi-armed bandit problem: it was proposed by Thompson in 1933 (Biometrika 25) and is used in practice for online advertising and recommendation, where it often performs as well as or better than upper-confidence-bound methods (Chapelle and Li, NIPS 2011; Scott 2010). Until 2012 its theoretical guarantees for the frequentist regret were weak: earlier analyses gave only $o(T)$ regret in time $T$ (Granmo 2010; May, Korda, Lee and Leslie 2011).

Agrawal and Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem (arXiv:1111.1797v3, COLT 2012), gave the first logarithmic finite-time bound on the expected regret of TS. This mission formalizes their two-armed result, Theorem 1. A companion mission covers the $N$-armed bound, Theorem 2.

Timeline. Lai and Robbins (1985) proved that every consistent algorithm has regret at least $\big[\sum_i \Delta_i/D(\mu_i\|\mu^*)+o(1)\big]\ln T$. Auer, Cesa-Bianchi and Fischer (2002) gave UCB1 with an $O(\sum_i \ln T/\Delta_i)$ finite-time bound. Agrawal and Goyal (2012) proved $O(\ln T/\Delta+1/\Delta^3)$ for two-armed TS. Kaufmann, Korda and Munos (ALT 2012) and Agrawal and Goyal (AISTATS 2013) later proved asymptotically optimal bounds for Bernoulli TS.

Setting

There are two arms. Arm $i\in\{1,2\}$ has a fixed, unknown reward distribution $D_i$ supported in $[0,1]$, with mean $\mu_i$. Plays of an arm give i.i.d. rewards, independent of the other arm. Arm 1 is the unique optimal arm, $\mu_1>\mu_2$, and $\Delta=\mu_1-\mu_2$ is the gap.

Thompson Sampling for general stochastic bandits (Algorithm 2 of the paper) keeps, for each arm $i$, a success count $S_i$ and a failure count $F_i$, both starting at $0$. In each round $t=1,2,\dots$ it

1. samples, independently for each arm, $\theta_i(t)\sim\mathrm{Beta}(S_i+1,F_i+1)$;
2. plays $i(t)=\arg\max_i\theta_i(t)$ and observes a reward $\tilde r_t\sim D_{i(t)}$;
3. performs a Bernoulli trial with success probability $\tilde r_t$, with outcome $r_t\in\{0,1\}$;
4. increments $S_{i(t)}$ if $r_t=1$ and $F_{i(t)}$ otherwise.

$k_i(t)$ is the number of plays of arm $i$ before round $t$. The expected regret in time $T$ is

$$\mathbb E[\mathcal R(T)]=\mathbb E\Big[\sum_{t=1}^T(\mu_1-\mu_{i(t)})\Big],$$

the expectation being over the rewards and the algorithm's randomness.

The analysis uses the Beta cdf $F^{beta}_{\alpha,\beta}$, the binomial cdf $F^B_{n,p}$, and the random variable $X(j,s,y)$: the number of independent $\mathrm{Beta}(s+1,j-s+1)$ draws made before one exceeds $y$.

Formalization targets

Goal: Theorem 1 (p. 3)

There is an absolute constant $C>0$ such that for every two-armed instance with rewards in $[0,1]$ and $\mu_1>\mu_2$, and every $T\ge 2$,

$$\mathbb E[\mathcal R(T)]\le C\Big(\frac{\ln T}{\Delta}+\frac1{\Delta^3}\Big).$$

The constant is not fixed numerically: the paper states the theorem in $O(\cdot)$ form (footnote 1), and the explicit display it reports on p. 8, $40\ln T/\Delta+48/\Delta^3+18\Delta$, is not the formal claim.

Milestones

• Fact 1 (p. 12): $F^{beta}_{\alpha,\beta}(y)=1-F^B_{\alpha+\beta-1,y}(\alpha-1)$ for positive integers $\alpha,\beta$.
• Lemma 1 (p. 6): $\mathbb E[X(j,s,y)]=1/F^B_{j+1,y}(s)-1$.
• Lemma 6 (p. 13): Hoeffding-type bounds (10)–(11) on binomial cdfs.
• Fact 2 (p. 13): every median of $\mathrm{Binomial}(n,p)$ is $\lfloor np\rfloor$ or $\lceil np\rceil$.
• Lemma 2 (p. 7): $\Pr(E_2(t))\ge 1-2/T^2$, where $E_2(t)=\{\theta_2(t)\le\mu_2+\Delta/2\ \text{or}\ k_2(t)<24\ln T/\Delta^2\}$.
• Lemma 3 (p. 7): a three-case bound on $\mathbb E\big[\mathbb E[\min\{X(j,s(j),y),T\}\mid s(j)]\big]$ for $s(j)\sim\mathrm{Binomial}(j,\mu_1)$.
• Eq. (1) (p. 7): $\mathbb E[k_2(T)]\le C(\ln T/\Delta^2+1/\Delta^4)$.

Significance

The result. Theorem 1 shows that TS, a randomized Bayesian heuristic with no explicit confidence bonus, has regret logarithmic in $T$ on every two-armed instance, matching the order in $T$ of the Lai–Robbins lower bound. The proof introduced a way to control the optimal arm's waiting time between plays through the Beta–Binomial duality, and later analyses of TS reuse that device.

Formalizing it. The result is proved on paper and has no machine-checked proof that we know of. The platform's existing TS results concern Gaussian TS (Lattimore and Szepesvári, Ch. 36) and Bayesian regret, which are different algorithms or regret notions. A formalization adds a reusable Lean model of Algorithm 2 on $[0,1]$-valued rewards, Beta–Binomial facts (Fact 1, Lemma 1), a binomial-median theorem, and binomial Hoeffding bounds. It also produces a proof with a constant that has been checked, since the printed constants contain an arithmetic slip.

Difficulty

The standard UCB argument does not transfer to TS. For UCB, the optimal arm's index exceeds its mean with high probability however often the arm has been played, because the exploration bonus is deterministic; the analysis then only has to count plays of the suboptimal arm until its own index concentrates, after $\Theta(\ln T/\Delta^2)$ plays. Under TS the optimal arm's sample $\theta_1(t)$ is random and, if the arm has been played rarely or its early rewards were poor, it falls below $\mu_2$ with constant probability. The optimal arm may then wait a long, random time between plays, and the length of that wait depends on the arm's posterior, which in turn depends on how long it has waited. Counting plays of the suboptimal arm with a union bound over rounds, under the assumption that the optimal arm is already concentrated, therefore does not work; controlling these waiting times is the central difficulty and is where the $1/\Delta^3$ dependence enters.

Formalization scope

• Model. The instance is the platform's StochasticBandit 2 (a probability measure on $\mathbb R$ per arm, mean banditArmMean), with the hypothesis that each reward law gives mass $1$ to $[0,1]$. Lean arm 0 is the paper's arm 1 and Lean arm 1 the paper's arm 2. Lean rounds are indexed from $0$.
• Algorithm. Algorithm 2 is realized on one probability space with three independent i.i.d. tables: Beta draws $W(i,t,a,b)\sim\mathrm{Beta}(a+1,b+1)$, rewards $X(i,t)\sim D_i$, and uniforms $V(i,t)$. Round $t$ uses $\theta_i(t)=W(i,t,S_i(t),F_i(t))$, $\tilde r_t=X(i(t),t)$ and $r_t=\mathbf 1\{V(i(t),t)<\tilde r_t\}$. Ties in the arg max go to the smaller index (a null event).
• Values. Regret and expectations are lower Lebesgue integrals in $[0,\infty]$. $X(j,s,y)$ is $\mathbb N\cup\{\infty\}$-valued, so Lemma 1 at $y=1$ reads $\infty=\infty$, as in the paper.
• O(·). The paper's $O(\cdot)$ (footnote 1: $f\le cg$ for $n\ge n_0$) is stated with one universal constant $C>0$, quantified before the instance, the means and the horizon, for all $T\ge 2$. Eq. (1) is stated the same way, without its printed numerals.
• Not trivial. The goal is about Algorithm 2 itself, with fresh Beta samples, fresh rewards and the Bernoulli coin. A statement about "any policy satisfying Lemma 2's event bound", or one whose constant depends on $\Delta$, the reward laws or $T$, would not be Theorem 1.
• Edge cases. $\mu_1<1$ is assumed only in Lemma 3, where the paper's $R$ and $D$ require it. It is not a hypothesis of the goal.
• Infrastructure. A complete proof needs: inverse-transform or order-statistics facts for Beta laws (Fact 1); geometric expectations; Hoeffding's inequality for sums of Bernoulli variables (Mathlib has Hoeffding/Azuma); the binomial median theorem (Jogdeo–Samuels; Kaas–Buhrman); and the coupling from the reward tables to the per-arm i.i.d. output stacks the paper reasons with. Fact 1, Lemma 6 and Fact 2 are reusable beyond this mission. Contributions to any milestone are welcome, and so is a direct proof of the regret bound with an explicit constant.

Selected references

• S. Agrawal and N. Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem, COLT 2012; arXiv:1111.1797v3. https://arxiv.org/abs/1111.1797
• W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25 (1933) 285–294. https://doi.org/10.2307/2332286
• T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6 (1985) 4–22. https://doi.org/10.1016/0196-8858(85)90002-8
• P. Auer, N. Cesa-Bianchi and P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47 (2002) 235–256. https://doi.org/10.1023/A:1013689704352
• K. Jogdeo and S. M. Samuels, Monotone convergence of binomial probabilities and a generalization of Ramanujan's equation, Annals of Mathematical Statistics 39 (1968) 1191–1195. https://doi.org/10.1214/aoms/1177698243
• R. Kaas and J. M. Buhrman, Mean, median and mode in binomial distributions, Statistica Neerlandica 34 (1980) 13–18. https://doi.org/10.1111/j.1467-9574.1980.tb00681.x
• O. Chapelle and L. Li, An empirical evaluation of Thompson Sampling, NIPS 2011. https://papers.nips.cc/paper/4321-an-empirical-evaluation-of-thompson-sampling

Motivation

Most Markovian queueing models have no closed-form transient solution. The M/M/1 queue already needs modified Bessel functions (Chapter 2 of the book), and a finite-capacity or multi-class model with state-dependent rates has no closed form at all. What an analyst can always write down is the system of forward equations $p'(t)=p(t)Q$ for the state probabilities. Chapter 8 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), presents two numerical techniques that turn such models into numbers: the randomization (or uniformization) method for the transient distribution of a finite continuous-time Markov chain, and the Fourier-series method for inverting a Laplace transform, as needed for the M/G/1 waiting-time transform (5.33) and the busy-period transform (5.37).

Uniformization goes back to Jensen (1953) and is the standard transient solver in performance-evaluation and reliability tools. Its appeal is that it replaces a matrix exponential, which is numerically delicate, by powers of a stochastic matrix weighted by Poisson probabilities, with an error bound that can be fixed before the computation starts (Grassmann 1977; Gross and Miller 1984). The Fourier-series method with Euler summation is due to Abate and Whitt (Abate and Whitt 1992; Abate, Choudhury and Whitt 1999).

Setting

A continuous-time Markov chain $X(t)$ on the states $\{0,1,\dots,N\}$ is described by its infinitesimal generator $Q=(q_{ij})$: for $i\ne j$, $q_{ij}\ge0$ is the rate of jumps from $i$ to $j$, and the diagonal entry is $-q_i$ with

$$q_i=\sum_{j\ne i}q_{ij},\qquad i=0,1,\dots,N.$$

The transient state-probability vector $p(t)=(p_0(t),\dots,p_N(t))$, $p_n(t)=\Pr\{X(t)=n\}$, is the solution of the forward equations

$$p'(t)=p(t)Q\quad(t\ge0),$$

started from a given probability vector $p(0)$. Fix a constant $\Lambda>0$ with $\Lambda\ge q_i$ for every $i$ (the book takes $\Lambda=\max_i q_i$) and define the uniformized matrix

$$\tilde P=\frac{Q}{\Lambda}+I,\qquad \tilde p_{in}=\begin{cases}q_{in}/\Lambda&(i\ne n),\\1-q_i/\Lambda&(i=n).\end{cases}$$

It is the transition matrix of a discrete-time chain $Y_k$: the state of $X$ after the $k$-th event of a Poisson process of rate $\Lambda$ that has been thinned. Write $\phi^{(k)}=p(0)\tilde P^{k}$ for its distribution after $k$ steps.

For the second half of the chapter, the Laplace transform of a real function $f$ on $[0,\infty)$ is $\bar f(s)=\int_0^\infty e^{-st}f(t)\,dt$, and the Fourier-series approximant with parameter $A$ is

$$f_{A,n}(t)=\frac{e^{A/2}}{2t}\Big[\bar f\Big(\frac{A}{2t}\Big)+2\sum_{k=1}^{n}(-1)^k\,\mathrm{Re}\,\bar f\Big(\frac{A+2k\pi i}{2t}\Big)\Big],$$

with $f_A(t)=\lim_{n\to\infty}f_{A,n}(t)$.

Formalization targets

Goal: the randomization formula with its truncation bound (Eqs. (8.9)–(8.12))

The forward equations have a solution, and every solution satisfies, for all $t\ge0$,

$$p(t)=\sum_{k=0}^{\infty}p(0)\tilde P^{(k)}\,\frac{e^{-\Lambda t}(\Lambda t)^k}{k!},$$

and whenever $\sum_{k=0}^{T}e^{-\Lambda t}(\Lambda t)^k/k!>1-\epsilon$, every component of the sum truncated at $k=T$ is within $\epsilon$ of $p_n(t)$.

Milestones

1. Eq. (8.12): $\tilde P$ has the entries above and is a stochastic matrix.
2. Eqs. (8.13)–(8.14): $\phi^{(k)}=\phi^{(k-1)}\tilde P$ and each $\phi^{(k)}$ is a probability vector.
3. p.385: $\phi=\phi\tilde P\iff0=\phi Q$.
4. Eqs. (8.27)–(8.28): for bounded Lipschitz $f$, $A>0$ and $t>0$,

$$f_A(t)-f(t)=\sum_{k=1}^{\infty}e^{-kA}f\big((2k+1)t\big),\qquad |f_A(t)-f(t)|\le\frac{Ce^{-A}}{1-e^{-A}}\ \text{ if } |f(x)|\le C \text{ for } x>3t.$$

The mission also contains Eqs. (8.7)–(8.8) as a further theorem, outside the milestone list: the transition probabilities satisfy $p_{in}(t)=\sum_k\tilde p^{(k)}_{in}e^{-\Lambda t}(\Lambda t)^k/k!$, and $p_n(t)=\sum_i p_i(0)p_{in}(t)$.

Significance

The randomization formula reduces the transient analysis of any finite Markovian queue (finite-buffer, multi-server, with balking, reneging or state-dependent rates) to repeated vector–matrix products with a sparse stochastic matrix. The truncation point is chosen from a Poisson tail alone, independently of $Q$. Milestone 3 shows that the same matrix gives the stationary equations, so one iteration serves both transient and steady-state computation. The discretization identity (8.27) is what justifies the parameter choice in Algorithm 8.1: the error decays like $e^{-A}$.

All of these results are classical and proved in the literature. None of them is formalized in Lean or Mathlib as far as a search of the platform and Mathlib shows. Mathlib has the matrix exponential and Poisson summation under decay hypotheses, but no continuous-time Markov chain generators, no uniformization, and no Laplace transform. This mission would add the finite-state link between generators, stochastic matrices and matrix exponentials that later chapters of queueing and reliability theory use, and a verified error formula for a numerical inversion method in wide use.

Difficulty

The book's derivation is probabilistic: it conditions on the number of events of the Poisson($\Lambda$) process and thins them. A formal statement cannot rest on that picture, because $p(t)$ is defined analytically, by the forward equations. The goal therefore contains a uniqueness statement for a linear ODE on $[0,\infty)$ with one-sided derivative at $0$, which the book never mentions. The componentwise bound then needs $\tilde P$ to be stochastic, so that every $\phi^{(k)}_n$ lies in $[0,1]$. That is exactly where $\Lambda\ge\max_i q_i$ is used; with a smaller $\Lambda$ the matrix $\tilde P$ has negative diagonal entries and the bound fails.

For (8.27), the book gives no proof. The identity is an aliasing (Poisson-summation) formula for a periodic function assembled from the values of $f$ at all odd multiples of $t$. The convergence of the conditionally summed series (8.24) is the delicate point: continuity of $f$ at $t$, the book's only hypothesis, does not guarantee convergence of a Fourier series. Mathlib's Poisson summation theorems require decay of the Fourier transform that the damped, reflected function built from $f$ does not have.

Formalization scope

• States are Fin (N+1); a row vector is Fin (N+1) → ℝ; $pQ$ is vecMul. A generator is a real matrix with nonnegative off-diagonal entries and diagonal $-\sum_{j\ne i}q_{ij}$.
• $p(t)$ is not defined as the series. It is any function with $p(0)=p_0$ and one-sided derivative $p(t)Q$ within $[0,\infty)$ at every $t\ge0$. The goal also asserts that such a function exists, so it cannot hold vacuously, and it asserts the series identity for every solution. Defining $p(t)$ as the series (8.9) would make the goal a tautology and is ruled out.
• $\Lambda$ is any real with $\Lambda>0$ and $\Lambda\ge q_i$ for all $i$ (the book takes equality with $\max_i q_i$).
• The truncation bound is stated componentwise, as on p.384 ("an error bound on $p_n(t)$ of $\epsilon$"), for an arbitrary real $\epsilon$ and truncation point $T$.
• The series (8.8), (8.9) are stated with HasSum, so convergence is part of the claim.
• The Laplace transform is the Lebesgue integral over $(0,\infty)$ at a complex argument. $f_A(t)$ is the limit of the partial sums $f_{A,n}(t)$, and the convergence is part of milestone 4.
• Strengthened hypotheses in milestone 4: $f$ bounded and Lipschitz on $[0,\infty)$ replaces "$t$ is a continuity point of $f$", which is not sufficient for convergence.
• Corrected misprints: $e^{-\lambda t}$ in (8.9) is $e^{-\Lambda t}$; $q_{ij}/\Lambda$ in (8.12) is $q_{in}/\Lambda$; $\phi(Q/\Lambda-I)$ on p.385 is $\phi(Q/\Lambda+I)$.
• Not formalized: Theorem 8.1 (Bromwich inversion) and the real form (8.21), which the book states without hypotheses on $f$; the limit claim $\lim_k\phi^{(k)}=\lim_t p(t)$ on p.385, which fails when $\tilde P$ is periodic; the Euler-summation approximation (8.26) and the round-off discussion, which are stated with "≈".

Useful infrastructure: the matrix exponential and its derivative (Matrix, NormedSpace.exp), uniqueness for linear ODEs (Grönwall), Fourier series on the circle, and a reusable Laplace transform file. Contributions of general lemmas on generators and stochastic matrices are welcome, as they apply to every finite Markovian model in the series.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §§8.1.2–8.2. https://doi.org/10.1002/9781118625651
• A. Jensen, "Markoff chains as an aid in the study of Markoff processes", Skandinavisk Aktuarietidskrift 36 (1953) 87–91.
• W. K. Grassmann, "Transient solutions in Markovian queueing systems", Computers & Operations Research 4 (1977) 47–53.
• D. Gross, D. R. Miller, "The randomization technique as a modeling tool and solution procedure for transient Markov processes", Operations Research 32 (1984) 343–361. https://doi.org/10.1287/opre.32.2.343
• J. Abate, W. Whitt, "The Fourier-series method for inverting transforms of probability distributions", Queueing Systems 10 (1992) 5–87. https://doi.org/10.1007/BF01158520
• J. Abate, G. L. Choudhury, W. Whitt, "An introduction to numerical transform inversion and its application to probability models", in W. Grassmann (ed.), Computational Probability, Kluwer, 1999, 257–323.

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

Many stochastic and nondifferentiable optimization problems are not solved by minimizing their true objective $f^0$ directly: $f^0$ may be nonsmooth, an expectation that cannot be evaluated, or only approximately known. A standard remedy replaces $f^0$ by a sequence of "good" approximations $F^0(\cdot, s)$ (smoothed versions, sample averages, perturbations) that converge to $f^0$, and runs one step of a descent method on the current approximation at every iteration. Approximation and optimization then proceed simultaneously. More generally, in nonstationary optimization the objective $F^0(\cdot, s)$ and the feasible set $X_s$ change with the iteration number $s$, and the iterates $x^s$ are required to follow the time path of the optimal solutions,

$$\lim_{s\to\infty}\bigl[F^0(x^s, s) - \min\{F^0(x, s) \mid x \in X_s\}\bigr] = 0 .$$

Such procedures are essentially nonmonotone: a step on $F^0(\cdot, s)$ gives no guarantee of decrease of $F^0(\cdot, t)$ for $t \ge s+1$, nor of $f^0$. Their convergence therefore cannot be proved by the usual monotone Lyapunov argument. Section 6.4 of Yu. Ermoliev's chapter "Stochastic Quasigradient Methods" in Ermoliev & Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), gives the basic deterministic convergence theorem for this setting (Theorem 6.3) and the convergence criterion for nonmonotone sequences on which its proof rests (Theorem 6.4, taken from Ermoliev's 1976 monograph; the chapter compares its conditions with Zangwill's necessary and sufficient convergence conditions).

Timeline, as recorded in the chapter's bibliography (pp. 180–181): Ermoliev and Nurminski introduced limit extremal problems, in which $F^0(\cdot, s)$ and $X_s$ both converge ("Limit extremal problems", Kibernetika 1973, [14]); Nurminski gave convergence conditions for stochastic programming algorithms (Kibernetika 1973, [11]); Gupal treated time-varying functions (Kibernetika 1974, [15]); Ermoliev's monograph Stochastic Programming Methods (Nauka, 1976, [5]) contains the criterion stated here as Theorem 6.4 (p. 181); Nurminski formulated the general problem of nonstationary optimization (Kibernetika 1977, [16]); and Gaivoronski proved convergence of stochastic nonstationary procedures (Kibernetika 1978, [19]), the source of the chapter's Theorem 6.5.

Setting

Throughout, points are vectors of $\mathbb R^n$ with the Euclidean norm $\|\cdot\|$ and inner product $\langle\cdot,\cdot\rangle$.

• The projection onto a nonempty closed convex set $X \subseteq \mathbb R^n$ is $\pi_X(y) = \arg\min\{\|y - x\|^2 : x \in X\}$, the unique nearest point of $X$ to $y$.
• A subgradient of a convex function $F : \mathbb R^n \to \mathbb R$ at $x$ is a vector $g$ with $F(y) \ge F(x) + \langle g, y - x\rangle$ for all $y$. The book writes $F^0_x(x, s)$ for a subgradient of $F^0(\cdot, s)$ at $x$.
• The nonstationary projected subgradient method (6.41) starts from any $x^0 \in \mathbb R^n$ and sets

$$x^{s+1} = \pi_X\bigl[x^s - \rho_s g_s\bigr], \qquad g_s \text{ a subgradient of } F^0(\cdot, s) \text{ at } x^s,\quad s = 0, 1, \dots$$

with step sizes $\rho_s \ge 0$.

• For a closed set $X^*$ (in the application, the set of minimizers of $f^0$ on $X$) and a sequence $(x^s)$, the exit time from the $\varepsilon$-ball around $x^{s_k}$ is $\tau_k = \min\{s \ge s_k : \|x^s - x^{s_k}\| > \varepsilon\}$.
• The Lyapunov function of the proof is $V(x) = \min_{x^* \in X^*}\|x^* - x\|^2$, the squared distance to $X^*$.

Formalization targets

Goal: Theorem 6.3 (pp. 153–154)

Let $F^0(\cdot, s)$ and $f^0$ be convex continuous on $\mathbb R^n$, $X$ a nonempty convex compact set, $F^0(\cdot, s) \to f^0$ uniformly on $X$, $\|g_s\| \le C$, $\rho_s \ge 0$, $\rho_s \to 0$ and $\sum_s \rho_s = \infty$. Then the iterates of (6.41) satisfy

$$F^0(x^s, s) \longrightarrow \min\{f^0(x) \mid x \in X\} \qquad (s \to \infty).$$

The statement fixes no rate and no constant: only the qualitative limit, which is what the book proves.

Milestones

1. p. 155 — the one-step recursion $V(x^{s+1}) \le V(x^s) + 2\rho_s\langle g_s, x^*(s) - x^s\rangle + \rho_s^2\|g_s\|^2$, with $x^*(s)$ a point of $X^*$ nearest to $x^s$.
2. p. 156 — the travel bound $\|x^b - x^a\| \le \sum_{s=a}^{b-1}\|x^{s+1} - x^s\| \le C\sum_{s=a}^{b-1}\rho_s$ along (6.41) once $x^a \in X$.
3. p. 155 — conditions (1) and (2)(a) of Theorem 6.4 for (6.41): the iterates stay in a compact set and $\|x^{s+1} - x^s\| \to 0$.
4. Theorem 6.4 (p. 155) — if $X^*$ is closed, $(x^s)$ lies in a compact set, steps vanish along subsequences converging into $X^*$, the sequence leaves every small ball around a subsequential limit outside $X^*$, and it leaves with a strictly lower value of a continuous $V$ that takes countably many values on $X^*$, then $V(x^s)$ converges and all accumulation points lie in $X^*$.
5. pp. 155–156 — conditions (2)(b) and (3) of Theorem 6.4 for (6.41) with $X^* = \arg\min_X f^0$ and $V = \operatorname{dist}(\cdot, X^*)^2$:

$$\limsup_{k\to\infty} V(x^{\tau_k}) < \lim_{k\to\infty} V(x^{s_k}).$$

Significance

Theorem 6.3 is the prototype of the convergence results for simultaneous optimization and approximation. It covers smoothing schemes in which $f^0$ is replaced by $F^0(x, s) = \mathbb E f^0(x + h(s))$ with a vanishing perturbation $h(s)$ (the chapter's (6.39)–(6.40)), penalty and regularization sequences, and the deterministic skeleton of stochastic nonstationary methods such as Theorem 6.5. Theorem 6.4 is reusable well beyond this mission: it is a general tool for proving that accumulation points of a nonmonotone algorithm are solutions; the chapter introduces it as the tool for "essentially nonmonotonic solution procedures" in general.

Both results are classical and proved (Theorem 6.3 in the chapter itself, Theorem 6.4 in Ermoliev's 1976 monograph, whose proof the chapter cites but does not reproduce). No machine-checked proof of either is known to the platform's catalogue (searches for nonstationary optimization, Zangwill-type criteria and nonmonotone convergence return no match). The formalization adds a Lean statement and proof of a nonmonotone convergence criterion, a Lean proof of convergence for projected subgradient steps on a changing objective, and reusable facts about Euclidean projection onto a convex compact set.

Difficulty

The obvious argument for projected subgradient methods tracks $V(x^s) = \operatorname{dist}(x^s, X^*)^2$ and shows that it decreases whenever $x^s$ is far from $X^*$. Here that argument fails at two points. First, the subgradient is taken on $F^0(\cdot, s)$, not on $f^0$, so the decrease of $V$ holds only up to an error controlled by $\sup_X|F^0(\cdot, s) - f^0|$, and only while the iterate stays away from $X^*$; near $X^*$, $V$ may increase. Second, a decrease of $V$ over each excursion does not by itself exclude "cycling": the sequence may visit every neighbourhood of a point $x' \notin X^*$ infinitely often. Theorem 6.4 is formulated in terms of exit times and subsequences rather than single steps for this reason, and its hypothesis that $V$ takes only countably many values on $X^*$ is what separates it from a monotone-descent statement.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); sequences are indexed by ℕ from $s = 0$ as in the book. The iteration (6.41) is a hypothesis on a given sequence, x (s+1) = projX X (x s - ρ s • g s), with a given selection of subgradients g s; the subgradient inequality is required on all of $\mathbb R^n$, and $F^0(\cdot, s)$, $f^0$ are convex and continuous on all of $\mathbb R^n$.
• projX X y is a minimizer of $\|y - x\|^2$ over $X$ (junk value $y$ when none exists; every statement assumes $X$ nonempty, closed and convex). optimalSet f X is the set of minimizers of $f$ on $X$; $V$ is Metric.infDist · X* ^ 2.
• Added hypotheses the page does not print: $\rho_s \ge 0$ (step sizes are nonnegative throughout the chapter) and $X \ne \varnothing$ (the minimum over $X$ must exist). The limit $\min_X f^0$ is written sInf (f '' X); $\sum_s\rho_s = \infty$ is divergence of the partial sums.
• Constants. The only unspecified constant is the $C$ of the travel bound on p. 156 ("where $C$ is a constant"); the proof yields $C$ = the bound of hypothesis (d), $\|g_s\| \le C$, and that is the constant in milestone 2. All other results are qualitative.
• Corrections of the page. (i) Theorem 6.4 (2)(b) is printed as "$\tau_k = \min\{s \mid s \ge s_k, \|x^{s_k} - x^s\| < \varepsilon\} > \infty$", which no sequence satisfies; following the proof of Theorem 6.3 it is read as: $\tau_k = \min\{s \ge s_k : \|x^s - x^{s_k}\| > \varepsilon\}$ is finite. "For $\varepsilon$ sufficiently small and for any $s_k$" is read as "there is $\varepsilon_0 > 0$ such that for all $\varepsilon \in (0,\varepsilon_0)$ and all $k$", and condition (3) is imposed for the same $\varepsilon$. (ii) The left limit in (3) is read as $\limsup$ (the proof prints $\overline{\lim}$); the right limit is $V(x')$. (iii) The display on p. 155 prints "$=$" where the projection gives "$\le$". (iv) The proof on p. 155 prints "$x^{s_k} \to x' \in X^*$" where $x' \notin X^*$ is meant.
• Theorem 6.5 (the stochastic version, p. 156) is not formalized: the chapter states it without proof, citing [19], its moment hypothesis $E\|\xi^0(s)\| < \mathrm{const}$ and the measurability of the random step sizes $\rho_s$ are not pinned down on the page, and it is not used by Theorem 6.3.
• A trivializing formalization is ruled out: the goal is about the iteration (6.41) itself, not a statement that assumes $x^s \to X^*$ and derives the limit of the values, and no hypothesis forces the sequence or the functions to be constant.
• Contributions welcome: properties of projX (existence, uniqueness, nonexpansiveness, the obtuse-angle characterization), a proof of Theorem 6.4, and the two proof steps on pp. 155–156.

Selected references

• Yu. Ermoliev, "Stochastic Quasigradient Methods", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 6, pp. 141–185 (§6.4, pp. 152–156). https://doi.org/10.1007/978-3-642-61370-8
• Yu. M. Ermoliev, Stochastic Programming Methods (in Russian), Nauka, Moscow, 1976 (the chapter's [5]; Theorem 6.4 is on p. 181).
• Yu. M. Ermoliev and E. A. Nurminski, "Limit extremal problems", Kibernetika 1 (1973) (the chapter's [14]).
• E. A. Nurminski, "Convergence conditions of algorithms of stochastic programming", Kibernetika 3 (1973) (the chapter's [11]).
• E. A. Nurminski, "The problem of nonstationary optimization", Kibernetika 2 (1977) (the chapter's [16]).
• A. A. Gaivoronski, "Nonstationary stochastic programming problems", Kibernetika 4 (1978) (the chapter's [19]).
• W. I. Zangwill, Nonlinear Programming: A Unified Approach, Prentice-Hall, 1969.

Why birth–death queues and Erlang's formulas

Every call center, hospital ward, cloud server pool and telephone exchange that is sized by formula is sized by one of a handful of explicit expressions from Markovian queueing theory. The two oldest are A. K. Erlang's: the Erlang-B (loss) formula of 1917, which gives the fraction of calls lost when $c$ trunks carry an offered load of $r$ erlangs, and the Erlang-C formula, which gives the probability that a customer of a $c$-server queue must wait. Both are still the default dimensioning rules of telecommunications and call-center workforce management (Gans, Koole & Mandelbaum 2003).

This mission formalizes Chapter 2, §§2.1–2.10, of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory, 4th ed. (Wiley 2008), which derives these formulas from a single result about birth–death processes and closes with the modern answer to the staffing question.

Timeline. Erlang (1917) obtained the loss formula; Vaulot (1927), Pollaczek (1932), Palm (1938) and Kosten (1948) completed its proof for general service times. Halfin and Whitt (1981) showed that in the $M/M/n$ queue the delay probability converges to a limit strictly between $0$ and $1$ exactly when the number of servers exceeds the offered load by an amount of order $\sqrt n$. This is the quality-and-efficiency-driven (QED) regime on which square-root staffing rests.

Setting

A birth–death process is a continuous-time Markov chain on the states $n \in \{0, 1, 2, \dots\}$ that moves from $n$ to $n+1$ at rate $\lambda_n \ge 0$ (a birth, or arrival) and, for $n \ge 1$, from $n$ to $n-1$ at rate $\mu_n > 0$ (a death, or departure). A steady-state solution is a probability sequence $\{p_n\}$ ($p_n \ge 0$, $\sum_n p_n = 1$) solving the global balance equations (2.1):

$$(\lambda_n + \mu_n)p_n = \lambda_{n-1}p_{n-1} + \mu_{n+1}p_{n+1}\ (n \ge 1), \qquad \lambda_0 p_0 = \mu_1 p_1.$$

The queues of the chapter are birth–death processes with particular rates. The $M/M/1$ queue has $\lambda_n = \lambda$, $\mu_n = \mu$ and traffic intensity $\rho = \lambda/\mu$. The $M/M/c$ queue has $\lambda_n = \lambda$, $\mu_n = \min(n, c)\mu$ (2.30), offered load $r = \lambda/\mu$ and $\rho = r/c$. The $M/M/c/c$ loss system is the same with $\lambda_n = 0$ for $n \ge c$. The $M/M/\infty$ queue has $\mu_n = n\mu$.

The explicit functions are the Erlang-B formula

$$B(c, r) = \frac{r^c/c!}{\sum_{i=0}^{c} r^i/i!},$$

the Erlang-C formula, defined for $\rho = r/c < 1$,

$$C(c, r) = \frac{r^c/(c!(1-\rho))}{r^c/(c!(1-\rho)) + \sum_{n=0}^{c-1} r^n/n!},$$

and, with $\phi$, $\Phi$ the standard normal density and distribution function,

$$\alpha(\beta) = \frac{\phi(\beta)}{\phi(\beta) + \beta\Phi(\beta)}.$$

Formalization targets

Goal: the Halfin–Whitt theorem (§2.4, p.75)

For offered loads $0 < r_n < n$,

$$\lim_{n\to\infty} C(n, r_n) = \alpha \in (0,1) \iff \lim_{n\to\infty} \frac{n - r_n}{\sqrt n} = \beta > 0, \qquad \alpha = \alpha(\beta).$$

It is stated as three facts: $\alpha$ maps $(0, \infty)$ into $(0, 1)$; each $\alpha \in (0, 1)$ has exactly one preimage $\beta > 0$; and for every $\beta > 0$ the two limits are equivalent.

Milestones

1. (2.3)–(2.4): the steady-state solution of a general birth–death process, $p_n = p_0\prod_{i=1}^n \lambda_{i-1}/\mu_i$, and its existence if and only if $1 + \sum_{n\ge1}\prod_{i=1}^n \lambda_{i-1}/\mu_i < \infty$.
2. (2.9): $M/M/1$, $p_n = (1-\rho)\rho^n$, existing iff $\rho < 1$.
3. (2.31)–(2.32): the $M/M/c$ law, existing iff $\lambda/(c\mu) < 1$.
4. (2.33): $L_q = r^c\rho\,p_0/(c!(1-\rho)^2)$.
5. (2.37)–(2.38): $1 - \sum_{n<c} p_n = C(c, r)$.
6. (2.52)–(2.53): the $M/M/c/c$ law and $p_c = B(c, r)$.
7. (2.54): $B(c, r) = rB(c-1, r)/(c + rB(c-1, r))$, $B(0, r) = 1$.
8. (2.55): $C(c, r) = cB(c, r)/(c - r + rB(c, r))$.
9. (2.57): $M/M/\infty$, $p_n = r^n e^{-r}/n!$.

Significance

The results. Items 1–9 are the working formulas of Markovian capacity planning: a stationary law for each basic model and the measures read off from it. (2.54) and (2.55) are how $B$ and $C$ are computed in practice, since the factorials of the closed forms overflow for $c > 170$. The Halfin–Whitt theorem is the reason the rule $c \approx r + \beta\sqrt r$ holds a fixed service level, and it is the entry point to the QED heavy-traffic literature (diffusion limits of many-server queues, Garnett–Mandelbaum–Reiman, Gamarnik–Momčilović).

Formalizing them. All results are classical and proved in the literature. The book states the Halfin–Whitt theorem without proof, and (2.54)–(2.55) are left to exercises. The formalization would supply machine-checked versions of the Erlang identities and of the Halfin–Whitt limit theorem. No Lean development of either was found on the platform when this mission was drafted. A related Erlang-B statement from Kelly and Yudovina is on the platform, stated with detailed balance on a finite state space.

Difficulty

The stationary laws are induction plus geometric and exponential series, and the Erlang identities are finite algebra. The difficulty is concentrated in the goal. $C(n, r_n)$ is a ratio of a Poisson-type tail to a truncated exponential sum in which both $n$ and $r_n$ grow. The naive route, substituting Stirling's formula term by term, fails: the sums have $\Theta(\sqrt n)$ significant terms, each of relative size $\exp(-k^2/2n)$, and the error has to be controlled uniformly over them. The converse direction also requires showing that $\alpha(\cdot)$ is strictly monotone. Without that, convergence of $C(n, r_n)$ does not force convergence of $(n - r_n)/\sqrt n$.

Formalization scope

Rates are real sequences indexed by $\mathbb N$, and a steady-state solution is a real sequence with HasSum p 1, nonnegative entries, and the balance equations (2.1) exactly as printed (global balance, not detailed balance). Every "the steady-state solution is X" is stated in both halves: X is a steady-state solution, and every steady-state solution equals X; the book's existence conditions ($\rho < 1$, $\lambda/(c\mu) < 1$, convergence of the series) are part of the statements. The $M/M/c/c$ system is the $\mathbb N$-indexed process with $\lambda_n = 0$ for $n \ge c$, as §2.5 sets it up; the statement records that states above $c$ carry no mass.

The closed forms that are fixed in Lean: $\prod_{i=1}^n \lambda_{i-1}/\mu_i$ over Finset.Icc 1 n; $B(c, r)$ and $C(c, r)$ exactly as displayed above; $\phi$ = gaussianPDFReal 0 1, $\Phi$ = the CDF of gaussianReal 0 1; $W_q(0) = \sum_{n=0}^{c-1} p_n$, as evaluated on p.69; $L_q = \sum_{n > c}(n - c)p_n$ as a convergent series.

$C(c, r)$ is a total function in Lean, but its value for $r \ge c$ carries no meaning. The goal assumes $0 < r_n < n$ for $n \ge 1$, the book's standing condition $\rho < 1$. A statement about some other function with the same limiting behaviour, or with $B$ and $C$ left abstract, would not be this mission. Neither would one-directional or existence-only versions of the stationary laws.

Not included: the waiting-time distributions (2.28) and (2.39), which need an FCFS waiting-time model with arrival-point probabilities; the $M/M/c/K$ measures (2.45)–(2.48); finite-source and state-dependent models (§§2.8–2.10). Useful contributions beyond the milestones are Poisson tail estimates at the $\sqrt n$ scale and monotonicity of $\alpha(\beta)$. Both are reusable in other many-server heavy-traffic statements.

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
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• N. Gans, G. Koole, A. Mandelbaum, Telephone call centers: tutorial, review, and research prospects, Manufacturing & Service Operations Management 5(2), 79–141, 2003. https://doi.org/10.1287/msom.5.2.79.16071
• A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektroteknikeren 13, 1917 (English translation in The Life and Works of A. K. Erlang, 1948).
• F. P. Kelly, E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781139565363

Motivation

Bayesian mechanism design asks which collective decisions and payments a designer can implement when every agent holds private information, the type, drawn from a commonly known prior. Most of the classical theory (Myerson's optimal auction, the Myerson–Satterthwaite impossibility, the public goods results) assumes that types are independent. Once types are correlated, as they are when bidders' values share a common component, the theory changes in a way that is best read as a paradox: Crémer and McLean (Econometrica 1988) showed that a designer can then extract the entire surplus, leaving agents no information rents. This mission formalizes Chapter 6 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press 2015), which sets up Bayesian mechanism design in general, treats independent types, and proves the Crémer–McLean theorem, together with the one numbered result of Chapter 9, the impossibility theorem of Jehiel and Moldovanu for interdependent values.

Timeline of the results formalized here:

• Rochet (1987) characterized implementable decision rules by cyclical monotonicity; Proposition 6.1 is its interim version for independent types.
• Crémer and McLean (1988): under their condition on the prior, every direct mechanism can be made Bayesian incentive-compatible without changing its decision rule or interim payments (Proposition 6.4).
• Krishna and Maenner (2001): revenue equivalence for convex type sets and convex utilities (Proposition 6.2).
• Jehiel and Moldovanu (2001): with interdependent values, efficient decisions are generically not Bayesian implementable (Proposition 9.1).
• Kosenok and Severinov (2008): an identifiability condition added to Crémer–McLean gives ex post budget balance as well (Proposition 6.6).

Setting

There are finitely many agents $i \in I$ and a set $A$ of alternatives. Agent $i$ has a type $\theta_i \in \Theta_i$ and utility $u_i(a,\theta_i) - t_i$ from alternative $a$ and payment $t_i$. Types $\theta = (\theta_1,\dots,\theta_N) \in \Theta = \prod_i \Theta_i$ are drawn from a common prior $\mu$; $\mu(\cdot\mid\theta_i)$ is the conditional distribution of the others' types $\theta_{-i}$ given $\theta_i$. Types are independent if $\mu(\cdot\mid\theta_i)$ does not depend on $\theta_i$.

A direct mechanism $(q, t_1,\dots,t_N)$ is a decision rule $q:\Theta\to A$ and payment rules $t_i:\Theta\to\mathbb R$. It is Bayesian incentive-compatible (BIC) if for every $i$ and all $\theta_i,\theta_i'$,

$$\int_{\Theta_{-i}} u_i(q(\theta_i,\theta_{-i}),\theta_i) - t_i(\theta_i,\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i) \ \ge\ \int_{\Theta_{-i}} u_i(q(\theta_i',\theta_{-i}),\theta_i) - t_i(\theta_i',\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i).$$

The interim decision rule $Q_i(\theta_i)$ is the distribution of $q(\theta_i,\theta_{-i})$ given $\theta_i$, and the interim expected payment is $T_i(\theta_i) = \int t_i(\theta_i,\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i)$. A mechanism is ex post budget balanced if $\sum_i t_i(\theta) = 0$ for every $\theta$, and ex ante budget balanced if $\int_\Theta \sum_i t_i\,d\mu = 0$.

In §6.4 every $\Theta_i$ is finite and $\mu(\theta) > 0$ for every $\theta$. The prior satisfies the Crémer–McLean condition if for no agent $i$ and type $\theta_i$ there are weights $\lambda \ge 0$ on $\Theta_i\setminus\{\theta_i\}$ with

$$\mu(\theta_{-i}\mid\theta_i) = \sum_{\theta_i'\ne\theta_i}\lambda(\theta_i')\,\mu(\theta_{-i}\mid\theta_i')\quad\text{for all }\theta_{-i}.$$

Identifiability requires that for every full-support distribution $\nu\ne\mu$ some agent's type $\theta_i$ has a belief $\nu(\cdot\mid\theta_i)$ that is not a nonnegative combination of the beliefs $\mu(\cdot\mid\theta_i')$.

Formalization targets

Goal: Crémer–McLean (Proposition 6.4)

If $\mu$ satisfies the Crémer–McLean condition, then for every direct mechanism $(q,t)$ there is a BIC direct mechanism $(q,t')$ with

$$\sum_{\theta_{-i}} t_i(\theta_i,\theta_{-i})\,\mu(\theta_{-i}\mid\theta_i) = \sum_{\theta_{-i}} t_i'(\theta_i,\theta_{-i})\,\mu(\theta_{-i}\mid\theta_i)\quad\text{for all } i,\theta_i.$$

Milestones

1. Proposition 6.1 (independent types): $q$ is part of a BIC mechanism iff it is interim cyclically monotone, $\sum_{\kappa=1}^{k-1}\big(\int_A u_i(a,\theta_i^{\kappa+1})\,dQ_i(\theta_i^\kappa) - \int_A u_i(a,\theta_i^\kappa)\,dQ_i(\theta_i^\kappa)\big)\le 0$ for every cycle $\theta_i^k = \theta_i^1$.
2. Proposition 6.2 (independent types, convex type sets, convex utilities): two BIC mechanisms with $Q_i' = Q_i$ have $T_i' = T_i + \tau_i$.
3. Proposition 6.3 (independent types): every ex ante budget balanced mechanism has an equivalent ex post budget balanced one.
4. Proposition 6.5 (Farkas's alternative), already proved on the platform as Polyhedral.farkas_lemma.
5. Proposition 6.6 (Kosenok–Severinov): under Crémer–McLean and identifiability, every ex ante budget balanced mechanism has an equivalent BIC and ex post budget balanced one.
6. Proposition 9.1 (Jehiel–Moldovanu): in the linear interdependent-values model, under a regularity condition on first best rules and the weight condition $\alpha^i_{ai}/\alpha^i_{bi}\ne\sum_j\alpha^i_{aj}/\sum_j\alpha^i_{bj}$ for some $i,a,b$, no first best direct mechanism is BIC. It uses its own model (§9.3) and is not on the goal's proof path.

Significance

The Crémer–McLean theorem says that, with correlated finite types, incentive compatibility imposes essentially no constraint: every decision rule and every interim payment rule can be implemented. In a single-unit auction this gives full surplus extraction. The result is the benchmark against which the literature on risk aversion, limited liability, collusion and the genericity of priors (Robert 1991, Laffont–Martimort 2000, Heifetz–Neeman 2006) measures its departures, and Proposition 6.6 extends it to budget-balanced mechanisms, which is what bilateral trade and public goods applications need. Propositions 6.1–6.3 are the independent-types counterpart that the correlated case breaks: they show why revenue equivalence and the ex ante/ex post budget-balance equivalence hold there and fail here. Proposition 9.1 shows the opposite failure, for interdependent values, where efficient decisions cannot be implemented even without participation or budget constraints.

All results are proved in the literature (Kosenok–Severinov's proof is omitted in the book). Apart from Farkas's alternative (Proposition 6.5), which is proved on the platform, none of them is formalized in Mathlib or on the platform; the platform's other mechanism design results (dominant-strategy results in a valuation model, revenue equivalence for symmetric independent auctions) do not cover correlated types.

Difficulty

For the goal the difficulty is the uniformity of the construction: a single payment adjustment must make truth-telling optimal against every possible deviation of every type of every agent, while leaving each type's expected payment unchanged. The obvious scoring-rule adjustment, charging $-\ln\mu(\theta_{-i}\mid\theta_i')$, changes interim payments, and removing that change is where the Crémer–McLean condition enters. For Proposition 6.2 the envelope argument must handle convex type sets that are not open and utilities that are only convex, not differentiable. For Proposition 9.1 the obvious argument differentiates interim utility twice; the proposition does not assume that interim utility is twice differentiable, so that regularity has to be derived from the hypotheses on the interim probabilities.

Formalization scope

Three definition files carry the three models. Independent types (§6.2–6.3): type sets are arbitrary measurable spaces, the prior is the product of probability measures $\rho_i$, and interim quantities are integrals against it. Finite correlated types (§6.4): finite type sets, a prior $\mu:\Theta\to\mathbb R$ with $\mu(\theta)>0$ and $\sum_\theta\mu(\theta)=1$, and conditional beliefs $\mu(\theta_{-i}\mid\theta_i) = \mu(\theta)/\mu(\theta_i)$; the alternative set $A$ is arbitrary. Interdependent values (§9.3): finite $A$, signals in $[0,1]^A$ with positive densities, independent across agents, linear utilities with nonzero weights $\alpha^j_{ai}$.

Committed conventions and explicit formulas:

• The Crémer–McLean condition uses nonnegative weights without a sum-to-one constraint, as Definition 6.7 prints it.
• "Equivalent" in Propositions 6.4 and 6.6 means the same decision rule and the same interim expected payments at truthful reports, as Proposition 6.4 states; in Proposition 6.3 it is the report-by-report notion, which under independence is equality of the interim payment rules $T_i$.
• Proposition 6.2 adds continuity of $u_i(a,\cdot)$ on $\Theta_i$, and Proposition 6.3 adds at least two agents; without them the printed statements are false.
• Measurability, which the book omits throughout, is made explicit: decision rules are measurable, and the payment sections and utilities are integrable against the relevant interim distributions.
• In Proposition 9.1 the partial derivatives are derivatives within the closed cube $[0,1]^K$, and the weight condition is the displayed ratio inequality.

A trivializing formalization of the goal, one that proves it only for mechanisms that are already incentive compatible, or with a payment rule that is not a function of the reported type profile, or with "equivalent" weakened to "some BIC mechanism exists", is ruled out: the statement quantifies over every direct mechanism and fixes both the decision rule and every interim payment.

Reusable infrastructure: finite conditional expectations under a full-support prior, the Crémer–McLean and identifiability conditions, and the interim model with product priors. Proofs of any milestone and of the goal, including via the Farkas reference, are welcome.

Selected references

• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• J. Crémer and R. P. McLean, "Full extraction of the surplus in Bayesian and dominant strategy auctions", Econometrica 56(6), 1988. https://doi.org/10.2307/1913096
• G. Kosenok and S. Severinov, "Individually rational, budget-balanced mechanisms and allocation of surplus", Journal of Economic Theory 140(1), 2008.
• P. Jehiel and B. Moldovanu, "Efficient design with interdependent valuations", Econometrica 69(5), 2001. https://doi.org/10.1111/1468-0262.00237
• V. Krishna and E. Maenner, "Convex potentials with an application to mechanism design", Econometrica 69(4), 2001. https://doi.org/10.1111/1468-0262.00225
• J.-C. Rochet, "A necessary and sufficient condition for rationalizability in a quasi-linear context", Journal of Mathematical Economics 16(2), 1987. https://doi.org/10.1016/0304-4068(87)90007-3