The OR Formalization Drive

Motivation

Battery-powered and energy-harvesting wireless devices cannot treat transmission power as free: a control algorithm that maximizes throughput without regard to energy will drain a device long before the network's other resources are exhausted. Chapter 6 of Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006) extends the drift-plus-penalty framework of Chapter 5 to problems with an explicit average-resource-budget constraint, and works out the Energy Constrained Control Algorithm (ECCA) of Neely [116] as its flagship example: a joint flow-control and power-allocation policy that keeps every data queue and a virtual "excess energy" queue bounded by an explicit, finite constant on every single time slot — not merely in expectation or in the long run.

Setting

A multi-user wireless downlink serves $L$ users over $L$ channels with a time-varying collective topology state $S(t)$ and link rate function $C_i(P,S(t))$ under power allocation $P=(P_1,\dots,P_L)$, subject to a per-slot power budget $\sum_i P_i(t)\le P_{max}$ and a target average power constraint $P_{av}<P_{max}$. Exogenous arrivals $A_i(t)\le\hat R$ are entirely admitted or entirely dropped each slot (no transport-layer storage). The ECCA algorithm runs, every slot: flow control — admit $A_i(t)$ into queue $i$ if $U_i(t)\le V$ (a fixed parameter), otherwise drop it entirely; power allocation — choose $P(t)$ to maximize $\sum_i[U_i(t)C_i(P,S(t))-D(t)P_i(t)]$ subject to the power budget, where $D(t)$ is a virtual power queue tracking accumulated excess energy expenditure, updated by $D(t{+}1)=\max[D(t)-P_{av},0]+\sum_i P_i(t)$.

Formalization targets

Goal — Theorem 6.3 (ECCA Performance)

$$U_i(t)\le U_{max}:=V+\hat R\ \ \forall i,t,\qquad D(t)\le D_{max}:=\beta V+\beta\hat R+P_{max}\ \ \forall t,$$

$\text{and consequently, for every $T$-slot interval, } \sum_{\tau} \textstyle\sum_i P_i(\tau) \le P_{av}\cdot T+D_{max},$ where $\beta>0$ is the constant in the rate function's marginal-benefit inequality $C_i(P,S)\le C_i(P^{[i]},S)+\beta P_i$ ($P^{[i]}$ being $P$ with its $i$-th entry zeroed). These bounds hold for every topology state process $S(t)$ and every admissible arrival process $A(t)$, on every sample path — the weakest, most general level, with no distributional assumption whatsoever on either process.

Significance

Theorem 6.3 gives a hard, deterministic worst-case guarantee — every queue in the system, actual or virtual, is bounded by an explicit closed-form constant on every single slot, not merely on average or asymptotically — which is exactly the kind of guarantee a resource-constrained embedded or battery-powered device needs: a device can be provisioned with buffer and battery-reserve capacity of the theorem's own $U_{max}$, $D_{max}$ and know, with certainty rather than in expectation, that it will never overflow. The corollary that no $T$-slot interval spends more than $P_{av}\cdot T+D_{max}$ in energy translates directly into a battery-lifetime guarantee. This is also, methodologically, the one point in the whole book's drift-plus-penalty method where an elementary induction — not a probabilistic Lyapunov drift argument — suffices, because ECCA's flow control rule directly caps $U_i(t)$ regardless of what the channel or arrivals do.

Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for virtual queue, energy-constrained control, power allocation — no faithful hits; one unrelated coincidental keyword match in a neural-coding combinatorics item was checked and is not relevant). This mission is the first formalization of the ECCA performance guarantee.

Difficulty

The obvious first idea is to bound $U_i(t)$ and $D(t)$ by unrolling their recursions and applying a probabilistic drift argument, as in every other capstone in this series. This is unnecessary and would in fact obscure the actual mechanism: $U_i(t)\le U_{max}$ follows from a two-case induction that needs no probability at all — if $U_i(t)\le V$, the flow control rule admits at most $\hat R$ more, giving $U_i(t{+}1)\le V+\hat R$; if $U_i(t)>V$, flow control drops everything, so $U_i(t{+}1)\le U_i(t)\le U_{max}$ by the induction hypothesis. The harder part is $D(t)\le D_{max}$: it requires connecting the virtual queue's own accumulation to the fact that the power-allocation optimization (6.14) will stop spending power on link $i$ once $D(t)$ grows past $U_i(t)\cdot\beta$ — a consequence of $P(t)$'s optimality for (6.14) together with the $\beta$-inequality on $C_i$, not a property one can read off the $D$-recursion alone.

Formalization scope

The power-allocation rule is stated as an explicit optimality hypothesis (hPopt): for every competing power vector $P'$ respecting the budget, the objective (6.14) at the chosen $P(t)$ is at least as large — the faithful rendering of "$P(t)$ is chosen to maximize (6.14)" without needing Lean's argmax/IsMaxOn machinery. The rate function's $\beta$-inequality is stated exactly as the book gives it, using Function.update P i 0 for $P^{[i]}$. Out of scope for this mission: the throughput conclusion under i.i.d. $A(t), S(t)$ (an expectation/liminf statement, unlike the rest of this theorem, needing the same conditional-expectation machinery as the other chapters' capstones) and Theorem 6.2 (the general GCLC framework this specializes, which needs Assumptions 1-4's four simultaneous existential clauses over an "S-only" policy) — both left for a future mission. A trivializing formalization to rule out: weakening the two sample-path conclusions to a limsup/expectation-style bound (the convention used elsewhere in this series) would misstate this theorem, whose entire distinguishing content is that the bounds hold for every time slot and every sample path, not merely in the long run.

Selected references

• Georgiadis, Neely & Tassiulas, Resource Allocation and Cross-Layer Control in Wireless Networks, Foundations and Trends in Networking, Vol. 1, No. 1 (2006), pp. 1-144. https://doi.org/10.1561/1300000001
• Neely, "Energy optimal control for time-varying wireless networks", IEEE Transactions on Information Theory, 52(7), 2006. https://doi.org/10.1109/TIT.2006.876219

One stage at a time

A serial supply chain is the simplest multiechelon system: a retailer orders from a warehouse, which orders from a plant, which orders from an outside supplier with unlimited stock. Only the retailer sees customer demand, only the retailer pays a stockout penalty, and every stage pays to hold inventory. Choosing how much each stage should hold looks like a joint optimization over all stages at once, because an upstream stockout delays every downstream replenishment. Clark and Scarf (1960) showed that it is not: measured in echelon terms, the optimal policy is a base-stock policy at every stage, and the optimal levels can be found one stage at a time from the customer upward, each step a single-variable convex minimization. Chapter 6 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) presents the infinite-horizon form of that result as its Theorem 6.3, the bounds of Shang and Song (2003) that make the levels cheap to approximate, and the contrasting guaranteed-service model of Graves and Willems (2000), in which stages quote delivery times rather than fill rates and the optimal safety stocks are all-or-nothing. This mission formalizes the chapter's numbered results, with Theorem 6.3 as its goal.

Setting

Stages are numbered $1, \dots, N$ from the customer upward. Stage $j$ has a local holding cost $h'_j$ per unit per period; its echelon holding cost is $h_j = h'_j - h'_{j+1}$ with $h'_{N+1} = 0$, so that $h'_j = \sum_{i \ge j} h_i$ (localHolding, echelonHolding). Stage $j$'s echelon consists of stages $j, j-1, \dots, 1$, and its echelon on-hand inventory $I_j$ (echelonOnHand) is all on-hand and in-transit stock in that echelon. Stage 1 pays a stockout cost $p$ per unit per period. Orders placed by stage $j$ arrive after a lead time $L_j$ if stage $j+1$ can ship them; $D_j$ denotes the lead-time demand at stage $j$.

An echelon base-stock policy gives each stage a level $S_j$ and orders to keep its echelon inventory position at $S_j$. The chapter derives, from conservation of flow, a recursion that evaluates the expected cost of any echelon base-stock vector $S$ (csBar, csHat, csG):

