Probability

Motivation

In a multi-armed bandit problem a learner chooses one of $K$ actions in each of $n$ rounds and observes only the reward of the chosen action. Two models of the rewards have separate theories. In the stochastic model, each arm pays independent draws from a fixed distribution; algorithms such as UCB1 (Auer, Cesa-Bianchi & Fischer 2002) have regret of order $\sum_i \log(n)/\Delta_i$, logarithmic in $n$. In the adversarial model, an adversary chooses the rewards; Exp3 and its variants (Auer, Cesa-Bianchi, Freund & Schapire 2002) have regret of order $\sqrt{nK}$, which is optimal there. An algorithm tuned for one model fails in the other: stochastic algorithms can suffer linear regret against an adversary, and adversarial algorithms pay $\sqrt n$ even when the rewards are i.i.d.

Bubeck and Slivkins (arXiv:1202.4473, COLT 2012) asked whether one algorithm can be near-optimal in both models without knowing which one it faces. They answered yes with the algorithm SAO. This result started the "best of both worlds" line of work on bandits. Later contributions include EXP3++ (Seldin & Slivkins 2014) and Tsallis-INF (Zimmert & Seldin 2021).

Setting

There are $K\ge2$ arms and $n\ge K$ rounds. On round $t$ the algorithm draws an arm $I_t$ from a probability vector $p_t=(p_{1,t},\dots,p_{K,t})$ computed from the history it has observed. At the same time a reward vector $g_t\in[0,1]^K$ is fixed, and the algorithm observes only $g_{I_t,t}$.

• Adversarial model. The vector $g_t$ is chosen by an adaptive adversary: a function of the arms $I_1,\dots,I_{t-1}$ played earlier, but not of $I_t$. The regret is $R_n=\max_i\sum_{t=1}^n g_{i,t}-\sum_{t=1}^n g_{I_t,t}$.
• Stochastic model. There are distributions $\nu_1,\dots,\nu_K$ on $[0,1]$ with means $\mu_i$, and all $g_{i,t}\sim\nu_i$ are independent. The pseudo-regret is $\overline R_n=\sum_{t=1}^n(\max_i\mu_i-\mu_{I_t})$. The gap of arm $i$ is $\Delta_i=\max_j\mu_j-\mu_i$, and the minimal gap is $\Delta=\min_{i:\Delta_i>0}\Delta_i$.

The analysis uses importance-weighted estimates $\widetilde H_{i,t}=\frac1t\sum_{s\le t}g_{i,s}\mathbb 1_{\{I_s=i\}}/p_{i,s}$, the sample means $\widehat H_{i,t}$, the averages $H_{i,t}=\frac1t\sum_{s\le t}g_{i,s}$, and the play counts $T_i(t)$.

SAO (Algorithm 1 of the paper) takes a parameter $\beta>1$. It keeps a set of active arms, initially all arms, and samples them uniformly at first. On each round it applies a test, (12), that deactivates an arm whose estimate $\widetilde H_{i,t}$ falls far below the best active one. The probability of a deactivated arm then decays as $q_i\tau_i/t$, where $\tau_i$ is the deactivation time and $q_i$ the arm's probability at that moment. Three further tests, (13)–(15), check that the observations stay consistent with stochastic rewards. If any of them fails on round $\tau_0$, SAO switches permanently to the adversarial algorithm Exp3.P (Bubeck & Cesa-Bianchi 2012, Fig. 3.1) for the remaining rounds.

Formalization targets

Goal: Theorem 4.1, high-probability form

For every $\delta\in(0,1)$ let $\beta=10Kn^3\delta^{-1}$. With probability at least $1-\delta$, SAO with parameter $\beta$ satisfies, in the stochastic model (whenever some arm has $\Delta_i>0$),

$$\overline R_n\le\frac{260K(1+\log K)\log^2(\beta)}{\Delta},$$

and, against every adaptive adversary with rewards in $[0,1]$,

$$R_n\le60(1+\log K)(1+\log n)\sqrt{nK\log(\beta)+5K^2\log^2(\beta)}+200K^2\log^2(\beta).$$

Milestones

The milestones follow the paper's proof in order:

• Freedman's inequality (Theorem 4.3) in the paper's two-sided form, and its variance-adaptive form, Lemma 4.4.
• The concentration lemmas for SAO's estimates (Lemmas 4.5, 4.6, 4.7) and the Exp3.P phase (Lemma 4.8).
• The two good events of §4.1, (21)–(25).
• The deterministic consequences on those events: Exp3.P is never started in the stochastic model; suboptimal arms are deactivated by time $260K\log(\beta)/\Delta_i^2$; $\sum_iq_i\le1+\log K$, (27); and the adversarial regret bound of §4.3.
• The two halves of Theorem 4.1.

