Stochastic Systems

Motivation

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

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

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

Setting

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

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

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

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

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

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

Formalization targets

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

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

Infinite horizon dynamic programming asks for the least expected cost of controlling a stochastic system forever, and for a policy attaining it. On finite or countable state spaces the theory has been classical since Bellman, Blackwell (1965) and Strauch (1966). Many models in operations research, inventory control, queueing and economics have continuous states and controls, however, and there the Bellman equation raises a question the countable theory never meets: the optimal cost need not be Borel-measurable, so its expectation under the transition law, which the equation requires, may not be defined.

Bertsekas and Shreve (1978) settled this question by working with lower semianalytic cost functions and universally measurable policies. In that framework the optimal cost is always measurable enough to be integrated, and the optimality equation holds with no continuity or compactness assumption. Chapter 9 of their book treats the infinite horizon model under the three classical cost structures: nonnegative costs (P), nonpositive costs (N), and bounded discounted costs (D).

Timeline:

• 1965: Blackwell, discounted dynamic programming on Borel spaces with Borel-measurable data, case (D).
• 1966: Strauch, negative dynamic programming, case (N), with Borel-measurable data.
• 1978: Bertsekas and Shreve, Chapter 9: lower semianalytic costs and universally measurable policies, in all three cases (P), (N), (D).
• 1979: Shreve and Bertsekas, the journal account of universally measurable policies.

Setting

An infinite horizon stochastic optimal control model (SM) is an eight-tuple $(S, C, U, W, p, f, \alpha, g)$. The state space $S$, the control space $C$ and the disturbance space $W$ are nonempty Borel spaces, that is, spaces homeomorphic to Borel subsets of complete separable metric spaces. The control constraint $U$ assigns to each state $x$ a nonempty set $U(x) \subseteq C$, and the set $\Gamma = \{(x,u) \mid u \in U(x)\}$ is analytic. The disturbance kernel $p(dw \mid x, u)$ is a Borel stochastic kernel and the system function $f : SCW \to S$ is Borel. The discount factor is $\alpha > 0$, and the one-stage cost $g : \Gamma \to [-\infty, \infty]$ is lower semianalytic: each sublevel set $\{g < c\}$ is analytic. The state moves by $x_{k+1} = f(x_k, u_k, w_k)$, with transition kernel $t(B \mid x, u) = p(\{w \mid f(x,u,w) \in B\} \mid x, u)$.

A policy $\pi = (\mu_0, \mu_1, \dots)$ chooses $u_k$ at random from a universally measurable stochastic kernel $\mu_k(du_k \mid x_0, u_0, \dots, x_k)$ concentrated on $U(x_k)$; $\Pi'$ is the set of all policies. A policy is Markov if each $\mu_k$ depends only on $x_k$, and it is stationary if, moreover, $\mu_k = \mu$ for all $k$. Writing $q_k(\pi, p_x)$ for the law of $(x_k, u_k)$ started from $x_0 = x$, the cost of $\pi$ and the optimal cost are