$$\bar g_0(x) = (p + h'_1)x^-, \qquad \hat g_j(x) = h_j x + \bar g_{j-1}(x), \qquad g_j(y) = \mathbb{E}[\hat g_j(y - D_j)], \qquad \bar g_j(x) = g_j(\min\{S_j, x\}),$$

and the expected cost of the system under $S$ is $g_N(S_N)$. The term $\bar g_j$ is the implicit penalty function: it charges stage $j+1$ for the downstream consequences of running short. A vector is sequentially optimal (CSSequential) when each $S_j$ minimizes $g_j$, which depends only on $S_1, \dots, S_{j-1}$.

The Shang-Song bounds compare $g_j$ with the cost of the $j$-stage truncated system when all its local holding costs are set to one value, $h_j$ for the lower bound and $\sum_{k \le j} h_k$ for the upper (ssLower, ssUpper). With equal holding costs all stock is held at stage 1, so each bound is a single-stage newsvendor cost for the demand $\tilde D_j = D_1 + \dots + D_j$ over the cumulative lead time (tildeLaw) with stockout cost $p + h'_{j+1}$, plus the holding cost of the stock in transit to stages $1, \dots, j-1$, whose mean is $\mathbb{E}[D_1] + \dots + \mathbb{E}[D_{j-1}]$ (pipelineMean).

In the guaranteed-service model each stage $i$ has a processing time $T_i$, quotes a committed service time $S_i$ to its customer, and receives an inbound time $SI_i = S_{i+1}$ from its supplier (gsInbound), $SI_N$ being external. Demand is bounded, so the stage can meet every order within $S_i$ by holding safety stock $k\sqrt{SI_i + T_i - S_i}$ with $k = z_\alpha\sigma$, and the holding cost is $g(S) = \sum_i h_i k \sqrt{SI_i + T_i - S_i}$ (gsCost) over the feasible times $0 \le S_i \le SI_i + T_i$ (GSFeasible).

Formalization targets

Goal: Theorem 6.3

For echelon holding costs $h_j \ge 0$, stockout cost $p \ge 0$ and lead-time demands of finite mean, if $S^*$ is sequentially optimal then for every echelon base-stock vector $S$,

$$g_N(S^*_N \mid S^*) \;\le\; g_N(S_N \mid S),$$

and $g_N(S^*_N \mid S^*)$ is the optimal cost. This is clark_scarf_sequential.

Supporting targets

Proposition 6.1, $\sum_j h_j I_j = \sum_j h'_j (I'_j + IT_{j-1})$; the stage-1 identities (6.29) and (6.30), that $g_1$ is a newsvendor cost with penalty $p + h'_2$ and its minimizer solves $F_1(S^*_1) = (p + h'_2)/(h_1 + p + h'_2)$; convexity of every $g_j$ under sequential optimality; existence of a sequentially optimal vector when $h_j > 0$ and $p > 0$; Theorem 6.4, $g^l_j \le g_j \le g^u_j$, and $S^l_j \le S^*_j \le S^u_j$ where $S^u_j$ minimizes $g^l_j$ and $S^l_j$ minimizes $g^u_j$ (the book's pairing, p. 200); and Theorem 6.5, that in the guaranteed-service serial system with $s_1 = 0$ every optimal $S^*_i$ is $0$ or $S^*_{i+1} + T_i$.

Theorem 6.2, the optimality of echelon base-stock policies among all policies, is stated in the book without a model of the policy space and is not a target here; Theorem 6.3 is the optimization it licenses.

Significance

Theorem 6.3 is what Zipkin calls the fundamental equations of supply chain theory. It reduces a joint optimization over $N$ coupled levels to $N$ one-dimensional convex problems, and every exact method and most heuristics for serial and assembly systems, Rosling's reduction of assembly systems to serial ones included, run through it. Theorem 6.4 turns the recursion into closed-form bounds and the Shang-Song heuristic, which the book reports as accurate to within a fraction of a percent. Theorem 6.5 explains the shape of optimal safety stock placement under guaranteed service and why its dynamic program only needs to examine endpoints.

None of these results has a machine-checked proof. The book proves none of them in full: Theorem 6.3 is asserted after an informal derivation, Theorem 6.4 is cited, and Proposition 6.1 and Theorem 6.5 are left as exercises. Formalizing the recursion's convexity and the exchange argument behind Theorem 6.3 produces a reusable treatment of the implicit penalty function; the concavity-on-a-polytope argument for Theorem 6.5 is reusable for the tree systems of Sect. 6.3.5.

Difficulty

The obvious attack on Theorem 6.3, differentiating the system cost in each $S_j$, fails immediately: the cost depends on $S_j$ through $\min\{S_j, x\}$ inside nested expectations and is not convex in $S$ jointly. The argument that works is an induction along the recursion, comparing $g_j(\cdot \mid S)$ with $g_j(\cdot \mid S^*)$ pointwise. Its key step is that, for the convex $g_j(\cdot \mid S^*)$ minimized at $S^*_j$, the value $g_j(\min\{S^*_j, x\})$ is the least value of $g_j$ on $(-\infty, x]$, so that any other truncation point can only cost more. That step needs convexity of $g_j(\cdot \mid S^*)$, which needs $\bar g_{j-1}(\cdot \mid S^*)$ convex, which needs $S^*_{j-1}$ to be a minimizer; for an arbitrary $S$ the functions $\bar g_j(\cdot \mid S)$ are not convex, and the induction must carry both vectors at once.

Integrability is a second, silent obstacle. Each $g_j$ is an expectation of translates of $\hat g_j$; the recursion preserves Lipschitz continuity with a constant growing with the costs, and finite means are exactly what make every integral in the recursion a genuine expectation rather than Lean's default value zero.

Theorem 6.4 requires relating the recursion, in which demands enter one stage at a time, to a single newsvendor cost in the sum $\tilde D_j$, which is a convolution; the inequalities come from the structure of (6.31) in the two extreme holding-cost profiles and are not obvious from the recursion's formulas. Theorem 6.5 is a statement about every minimizer, not the existence of an extreme one, so the proof must show the cost is strictly concave along every feasible direction that changes a net lead time and then classify the vertices of the feasible region.

Formalization scope

Stages are indexed by natural numbers $1, \dots, N$; the cost functions take total functions on $\mathbb{N}$ and never read values outside that range. The recursion is defined for every vector $S$, so the theorem compares values of one family of functions rather than a separately defined system cost; the identification of $g_N(S_N \mid S)$ with the steady-state expected cost of the physical system is the book's derivation and is not restated. Expectations are Lebesgue integrals under the lead-time demand laws, assumed to be probability measures on $\mathbb{R}$ with finite means. Sequential optimality is a hypothesis of the goal; a separate target shows it is satisfiable when $h_j > 0$ and $p > 0$, so the goal is not vacuous.

The bounding functions of Theorem 6.4 keep the holding cost of pipeline stock that the truncated cost (6.31) charges. The book omits that constant when it writes their minimizers, which it does not affect, but part (a) compares values, and without the constant the upper bound fails already in the book's own Example 6.1. For part (b) the minimizers of the bounding functions are asserted to exist and to bracket $S^*_j$; when the fractiles of $\tilde D_j$ are unique these are the book's quantile values. Theorem 6.5 is stated over real service times; because the feasible region's vertices are integral when the data are, every integer-optimal vector is optimal over the reals, so the real statement contains the book's integer program (6.38) to (6.42). Proposition 6.1 is stated with $IT_0 = 0$ built into the echelon sum.

The definition module is shared by all nine items. The dynamic program (6.43) to (6.44) for guaranteed-service serial systems and the tree-system algorithm of Sect. 6.3.6 are natural extensions on the same definitions.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 6. https://doi.org/10.1002/9781119584445
• A. J. Clark and H. Scarf, Optimal policies for a multi-echelon inventory problem, Management Science 6(4), 1960. https://doi.org/10.1287/mnsc.6.4.475
• F. Chen and Y.-S. Zheng, Lower bounds for multi-echelon stochastic inventory systems, Management Science 40(11), 1994. https://doi.org/10.1287/mnsc.40.11.1426
• K. H. Shang and J.-S. Song, Newsvendor bounds and heuristic for optimal policies in serial supply chains, Management Science 49(5), 2003. https://doi.org/10.1287/mnsc.49.5.618.15147
• S. C. Graves and S. P. Willems, Optimizing strategic safety stock placement in supply chains, Manufacturing & Service Operations Management 2(1), 2000. https://doi.org/10.1287/msom.2.1.68.23267

Motivation

The index theorem says that among several Markov reward processes, of which one may be advanced at each decision time, the right one to advance is the one of greatest Gittins index. Chapter 4 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks how far this extends when the constituents are not reward processes but decision processes, each with its own controls: a research project that can be run in several ways, a job that can be processed at different speeds, a sampling process that may be stopped and exploited. A family of such superprocesses requires two choices at every decision time, which superprocess to continue and with which control, and an index policy in the sense of Chapter 2 need not be optimal (Example 4.1). Whittle (1980) identified the condition under which it is: Condition D, that when a superprocess is played against a standard bandit process paying a constant rent, the control one should apply to it does not depend on the rent. Under that condition the index theorem survives (Theorem 4.3), the index is characterized (Note 4.2), stoppable bandit processes with improving stopping options satisfy the condition (Lemma 4.4), and the chapter adds two results about indices themselves: any index that works for all bandit processes is a strictly increasing function of the Gittins index (Theorem 4.8), and a policy that is within $\varepsilon$ of the index policy loses at most $\varepsilon\gamma^{-1}(1-e^{-\gamma})^{-1}$ (Theorem 4.18).

