Probability

Motivation

Mission IX (09-proportional-fairness-core) formalized proportional fairness (PF) as a control policy and proved the technical core of its stability theory: under a load condition, the PF fluid model is stable (Theorem 10.5), via an entropy Lyapunov function that is genuinely not Lipschitz continuous — a departure from every other stability argument in J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org). A stability theorem for one fixed arrival-rate vector is, on its own, a narrower claim than practitioners actually want: real systems see load that changes over time, and a control policy worth adopting should not need re-tuning every time the mix of traffic shifts. This mission completes Theorem 10.5's proof and turns it into exactly that stronger guarantee — proportional fairness is maximally stable: stable throughout the entire region where any policy could be stable, without knowing the arrival rates in advance — and specializes the result to two concrete network families, bandwidth-sharing networks and queueing networks under head-of-line proportional processor sharing (HLPPS), that were already familiar from earlier in the book under different control policies.

Setting

Fix a unitary network operating under PF control with mean service times $m > 0$, routing matrix $P$, a partition of job classes into demand groups $\{\mathcal I(\ell), \ell \in \mathcal L\}$, and a reduced allocation set $\tilde{\mathcal A} \subset \mathbb R^{\mathcal L}_+$ (all restated from mission IX, Definition 10.3). The entropy Lyapunov function $\varphi(t) := \sum_i Z_i(t)\log(\dot D_i(t)/\alpha_i)$ (Eq. 10.38, mission IX) admits an alternative decomposition $\varphi = \sum_\ell \varphi_\ell$ in terms of the within-group entropy term

$$f(t) := \sum_{\ell\in\mathcal L}\sum_{i\in\mathcal I(\ell)} Z_i(t)\log\!\left(\frac{Z_i(t)}{Y_\ell(t)}\right), \qquad Y(t) := GZ(t) \quad \text{(Eq. 10.50)},$$

with the convention that the term for class $i$ is $0$ when $Z_i(t)=0$. Here $D^+$/$D^-$ denote the upper-right/upper-left Dini derivatives (Appendix A.4, Eqs. A.9-A.10): at a point where the ordinary derivative may not exist, these one-sided $\limsup$s still let a Lyapunov-drift argument go through. A control policy is maximally stable (Section 5.7) for a network if its implementation does not depend on the arrival-rate vector $\lambda$ and it is stable for every $\lambda$ in the network's stability region $\Lambda^*$ — the largest region any policy could possibly stabilize.

Formalization targets

Goal: Corollary 10.16 — maximal stability of PF control for a unitary network

$$\text{IsMaximallyStable}\Big(\lambda \mapsto \text{PFFluidStable}(\lambda, m, P, \mathrm{grp}, \tilde{\mathcal A})\Big)$$

for the single PF policy value (its implementation never depends on $\lambda$). This is the applied payoff of Theorem 10.5 (mission IX): combined with Theorem 6.2 (mission III, fluid stability implies SPN stability) and Corollary 5.6 (mission II, a $\lambda$-independent policy stable throughout the subcritical region is automatically maximally stable), it upgrades a single-$\lambda$ stability statement to the strongest form the book's own framework can express.

Supporting milestones

Lemmas 10.11-10.15 supply the remaining technical content of Theorem 10.5's proof that mission IX's own milestones left open: Lemma 10.11 is the uniform negative-drift bound $\sum_i \dot Z_i(t)\log(\dot D_i(t)/\alpha_i) \le -\varepsilon$ at every regular point with $Z(t) \ne 0$; Lemmas 10.12-10.14 establish continuity and two successively sharper Dini-derivative bounds on the within-group entropy term $f$; Lemma 10.15 shows that positivity of the departure rate $\dot D_i(t)$ propagates from occupied classes to every class. Corollaries 10.17 and 10.18 specialize the goal to bandwidth-sharing networks and to HLPPS-controlled queueing networks, respectively.

Significance

The result itself. A stability theorem tied to one fixed $\lambda$ is of limited practical use: it would need to be re-verified every time the arrival-rate vector changes, which real traffic does constantly. Maximal stability removes that dependency entirely — a single policy, implemented without any knowledge of $\lambda$, is guaranteed stable throughout the full region any control could stabilize. Corollaries 10.17 and 10.18 make this concrete for two network families with independent histories in the literature: bandwidth-sharing networks (the original motivation for proportional fairness, Kelly 1997) and queueing networks under HLPPS, connecting PF's static, utility-theoretic motivation to a scheduling rule that predates it.

Formalizing it. A live prior-art check (GET /theorems?q=proportional%20fairness, q=maximal%20stability, q=bandwidth%20sharing) finds no relevant hits on the platform. This mission formalizes the remaining entropy-Lyapunov lemmas, the within-group entropy term, the BWS and HLPPS network models (restated locally, since no other drafted chunk covers Sections 4.5-4.6), and the maximal-stability predicate, reusing only Mathlib's general real-analysis substrate (Dini derivatives via Filter.limsup) and definitions restated from missions II, III, V, and IX under this series' restate-not-import convention for concurrently-drafted chunks.

Difficulty

The obvious approach to Corollary 10.16 — restate "maximally stable" with an explicit $\lambda$-dependent policy family and add "the policy doesn't actually depend on $\lambda$" as a side hypothesis — obscures the point: a policy that is definitionally independent of $\lambda$ is a stronger and cleaner claim than one that happens to satisfy an extra equation. This formalization instead instantiates the abstract policy type at Unit, so $\lambda$-independence holds by construction rather than as a hypothesis to verify, matching the book's own reading of Section 5.7's definition. A second difficulty is Lemma 10.13's Dini-derivative inequality (Eq. 10.56): the plain-text extraction of this display equation loses bracket and subscript structure that changes its meaning, so the exact grouping was confirmed against the PDF page directly and cross-checked against the book's own re-derivation of the same bracketed expression inside Lemma 10.14's proof. A third is Corollary 10.17's proof, which genuinely depends on three facts outside this chunk's own chapter portion (Proposition 4.4 and the Section 4.4 model translation, Proposition 5.1, Theorem 5.2); rather than silently assuming them or re-deriving their proofs from scratch, they are stated as explicit hypotheses of the milestone itself, so the item's actual content — deriving the two-sided conclusion — is exactly what remains to be proved.

Formalization scope