$$J_\pi(x) = \sum_{k=0}^\infty \alpha^k \int g\, dq_k(\pi, p_x), \qquad J^*(x) = \inf_{\pi \in \Pi'} J_\pi(x).$$

For $J : S \to [-\infty, \infty]$, the dynamic programming operators are

$$T(J)(x) = \inf_{u \in U(x)} \Big\{ g(x,u) + \alpha \int_S J(x')\, t(dx' \mid x, u) \Big\}, \qquad T_\mu(J)(x) = \int_C \Big[ g(x,u) + \alpha \int_S J\, dt \Big] \mu(du \mid x).$$

The three cases are (P) $g \ge 0$ on $\Gamma$; (N) $g \le 0$ on $\Gamma$; (D) $\alpha < 1$ and $|g| \le b$ on $\Gamma$ for some real $b$.

Formalization targets

Goal: the optimality equation (Proposition 9.8, Eq. (22))

Under each of (P), (N) and (D),

$$J^* = T(J^*).$$

Milestones

• $J^*$ is lower semianalytic (Corollary 9.4.1).
• For a stationary policy, $J_\mu = T_\mu(J_\mu)$ (Proposition 9.9).
• Optimality tests for stationary policies: under (P) or (D), $(\mu, \mu, \dots)$ is optimal iff $J^* = T_\mu(J^*)$ (Proposition 9.12); under (N) or (D), iff $J_\mu = T(J_\mu)$ (Proposition 9.13).
• Under (N) or (D), value iteration from $0$ converges to $J^*$, and under (D) it converges uniformly from every bounded lower semianalytic start (Proposition 9.14).

Further statements of the mission

• Markov policies suffice: at each state some Markov policy matches any policy's cost (Proposition 9.1), so $J^* = \inf_{\pi \in \Pi} J_\pi$ (Corollary 9.1.1).
• Partial converses of the optimality equation: $J \ge T(J)$, $J \ge 0$ gives $J \ge J^*$ under (P); $J \le T(J)$, $J \le 0$ gives $J \le J^*$ under (N); a bounded solution of $J = T(J)$ equals $J^*$ under (D) (Proposition 9.10). The analogous statements for $T_\mu$ and $J_\mu$ (Proposition 9.11).

Significance

The optimality equation is the basic structural fact of infinite horizon control. Corollary 9.12.1 uses it to construct optimal stationary policies from minimizers in the equation. The existence results for $\varepsilon$-optimal policies (Propositions 9.19 and 9.20), the convergence analysis of value iteration in Section 9.5, and the reduction of imperfect state information problems in Chapter 10 all build on it. It holds for arbitrary Borel models, with no continuity or compactness assumption.

All results of the mission were proved in 1978. None of them has a machine-checked proof: Mathlib has stochastic kernels and the Ionescu-Tulcea construction for measurable kernels, but no theory of lower semianalytic functions, universally measurable kernels, or dynamic programming on Borel spaces. A formal development would fix the measurability bookkeeping on which the textbook proofs rest and supply a reusable substrate for the stochastic control papers that cite this book.

Difficulty

Under (D), $T$ is a contraction on bounded functions, and its fixed point is the limit of value iteration. That argument, however, gives a fixed point only within a fixed class of measurable functions. Showing that this fixed point equals $J^*$ requires knowing that $J^*$ belongs to the class and that history-dependent randomized policies do no better. Under (P), value iteration can converge to the wrong limit (Example 1 of the chapter: $\lim_k J_k(0) = 0$ while $J^*(0) = \infty$). Even when each $J_k$ is Borel, $J^*$ may fail to be (Example 2). So $J^* = T(J^*)$ cannot be obtained as a limit of the finite horizon equations, and the natural class of Borel functions is not closed under the partial minimization that defines $T$.

The book's route lifts (SM) to a deterministic model on the space of probability measures $P(S)$, where no measurability restriction is needed, and transfers the results back. Making this transfer rigorous requires that the cost of a randomized policy be a measurable functional of its law, and that the infimum over policies preserve lower semianalyticity.

Formalization scope

The draft fixes the following conventions.

• Spaces. Borel spaces are topological spaces homeomorphic to Borel subsets of complete separable metric spaces, carrying their Borel $\sigma$-algebras. Analytic sets are Mathlib's AnalyticSet. A set is universally measurable if it is null-measurable for every probability measure.
• Extended reals. Values lie in EReal. The book's convention $\infty - \infty = -\infty + \infty = \infty$ is implemented explicitly, because Mathlib's EReal sets $\bot + \top = \bot$. The integral of an extended-real function is $\int f^+ - \int f^-$ with the same convention.
• Policies. These are sequences of universally measurable stochastic kernels on the history spaces $S_0C_0 \cdots S_k$, charging $U(x_k)$ with mass one. The laws of $(x_0, u_0, \dots, x_k, u_k)$ are built recursively from the kernels.
• Costs. $J_\pi$ is the series $\sum_k \alpha^k \int g\, dq_k$, computed as the difference of the series of positive and negative parts. Under each of (P), (N), (D) it coincides with the integral of the total discounted cost. $J^*$ is the infimum over all policies.
• Case labels. Each statement carries the case labels the book attaches to it, as hypotheses on the model.
• Scope. Only the (SM) statements are formalized. The deterministic model (DM) on $P(S)$ is the book's proof device and enters no statement.

The goal admits a trivializing formalization that this draft rules out. $J^*$ is not defined as a fixed point of $T$, nor as the limit of $T^k(0)$; it is the infimum of the costs of all policies, which under (P) can differ from that limit.

A complete development needs universally measurable kernels and their compositions on product spaces, measurability of $x \mapsto \int f(x, y)\, q(dy \mid x)$ for universally measurable integrands, the measurable selection theorem of Jankov and von Neumann, and the closure of lower semianalytic functions under partial infimum. These are the subject of the series' mission on Chapter 7, and they are reusable for any stochastic control model on Borel spaces. Contributions are welcome at any level: these foundations, the Markov reduction (Proposition 9.1), or the case-by-case arguments.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996. Chapter 9. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, Discounted dynamic programming, Annals of Mathematical Statistics 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
• R. E. Strauch, Negative dynamic programming, Annals of Mathematical Statistics 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
• S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Mathematics of Operations Research 4 (1979), 15–30. https://doi.org/10.1287/moor.4.1.15

Motivation

Finite-horizon stochastic control on general state and control spaces — inventory levels, queue lengths, positions, beliefs — cannot be written down without measure theory, and the measure theory turns out to be the hard part. The dynamic programming (DP) recursion "start from zero and minimise one stage at a time" is easy to state, but on uncountable spaces the minimisation in each step produces functions that need not be Borel-measurable, and the infimum over policies has to be taken over a class large enough to contain near-minimisers. Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978; Athena reprint 1996) resolved this by working with universally measurable policies and lower semianalytic costs. Chapter 8 is the finite-horizon core of that theory, and the infinite-horizon results of Chapter 9 and the imperfect-information reduction of Chapter 10 are built on it.

Timeline. Blackwell (1965) treated discounted problems on Borel spaces with bounded costs and Borel policies, where ε-optimal Borel policies may fail to exist. Strauch (1966) studied positive and negative models. Blackwell, Freedman and Orkin (1974) introduced analytic sets and analytically measurable policies into DP. Bertsekas and Shreve (1978, Chapters 7–8) gave the universally measurable finite-horizon theory formalized here, including the unbounded-cost assumptions (F⁺)/(F⁻).

Setting

A finite horizon stochastic optimal control model is a nine-tuple $(S,C,U,W,p,f,\alpha,g,N)$. The state space $S$, control space $C$ and disturbance space $W$ are nonempty Borel spaces (topological spaces homeomorphic to Borel subsets of complete separable metric spaces). The constraint $U(x)\subseteq C$ is nonempty and $\Gamma=\{(x,u)\mid u\in U(x)\}$ is analytic in $S\times C$. Disturbances are drawn from a Borel stochastic kernel $p(dw\mid x,u)$, the system moves by $x_{k+1}=f(x_k,u_k,w_k)$ with $f$ Borel, the discount factor $\alpha$ is a positive real, the one-stage cost $g:\Gamma\to[-\infty,\infty]$ is lower semianalytic ($\{g<c\}$ is analytic for every real $c$), and $N\ge1$ is the horizon. The state transition kernel is $t(B\mid x,u)=p(\{w\mid f(x,u,w)\in B\}\mid x,u)$.