Setting

A decision process $D$ on a countable state space $S$ has in each state $x$ a nonempty finite set $\Gamma(x)$ of controls; applying $u$ yields the reward $r(x, u)$ and moves the state by $P(\cdot \mid x, u)$. Adding the freeze control, which leaves the state unchanged and yields nothing, makes $D$ a superprocess $S$. Operating $D$ under a feasible deterministic stationary Markov policy $g$ (that is, $g(x) \in \Gamma(x)$) gives an ordinary bandit process $D_g$, and the superprocess index is

$$\nu(S, x, u) = \sup_{g : g(x) = u} \nu(D_g, x), \qquad \nu(S, x) = \max_{u \in \Gamma(x)} \nu(S, x, u), \tag{4.1}$$

with $\nu(D_g, x)$ the Gittins index of the Bandit Algorithms model. A simple family of alternative superprocesses (SFAS) is $n$ superprocesses on a common $(S, U)$; at each decision time $0, 1, 2, \dots$ exactly one is continued, with a control from its control set, the others being frozen, and rewards are discounted by $a^t$. A policy is a Markov kernel per decision time from the history to the pair (superprocess, control); it is optimal if it is feasible and attains the supremum of the discounted payoff over feasible policies from every initial state-vector, and it is an index policy if it always continues a superprocess and control of maximal $\nu(S_i, x_i, u)$.

Condition D. Let $\Lambda$ be a standard bandit process with parameter $\lambda$ (one state, reward $\lambda$). $S$ satisfies Condition D if there is a function $g$ such that, for every $x$ and $\lambda$ for which it is optimal in the family $\{S, \Lambda\}$ to select $S$ in state $x$, it is optimal to apply the control $g(x)$. A stoppable bandit process is a bandit process with a stop control that makes it behave as a standard bandit process with parameter $\mu(x)$; its stopping option is improving if $\mu(x(t))$ is almost surely nondecreasing in process time.

Formalization targets

Goal: Theorem 4.3

For a decision process with bounded rewards and a Condition-D control $g$, every index policy with respect to $\nu(D, \cdot, \cdot)$ that applies $g(x_i)$ to the superprocess $i$ it continues is optimal for the family of $n$ superprocesses:

$$\text{index policy } \pi \implies \pi \text{ feasible and } R_\pi(x) = \sup_{\pi' \text{ feasible}} R_{\pi'}(x)\ \text{ for every } x \in S^n.$$

Milestones

Note 4.2 (under Condition D, $S$ is selected in $\{S, \Lambda(\lambda)\}$ iff $\nu(S, x) \ge \lambda$, and at $\lambda = \nu(S, x)$ a control $u$ is optimal iff $\nu(S, x, u) = \nu(S, x)$; the printed equivalence fails for $\lambda < \nu(S, x)$); Lemma 4.4 (Condition D for stoppable bandit processes with improving stopping options); Theorem 4.8 (an index for the bandit processes with discount factor $a$ is strictly increasing in $\nu$); Theorem 4.18 (the $\varepsilon$-index bound, $\varepsilon/(1-a)^2$ for the discrete-time index).

Significance

Theorem 4.3 is the widest form in which the index theorem holds without further structure, and Condition D is exactly the right hypothesis: it says the superprocess has a canonical control, and once it does the family reduces to a family of bandit processes and the prevailing-charge argument goes through. Lemma 4.4 gives the model where the condition is known to hold, a research project that may be exploited at any time; the buyer's problem of Bergman and Bather is the case where it fails. Theorem 4.8 explains why every index theorem in the book is about the Gittins index: any function that orders bandit processes optimally must order them as $\nu$ does. Theorem 4.18 is the quantitative version of the index theorem that heuristics and computations rely on.

Nothing here is machine-checked. The mission builds the first controlled multi-armed model on the platform, a run law for families of decision processes with an explicit feasibility constraint, and states Whittle's condition as a property of the two-member family, which is how the literature uses it. Theorems 4.8 and 4.18 are statements about the existing Bandit Algorithms model and are usable by any later work on that model.

Difficulty

The obvious attack on Theorem 4.3, "replace each superprocess by the bandit process $D_{g}$ for its Condition-D policy $g$ and apply the index theorem", is the second half of the book's proof; the first half is to show that an optimal policy never gains by applying a control other than $g(x_i)$ to a superprocess it continues, and that uses the prevailing-stake accounting of §4.3 with the other superprocesses treated as one bandit process, plus the observation that the class of policies deviating at most $k$ times is $\varepsilon$-exhaustive. Both halves require the whole run law of the family to be related to the run laws of its constituents, which is where a formalization spends its effort. Note 4.2 is short on the page but needs the optimal-stopping characterization of Chapter 2 for the bandit process $D_g$ under charge $\lambda$. Theorem 4.8 is elementary given the value of $\{B, \Lambda\}$ under a freezing rule, $R_f(B) + \lambda\gamma^{-1} - \lambda W_f(B)$, but that identity is itself a computation on the run law. Theorem 4.18 has no proof in the book (Glazebrook 1982c); the natural route is the prevailing-charge upper bound with the charges perturbed by $\varepsilon$.

Formalization scope

Decision processes carry their control sets as finsets with a nonemptiness proof and their kernels as Markov kernels; the state space is countable with measurable singletons (so stationary kernels and control-dependent maps are measurable without side conditions) and the control type is finite with measurable singletons. The family's run law is built decision time by decision time as the Bandit Algorithms model builds markovBanditMeasure, with the policy's kernel producing the pair (superprocess, control). Feasibility is an almost-sure condition on the policy kernel, and optimality is the book's: feasible, and the supremum from every initial state-vector. The superprocess index is a real supremum over feasible stationary policies with $g(x) = u$, bounded by the reward bound and nonempty for $u \in \Gamma(x)$; for an unavailable $u$ it is a default value that no index policy consults. Condition D is stated on the family $\{S, \Lambda\}$ on $S \oplus \mathrm{Unit}$, where the standard state has every control available, all equivalent. A stoppable bandit process is the decision process with control type Bool. Theorem 4.8 quantifies over index functions defined on every measurable state space and takes as hypothesis only what its proof uses, optimality of $\mu$-index policies for the families $\{B, \Lambda\}$. Theorem 4.18 is on the $k$-armed Bandit Algorithms model with $\varepsilon \ge 0$ and the bound $\varepsilon/(1-a)^2$: the book's $\varepsilon\gamma^{-1}(1 - e^{-\gamma})^{-1}$ is in continuous-time index units, $\gamma/(1-a)$ times the discrete-time index used here, and read with the discrete index it is false for $a < 1/e$. Theorem 4.3's index policy applies the Condition-D control $g$ to the superprocess it continues, as the book's proof does; an index policy that breaks ties among controls otherwise need not be optimal.

Trivializing readings are excluded: index policies must be feasible, optimality is required from every initial state, and Condition D is a statement about optimal policies of a genuine two-member family, not about a chosen policy. Welcome contributions: the relation between the family's run law and the constituents' chain laws, the freezing-rule value identity behind Theorem 4.8, and the prevailing-stake accounting of §4.3.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 4. doi:10.1002/9780470980033
• P. Whittle, Multi-armed bandits and the Gittins index, Journal of the Royal Statistical Society B 42(2), 1980. doi:10.1111/j.2517-6161.1980.tb01111.x
• K. D. Glazebrook, Stoppable families of alternative bandit processes, Journal of Applied Probability 16(4), 1979. doi:10.2307/3213152
• K. D. Glazebrook, On the evaluation of suboptimal strategies for families of alternative bandit processes, Journal of Applied Probability 19(3), 1982. doi:10.2307/3213524
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401

Motivation

A coherent risk measure assigns to a future financial position the smallest amount of capital that makes it acceptable to a supervisor. Artzner, Delbaen, Eber and Heath characterised the one-period version: every coherent risk measure has the form $\pi(X)=\inf_{\mathbb Q\in\mathcal P}\mathbb E_{\mathbb Q}[X]$ for a set $\mathcal P$ of test probabilities (ADEH 1999). Regulators, insurers and banks, however, assess positions that evolve over several periods and whose risk is re-evaluated as information arrives. A multiperiod measurement should then be time consistent: the value assigned today should agree with the values the same method assigns tomorrow, so that it can be computed by backward induction, as in dynamic programming.