RestatedCore, RestatedFluidModel, and the maximal-stability predicate MaximalStability are restated verbatim (or, for MaximalStability, in shape) from missions IX, III/V, and II respectively, since concurrently-drafted chunks in this series do not import one another's Lean files even when they share a sub-namespace. New to this chunk: diniUpperLeft (Eq. A.10, needed alongside mission IX's diniUpperRight for Lemma 10.13's two-sided bound), the within-group entropy term withinGroupEntropy (Eq. 10.50, deliberately not named f, since the book's own f already denotes the unrelated PF optimization objective of Eq. 10.2 within the same chapter), and BWSNetworkData/QueueingNetworkDataHL/HLPPSFluidStable (Sections 4.5-4.6, restated locally since no drafted chunk's BRIEF.md covers them). The formalization does not admit a trivializing reading: IsMaximallyStable is instantiated with the genuine, non-vacuous predicate PFFluidStable/HLPPSFluidStable — the same predicate whose stability Theorem 10.5 (mission IX) already establishes on the load-condition region — never with a policy type or stability predicate engineered to make the maximal-stability claim vacuous. Contributions completing the eight by sorry proofs are welcome, particularly Lemma 10.13's Dini-derivative estimate (Section B.4's preliminary results) and Lemma 10.15's connectivity argument (Appendix B.9/B.17).

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• F. P. Kelly, "Charging and rate control for elastic traffic," European Transactions on Telecommunications 8 (1997), 33–37.
• F. P. Kelly, A. K. Maulloo, and D. K. H. Tan, "Rate control for communication networks: shadow prices, proportional fairness and stability," Journal of the Operational Research Society 49 (1998), 237–252.

Motivation

Dynamic pricing under limited inventory is a core problem of revenue management: a seller holds $C_0$ units of a perishable product (airline seats, hotel rooms, seasonal goods) and must choose prices over a finite selling horizon while demand is random and responds to price. The exactly optimal policy solves a stochastic dynamic program whose state is the remaining inventory, and it changes the price after every sale. In practice sellers often prefer a simpler rule, fixed in advance: solve the deterministic version of the problem, in which random demand is replaced by its mean, and charge the resulting prices whatever happens.

Gallego and van Ryzin (Management Science 1994) showed that in continuous time with Poisson demand this fixed-price heuristic is asymptotically optimal, and bounded its relative loss by the coefficient of variation of demand. Bitran and Caldentey's survey (MSOM 2003, §3.2.1) extends this bound to a discrete-time, periodic-review model with general demand distributions, as Proposition 8, proved in the paper's Appendix. The proof combines three ingredients: a Lagrangian duality argument showing that the deterministic problem is an upper bound on the optimal expected revenue, a sample-path comparison of lost sales, and a distribution-free moment bound of Gallego (1992) on $E[(X-C)^+]$.

Setting

A single product is sold over $N \ge 1$ periods $n = 1, \dots, N$ starting from inventory $C_0$. In period $n$ the seller charges a price $p \ge 0$, and the demand $D_n(p)$ is a nonnegative random variable with finite mean $E[D_n(p)]$, whose law may depend on $n$ and $p$ arbitrarily. With inventory $C$ the seller sells $\min\{D, C\}$ units; unmet demand is lost.

The optimal expected revenue $V_1(C_0)$ is defined by the Bellman recursion $V_{N+1} \equiv 0$,

$$V_n(C) = \sup_{p \ge 0} E\big[p\min\{D_n(p), C\} + V_{n+1}\big(C - \min\{D_n(p), C\}\big)\big].$$

The deterministic problem (32)–(33) is

$$V_1^{\det}(C_0) = \sup_{p \in [0,\infty)^N} \sum_{n=1}^N p_n E[D_n(p_n)] \quad \text{subject to} \quad \sum_{n=1}^N E[D_n(p_n)] \le C_0,$$

and $p^{\det}$ denotes an optimal solution. The deterministic-price heuristic charges $p^{\det}_n$ in period $n$ regardless of sales. Its period demands $D_n(p_n^{\det})$ are independent, $\mathscr{D}_n^{\det} = \sum_{i=1}^n D_i(p_i^{\det})$ is the cumulative demand, and its expected revenue is

$$V_1(p^{\det}, C_0) = \sum_{n=1}^N p_n^{\det} E\Big[D_n(p_n^{\det}) - \big(D_n(p_n^{\det}) - (C_0 - \mathscr{D}_{n-1}^{\det})^+\big)^+\Big].$$

With $\sigma_n^2 = \operatorname{Var}(\mathscr{D}_n^{\det})$, eq. (34) defines

$$\eta_n^{\det}(C_0) = \frac{\sqrt{\sigma_n^2 + (C_0 - E[\mathscr{D}_n^{\det}])^2} - (C_0 - E[\mathscr{D}_n^{\det}])}{2},$$

and $\nu(C_0) = \sigma_N / E[\mathscr{D}_N^{\det}]$ is the coefficient of variation of the total demand.

Formalization targets

Goal: Proposition 8, eq. (35)

Assume that $p \mapsto p\,E[D_n(p)]$ is concave and $p \mapsto E[D_n(p)]$ is convex on $[0,\infty)$ for each $n$, that some price $p^\infty \ge 0$ has $\sum_n E[D_n(p^\infty)] < C_0$, and that $p^{\det}$ is optimal for (32)–(33). Then

$$1 \ge \frac{V_1(p^{\det}, C_0)}{V_1(C_0)} \ge \frac{1}{V_1^{\det}(C_0)} \sum_{n=1}^N p_n^{\det} E[D_n(p_n^{\det})]\left(1 - \frac{\eta_n^{\det}(C_0)}{E[D_n(p_n^{\det})]}\right) \ge 1 - \max_n \frac{\eta_n^{\det}(C_0)}{E[D_n(p_n^{\det})]}.$$

The constants are the paper's, and the goal is the full chain.

Milestones

1. Gallego's bound (Appendix, (*)): for square-integrable $X$, $E[(X - C)^+] \le \frac12\big(\sqrt{\operatorname{Var}X + (C - EX)^2} - (C - EX)\big)$, which is at most $\frac12\sqrt{\operatorname{Var} X}$ when $EX \le C$.
2. Eq. (24): in one period, $E[p\min\{D(p), C\}] \le p\min\{E[D(p)], C\}$, so $V(C) \le V^{\det}(C)$.
3. Proposition 6, eq. (26): in one period, $V(C, p^{\det})/V(C) \ge 1 - \nu^{\det}/2$.
4. $V_1^{\det}$ is concave in the capacity (first sentence of the Appendix proof).
5. Proposition 8, first assertion: $V_1(C_0) \le V_1^{\det}(C_0)$.
6. The Appendix display bounding $V_1(p^{\det}, C_0)$ below by $\sum_n p_n^{\det}E[D_n](1 - E[(\mathscr{D}_n^{\det} - C_0)^+]/E[D_n])$.
7. Eq. (36), after the goal: if $E[D_n(p)] = T_n\lambda(p)$, one constant price solves (32)–(33) and $1 \ge V_1(p^{\det},C_0)/V_1(C_0) \ge 1 - \nu(C_0)/2$.

Significance

The result gives a guarantee for a pricing policy that needs no inventory tracking: its relative loss is controlled by the first two moments of cumulative demand, with no distributional assumption beyond finite variance. When demand grows while its coefficient of variation shrinks, as for sums of independent period demands, the guarantee tends to one, which is the discrete-time form of asymptotic optimality of fixed prices. The upper bound $V_1 \le V_1^{\det}$ is used throughout revenue management as the benchmark for heuristics (fluid or deterministic LP bounds).

The paper's proof is complete in the Appendix, and the mathematics is not in question beyond minor typos. None of it is machine-checked. A formal development adds a checked Bellman model of periodic-review pricing with general demand laws, a checked fluid upper bound for it, and a checked form of Gallego's moment bound, all reusable for other revenue-management statements. A related platform theorem, RevenueManagement.deterministic_upper_bound (mission The Theory and Practice of Revenue Management III), states the deterministic bound for a Bernoulli-arrival model with at most one sale per period; the model here is different (arbitrary demand laws, continuous inventory), and neither statement implies the other.

Difficulty

The upper bound $V_1(C_0) \le V_1^{\det}(C_0)$ is the hard part. The natural induction replaces $V_2$ by $V_2^{\det}$ and applies Jensen's inequality, but $V_2^{\det}(C)$ is $-\infty$ at capacities where the remaining deterministic problem is infeasible, while $V_2(C)$ stays nonnegative. The induction therefore fails as stated when mean demand never vanishes. The paper's argument also passes through the Lagrangian dual of (32)–(33), and strong duality for that program on $[0,\infty)^N$ under the Slater point $p^\infty$ is not available in Mathlib in this form.

The lower bound is less deep but technical: it needs the product law of the period demands, linearity of expectation for truncated sums, and variances of partial sums. Gallego's inequality is elementary once the right quadratic bound on $(x - C)^+$ is found, but it is not in Mathlib.

Formalization scope

• Periods are Fin N, 0-based. Demand laws are μ n p : Measure ℝ, probability measures carried by $[0,\infty)$ with finite mean, required at every price (laws at negative prices never enter a statement).
• The Bellman value is computed in $[0,\infty]$ with the lower Lebesgue integral and ⨆ over $p \ge 0$, so no supremum takes a junk value; the paper's $V_n$ is valueToGo M (N - n + 1). Ratios use its real value.
• $V_1^{\det}$ is an EReal supremum over the feasible set ($-\infty$ if infeasible). In the goal $p^{\det}$ is an optimal solution, so $V_1^{\det}(C_0)$ is its objective value.
• The heuristic's demands are independent: the joint law is the product measure.
• Implicit hypotheses made explicit: "concave objective and convex feasible region" is read as concavity of $p\,E[D_n(p)]$ and convexity of $E[D_n(p)]$ on $[0,\infty)$, the latter making (33) convex for every capacity; existence of the optimal deterministic solution; finite variance and positive mean of each $D_n(p_n^{\det})$; and $V_1^{\det}(C_0) > 0$, without which the ratios are $0/0$.
• The typo $\mathscr{D}_n^{\det} := \sum_{i=1}^n D_n(p^{\det})$ on p. 221 is read as $\sum_{i=1}^n D_i(p_i^{\det})$.

Trivializing formalizations ruled out: $V_1$ is defined by the Bellman recursion, not as a supremum over an unspecified policy class or as a variable constrained by hypotheses; $\eta_n^{\det}$ is the expression (34), not a hypothesis-supplied bound on expected overflow; the goal does not assume strong duality or a Lagrange multiplier, since that is the proof's key step; independence is built into the joint law, not assumed as an inequality; variances are taken only under square integrability, since Mathlib's variance is $0$ for infinite variance.

Needed infrastructure: measurability of the Bellman integrand (monotonicity of $V_n$ in inventory), Jensen's inequality for $\min\{\cdot, C\}$ (ConcaveOn.le_map_integral), Lagrangian strong duality for a separable concave program with one convex constraint, marginals and variances of sums under Measure.pi, and Gallego's bound. The duality and moment results are reusable beyond this mission. Proofs of any milestone, and alternative proofs of the upper bound, are welcome.

Selected references

• G. R. Bitran, R. Caldentey, An Overview of Pricing Models for Revenue Management, Manufacturing & Service Operations Management 5(3):203–230, 2003. https://doi.org/10.1287/msom.5.3.203.16061
• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• G. Gallego, A Minmax Distribution Free Procedure for the (Q, R) Inventory Model, Operations Research Letters 11(1):55–60, 1992 (as cited in Bitran and Caldentey 2003).
• M. S. Bazaraa, H. D. Sherali, C. M. Shetty, Nonlinear Programming: Theory and Algorithms, 2nd ed., Wiley, 1993.

Motivation

Every control policy formalized so far in this series — HLSPS (mission VI), back-pressure/ max-weight (mission VIII) — allocates service effort to entire job classes as indivisible units. Proportional fairness takes a different starting point: it is a general-purpose recipe for dividing a shared, continuously divisible resource among competing demands, originally developed for bandwidth allocation in communication networks and later adopted throughout economics and operations research as the canonical notion of a "fair" allocation. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 10 to showing that proportional fairness, applied dynamically to a processing network's current buffer contents, is not just an attractive fairness criterion but a maximally stable control policy — stable throughout the entire subcritical region of any unitary network. This mission formalizes the static optimization problem underlying proportional fairness, its key structural properties, the resulting fluid model, and the deepest single theorem of the chapter: fluid stability under the standard load condition, proved via a Lyapunov function that is explicitly not Lipschitz continuous — a genuine departure from every other stability proof in the book.

Setting

The PF allocation function $\psi(z)$ solves, for a demand vector $z \in \mathbb R^I_+$, the concave optimization problem $\max_{x \in \mathcal A} \sum_i z_i \log(x_i)$ (Eq. 10.3-10.4) over a bounded, closed, convex, monotone capacity-constraint set $\mathcal A$. When $\mathcal A$ has the special "aggregate" structure induced by grouping classes with identical resource requirements into demand groups, $\psi$ satisfies a resource-relevant aggregation property (Proposition 10.2): its value depends on the full demand vector only through group-level aggregates. Applying $\psi$ dynamically — recomputing it from the current buffer-content vector at every decision time — to a unitary network (one-to-one correspondence between job classes and service types) under relaxed control defines the PF control policy, whose fluid limit is the PF fluid model (Definition 10.3, Eqs. 10.29-10.35).

Formalization targets

Goal: Theorem 10.5 — fluid stability of the PF control policy

If the load condition (10.37) — an equivalent, group-level-aggregate reformulation of the standard load condition $\rho < b$ — holds, then the PF fluid model is stable. Combined with Theorem 6.2 (mission III) and Corollary 5.6, this is the technical core of showing PF control is maximally stable, exactly the same shape of result as mission VIII's back-pressure theorem, but for a policy defined by a fundamentally different (utility-maximization, rather than weighted-throughput-maximization) principle.

Supporting milestones

Lemma 10.1 establishes that $\psi$ is well-defined at all (existence), essentially unique where it matters (uniqueness on positive-demand coordinates), extreme, scale-invariant, and continuous — six properties that everything downstream depends on. Proposition 10.2 is the aggregation property described above. Proposition 10.4 restates the standard load condition in the group-level-aggregate coordinates Theorem 10.5's proof actually uses. Lemmas 10.6, 10.7, 10.8, and 10.9 develop the properties of the entropy Lyapunov function $\varphi(t) := \sum_i Z_i(t)\log(\dot D_i(t)/\alpha_i)$ (Eq. 10.38) that Theorem 10.5's proof needs: nonnegativity (and strict positivity away from the origin), continuity on $(0,\infty)$, a uniform upper bound on its Dini derivative, and a pointwise bound on that derivative at regular points, in terms of the fluid-scale departure and content rates.

Significance

The result itself. Theorem 10.5 shows that proportional fairness — motivated purely by a static fairness axiom (Eq. 10.14) with no reference to queueing dynamics at all — turns out to be a maximally stable dynamic control policy once applied recursively to a unitary network's evolving buffer contents. This is a substantive and non-obvious fact: nothing in PF's static definition anticipates a stability guarantee, and the book's own text stresses the mismatch between PF's static motivation (utility/fairness) and the metric of interest for a queueing system (buffer content, response time). Unlike essentially every other stability proof in the book, Theorem 10.5's proof uses a Lyapunov function ($\varphi$) that is provably not absolutely continuous, which is why it needs Lemma 8.11's more delicate Dini-derivative extinction criterion (mission V) rather than the simpler Lipschitz-based criteria (Lemmas 8.5/8.6) used everywhere else.

Formalizing it. A live prior-art check (GET /theorems?q=proportional%20fairness, q=entropy, q=concave%20optimization) finds no relevant hits — the one "entropy" result on the platform is an unrelated matrix-multiplication construction. This mission formalizes the concave PF optimization problem, its allocation function, the aggregation property, and the entropy Lyapunov machinery entirely from scratch, reusing only Mathlib's general convex-analysis and EReal substrate.

Difficulty

The chapter's own convention $\log(0) = -\infty$, $0\log(0) = 0$ (Eq. 10.2) cannot be captured by Mathlib's Real.log, whose value at 0 is 0, not -\infty — a silent substitution would corrupt exactly the boundary behavior Lemma 10.1(a)'s existence/uniqueness argument turns on (distinguishing feasible points with $x_i=0$ for some $i \in \mathcal I_+(z)$, which must be strictly dominated, from those without). This mission instead defines the PF objective via EReal, using an explicit extended logarithm (⊥ at 0) and Mathlib's own convention that EReal multiplication satisfies 0 * y = 0 for every y — which reproduces the book's 0 log(0) = 0 rule automatically, with no case split, a pleasant instance of genuine Mathlib substrate reuse resolving what looked like a from-scratch formalization problem. A second difficulty is structural: $\psi$ is not merely "a maximizer" but a specific maximizer, normalized to zero on every coordinate with zero demand (Eq. 10.5) — needed so that Lemma 10.1(c)/(d)'s scale-invariance and continuity statements are about a genuine function of $z$, not merely about an arbitrarily-chosen selection from a possibly-multivalued correspondence.

Formalization scope

IsPFDomain, f, IsPFMaximizer, and psi formalize Section 10.1's optimization problem directly, with IsPFMaximizer phrased as "feasible and dominates every feasible alternative" (avoiding sSup/⨆ entirely, per this series' junk-value-avoidance convention). IsTotalArrivalRates (restating Eq. 2.38) and RegularPoint (restating Definition 8.7) are restated locally, matching this series' convention that drafts do not import one another. diniUpperRight duplicates mission V's LyapunovCriteria.diniUpperRight verbatim — this chunk's own BRIEF.md dependency list does not include mission V, so, per the same restate-not-import convention, it is restated here rather than cross-imported (the duplication is intentional and documented, not an oversight). Lemma 10.7 (continuity of $\varphi$ on $(0,\infty)$) is added beyond BRIEF.md's own disposition table: the book itself lists it as one of "the following five lemmas" (10.6, 10.7, 10.8, 10.9, 10.11) that suffice to prove Theorem 10.5, on the same page as Lemmas 10.6/10.8/10.9 — a planning-time omission caught during drafting and documented in HARD.md. Lemma 10.11 itself, though stated on the same page, is not included here: the companion chunk (10-proportional-fairness-applications) explicitly begins at "Lemma 10.11 onward," and its own negative-drift conclusion is exactly what completes Theorem 10.5's proof — a dependency this mission's goal theorem does not need to expose in its own statement, since (10.37) is already the theorem's complete, book-stated hypothesis. IsPFDomain, IsPFMaximizer, psi, groupAggregate, IsPFFluidModelSolution, and phi are the primary reusable contributions; contributions completing the eight by sorry proofs, especially Lemma 10.1's six-part argument and the entropy-Lyapunov lemmas' analysis (Section B.4's preliminary results), are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• F. P. Kelly, A. K. Maulloo, and D. K. H. Tan, "Rate control for communication networks: shadow prices, proportional fairness and stability," Journal of the Operational Research Society 49 (1998), 237–252.
• R. Srikant and L. Ying, Communication Networks: An Optimization, Control, and Stochastic Networks Perspective, Cambridge University Press, 2014.

