Operations Research

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

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

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$,

The deterministic problem (32)–(33) is

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

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

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

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

Multistage stochastic linear programs model decisions taken in periods $t = 1, \dots, T$ while a random vector $\xi_t$ is revealed period by period: production and capacity planning, energy scheduling, asset–liability management. With finitely many scenarios the problem is one very large linear program with a tree structure, and decomposition methods solve it by passing information up and down the scenario tree instead of solving it whole. John R. Birge's Nested Decomposition for Stochastic Programming Algorithm (NDSPA), published in Operations Research in 1985 (DOI), is the multistage extension of the L-shaped method of Van Slyke and Wets (SIAM J. Appl. Math. 1969) and the ancestor of the nested Benders and stochastic dual dynamic programming codes in use today.

The paper reports a practical defect of the method: degeneracy leads to many repeated solutions of the same scenario problem (Remark 4, p. 996–997), an effect Abrahamson (1980) had observed for deterministic nested decomposition. Propositions 3 and 4 (p. 997) identify where the degeneracy comes from: cuts that bind at the ancestor force the descendant problems that produced them into degenerate bases. This mission formalizes those two propositions.

Setting

Fix a node of a finite scenario tree: scenario $j$ at period $t$, with decision $x \in \mathbb{R}^{n}$. Its ancestor's decision $x^{a}$ enters only through the right-hand side of its equality rows. After $r$ feasibility cuts and $s$ optimality cuts have been added, the node solves the scenario problem (7):

over $x$ and a free scalar $\theta$, which stands in for the expected future cost. During NDSPA's forward pass the node also carries the restriction $\theta = 0$; a last-period node has no future cost and keeps that restriction.

A descendant problem (period $t+1$, scenario $j' \in J'$) has the same shape, with right-hand side $\xi_{j'} + B_{j'} x$ depending on the node's decision $x$. Two kinds of cut flow from descendants to the node:

• a feasibility cut arises when a descendant is infeasible at some $x^0$: a Farkas certificate $\lambda$ of that infeasibility, with parts $\pi, \rho, \sigma$ on the descendant's rows (7.2), (7.3), (7.4), yields the cut $D^\top x \ge d$ with $D = -\pi^\top B_{j'}$ and $d = \pi^\top \xi_{j'} + \rho^\top d_{j'} + \sigma^\top e_{j'}$;
• an optimality cut is built in NDSPA Step 3a from optimal dual vectors $\lambda_{j'}$ of all descendants at the current $\bar x$ and weights $p_{j'}$: $E = -\sum_{j'} p_{j'} \pi_{j'}^\top B_{j'}$ and $e = \sum_{j'} p_{j'} (\pi_{j'}^\top \xi_{j'} + \rho_{j'}^\top d_{j'} + \sigma_{j'}^\top e_{j'})$. It is added only if it cuts off the current point, the test (9): $\bar\theta < e - E^\top \bar x$.

A cut $E^\top x + \theta \ge e$ is valid when $e - E^\top x$ never exceeds the weighted sum of the descendants' objective values at feasible points, for any $x$. A basic solution of (7) is a point at which all equality rows hold and $n + 1$ linearly independent constraints are active; it is degenerate when more than $n + 1$ constraints are active.

Formalization targets

Goal: Proposition 4

Let two distinct valid optimality cuts $l_1, l_2$ bind at $(\bar x, \bar\theta)$. Let each descendant $j'$ have an optimal basic feasible solution $z_{j'}$ and an optimal dual vector $\lambda_{j'}$ at $\bar x$, and suppose the Step 3a cut built from these duals fails (9), so that $\bar\theta \ge e - E^\top \bar x$. Then

Milestone: Proposition 3

If descendant $j'$ generates feasibility cut $l'$ of the node and that cut binds at $\bar x$, then

Significance

The result. The two propositions explain a failure mode that every nested-decomposition implementation meets. The backward pass of NDSPA stalls, adding no cut, at exactly the points where Proposition 4 applies, and the degenerate descendant bases it predicts are what make the same ancestor basis recur over many iterations. The analysis motivated the partitioning method of Section 3 of the paper and the intermediate problem of Birge (1980), and it is the reason later codes pay attention to the choice among multiple optimal duals.

Formalizing it. The paper states both propositions without proof and refers the proofs to Birge (1980), an unpublished technical report. A machine-checked proof makes the statements self-contained. It also pins down what they assume: which cuts are meant, which invariants of the algorithm they rely on, and which notion of degeneracy applies to a problem with a free variable and inequality cuts. The definition layer (scenario problems with their cut families, LP duals, Farkas certificates, the Step 3a cut) is reusable for any statement about nested Benders or L-shaped methods. The finite convergence of the nested method is the subject of a separate private formalization (Birge and Louveaux, Ch. 6, Thm. 1, StochasticProg.Multistage.thm1_finite_convergence), so this mission does not restate NDSPA's convergence.

Difficulty

The statements connect the geometry of the ancestor's value function to the combinatorics of descendant bases. For Proposition 4 the difficulty is that nothing in the hypotheses mentions the descendants' bases directly: they speak of two cuts at the ancestor and one failed test. The conclusion is a statement about the descendants' simplex bases, so the ancestor-level information has to be transported down to the descendant problems, where the relevant objects (optimal bases, optimal duals, optimal-value functions of the right-hand side) are not unique in exactly the degenerate case the proposition is about. Two hypotheses that look dispensable are not. Without distinctness a duplicated cut gives a counterexample. Without validity a cut that is not a lower bound can bind anywhere. For Proposition 3 the certificate must be the one that generated the cut; an arbitrary cut row that happens to bind says nothing about the descendant.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the variable of (7) is $z = (x, \theta) \in$ Fin (n+1) → ℝ with $\theta$ its last coordinate. The paper suppresses transposes; here they are explicit, and a row vector times a matrix ($\pi B$) is vecMul. Basic, basic feasible and degenerate solutions are the general-form notions of Bertsimas and Tsitsiklis (Defs. 2.9–2.10), reused from the public definition BasicSolution, applied to the whole constraint family of (7), the free $\theta$ included. A last-period node is represented with the restriction $\theta = 0$, which pairs one extra variable with one extra active equality and so preserves basicness and degeneracy.

Readings of informal words, each stated in the items:

• "generate a feasibility constraint": the Van Slyke–Wets construction from a Farkas certificate at an earlier input $x^0$, stated against the descendant's current constraint family;
• "binding for some solution": the row holds with equality at the point; feasibility or optimality of the point for the ancestor is not assumed, which strengthens both statements;
• "two constraints of type (7.4)": two distinct cuts, both valid, the invariants NDSPA maintains;
• "every set of optimal solutions … that produces $E$ and $e$": one optimal basic feasible solution and one optimal dual vector per descendant, the cut computed from those duals;
• "degenerate": general-form degeneracy, not the standard-form count of zero components.

Correction to the page. Step 3a prints $E = -\sum \pi B_t$ and $e = \sum \pi \xi$. The formalization completes $e$ with the terms $\rho^\top d + \sigma^\top e$ from the descendants' own cuts, without which the cut is not a valid lower bound when the descendants carry cuts. It also adds weights $p_{j'} > 0$; conditional probabilities are a special case, and $p \equiv 1$ is the printed sum. The data $A$, $B$ may differ between descendants, which is more general than the paper.

Proposition 3 is vacuous when the descendant is infeasible at $\bar x$; that is the paper's statement. No trivializing reading is available for the goal: the cuts are computed from certificates and duals inside the statement, never taken as arbitrary vectors, and a sorry-free local check confirms that all hypotheses of Proposition 4 hold together on a small instance. Propositions 1 and 2, NDSPA's convergence, the partitioning method of Section 3 and the computational study are out of scope. Contributions welcome: proofs of Propositions 3 and 4, and supporting lemmas on LP duality and basis stability over general-form constraint families.

Selected references

• J. R. Birge, Decomposition and Partitioning Methods for Multistage Stochastic Linear Programs, Operations Research 33(5):989–1005, 1985. https://doi.org/10.1287/opre.33.5.989
• R. M. Van Slyke and R. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM J. Appl. Math. 17(4):638–663, 1969. https://doi.org/10.1137/0117061
• J. R. Birge, Solution Methods for Stochastic Dynamic Linear Programs, Technical Report SOL 80-29, Stanford University, 1980.
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Defs. 2.9–2.10).
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011 (nested L-shaped method for multistage problems). https://doi.org/10.1007/978-1-4614-0237-4

Motivation