Artzner, Delbaen, Eber, Heath and Ku (Ann. Oper. Res. 2007) identify exactly which sets of test probabilities give time-consistent multiperiod risk-adjusted values. The condition, stability under pasting, also appears as "rectangularity" in the recursive multiple-priors model of decision theory (Epstein and Schneider 2003), and as m-stability in the theory of risk-neutral measures (Delbaen, The structure of m-stable sets, Séminaire de Probabilités XXXIX, 2006). Riedel treated dynamic coherent risk measures on finite state spaces (Riedel 2004); the continuous-time case is in Delbaen's m-stable paper and Cheridito, Delbaen and Kupper 2004.

Setting

Let $(\Omega,\mathcal F,\mathbb P_0)$ be a probability space with a filtration $(\mathcal F_n)_{n\ge0}$ and a horizon $N$. A value process is an adapted process $X=(X_n)_{0\le n\le N}$ with every $X_n$ essentially bounded; the class of value processes is $\mathcal G$. All stopping times take values in $\{0,\dots,N\}$, and $\mathcal F_\sigma$ is the σ-algebra of the stopping time $\sigma$.

A set $\mathcal P$ of test probabilities is a closed convex set of probabilities on $(\Omega,\mathcal F_N)$, each absolutely continuous with respect to $\mathbb P_0$. Its elements are identified with their densities $f=d\mathbb Q/d\mathbb P_0$, and "closed" refers to $L^1(\mathbb P_0)$. $\mathcal P^e$ denotes the elements equivalent to $\mathbb P_0$. Each $\mathbb Q\in\mathcal P$ has the density martingale $Z^{\mathbb Q}_n=\mathbb E_{\mathbb P_0}[d\mathbb Q/d\mathbb P_0\mid\mathcal F_n]$.

Pasting. For $\mathbb Q^0,\mathbb Q\in\mathcal P^e$ with density martingales $Z^0,Z$ and a stopping time $\tau$, the pasted martingale is $L_n=Z^0_n$ for $n\le\tau$ and $L_n=Z^0_\tau Z_n/Z_\tau$ for $n\ge\tau$: the pasted probability follows $\mathbb Q^0$ up to $\tau$ and $\mathbb Q$ afterwards. $\mathcal P$ is stable (Definition 3.1) if every such pasting is again in $\mathcal P$.

Two risk-adjusted values. For a value process $X$ and a stopping time $\sigma$,

$$\Psi_\sigma(X)=\operatorname*{ess.inf}\bigl\{\mathbb E_{\mathbb Q}[X_\tau\mid\mathcal F_\sigma]\ \bigm|\ \tau\ge\sigma\text{ a stopping time},\ \mathbb Q\in\mathcal P^e\bigr\},$$

the worst conditional expected value over all test probabilities and all later stopping times. The generalized Snell envelope is the backward recursion

$$\bar\Psi_N(X)=X_N,\qquad \bar\Psi_n(X)=X_n\wedge\operatorname*{ess.inf}_{\mathbb Q\in\mathcal P^e}\mathbb E_{\mathbb Q}\bigl[\bar\Psi_{n+1}(X)\mid\mathcal F_n\bigr].$$

For a stopping time $\tau$ let $X^{\tau-}_n=X_n$ for $n<\tau$ and $X_{\tau-1}$ for $n\ge\tau$, and ${}^\tau X_n=0$ for $n<\tau$ and $X_n-X_{\tau-1}$ for $n\ge\tau$.

Formalization targets

Goal: Theorem 4.2

Assume $\mathcal F_0$ is $\mathbb P_0$-trivial and $\mathcal P^e\neq\emptyset$. Then the following are equivalent:

1. $\mathcal P$ is stable.
2. For every $\mathbb Q\in\mathcal P$ and $X\in\mathcal G$, $\Psi(X)$ is a $\mathbb Q$-submartingale.
3. $\Psi(X)=\bar\Psi(X)$ for every $X\in\mathcal G$.
4. Bellman's principle holds: for every $X\in\mathcal G$ and all stopping times $\sigma\le\tau$,

$$\Psi_\sigma(X)=\Psi_\sigma\bigl(X^{\tau-}+\Psi_\tau({}^\tau X)\mathbf 1_{[\tau,N]}\bigr).$$

Milestones

In attack order, all stated for any set $\mathcal P$ with $\mathcal P^e\neq\emptyset$ unless stability is named:

• Theorem 4.1. $\bar\Psi(X)$ is the largest process in $\mathcal G$ that lies below $X$ and is a $\mathbb Q$-submartingale for every $\mathbb Q\in\mathcal P$.
• Step (1) of the proof of Theorem 4.2. $\Psi_n(X)\ge\bar\Psi_n(X)$.
• Theorem 4.2, first sentence. The family $(\Psi_\sigma(X))_\sigma$ is a process: $\Psi_\sigma(X)=\Psi_{\sigma(\omega)}(X)(\omega)$ a.s.
• Remark after Theorem 4.2. $\Psi_\tau(X)=\Psi_\tau({}^\tau X)+X_{\tau-1}$.
• Lemma 3.1 (stable $\mathcal P$). For $\tau\le\sigma\le\nu$, $\{(Z_\nu/Z_\sigma,Z_\sigma/Z_\tau)\mid Z\in\mathcal P^e\}=\{(Z'_\nu/Z'_\sigma,Z_\sigma/Z_\tau)\mid Z,Z'\in\mathcal P^e\}$.
• Lemma 4.1 (stable $\mathcal P$). The family defining $\Psi_\sigma(X)$ is closed under minima and maxima.
• Corollary of Lemma 4.1 (stable $\mathcal P$). $\mathbb E_\mu[\Psi_\sigma(X)]=\inf\{\mathbb E_\mu[\mathbb E_{\mathbb Q}[X_\tau\mid\mathcal F_\sigma]]\mid\mathbb Q\in\mathcal P^e,\ \tau\ge\sigma\}$ for every probability $\mu\ll\mathbb P_0$.

A supporting item states that the essential infimum defining $\Psi_\sigma(X)$ exists.

Significance

The result. Theorem 4.2 characterises the sets of test probabilities for which the natural worst-case risk-adjusted value is computable by dynamic programming. Stability is thereby the structural condition behind time-consistent coherent risk measurement, recursive multiple-priors utility and backward-induction pricing under ambiguity. Without it, the worst-case value computed today may disagree with the value obtained by first computing tomorrow's worst case and then today's. The equivalence with the submartingale property says that stability is also exactly what makes $\Psi(X)$ the largest submartingale minorant of Theorem 4.1. Theorem 4.3 and the recursivity results for final values in Section 5 are corollaries.

Formalizing it. The paper's proof is complete apart from Lemma 4.1 and its Corollary, whose proofs are left to the reader. No machine-checked version of this result, of the generalized Snell envelope or of essential infima of families of random variables is known to exist. A formal proof would provide a reusable development of discrete-time optimal stopping under a set of probabilities, the essential-infimum calculus of Neveu, and density-martingale pasting — infrastructure that many results on robust optimal stopping, dynamic risk measures and robust Markov decision processes need.

Difficulty

The direction from stability to Bellman's principle needs an essential infimum to be exchanged with a conditional expectation under another probability (step (3) of the proof). This is false for a general family: an essential infimum of conditional expectations is not the conditional expectation of an essential infimum. The exchange works only because stability makes the family closed under minima (Lemma 4.1), so that it is directed downward and its essential infimum is the limit of a decreasing sequence, and because Lemma 3.1 lets the test probabilities used before and after $\tau$ be chosen independently. The converse, from the submartingale property to stability, is not a computation: it uses the separation theorem in $L^1$ against a pasted density assumed outside $\mathcal P$, which is where convexity and $L^1$-closedness of $\mathcal P$ are used. Dropping either hypothesis breaks that direction.

Formalization scope

Lean represents $\mathcal P$ by its set of densities in $\mathbb P_0$: $\mathcal F_N$-measurable, a.s. nonnegative, integrable, of mass one, convex, sequentially closed in the $L^1(\mathbb P_0)$ seminorm and saturated under a.s. equality. Test probabilities are $\mathbb Q_f=f\cdot\mathbb P_0$, and $\mathbb E_{\mathbb Q}[\cdot\mid\mathcal F_\sigma]$ is Mathlib's conditional expectation under $\mathbb Q_f$. Time is $\mathbb N$, and every stopping time is bounded by $N$. A $\mathbb Q$-submartingale on $0,\dots,N$ is Mathlib's Submartingale of the process frozen after $N$. The essential infimum of a family is defined in the mission (Mathlib has only that of a single function); a supporting item shows that it exists, so its fallback value is never used. All identities between risk-adjusted values hold $\mathbb P_0$-almost surely.

Conventions made explicit:

• the goal assumes that $\mathcal F_0$ is $\mathbb P_0$-trivial, which the proof uses when it treats $\Psi_0(X)$ as a number (without it, stability is not implied by (2)–(3));
• $\mathcal P^e\neq\emptyset$ replaces the paper's convenience assumption $\mathbb P_0\in\mathcal P$;
• $X_{-1}=0$;
• the Corollary's printed essential infimum over $\mathbb Q$ alone is read over $\mathbb Q$ and $\tau\ge\sigma$, as its right-hand side and its use require.

Bellman's principle must be stated with $\Psi$ on both sides and for all stopping times $\sigma\le\tau$. Replacing $\Psi$ by $\bar\Psi$, or restricting to deterministic times, turns the goal into a property of the recursion and is not the theorem.

Needed infrastructure, reusable beyond this mission: existence and directedness of essential infima of families; conditional expectations under equivalent measures and the Bayes formula; optional sampling for bounded stopping times under each $\mathbb Q$; the $L^1$–$L^\infty$ separation theorem. Contributions of any of these, and proofs of the milestones in any order, are welcome.

Selected references

• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, H. Ku, Coherent multiperiod risk adjusted values and Bellman's principle, Annals of Operations Research 152 (2007) 5–22. https://doi.org/10.1007/s10479-006-0132-6
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9 (1999) 203–228. https://doi.org/10.1111/1467-9965.00068
• L. G. Epstein, M. Schneider, Recursive multiple-priors, Journal of Economic Theory 113 (2003) 1–31. https://doi.org/10.1016/S0022-0531(03)00097-8
• F. Riedel, Dynamic coherent risk measures, Stochastic Processes and their Applications 112 (2004) 185–200. https://doi.org/10.1016/j.spa.2004.03.004
• P. Cheridito, F. Delbaen, M. Kupper, Coherent and convex monetary risk measures for bounded càdlàg processes, Stochastic Processes and their Applications 112 (2004) 1–22. https://doi.org/10.1016/j.spa.2004.01.009
• F. Delbaen, The structure of m-stable sets and in particular of the set of risk neutral measures, Séminaire de Probabilités XXXIX, Lecture Notes in Mathematics 1874 (2006) 215–258. https://doi.org/10.1007/978-3-540-35513-7_17
• J. Neveu, Discrete-Parameter Martingales, North-Holland, 1975 (French original: Martingales à temps discret, Masson, 1972).
• Y. S. Chow, H. Robbins, D. Siegmund, Great Expectations: The Theory of Optimal Stopping, Houghton Mifflin, 1971; Dover reprint, 1991.

Motivation

In the predict-then-optimize paradigm a model first predicts the cost vector of a linear optimization problem from contextual features, and the prediction is then fed to an optimization solver that returns a decision. Examples include routing with predicted travel times and portfolio choice with predicted returns. The quality of a prediction is judged by the decision it produces. The Smart Predict-then-Optimize (SPO) loss of Elmachtoub and Grigas (Management Science 2022) measures exactly that: the excess cost of acting on the prediction instead of on the true cost vector.

El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3) ask when a model with small empirical SPO loss also has small expected SPO loss. The SPO loss is non-convex and discontinuous, so standard Lipschitz-contraction arguments do not apply to it directly. Their Section 4 introduces a margin version of the SPO loss, in the spirit of the margin theory of Koltchinskii and Panchenko (Ann. Statist. 2002) for classification. They show that it is Lipschitz under a geometric condition on the feasible region, and derive a generalization bound in terms of the multivariate Rademacher complexity of the hypothesis class. This mission formalizes that bound.