A set is universally measurable if it is measurable for the completion of the Borel σ-algebra under every probability measure. A policy $\pi=(\mu_0,\dots,\mu_{N-1})$ chooses $u_k$ from a universally measurable stochastic kernel $\mu_k(du_k\mid x_0,u_0,\dots,x_k)$ concentrated on $U(x_k)$; it is Markov if $\mu_k$ depends on $x_k$ only, and nonrandomized if every $\mu_k(\cdot\mid\cdot)$ is a point mass. $\Pi'$ denotes all policies and $\Pi$ the Markov ones. A policy and an initial distribution $p$ determine a probability measure $r_N(\pi,p)$ on state–control paths, and the $K$-stage cost and optimal cost are

$$J_{K,\pi}(x)=\int\Big[\sum_{k=0}^{K-1}\alpha^k g(x_k,u_k)\Big]dr_N(\pi,p_x),\qquad J^*_K(x)=\inf_{\pi\in\Pi'}J_{K,\pi}(x).$$

Assumption (F⁺) requires $\int g^-\,dq_k(\pi,p_x)<\infty$, and (F⁻) requires $\int g^+\,dq_k(\pi,p_x)<\infty$, for every policy, initial state and stage, where $q_k$ is the marginal of $r_N$ on the $k$-th pair. The DP operators are

$$T_\mu(J)(x)=\int_C\Big[g(x,u)+\alpha\!\int_S J\,dt(\cdot\mid x,u)\Big]\mu(du\mid x),\qquad T(J)(x)=\inf_{u\in U(x)}\Big\{g(x,u)+\alpha\!\int_S J\,dt(\cdot\mid x,u)\Big\}.$$

Formalization targets

Goal: Proposition 8.2

$$J^*_K=T^K(J_0),\qquad K=1,\dots,N,$$

under (F⁺) or (F⁻), where $J_0\equiv0$. The goal leaves the horizon, the discount factor and the sign of $g$ unrestricted beyond (F⁺)/(F⁻), and it compares an infimum over all history-dependent randomized policies with a pointwise recursion.

Milestones

In attack order: Lemma 8.1 (the cost of a Markov policy equals $T_{\mu_0}\cdots T_{\mu_{K-1}}(J_0)$), Proposition 8.1 and Corollary 8.1.1 (Markov policies suffice), Lemma 8.2 (an ε-optimal universally measurable kernel for one application of $T$), Lemma 8.3 (under (F⁺), $T^K(J_0)>-\infty$), Lemma 8.4 (monotone and bounded convergence for $T_\mu$). Two consequences of the goal complete the chapter's existence theory: Corollary 8.2.1 ($J^*_K$ is lower semianalytic) and Proposition 8.3 (ε-optimal nonrandomized Markov policies under (F⁺); nonrandomized semi-Markov and randomized Markov ones under (F⁻)).

Significance

Proposition 8.2 says the DP algorithm computes the true optimal cost of the Borel model, with no restriction to Markov or nonrandomized policies and with costs that may be unbounded in either direction. Corollary 8.2.1 identifies the regularity of the value function — lower semianalytic, possibly not Borel (Example 1 of Chapter 8) — and Proposition 8.3 turns the recursion into near-optimal policies. These results are the base case for the infinite-horizon theory of Chapter 9 (positive, negative and discounted models are analysed as limits of finite-horizon problems) and for the sufficient-statistic reduction of Chapter 10.

All results here are proved in the book. None is formalized: the platform has finite-state, finite-action DP theorems and Borel models with Borel-measurable policies, but no universally measurable policies, no lower semianalytic costs and no Ionescu-Tulcea construction for universally measurable kernels. The mission poses the finite-horizon Borel theory, with reusable infrastructure: the universal σ-algebra, universally measurable kernels, iterated path integrals representing integration against the induced path measure, and the operator calculus on extended-real functions with the convention $\infty-\infty=\infty$.

Difficulty

The obvious argument fails at measurability. On countable spaces, Proposition 8.2 follows from the Part I argument: induct on $K$, choose near-minimising controls state by state, assemble them into a policy. On Borel spaces, a pointwise choice of near-minimisers is not a policy unless it is measurable, and $T(J)$ is generally not Borel even when $J$ and $g$ are; Borel policies are too few for $\varepsilon$-optimal ones to exist. The book's way out needs the selection theorem for lower semianalytic functions (Proposition 7.50), integration of universally measurable functions against universally measurable kernels (Propositions 7.45–7.46), and care with infinite values: without (F⁺) or (F⁻), the integral of the stage sum and the sum of the stage integrals can disagree, and Lemma 8.1 fails.

Formalization scope

Lean conventions:

• Spaces carry [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [IsBorelSpace X] [Nonempty X]. IsBorelSpace is the book's Definition 7.7.
• Extended reals are EReal. Addition inside costs and integrands uses the book's convention $-\infty+\infty=+\infty$ (badd), not Mathlib's, which gives $\bot+\top=\bot$. Integrals are $\int f^+-\int f^-$ with $\infty-\infty=\infty$ (extInt).
• The universal σ-algebra is the intersection of all completions (universalSigma). Kernels are universally measurable in the sense of Lemma 7.28(b).
• The integral against $r_N(\pi,p)$ is the iterated integral of Eq. (4) of Chapter 8 (pathInt).
• Stages are indexed $0,\dots,N-1$, and a history is $k$ state–control pairs plus the current state.
• $g$ is stored on $S\times C$, but only its values on $\Gamma$ are constrained or used.

A trivializing formalization is excluded by construction. $J^*_K$ is the infimum over all policies in $\Pi'$, not over Markov or nonrandomized ones. $J_{K,\pi}$ is the integral of the stage sum against the path measure, never the operator composition of Lemma 8.1, so the goal does not collapse to the Part I result.

A complete development needs:

• the analytic-set and universal-measurability theory of §7.6–7.7: closure of analytic sets under projections and sections, measurability of integrals against universally measurable kernels (Proposition 7.46), and the selection theorem (Proposition 7.50);
• extended-real integration lemmas in the style of Lemma 7.11.

This infrastructure is reusable for the infinite-horizon Borel models (Chapter 9), for the imperfect-information reduction (Chapter 10), and for papers that cite this book. Contributions of these supporting lemmas as separate theorems are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996, Chapter 8. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
• R. E. Strauch, Negative dynamic programming, Ann. Math. Statist. 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
• D. Blackwell, D. Freedman and M. Orkin, The optimal reward operator in dynamic programming, Ann. Probab. 2 (1974), 926–941. https://doi.org/10.1214/aop/1176996558
• S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Math. Oper. Res. 4 (1979), 15–30. https://doi.org/10.1287/moor.4.1.15

Motivation

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

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

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

Setting

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: consistency under sampling (Theorem 7.1)

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

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

Milestones

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

Periodic-review inventory control with backorders is one of the basic models of operations research: in each period a manager decides how much to order, orders arrive after a lead time, unmet demand is backlogged at a penalty, and stock left over is charged a holding cost. When demands in different periods are independent, dynamic programming yields an optimal base-stock policy and computing it is tractable. In practice demands are correlated and forecasts evolve over time, for example under the martingale model of forecast evolution (Heath and Jackson, 1994, doi:10.1080/07408179408966604). The dynamic program then has to range over all possible information states, whose number is typically exponential in the input (Zipkin, 2000), so optimal policies are out of reach and the heuristics in use came without performance guarantees.

Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2):284–302, 2007) gave the first policy for this model with a worst-case guarantee that holds for arbitrary correlated, nonstationary demand distributions: the dual-balancing policy costs at most twice the optimum in expectation. The analysis rests on a marginal cost accounting that charges each order, at the time it is placed, all the holding cost its units will ever incur. This mission formalizes that guarantee.