Significance

The theorem shows that the stochastic and adversarial regret rates are not in conflict. A single algorithm, with no information about the model, gets $O(K\log K\log^2(n/\delta)/\Delta)$ pseudo-regret on stochastic rewards and $\tilde O(\sqrt{nK})$ regret against adaptive adversaries. Each rate is within polylogarithmic factors of optimal for its model. Later algorithms improved the logarithmic factors and removed the explicit switching, but they are compared against this result.

The theorem is proved in the paper. It is not known to have a machine-checked proof. Formalizing it requires a precise model of an adaptive adversary interacting with a randomized algorithm, martingale concentration with random variance (Lemma 4.4), and an exact statement of SAO including its boundary cases. The pieces are reusable: the interaction model, the estimators, Exp3.P and its high-probability guarantee all apply to other adversarial bandit results.

Difficulty

Neither standard analysis carries over. In the stochastic model, SAO's sampling probabilities are random and depend on the past, and a deactivated arm's probability keeps changing. Hoeffding-type bounds for a fixed sampling scheme therefore do not apply to $\widetilde H_{i,t}$. The variance of the importance-weighted estimate grows like $\sum_s1/p_{i,s}$, which is controlled only through the algorithm's own schedule (16). This is why Lemma 4.5 has the two-part radius with $\max(t-\tau_i,0)/(q_i\tau_it)$. In the adversarial model, the deterministic argument has to show that whenever the consistency tests pass, the regret accumulated before the switch is already small, for an adversary that adapts to the arms played. A union bound over all quantities, all arms and all times (§4.1) is needed before any deterministic reasoning, so every constant in the event matters.

Formalization scope

All declarations live in the namespace BestBothWorlds.SAO.

• Arms and paths. Arms are Fin K and rounds are $1,\dots,n$. An arm path is Fin n → Fin K.
• Algorithms and adversaries. An algorithm is a deterministic map from the observed history to a probability vector. A deterministic adaptive adversary is a map from the list of earlier arms to a reward vector; randomized adversaries are mixtures of these.
• Probabilities. For a fixed adversary, the probability of an event is $\sum_{I\in E}\prod_tp_{I_t,t}$. In the stochastic model this is integrated against the product law of the reward table.
• Logarithms and constants. Real.log is the natural logarithm. All constants of Theorem 4.1 are explicit, with $\beta=10Kn^3\delta^{-1}$.
• SAO. It is defined exactly as Algorithm 1. Arms are tested in order within a round, and the active set changes during the loop. Test (13) is false when $T_i(t)=0$, and test (14) is false when $\tau_i=1$.
• Exp3.P. After the switch, Exp3.P runs from scratch for $n-\tau_0$ rounds. Its parameters are those of Bubeck–Cesa-Bianchi Theorem 3.2 with confidence $K/\beta$, and $\gamma$ and $\beta_{\mathrm P}$ are clipped at $1$.
• §4 notation. $\tau_0$, $\tau_i\leftarrow\min(\tau_i,\tau_0)$ and $q_i=p_{i,\min(\tau_i,\tau_0)}$ are computed from the run, never assumed.

A trivializing formalization is ruled out. The goal's hypotheses concern only the instance ($K$, $n$, $\delta$, the distributions or the adversary). The algorithm's quantities ($\tau_0$, $\tau_i$, $q_i$, the sampling probabilities) are computed by the definition of SAO and are never free variables or hypotheses. The adversarial half covers adaptive adversaries, not only oblivious reward tables.

The expectation form of Theorem 4.1 ($O(\cdot)$ bounds with $\beta=n^4$), Theorem 1.1 and the two-armed warm-up of §3 are out of scope. Proofs of any milestone are welcome, as are alternative proofs of the concentration lemmas from Mathlib's martingale library.

Selected references