A two-sided market in which each participant trades with at most one partner on the other side — houses and buyers, workers and firms, producers and consumers under exclusive bilateral contracts — is the setting of L. S. Shapley and M. Shubik's assignment game (Int. J. Game Theory 1 (1971) 111–130). Money is transferable, so the natural solution concept is cooperative: a division of the total gain that no coalition of traders can improve upon. The question the paper answers first is whether such a division exists and how to find it, given that a market with $m$ sellers and $n$ buyers has $2^{m+n}$ coalitions.

The answer, Theorem 2 of the paper, connects the core of the game with the dual of the linear-programming relaxation of the optimal assignment problem. It is the starting point of the literature on two-sided matching markets with transfers: the lattice structure of the core (Theorem 3 of the same paper), the ascending auctions of Demange, Gale and Sotomayor (J. Polit. Econ. 94 (1986)), and the equivalence of core outcomes with competitive equilibrium prices. The same LP pairing reappears in stable matching with transfers and in the VCG analysis of multi-item auctions with unit demand.

Setting

Let $M$ be a finite set of sellers and $N$ a finite set of buyers; either may be empty and their sizes need not agree. A matrix $a = (a_{ij})_{i \in M, j\in N}$ of nonnegative reals records the profit $a_{ij} \ge 0$ that the partnership of seller $i$ and buyer $j$ can realise (in the real-estate reading, $a_{ij} = \max(0, h_{ij} - c_i)$ with $h_{ij}$ buyer $j$'s valuation of house $i$ and $c_i$ its owner's reservation value).

A coalition $S \subseteq M \cup N$ is described by its sellers $A = S\cap M$ and buyers $B = S \cap N$. A matching inside $(A, B)$ is a set of seller–buyer pairs from $A \times B$ in which no player appears twice. The characteristic function (2.6) assigns to $S$ its worth

the maximum over matchings $P$ inside $S$. One-sided coalitions and singletons are worth $0$.