Setting

There are $T$ periods $t = 1, \dots, T$ and a known lead time $L \ge 0$: an order placed in period $t$ arrives in period $t + L$. Period $t$ has a per-unit holding cost $h_t \ge 0$ and a per-unit backlogging penalty $p_t \ge 0$. Ordering costs are zero ($c_t = 0$), which is the standing assumption of the paper's §4. The initial data are the net inventory $ni_0$ and the pipeline orders $q_{1-L}, \dots, q_0 \ge 0$.

Demands $D_1, \dots, D_T$ are nonnegative random variables on a probability space with a filtration $(\mathcal F_t)$; $\mathcal F_t$ is the information at the beginning of period $t$, and $D_t$ is $\mathcal F_{t+1}$-measurable. A feasible policy $P$ places orders $Q^P_t \ge 0$ that are $\mathcal F_t$-measurable. Write $D_{[s,t]} = \sum_{j=s}^t D_j$ (with $D_j = 0$ for $j \le 0$), $X_t = ni_0 + \sum_{j=1-L}^{t-1} Q_j - D_{[1,t-1]}$ for the inventory position before ordering and $Y_t = X_t + Q_t$ after ordering.

The marginal holding cost of period $t$ is the holding cost that the units ordered in $t$ incur until the end of the horizon, and the marginal backlogging cost is the penalty incurred one lead time later:

$$H^P_t = \sum_{j=t+L}^{T} h_j\,\bigl(Q^P_t - (D_{[t,j]} - X^P_t)^+\bigr)^+, \qquad \Pi^P_t = p_{t+L}\,\bigl(D_{[t,t+L]} - Y^P_t\bigr)^+ .$$

The cost of $P$ is $\mathcal C(P) = \sum_{t=1}^{T-L}(H^P_t + \Pi^P_t)$; by Eq. (3) it differs from the total holding and backlogging cost only by a policy-independent nonnegative term.

A dual-balancing policy $B$ orders nothing after period $T - L$, and in each period $t \le T - L$ orders the quantity that balances the two conditional expected marginal costs:

$$E\bigl[H^B_t \mid \mathcal F_t\bigr] = E\bigl[\Pi^B_t \mid \mathcal F_t\bigr] \quad\text{almost surely.}$$

Formalization targets

Goal: Theorem 4.1

For every dual-balancing policy $B$ and every feasible policy $P$,

$$E[\mathcal C(B)] \;\le\; 2\,E[\mathcal C(P)] .$$

The paper writes $P = OPT$; quantifying over all feasible $P$ is the same statement whenever an optimum exists and needs no existence assumption.

Milestones

1. Lemma 4.1. $E[\mathcal C(B)] = 2\sum_{t=1}^{T-L}E[Z_t]$ with $Z_t = E[H^B_t \mid \mathcal F_t]$.
2. Lemma 4.2. With $\mathcal T_H = \{t : Y^B_t < Y^P_t\}$, $\sum_{t\in\mathcal T_H} H^B_t \le \sum_{t=1}^{T-L} H^P_t$ on every realization.
3. Lemma 4.3. With $\mathcal T_\Pi = \{t : Y^B_t \ge Y^P_t\}$, $\sum_{t\in\mathcal T_\Pi} \Pi^B_t \le \sum_{t=1}^{T-L} \Pi^P_t$ on every realization.

Two further items are not milestones. Eq. (3) states that, along every realization, the period-by-period holding and backlogging cost equals $\sum_{t=1-L}^{0}\Pi_t + H_{(-\infty,0]} + \sum_{t=1}^{T-L}(H_t + \Pi_t)$, which is why the cost of Eq. (4) is the right objective. The other states that a dual-balancing policy exists when $h_T > 0$ and the demands are integrable, so the goal is not about an empty class.

Significance