Motivation

Every stability result up through mission VII proves that a particular control policy — a fixed priority list, HLSPS, a policy tailored to one network's topology — keeps a specific processing network stable throughout its subcritical region. None of them answer a more practical question a system designer actually faces: given an arbitrary Leontief network (one where every activity has a well-defined, unique buffer it draws from), is there a single control rule, computable from the network's data alone with no bespoke analysis, that is guaranteed stable whenever stability is possible at all? J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) answers this in Chapter 9 with the back-pressure (equivalently, in the single-hop case, max-weight) control policy: at every decision time, choose the allocation of service effort that maximizes a bilinear "weighted throughput" objective built directly from current buffer contents. This mission formalizes the policy, the characteristic fluid equation it induces, and the resulting maximal-stability theorem — the chapter's central result and one of the most cited scheduling policies in the queueing-networks literature.

Setting

A Leontief network (Definition 9.5) is an SPN whose input-output matrix $R$ satisfies two assumptions: Assumption 9.1, that each activity has a unique buffer it draws material from (so $i(j)$, the buffer served by activity $j$, is well-defined), and Assumption 9.2, that there is a nonnegative activity-level vector driving every buffer's net output rate strictly positive — the structural condition under which the network can be drained at all. The back-pressure (or, in the single-server, single-hop case, max-weight) control policy chooses, at each decision time, the feasible allocation $\beta$ of service rates that maximizes the bilinear objective $p(\beta, \hat z) = \hat z \cdot R\beta$, where $\hat z$ is the current vector of buffer contents. The "relaxed" version of the policy allows $\beta$ to range continuously over the allocation polytope $\mathcal A = \{\beta \in \mathbb R^J_+ : A\beta \le b\}$; the "basic" version restricts to integer service-initiation decisions in a genuine SPN with discrete jobs. A network's static planning problem's optimal value $\gamma^* < 1$ is the subcriticality condition throughout this chapter, exactly as in missions II, III, and V.

Formalization targets

Goal: Theorem 9.12 — maximal stability of relaxed back-pressure

Consider a Leontief network operating under the relaxed back-pressure control policy. If the static planning problem has optimal objective value $\gamma^* < 1$, then the corresponding fluid limit is stable, and hence, by Theorem 6.2 (mission III), the network's ambient Markov chain is positive recurrent. This is the chapter's payoff: back-pressure control needs no network-specific tuning — it stabilizes every Leontief network throughout its entire subcritical region, the same universal guarantee mission VI showed only for feedforward networks and HLSPS control specifically.

Supporting milestones