• S. Bubeck and A. Slivkins, The best of both worlds: stochastic and adversarial bandits, COLT 2012; arXiv:1202.4473v1. https://arxiv.org/abs/1202.4473
• S. Bubeck and N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. https://doi.org/10.1561/2200000024
• D. A. Freedman, On tail probabilities for martingales, Annals of Probability 3(1), 1975. https://doi.org/10.1214/aop/1176996452
• P. Auer, N. Cesa-Bianchi and P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• P. Auer, N. Cesa-Bianchi, Y. Freund and R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• Y. Seldin and A. Slivkins, One practical algorithm for both stochastic and adversarial bandits, ICML 2014. https://proceedings.mlr.press/v32/seldinb14.html
• J. Zimmert and Y. Seldin, Tsallis-INF: an optimal algorithm for stochastic and adversarial bandits, JMLR 22, 2021. https://jmlr.org/papers/v22/19-753.html

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

Temporal-difference learning estimates the value of a policy from observed state transitions and rewards. In a finite Markov decision process, fixing a policy produces a Markov chain, so policy evaluation becomes the task of estimating the expected return from each state. Bradtke and Barto's 1996 paper introduced a least-squares temporal-difference method, LS TD, that uses each observed transition in a linear system instead of selecting a learning-rate schedule. Their Theorem 1 states probability-one convergence for trials that end at absorbing states under explicit conditions on state access, rewards, and features. This mission formalizes that result and the statements the authors use to reach it. Bradtke and Barto, 1996.

The result matters for episodic policy evaluation: a learner may collect many short trajectories, each begun from a prescribed start distribution, and update the same estimate as data accumulate. The theorem identifies conditions under which the limit is the true value parameter even when the discount factor is one. That endpoint is useful for undiscounted tasks ending in an absorbing goal state; it also makes the convergence claim more delicate than the standard discounted case. The paper proves the result mathematically. The Lean statements in this mission are targets for machine-checked proofs, not claims of proofs already present in Mathlib. Bradtke and Barto, Theorem 1, pp. 43–44.

Setting

Let $X$ be a finite, nonempty set of states. After a policy is fixed, $P(x,y)$ is the probability of a transition from $x$ to $y$, so each row of $P$ is nonnegative and sums to one. A transition earns a deterministic real reward $R(x,y)$. A state is absorbing when $P(x,x)=1$; let $\mathcal T$ be the absorbing states and $\mathcal N=X\setminus\mathcal T$ the others. The chain is absorbing when some absorbing state can be reached with positive probability from every state. A start distribution $S$ gives the state at the beginning of each trial. No state is inaccessible when every state can be reached from the positive support of $S$.

For a discount $\gamma$, the expected immediate reward is $\bar r(x)=\sum_yP(x,y)R(x,y)$. The true value function is defined by the expected return

$$V(x)=\sum_{k=0}^{\infty}\gamma^k(P^k\bar r)(x).$$

A feature vector $\phi_x\in\mathbb R^m$ represents state $x$. The matrix $\Phi$ has row $x$ equal to $\phi_x^\top$. The target parameter $\theta^*$ is a vector for which $V(x)=\phi_x^\top\theta^*$ at every state; it is something the theorem must establish, not an input chosen by a formula. Equation (11) forms an LS TD estimate $\theta_n$ from the observed feature differences and rewards. Bradtke and Barto, §2, Table 1, Eq. (11).

Figure 2 collects trials. Each starts from $S$, follows $P$ while the current state is non-absorbing, and ends upon entry into $\mathcal T$. The next trial starts with a fresh draw from $S$. The estimator includes transitions taken within trials; a draw that starts the next trial is not an observed transition for Eq. (11). Bradtke and Barto, Figure 2, p. 42.

Formalization targets

Theorem 1: convergence of trial-based LS TD

If every state is accessible from $S$, rewards between absorbing states vanish, the feature vectors on $\mathcal N$ are linearly independent, features on $\mathcal T$ are zero, $m=|\mathcal N|$, and $0\le\gamma\le1$, then the expected-return series converges and there is a parameter $\theta^*$ satisfying

$$V(x)=\phi_x^\top\theta^*\quad(x\in X),\qquad \theta_n\longrightarrow\theta^*\quad\text{with probability one}.$$

The theorem keeps the paper's endpoint $\gamma=1$. The return series' convergence is explicit because a real infinite sum in Lean has a default value when it diverges. Bradtke and Barto, Theorem 1, p. 43.

Supporting targets

The milestone list follows the statements used in the paper: almost-sure visits and departure proportions for the trials; invertibility of the non-absorbing block of $I-\gamma P$; invertibility of $\Phi^\top\Pi(I-\gamma P)\Phi$ for positive non-absorbing weights; Lemma 5's probability-one limit $[\Phi^\top\Pi(I-\gamma P)\Phi]^{-1}\Phi^\top\Pi\bar r$; and Eq. (12), $\bar r=(I-\gamma P)\Phi\theta^*$, together with finiteness of the true parameter. Here $\Pi=\operatorname{diag}(\pi)$. Bradtke and Barto, Lemma 5, p. 43; Proof of Theorem 1, p. 44.