Setting

Decisions live in $\mathbb R^d$ with a norm $\|\cdot\|$; cost vectors are linear functionals with the dual norm $\|c\|_*=\max_{\|w\|\le1}c^\top w$. The feasible region $S\subseteq\mathbb R^d$ is nonempty, compact and convex, and throughout Section 4 it is not a singleton. An optimization oracle $w^*$ maps each cost vector $c$ to some minimizer $w^*(c)\in\arg\min_{w\in S}c^\top w$. The SPO loss of a prediction $\hat c$ against the realized cost $c$ is

$$\ell_{\rm SPO}(\hat c,c)=c^\top w^*(\hat c)-c^\top w^*(c),$$

and the linear optimization gap is $\omega_S(c)=\max_{w\in S}c^\top w-\min_{w\in S}c^\top w$, with $\omega_S(\mathcal C)=\sup_{c\in\mathcal C}\omega_S(c)$ and $\rho_2(\mathcal C)=\sup_{c\in\mathcal C}\|c\|_2$ for the set $\mathcal C$ of possible true costs.

A cost vector is degenerate if $\min_{w\in S}\hat c^\top w$ has more than one optimal solution; $\mathcal C^\circ$ is the set of degenerate costs. The distance to degeneracy is $\nu_S(\hat c)=\inf_{c\in\mathcal C^\circ}\|c-\hat c\|_*$. The region $S$ has the strength property with parameter $\mu>0$ if

$$\hat c^\top\big(w-w^*(\hat c)\big)\ge\frac{\mu\,\nu_S(\hat c)}{2}\,\|w-w^*(\hat c)\|^2\qquad\text{for all }w\in S\text{ and all }\hat c .$$

For $\gamma>0$ the $\gamma$-margin SPO loss $\ell^\gamma_{\rm SPO}(\hat c,c)$ equals $\ell_{\rm SPO}(\hat c,c)$ when $\nu_S(\hat c)>\gamma$ and $\frac{\nu_S(\hat c)}{\gamma}\ell_{\rm SPO}(\hat c,c)+\big(1-\frac{\nu_S(\hat c)}{\gamma}\big)\omega_S(c)$ otherwise. It dominates the SPO loss.

Data $(x,c)$ are drawn from a distribution $\mathcal D$ on features $\mathcal X$ and costs in $\mathcal C$, and $\mathcal H$ is a class of prediction functions $f:\mathcal X\to\mathbb R^d$. The SPO risk is $R_{\rm SPO}(f)=\mathbb E_{\mathcal D}[\ell_{\rm SPO}(f(x),c)]$ and the empirical margin risk is $\hat R^\gamma_{\rm SPO}(f)=\frac1n\sum_i\ell^\gamma_{\rm SPO}(f(x_i),c_i)$. The multivariate empirical Rademacher complexity is $\hat{\mathfrak R}^n(\mathcal H)=\mathbb E_{\boldsymbol\sigma}\big[\sup_{f\in\mathcal H}\frac1n\sum_i\boldsymbol\sigma_i^\top f(x_i)\big]$ with i.i.d. Rademacher vectors $\boldsymbol\sigma_i\in\{\pm1\}^d$, and $\mathfrak R^n(\mathcal H)$ is its expectation over the sample.

Formalization targets

Goal: Theorem 4, second display (pp. 19–20)

In the $\ell_2$ set-up, under the strength property with $\mu>0$ and for fixed $\gamma>0$, for every $\delta>0$, with probability at least $1-\delta$ over an i.i.d. sample of size $n$, for all $f\in\mathcal H$:

$$R_{\rm SPO}(f)\le\hat R^\gamma_{\rm SPO}(f)+\Big(\frac{2\sqrt2\rho_2(\mathcal C)+2\sqrt2\mu\,\omega_S(\mathcal C)}{\gamma\mu}\Big)\mathfrak R^n(\mathcal H)+\omega_S(\mathcal C)\sqrt{\frac{\log(1/\delta)}{2n}} .$$

Milestones