The theorem gives a policy that is computable period by period, by a one-dimensional search, with a factor-two guarantee that holds for every joint demand distribution, including correlated, nonstationary and forecast-driven ones, where the optimal policy cannot be computed. The constant is tight: the paper exhibits instances where the ratio tends to two. The second mission of this series treats the stochastic lot-sizing problem of the same paper, which uses the same marginal cost accounting.

The result is proved in the paper; no machine-checked proof of it is known. Formalizing it produces a reusable model of the periodic-review backlogging system with lead times and adapted policies, a verified marginal cost identity, and a formal approximation guarantee for a stochastic inventory policy. The pathwise comparison lemmas are stated for arbitrary pairs of order sequences and so apply to other balancing-type policies.

Difficulty

The obvious attempt compares the two policies period by period. That fails: in a given period the dual-balancing policy may hold far more or far less inventory than the comparison policy, and neither the holding nor the backlogging cost of one period is bounded by the comparator's cost in that period. The comparison only works after re-charging holding costs to the period in which the units were ordered, which requires the identity Eq. (3) to be established exactly, including the pipeline units, the initial stock and the lead-time shift. The probabilistic step then needs the random index sets $\mathcal T_H$ and $\mathcal T_\Pi$ to be determined by the information of period $t$, so that conditioning on $\mathcal F_t$ commutes with the indicators; this is where the nonanticipativity of both policies enters. The existence of a balancing quantity needs a measurable selection from conditional laws, and it fails without a positive late holding cost.

Formalization scope

• Periods are integers (ℤ). Orders and demands are functions ℤ → Ω → ℝ; only periods $1, \dots, T$ are read, and the pipeline $q_t$ is substituted for $t \le 0$.
• Ordering costs are $c_t = 0$ and there is no discounting, as in the paper's §4; the reduction of §4.6 from general instances is not formalized. The lead time $L$ is general.
• Information is an arbitrary Filtration ℤ to which demands are adapted with a one-period lag; the paper's information vectors are a special case, and randomized policies are covered when their randomness is part of the information.
• Expected costs are lower Lebesgue integrals in $[0,\infty]$, so an infinite expected cost is never read as $0$.
• The balancing condition carries integrability of $H^B_t$ and $\Pi^B_t$, so a conditional expectation of a non-integrable cost (which Mathlib sets to $0$) cannot satisfy it vacuously. The existence item rules out an empty policy class.
• Lemmas 4.2 and 4.3 are pathwise and do not use the balancing rule. The comparator totals are the marginal totals of Eq. (4), which is the stronger reading.
• Eq. (2) prints $X_{t+L}$ and its restatement on p. 292 prints $p_t$; both are typos, and the formalization uses $X_t$ and $p_{t+L}$.

A complete development needs finite-sum manipulations for Eq. (3) and Lemma 4.2, conditional expectation (tower property, pulling out bounded $\mathcal F_t$-measurable factors) for Lemma 4.1 and the goal, and regular conditional distributions with a measurable selection for the existence item. Theorem 4.2 (the randomized policy for integer demands) is outside this mission.

Selected references

• R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2):284–302, 2007. doi:10.1287/moor.1060.0205
• D. C. Heath, P. L. Jackson, Modeling the evolution of demand forecasts with application to safety stock analysis in production/distribution systems, IIE Transactions 26(3):17–30, 1994. doi:10.1080/07408179408966604
• P. H. Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000. ISBN 978-0-256-11379-7.

Motivation

The bullwhip effect is the observation that the variability of orders grows as one moves up a supply chain, from the retailer to the wholesaler, the distributor and the factory, even when customer demand is stable. It was documented in industry practice by Lee, Padmanabhan and Whang (Management Science, 1997), who identified demand forecasting as one of its main causes. Amplified order variability raises the safety stock, capacity and transportation costs of every upstream firm, so the question of how large the effect is, and what reduces it, is central to supply chain management.

Chen, Drezner, Ryan and Simchi-Levi (Management Science 46(3), 2000) quantified the effect for a retailer that forecasts with a moving average and follows an order-up-to policy. Their §3 asks whether sharing customer demand information with every stage removes the effect. Theorem 3.1 (the companion mission of this series) shows that it does not; Theorem 3.2, the goal of this mission, gives the lower bound for the chain in which no demand information is shared.

Setting

Time is indexed by the integers $t \in \mathbb Z$. The retailer faces i.i.d. demand

$$D_t = \mu + \epsilon_t,$$

where the error terms $\epsilon_t$ are independent and identically distributed from a symmetric distribution with mean $0$ and variance $\sigma^2 > 0$.

Single-stage policy (§2). With $p \ge 1$ observations, a lead time $L$, a safety factor $z$ and a constant $C_{L,\rho}$, the retailer forms the moving-average estimates

$$\hat D^L_t = L\,\frac{\sum_{i=1}^p D_{t-i}}{p}, \qquad \hat\sigma^L_{et} = C_{L,\rho}\sqrt{\frac{\sum_{i=1}^p e_{t-i}^2}{p}}, \qquad e_t = D_t - \hat D^1_t,$$

raises its inventory position to the order-up-to point $y_t = \hat D^L_t + z\hat\sigma^L_{et}$, and so orders $q_t = y_t - y_{t-1} + D_{t-1}$. Orders may be negative: excess inventory is returned without cost.

Decentralized chain (§3). Stages $k = 1, 2, \dots$ form a serial chain; stage 1 is the retailer, and $L_k$ is the lead time between stages $k$ and $k+1$. No stage sees customer demand except the retailer. Stage $k$ forecasts from the orders it receives,

$$\hat D^{(1)}_t = \frac{\sum_{i=1}^p D_{t-i}}{p}, \qquad \hat D^{(k)}_t = \frac{\sum_{j=0}^{p-1} q^{k-1}_{t-j}}{p} \quad (k \ge 2),$$