Significance

Theorem 1 identifies the target of the asymptotic LS TD estimate: the value function defined from rewards, rather than merely a vector satisfying a sampled linear system. It covers an undiscounted absorbing chain, where a general fixed-point equation for values would fail to determine the values of absorbing states. The zero-reward and zero-feature conditions determine that boundary correctly. The result also explains the dimension condition: one independent feature vector for each non-absorbing state permits exact representation of the return. Bradtke and Barto, pp. 43–44.

A complete formal development would connect finite-state stochastic-process laws, visit frequencies, matrix limits, and the return-defined value function in one checked statement. The reusable parts include a finite row-stochastic chain model, a path-law description of restarts, a filtered least-squares estimator, and results about transient blocks of stochastic matrices. The paper's mathematical proof exists; this mission asks for formal proofs of its Lean targets. It also leaves room for alternative proofs and sharper, separately stated variants without weakening Theorem 1.

Difficulty

Ordinary matrix convergence cannot be applied until the observed transition frequencies are known to converge and the limiting matrix is invertible. A trial has random length, and the process resets after absorption, so a sequence indexed by all restart-process steps does not have the same raw state proportions as a count indexed by trials. The proof must account for both clocks while retaining the in-trial data of Eq. (11). At $\gamma=1$, a direct geometric-series argument for the value function is unavailable; its finiteness depends on absorption and the reward convention. The matrix $I-\gamma P$ itself is singular at the undiscounted endpoint because of absorbing states, while its non-absorbing block is the relevant invertible matrix. Bradtke and Barto, Proof of Theorem 1, p. 44.

Formalization scope

The Lean state type is finite and nonempty. The paper evaluates one fixed policy, so $P$ is a real row-stochastic matrix and $R$ is a deterministic real reward on transitions; there is no action type in the formal statement. Absorbing states are exactly those with $P(x,x)=1$, and “absorbing chain” means that an absorbing state is reachable from every state. The paper does not define “inaccessible”; the formalization reads it as unreachable from the positive support of $S$. The state space carries the discrete measurable structure. Theorem 1's restart process and Lemma 5's ordinary Markov chain are each constrained by their finite-dimensional cylinder probabilities, not by assumed transition frequencies.

The feature space is $\mathbb R^m$, and $m$ equals the cardinality of the subtype $\mathcal N$. LS TD uses only departures from $\mathcal N$. Index $n$ counts restart-process steps, so the estimate repeats at a restart draw; the paper counts in-trial transitions. These indices have the same asymptotic estimate when transitions continue. The $1/t$ factors in Eq. (11) cancel, and early singular inverses take Lean's total-inverse default. The value function is the return series, and the goal explicitly asserts its summability. The true parameter is existential, never defined by the formula whose convergence the theorem is meant to prove.

The paper defines $\pi_x$ for absorbing chains as expected departures from $x$ per trial. The Theorem 1 visit-frequency milestone normalizes by restart-process steps, which rescales all weights by one positive common factor; Lemma 5's matrix expression is invariant under that rescaling. Lemma 5 itself counts every ordinary-chain transition and carries the paper's “any Markov chain” scope. The milestone on invertibility allows arbitrary weights at absorbing states because their feature rows are zero. These conventions are recorded with each Lean item. Contributions toward the path-law frequency theorem, transient-matrix invertibility, return-series summability, and the matrix limit are all within scope. A vacuous path law or a value function defined from the desired linear equation would not establish the stated goal.

Selected references

• S. J. Bradtke and A. G. Barto, Linear Least-Squares Algorithms for Temporal Difference Learning, Machine Learning 22, 33–57 (1996). DOI: 10.1023/A:1018056104778.

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.

Motivation

Dynamic programming over uncountable state and control spaces needs two things at every stage: the optimal cost-to-go, obtained by minimizing over the control, must be a function that can be integrated against the next stage's transition probabilities, and a policy that nearly attains the minimum must be measurable, so that it defines a stochastic process. With Borel-measurable costs and Borel-measurable policies both requirements fail. Minimizing a Borel function of $(x,y)$ over $y$ produces a function whose level sets are projections of Borel sets, and such projections need not be Borel (Suslin, 1917). The repair, developed by Blackwell, Freedman and Orkin (1974), Shreve and Bertsekas, and set out in Chapter 7 of Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978), is to enlarge the class of costs to the lower semianalytic functions and the class of policies to the analytically or universally measurable ones. Sections 7.6–7.7 of the book establish that this class is closed under partial minimization and admits measurable ε-optimal selectors. Chapters 8–10 of the book, and much of the later literature on Borel-space Markov decision processes (Hernández-Lerma and Lasserre; Feinberg and coauthors), build on these results.