1. Theorem 3(a): $\|w^*(\hat c_1)-w^*(\hat c_2)\|\le\frac{\|\hat c_1-\hat c_2\|_*}{\mu\min\{\nu_S(\hat c_1),\nu_S(\hat c_2)\}}$.
2. Theorem 3(b): the same Lipschitz-like bound for $\ell_{\rm SPO}(\cdot,c)$, with an extra factor $\|c\|_*$.
3. Theorem 3(c): $\ell^\gamma_{\rm SPO}(\cdot,c)$ is $\frac{\|c\|_*+\mu\,\omega_S(c)}{\gamma\mu}$-Lipschitz for the dual norm.
4. Eq. (7) with $C=\sqrt2$ (Maurer's vector contraction inequality): for $L$-Lipschitz $\Phi_i$ on Euclidean $\mathbb R^d$,

$$\mathbb E_\sigma\Big[\sup_{f\in\mathcal H}\frac1n\sum_i\sigma_i\Phi_i(f(x_i))\Big]\le\sqrt2L\,\hat{\mathfrak R}^n(\mathcal H).$$

5. Theorem 4, first display: for any fixed sample with costs in $\mathcal C$,

$$\hat{\mathfrak R}^n_{\gamma\rm SPO}(\mathcal H)\le\Big(\frac{\sqrt2\rho_2(\mathcal C)+\sqrt2\mu\,\omega_S(\mathcal C)}{\gamma\mu}\Big)\hat{\mathfrak R}^n(\mathcal H).$$

Theorem 3 is stated for a general norm, as in the paper. Eq. (7), Theorem 4 and the goal are Euclidean. The paper's Theorem 5 (p. 20), a version of the goal uniform over $\gamma\in(0,\bar\gamma]$, is not part of this mission.

Significance

The bound replaces the loss-class complexity of the SPO loss, which is controlled only through combinatorial dimensions (Natarajan dimension in the polyhedral case, Section 3 of the paper), by the multivariate Rademacher complexity of $\mathcal H$ itself. For norm-bounded linear hypothesis classes this complexity has mild, even logarithmic, dependence on the dimensions $p$ and $d$ (Section 4.4). The result applies to every feasible region with the strength property. By Section 5 of the paper these include strongly convex sets and polytopes, where $\nu_S$ can also be computed. When most predictions stay far from degeneracy, $\hat R^\gamma_{\rm SPO}\approx\hat R_{\rm SPO}$ and the bound is much sharper than the combinatorial one. It is also a strict generalization of margin bounds for binary classification (Example 7).

The theorem is proved in the paper, which imports two external tools without proof: the Rademacher generalization bound of Bartlett and Mendelson, applied to the margin loss, and Maurer's inequality. To our knowledge none of these results has a machine-checked proof. The mission produces a checked proof of the margin bound and a Lean statement of Maurer's inequality. It also formalizes the strength property and the Lipschitz estimates of Theorem 3, which the companion missions on strongly convex sets and polytopes rely on.

Difficulty

The SPO loss is discontinuous in $\hat c$ at degenerate predictions. The standard route, scalar Ledoux–Talagrand contraction applied to the loss class, therefore fails at the first step. It would fail even for a Lipschitz loss, because it relates the loss class only to a scalar class, and $\mathcal H$ is vector valued. Lipschitz continuity of the margin loss needs the oracle to be stable away from $\mathcal C^\circ$. Convexity and compactness of $S$ alone do not give that: for an $\ell_p$ ball with $2<p<\infty$ the strength property fails for every $\mu>0$ (p. 14). The vector contraction inequality of Maurer (2016) is a nontrivial probabilistic inequality, and its constant $\sqrt2$ must not depend on the dimension $d$. The final concentration step is McDiarmid's inequality for a supremum over a possibly uncountable class, which in a formal proof needs measurability of that supremum.

Formalization scope

The decision space is a finite-dimensional real normed space E. Cost vectors and predictions are continuous linear functionals, StrongDual ℝ E, whose operator norm is the paper's dual norm. In the $\ell_2$ statements E = EuclideanSpace ℝ (Fin d), where the dual norm is Euclidean. Every statement carries the standing assumptions: $S$ nonempty, compact, convex and not a singleton, an arbitrary oracle (no tie-breaking rule), and $\mu>0$, $\gamma>0$. The Lipschitz-like bounds of Theorem 3(a)–(b) are stated multiplied out, because the paper reads $1/0$ as $+\infty$. Expectations over signs are finite averages over sign patterns. $\omega_S(\mathcal C)$ and $\rho_2(\mathcal C)$ are suprema over a nonempty bounded $\mathcal C$ containing the cost almost surely. "With probability at least $1-\delta$" is the statement that the outer $\mathcal D^n$-measure of the failure event is at most $\delta$.

Added hypotheses, all disclosed in the statements: the multivariate Rademacher sums are bounded above (almost surely in the goal) and $\hat{\mathfrak R}^n(\mathcal H)$ is integrable, since otherwise Lean's junk value $0$ would replace an infinite complexity and make the bound false rather than vacuous. Hypotheses $f$ and $\ell_{\rm SPO}(f(x),c)$ measurable, and the uniform deviation and margin Rademacher suprema a.e.-measurable, are also added; the paper is silent on measurability. A singleton $S$ would make $\mathcal C^\circ$ empty and the strength property hold for free; this is excluded explicitly, so the strength property is not vacuous.

A complete development needs the Bartlett–Mendelson symmetrization bound for bounded losses, McDiarmid's inequality, Maurer's inequality, and the Lipschitz and distance-to-degeneracy facts of Section 4.1. Maurer's inequality and the multivariate Rademacher complexity are reusable across vector-valued learning theory. Proofs of any milestone, and of Maurer's inequality in particular, are welcome.

Selected references

• O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, Mathematics of Operations Research, 2023; preprint arXiv:1905.11488v3, 2022. https://arxiv.org/abs/1905.11488
• A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 2022. https://doi.org/10.1287/mnsc.2020.3922
• A. Maurer, A Vector-Contraction Inequality for Rademacher Complexities, Algorithmic Learning Theory (ALT), 2016. https://arxiv.org/abs/1605.00251
• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
• V. Koltchinskii, D. Panchenko, Empirical Margin Distributions and Bounding the Generalization Error of Combined Classifiers, Annals of Statistics 30(1), 2002. https://doi.org/10.1214/aos/1015362183

Motivation

Networks of queues model computer systems, communication networks and manufacturing lines: customers (jobs, packets, parts) move between service centers, wait, receive service and move on. Their equilibrium behaviour determines throughputs, utilizations and response times, and for most networks it can only be computed by solving the full balance equations of a continuous-time Markov chain whose state space grows combinatorially with the number of centers and customers. A product-form network is one whose equilibrium distribution factorizes over the centers; for such networks performance measures can be computed exactly by efficient algorithms (convolution, mean value analysis), and this is the basis of much of classical computer-performance modelling.

Timeline of the main product-form results:

• 1957–1963, Jackson (Oper. Res. 5, 1957; Manag. Sci. 10, 1963): open networks of exponential FCFS queues, one customer class, Poisson arrivals.
• 1967, Gordon and Newell (Oper. Res. 15): the closed single-class exponential case.
• 1975, Baskett, Chandy, Muntz and Palacios (J. ACM 22): several customer classes with class switching, four service disciplines (FCFS, processor sharing, infinite server, preemptive-resume LCFS), service times with rational Laplace transforms at the last three, and open, closed or mixed networks with state-dependent Poisson arrivals. This is the BCMP theorem, the subject of this mission.
• 1975–1979, Kelly (J. Appl. Prob. 12, 1975; Reversibility and Stochastic Networks, Wiley 1979): symmetric queues and quasi-reversibility, a general framework containing the BCMP disciplines.

Setting

A network has $N$ service centers and $R$ customer classes. A class-$r$ customer finishing service at center $i$ next requires center $j$ in class $s$ with probability $p_{i,r;j,s}$ and leaves the network with probability $1-\sum_{j,s}p_{i,r;j,s}$. The pairs $(i,r)$ are partitioned into subchains $E_1,\dots,E_m$ that routing never leaves. Each center has one of four types:

1. FCFS, with an exponential service time of rate $\mu_i$ common to all classes;
2. a single processor-sharing server (each of $n$ customers is served at rate $1/n$);
3. an infinite-server center;
4. a single preemptive-resume LCFS server.

At types 2–4 the class-$r$ service time is Coxian: $u_{ir}\ge1$ exponential stages of rates $\mu_{irl}$, and after stage $l$ the customer continues with probability $a_{irl}$ or finishes with probability $b_{irl}=1-a_{irl}$. The state $S=(x_1,\dots,x_N)$ records the FCFS order of classes at type 1, the number $m_{irl}$ of class-$r$ customers in stage $l$ at types 2 and 3, and the LCFS order of (class, stage) pairs at type 4. External arrivals are Poisson, either with rate $\lambda(M(S))$ depending on the total population $M(S)$ (process A) or with one stream per subchain of rate $\lambda_k(M(S/E_k))$ (process B); an arrival joins center $j$ in class $s$ with probability $q_{js}$. A subchain with $q\equiv0$ is closed and keeps a fixed population $K_k$.

With relative arrival rates $e_{ir}\ge0$ solving the traffic equations $\sum_{(i,r)}e_{ir}p_{i,r;j,s}+q_{js}=e_{js}$ and $A_{irl}=\prod_{j<l}a_{irj}$ (the probability of reaching stage $l$, stages numbered from 0), the paper defines $f_i(x_i)$ per center type and a factor $d(S)$ from the arrival rates.

Formalization targets

Goal: the BCMP theorem (§3.2, pp. 253–254)

$$\pi(S)=d(S)\,f_1(x_1)\,f_2(x_2)\cdots f_N(x_N)$$

satisfies the global balance equations of the network, and, under the paper's assumption that the equilibrium distribution is unique, every equilibrium distribution equals $\pi/Z$ whenever $Z=\sum_S\pi(S)$ is finite and positive. The goal covers all four center types, open, closed and mixed networks, and both arrival processes.

Milestones

• §3.1 (p. 252): independent balance implies global balance.
• §3.2 (p. 254): the product form satisfies the independent balance equations.
• §4.1 (p. 254): the aggregate-state probabilities are $C\,d(S)\,g_1(y_1)\cdots g_N(y_N)$.

A further supporting item, also from §4.1 (p. 254), states that summing $f_i$ over local states with fixed class counts gives $g_i$. So $g_i$ depends on the service times only through their means $1/\mu_{ir}=\sum_lA_{irl}/\mu_{irl}$.

Significance

The theorem places the four disciplines, class switching and mixed open/closed populations under one formula. Its corollary in §4.1, that aggregate probabilities depend on service time distributions only through their means (insensitivity), is what makes the model usable with measured mean service times, and it underlies the convolution and mean value analysis algorithms for normalizing constants.

The result is classical and proved on paper. As far as the platform's catalogue shows, it is not formalized: the platform has Kelly's single-class migration process with exponential service, a special case. A machine-checked BCMP theorem would provide a verified multiclass queueing-network model (states, event-driven transition rates, balance equations) on which later results can build: mean value analysis, the state-dependent rates of §5, and the open-network marginals of §4.2.

The printed statement contains an error. The paper defines $A_{irl}=\prod_{j=1}^{l}a_{irj}$ (p. 253). With the branching of its Figs. 1 and 3, this product includes the branch out of stage $l$. For exponential service ($u_{ir}=1$) it gives $A_{ir1}=a_{ir1}=0$, so every $f_i$ of a type 2–4 center with a customer present vanishes, and a closed network of such centers would have no normalizable solution. The mission states the corrected theorem with $A_{irl}=\prod_{j<l}a_{irj}$, which the mean-service-time identity of §4.1 also requires. The type-2 factor $1/m_{ikl}!$ is read as $1/m_{irl}!$.

Difficulty

The algebra of the paper's proof is local: each independent balance equation reduces to the traffic equations. The difficulty is in making that statement precise for a real state space. The independent balance equations need a consistent labelling of each moving customer by the "stage" it leaves and enters. That labelling has to cover FCFS centers, where per-class labels are inconsistent (p. 253), the outside world of each open subchain, and LCFS preemption. Every in-flow into a state is a sum over predecessor states, and those states differ by list operations (appending at an FCFS tail, pushing on an LCFS head) or by stage-count updates. The factorials in the processor-sharing and infinite-server factors, and the telescoping identity $\sum_lA_{irl}b_{irl}=1$ for departures, must line up exactly with the rates. The obvious shortcut is to check global balance directly for a single class with exponential service. That covers neither class switching, nor Coxian stages, nor mixed networks.

Formalization scope

Centers are Fin N, classes Fin R and subchains Fin m. The class-$r$ stages at center $i$ are Fin (u i r) with u i r : ℕ+, numbered from 0. A local state is an inductive type with three shapes (FCFS list, stage-count array, LCFS list of (class, stage) pairs). The state space is the subtype of configurations whose shapes match the center types and whose closed subchains hold their fixed populations. Transition rates are the sums of the rates of explicit events (arrivals, FCFS completions, stage moves and completions, LCFS moves and completions). Global balance uses tsum; every state has finitely many successors and predecessors with nonzero rate, so these sums are finite. The standing assumptions (substochastic routing closed on subchains, closed subchains with no arrivals and no departures, positive rates, continuation probabilities in $[0,1]$ vanishing at the last stage) are collected in Network.IsValid. Irreducibility of subchains is not assumed, and any nonnegative solution of the traffic equations is allowed. Under process B the product in $d(S)$ runs over open subchains only. Uniqueness of the equilibrium is a hypothesis, as in the paper. The type-1 rate is constant, and the state-dependent rates of Condition 1 and §5 are not covered.

The following formalizations would trivialize the mission and are ruled out: stating only global balance of $\pi$ (satisfied by $\pi\equiv0$), quantifying over arbitrary rate functions instead of the rates built from the network data, and restricting the goal to exponential service or to a single class.

Needed infrastructure: finite-support tsum manipulations, multinomial identities for the §4.1 sums over orderings and stage assignments, and bookkeeping for list and array updates. The model and the balance-equation layer can be reused for later queueing missions. Contributions are welcome on each milestone, on the per-center-type pieces of the independent balance check, and on helper lemmas about the event system.

Selected references

• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, Closed, and Mixed Networks of Queues with Different Classes of Customers, J. ACM 22(2):248–260, 1975. https://doi.org/10.1145/321879.321887
• J. R. Jackson, Networks of Waiting Lines, Operations Research 5(4):518–521, 1957. https://doi.org/10.1287/opre.5.4.518
• J. R. Jackson, Jobshop-like Queueing Systems, Management Science 10(1):131–142, 1963. https://doi.org/10.1287/mnsc.10.1.131
• W. J. Gordon, G. F. Newell, Closed Queuing Systems with Exponential Servers, Operations Research 15(2):254–265, 1967. https://doi.org/10.1287/opre.15.2.254
• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979. http://www.statslab.cam.ac.uk/~frank/rsn.html
• D. R. Cox, A Use of Complex Probabilities in the Theory of Stochastic Processes, Proc. Cambridge Phil. Soc. 51:313–319, 1955. https://doi.org/10.1017/S0305004100030231

Motivation

The combinatorial diameter of a polyhedron is the largest distance, in its vertex-edge graph, between two vertices. It is a lower bound on the number of pivots any edge-following method such as the simplex method needs in the worst case, which is why the polynomial Hirsch conjecture — the diameter of $P = \{x \in \mathbb{R}^n : Ax \le b\}$ is bounded by a polynomial in $m$ and $n$ — is a central open question of linear optimization and discrete geometry. The best general upper bound is quasi-polynomial, $m^{1+\log n}$ (Kalai–Kleitman 1992); the original Hirsch bound $m - n$ is false for polytopes (Santos 2012).

A different line of work bounds the diameter by the arithmetic of the constraint matrix instead of its size. For an integer matrix $A$ let $\Delta$ be the largest absolute value of a sub-determinant of $A$. Dyer and Frieze (1994) showed that for totally unimodular $A$ ($\Delta = 1$) the diameter is polynomial, $O(m^{16} n^3 (\log mn)^3)$. Bonifas, Di Summa, Eisenbrand, Hähnle and Niemeier (SoCG 2012; Discrete Comput Geom 52, 2014) improved and generalized this to $O(\Delta^2 n^4 \log n\Delta)$ for all polyhedra and $O(\Delta^2 n^{3.5} \log n\Delta)$ for polytopes, bounds that do not depend on the number $m$ of inequalities. This mission formalizes the polytope case.

Setting

Let $A \in \mathbb{Z}^{m\times n}$ with rows $a_1,\dots,a_m$, let $b \in \mathbb{R}^m$, and let $P = \{x \in \mathbb{R}^n : Ax \le b\}$. A vertex of $P$ is an extreme point; for a polyhedron this is a point of $P$ at which $n$ linearly independent inequalities are tight. Two vertices $u \ne v$ are adjacent if the segment $[u,v]$ is an edge (a one-dimensional face) of $P$. This gives the polyhedral graph $G_P = (V, E)$, and the diameter of $P$ is at most $B$ if every two vertices are joined by a walk of at most $B$ edges.

$A$ has sub-determinants bounded by $\Delta$ if every $k\times k$ submatrix, for every $k \ge 1$, has determinant in $[-\Delta, \Delta]$. In particular every entry is at most $\Delta$ in absolute value.

For a vertex $v$ the normal cone $C_v$ is the set of objectives $c$ for which $v$ maximizes $c^T x$ over $P$. With $B_n$ the closed unit ball, the volume of a set $U \subseteq V$ of vertices is

$$\mathrm{vol}(U) = \mathrm{vol}\Big(\bigcup_{v\in U} C_v \cap B_n\Big),$$

and the neighbourhood $\mathcal N(I)$ of $I \subseteq V$ is the set of vertices outside $I$ adjacent to a vertex of $I$. A spherical cone is $S = C \cap B_n$ with $C$ closed under non-negative scaling; its dockable surface $D(S)$ is the $(n-1)$-dimensional measure of the part of its boundary inside the open ball. A cone of revolution of angle $0<\theta\le\pi/2$ is $\{x \in B_n : v^T x \ge \cos\theta\,\|v\|\,\|x\|\}$. $P$ is non-degenerate if every vertex has exactly $n$ tight inequalities.

Formalization targets

Goal: Theorem 2 (p. 105)

If $A \in \mathbb{Z}^{m\times n}$ has all sub-determinants bounded by $\Delta$ and $P$ is bounded, then

$$\operatorname{diam}(P) \le 2\Big\lfloor \sqrt{2\pi}\,\Delta^2 n^{5/2}\ln\!\big(2^n\, n!\, n^{n/2}\,\Delta^n\big)\Big\rfloor + 2 \;=\; O(\Delta^2 n^{3.5}\log n\Delta).$$

No non-degeneracy, full-dimensionality or rank condition is assumed, and the bound is uniform in $m$ and $b$.

Milestones

1. Lemma 3 (p. 108): for a vertex $v$ of a non-degenerate polytope, $D(S_v) \le \Delta^2 n^3\,\mathrm{vol}(S_v)$, where $S_v = C_v \cap B_n$.
2. Lemma 4 (p. 109): among spherical cones of a given volume, a cone of revolution has minimum dockable surface.
3. Lemma 5 (p. 110): for a cone of revolution, $D(S) \ge \sqrt{2n/\pi}\,\mathrm{vol}(S)$.
4. Lemma 6 (p. 111): for every measurable spherical cone with $\mathrm{vol}(S) \le \frac12 \mathrm{vol}(B_n)$, $D(S) \ge \sqrt{2n/\pi}\,\mathrm{vol}(S)$.
5. Lemma 1 (p. 105): for a non-degenerate polytope and $I \subseteq V$ with $\mathrm{vol}(I) \le \frac12\mathrm{vol}(B_n)$,

$$\mathrm{vol}(\mathcal N(I)) \ge \sqrt{\tfrac{2}{\pi}}\,\frac{1}{\Delta^2 n^{2.5}}\,\mathrm{vol}(I).$$

6. Eq. (1) (p. 105): if $I_j$ is the set of vertices at graph distance at most $j$ from a vertex $v$ and $\mathrm{vol}(I_j) \le \frac12\mathrm{vol}(B_n)$, then $j \le \sqrt{2\pi}\,\Delta^2 n^{2.5}\ln(2^n/\mathrm{vol}(I_0))$.

Significance

The result. Theorem 2 bounds the diameter of every integral polytope by a polynomial in the dimension and the largest sub-determinant, independently of the number of facets. For totally unimodular matrices, which cover network-flow, bipartite matching and transportation polytopes, it gives $O(n^{3.5}\log n)$, improving the Dyer–Frieze bound by a large polynomial factor. It shows that the obstruction to a polynomial Hirsch bound, if any, must come from matrices with large sub-determinants. The volume-expansion method — measuring breadth-first search by the volume of the normal fan it has covered — was later refined, for instance in the shadow-vertex analysis of Dadush–Hähnle, which improves the dependence on $n$.

Formalizing it. The theorem is proved (2012/2014); no machine-checked proof is known. A formal development needs, on top of Mathlib, the normal fan of a polytope and its relation to the vertex-edge graph, a Hausdorff-measure calculus for cones (surface of a cone in terms of its base), Lévy's isoperimetric inequality on the sphere in a measure-theoretic form, and explicit Gamma-function estimates. Each of these is reusable well beyond this paper.

Difficulty

The combinatorial side is short; the geometry is not. Lemma 4 is the spherical isoperimetric inequality of Lévy, which Mathlib does not have in any form, and which the paper cites rather than proves; the relations between the volume of a spherical cone, the area of its base, its lateral surface and the length of the base's boundary (Eq. (3), "basic integration") are also absent. Lemma 3 depends on the structure of the normal cone of a vertex of a non-degenerate polytope (full-dimensional, simplicial, generated by rows of $A$), none of which is available for Mathlib's extreme points. Lemma 1 depends on the normal fan of a polytope: the normal cones have pairwise disjoint interiors, cover $\mathbb{R}^n$, and share a facet exactly when their vertices are adjacent. The step from non-degenerate to arbitrary polytopes perturbs $b$ and needs the diameter not to decrease, a statement about the vertex-edge graph under perturbation. A shortcut through a finite graph abstraction is not available: the constant depends on the geometry of the normal cones, not only on the graph.

Formalization scope

The polyhedron is Hirsch.Hpoly (rowVec A) b, with rowVec A i the $i$-th row of $A \in$ Matrix (Fin m) (Fin n) ℤ as a vector of EuclideanSpace ℝ (Fin n). Vertices are Set.extremePoints ℝ P, adjacency is Hirsch.Adj, "diameter at most $B$" is Hirsch.DiamLE P B, all from the published Hirsch_model. The normal cone is the published FirstOrderOpt.ConvexTheory.normalCone. Volumes are Lebesgue measure with values in $[0,\infty]$; the dockable surface uses μHE[n-1], the Hausdorff measure normalized to agree with Lebesgue measure on hyperplanes, applied to frontier S ∩ Metric.ball 0 1. $\Delta$ is a natural number and the sub-determinant bound ranges over all sizes $k \ge 1$.

Explicit constants. The paper writes $O(\Delta^2 n^{3.5}\log n\Delta)$ in Theorem 2; the proof on pp. 105–106 yields $2\lfloor K\rfloor + 2$ with $K = \sqrt{2\pi}\,\Delta^2 n^{5/2}\ln(2^n n!\, n^{n/2}\Delta^n)$, from Eq. (1), the bound $\mathrm{vol}(I_0) \ge 1/(n!\,n^{n/2}\Delta^n)$ and the fact that the diameter is at most twice the number of breadth-first-search iterations needed to cover more than half of $B_n$. This explicit bound is the goal. The ratios $D/\mathrm{vol}$ of Lemmas 3, 5, 6 are stated in multiplicative form.

Non-degeneracy is a hypothesis of Lemma 3, Lemma 1 and Eq. (1) only, as in the paper's §1.1, and never of Theorem 2. The neighbourhood $\mathcal N(I)$ excludes $I$; including it would make Lemma 1 trivial, since its constant is below $1$. Lemma 4 is stated against every competitor: for every measurable spherical cone $S$ and every cone of revolution $S^*$ of the same volume, $D(S^*) \le D(S)$; it does not assert existence of a cone of a prescribed volume. The goal is Theorem 2 about the polytope and its graph, not an abstract statement about set families with a volume-expansion property; integrality of $A$ and the bound on minors of every size are both essential (scaling a real matrix down makes $\Delta$ arbitrarily small), and the raw Hausdorff measure μH[n-1] would put Lemmas 3 and 6 on incompatible scales.

Contributions are welcome at every level: the normal fan and its adjacency structure, cone surface formulas, the Gamma estimate $\Gamma(x+\frac12)/\Gamma(x) \ge \sqrt{x-\frac14}$, and a formal Lévy inequality.

Selected references

• N. Bonifas, M. Di Summa, F. Eisenbrand, N. Hähnle, M. Niemeier, On Sub-determinants and the Diameter of Polyhedra, Discrete Comput Geom 52 (2014) 102–115. https://doi.org/10.1007/s00454-014-9601-x
• M. Dyer, A. Frieze, Random walks, totally unimodular matrices, and a randomised dual simplex algorithm, Math. Program. 64 (1994) 1–16. https://doi.org/10.1007/BF01582563
• G. Kalai, D. J. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. Amer. Math. Soc. 26 (1992) 315–316. https://doi.org/10.1090/S0273-0979-1992-00285-9
• F. Santos, A counterexample to the Hirsch conjecture, Annals of Math. 176 (2012) 383–412. https://doi.org/10.4007/annals.2012.176.1.7
• T. Figiel, J. Lindenstrauss, V. Milman, The dimension of almost spherical sections of convex bodies, Acta Math. 139 (1977) 53–94 (Lévy's isoperimetric inequality, Theorem 2.1). https://doi.org/10.1007/BF02392234
• D. Dadush, N. Hähnle, On the shadow simplex method for curved polyhedra, Discrete Comput Geom 56 (2016). https://arxiv.org/abs/1412.6705