uses the order-up-to point $y^k_t = L_k\hat D^{(k)}_t$, and orders

$$q^1_t = y^1_t - y^1_{t-1} + D_{t-1}, \qquad q^k_t = y^k_t - y^k_{t-1} + q^{k-1}_t \quad (k \ge 2).$$

Formalization targets

Goal: Theorem 3.2 (Eq. (7))

For every stage $k \ge 1$ and every period $t$,

$$\frac{\operatorname{Var}(q^k_t)}{\operatorname{Var}(D_t)} \;\ge\; \prod_{i=1}^{k}\left(1 + \frac{2L_i}{p} + \frac{2L_i^2}{p^2}\right).$$

The bound is the paper's, with its explicit constants. The paper asserts no tightness for this theorem, and none is claimed.

Milestone: Eq. (6)

For the single-stage policy with any safety factor $z$ and any constant $C_{L,\rho}$,

$$\frac{\operatorname{Var}(q_t)}{\operatorname{Var}(D_t)} \;\ge\; 1 + \frac{2L}{p} + \frac{2L^2}{p^2}.$$

This is the i.i.d. case $\rho = 0$ of the paper's Theorem 2.2. With $z = 0$ and $L = L_1$ the single-stage orders are the stage-1 orders of the chain, so Eq. (6) contains the case $k = 1$ of the goal.

Significance

The result. Theorem 3.2 is half of the paper's comparison between centralized and decentralized information. When demand information is shared, the amplification from the retailer to stage $k$ in the i.i.d. case equals $1 + 2(\sum_{i\le k}L_i)/p + 2(\sum_{i\le k}L_i)^2/p^2$ (Eq. (8)), which grows additively in the lead times. Without sharing, the lower bound (7) is a product over stages and grows multiplicatively. The paper concludes that centralizing demand information "can significantly reduce the bullwhip effect", and that the gap widens as one moves up the chain. Eq. (6) is the single-stage statement that forecasting with a moving average alone already amplifies variability, by a factor depending only on the ratio $L/p$.

Formalizing it. The paper gives no proof of Theorem 3.2; it refers to Ryan (1997, PhD thesis) and to Chen et al. (1998). A machine-checked proof would therefore supply the first self-contained, verified argument for the multiplicative bound. The Gaussian special case of Eq. (6) is already formalized on Prove2Me, in the Snyder–Shen chapter on the bullwhip effect (SupplyChainTheory.bullwhip_signal_processing at $\rho = 0$); that statement assumes Gaussian errors, whereas this mission assumes only symmetry, mean $0$ and variance $\sigma^2$. Neither the multistage bound nor the symmetric-error version of Eq. (6) has a formal proof.

Difficulty

The natural first idea is induction on the stage: treat the orders of stage $k-1$ as the demand of stage $k$ and apply the single-stage bound. That step fails, because the single-stage bound is a statement about i.i.d. demand, and the orders reaching stage $k \ge 2$ are not i.i.d.: they are autocorrelated, and stage $k$'s moving average of those orders interacts with the correlation in a way that can raise or lower the variance. Whether the product bound survives depends on controlling that interaction at every stage. For Eq. (6), the safety-stock term $z\hat\sigma^L_{et}$ is a nonlinear function of the demands, and only symmetry of the errors, not normality, is available to control its interaction with the linear part of the order.

Formalization scope

All objects live in the namespace ChenBullwhip.Decentralized.

• IIDDemand P is the demand model on a probability space $(\Omega, P)$: a constant mu, sigma > 0, and errors eps : ℤ → Ω → ℝ that are measurable, mutually independent (iIndepFun), identically distributed, symmetric (eps t and -eps t have the same law), in $L^2$, with mean $0$ and variance sigma ^ 2. Demand is D t = mu + eps t. Variances are Mathlib's ProbabilityTheory.variance.
• SingleStage defines $\hat D^L_t$, $e_t$, $\hat\sigma^L_{et}$, $y_t$ and $q_t$ of §2; $C_{L,\rho}$ is a free real parameter, as the paper does not fix it.
• Chain defines the forecasts $\hat D^{(k)}_t$ and the orders $q^k_t$ by recursion on the stage, with the convention $q^0_t = D_{t-1}$, so that stage 1 orders $y^1_t - y^1_{t-1} + D_{t-1}$. The recursion $q^k_t = y^k_t - y^k_{t-1} + q^{k-1}_t$ is not printed in the paper; it is the §2.2 order identity applied to a stage whose incoming demand is $q^{k-1}_t$, as the sequence of events on p. 440 describes.

Disclosed hypotheses not on the page: $p \ge 1$ (a moving average needs an observation), $\sigma > 0$ (the paper divides by $\operatorname{Var}(D) = \sigma^2$), and square-integrable errors (Mathlib's variance is $0$ off $L^2$). The paper's model (1) asks $\mu \ge 0$; since $\mu$ affects no variance, no sign condition is imposed. Lead times are natural numbers. The statements hold in every period $t$, with no stationarity hypothesis.

Trivializing formalizations are excluded: the orders are computed from the demands, not posited processes with a given covariance; the variances are genuine because every random variable involved is square integrable; and the ratio's denominator is $\sigma^2 > 0$.

A complete development needs variance and covariance calculus for finite linear combinations of independent $L^2$ variables, and, for Eq. (6), the vanishing of the covariance between an odd and an even function of a symmetric random vector. Both are reusable well beyond this mission. Proofs of either target, and general lemmas on variances of linear filters of i.i.d. sequences, are welcome.

Selected references

• F. Chen, Z. Drezner, J. K. Ryan, D. Simchi-Levi, Quantifying the Bullwhip Effect in a Simple Supply Chain: The Impact of Forecasting, Lead Times, and Information, Management Science 46(3):436–443, 2000. https://doi.org/10.1287/mnsc.46.3.436.12069
• H. L. Lee, V. Padmanabhan, S. Whang, Information Distortion in a Supply Chain: The Bullwhip Effect, Management Science 43(4):546–558, 1997. https://doi.org/10.1287/mnsc.43.4.546
• J. K. Ryan, Analysis of Inventory Models with Limited Demand Information, Ph.D. dissertation, Department of Industrial Engineering and Management Science, Northwestern University, 1997.
• L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 13 (formalized on Prove2Me as SupplyChainTheory.*).

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

the mean number of arrivals per service.

Formalization targets

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

A call center has to decide how many agents to staff. In practice the decision is often posed as a service-level constraint rather than a cost trade-off: use the fewest agents for which the expected waiting cost, or the fraction of customers who wait, stays below a target. Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; journal version in Operations Research 52(1), 2004, doi:10.1287/opre.1030.0081) treat this constraint problem in Section 8 of their paper, alongside the cost-minimization problem of Sections 5–7, and show that a simple square-root staffing rule solves it asymptotically as the arrival rate grows.