A payoff vector is a pair $(u, v)$ with $u \in \mathbb R^M$, $v \in \mathbb R^N$ (the paper uses $v$ both for the characteristic function and for buyers' payoffs; the formal development calls the former worth). The core is the set of payoff vectors with

The assignment LP (3.1)–(3.2) maximises $z = \sum_{i,j} a_{ij} x_{ij}$ over $x_{ij} \ge 0$ with $\sum_{i} x_{ij} \le 1$ for each $j$ and $\sum_j x_{ij} \le 1$ for each $i$. Its dual (3.3)–(3.4) minimises $w = \sum_i u_i + \sum_j v_j$ over $u_i \ge 0$, $v_j \ge 0$ with $u_i + v_j \ge a_{ij}$ for all $i, j$. The optimal values are $z_{\max}$ and $w_{\min}$.

Formalization targets

Goal: Theorem 2 (p. 118)

The statement holds for every finite $M$, $N$ and every $a \ge 0$, with no constants to fix.

Milestones, in the order the paper's argument uses them

1. Eq. (3.6), p. 118: every dual-feasible $(u, v)$ gives every coalition at least its worth.
2. Sec. 3.1, p. 117 (quoting Dantzig, p. 318): the assignment LP attains its maximum at a $0/1$ point, and $z_{\max} = v(M \cup N)$.
3. Sec. 3.1, p. 118 (quoting Dantzig, p. 129): both LPs have optima and $w_{\min} = z_{\max}$.
4. Eq. (3.5), p. 118: every dual minimiser satisfies $\sum_i u_i + \sum_j v_j = v(M \cup N)$.

Further results on the same definitions

• Sec. 3.2, p. 118: the core is nonempty.
• Sec. 3.2, p. 119: for $(u,v)$ in the core, $v_j = \max\bigl(0, \max_{i}(a_{ij} - u_i)\bigr)$ for every buyer $j$ — at the seller prices $p_i = c_i + u_i$, buyer $j$'s best net gain is exactly $v_j$.

Significance

Theorem 2 replaces the $2^{m+n}$ coalition constraints of the core with the $mn$ constraints of a linear program. Consequences stated in the paper: the core is never empty; its points are exactly the dual optimal solutions, so the core is a polytope computable by linear programming without evaluating the worth of any coalition other than the grand one; and dual variables are prices — a seller's core payoff determines a price at which every buyer's best purchase yields that buyer's core payoff. The lattice and corner results of Sec. 3.3 build on this identification.

The paper's proof is short but leans on two results quoted from Dantzig's Linear Programming and Extensions: the integrality of the rectangular assignment polytope and the LP duality theorem. A formalization makes these dependencies explicit for the inequality-constrained rectangular case with possibly unequal sides. To our knowledge Theorem 2 has no machine-checked proof. On Prove2Me, general LP strong duality is formalized (LinearOptimization.lp_strong_duality, SmaleNinth.lp_strong_duality), and integrality of the square doubly stochastic assignment LP (UnderstandingML.assignment_lp_integral, FamousTheorems.birkhoff_von_neumann); neither is the specialised statement here, but both are natural substrate.

Difficulty

The inclusion "dual optimal ⊆ core" needs the value of the dual to equal the combinatorial worth $v(M \cup N)$, which is not a statement about linear programming alone: it needs both LP duality and the integrality of the assignment polytope. The integrality needed is for the polytope cut out by inequalities $\le 1$ on a possibly non-square matrix, which is not the Birkhoff polytope of doubly stochastic matrices already on the platform; the gap between the two must be bridged.

The converse, "core ⊆ dual optimal", is dismissed as "clearly" in the paper, but the core is defined through the worth of every coalition, a maximum over exponentially many matchings, while dual optimality is a comparison with every dual-feasible vector. Neither side mentions the other's objects, and the naive reading "the core is the dual feasible set" is false: large payoffs are dual feasible and violate (3.5).

Formalization scope

Lean represents sellers and buyers as types M, N with [Fintype M] [Fintype N]; no nonemptiness is assumed, so markets with an empty side are included (there the core is $\{0\}$). The matrix is a : M → N → ℝ with the standing hypothesis ∀ i j, 0 ≤ a i j on every theorem. A coalition is a pair (A, B) : Finset M × Finset N. A matching is a Finset (M × N) inside A ×ˢ B with no repeated seller and no repeated buyer. The worth is Finset.sup' over the finite, nonempty set of matchings (the empty matching is always present), so there is no junk value. The paper's (2.6) takes exactly $k = \min(|S\cap M|, |S\cap N|)$ pairs; the formal definition takes all partial matchings, which gives the same maximum because $a \ge 0$.

Payoff vectors are pairs (M → ℝ) × (N → ℝ). The core is defined by (3.5) and (3.6) for all coalitions; nonnegativity is not a separate clause since it follows from singleton coalitions. The dual LP keeps the nonnegativity of $u$ and $v$ that (3.3) imposes, and "solutions of the LP dual" is read as optimal solutions (DualOptimal: dual feasible and of minimal objective among dual-feasible vectors), as the text preceding Theorem 2 does.

The worth is the combinatorial maximum, not the LP value, and the core is defined by coalitions, not through the dual; defining either through the other would make Theorem 2 true by unfolding, and such a formalization is ruled out. Likewise the goal is not the weaker "core = dual feasible set", which is false.

Contributions welcome: integrality of the rectangular inequality-form assignment polytope, a specialisation of general LP duality to this pair, and the coalitional inequality (3.6). The first two are reusable for any bipartite matching model.

Selected references

• L. S. Shapley and M. Shubik, The Assignment Game I: The Core, International Journal of Game Theory 1 (1971), 111–130. https://doi.org/10.1007/BF01753437
• G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963. https://doi.org/10.1515/9781400884179
• L. S. Shapley, Complements and substitutes in the optimal assignment problem, Naval Research Logistics Quarterly 9 (1962), 45–48. https://doi.org/10.1002/nav.3800090106
• G. Demange, D. Gale and M. Sotomayor, Multi-Item Auctions, Journal of Political Economy 94 (1986), 863–872. https://doi.org/10.1086/261393

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

Monotone operators from a Banach space $E$ to its dual $E^*$ are the abstract framework for nonlinear equations, variational inequalities and evolution equations, and for the convergence theory of proximal-point and splitting algorithms in infinite dimensions. Within that framework, the class that behaves well — for surjectivity results, for resolvents, for sums — is the class of maximal monotone operators. The most important source of such operators is convex analysis: the subdifferential of a convex function. Whether every subdifferential of a closed proper convex function is maximal monotone, in an arbitrary Banach space, is therefore a basic question for convex optimization in function spaces.

Timeline:

• 1964. G. J. Minty proves maximality of the subdifferential for convex functions that are finite and continuous everywhere (Minty, Pacific J. Math. 14 (1964)).
• 1965. A. Brøndsted and R. T. Rockafellar show that subgradients exist on a dense set and approximate ε-subgradients (Brøndsted–Rockafellar, Proc. AMS 16 (1965)). J.-J. Moreau develops proximal maps and conjugate duality for convex functions in Hilbert space (Moreau, Bull. SMF 93 (1965)); his later lecture notes Fonctionnelles convexes (Collège de France, 1967) are the paper's reference for conjugates in locally convex spaces.
• 1966. R. T. Rockafellar announces the general Banach-space result, for every lower semicontinuous proper convex function (Rockafellar, Pacific J. Math. 17 (1966)). H. Brézis later points out a gap in that proof: a subgradient chosen in the argument may grow without bound.
• 1970. Rockafellar gives a complete proof by a different route, valid in nonreflexive spaces, in the paper formalized here (Rockafellar, Pacific J. Math. 33 (1970)).

Setting

Let $E$ be a real Banach space with dual $E^*$ and bidual $E^{**}$, and write $\langle x, x^*\rangle = x^*(x)$. $E$ sits in $E^{**}$ through the canonical embedding.

A proper convex function on $E$ is a function $f : E \to (-\infty, +\infty]$, not identically $+\infty$, such that $f((1-\lambda)x + \lambda y) \le (1-\lambda) f(x) + \lambda f(y)$ for all $x, y \in E$ and $0 < \lambda < 1$. It is lower semicontinuous for the norm topology.

The subdifferential of $f$ is the multivalued map $\partial f : E \to E^*$,

A multivalued map $T : E \to E^*$ is monotone if $\langle x_0 - x_1, x_0^* - x_1^* \rangle \ge 0$ whenever $x_0^* \in T(x_0)$ and $x_1^* \in T(x_1)$. It is maximal monotone if, in addition, its graph $\{(x, x^*) \mid x^* \in T(x)\}$ is not properly contained in the graph of any other monotone map $T' : E \to E^*$.

The conjugate of $f$ is $f^*(x^*) = \sup_{x \in E} \{\langle x, x^*\rangle - f(x)\}$, a function on $E^*$; its subdifferential $\partial f^*$ maps $E^*$ into $E^{**}$. Finally $j(x) = \tfrac12 \|x\|^2$.

In Lean these are ProperConvex f, subdiff f, IsMonotoneOp T, IsMaximalMonotone T, conj f and halfSqNorm, all stated over an arbitrary real normed space V so that they apply equally to $E$ and to $E^*$.

Formalization targets

Goal: Theorem A (p. 210)

No reflexivity, inner product or finite dimension is assumed.

Milestones, in attack order

1. (2.2) Fenchel–Young: $f(x) + f^*(x^*) \ge \langle x, x^* \rangle$, with equality iff $x^* \in \partial f(x)$.
2. §2, p. 210. $f^*$ is a weak* lower semicontinuous (hence strongly lower semicontinuous) proper convex function on $E^*$.
3. §2, p. 211. The restriction of $f^{**}$ to $E$ is $f$.
4. Proposition 1. $x^{**} \in \partial f^*(x^*)$ iff there are a net $x_i^* \to x^*$ in norm and a bounded net $x_i \to x^{**}$ weak**, on one directed index set, with $x_i^* \in \partial f(x_i)$.
5. (3.1) $\partial(f + j)(x) = \partial f(x) + \partial j(x)$ for all $x \in E$.
6. §3, p. 213. $(f + j)^*$ is finite and continuous throughout $E^*$.
7. §3, p. 213 (Minty). On any real Banach space, a convex function that is finite and continuous everywhere has a maximal monotone subdifferential.

Significance

Theorem A places every closed proper convex function in the maximal monotone class, in every real Banach space. Downstream, it is what allows convex minimization problems to be treated by the general theory: surjectivity of $\partial f + \lambda J$ (with $J$ the duality map) in reflexive spaces, existence for evolution equations governed by subdifferentials, the definition of resolvents and proximal maps, and the convergence of proximal-point and splitting methods for convex problems. Proposition 1 is of independent interest: in a nonreflexive space $\partial f^*$ is not the inverse of $\partial f$, but it is still completely determined by $\partial f$ through bounded weak** nets.

The theorem is classical and fully proved in the literature. What this mission adds is a machine-checked proof of the nonreflexive Banach-space statement, together with the infrastructure it needs: extended-real-valued proper convex functions, the subdifferential and the conjugate on a normed space and its dual, monotone and maximal monotone operators, and the Fenchel–Moreau identity $f^{**}|_E = f$. None of these exists in Mathlib at the pinned revision, and Mathlib contains no statement of Theorem A, in Hilbert or in Banach spaces.

Difficulty

Monotonicity of $\partial f$ follows in two lines from the definition; the whole difficulty is maximality. In a Hilbert space the standard argument solves $x + \partial f(x) \ni y$ by minimizing $f + \tfrac12\|\cdot - y\|^2$ and uses the identification of $E$ with $E^*$; in a general Banach space there is no such identification, and minimizers need not exist without reflexivity. The 1966 argument tried to approximate subgradients of $f$ at nearby points, and it failed because those subgradients could become unbounded as the approximation was refined. Any argument that passes through the dual meets a second obstacle: $\partial f^*$ takes values in the bidual $E^{**}$, which is strictly larger than $E$ when $E$ is not reflexive, so $\partial f^*$ is not the inverse of $\partial f$. Relating the two is the content of Proposition 1, and its necessity half requires approximation results well beyond the definitions.

Formalization scope

Lean representation and committed conventions:

• $E$ is a real Banach space: NormedAddCommGroup E, NormedSpace ℝ E, CompleteSpace E. $E^*$ is StrongDual ℝ E with the operator norm; the pairing $\langle x, x^*\rangle$ is x' x; $E^{**}$ is StrongDual ℝ (StrongDual ℝ E) and $E \hookrightarrow E^{**}$ is NormedSpace.inclusionInDoubleDual ℝ E.
• The value set $(-\infty,+\infty]$ is EReal with the clause "never $\bot$". Properness also requires some value $\ne \top$. Convexity is the paper's inequality for $0 < \lambda < 1$, computed in EReal.
• Multivalued maps are V → Set (StrongDual ℝ V). Maximality is graph inclusion, quantified over every monotone T', not only over subdifferentials.
• The conjugate is an EReal supremum over all of $V$; the biconjugate is conj (conj f) on the bidual.
• (2.2) is stated as $\langle x, x^*\rangle \le f(x) + f^*(x^*)$ with the equality case, avoiding EReal subtraction.
• Weak* lower semicontinuity of $f^*$ is lower semicontinuity on WeakDual ℝ E.
• In Proposition 1 a net is a map from a nonempty, directed, partially ordered index type (in the universe of $E$), with convergence along atTop. Weak** convergence is pointwise convergence on $E^*$ of the canonical images, which is convergence in the weak topology induced on $E^{**}$ by $E^*$. Boundedness is a uniform norm bound.
• (3.1) reads the printed $\partial(f+j)$ as $\partial(f+j)(x)$; the right side is the pointwise (Minkowski) set sum.
• "Finite and continuous" for $(f+j)^*$ is the existence of a continuous real-valued $h$ on $E^*$ equal to it everywhere.
• Minty's case is stated for an arbitrary real Banach space $V$, because the proof applies it on $E^*$.

A trivializing formalization is ruled out: properness excludes $f \equiv +\infty$ (whose empty subdifferential is monotone but not maximal) and $-\infty$ values, maximality ranges over all monotone operators, and the index set in Proposition 1 is nonempty and directed so that no convergence statement holds vacuously.

Infrastructure needed and reusable beyond this mission: extended-real convex analysis on normed spaces (conjugates, the Fenchel–Moreau theorem via Hahn–Banach separation, lower semicontinuity in the weak and weak* topologies), subdifferential calculus for a sum with a continuous function, nets and weak** approximation in the bidual (Goldstine-type arguments), and the Brøndsted–Rockafellar approximation of ε-subgradients. Contributions are welcome at every milestone; the definitions layer and milestones 1–3 are the natural starting points.

Selected references

• R. T. Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific Journal of Mathematics 33 (1970), 209–216. https://doi.org/10.2140/pjm.1970.33.209
• R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific Journal of Mathematics 17 (1966), 497–510. https://doi.org/10.2140/pjm.1966.17.497
• G. J. Minty, On the monotonicity of the gradient of a convex function, Pacific Journal of Mathematics 14 (1964), 243–247. https://doi.org/10.2140/pjm.1964.14.243
• J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bulletin de la Société Mathématique de France 93 (1965), 273–299. https://doi.org/10.24033/bsmf.1625
• A. Brøndsted and R. T. Rockafellar, On the subdifferentiability of convex functions, Proceedings of the American Mathematical Society 16 (1965), 605–611. https://doi.org/10.1090/S0002-9939-1965-0178103-8

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$:

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.