Lemma 9.3 and Proposition 9.4 develop the linear-algebraic machinery of basis matrices: any feasible material-balance vector can be re-expressed using only $I$ "basic" activities (Lemma 9.3), and Assumption 9.2 holds if and only if some basis's associated matrix has spectral radius below one (Proposition 9.4) — the practical, checkable criterion for the network being well-posed at all. Proposition 9.6 shows the back-pressure optimization problem always admits a solution among the finitely many extreme allocations, licensing Remark 9.7's standing convention of restricting attention to that finite set. Lemma 9.10 shows a $z$-maximal extreme allocation can always be chosen to idle any activity whose buffer is currently empty — a fact that looks obvious but genuinely needs proof, because at the fluid level an activity can serve an instantaneously empty buffer at a positive rate (Section 9.5's tandem-model illustration). Theorem 9.8 is the chapter's characteristic fluid equation: under relaxed back-pressure control, the realized fluid service-rate derivative always achieves the bilinear maximum over the allocation polytope, at every regular point. Lemma 9.11 derives this from the raw ("pre-limit") stochastic dynamics — a strictly dominated allocation accrues no processing time — via a genuine limit-passage argument. Theorem 9.13 and Lemma 9.14 extend the maximal-stability guarantee from the relaxed policy to the basic (discrete-decision) policy, under the extra restriction that each server pool is a single server acting alone; this needs a residual-time strong law of large numbers (Lemma 9.14) to show that a server's decision to switch away from a dominated allocation happens quickly enough, relative to elapsed time, that the fluid limit is unaffected.

Significance

The result itself. Theorem 9.12 is the book's formalization of the max-weight/back-pressure maximal-stability theorem originally due to Tassiulas and Ephremides (1992) for multi-hop packet radio networks, later popularized under the "back-pressure" name by Tassiulas (1995) and extended substantially by Dai and Lin (2005), on whose work this chapter is explicitly based. Unlike every policy considered in missions IV, VI, and VII, back-pressure requires no topology-specific insight to design or verify — it is defined uniformly from $B$, $\Gamma$, $A$, and current buffer contents, and Theorem 9.12 certifies it stable for every Leontief network in its subcritical region. This universality is precisely what distinguishes it from HLSPS (mission VI), which needs the network to be feedforward or the policy to be head-of-the-line proportional-sampling before the same guarantee holds.

Formalizing it. A live prior-art check (GET /theorems?q=max-weight%20scheduling, q=back-pressure) returns no hits, so this mission formalizes the policy, its characteristic fluid equation, and both stability theorems entirely from scratch. SPNPlanningData, the input-output matrix R, and the static planning problem are restated from mission II's own apparatus; RegularPoint is restated from mission V's Definition 8.7.

Difficulty

The chapter's central subtlety is that "operating under back-pressure control" cannot be stated directly as a hypothesis on the fluid-limit path $(\hat D,\hat F,\hat T,\hat Z)$ itself: the policy is defined in terms of the discrete, pre-limit decision process, and its fluid-level consequence — the characteristic equation (9.22) — is a genuine theorem (9.8), not a restatement of the policy's definition. Formalizing Theorem 9.8 naively by hypothesizing "$\hat T$ satisfies (9.22)" would make Lemma 9.11 (whose conclusion (9.28)-(9.31) is what Theorem 9.8's own proof literally invokes) circular relative to it. This mission instead hypothesizes Lemma 9.11's raw, pre-limit optimality condition (hYopt: a strictly dominated allocation accrues no processing time over any interval where domination persists) as the operational meaning of "following the back-pressure rule," and derives (9.28)-(9.31) from it as Lemma 9.11's genuine conclusion — Fed into Theorem 9.8 exactly as the book's own proof does ("By Lemma 9.11 and the fact that $\sum_\beta \dot{\hat Y}_\beta(t) = 1$..."). A second difficulty is Theorem 9.13's genuinely distinct proof from Theorem 9.12's: the basic (discrete) policy's fluid limit satisfying the same characteristic equation is not automatic, and needs the residual-time SLLN of Lemma 9.14 plus two extra structural hypotheses (each server pool is a single server, each activity uses exactly one server) that go beyond "basic vs. relaxed" and are stated explicitly rather than folded silently into the policy's name.

Formalization scope

SPNPlanningData, its input-output matrix R, and the static planning problem (SPPFeasible, IsOptimalSPPValue) are restated unmodified from mission II's own apparatus (drafts in this series do not import one another); RegularPoint is restated unmodified from mission V's Definition 8.7. "Basis" is named ActivityBasis, not Basis, to avoid colliding with Mathlib's vector-space Basis type — a deliberate departure from the book's own overloaded terminology, which its own text flags as "slightly narrower than [the] standard meaning in linear programming theory." ExtremeAllocations reuses Mathlib's Set.extremePoints directly rather than restating extreme-point theory from scratch, and Proposition 9.4's spectral-radius condition reuses Mathlib's own spectralRadius (Mathlib.Analysis.Normed.Algebra.Spectrum) rather than defining eigenvalues by hand. IsZMaximal (Definition 9.9) is phrased as "feasible and dominates every feasible alternative" rather than via an explicit sSup/⨆ expression, which sidesteps any Mathlib junk-value risk while remaining definitionally equivalent to "achieves the maximum" whenever a maximizer exists — the same convention this series has used since mission III. Theorem 9.8's hypothesis that the fluid limit "operates under relaxed back-pressure control" is packaged as Lemma 9.11's own conclusion (hTY/hYmono/hYsum/hYopt), matching the book's proof architecture exactly rather than re-deriving it inline. Theorem 9.13 states its two extra single-server hypotheses (hb1, hA01) explicitly as the mission's own BRIEF.md warns to. Lemma 9.14's condition (9.44) — quoted in the book's preparatory material for Theorem 9.13 rather than in the excerpt originally assembled for this lemma — was located directly in source.txt (p. 178, PDF p. 194) and confirmed verbatim, not reconstructed; its formalization (h944) matches the confirmed text exactly. The one acknowledged source inconsistency, noted by BRIEF.md itself, is that (9.56)'s printed left-hand side reads u_i(s,ω) where the surrounding proof otherwise uses t throughout — treated as a typesetting slip and formalized with t, as the lemma evidently intends. IsFluidModelSolution, IsRelaxedBPFluidSolution, RelaxedBPFluidStable, ActivityBasis, AllocationPolytope, and IsZMaximal are the primary reusable contributions; contributions completing the nine by sorry proofs, especially Lemma 9.11's limit-passage argument and Lemma 9.14's SLLN chain, are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• L. Tassiulas and A. Ephremides, "Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks," IEEE Transactions on Automatic Control 37 (1992), 1936–1948.
• J. G. Dai and W. Lin, "Maximum pressure policies in stochastic processing networks," Operations Research 53 (2005), 197–218.

Motivation

In supervised binary classification, a hypothesis class is learnable if and only if it has uniform convergence, meaning that empirical risks converge to true risks uniformly over the class. When that holds, empirical risk minimisation (ERM) learns. This equivalence, due to Vapnik and Chervonenkis and extended to real-valued losses by Alon, Ben-David, Cesa-Bianchi and Haussler, is the usual starting point of statistical learning theory.

Vapnik's General Learning Setting is broader. It covers stochastic convex optimisation, clustering and density estimation, and in it the equivalence breaks down. Shalev-Shwartz, Shamir, Srebro and Sridharan (JMLR 11 (2010) 2635–2670) exhibit learnable problems with no uniform convergence, and learnable problems where ERM fails. So neither uniform convergence nor the success of ERM characterises learnability there, and something else has to. This mission formalizes the paper's answer, its Theorem 7: stability.

Timeline:

• 1971–1995: Vapnik and Chervonenkis prove learnability ⇔ uniform convergence for binary classification. Vapnik (1995) introduces the General Learning Setting.
• 2002: Bousquet and Elisseeff show that uniform stability of a learning rule implies generalization.
• 2006: Mukherjee, Niyogi, Poggio and Rifkin show that, in the supervised setting, stability of ERM is necessary and sufficient for learnability.
• 2009–2010: Shalev-Shwartz, Shamir, Srebro and Sridharan (COLT 2009, JMLR 2010) prove that, in the General Learning Setting, learnability is equivalent to the existence of a uniform-RO stable, universally asymptotic empirical risk minimiser (Theorem 7).

Setting

A learning problem consists of a hypothesis class $\mathcal H$ (nonempty), an instance set $\mathcal Z$ with a $\sigma$-algebra, and an objective $f:\mathcal H\times\mathcal Z\to\mathbb R$ with $|f(h;z)|\le B$ for all $h,z$. Given a probability distribution $\mathcal D$ on $\mathcal Z$ and an i.i.d. sample $S=(z_1,\dots,z_m)\sim\mathcal D^m$, the following quantities are defined:

• the risk is $F(h)=\mathbb E_{z\sim\mathcal D}[f(h;z)]$, and $F^*=\inf_{h}F(h)$;
• the empirical risk is $F_S(h)=\frac1m\sum_{i=1}^m f(h;z_i)$, and $F_S(\hat h_S)=\inf_h F_S(h)$ is the minimal empirical risk. Only the value is used; no minimiser need exist.

A learning rule $A$ maps each sample $S$ of each size $m$ to a hypothesis $A(S)$. A rate $\varepsilon(m)$ is a non-increasing sequence tending to $0$. For a rule $A$ the paper defines the following properties:

• $A$ is consistent with rate $\varepsilon_{\rm cons}$ under $\mathcal D$ if $\mathbb E_S[F(A(S))-F^*]\le\varepsilon_{\rm cons}(m)$. It is universally consistent if this holds for every $\mathcal D$ with the same rate. The problem is learnable (Definition 1) if a universally consistent rule exists.
• $A$ is an AERM (asymptotic empirical risk minimiser) with rate $\varepsilon_{\rm erm}$ under $\mathcal D$ if $\mathbb E_S[F_S(A(S))-F_S(\hat h_S)]\le\varepsilon_{\rm erm}(m)$, and universally so if this holds for every $\mathcal D$.
• $A$ generalizes with rate $\varepsilon_{\rm gen}$ under $\mathcal D$ if $\mathbb E_S[|F(A(S))-F_S(A(S))|]\le\varepsilon_{\rm gen}(m)$.
• With $S^{(i)}$ the sample $S$ with $z_i$ replaced by $z_i'$, $A$ is uniform-RO stable with rate $\varepsilon_{\rm stable}$ (Definition 4) if, for all $S$, all replacements $(z_1',\dots,z_m')$ and all $z'\in\mathcal Z$,

$$\frac1m\sum_{i=1}^m\bigl|f(A(S^{(i)});z')-f(A(S);z')\bigr|\le\varepsilon_{\rm stable}(m).$$

Average-RO stability (Definition 5) is the in-expectation analogue, with the replacement point also serving as the test point.

Formalization targets

Goal: Theorem 7

The problem is learnable if and only if there is a learning rule that is uniform-RO stable and universally an AERM. Quantitatively, if $A$ is universally consistent with rate $\varepsilon_{\rm cons}$, then some rule $A'$ is uniform-RO stable and universally AERM with

$$\varepsilon_{\rm stable}(m)=\frac{2B}{\sqrt m},\qquad \varepsilon_{\rm erm}(m)=3\,\varepsilon_{\rm cons}\bigl(\lfloor m^{1/4}\rfloor\bigr)+\frac{8B}{\sqrt m},$$

and conversely, a uniform-RO stable universal AERM is universally consistent with rate $\varepsilon_{\rm stable}(m)+\varepsilon_{\rm erm}(m)$.

Milestones

These follow the order of the paper's proof.

• Sufficiency: Utility Lemma 12 (a bounded sample mean deviates by at most $B/\sqrt m$ in expectation), Lemma 11 (on-average generalization ⇔ average-RO stability), Claim 6 (uniform-RO ⇒ average-RO stability), Lemma 15 (an on-average generalizing AERM is consistent), and Theorem 8 (a stable AERM is consistent with rate $\varepsilon_{\rm stable}+\varepsilon_{\rm erm}$ and generalizes with rate $\varepsilon_{\rm stable}+2\varepsilon_{\rm erm}+2B/\sqrt m$).
• Necessity: Lemma 20 (every rule has a uniform-RO stable, $3B/\sqrt m$-generalizing version with consistency rate $\varepsilon_{\rm cons}(\lfloor\sqrt m\rfloor)$), Lemma 16, the Main Converse Lemma ($\mathbb E|F_S(\hat h_S)-F^*|\le2\varepsilon_{\rm cons}(m')+2B/\sqrt m+2Bm'^2/m$ for $2\le m'\le m/2$), and Lemma 18 (under that bound, a consistent and generalizing rule is an AERM).

Significance

Theorem 7 shows that in the General Learning Setting, stability replaces uniform convergence as the notion that characterises learnability. It also says where to look for a learning rule: ERM may fail, but some AERM always works, and it must be stable. The rates are explicit and polynomial. Downstream, the paper uses Theorem 7 to prove Theorem 23 (randomised rules) and to design a generic learning algorithm (Theorem 25). Mission II of this series (Tikhonov-regularised ERM for stochastic convex optimisation) is a concrete instance of a stable AERM for a problem with no uniform convergence.

The theorem has been proved since 2010 but has not been formalized. The platform has the textbook side of the same authors' framework: Understanding Machine Learning Theorem 13.2, UnderstandingML.stability_identity, the replace-one identity behind Lemma 11, stated for hypotheses in $\mathbb R^d$. The platform does not have learnability in the General Learning Setting, over an arbitrary hypothesis class, or the converse direction. That direction is the new content: learnability forces a stable AERM to exist.

Difficulty

The sufficiency direction is a chain of expectation identities. The necessity direction is harder. A universally consistent rule need not be an AERM, need not generalize and need not be stable (Example 2 of the paper), so it cannot simply be reused. ERM cannot be used either, since it can fail on learnable problems. The Main Converse Lemma is where universal consistency is used in full: the rule's guarantee has to be applied under a distribution other than $\mathcal D$, and a naive argument under $\mathcal D$ alone fails (Example 1: consistency under one distribution does not imply generalization under it). Combining the lemmas into the stated rates requires choosing the auxiliary sample size and tracking every constant, including the regime of small $m$ where Lemma 16's hypothesis $2\le m'\le m/2$ cannot be met.

Formalization scope

Samples are Fin m → Z, the sample law $\mathcal D^m$ is Measure.pi, and $S^{(i)}$ is Function.update S i (S' i). Learning rules have type (m : ℕ) → (Fin m → Z) → H, and every property is asserted for $m\ge1$. The minimal empirical risk and $F^*$ are real infima over the nonempty, bounded-below family, never values at a chosen minimiser. Rates are non-increasing on $m\ge1$ and tend to $0$. $\lfloor m^{1/4}\rfloor$ and $\lfloor\sqrt m\rfloor$ are Nat.sqrt (Nat.sqrt m) and Nat.sqrt m, the paper's $\varepsilon_{\rm cons}(m^{1/4})$ read at an integer sample size. The paper's $B=\sup|f|$ is replaced by any bound $B$ (all rates increase in $B$).

The paper never discusses measurability. This formalization adds one standing assumption, identical across the series: each $f(h;\cdot)$ is measurable, the minimal empirical risk $S\mapsto\inf_hF_S(h)$ is measurable (true for countable $\mathcal H$, for example), and every learning rule, whether assumed or asserted to exist, has $(S,z)\mapsto f(A(S);z)$ jointly measurable. Without this a non-measurable rule would have Bochner integrals equal to $0$, and existence claims such as "some rule is a universal AERM" would be satisfied by junk. Every existential in the goal therefore produces a measurable rule, and learnability is quantified over measurable rules with the rate chosen before the distribution. Uniform-RO stability is pointwise over all samples, replacement vectors and test points; it is never replaced by the in-expectation Definition 5.

No statement is corrected. The proof of the converse in the paper calls $A'$ "$2B/\sqrt m$-generalizing" where Lemma 20 gives $3B/\sqrt m$. The stated $8B/\sqrt m$ absorbs either value, so Theorem 7 is formalized as printed.

The definitions (risks, rules, consistency, AERM, generalization, the two RO-stability notions) are reusable by the other missions of this series and by any stability-based result in the General Learning Setting. Contributions are welcome at every level: proofs of the milestones, the measure-theoretic infrastructure they need (exchangeability of i.i.d. coordinates under Measure.pi, sub-sampling and restriction of product measures, the variance bound for bounded sample means), and the remaining results of Section 5 (Theorems 9 and 10, Lemmas 14 and 17).

Selected references

• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, Stability and Uniform Convergence, Journal of Machine Learning Research 11 (2010) 2635–2670. https://jmlr.org/papers/v11/shalev-shwartz10a.html
• V. N. Vapnik, The Nature of Statistical Learning Theory, Springer, 1995. https://doi.org/10.1007/978-1-4757-2440-0
• N. Alon, S. Ben-David, N. Cesa-Bianchi, D. Haussler, Scale-sensitive dimensions, uniform convergence, and learnability, Journal of the ACM 44(4) (1997) 615–631. https://doi.org/10.1145/263867.263927
• O. Bousquet, A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://jmlr.org/papers/v2/bousquet02a.html
• S. Mukherjee, P. Niyogi, T. Poggio, R. Rifkin, Learning theory: stability is sufficient for generalization and necessary and sufficient for consistency of empirical risk minimization, Advances in Computational Mathematics 25 (2006) 161–193. https://doi.org/10.1007/s10444-004-7634-z
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 13. https://doi.org/10.1017/CBO9781107298019

Motivation

Mission III's Theorem 6.2 reduces SPN stability to a question about deterministic fluid model solutions: does every solution of a fixed system of equations get driven to the origin, uniformly in its starting size? Mission IV showed how to derive the extra, policy-specific equations a fluid model must satisfy. What remains is a method for proving that a system of fluid equations forces extinction — and the standard tool for that, across dynamical systems generally, is a Lyapunov function: a scalar-valued potential that decreases along every trajectory. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 8 to making this method precise for fluid models, and to explaining exactly why it is easier to apply here than the analogous drift condition for the underlying Markov chain.

The chapter's calculus culminates in a genuinely delicate real-analysis fact: the ordinary "Lyapunov function decreases everywhere it should" argument needs the function to be differentiable, but fluid model solutions are typically only Lipschitz (hence differentiable only almost everywhere), and some Lyapunov functions used later in the book (Chapter 10's entropy function) are not even Lipschitz. The chapter's most general result, Lemma 8.11, resolves this by working with the upper-right Dini derivative rather than the ordinary one, following an approach whose subtlety is illustrated by a counterexample due to L. Massoulié when one of its three hypotheses is dropped.

Setting

Throughout this mission, (D,F,T,Z) (without hats) denotes an arbitrary solution of the fluid equations (6.1)-(6.6), restated from mission III (drafts in this series do not import one another). A function $g$ is Lipschitz if it satisfies a Lipschitz bound on every bounded set, with a constant that may depend on the set; it is globally Lipschitz if one constant works everywhere. A point $t > 0$ is a regular point of a fluid model solution if all four components are differentiable there; because every solution is globally Lipschitz, the non-regular points form a Lebesgue-null set. A Lyapunov function for a fluid model is a Lipschitz function $H : \mathbb{R}^I_+ \to \mathbb{R}_+$ with $H(0)=0$ and $H(z) \ne 0$ for $z \ne 0$ — a positive-definite potential.

Formalization targets

Goal: Lemma 8.11 — the general Dini-derivative extinction criterion

For $f : \mathbb{R}_+ \to \mathbb{R}_+$ continuous on $(0,\infty)$, with a locally bounded upper Dini derivative $D^+f$ and $D^+f(t) \le -\varepsilon$ for a.e. $t$ with $f(t) > 0$:

$$f(t) = 0 \quad \text{for } t \ge f(0)/\varepsilon.$$

This is the weakest natural target: it drops the Lipschitz requirement of Lemma 8.5 entirely, replacing it with only continuity plus a one-sided, locally bounded derivative condition, and Lemmas 8.5 and 8.6 are recovered as the special cases $f = H \circ Z$ for $H$ Lipschitz (respectively linear-type and square-root-type drift bounds).

Supporting milestones

Lemma 8.2 (composition of Lipschitz functions) and Lemma 8.3 (every fluid model solution is globally Lipschitz) supply the regularity Lemma 8.5 needs. Lemma 8.5 (linear drift bound) and Lemma 8.6 (square-root drift bound) are the two directly-applicable extinction criteria the book presents before generalizing to Lemma 8.11. Lemma 8.9 identifies a structural fact used in nearly every application: at a regular point, an empty buffer's fluid arrival and departure rates necessarily coincide. Lemma 8.10 gives the calculus of a pointwise maximum's derivative, needed for piecewise-linear Lyapunov functions. Theorem 8.12 is the chapter's worked illustration: the tandem queueing network's fluid model is stable under the standard load condition, proved with a linear Lyapunov function that (the chapter goes on to show) does not translate into a valid Markov-chain drift bound — the concrete illustration of why the fluid-model method earns its keep.

Significance

The result itself. Lemma 8.11 is the single tool every subsequent stability chapter of the book applies: feedforward and generalized Jackson networks, the Rybko–Stolyar boundary, back-pressure control, proportionally fair allocation (whose entropy Lyapunov function is exactly the non-Lipschitz case this lemma was built to handle), and task allocation all conclude fluid model stability via an instance of this criterion. Theorem 8.12's side observation — the same Lyapunov function that works effortlessly for the fluid model fails to give a Markov-chain drift bound at all — is the chapter's explicit argument for why fluid-model methodology is not just a convenience but a genuine technical advance over direct Markov-chain analysis.

Formalizing it. Searches for "Lyapunov function," "Dini derivative," and "Lipschitz continuous" (q=Lyapunov%20function, q=Dini%20derivative) surface no reusable extinction-criterion result; the one Lyapunov-adjacent hit, posDef_quadratic_form_lower_bound, is an unrelated quadratic-form bound. This mission is a from-scratch formalization of the fluid model's Lyapunov calculus, reusing Mathlib's own LipschitzOnWith/LipschitzWith substrate for Definition 8.1 rather than restating ordinary Lipschitz continuity, per this mission's own BRIEF.md recommendation.

Difficulty

The central difficulty is Lemma 8.11 itself: proving that a bound on the upper Dini derivative $D^+f(t)$ (not the ordinary derivative) forces $f$ to decrease is genuinely subtler than the Lipschitz case, because $D^+f$ is one-sided and may not correspond to an actual rate of change at every point. The book's own proof needs a technical intermediate inequality (8.8), $f(b)-f(a) \le \int_a^b D^+f$, and states explicitly that this can fail without the local upper-boundedness hypothesis (b) — citing a counterexample of L. Massoulié — so a formalization that dropped condition (b) as "obviously implied by continuity" would be proving a false generalization, not a faithful specialization. A second difficulty, specific to Lemma 8.5/8.6's formalization, is that the hypothesis "$\dot f(t) \le -\varepsilon$ for almost all $t$ with $Z(t)\ne 0$" implicitly presupposes $\dot f(t)$ exists almost everywhere (a fact Lemma 8.3 supplies, not something to assume outright) — stating the hypothesis as a universally quantified implication over any witnessing derivative avoids smuggling in an unearned existence claim.

Formalization scope

Mission III's fluid-equation apparatus is restated locally (per that mission's own note that later chunks cannot import its draft), unmodified. Definition 8.1's two Lipschitz notions (bounded-set-wise and global) are formalized via Mathlib's own LipschitzOnWith, generalized over arbitrary (pseudo)metric domain and codomain types so the same definition serves $g:\mathbb{R}^d\to\mathbb{R}^m$ and $g:\mathbb{R}^m\to\mathbb{R}$ uniformly — reusing Mathlib substrate rather than restating Definition 8.1's $\varepsilon$-$\delta$ inequality from scratch, per BRIEF.md's explicit recommendation. The upper-right Dini derivative is restated inline (Appendix A.4 is out of series scope) via Filter.limsup along the right-neighborhood filter, and is used throughout Lemma 8.11 in place of the ordinary derivative — using deriv instead would be a strictly stronger, unfaithful hypothesis. Lemma 8.10's pointwise maximum is a supremum over the finite index type Fin d, always a genuine maximum with no junk-value risk. Theorem 8.12 restates the tandem queueing network's already-reduced fluid equations (8.11)-(8.15) directly, since Figure 1.1 belongs to Chapter 1, outside this mission series. A formalization that replaced Lemma 8.11's Dini-derivative hypotheses with ordinary-derivative ones, or that dropped condition (b)'s local bound, would each be an unfaithful strengthening or a false generalization — both ruled out here. The Lyapunov extinction criteria (lyapunov_extinction_linear, lyapunov_extinction_sqrt, dini_extinction_criterion) are the primary reusable contributions, intended for direct reuse (matching shape, since drafts do not import one another) by every later stability mission in the series; contributions completing the eight by sorry proofs are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• L. Massoulié, "Structural properties of proportional fairness: stability and insensitivity," Annals of Applied Probability 17 (2007), 809–839.
• J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.

Motivation

In a periodic-review inventory system a manager observes the stock level before ordering, decides how much to order, and then faces random demand. When ordering costs a fixed setup charge plus a constant price per unit, Scarf (1960) proved that an $(s,S)$ policy is optimal in every period of a finite-horizon problem: order up to $S$ when the stock falls below $s$, otherwise order nothing. Real ordering costs are often not of this form. Quantity discounts, a choice between production facilities with different setup and marginal costs, or a supplier whose price schedule falls with volume all give an ordering cost that is concave and increasing but not "setup plus linear". Karlin had analysed the single-period problem with such costs; Porteus (1971) gave the first multiperiod result with random demand.

Timeline:

• Scarf (1960): $(s,S)$ optimality for setup-plus-linear ordering cost, via $K$-convexity of the expected cost-to-go.
• Veinott (1966): an alternative proof of $(s,S)$ optimality under different conditions (quasi-convex one-period costs).
• Porteus (1971): for concave increasing ordering costs and demand with a one-sided Pólya density, a generalized $(s,S)$ policy is optimal in every period; when the cost is piecewise linear with $r$ pieces it is an $(s,S)_r$ policy with at most $r$ reorder levels.

Setting

The ordering cost $c : [0,\infty) \to \mathbb R$ is concave, nondecreasing, and $c(0) = 0$. For $z > 0$, $C_2(z)$ is the supporting line of $c$ at $z$ with the smallest intercept, written as a pair (slope, intercept) $(\kappa, K)$. The set of slopes that occur is $C$, and $K_\kappa$ is the intercept belonging to slope $\kappa \in C$, so $c(z) = \min_{\kappa \in C}\{K_\kappa + \kappa z\}$ for $z > 0$. The limits $(c_0, K_0) = \lim_{z \downarrow 0} C_2(z)$ and $(c_\infty, K_\infty) = \lim_{z\to\infty} C_2(z)$ are assumed to exist.

Demands in successive periods are i.i.d. with density $\varphi$. A function $\varphi$ is $PF_n$ if $0 < \int\varphi < \infty$ and $\det[\varphi(x_i - t_j)]_{i,j\le k} \ge 0$ for all $k \le n$ and increasing $x_1<\dots<x_k$, $t_1<\dots<t_k$; it is a one-sided Pólya density if it is $PF_n$ for every $n$, integrates to $1$ and vanishes on $(-\infty,0)$. Exponential and Erlang densities are examples.

With holding-and-shortage cost $m$ (PF-integrable, bounded below), terminal cost $f_0$, discount factor $0 \le \alpha \le 1$, and convolution $(f*\varphi)(y) = \int f(y-x)\varphi(x)\,dx$, the value functions are

$$h_n = m * \varphi + \alpha\, f_{n-1} * \varphi, \qquad f_n(x) = \inf_{y \ge x}\{c(y-x) + h_n(y)\},$$

where $n$ counts the periods remaining. $Y_n(x)$ is the set of minimizers $S \ge x$. A generalized $(s,S)$ policy is a function $y$ with $y(x) = x$ for $x \ge s$ and $y(z) \ge y(x) \ge S \ge s$ for $z < x < s$: no order above $s$, and below $s$ an order-up-to level that is at least $S$ and does not increase with the starting stock.

Two function classes carry the argument. $f$ is non-$K$-decreasing on $X$ if $f(x) \le f(y) + K$ for $x \le y$ in $X$. For $K \ge 0$, $C_a(K)$ consists of the piecewise continuous, PF-integrable functions with $f(x)\to\infty$ as $|x|\to\infty$ that are nonincreasing on $(-\infty,a)$ or $(-\infty,a]$ and non-$K$-decreasing on the rest of the line. $C(K)$ is its continuous part. With $G_{\kappa n} = \kappa\cdot + h_n$, the assumptions A1–A5 of §VI tie $m$ and $f_0$ to $c_0$, $c_\infty$ and the $K_\kappa$.

Formalization targets

Goal: Theorem 3

Under the standing assumptions and A1–A5, for every $n \ge 1$ the convolution $f_{n-1}*\varphi$ exists and

$$\exists\, s, S,\ \exists\, y \text{ generalized } (s,S) \text{ policy}: \quad y(x) \in Y_n(x) \ \ \forall x \in \mathbb R.$$

The statement fixes no numbers: $s$ and $S$ depend on $n$ and on the data.

Milestones

1. Lemma 9: $\bigcup_a C_a(K)$ equals the class of quasi-$K$-convex, piecewise continuous, PF-integrable functions tending to $\infty$ as $|x| \to \infty$.
2. Lemma 1: every $f \in C(K)$ has reals $s \le S$ with $S$ a global minimizer, $f > f(S) + K$ on $(-\infty,s)$, $f$ nonincreasing there, and $f$ non-$K$-decreasing on $[s,\infty)$.
3. Lemma 5: for continuous $g$, $f(x) = \int_0^\infty g(x-t)\lambda e^{-\lambda t}dt$ is $C^1$ with $f' = \lambda(g-f)$.
4. Lemma 6: $g*\varphi$ is continuous and $C^1$ off a finite set for a one-sided Pólya $\varphi$.
5. Lemma 10 and Theorem 1: $f \in C_a(K) \Rightarrow f*\varphi \in C(K)$, first for exponential $\varphi$, then for every one-sided Pólya density.
6. Theorem 2: if every $G_{\kappa n} \in C(K_\kappa)$ and every $Y_n(x) \ne \emptyset$, a generalized $(s,S)$ policy is optimal in period $n$.
7. Lemma 2: $f_n(x) \le f_n(y) + c(y-x)$ for $x \le y$.
8. Lemma 3: the inductive step producing the hypotheses of Theorem 2 from properties of $f_{n-1}$.

Significance

The result extends $(s,S)$-type structure from setup-plus-linear to arbitrary concave increasing ordering costs, which covers quantity discounts and multi-facility production. When $c$ is piecewise linear with $r$ pieces, the optimal policy is an $(s,S)_r$ policy described by at most $r$ reorder points and order-up-to levels. That is a finite-dimensional family, which makes computing policies tractable. The class $C(K)$ and its closure under Pólya convolution (Theorem 1) are statements about functions of one real variable, independent of the inventory model. Quasi-$K$-convexity extends both $K$-convexity and quasi-convexity (Lemma 8 of the paper).

The theorem is classical and proved on paper; no machine-checked version is known. Its appendix leaves several steps as "easily proved by contradiction", which a formal proof has to fill in. The platform has Bertsekas's $K$-convex $(s,S)$ lemma (BertsekasDP.kconvex_sS_structure, a result about $K$-convex rather than $C(K)$ functions), but no Pólya frequency functions, no quasi-$K$-convexity, and no concave-cost inventory model.

Difficulty

The obvious route copies Scarf: show that the cost-to-go is $K$-convex and that $K$-convexity survives taking expectations. With a concave ordering cost there is no single $K$, and the relevant functions $G_{\kappa n}$ are generally not $K_\kappa$-convex. The weaker property that does hold, membership in $C(K_\kappa)$, is not preserved by convolution with an arbitrary density. It is preserved by one-sided Pólya densities, and Theorem 1 is the step that shows this: exponential kernels come first (via the differential identity (23)), and the general case needs the Schoenberg representation of one-sided Pólya densities as limits of convolutions of exponentials. The second difficulty is combining the different slopes $\kappa \in C$ into one policy (Theorem 2). Separate $(s,S)$ pairs for each $\kappa$ do not by themselves give a monotone policy.

Formalization scope

All functions are ℝ → ℝ; the ordering cost is used only on $[0,\infty)$. The demand density is a function, not a measure; convolution is the Lebesgue integral over $\mathbb R$. $PF_n$ uses Matrix.det over Fin k. The value functions are defined by structural recursion on $n : \mathbb N$ with $f_0$ the terminal cost; $h_n$ is used for $n \ge 1$. $Y_n(x)$ is defined by the optimality inequality, never through the infimum. $G_{\kappa n}$ is defined by the paper's identity (7), $\kappa y + h_n(y)$. $R^- = (-\infty,0)$ is open, and "increasing" is read as nondecreasing. Slopes in $C$ are written $\kappa$ to separate them from the cost function $c$.

Added hypotheses and conventions:

• $m$ piecewise continuous. The paper uses this without stating it (proof of Lemma 3). It is a hypothesis of Lemma 3 and Theorem 3.
• Real-valued $f_n$ in Lemma 2. Following the convention of §X, Lemma 2 assumes each infimum defining $f_n$ is over a set bounded below.
• Measurability of $m$ and $f_0$ (§X) is implied by their piecewise continuity and is not stated separately.

Lean returns $0$ for an infimum over a set unbounded below and for the integral of a non-integrable function. The goal therefore concludes that $f_{n-1}*\varphi$ exists and that $Y_n(x)$ is nonempty (so the infimum is a minimum); it does not assume these. It also does not quantify over arbitrary functions satisfying a Bellman equation or over an arbitrary set-valued $Y$. Everything is built from the data $(c, m, \varphi, \alpha, f_0)$. The class $C(K)$ includes PF-integrability and coercivity, without which Lemma 1 fails.

Welcome contributions: Pólya frequency functions and the exponential special cases (the exponential density is $PF_\infty$), Leibniz-rule lemmas for exponential kernels, the theory of $C(K)$ and quasi-$K$-convex functions (reusable for other inventory models), and a formal Schoenberg representation (Theorem 6 of the paper, cited there and needed for Theorem 1). Theorems 4 and 5 (nonstationary and partial-backlogging extensions) are not part of this mission.

Selected references

• E. L. Porteus, On the Optimality of Generalized (s, S) Policies, Management Science 17(7):411–426, 1971. https://doi.org/10.1287/mnsc.17.7.411
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• A. F. Veinott Jr., On the Optimality of (s, S) Inventory Policies: New Conditions and a New Proof, SIAM Journal on Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
• I. J. Schoenberg, On Pólya Frequency Functions I. The Totally Positive Functions and their Laplace Transforms, Journal d'Analyse Mathématique 1:331–374, 1951. https://doi.org/10.1007/BF02790092
• S. Karlin, Total Positivity, Volume 1, Stanford University Press, 1968.

Motivation

A robust Markov decision process replaces the unknown transition probabilities of an MDP by sets of plausible values and optimises against the worst case. Nilim and El Ghaoui (Oper. Res. 53 (2005)) showed that, when the uncertainty is rectangular (each row of each transition matrix varies independently in its own set), the robust problem is solved by a Bellman-type recursion. Each step of that recursion needs, for every state and action, the value of an inner problem: the largest expectation of the next-stage value vector over the uncertainty set of one transition row. The recursion is only as tractable as this inner problem.

The paper studies several uncertainty models built from statistical estimates of the transition rows. In the entropy model the uncertain row is any distribution within a prescribed Kullback–Leibler divergence of a nominal distribution. For this model the paper reduces the inner problem to the minimisation of a scalar convex function, which is then solved by bisection. Iyengar (Math. Oper. Res. 30 (2005)) obtained the same robust recursion independently, and the same scalar reduction is the basic computation in later KL-constrained distributionally robust optimisation. This mission formalizes that reduction and the properties of the scalar function that the paper derives from it.

Setting

Let $n\ge 1$ and let $\Delta_n=\{p\in\mathbb R^n : p\ge 0,\ \sum_j p(j)=1\}$ be the probability simplex. For $p,q\in\mathbb R^n$ the Kullback–Leibler divergence is

$$D(p\|q)=\sum_j p(j)\log\frac{p(j)}{q(j)},$$

with $0\log 0=0$. Fix a nominal distribution $q\in\Delta_n$ with $q(j)>0$ for every $j$, and a level $\beta>0$. The entropy uncertainty set is

$$\mathcal P=\{p\in\Delta_n : D(p\|q)\le\beta\}.$$

For a vector $v\in\mathbb R^n$ (in the MDP, the value function of the next stage), the inner problem (17) is

$$\sigma_{\mathcal P}(v)=\max_{p\in\mathcal P} p^{\mathsf T}v .$$

The paper's scalar dual function (47) is, for $\lambda>0$,

$$\sigma(\lambda)=\lambda\log\Big(\sum_j q(j)\,e^{v(j)/\lambda}\Big)+\beta\lambda .$$

Write $v_{\max}=\max_j v(j)$ and $Q(v)=\sum_{j:\,v(j)=v_{\max}}q(j)$, the $q$-mass of the maximisers of $v$. The tilted distribution at $\lambda>0$ is $p^*(j)=q(j)e^{v(j)/\lambda}/\sum_i q(i)e^{v(i)/\lambda}$.

In Lean, vectors are Fin n → ℝ, $\Delta_n$ is stdSimplex ℝ (Fin n), and $D$, $\mathcal P$, $\sigma$, $p^*$, $v_{\max}$, $Q(v)$ are klDiv, klBall, dualFn, tiltedDist, vmax, maxMass in the namespace RobustMDP.EntropyInner.

Formalization targets

Goal: the dual of the inner problem (§6.2, Eq. (47), p. 791)

$$\max_{p\in\mathcal P} p^{\mathsf T}v=\inf_{\lambda>0}\sigma(\lambda),$$

with the maximum attained. This is kl_ball_inner_problem_dual. It holds for every $n$, every $v$, every $q>0$ in $\Delta_n$ and every $\beta>0$.

Milestones

1. §6.1: $\max_{p\in\Delta_n}D(p\|q)=\max_i(-\log q_i)$, and for $\beta\ge\max_i(-\log q_i)$ the set $\mathcal P$ is all of $\Delta_n$ and the inner value is $v_{\max}$.
2. Eq. (48): $q^{\mathsf T}v+\beta\lambda\le\sigma(\lambda)\le v_{\max}+\beta\lambda$ for $\lambda>0$.
3. §6.2, the optimal distribution: $p^{\mathsf T}v-\lambda D(p\|q)\le\lambda\log\sum_j q(j)e^{v(j)/\lambda}$ on $\Delta_n$, with equality at $p^*$.
4. §6.2, elimination of $\mu$: $\min_{\mu}\big[\mu+\beta\lambda+\lambda\sum_j q(j)e^{(v(j)-\mu)/\lambda-1}\big]=\sigma(\lambda)$.
5. Eq. (49): $\sigma(\lambda)=v_{\max}+(\beta+\log Q(v))\lambda+o(\lambda)$ as $\lambda\to0^+$.
6. Eq. (50): $\sigma(\lambda)=q^{\mathsf T}v+\beta\lambda+o(1)$ as $\lambda\to\infty$.
7. §6.3: if $\beta\ge-\log Q(v)$, then $\inf_{\lambda>0}\sigma=v_{\max}$ and the inner value is $v_{\max}$.

Significance

The goal turns an $n$-dimensional optimisation over a nonpolyhedral convex set into a one-dimensional convex minimisation whose objective costs $O(n)$ to evaluate. Combined with the bisection bracket from (48) and the behaviour at $0$ from (49), it gives the paper's $O(n\log(v_{\max}/\delta))$ cost per inner problem (§6.4), and hence the per-step cost of the robust Bellman recursion under entropy uncertainty. Milestone 7 identifies exactly when the uncertainty set is large enough that the robust step ignores the nominal model; unlike the cruder threshold of milestone 1, it depends on $v$.

The result is proved in the paper modulo "standard duality arguments". The paper gives no proof of the duality step itself, and its expansions (49)–(50) are proved only in outline in Appendix C. No formal proof of any of these statements is known to exist; Mathlib has the measure-theoretic Donsker–Varadhan ingredients but not the finite, constrained dual stated here. The mission produces a machine-checked version of the whole chain, with the attainment questions (which side is a max, which is only an infimum) settled explicitly.

Difficulty

The inequality $\max_{\mathcal P}p^{\mathsf T}v\le\sigma(\lambda)$ for every $\lambda>0$ is the routine half. The obstacle is the reverse inequality. The paper appeals to Lagrangian strong duality under a Slater condition, but the Lagrangian dual function equals $\sigma(\lambda)$ only for $\lambda>0$; at $\lambda=0$ it is $v_{\max}$, and the dual infimum may be approached only as $\lambda\to0^+$. A proof that looks for a minimiser $\lambda^*>0$ and a matching primal point $p^*$ fails in precisely the regime $\beta\ge-\log Q(v)$ of milestone 7, where no such $\lambda^*$ exists and the primal optimum sits on the face of the simplex spanned by the maximisers of $v$. The strong-duality argument must also handle the boundary of $\Delta_n$, where $D(\cdot\|q)$ is not differentiable.

Formalization scope

• Vectors are Fin n → ℝ; $\Delta_n$ is stdSimplex ℝ (Fin n). $D(p\|q)$ is a local finite sum with Lean's $\log 0=0$, which gives $0\log0=0$; Mathlib's measure-valued InformationTheory.klDiv is not used.
• Standing hypotheses in every theorem: $q\in\Delta_n$, $q(j)>0$ for all $j$, and $\beta>0$, as in §6.1. No restriction on $v$ is imposed; the "without loss of generality $v\ge0$" of the paper's §5 is not assumed here.
• The primal "max" is stated with IsGreatest (attained, since the KL ball is compact). The paper's "$\min_{\lambda>0}\sigma(\lambda)$" is an infimum, stated with IsGLB over $\{\sigma(\lambda):\lambda>0\}$: it is not attained when $\beta\ge-\log Q(v)$.
• dualFn is total in $\lambda$ and equals $0$ at $\lambda=0$ (division by zero), not the paper's $\sigma(0)=v_{\max}$. Every statement uses $\lambda>0$; the value at $0$ appears as the one-sided limit of (49). Accordingly (48) is stated for $\lambda>0$.
• $v_{\max}$ is ⨆ j, v j, the attained maximum over the finite nonempty index set; $\max_i(-\log q_i)$ likewise.
• (49) is stated as a limit along 𝓝[>] 0 together with a little-o remainder; (50) as a limit along atTop.
• Milestone 7 uses the non-strict condition $\beta\ge-\log Q(v)$ of the paper's first sentence, which contains the strict version of its second.
• Trivializing formalizations are excluded: the statements quantify over all $n$, $v$ and $q$, so a constant $v$, $n=1$, or the whole-simplex case of milestone 1 does not discharge the goal.

Useful infrastructure: a finite Gibbs variational inequality, compactness of the KL ball, and convexity and one-sided asymptotics of the log-sum-exp function in the temperature parameter. These are reusable for any KL-constrained robust optimisation mission. Proofs of the milestones, alternative proofs of the goal that avoid a general strong-duality theorem, and the sharper $O(\lambda e^{-t/\lambda})$ remainder of Appendix C are all welcome.

Selected references

• A. Nilim and L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• M. D. Donsker and S. R. S. Varadhan, Asymptotic evaluation of certain Markov process expectations for large time, I, Communications on Pure and Applied Mathematics 28(1):1–47, 1975. https://doi.org/10.1002/cpa.3160280102

Motivation

Before a queueing network's stability can be studied in any depth, a much cruder question has to be settled: is stability even possible for the given arrival rates and service capacities, under any control policy at all? For a single M/M/1 queue the answer is the familiar $\lambda < \mu$, but a general stochastic processing network (SPN) — many buffers, many activities, servers that can be pooled or shared across job classes — has no single scalar "utilization" to compare against a threshold. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) answers this with a linear program: the static planning problem, first formulated by Harrison (2000). This mission formalizes the theorem that answers the crude question in one direction — no control policy can stabilize a network outside the region that program identifies — which is why, as the book puts it, "throughout the remainder of this book, attention is essentially restricted to subcritical networks."

Setting

An SPN has $I$ buffers, indexed by $i \in \mathcal{I}$, and $J$ activities, indexed by $j \in \mathcal{J}$. Its first-order data — the quantities that matter for a capacity calculation, as opposed to full stochastic detail — are: the $I \times J$ material requirement matrix $B$ ($B_{ij}$ = number of class-$i$ items one type-$j$ service consumes), the $I \times J$ mean output matrix $\Gamma$ (its $j$th column is the expected output vector of a type-$j$ service), the mean service times $m_j > 0$, the $K \times J$ capacity consumption matrix $A$ (server pool $k$ against activity $j$), and the server-pool capacities $b \in \mathbb{R}_+^K$. From these,

$$R := (B - \Gamma)M^{-1}, \qquad M := \operatorname{diag}(m_1, \dots, m_J),$$

so that $R_{ij}$ is the long-run average rate at which activity $j$ depletes buffer $i$'s content.

Given an arrival-rate vector $\lambda \in \mathbb{R}_+^I$, the static planning problem (SPP) is the linear program

$$\gamma^\ast(\lambda) := \min_{x \ge 0,\, \gamma} \ \gamma \quad \text{s.t.} \quad Rx = \lambda, \quad Ax \le \gamma b,$$

whose decision variable $x_j$ is a long-run average activity rate and whose objective $\gamma$ upper-bounds every server pool's utilization. The network is subcritical at $\lambda$ if $\gamma^\ast(\lambda) < 1$, and the subcritical region is $\Lambda := \{\lambda : \gamma^\ast(\lambda) < 1\}$.

An SPN is stable (Definition 3.6, mission I) when its ambient Markov chain is positive recurrent, equivalently has a unique stationary distribution, equivalently its buffer contents converge in distribution to a non-defective limit. This mission's chapter portion (Chapters 4-5) also treats three extensions used elsewhere in the book: a Markovian arrival process replacing independent Poisson arrivals; alternate routing with immediate commitment, where arrivals must be routed into an eligible buffer at the instant they arrive, with routing rates constrained by an augmented version of the SPP; and processor sharing (PS) networks, whose service discipline falls outside the book's ordinary relaxed-control framework and is instead analyzed through an equivalent head-of-line (EHL) model built to have the same generator.

Formalization targets

Goal: Theorem 5.2 — only subcritical networks can be stable

$$\text{(baseline stochastic assumptions)} \ \wedge \ \text{(Markov representation)} \ \wedge \ \text{(SPN stable)} \implies \lambda \in \Lambda.$$

This is the weakest target that captures the chapter's content: it asserts nothing about which policy achieves stability, or whether subcriticality is sufficient (Chapters 6 onward answer that, case by case, and Chapter 5 itself gives two counterexamples where it is not) — only that subcriticality is unconditionally necessary.

Further results (milestones)

Proposition 4.1 (a strong law of large numbers for class-level arrivals under randomized routing), Proposition 4.4 (PS-network stability reduces to EHL-model stability), Proposition 5.1 (for a unitary network, subcriticality reduces to the classical load condition $\rho < b$), and Corollaries 5.4-5.6 (the same necessity conclusion under a Markovian arrival process, under alternate routing, and its consequence for maximally stable policies).

Significance

The result itself. Theorem 5.2 converts "can this network be stabilized at all?" from an open-ended search over control policies into a single linear-program feasibility check on first-order data alone. Corollary 5.6 turns this into the standard proof template every later chapter uses: exhibit a policy whose implementation does not reference $\lambda$, show it is stable throughout the subcritical region, and conclude maximal stability — without having to separately characterize the true stability region $\Lambda^\ast$, which the book calls "a deep mathematical problem" in general.

Formalizing it. A search of the platform for "processing network," "static planning problem," and "linear program" returned no hits: the SPN-specific static planning problem — its decision variables $x$ tied to a network's material-balance matrix $R$ and capacity matrix $A$ — has no existing counterpart, though the platform's linear-optimization field (16 missions) has general LP duality substrate a future proof of Proposition 5.1 or Theorem 5.2 could draw on. This mission is a from-scratch formalization of the SPP, the subcritical region, and the necessity theorem.

Difficulty

The natural first attempt states Theorem 5.2 as a claim about the buffer-contents process $Z(t)$ directly. This fails to separate cleanly from the proof, because the actual argument passes through an auxiliary quantity — the stationary mean $x := \mathbb{E}_\pi[N(0)]$ under the chain's (unique, by stability) stationary distribution $\pi$ — that has no meaning outside a specific proof strategy. The formalization instead states the goal purely in terms of the data $(R, A, b)$ and the hypothesis of stability, exactly as the book's own statement does, leaving $x$'s construction to the (currently sorry) proof. A second difficulty is Corollary 5.4's Markovian arrival process: naively reusing BaselineAssumptions with a non-Poisson arrival process is impossible, since Poisson-ness is a mandatory structural field of that definition, not an optional hypothesis — the corollary needs its own hypothesis structure that changes exactly the one clause Assumption 2.1(a) contributes and nothing else.

Formalization scope

Buffers and activities are Fin I, Fin J; matrices are Matrix over ℝ. The subcritical region is defined via the optimal SPP value $\gamma^\ast$, formalized with Mathlib's IsLeast (attained infimum, matching the book's own "$\gamma^\ast \le 1$ iff $x$ exists" phrasing, which presupposes attainment) rather than a bare existential — a formalization using, say, sInf would silently commit to junk values on an infeasible or unbounded LP and would not obviously match the book's own usage of $\gamma^\ast$ as literally attained. The basic SPN model's full state-process construction (Sections 2.3-2.4) is not re-derived from scratch here; Theorem 5.2 instead takes the structural facts its own proof invokes — the capacity constraint $AN(t) \le b$ (Eq. 2.11) and the material-requirement matrix $B$ — as explicit data, reusing mission I's BaselineAssumptions and MarkovRepresentation for the stochastic and Markov-chain apparatus. Proposition 4.4's shared- generator fact between a PS network and its EHL model (the actual content the book's construction of Section 4.4 establishes) is likewise taken as an explicit hypothesis rather than rebuilt from the refined-class/phase-type machinery of Eqs. (4.19)-(4.29); reconstructing that machinery from scratch, or reproving Proposition 4.1's SLLN from the chain's strong Markov property at regeneration times, are both welcome future contributions. A formalization that stated Theorem 5.2 with $\Lambda$ replaced by an unconstrained existential (dropping the LP structure entirely) would trivialize the chapter's actual content — the LP-feasibility characterization is what makes $\Lambda$ checkable, and is preserved here in full.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• J. M. Harrison, "Brownian models of open processing networks: canonical representation of workload," Annals of Applied Probability 10 (2000), 75-103.
• J. G. Dai and W. Lin, "Maximum pressure policies in stochastic processing networks," Operations Research 53 (2005), 197-218.