The rule matters because it is what practitioners use. Under the classical Erlang-C model, the exact optimum requires evaluating the Erlang-C formula over many staffing levels. The asymptotic rule replaces this with a single equation in the Halfin–Whitt function $P$: when the target is a delay probability $\varepsilon$ (Example 8.5 of the paper), it reduces to staffing $\lambda/\mu + P^{-1}(\varepsilon)\sqrt{\lambda/\mu}$ servers.

Timeline. Erlang's formula for the M/M/N delay probability dates from 1917. Halfin and Whitt (Operations Research 29, 1981) identified the limit $P(x)$ of the delay probability under square-root staffing $N = \lambda/\mu + x\sqrt{\lambda/\mu}$ with integer $N$. Jagers and Van Doorn (Operations Research Letters 5, 1986; SIAM Review 33, 1991) studied the continued Erlang loss and delay functions at non-integer numbers of servers, including their convexity, which is what lets the staffing problem be relaxed to a continuous one. Borst, Mandelbaum and Reiman (2000/2004) used these to prove asymptotic optimality of square-root rules for both the cost and the constraint formulations.

Setting

Customers arrive at rate $\lambda$ to $N$ identical servers, each with service rate $\mu > 0$; $\mu$ is fixed while $\lambda \to \infty$. Stability requires $N > \lambda/\mu$. A customer who waits $t$ time units costs $D_\lambda(t)$, where $D_\lambda(0) = 0$, $D_\lambda$ is strictly increasing on $[0,\infty)$ and $\int_0^\infty D_\lambda(t)e^{-\theta t}\,dt < \infty$ for all $\theta > 0$.

The Erlang-C probability of waiting is

$$\pi(N,\nu) = \frac{\nu^N}{N!}\Big\{(1-\nu/N)\sum_{n=0}^{N-1}\frac{\nu^n}{n!} + \frac{\nu^N}{N!}\Big\}^{-1},$$

and the conditional waiting cost is $G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt$. The waiting cost per unit time with $N$ servers is

$$K(N,\lambda) = \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda).$$

Given a target $M_\lambda > 0$, the optimal staffing level is the least integer $N > \lambda/\mu$ with $K(N,\lambda) \le M_\lambda$; call it $N^*_\lambda$.

In the continuous parametrization $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$, define $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$, the continuous Erlang-C function $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$ with $H(M,\alpha) = \{\alpha\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt\}^{-1}$, and $K_\lambda(x) = \pi_\lambda(x)G_\lambda(x)$. The Halfin–Whitt function is $P(x) = 1/(1 + x/h(-x))$ with $h = \phi/(1-\Phi)$ the standard normal hazard rate. A staffing function $x_\lambda > 0$ is judged by the rounding gap

$$T_\lambda(x) = \min\big\{|K(\lfloor N_\lambda(x)\rfloor,\lambda) - M_\lambda|,\ |K(\lceil N_\lambda(x)\rceil,\lambda) - M_\lambda|,\ |K(\lceil N_\lambda(x)\rceil,\lambda) - K(N^*_\lambda,\lambda)|\big\}.$$

It is asymptotically optimal when $T_\lambda(x_\lambda)/M_\lambda \to 0$ as $\lambda\to\infty$.

Formalization targets

Goal: Theorem 8.2 (rationalized regime)

Suppose that for some $\kappa > 0$ and $\gamma \in (0,\infty)$, $G_\lambda(\kappa)/M_\lambda \to \gamma$, i.e. the waiting cost is comparable to the target. Let $y^*_\lambda > 0$ solve $P(y)G_\lambda(y) = M_\lambda$. Then

$$\lim_{\lambda\to\infty}\frac{T_\lambda(y^*_\lambda)}{M_\lambda} = 0.$$

Supporting milestones

• Lemma C.1: $G_\lambda$ is strictly convex and decreasing on $(0,\infty)$.
• Section 3: $\pi_\lambda(x) = \pi(N_\lambda(x),\lambda/\mu)$ when $N_\lambda(x)$ is an integer.
• Lemma 8.1: if $z^*_\lambda > 0$ solves $\hat\pi_\lambda(z)\hat G_\lambda(z) = M_\lambda$ and $K_\lambda(z^*_\lambda)/(\hat\pi_\lambda\hat G_\lambda)(z^*_\lambda) \to 1$, then $T_\lambda(z^*_\lambda)/M_\lambda \to 0$.
• Lemma B.1: $P$ is strictly convex and decreasing on $(0,\infty)$.
• Eq. (17): $\limsup a_\lambda/b = \infty$ implies $\liminf P(a_\lambda)/P(b) = 0$ and $\liminf \pi_\lambda(a_\lambda)/\pi_\lambda(b) = 0$.
• Lemma 4.1 (Halfin–Whitt): for bounded $x_\lambda > 0$, $\pi_\lambda(x_\lambda)/P(x_\lambda) \to 1$; with $x_\lambda \to x$, $\pi_\lambda(x_\lambda)/P(x)\to 1$.