Timeline:

• 1917: Suslin shows that projections of Borel sets need not be Borel and introduces analytic sets; Lusin proves that analytic sets are universally measurable.
• 1941–1949: Jankov and von Neumann independently prove that an analytic subset of a product admits a selector measurable with respect to the σ-algebra generated by analytic sets.
• 1974: Blackwell, Freedman and Orkin use analytic sets to construct ε-optimal policies in Borel dynamic programming.
• 1978: Bertsekas and Shreve give the treatment used here (§7.6–7.7), including the selection theorem for lower semianalytic functions, Proposition 7.50.

Setting

A Borel space is a topological space homeomorphic to a Borel subset of a complete separable metric space (Definition 7.7); its Borel σ-algebra is $\mathscr B_X$. The Baire space is $\mathscr N=\mathbb N^{\mathbb N}$ with the product topology. A set $A\subseteq X$ is analytic if it is empty or the image of $\mathscr N$ under a continuous map; by Proposition 7.41 this is the book's Definition 7.16 (the Suslin operation applied to closed sets). Every Borel set is analytic, and the converse fails when $X$ is uncountable.

Three σ-algebras on $X$ are in play. The analytic σ-algebra $\mathscr A_X$ is generated by the analytic sets (Definition 7.19). The universal σ-algebra is $\mathscr U_X=\bigcap_{p}\mathscr B_X(p)$, the intersection over all probability measures $p$ on $(X,\mathscr B_X)$ of the $p$-completions of $\mathscr B_X$ (Definition 7.18). For a function $f$ from $D\subseteq X$ into a Borel space $Y$, $f$ is analytically measurable if $D\in\mathscr A_X$ and $f^{-1}(B)\in\mathscr A_X$ for every $B\in\mathscr B_Y$, and universally measurable if the same holds with $\mathscr U_X$ (Definition 7.20).

Let $R^*=[-\infty,\infty]$. A function $f:D\to R^*$ is lower semianalytic if $D$ is analytic and $\{x\in D\mid f(x)<c\}$ is analytic for every real $c$ (Definition 7.21). For $D\subseteq X\times Y$ write $D_x=\{y\mid (x,y)\in D\}$, $\mathrm{proj}_X(D)=\{x\mid D_x\neq\emptyset\}$, and define the partial infimum

$$f^*(x)=\inf_{y\in D_x}f(x,y),\qquad x\in\mathrm{proj}_X(D).$$

A selector is a function $\varphi:\mathrm{proj}_X(D)\to Y$ whose graph $\mathrm{Gr}(\varphi)$ lies in $D$.

Formalization targets

Goal: Proposition 7.50

Let $X,Y$ be Borel spaces, $D\subseteq X\times Y$ analytic, and $f:D\to R^*$ lower semianalytic.

(a) For every $\varepsilon>0$ there is an analytically measurable selector $\varphi$ with

$$f[x,\varphi(x)]\le\begin{cases}f^*(x)+\varepsilon&\text{if }f^*(x)>-\infty,\\-1/\varepsilon&\text{if }f^*(x)=-\infty.\end{cases}$$

(b) The set $I$ of points where the infimum is attained is universally measurable, and for every $\varepsilon>0$ there is a universally measurable selector $\varphi$ with $f[x,\varphi(x)]=f^*(x)$ on $I$ and the bounds of (a) off $I$.

The goal fixes no constant beyond the book's $\varepsilon$ and $-1/\varepsilon$.

Milestones

In attack order: Proposition 7.40 (Borel images and preimages of analytic sets are analytic), Corollary 7.42.1 ($\mathscr A_X\subseteq\mathscr U_X$), Corollary 7.44.2 (composites of analytically measurable maps are universally measurable), and Proposition 7.49, the Jankov–von Neumann theorem:

$$A\subseteq X\times Y\text{ analytic}\ \Longrightarrow\ \exists\,\varphi:\mathrm{proj}_X(A)\to Y\ \text{analytically measurable},\ \mathrm{Gr}(\varphi)\subseteq A.$$