Further target: Theorem 8.6 (efficiency-driven regime)

If $G_\lambda(\kappa)/M_\lambda \to 0$ for every $\kappa > 0$ and $y^*_\lambda > 0$ solves $G_\lambda(y) = M_\lambda$, then $T_\lambda(y^*_\lambda)/M_\lambda \to 0$.

Significance

The theorem certifies the staffing rule used in workforce-management practice: the excess staffing is determined by one scalar equation involving the Gaussian function $P$ and the scaled waiting cost, and rounding the resulting staffing level misses the constraint by a vanishing fraction of the target. Lemma 8.1 is a reusable framework: any approximation $\hat\pi_\lambda\hat G_\lambda$ that is asymptotically exact at the proposed staffing level yields an asymptotically optimal rule, and the paper instantiates it in three regimes (Theorems 8.2, 8.6, 8.9).

The results are proved on paper. To the best of current knowledge none of them, nor the Halfin–Whitt limit for the continuous Erlang-C extension, has a machine-checked proof. A formalization would produce the first verified heavy-traffic limit of the Erlang-C delay probability, a verified continuous Erlang-C extension with its integer identity, and the convexity facts about $P$ and $G_\lambda$ that many staffing papers cite without proof.

Difficulty

The obvious argument is to quote Halfin and Whitt: the delay probability converges to $P(x)$ under square-root staffing, so $P$ can replace the Erlang-C formula. That limit, as published in 1981, is about integer server counts along sequences with a convergent excess-staffing parameter. The paper needs it for the continuous function $H$ at non-integer server counts and for staffing functions that are merely bounded, and it also needs the identity $H(N,\nu) = \pi(N,\nu)$ at integers and the monotonicity of $\pi_\lambda$ in $x$, both cited from Jagers and Van Doorn rather than proved. None of these is in Mathlib. A second obstacle is that the staffing function $y^*_\lambda$ is defined only implicitly by an equation involving $G_\lambda$, which depends on the arbitrary cost functions $D_\lambda$; nothing a priori prevents it from escaping to infinity, outside the range where the Halfin–Whitt approximation applies. Finally, $T_\lambda$ compares integer-level costs given by the Erlang-C formula with a continuous approximation, so both representations of the delay probability are in play at once.

Formalization scope

The queue itself is not formalized: there is no Markov chain and no waiting-time distribution. Every statement is about the closed-form waiting cost $K(N,\lambda)$ with $\pi$ given by the Erlang-C formula, exactly as the paper's analysis is. Conventions, all in the namespace DimCallCenters.Constraint:

• lam : ℝ is the arrival rate (λ is a Lean keyword); limits are Filter.atTop in lam, with μ fixed. Objects indexed by λ ($M_\lambda$, $N^*_\lambda$, $y^*_\lambda$) are functions of lam constrained only for lam > 0.
• WaitModel packages μ > 0 and $D_\lambda$ with $D_\lambda(0) = 0$, strict monotonicity on $[0,\infty)$, and integrability of $D_\lambda(t)e^{-\theta t}$ on $(0,\infty)$ for θ > 0 (the paper's finiteness of $G$; integrability is required because Lean's integral of a non-integrable function is 0).
• $N^*_\lambda$ is a function Nstar : ℝ → ℕ given with its two defining properties (feasible; below every feasible integer level above λ/μ). $y^*_\lambda$ and $z^*_\lambda$ are any positive solutions of their equations; existence and uniqueness are not hypotheses.
• In $T_\lambda$ the round-down term is dropped when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$ (an unstable level where $K$ is undefined). This can only enlarge $T_\lambda$.
• Asymptotic relations are limits of ratios. $\limsup = \infty$ and $\liminf = 0$ are stated with ∃ᶠ ("frequently"), $\limsup < \infty$ as eventual boundedness.
• $P$ is defined through explicit $\phi$, $\Phi$, $h$; the formula also gives $P(0) = 1$, used in Lemma 4.1(2) at $x = 0$.
• No hypothesis $\lim_{N\downarrow\lambda/\mu}G(N,\lambda) = \infty$ is added: it is not needed for the statements here.

A trivializing formalization is ruled out: $T_\lambda$ keeps all of the paper's terms and is never replaced by a smaller quantity, and the hypotheses are jointly satisfiable — $D_\lambda(t) = a\sqrt{\lambda/\mu}\,t$ with $M_\lambda = M\lambda$ satisfies (33) for every $\kappa$ with $\gamma = a/(\mu\kappa M)$.

Infrastructure needed: the continuous Erlang-C function and its integer identity; the Halfin–Whitt limit (a Gaussian approximation of Poisson/gamma tails); calculus facts about the normal hazard rate. These are reusable beyond this mission, notably by the sibling missions on the cost-minimization problem. Example 8.5 (delay-probability target with $D_\lambda = 1_{t>0}$) motivates the rule but violates the strict monotonicity of $D_\lambda$, so it is not an instance of the theorem as stated. Contributions on any milestone, and on Theorem 8.9 (quality-driven regime, which needs Lemma 4.2), are welcome.

Selected references

• S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000; Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
• 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
• A. A. Jagers, E. A. Van Doorn, On the Continued Erlang Loss Function, Operations Research Letters 5:43–46, 1986.
• A. A. Jagers, E. A. Van Doorn, Convexity of Functions which are Generalizations of the Erlang Loss Function and the Erlang Delay Function, SIAM Review 33:281–282, 1991.