Further items of the mission, on the same definitions: Proposition 7.39 (projections of analytic sets are analytic, and every analytic set is a projection of a Borel set), Lemma 7.30(1) (strict and non-strict, real and extended level sets give the same class) and Proposition 7.47 (lower semianalytic functions are exactly partial infima of Borel functions).

Significance

Proposition 7.50 is the selection theorem behind the existence of ε-optimal policies in Borel-space dynamic programming. In the finite-horizon model of Chapter 8 the optimal cost-to-go at each stage is lower semianalytic, by Propositions 7.47 and 7.48. Proposition 7.50 then turns the one-stage minimization into a measurable policy, analytically measurable when only ε-optimality is required and universally measurable when the minimum is attained. Chapters 8–9 of the book (the finite-horizon recursion $J^*_K=T^K(J_0)$ and the optimality equation under (P), (N), (D)) use it at every step. Downstream catalog papers on average-cost and stochastic shortest-path problems over Borel spaces cite these results.

All results here are proved in the book and in the descriptive set theory literature (Kechris, Classical Descriptive Set Theory, §18 and §29). None is formalized on Prove2Me. Mathlib has analytic sets in Polish-type settings, the Lusin separation theorem and Suslin's theorem, but it has no universal σ-algebra, no analytic σ-algebra, no lower semianalytic functions and no Jankov–von Neumann uniformization. The definitions in this mission are reusable by the later missions of the series (Chapters 8–10), which restate them locally until these are published.

Difficulty

The obvious route to a selector is to choose, for each $x$, a minimizing or near-minimizing $y$. The axiom of choice provides such a function, but nothing makes it measurable, and the conclusion of the theorem is exactly that measurability. The Borel route fails too: the set $\{x\mid f^*(x)<c\}$ is a projection of a Borel set, which is analytic but in general not Borel, so no Borel-measurable selector exists in general. The Jankov–von Neumann theorem needs a lexicographically least branch of a continuous parametrization of $A$ by $\mathscr N$, and an argument that the resulting map is measurable with respect to $\mathscr A_X$, which is generated by sets that are not closed under complementation. Part (b) adds a further obstacle: the composite of two analytically measurable maps need not be analytically measurable, so the exact selector is only universally measurable. Proving that requires Lusin's theorem that analytic sets are measurable for every completed probability measure.

Formalization scope

• A Borel space is a type with a topology satisfying the class IsBorelSpace (Definition 7.7, the ambient complete separable metric space taken in the same universe), together with Mathlib's [MeasurableSpace X] [BorelSpace X], so measurable sets are exactly the Borel sets. On $X\times Y$ the product σ-algebra is used; it coincides with $\mathscr B_{X\times Y}$ for separable metrizable spaces (Proposition 7.13).
• Analytic sets are Mathlib's MeasureTheory.AnalyticSet (empty or a continuous image of ℕ → ℕ).
• $R^*$ is EReal. The book uses $\infty-\infty=\infty$, and Mathlib's EReal uses $\bot+\top=\bot$. No statement of this mission adds infinities of opposite sign; $f^*(x)+\varepsilon$ adds a real number.
• Functions on $D$ and on $\mathrm{proj}_X(D)$ are functions on subtypes. The graph condition $\mathrm{Gr}(\varphi)\subseteq D$ is part of every selector statement.
• Universally measurable means NullMeasurableSet E p for every probability measure p.
• "Analytically measurable" refers to the σ-algebra generated by analytic sets. Replacing it by the power set, dropping the graph condition, or dropping the $-1/\varepsilon$ case would make the selection theorems a consequence of the axiom of choice. The statements rule all three out.

Not included: Lusin's theorem in Suslin-scheme form (Proposition 7.42, which needs the Suslin operation as a definition), Proposition 7.43 on $P(X)$, the integration results of Propositions 7.46 and 7.48, and Lemma 7.30(2)–(4). None is used in the proof of the goal. Contributions welcome: the bridge between IsBorelSpace and Mathlib's StandardBorelSpace, the universal σ-algebra API, and the Jankov–von Neumann theorem itself.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific 1996, §7.6–7.7. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, D. Freedman and M. Orkin, The optimal reward operator in dynamic programming, Annals of Probability 2 (1974) 926–941. https://doi.org/10.1214/aop/1176996558
• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer 1995, §18 (Jankov–von Neumann uniformization), §29 (measurability of analytic sets). https://doi.org/10.1007/978-1-4612-4190-4
• 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