Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Many computations need the trace of a matrix that is never formed explicitly and can only be applied to vectors: the trace of a matrix function such as or in statistics and lattice QCD, the Frobenius norm of an operator, or the number of triangles of a graph. The standard tool is Monte-Carlo estimation, introduced by M. F. Hutchinson (Hutchinson 1989): average quadratic forms over random sign vectors . Each sample costs one matrix–vector product, uses one random bit per entry, and needs only additions and subtractions.
Before Avron and Toledo (2011), only the variance of such estimators had been analysed. A small variance does not say how many samples guarantee a given relative error with a given probability. Avron and Toledo gave the first bounds of this kind for several estimators. This mission covers the bound for Hutchinson's estimator, their Theorem 7.1.
A Rademacher random variable takes the values and , each with probability . Let be symmetric positive semi-definite. Draw independent random vectors whose entries are independent Rademacher variables. Hutchinson's trace estimator is
A single sample is an unbiased estimator of (Lemma 2.1 of the paper, due to Hutchinson). For symmetric its variance is , twice the squared Frobenius mass of off the diagonal.
Given and , a random estimator is an -approximator of if
The rank is the number of nonzero eigenvalues of , counted with multiplicity.
For every symmetric positive semi-definite , every and every ,
The bound depends on only through its rank. It does not depend on the dimension , on the condition number, or on how the trace is spread over the diagonal.
Theorem 7.1 gives a practitioner an explicit number of matrix–vector products after which Hutchinson's method is guaranteed to reach relative accuracy with confidence . No bound was available before, although the method had been in wide use for two decades. The bound exceeds the one the same paper proves for Gaussian test vectors () by a factor. The authors conjecture that this factor is not needed. Later work removed it: Roosta-Khorasani and Ascher (2015) proved a rank-free bound for the Rademacher case, and Cortinovis and Kressner (2022) extended sample bounds to indefinite matrices. Sample bounds of this type underlie variance-reduced estimators such as Hutch++ (Meyer et al. 2021).
The theorem is proved in the literature. To the platform's knowledge it has no machine-checked proof. Formalizing it produces a checked Rademacher concentration inequality for averages of squared linear forms (Achlioptas' lemma, which is also a core lemma of database-friendly Johnson–Lindenstrauss projections), and a checked spectral reduction from a quadratic-form estimator to its eigen-directions. Neither is currently in Mathlib.
The estimator is not an average of independent copies of a bounded variable with a small range: a single sample can deviate from by an amount comparable to . Chebyshev's inequality with the variance of Lemma 2.1 only gives a polynomial dependence on . Hoeffding's inequality applied to directly gives a dependence on and on the size of the entries of . Unlike the Gaussian case, the estimator cannot be written as a weighted sum of independent chi-squared variables, because rotating a Rademacher vector does not give another Rademacher vector. The central difficulty is Lemma 7.2: a tail bound for that holds uniformly over every unit direction , including directions in which is far from Gaussian (for it is a constant).
Matrices are Matrix (Fin n) (Fin n) ℝ, and positive semi-definiteness is Matrix.PosSemidef. The Rademacher law is on ℝ. The sample space is Fin M → Fin n → ℝ with the product of copies of this law (hutchinsonSampleMeasure), so the law of the estimator is constructed, not assumed. . Probabilities are Measure.real, and the -approximator is Definition 4.1 verbatim. is Matrix.rank. In Lemma 7.2 the i.i.d. copies are the functions on this product space.
Corrections of printed statements, each recorded in the item's Formalization Note:
For the threshold involves . Lean's Real.log 0 = 0 turns the condition into , which agrees with the paper's reading . The conclusion then holds because , so no extra hypothesis is added. A formalization that took the law of the samples as a hypothesis could make that hypothesis unsatisfiable and the theorem vacuous; the constructed product space rules this out.
A complete development needs:
The Rademacher concentration results are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 7.2.
A Markov Decision Model (MDM) formalizes sequential decision-making under uncertainty: a controller observes the current state of a system, chooses an action, receives a reward, and the system moves to a new (random) state whose law depends on the current state and action. This framework underlies dynamic programming across operations research, economics, and engineering — inventory control, sequential portfolio choice, queueing control, and reinforcement learning are all instances of it. The finite-horizon theory developed here is the foundation on which every later chapter of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) builds, including the infinite-horizon, partially observed, and optimal-stopping variants treated later in the book.
The classical treatment of dynamic programming for finite state and action spaces goes back to Bellman (1957) and is standard textbook material (see e.g. Puterman, Markov Decision Processes, 1994). The generalization to Borel state and action spaces — needed as soon as a state variable is continuous, as in almost every financial application — requires genuine measure-theoretic care: suprema over an infinite (even uncountable) action set need not be attained, and the resulting value function need not be measurable. Bertsekas and Shreve's Stochastic Optimal Control: The Discrete Time Case (1978) is the classical reference for this general theory; Bäuerle and Rieder's treatment isolates the exact abstract hypothesis — the Structure Assumption (SAN) below — under which the finite-horizon theory goes through cleanly, separating the recursive (Bellman) machinery from the case-by-case verification of when it applies.
A Markov Decision Model with planning horizon consists of a state space and action space (measurable spaces), and, for each stage : a measurable set of admissible state-action pairs (containing the graph of some measurable selection ); a stochastic transition kernel giving the law of the next state; a measurable one-stage reward ; and a terminal reward .
A decision rule at time is a measurable with for every ; an -stage policy is a sequence of such rules. Given and an initial state at time , the process evolves as a (non-stationary) Markov chain, and the value of is the expected total reward
with value function , the best attainable expected reward. A policy is optimal if . Write for the measurable functions (never ), and define, for , the one-step operators , , and . A decision rule is a maximizer of at time if .
Under the Structure Assumption (SAN) — the existence of sets , with , mapping into , and every admitting a maximizer in — the value function satisfies the Bellman equation (with ), and every sequence of maximizers of defines an optimal policy. This is the weakest level at which the theorem holds: it names an abstract structural hypothesis rather than a specific sufficient condition (e.g. compactness plus semicontinuity, treated in a later mission), so any future refinement of sufficient conditions for (SAN) leaves this statement untouched.
Reducing an -stage optimization over an infinite-dimensional policy space to one-stage optimizations — literally the content of the Bellman equation — is what makes dynamic programming computationally and theoretically tractable at all. For finite state and action spaces this reduction is elementary (a supremum over a finite set is always attained); the content of the Structure Theorem is doing this correctly when , are general Borel spaces, where existence of the supremum and of a measurable maximizing selection are not automatic and must be assumed abstractly.
Formalizing this theorem produces machine-checked statements of the finite-horizon Bellman equation and verification theorem in the generality actually used throughout the book's finance applications (wealth is real-valued, portfolios are vector-valued — never finite sets). The statement, proof, and every hypothesis are original to this textbook chapter; no formalized version of this general-Borel-space theory exists on the platform. The closest prior art, finite state-and-action-space Bellman equations and verification theorems (e.g. discounted infinite-horizon and stochastic-shortest-path theorems for finite MDPs), is a strictly weaker special case in which the Structure Assumption's existence-of-maximizer clause is automatic; this mission's goal is not restated as a reference to that prior art; the generalization is exactly the mission's content.
The obvious first attempt — prove directly from the definitions of and — runs into two separate obstructions that (SAN) is built to bypass simultaneously. First, and are a priori different suprema (over policies versus over actions), and showing they agree requires that the pointwise supremum over decision rules of equals the supremum over bare actions — which needs a measurable selection achieving (or approaching) the action-wise optimum, not just its existence pointwise. Second, itself must be shown measurable — an a priori supremum of measurable functions over an uncountable index set (all policies) need not be measurable — before the integral even makes sense. (SAN)'s three clauses are exactly what supplies both a well-behaved measurability class closed under and a measurable maximizing selection at every stage, letting a backward induction on establish both facts together.
State and action spaces are arbitrary measurable spaces (MeasurableSpace E, MeasurableSpace A
type classes), not restricted to Borel subsets of Polish spaces, since none of this mission's
statements use topology. Time is indexed by ℕ rather than Fin N, with n < N as an explicit
side condition throughout (documented in MODERATION_NOTES.md); this changes no content but
avoids Fin-cast noise in the several backward recursions the chapter's operators require.
Extended-real values (EReal) are used throughout for value functions, restricted by hypothesis
to never equal , matching exactly; a
formalization using plain ℝ-valued value functions would be a strictly stronger — and
unfaithful — claim, since it silently assumes no policy can drive the expected reward to
.
The mission does not construct the canonical path measure on the full trajectory space via the Ionescu–Tulcea theorem; the value of a policy is instead built as an explicit backward accumulator recursion over the model's one-step kernels, which computes the same quantity by the tower property of conditional expectation. Definitions 2.1.1, 2.1.5, 2.2.2, 2.3.1, and 2.3.6 — the Markov Decision Model, (Markov and history-dependent) policies, and the operators — are restated from scratch in this mission's own namespace, since drafts in this series cannot import one another; later missions in the same series restate the same vocabulary independently. A trivializing formalization of the goal would state as an unspecified object merely postulated to satisfy the Bellman equation (Theorem 2.3.7's weaker claim) rather than as the supremum-over-policies value function fixed before the theorem — this mission states the latter.
Many matrices in scientific computing are available only implicitly: one can multiply a vector by , for instance by solving a linear system or applying a matrix function, but the entries of are never formed. Quantities such as the trace must then be estimated from a small number of matrix–vector products. Randomized trace estimators do exactly this: draw random vectors , compute the quadratic forms , and average.
Avron and Toledo (J. ACM 58(2), 2011) gave the first sample bounds of the form " samples suffice for relative error with probability " for the standard estimators. Among their results is a case in which the estimate is not merely approximate but exact: when is a projection matrix, its trace equals its rank, an integer, and rounding a Gaussian trace estimate recovers that integer with high probability. Computing the rank of a projection arises, for example, when charge densities are computed in electronic structure calculations without diagonalization (Bekas, Kokiopoulou and Saad 2007).
Let and . A projection matrix here is an orthogonal projection: is symmetric and . Equivalently, is symmetric and every eigenvalue of is or ; its rank is the number of eigenvalues equal to .
Fix a number of samples . Let be random vectors whose entries are independent standard normal random variables. The Gaussian trace estimator (Definition 3.1 of the paper) is
Its expectation is . For , denotes the nearest integer to . For , a random variable has the distribution with degrees of freedom, , if it has the law of for independent standard normal .
For a projection matrix , a failure probability , and every integer with ,
The number of samples depends on the rank and on only; there is no accuracy parameter, and none on .
The lemma turns a randomized estimator into an exact algorithm with a controlled failure probability: the rank of an implicitly given projection is obtained from matrix–vector products, independently of the dimension . It is also an instance where the paper's general relative-error bound for the Gaussian estimator (Theorem 5.2, whose sample count grows like ) is improved by exploiting the spectrum of : an absolute error below is a relative error , for which the general bound would require a number of samples quadratic in the rank, whereas Lemma 5.3 needs only a linear number.
The result is proved in the paper. The mission produces a machine-checked version of it, together with two pieces of reusable substrate: the exact law of a Gaussian quadratic form in an orthogonal projection, and a two-sided tail bound with explicit constant on the range . To the best of available knowledge, none of these statements is formalized in Mathlib; a platform mission on the Johnson–Lindenstrauss lemma states a concentration bound with a different exponent, , on the open range , which does not cover the value needed here when .
The deterministic part is short; the probabilistic part is not. The step " has independent standard normal entries because is orthogonal" is the rotation invariance of the standard Gaussian measure on , and it must be combined with the independence of the samples to identify the law of a sum of squares; this is a statement about product measures and pushforwards, not about moments. The tail bound is quoted by the paper without proof. Its constant is not the constant of the usual textbook estimates, and the bound is false outside a restricted range of (see below), so a generic sub-exponential concentration inequality with unspecified constants does not deliver it. Finally, the rounding step requires matching Mathlib's round with the event .
All declarations live in the namespace TraceEstimation.ProjectionRank. Matrices are Matrix (Fin n) (Fin n) ℝ. The sample space of is Fin M → Fin n → ℝ with the product measure Measure.pi (fun _ => Measure.pi (fun _ => gaussianReal 0 1)), so the law of the estimator is constructed, not assumed. Probabilities are Measure.real of events. "Projection matrix" is A.IsHermitian ∧ A * A = A (orthogonal projection); a non-symmetric idempotent also has eigenvalues and , but the paper's proof diagonalizes by a unitary matrix, which requires symmetry. round is Mathlib's round : ℝ → ℤ; the rank is Matrix.rank. The distribution is not defined: its role is played by the pushforward of a product of standard normals under .
Corrections of the printed text, both in the tail bound (milestone 2):
The goal keeps the paper's hypotheses: with no upper bound, and allowed (both are true cases). A statement about the event , or Eq. (2) alone, is not the goal; the goal is about . The sample measure is a probability measure, so the bound is not vacuous.
Contributions welcome beyond the milestones: rotation invariance of the standard Gaussian vector under orthogonal matrices, the moment generating function of , and the spectral fact for idempotents, each reusable well outside this mission.
Cooperative games model the division of a jointly produced surplus, or a jointly incurred cost, among the participants of an enterprise: towns sharing a water supply system, divisions of a firm sharing overhead, members of a consortium sharing the savings of joint investment. In such applications allocations are rarely fixed once and for all. Costs and revenues are re-estimated, projects are re-scoped, and the allocation is recomputed. A natural requirement on any allocation method is then monotonicity: when the underlying data change in a player's favour, that player's share should not fall.
H. P. Young, Monotonic Solutions of Cooperative Games (Int. J. Game Theory 14, 1985), studies several forms of this principle. The weakest, aggregate monotonicity, asks that no player lose when only the value of the grand coalition increases; Megiddo (1974) had already shown that the nucleolus violates it. The paper's first theorem concerns a stronger and more natural form, coalitional monotonicity, which was first proposed by Shubik (1962) in the context of cost allocation within a firm, and shows that it cannot be reconciled with the core, the most widely used stability requirement. This mission formalizes that impossibility theorem.
Fix players, . A cooperative game on is a function assigning a real number to every coalition , with . No superadditivity or other structural assumption is imposed.
An allocation procedure is a map that assigns to every game on an allocation satisfying efficiency:
The core of is the set of allocations that no coalition can improve upon on its own:
It may be empty. An allocation procedure is a core allocation rule if for every game whose core is nonempty. The nucleolus is the standard example.
An allocation procedure is coalitionally monotonic (Eq. (4) of the paper) if raising the value of a single coalition, with all other values unchanged, never decreases the allocation of any member of that coalition: for all games and every coalition ,
The paper notes that this is equivalent to its one-player form (5): if every coalition containing player weakly gains in value and every coalition not containing is unchanged, then does not decrease.
In the Lean development these objects are Game n, IsAllocationProcedure, IsCoreRule and IsCoalitionallyMonotonic in the namespace MonotonicSolutions.CoreRules, and the core is the published definition Supermodularity.Cooperative.Core.
For every ,
An additional statement records the paper's remark that the egalitarian rule satisfies (5), so that the monotonicity axiom on its own is satisfiable.
The theorem shows that no refinement of the core, however cleverly designed, can be coalitionally monotonic once there are five or more players. For the nucleolus this strengthens Megiddo's earlier observation, and the paper uses it to motivate the search for monotonic solution concepts outside the core, which leads to its second theorem: the Shapley value is the unique symmetric allocation procedure satisfying an even stronger monotonicity property (the subject of the companion mission). In cost-allocation practice the result says that an allocation method that is always stable against coalitional secession must sometimes penalise a division for making its own operations cheaper.
The result has been proved since 1985, and its proof is a short explicit counterexample. What the formalization adds is a machine-checked version of the counterexample (two explicit games whose cores are single points), a verified equivalence between the coalition-wise and player-wise forms of monotonicity, and the extension from five to arbitrarily many players, which the paper dismisses as an "obvious extension". To the best of the curators' knowledge none of these statements is formalized in any proof assistant.
The individual steps are elementary, but each requires care. Determining the core of each counterexample game exactly means showing both that the given point satisfies all coalition constraints and that no other point does. The equivalence of (4) and (5) is stated in the paper as following from "successive application" of (4), and every game involved must vanish on the empty coalition. The two counterexample games differ on two coalitions, and , so a single application of (4) does not suffice. Finally, the paper passes from five players to players with the words "by obvious extension"; a formal proof has to make that step explicit, for arbitrary and for rules defined on all games with players, not only on those derived from five-player games.
Fin n; the paper's player is the Lean index . Thus the core points and appear as ![0,1,2,7,1] and ![3,0,0,6,3], and the players "2 and 4" whose allocations decrease are indices 1 and 3.Game n := {v : Finset (Fin n) → ℝ // v ∅ = 0}. Monotonicity axioms therefore quantify only over normalised games, as in the paper.Fin n → ℝ. Efficiency is part of the goal's hypotheses, matching the paper's definition of an allocation procedure.Supermodularity.Cooperative.Core Finset.univ v.1, the published core definition from Supermodularity and Complementarity, which coincides with the set on p. 68 of the paper.IsCoreRule requires only when is nonempty. The unconditional requirement would be unsatisfiable, because some games have an empty core, and would make the goal trivially true; that reading is ruled out.IsCoalitionallyMonotonic is Eq. (4) with ranging over all coalitions, including . Restricting to , or restricting the games to superadditive ones, would change the theorem.YoungGames: for , the value is the largest listed over the , and if there is none.Contributions welcome: proofs of the four milestones and the goal; a general lemma that padding a game with null players preserves the core up to zeros, which is reusable for other small-counterexample results in cooperative game theory; and decision procedures for linear feasibility over the coalitions of small games.
Mission XII (12-packet-networks-model) built the discrete-time, slotted packet-network model
from scratch and proved the chapter's own version of the fluid-to-stochastic stability bridge
(Theorem 12.10). That result is only useful once paired with an actual control policy whose fluid
model can be shown stable. 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) supplies exactly such a policy in Sections
12.4-12.5: back-pressure control (called max-weight when the network is single-hop), a rule
that has become the default choice in the switching and wireless-scheduling literature because it
requires no advance knowledge of arrival rates and achieves the largest possible stability region.
This mission formalizes back-pressure control for the discrete-time packet network model and
proves it maximally stable — the chapter's own counterpart to mission VIII's continuous-time
Theorem 9.12.
At the start of each timeslot, having observed the current buffer contents , the max-weight/ back-pressure (MW/BP) policy solves (Eq. 12.41), where restricts the schedule set (mission XII) to what is actually available given . Equivalently (Eq. 12.42-12.43), writing (with ) for the "weight" of activity , the policy maximizes — the schedule that clears the most "backlog pressure" per timeslot. The policy is deterministic (no randomization variable is needed, since (12.41) is a genuine optimization problem, not one that inherently requires randomized tie-breaking).
Consider a packet network satisfying (12.1) and Assumption 12.1, operating under back-pressure control. The DTMC is aperiodic and irreducible unconditionally. If the stability condition (12.26) — the existence of with — is additionally satisfied, is positive recurrent. This is the mission's headline result, and it packages both a structural fact (irreducibility/aperiodicity, needed regardless of load) and a conditional stability fact (positive recurrence, needed only under (12.26)) in one theorem.
Lemma 12.17 shows the optimization problem (12.41) always has a nonzero solution whenever the network is nonempty — the fact that back-pressure never "idles unnecessarily," which Lemma 12.18 uses to show every state can reach the empty state (hence irreducibility) and that state has period (hence aperiodicity, via (12.1)'s own assumption that no external arrivals is possible with positive probability). Lemma 12.20 is the back-pressure fluid equation (12.44), the discrete-time analog of mission VIII's Theorem 9.8: at each regular point, the fluid-scaled buffer content dotted with the fluid departure rate equals the maximum of that same dot product over the convex hull of the schedule set. Lemma 12.21 shows this fluid model is stable whenever (12.26) holds, via an explicit quadratic Lyapunov function.
The result itself. Theorem 12.16 shows that back-pressure control — a rule requiring no knowledge of arrival rates, computed fresh from the current buffer contents every timeslot — is maximally stable: combined with Theorem 12.8 and Proposition 12.9 (mission XII), it stabilizes every packet network arrival-rate vector that any policy could possibly stabilize. This is the discrete-time, slotted analog of mission VIII's Theorem 9.12, and the two proofs share their essential Lyapunov argument (the book's own text calls Lemma 12.21's proof "almost identical to that of Theorem 9.12"), even though the two chapters' back-pressure equations are built from different underlying objects — mission VIII's continuous-time allocation polytope versus this chapter's convex hull of a discrete schedule set.
Formalizing it. A live prior-art check (GET /theorems?q=back-pressure, q=max-weight) finds
no relevant hits, matching mission VIII's own finding for the continuous-time version. This
mission formalizes the back-pressure optimization problem and policy, the back-pressure fluid
equation, and its stability from scratch, restating (per this series' convention for
concurrently-drafted chunks sharing a sub-namespace) the minimal apparatus needed from mission
XII: the packet network model, Assumption 12.1, the raw processes, fluid limit paths, the fluid
equations (12.31)-(12.36), and the ambient-chain machinery, plus a new Aperiodic predicate this
chunk needs that mission XII's own results do not.
The obvious approach to Lemma 12.20's back-pressure fluid equation — directly differentiate the discrete system equation — obscures the actual argument, which reduces a maximum over the (potentially non-polytope) discrete schedule set to a maximum over its convex hull (justified because a linear functional on a compact polytope is maximized at an extreme point) and then shows that every schedule with a strictly smaller objective value than the maximizer contributes zero derivative to the usage-counting process — the discrete-time analog of mission VIII's Lemmas 9.10-9.11. A second difficulty is connecting the maximum-over-a- finite-set at the fluid-scaled level to Definition 12.3's discrete, arrival-indexed back-pressure policy: this mission's own Lemma 12.20 item states the fluid-relevant consequence of the discrete policy as a documented hypothesis (mirroring mission XI's own scope decision for its structurally identical WWTA fluid equation) rather than re-deriving it from the raw stochastic recursion, which would require reconstructing infrastructure outside this chapter's own numbered results.
The packet network model, Assumption 12.1, the raw processes, and the fluid-limit apparatus are
restated verbatim from mission XII (12-packet-networks-model), since concurrently-drafted chunks
sharing a sub-namespace do not import one another's Lean files. IsBPOptimal is phrased via
domination over the feasible-at- schedule set, not sSup/argmax, per this series'
junk-value-avoidance convention; the same convention is applied to the maximum over in the back-pressure fluid equation. The formalization does not admit a trivializing
reading: irreducibility and aperiodicity are the same non-vacuous renewal-theoretic notions used
throughout this series (Aperiodic requires a genuine positive self-transition probability, not a
vacuously-true condition), and the goal's positive-recurrence conjunct is genuinely conditional on
(12.26), stated with the correct strict inequality rather than weakened to . Contributions
completing the five by sorry proofs are welcome, particularly Lemma 12.17's hop-count induction
and Lemma 12.20's extreme-point/zero-derivative argument (mirroring mission VIII's own Lemmas
9.10-9.11, adapted to discrete time).
Internet routers, wireless base stations, and data-switch fabrics all face the same recurring decision: in each discrete time slot, which of many possible transfer operations should be executed, given the packets currently queued and the physical constraints (link capacities, interference between simultaneous transmissions) on what can be done at once? 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 12 to exactly this question, under the name packet networks. Unlike every prior chapter of the book, which works in continuous time with Poisson-driven Markov chains, this chapter builds its stability theory from scratch for a discrete-time, slotted model — the natural setting for a system that makes one scheduling decision per clock tick. This mission formalizes the chapter's foundational layer: the model itself, its notion of a feasible schedule and control policy, subcriticality, and the discrete-time fluid-limit machinery that Chapters 13 and 14 (back-pressure control and random proportional scheduling, respectively) build their own stability proofs on top of.
A packet network (Section 12.1) has I packet classes and J activities (service types);
activity transfers a packet from its input class to its output class (or
removes it from the network if ), giving an input-output matrix . A
processing plan for class (Definition 12.2) is a chain of activities from to exit;
Assumption 12.1 requires every class to have one and forbids cycles. In each timeslot the
system manager chooses a schedule from a feasible set satisfying the
packet-availability constraint (the current buffer contents); is typically built
(Section 12.2) from a link usage matrix and a set of feasible link configurations
via , . A Markovian control policy
(Definition 12.3, Eq. 12.8) chooses from the current buffer
contents and an independent randomization variable; it is admissible if it never overdraws a
buffer, and stable if the resulting discrete-time Markov chain is irreducible and positive
recurrent.
If the DTMC under a Markovian policy is irreducible and its fluid limit is stable (Definitions 12.14-12.15), then is positive recurrent. This is the chapter's own version of Theorem 6.2 (mission III) — the technical fulcrum that lets a deterministic fluid-model stability argument certify the stability of the original discrete, stochastic system — restated for a genuinely different probabilistic model, since Theorem 6.2 was built under continuous-time, Poisson-arrival hypotheses this chapter does not share.
Propositions 12.6-12.7 characterize the convex hulls and as explicit polytopes cut out by the link usage matrix — the combinatorial core that Theorem 12.8 (stability implies subcriticality, this chapter's analog of Theorem 5.2) and Proposition 12.9 (a necessary condition for subcriticality) both build on. Lemma 12.11 records that the schedule-usage counting process is Lipschitz; Lemma 12.12 is the functional strong law of large numbers the external arrival process satisfies; and Theorem 12.13 combines them to establish existence of discrete-time fluid limits satisfying the chapter's own fluid equations (12.31)-(12.36) — the chapter's analog of Theorem 6.5.
The result itself. Theorem 12.10 is what makes the rest of Chapter 12 (and Chapters 13-14) tractable: rather than analyzing an infinite-state discrete-time Markov chain's positive recurrence directly — a notoriously hard problem in general — it suffices to exhibit a deterministic fluid model and show every solution of that fluid model empties in finite time. This is the same strategy Chapter 6 established for the book's continuous-time model, but Chapter 12 cannot simply invoke that earlier theorem: the packet network model uses discrete time slots rather than a continuous clock, and its probabilistic structure (arbitrary i.i.d. arrival increments rather than Poisson arrivals) is different enough that the fluid-limit compactness argument has to be redone, even though — as the book's own text notes — "the proof mimics that of Theorem 6.2."
Formalizing it. A live prior-art check (GET /theorems?q=packet+network,
q=discrete-time+Markov+chain, q=slotted+time) finds no relevant hits. A dedicated further
check for MarkovMixing, a different mission's own corpus offering a PositiveRecurrent
predicate for Markov chains, found a representationally distinct formalization (a row-function
transition kernel rather than this series' own PMF-based jump-chain convention); this mission
restates positive recurrence and irreducibility locally instead, consistent with every mission in
this series since mission I. Everything else — the packet network model, schedules and
configurations, the subcritical region, Markovian policies, and the discrete-time fluid-limit
apparatus — is formalized from scratch.
The most consequential decision in this mission is representational, not mathematical: Theorem 12.10's fluid-limit-stability hypothesis quantifies over all fluid limit paths, which are themselves scaling limits of a genuinely stochastic discrete-time process — reconstructing that process from Chapter 2/4's own primitive stochastic elements (arrival processes, phase-type service mechanics) would require rebuilding infrastructure this chapter's own numbered results do not supply. Following mission III's own precedent for its structurally identical Theorem 6.5, this mission instead takes the raw, per-initial-state schedule-usage and arrival processes as given data satisfying only the recap properties the chapter's own proofs actually cite (Eq. 12.9-12.10's system equation, monotonicity), and fixes a single sample point together with an explicit SLLN hypothesis rather than a bare "for almost all " quantifier — matching the book's own statement of Theorem 12.13, which itself begins "Fix an " rather than quantifying almost everywhere within the theorem itself. A second difficulty is genuinely combinatorial: Proposition 12.6's proof constructs an explicit product-form probability distribution over schedules (one independent randomization per link) whose mean recovers an arbitrary point of the polytope — a real combinatorial argument, not a formal consequence of the convex-hull operator's definition.
Classes, activities, links, schedules and configurations are represented via Fin-indexed types
throughout; S and C are taken as Finsets (every worked example in the book has finitely many
configurations, and the link usage matrix's single-1-per-column structure bounds each schedule
component, so this is a genuine, if implicit, standing feature of the model rather than an added
restriction). IsScheduleSetAt/IsScheduleSet characterize / via an ↔ against the
underlying capacity constraint, rather than constructing them, matching how set-valued model data
is handled elsewhere in this series. The formalization does not admit a trivializing reading: the
ambient chain's positive recurrence (PositiveRecurrent) is the same non-vacuous renewal-theoretic
notion used throughout this series, PacketFluidLimitStable quantifies over every genuine fluid
limit path (not a hand-picked one), and subcriticalRegion is stated with a strict inequality
() exactly as Eq. 12.24 requires, not weakened to . Contributions completing
the eight by sorry proofs are welcome, particularly Proposition 12.6's explicit randomized-
schedule construction and Theorem 12.13's compactness argument (mirroring mission III's own
Theorem 6.5 proof, adapted to discrete time).
Large-scale data-intensive computing splits a job into many small "map tasks," each of which must be assigned to one of thousands of general-purpose servers in a data center — the MapReduce paradigm introduced by Dean and Ghemawat (2008). Because a task's input data is stored on only a few of those servers, routing it to a server that already holds its data ("data locality") avoids costly network transfer, so a task-allocation policy that ignores locality can leave a server farm badly underutilized even when raw compute capacity is ample. 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 11 to a rigorous stability analysis of Xie, Yekkehkhany, and Lu's (2016) workload-weighted task allocation (WWTA) policy, which routes each arriving task to whichever eligible server currently carries the least (locality-weighted) backlog. This mission formalizes the chapter's central result: WWTA is not merely a reasonable heuristic but is maximally stable — it keeps the system stable whenever any routing policy could.
A task allocation model (Sections 11.2-11.3) has L task categories and K servers; a class
is a pair , a category routed to a specific server, with mean service time (Eq. 11.3) reflecting both data locality (local, rack-local, or remote access) and the server's
relative processing speed. Tasks in category arrive according to a Markovian arrival
process (MArP) with long-run average rate — a substantially more general model than
the independent Poisson streams used elsewhere in the book, needed to capture batches of map tasks
generated from a single job. Routing is by immediate commitment: each task is assigned to a
server the instant it arrives, based only on its category and the current backlog, with no
possibility of later reassignment. The workload of server at time (Eq. 11.7) is
, the locality-weighted total backlog assigned to it.
Workload-weighted task allocation (WWTA), Definition 11.3, routes an arriving category-
task to any server achieving (Eq. 11.8, ties broken
arbitrarily), where is the workload vector's left limit at the arrival instant.
If there exists with for each category (Eq. 11.4) and for each server (Eq. 11.5), then the WWTA fluid model — the deterministic fluid equations (11.11)-(11.16) that arise as scaling limits of the stochastic model under WWTA control — is stable: every solution reaches the zero state in finite time proportional to its initial size.
Lemma 11.2 shows this load condition is equivalent to subcriticality of the task allocation model, in the sense of Section 5.2's general definition, reducing an existence statement over the model's full apparatus to a simple linear-feasibility check. Theorem 11.4 establishes that fluid limits of the stochastic model exist and satisfy the general fluid equations (11.11)-(11.15) under any immediate-commitment routing policy, and the WWTA-specific equation (11.16) under WWTA — the chapter's version of the fluid-limit machinery Chapter 6 builds for the book's standard model, adapted to Markovian (not Poisson) arrivals and immediate-commitment routing. Theorem 11.5 is the corresponding replacement for Theorem 6.2 (mission III): fluid limit stability implies stability of the original stochastic model. Corollary 11.7 is the mission's other headline consequence: WWTA is maximally stable, stabilizing the model whenever any simply structured routing policy could.
The result itself. A task-allocation heuristic motivated purely by an intuitive "balance-the-weighted-backlog" idea turns out to have the strongest stability guarantee a policy can have: it never needs re-tuning as arrival rates change, and no alternative policy can stabilize a regime WWTA cannot. Xie, Yekkehkhany, and Lu (2016) proved this fact (calling it "throughput optimality") by direct analysis of the discrete stochastic model using a quadratic Lyapunov function; Dai and Harrison's contribution is to prove the same conclusion via the fluid-model route, and — because the task allocation model violates two of the standing assumptions under which Chapter 6's general theory was built (MArP rather than Poisson arrivals, immediate-commitment routing rather than the book's default relaxed control) — to show that the general fluid-stability machinery survives those changes with only minor modification.
Formalizing it. A live prior-art check (GET /theorems?q=task+allocation,
q=server%20farm, q=data%20locality) finds no relevant hits on the platform (workload returns
one unrelated text-corpus-statistics result). This mission formalizes the task allocation model,
WWTA, the fluid equations, and the stochastic-to-fluid bridge from scratch, reusing Mathlib's
general real-analysis, measure-theory, and PMF-based Markov-chain substrate, and restating (per
this series' convention for concurrently-drafted chunks) the minimal apparatus needed from
missions I and III.
The obvious approach to Definition 11.3 — pick a canonical minimizer of ,
e.g. via Finset.min' — silently narrows WWTA to a single tie-breaking rule, when (11.8)
explicitly allows any minimizer; this mission instead states WWTA as domination over every
server, accepting every admissible tie-break. A second difficulty is genuinely structural: Theorem
11.4's "for almost all " existence claim is a measure-theoretic statement about a
probability space that mission III's own analogous Theorem 6.5 sidesteps by fixing a sample point
together with the specific SLLN limit that argument needs — this mission follows the same
precedent rather than introducing a bare "almost everywhere" quantifier, which does not by itself
supply the type information Lean's typeclass resolution needs to identify an ambient measure. A
third is connecting Definition 11.3's discrete, arrival-indexed routing rule to the raw
(pre-limit) process family that Theorem 11.4's existence argument operates on: the book's own proof
derives the needed consequence (Eq. 11.22, "server receives no more category- tasks in a
neighbourhood of ") via an explicit - argument from the discrete policy,
which this mission takes as a documented hypothesis rather than re-deriving, since building the
arrival-sequence-to-counting-process reconstruction is genuinely Chapter 2/4 machinery outside this
chapter's own numbered results.
Classes are represented as pairs (ℓ,k) : Fin L × Fin K rather than flattened to a single index,
avoiding an arbitrary choice of encoding. TaskAllocationProcessFamily, FluidLimitPath, and
TaskAllocationFluidLimitStable restate mission III's SPNProcessFamily/FluidLimitPath/
FluidLimitStable apparatus, adapted to this model's (E,D,Z) triple and doubly-indexed classes;
PositiveRecurrent restates mission I's renewal-theoretic positive-recurrence notion. The
formalization does not admit a trivializing reading: IsWWTA accepts every admissible tie-break
rather than a single canonical one, SatisfiesWWTAFluidEquation requires Nonempty (Fin K) so its
min_{k} is a genuine minimum rather than a junk value at zero servers, and the goal's conclusion
WWTAFluidStable is the same non-vacuous fluid-model-stability predicate (Definition 6.3,
specialized) used throughout this series. Contributions completing the five by sorry proofs are
welcome, particularly Theorem 11.4's fluid-limit compactness argument (mirroring mission III's own
Theorem 6.5 proof) and Theorem 11.6's explicit quadratic-Lyapunov-function argument.
An inventory manager who stocks many products, faces random demand and pays ordering, holding and shortage costs must decide each period how much of each product to order. In general the optimal decision depends on the whole state and is found by solving a dynamic programme, which becomes impractical as the number of products grows. Myopic (or base stock) policies avoid this: in each period they aim at a target level computed from that period's data alone. Knowing when such a policy is optimal over an infinite horizon tells a practitioner when the multi-period problem decouples into a sequence of one-period problems.
Arthur F. Veinott, Jr. gave such conditions in Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem (Management Science 12(3):206–222, 1965). Earlier results of this type were for a single product (the paper cites Karlin, Management Science 6(3), 1960, Bellman–Glicksberg–Gross, Management Science 2(1), 1955, Iglehart–Karlin 1962, and the Arrow–Karlin–Scarf volume of 1958); Veinott's model allows several products, several demand classes, costs and demand distributions that change over time, general ordering constraints and general stock dynamics (backlogging, lost sales, and mixtures), and it does not use the functional equation of dynamic programming. Instead, the proofs analyse the inventory process directly.
There are products and demand classes. Vectors are compared componentwise: means for all . In period the manager observes the inventory vector (negative coordinates are backlogs) and orders up to a vector , subject to , where is a vector of extended-real functions (for instance forbids disposal). A random demand vector with law and values in a Borel set then occurs, and the next inventory vector is . The demands are independent. Ordering costs , the holding and shortage cost is , and is the discount factor of period .
Regrouping the ordering costs gives the one-period cost
with discount weights and . The integrals are assumed finite, and with . An ordering policy chooses as a Borel function of the past; it is feasible if and for every possible history. Its cost is
and a feasible policy of least cost is optimal.
Let minimize over . When is not attainable from , the minimal feasible level is the least element of . The base stock ordering policy orders up to if and up to otherwise.
The hypotheses are: (3a) minimizes over ; (3b) for ; (3c) is closed and linearly ordered by ; (3d) and are nondecreasing on , and is nondecreasing where .
Under (3a)–(3d), the base stock ordering policy
is feasible and optimal: for every feasible .
The theorem shows that under (3a)–(3d) the infinite-horizon, nonstationary, multi-product problem is solved by one-period optimization: compute from alone, and when it is unreachable order the least feasible amount. No value function is computed. It covers backlogging and lost sales, products stocked in fixed proportions, and time-varying cost and demand data, and Theorem 3.1 alone settles the frequent case in which the initial stock is small.
The result is proved in the paper. To our knowledge it has not been machine-checked: this mission produces a Lean model of a general stochastic, infinite-horizon, multi-product inventory problem (feasible policies, the expected discounted cost with allowed), and a checked proof that a myopic policy is optimal in it. The model and its cost are reusable for other base stock and myopic optimality results.
The obvious argument would compare the base stock policy with an arbitrary policy period by period using (3a) alone. That fails once is unreachable. The base stock policy then holds less stock than would require, and it has to be shown that no other policy can reach a lower-cost level later. The proof couples the two trajectories along every demand path, using the monotonicity in (3d) and the linear order of from (3c), until the base stock level becomes attainable, after which (3b) keeps it attainable. The formal difficulties are:
Periods are 0-based in Lean (Lean period is the paper's period ). Vectors are Fin n → ℝ with the product order; takes values in Fin n → EReal. Policies are functions of the past demands. The paper shows on p. 219 that this loses no generality once is fixed. The cost is excess, a -valued series of lower Lebesgue integrals of , plus the finite real , taken in EReal. A divergent series therefore gives and never the junk value . "Minimal element" is IsLeast. The in the statements is the integral of built from the data, and the policy in the goal is constructed from , , and . Neither is an arbitrary object satisfying the conclusion. The goal concludes optimality, which includes feasibility: a pathwise or conditional statement would not be the theorem.
Hypotheses added relative to the page, each used by the paper without being stated:
A complete development needs: least elements of closed chains in ; measurability of the least-element selection ; a Fubini/independence argument for ; and monotone summation of lower integrals. The least-element lemma and the cost encoding are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments.
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.
Fix a unitary network operating under PF control with mean service times , routing matrix , a partition of job classes into demand groups , and a reduced allocation set (all restated from mission IX, Definition 10.3). The entropy Lyapunov function (Eq. 10.38, mission IX) admits an alternative decomposition in terms of the within-group entropy term
with the convention that the term for class is when . Here / 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 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 and it is stable for every in the network's stability region — the largest region any policy could possibly stabilize.
for the single PF policy value (its implementation never depends on ). 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 -independent policy stable throughout the subcritical region is automatically maximally stable), it upgrades a single- stability statement to the strongest form the book's own framework can express.
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 at every regular point with ; Lemmas 10.12-10.14 establish continuity and two successively sharper Dini-derivative bounds on the within-group entropy term ; Lemma 10.15 shows that positivity of the departure rate 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.
The result itself. A stability theorem tied to one fixed 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 , 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.
The obvious approach to Corollary 10.16 — restate "maximally stable" with an explicit
-dependent policy family and add "the policy doesn't actually depend on " as a
side hypothesis — obscures the point: a policy that is definitionally independent of
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 -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.
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).
Dynamic pricing under limited inventory is a core problem of revenue management: a seller holds 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 .
A single product is sold over periods starting from inventory . In period the seller charges a price , and the demand is a nonnegative random variable with finite mean , whose law may depend on and arbitrarily. With inventory the seller sells units; unmet demand is lost.
The optimal expected revenue is defined by the Bellman recursion ,
The deterministic problem (32)–(33) is
and denotes an optimal solution. The deterministic-price heuristic charges in period regardless of sales. Its period demands are independent, is the cumulative demand, and its expected revenue is
With , eq. (34) defines
and is the coefficient of variation of the total demand.
Assume that is concave and is convex on for each , that some price has , and that is optimal for (32)–(33). Then
The constants are the paper's, and the goal is the full chain.
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 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.
The upper bound is the hard part. The natural induction replaces by and applies Jensen's inequality, but is at capacities where the remaining deterministic problem is infeasible, while 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 under the Slater point 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 is found, but it is not in Mathlib.
Fin N, 0-based. Demand laws are μ n p : Measure ℝ, probability measures carried by with finite mean, required at every price (laws at negative prices never enter a statement).⨆ over , so no supremum takes a junk value; the paper's is valueToGo M (N - n + 1). Ratios use its real value.EReal supremum over the feasible set ( if infeasible). In the goal is an optimal solution, so is its objective value.Trivializing formalizations ruled out: is defined by the Bellman recursion, not as a supremum over an unspecified policy class or as a variable constrained by hypotheses; 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 for infinite variance.
Needed infrastructure: measurability of the Bellman integrand (monotonicity of in inventory), Jensen's inequality for (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.
Multistage stochastic linear programs model decisions taken in periods while a random vector 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.
Fix a node of a finite scenario tree: scenario at period , with decision . Its ancestor's decision enters only through the right-hand side of its equality rows. After feasibility cuts and optimality cuts have been added, the node solves the scenario problem (7):
over and a free scalar , which stands in for the expected future cost. During NDSPA's forward pass the node also carries the restriction ; a last-period node has no future cost and keeps that restriction.
A descendant problem (period , scenario ) has the same shape, with right-hand side depending on the node's decision . Two kinds of cut flow from descendants to the node:
A cut is valid when never exceeds the weighted sum of the descendants' objective values at feasible points, for any . A basic solution of (7) is a point at which all equality rows hold and linearly independent constraints are active; it is degenerate when more than constraints are active.
Let two distinct valid optimality cuts bind at . Let each descendant have an optimal basic feasible solution and an optimal dual vector at , and suppose the Step 3a cut built from these duals fails (9), so that . Then
If descendant generates feasibility cut of the node and that cut binds at , then
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.
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.
Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the variable of (7) is Fin (n+1) → ℝ with its last coordinate. The paper suppresses transposes; here they are explicit, and a row vector times a matrix () 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 included. A last-period node is represented with the restriction , 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:
Correction to the page. Step 3a prints and . The formalization completes with the terms from the descendants' own cuts, without which the cut is not a valid lower bound when the descendants carry cuts. It also adds weights ; conditional probabilities are a special case, and is the printed sum. The data , may differ between descendants, which is more general than the paper.
Proposition 3 is vacuous when the descendant is infeasible at ; 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.
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.
The PF allocation function solves, for a demand vector , the concave optimization problem (Eq. 10.3-10.4) over a bounded, closed, convex, monotone capacity-constraint set . When has the special "aggregate" structure induced by grouping classes with identical resource requirements into demand groups, satisfies a resource-relevant aggregation property (Proposition 10.2): its value depends on the full demand vector only through group-level aggregates. Applying 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).
If the load condition (10.37) — an equivalent, group-level-aggregate reformulation of the standard load condition — 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.
Lemma 10.1 establishes that 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 (Eq. 10.38) that Theorem 10.5's proof needs: nonnegativity (and strict positivity away from the origin), continuity on , 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.
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 () 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.
The chapter's own convention , (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 for some , 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: 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 , not merely about an
arbitrarily-chosen selection from a possibly-multivalued correspondence.
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 on ) 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.
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 sellers and buyers has 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.
Let be a finite set of sellers and a finite set of buyers; either may be empty and their sizes need not agree. A matrix of nonnegative reals records the profit that the partnership of seller and buyer can realise (in the real-estate reading, with buyer 's valuation of house and its owner's reservation value).
A coalition is described by its sellers and buyers . A matching inside is a set of seller–buyer pairs from in which no player appears twice. The characteristic function (2.6) assigns to its worth
the maximum over matchings inside . One-sided coalitions and singletons are worth .
A payoff vector is a pair with , (the paper uses 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 over with for each and for each . Its dual (3.3)–(3.4) minimises over , with for all . The optimal values are and .
The statement holds for every finite , and every , with no constants to fix.
Theorem 2 replaces the coalition constraints of the core with the 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.
The inclusion "dual optimal ⊆ core" needs the value of the dual to equal the combinatorial worth , 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 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).
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 ). 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 pairs; the formal definition takes all partial matchings, which gives the same maximum because .
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 and 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.
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.
A Leontief network (Definition 9.5) is an SPN whose input-output matrix satisfies two assumptions: Assumption 9.1, that each activity has a unique buffer it draws material from (so , the buffer served by activity , 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 of service rates that maximizes the bilinear objective , where is the current vector of buffer contents. The "relaxed" version of the policy allows to range continuously over the allocation polytope ; 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 is the subcriticality condition throughout this chapter, exactly as in missions II, III, and V.
Consider a Leontief network operating under the relaxed back-pressure control policy. If the static planning problem has optimal objective value , 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.
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 "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 -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.
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 , , , 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.
The chapter's central subtlety is that "operating under back-pressure control" cannot be
stated directly as a hypothesis on the fluid-limit path 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 " 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
..."). 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.
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.
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:
A learning problem consists of a hypothesis class (nonempty), an instance set with a -algebra, and an objective with for all . Given a probability distribution on and an i.i.d. sample , the following quantities are defined:
A learning rule maps each sample of each size to a hypothesis . A rate is a non-increasing sequence tending to . For a rule the paper defines the following properties:
Average-RO stability (Definition 5) is the in-expectation analogue, with the replacement point also serving as the test point.
The problem is learnable if and only if there is a learning rule that is uniform-RO stable and universally an AERM. Quantitatively, if is universally consistent with rate , then some rule is uniform-RO stable and universally AERM with
and conversely, a uniform-RO stable universal AERM is universally consistent with rate .
These follow the order of the paper's proof.
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 . 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.
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 , and a naive argument under 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 where Lemma 16's hypothesis cannot be met.
Samples are Fin m → Z, the sample law is Measure.pi, and is Function.update S i (S' i). Learning rules have type (m : ℕ) → (Fin m → Z) → H, and every property is asserted for . The minimal empirical risk and are real infima over the nonempty, bounded-below family, never values at a chosen minimiser. Rates are non-increasing on and tend to . and are Nat.sqrt (Nat.sqrt m) and Nat.sqrt m, the paper's read at an integer sample size. The paper's is replaced by any bound (all rates increase in ).
The paper never discusses measurability. This formalization adds one standing assumption, identical across the series: each is measurable, the minimal empirical risk is measurable (true for countable , for example), and every learning rule, whether assumed or asserted to exist, has jointly measurable. Without this a non-measurable rule would have Bochner integrals equal to , 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 "-generalizing" where Lemma 20 gives . The stated 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).
Monotone operators from a Banach space to its dual 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:
Let be a real Banach space with dual and bidual , and write . sits in through the canonical embedding.
A proper convex function on is a function , not identically , such that for all and . It is lower semicontinuous for the norm topology.
The subdifferential of is the multivalued map ,
A multivalued map is monotone if whenever and . It is maximal monotone if, in addition, its graph is not properly contained in the graph of any other monotone map .
The conjugate of is , a function on ; its subdifferential maps into . Finally .
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 and to .
No reflexivity, inner product or finite dimension is assumed.
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 (with 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 is not the inverse of , but it is still completely determined by 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 . None of these exists in Mathlib at the pinned revision, and Mathlib contains no statement of Theorem A, in Hilbert or in Banach spaces.
Monotonicity of follows in two lines from the definition; the whole difficulty is maximality. In a Hilbert space the standard argument solves by minimizing and uses the identification of with ; 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 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: takes values in the bidual , which is strictly larger than when is not reflexive, so is not the inverse of . Relating the two is the content of Proposition 1, and its necessity half requires approximation results well beyond the definitions.
Lean representation and committed conventions:
NormedAddCommGroup E, NormedSpace ℝ E, CompleteSpace E. is StrongDual ℝ E with the operator norm; the pairing is x' x; is StrongDual ℝ (StrongDual ℝ E) and is NormedSpace.inclusionInDoubleDual ℝ E.EReal with the clause "never ". Properness also requires some value . Convexity is the paper's inequality for , computed in EReal.V → Set (StrongDual ℝ V). Maximality is graph inclusion, quantified over every monotone T', not only over subdifferentials.EReal supremum over all of ; the biconjugate is conj (conj f) on the bidual.EReal subtraction.WeakDual ℝ E.atTop. Weak** convergence is pointwise convergence on of the canonical images, which is convergence in the weak topology induced on by . Boundedness is a uniform norm bound.A trivializing formalization is ruled out: properness excludes (whose empty subdifferential is monotone but not maximal) and 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.
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.
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 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 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 with and for
— a positive-definite potential.
For continuous on , with a locally bounded upper Dini derivative and for a.e. with :
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 for Lipschitz (respectively linear-type and square-root-type drift bounds).
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.
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.
The central difficulty is Lemma 8.11 itself: proving that a bound on the upper Dini derivative (not the ordinary derivative) forces to decrease is genuinely subtler than the Lipschitz case, because 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), , 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 " for almost all with " implicitly presupposes 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.
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
and uniformly — reusing Mathlib
substrate rather than restating Definition 8.1's - 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.
An insurance company's surplus grows with premiums and falls with claims. In the Cramér–Lundberg model with a positive safety loading, the surplus drifts to with probability one. De Finetti (1957) objected that a company does not accumulate capital indefinitely: surplus above some level is paid out to shareholders. He proposed choosing the payout policy to maximize the expected discounted dividends paid before ruin. This is the optimal dividend problem. It is one of the basic stochastic control problems of actuarial mathematics and corporate finance, and it serves as a test case for singular control of processes with jumps.
The classical answer is a barrier strategy: pay out whatever lifts the surplus above a level and nothing else. Jeanblanc and Shiryaev (1995) proved this optimal when the surplus is a Brownian motion with drift, and Gerber and Shiu studied the same Brownian setting. Azcue and Muler (2005) showed that it can fail in the Cramér–Lundberg model, where the optimal policy may be a band strategy. Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007) 156–180) treated a general spectrally negative Lévy process, a process with stationary independent increments and only downward jumps. They found the value of every barrier strategy in closed form through the scale function of the process and identified the best barrier level . They also gave a verification condition under which the barrier at is optimal among all strategies. Loeffen (2008) later showed that the condition holds whenever the Lévy measure has a completely monotone density.
Let be a spectrally negative Lévy process on a filtered probability space with and Lévy triplet . Its Laplace exponent is , finite for :
Increments after time are independent of . Initial capital is added to . The standing assumptions are the following: does not have monotone paths, , and either , , or has a density.
A dividend strategy is a nondecreasing, left-continuous, adapted process with . The risk process is and the ruin time is . The strategy is admissible () if no lump sum exceeds the current reserves. Its value is
with discount rate . For , consists of the admissible strategies that keep for .
The -scale function is the unique continuous nondecreasing function on with for large . It is extended by on . The barrier strategy reflects at the level , paying at time . The paper computes its value
and the optimal barrier level is , read as when this set is empty and for all . The generator is
Assume , or has bounded variation, or . Then and:
The goal fixes no constants: the barrier level and the value function are both given by the scale function of the given process.
The theorem gives an explicit solution to a singular control problem for a general Lévy model. The candidate value function and barrier level are expressed through one special function, , and optimality over all strategies reduces to one inequality on . It is the basis of the later literature on scale-function methods in dividend problems (Loeffen 2008, Kyprianou–Rivero–Song 2010, and the refracted and Parisian variants). Part (i) holds with no condition on the Lévy measure. Part (ii) shows exactly where barrier optimality can fail.
The paper's proofs use fluctuation identities (exit problems, excursion theory) and Itô's formula for semimartingales with jumps. None of these is in Mathlib. As far as is known, none of these results has been machine-checked. A formalization would produce a Lévy-process and scale-function layer, a formal model of singular control with jumps and lump-sum payments, and a checked verification argument. Each of these can be reused beyond this paper.
The analytic part is elementary once the value formula (5.1) is available: the choice of , Proposition 3(i) and Lemma 3(i) follow from the shape of . The difficulty lies in the two probabilistic steps. Proposition 1 identifies the value of a reflected process through exit identities for . Those identities rest on excursion theory, or on the martingale property of up to exit. The verification step, Proposition 4(i), needs Itô's formula for . Here is a jump process controlled by a left-continuous finite-variation process that may itself jump. The change-of-variables formula must also run under only regularity when has bounded variation. Just proving that and imply a supermartingale inequality does not settle the question: the lump-sum payments and the jumps of enter the Itô expansion separately and must each be bounded.
Time is (ℝ≥0). is a structure carrying the triplet and pathwise càdlàg paths with only downward jumps. It also carries independence of increments from the filtration and stationarity. Its law is fixed by the Laplace transform for . The standing assumptions of §2 and (3.3) are bundled as one predicate. The scale function is a hypothesis on a function argument (it is unique). is an extended real, since it is for unbounded variation without a Gaussian part.
Values of strategies and value functions lie in . The dividend integral is a Lebesgue–Stieltjes integral over : it counts the lump sum at time and excludes a payment at the ruin instant.
Several conventions are fixed, and each is disclosed in the item it affects:
A trivializing encoding is ruled out: the value is not a real supremum, the barrier strategy is constructed rather than assumed, and is a conclusion.
A complete development needs:
The Lévy and scale-function layer is shared with the companion mission on the bail-out problem. Contributions of general lemmas (Stieltjes integration by parts, optional stopping for càdlàg martingales) are welcome.
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 policy is optimal in every period of a finite-horizon problem: order up to when the stock falls below , 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:
The ordering cost is concave, nondecreasing, and . For , is the supporting line of at with the smallest intercept, written as a pair (slope, intercept) . The set of slopes that occur is , and is the intercept belonging to slope , so for . The limits and are assumed to exist.
Demands in successive periods are i.i.d. with density . A function is if and for all and increasing , ; it is a one-sided Pólya density if it is for every , integrates to and vanishes on . Exponential and Erlang densities are examples.
With holding-and-shortage cost (PF-integrable, bounded below), terminal cost , discount factor , and convolution , the value functions are
where counts the periods remaining. is the set of minimizers . A generalized policy is a function with for and for : no order above , and below an order-up-to level that is at least and does not increase with the starting stock.
Two function classes carry the argument. is non--decreasing on if for in . For , consists of the piecewise continuous, PF-integrable functions with as that are nonincreasing on or and non--decreasing on the rest of the line. is its continuous part. With , the assumptions A1–A5 of §VI tie and to , and the .
Under the standing assumptions and A1–A5, for every the convolution exists and
The statement fixes no numbers: and depend on and on the data.
The result extends -type structure from setup-plus-linear to arbitrary concave increasing ordering costs, which covers quantity discounts and multi-facility production. When is piecewise linear with pieces, the optimal policy is an policy described by at most reorder points and order-up-to levels. That is a finite-dimensional family, which makes computing policies tractable. The class and its closure under Pólya convolution (Theorem 1) are statements about functions of one real variable, independent of the inventory model. Quasi--convexity extends both -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 -convex lemma (BertsekasDP.kconvex_sS_structure, a result about -convex rather than functions), but no Pólya frequency functions, no quasi--convexity, and no concave-cost inventory model.
The obvious route copies Scarf: show that the cost-to-go is -convex and that -convexity survives taking expectations. With a concave ordering cost there is no single , and the relevant functions are generally not -convex. The weaker property that does hold, membership in , 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 into one policy (Theorem 2). Separate pairs for each do not by themselves give a monotone policy.
All functions are ℝ → ℝ; the ordering cost is used only on . The demand density is a function, not a measure; convolution is the Lebesgue integral over . uses Matrix.det over Fin k. The value functions are defined by structural recursion on with the terminal cost; is used for . is defined by the optimality inequality, never through the infimum. is defined by the paper's identity (7), . is open, and "increasing" is read as nondecreasing. Slopes in are written to separate them from the cost function .
Added hypotheses and conventions:
Lean returns for an infimum over a set unbounded below and for the integral of a non-integrable function. The goal therefore concludes that exists and that 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 . Everything is built from the data . The class 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 ), Leibniz-rule lemmas for exponential kernels, the theory of and quasi--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.
Many problems in signal processing, statistics and operations research ask to minimize a sum of a nonsmooth convex term (a constraint indicator, an penalty) and a smooth term . The standard method is the forward-backward (proximal-gradient) algorithm: an explicit gradient step on followed by a proximal step on . Its classical convergence theory requires to be convex and the step size to stay below , where is the Lipschitz constant of .
Attouch, Peypouquet and Redont (authors' manuscript of SIAM J. Optim. 24 (2014)) derive an inertial forward-backward algorithm (IFB) as a time discretization of a second-order dissipative dynamical system with Hessian-driven damping. The added inertial terms cost essentially nothing to compute, yet they allow step sizes beyond and a smooth part that is not convex, provided the sum is.
Timeline of the relevant results:
Let be a real Hilbert space with inner product . Let and , and write and . A vector is a subgradient of at , written , if and for all .
Hypothesis H fixes positive constants , , and a step size with:
Algorithm (IFB). From any , compute for
A sequence converges weakly to , written , if for every . The analysis uses the velocity , the energy with , and two auxiliary real sequences and , defined from , and a reference point by (17) and (18) of the paper.
Under Hypothesis H, for every sequence generated by (IFB),
if and one of (i) is a singleton, (ii) is differentiable with weak-to-weak sequentially continuous gradient, (iii) is weak-to-weak sequentially continuous, (iv) is convex, holds, then
and if , then .
In the order of the paper's argument: Proposition 2 (energy decrease, ); Proposition 3 (the identity and inequality (19) for ); Proposition 4 ( is bounded above for ); the lower bound (28) on ; Lemma 5 (a real-sequence lemma); Proposition 6 (, weak cluster points lie in ); Lemma 7 (a boundedness lemma); Proposition 8 (boundedness of and convergence of when ).
The result gives convergence of a forward-backward type method under a step-size bound that can be made arbitrarily large by choosing small, and for a smooth term that need not be convex. The special case (indicator of a closed convex set) yields an inertial gradient-projection method, and the paper applies the theorem to feasibility problems, the CQ algorithm, Pareto fronts and signal recovery.
The theorem is proved in the paper; to our knowledge it is not formalized anywhere. A complete formalization would provide a machine-checked Liapunov analysis of an inertial proximal method in an infinite-dimensional Hilbert space, including the passage from a minimizing sequence to weak convergence. The milestones Proposition 2, 3 and 8 are energy estimates that also underlie other inertial and proximal schemes.
The energy controls the values and the velocities , but not the iterates themselves. The first idea, proving that is nonincreasing for every (Fejér monotonicity, the standard route for the classical forward-backward method), does not come out of the energy estimates for (IFB): the inertial variable couples consecutive steps, and the distance to a minimizer is not a Liapunov function. The paper's replacement, the sequence , carries the auxiliary sum , whose upper bound already requires the full Hypothesis H. Because is infinite-dimensional, bounded sequences have only weakly convergent subsequences, so the minimizing property has to pass through weak lower semicontinuity of , and the final step, uniqueness of the weak cluster point, needs a separate argument in each of the cases (i)–(iv) together with Opial's lemma, which is not in Mathlib.
InnerProductSpace ℝ H with CompleteSpace H); nothing is specialized to finite dimension.EReal. Properness excludes . Convexity of an extended-valued function is convexity of its epigraph in , because Mathlib's ConvexOn needs a scalar action that EReal lacks. The subgradient predicate requires , so off .lam.EReal.toReal ⊤ = 0.A complete development needs Opial's lemma, weak sequential compactness of bounded sets in Hilbert space, weak lower semicontinuity of lower semicontinuous convex functions, the descent lemma for functions with Lipschitz gradient, and monotonicity of the subdifferential. These are reusable well beyond this mission; contributions of any of them, and of the milestones in any order, are welcome.
Sorting a collection of strings in lexicographic order is a basic subroutine in compilers, string indexing, suffix sorting and the construction of tries. The classical method, due to Aho, Hopcroft and Ullman (The Design and Analysis of Computer Algorithms, 1974), is a multipass radix sort that processes the strings from the last position to the first and runs in time proportional to the total length of the input plus the alphabet size . Mehlhorn showed that a straightforward first-to-last scan of equal-length strings needs time.
Paige and Tarjan (Three Partition Refinement Algorithms, SIAM J. Comput. 16(6):973–989, 1987, doi:10.1137/0216062) observed that most of the input is usually irrelevant to the sorted order: only the shortest prefix of each string that tells it apart from the others matters. Their algorithm separates the problem into two steps: (1) find this distinguishing prefix of every string, and (2) sort the distinguishing prefixes. The first step is carried out by partition refinement, the same technique that the paper then applies to the relational coarsest partition problem (the second mission of this series) and to double lexical ordering. This mission formalizes the correctness and the termination bound of the first step.
Fix and the alphabet , together with an end marker that is smaller than every symbol. A string is a finite sequence over ; is the empty string, is the length of , and is its -th symbol (positions start at ). A string is a prefix of if for some string ; every string is a prefix of itself. is the set of strings over followed by one .
The input is a multiset with ; repeated strings are allowed. The distinguishing prefix of in is
Write .
For a string , the labeled block is the multiset of strings of having as a prefix, and is its associated prefix. The block is finished if for some , and unfinished otherwise. A state is a set of labeled blocks. For an unfinished block ,
The refinement algorithm starts from and repeatedly applies the step Refine: pick any unfinished block and replace by . A run with steps is a sequence produced this way; any choice of unfinished block is allowed at every step.
For every run of the refinement algorithm,
The paper states Theorem 1 as "The algorithm terminates and is correct"; the bound is the explicit count proved in the last sentence of its proof (p. 975). The goal leaves the choice of unfinished block free, so it holds for every refinement order.
A supplementary item states the fact on p. 974 that motivates the two-step design: distinct strings have distinct distinguishing prefixes, and iff in lexicographic order.
Theorem 1 is the correctness half of the lexicographic sorting algorithm: once the distinguishing prefixes are known, sorting reduces to sorting strings of total length , which is how the paper obtains its time bound in place of . The paper notes that under a natural probability model is of order , so the gain is large whenever the strings are long. The invariant of Lemma 1 is also the pattern on which the later partition refinement algorithms of the paper are built: a target partition is shown to refine every intermediate partition, and a potential function bounds the number of refinement steps.
The result has been proved since 1987. What this mission adds is a machine-checked account of the algorithm at the level of its abstract refinement steps, with the explicit bound rather than an asymptotic statement, and with the standing assumptions of §2 (non-empty input, end markers) made explicit. No formal proof of this algorithm is present in Mathlib or on the platform.
The obvious argument, "each step makes the labels longer, and labels never grow past the distinguishing prefixes", needs two facts that are not immediate from the definitions. First, the labels of a reached state must form a partition of into non-empty blocks whose labels are pairwise incomparable under the prefix order; this is an invariant of the algorithm, not part of the definition of a state, and it fails for arbitrary sets of labels. Second, the label of an unfinished block must be a proper prefix of every finished label below it, which rests on the end marker: without end markers a string can be a proper prefix of another, a block can be unfinished yet have no strictly longer children, and the algorithm can stall. Bounding the sum of label lengths by is not a label-by-label comparison: a state can have fewer labels than strings, and the distinguishing prefixes of different strings can share a label as a common prefix.
Strings are List (Fin (k + 1)), with 0 : Fin (k + 1) the end marker and prefix the Mathlib relation <+:. The multiset is a family x : Fin n → List (Fin (k + 1)), so repetitions are distinct indices. The hypotheses 0 < n and EndMarked x () are the paper's standing assumptions. A block is identified by its label, not by its set of members: two different labels can carry the same strings (for instance when every string begins with ), and they are different blocks. A state is a Finset of labels; a run is a map Fin (K + 1) → Finset (List (Fin (k + 1))) starting at {[]}. Positions are 1-based in the paper and 0-based in Lean, so is (x i)[α.length]?. The distinguishing prefix follows the literal definition; for it is the empty string.
The running times and space, the implementation with a queue and a global index, and step two (sorting the prefixes via the refinement tree) are RAM-model statements and are not formalized. Only the explicit step count is. A formalization in which split added all children, added none, or allowed refining a finished block would change the theorem (the bound fails or the goal becomes vacuous); the definitions add exactly the children realized by some string of the block and refine only unfinished blocks.
Contributions welcome: proofs of the milestones, a general API for prefix-closed partition refinement on List, and a proof of the order-preservation item via Mathlib's List.Lex.
A stochastic processing network (SPN) — buffers holding waiting work, activities that consume items from buffers and produce items into others, driven by stochastic arrivals and service requirements — is stable, in the sense of mission I's Definition 3.6, exactly when its ambient Markov chain is positive recurrent. That definition is correct, but it is a statement about an infinite-state continuous-time Markov chain, and Markov chains of that kind almost never admit a hand-computed stationary distribution or a directly verifiable positive-recurrence criterion for anything beyond the smallest examples. What is needed is a method that turns "is this specific queueing network, under this specific control policy, stable?" into a tractable, purely deterministic question. 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) supplies exactly this method in Chapter 6, and the theorem that licenses it — Theorem 6.2 — is introduced by the authors themselves as "the fulcrum that supports all other results developed in this book." Every stability theorem in the remaining eight chapters of the book (feedforward and generalized Jackson networks, the Rybko–Stolyar boundary, back-pressure control, proportionally fair allocation, task allocation, packet networks) is an application of this one theorem to a model-specific fluid model.
The method traces to Rybko and Stolyar's 1992 study of a single two-station network and to J. G. Dai's 1995 unification of fluid-limit stability arguments across general queueing networks (Annals of Applied Probability 5, 49–77), with independent contemporaneous work by A. Stolyar for discrete state spaces and a parallel probabilistic route through reflecting Brownian motion due to Dupuis and Williams (1994). This mission formalizes the version of the argument specific to Dai and Harrison's general SPN framework.
Under a fixed control policy, an SPN with buffers and activities generates four
continuous-time processes: the cumulative departure process , the
cumulative service-completion process , the cumulative service-effort
process , and the buffer-contents process . The
model's first-order data — the material-requirement matrix , the
expected-output matrix , the vector of mean service times, the
capacity-consumption matrix , the -vector of server-pool capacities, and the vector
of external arrival rates — determine six basic relationships that Chapter 2 derives
directly from the SPN's construction, and that this mission packages as IsFluidModelSolution.
To study scaling limits, Section 6.3 constructs, on one common probability space, a whole family of versions of the SPN's processes, one for each initial state of the ambient chain: the superscripted . Writing for the total initial buffer content, the fluid-scaled processes are
A fluid limit path (Definition 6.6) is any limit of such a family, along a sequence of initial states with , uniform on compact time intervals (u.o.c.). A fluid model solution is any four-tuple satisfying the six equations above, whether or not it arises as an actual limit — a purely deterministic notion.
where "fluid limit... is stable" (Definition 6.1) means: there is such that every fluid limit path has for all . This is the weakest possible target: it asserts only that fluid limit paths are eventually driven to zero, with no rate or further structure attached, and it is exactly the hypothesis every later chapter's Lyapunov argument is built to establish.
Theorem 6.5 (existence of fluid limits): along any sequence of initial states with , the fluid-scaled processes have a u.o.c.-convergent subsequence, and every such limit is automatically a fluid model solution — the bridge from the purely equational Definition 6.3 (used by every later chapter) to the genuinely stochastic Definition 6.1 (needed by this theorem). Its proof rests on two convergence lemmas (6.7: compactness of the scaled service-effort process via an equicontinuity argument; 6.8: the scaled completion process converges exactly when the scaled effort process does) and, behind Lemma 6.8, a uniform strong law of large numbers for a "delayed" random walk (Lemma 6.9). A separate uniform-integrability result (Lemma 6.10) supplies the remaining ingredient the goal theorem's proof needs to convert an almost-sure fluid-scale limit into the expectation bound mission I's Lemma 3.7 requires.
The result itself. Theorem 6.2 converts a probabilistic stability question about an infinite-state Markov chain into a real-analysis question about a deterministic dynamical system: does every solution of a fixed, checkable system of equations reach zero in finite time, uniformly in its starting size? Every one of the book's remaining eight chapters answers a version of this question for a specific policy and concludes SPN stability via this theorem alone — none of them re-derives positive recurrence directly.
Formalizing it. No prior formalization of fluid limits, fluid models, or scaling-limit
stability of any stochastic system exists on Prove2Me (q=fluid limit, q=fluid model, q=u.o.c. convergence, q=queueing network stability all return zero hits). This mission is a from-scratch
formalization of the model data, the fluid equations, the per-state process family, and the two
notions of fluid stability, together with the five supporting results and the goal theorem that
connects them — the shared infrastructure the rest of the fourteen-mission series depends on.
The obvious shortcut — state Theorem 6.2 using fluid model stability (Definition 6.3, the purely equational notion) in place of fluid limit stability (Definition 6.1) — would produce a strictly easier, unfaithful theorem: fluid model solutions are not restricted to arise as actual scaling limits, so the genuine content of Theorem 6.2 (that convergence of a stochastic family forces a probabilistic conclusion) would be lost, and the theorem would reduce to a tautology once Theorem 6.5 is assumed. The two notions are visually almost identical in the book's own text ("-attraction to the origin," applied to two different objects) and keeping them distinct is this mission's central discipline. A second difficulty is that Mathlib has no existing theory of stochastic-process scaling limits, u.o.c. convergence, or the specific renewal/SLLN machinery (Lemma 6.9's uniform strong law for a state-dependent "delayed" random walk) the proof needs — every one of these had to be defined from the ground up rather than instantiated from a general framework.
The ambient chain's state space is an arbitrary countable type, following mission 01; the
per-state process family SPNProcessFamily takes as given real-valued
functions satisfying exactly the pathwise properties (Eqs. 2.31–2.32) that Section 6.4's proofs
use, since Chapter 2's construction of these processes from primitive stochastic elements is that
chapter's own "recap" of already-established facts, not a numbered result of Chapter 6.
UOCConverges is stated by its direct --on-every-compact-interval meaning, and
Lemma 6.9's "" is likewise stated by its direct - meaning rather than a
Lean supremum expression, because the state space may be countably infinite and an explicit
supremum over an unbounded-above family of reals would silently collapse to a junk value of zero
in that case — a real risk of trivializing the statement that this formalization avoids outright.
A formalization that reused FluidModelStable as the goal theorem's hypothesis, or that dropped
from Theorem 6.5, would each be a trivializing shortcut of exactly the kind ruled
out above. The five definitions (FluidEquationData, IsFluidModelSolution, SPNProcessFamily,
FluidLimitPath, FluidLimitStable) are the primary reusable contribution — the shared
vocabulary every later mission in the series restates in its own namespace, since drafts do not
import one another. Contributions completing the six by sorry proofs are welcome.
An expander is a sparse graph in which every set of vertices has many neighbours outside itself. Expanders are the building blocks of superconcentrators (sparse directed graphs that route any inputs to any outputs along vertex-disjoint paths), of sorting and switching networks, and of many constructions in complexity theory and coding; the survey of Hoory, Linial and Wigderson (Bull. AMS 2006) describes these uses. Random regular graphs are expanders with high probability, but applications need explicit families with fixed degree and a uniform expansion constant.
Alon and Milman (J. Combin. Theory Ser. B 38 (1985)) replace combinatorial expansion by a spectral quantity, the second-smallest eigenvalue of the matrix of a graph, which Fiedler called the algebraic connectivity (Czech. Math. J. 1973). Their Theorem 4.3 shows that a regular graph with bounded away from yields an expander. This mission formalizes their Section 4 source of such graphs: Cayley graphs of the finite quotients of a group with Kazhdan's property (T).
Timeline:
Let be a finite group. A finite multigraph on is a symmetric matrix of nonnegative integers, being the number of edges joining and (diagonal entries count loops). It is -regular if every row sums to . Its matrix is with , a real symmetric positive semidefinite matrix. Its eigenvalues, repeated according to multiplicity, are , and denotes the second of them.
Let be a group, a finite set with , and a homomorphism onto . The Cayley multigraph joins and by as many edges as there are with . It is -regular, and its matrix is , where is the permutation matrix of the left regular representation, iff .
An -enlarger (Definition 4.1) is a -regular graph on vertices with .
A unitary representation of in a complex Hilbert space is essentially nontrivial (Definition 4.5) if no nonzero vector is fixed by every . A discrete group has property (T) (Definition 4.6) if there are and a finite such that for every essentially nontrivial unitary representation and every unit vector some satisfies .
Let have property (T), let be a finite generating set of with , and let be surjective homomorphisms onto finite groups with . Then there is one with
The constant is unspecified: the theorem asserts uniformity in , not a value.
Theorem 4.9 turns an analytic property of one infinite group into a uniform spectral bound for infinitely many finite graphs of fixed degree. With Theorem 4.3 of the paper it produces explicit families of linear expanders, hence of linear superconcentrators; for , , and its reductions modulo the paper obtains infinitely many explicit families of -enlargers. The same mechanism underlies later work on expanders from groups, surveyed in Lubotzky's monograph (Birkhäuser 1994).
The result is proved in the paper, modulo Lemma 4.7, which the paper refers to Margulis for. The formalization adds a checked account of every step, including Lemma 4.7 itself. At the pinned Mathlib revision there is no notion of property (T), of Kazhdan constants, or of the algebraic connectivity of a multigraph, and no machine-checked version of Theorem 4.9 is known on this platform.
The combinatorial and linear-algebra steps are routine; the substance is in two places. First, Lemma 4.7: Definition 4.6 supplies a constant for one finite set , nothing in the definition relates to a given generating set , the paper gives no proof, and the standard references state the textbook form rather than the paper's absolute-value form . Second, the uniformity: a spectral gap for each fixed quotient is easy, since a connected graph has , but a bound that does not decay as is exactly what cannot come from any finite computation and must come from property (T) through Lemma 4.8. The Rayleigh quotient of milestone 3 is taken over real vectors, while Lemma 4.7 is stated for complex Hilbert spaces.
Groups are Lean types with a Group instance; the finite groups carry Fintype and DecidableEq. Graphs are multigraphs given by symmetric matrices Matrix T T ℕ, with loops allowed. This matters: when identifies two generators or sends one to the identity, the degree is still , and a loop contributes to . Mathlib's SimpleGraph Cayley graph forgets these multiplicities and is not used. is the second-smallest eigenvalue with multiplicity of the real symmetric matrix (via Matrix.IsHermitian.eigenvalues₀). It is defined spectrally, as in the paper, and not as a Rayleigh minimum. It is only meaningful for , and the goal excludes trivial quotients explicitly. Unitary representations are homomorphisms into the unitary group of bounded operators on a complex Hilbert space in universe Type. Compact subsets of a discrete group are finite sets.
A trivializing formalization is ruled out. Property (T) is not replaced by the hypothesis that the regular representations of the quotients have no almost-invariant vectors, which would make Theorem 4.9 a restatement of its hypothesis. And is not defined as the minimum of over zero-sum unit vectors, which would make milestone 3 true by definition.
A complete development needs basic Kazhdan-constant manipulations, Courant–Fischer for real symmetric matrices, and the regular representation of a finite group as a unitary representation. The regularity of Cayley multigraphs and the identity are short. The spectral and representation-theoretic lemmas are reusable beyond this mission. Contributions of intermediate lemmas, such as the variational characterization of eigenvalues₀ or the invariance of the zero-sum subspace, are welcome.
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.
Let and let be the probability simplex. For the Kullback–Leibler divergence is
with . Fix a nominal distribution with for every , and a level . The entropy uncertainty set is
For a vector (in the MDP, the value function of the next stage), the inner problem (17) is
The paper's scalar dual function (47) is, for ,
Write and , the -mass of the maximisers of . The tilted distribution at is .
In Lean, vectors are Fin n → ℝ, is stdSimplex ℝ (Fin n), and , , , , , are klDiv, klBall, dualFn, tiltedDist, vmax, maxMass in the namespace RobustMDP.EntropyInner.
with the maximum attained. This is kl_ball_inner_problem_dual. It holds for every , every , every in and every .
The goal turns an -dimensional optimisation over a nonpolyhedral convex set into a one-dimensional convex minimisation whose objective costs to evaluate. Combined with the bisection bracket from (48) and the behaviour at from (49), it gives the paper's 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 .
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.
The inequality for every 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 only for ; at it is , and the dual infimum may be approached only as . A proof that looks for a minimiser and a matching primal point fails in precisely the regime of milestone 7, where no such exists and the primal optimum sits on the face of the simplex spanned by the maximisers of . The strong-duality argument must also handle the boundary of , where is not differentiable.
Fin n → ℝ; is stdSimplex ℝ (Fin n). is a local finite sum with Lean's , which gives ; Mathlib's measure-valued InformationTheory.klDiv is not used.IsGreatest (attained, since the KL ball is compact). The paper's "" is an infimum, stated with IsGLB over : it is not attained when .dualFn is total in and equals at (division by zero), not the paper's . Every statement uses ; the value at appears as the one-sided limit of (49). Accordingly (48) is stated for .⨆ j, v j, the attained maximum over the finite nonempty index set; likewise.𝓝[>] 0 together with a little-o remainder; (50) as a limit along atTop.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 remainder of Appendix C are all welcome.
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 , 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."
An SPN has buffers, indexed by , and activities, indexed by . Its first-order data — the quantities that matter for a capacity calculation, as opposed to full stochastic detail — are: the material requirement matrix ( = number of class- items one type- service consumes), the mean output matrix (its th column is the expected output vector of a type- service), the mean service times , the capacity consumption matrix (server pool against activity ), and the server-pool capacities . From these,
so that is the long-run average rate at which activity depletes buffer 's content.
Given an arrival-rate vector , the static planning problem (SPP) is the linear program
whose decision variable is a long-run average activity rate and whose objective upper-bounds every server pool's utilization. The network is subcritical at if , and the subcritical region is .
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.
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.
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 ), 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).
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 , show it is stable throughout the subcritical region, and conclude maximal stability — without having to separately characterize the true stability region , 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 tied to a network's material-balance matrix and capacity matrix — 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.
The natural first attempt states Theorem 5.2 as a claim about the buffer-contents process
directly. This fails to separate cleanly from the proof, because the actual argument passes
through an auxiliary quantity — the stationary mean under the chain's
(unique, by stability) stationary distribution — that has no meaning outside a specific
proof strategy. The formalization instead states the goal purely in terms of the data and the hypothesis of stability, exactly as the book's own statement does, leaving '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.
Buffers and activities are Fin I, Fin J; matrices are Matrix over ℝ. The subcritical
region is defined via the optimal SPP value , formalized with Mathlib's IsLeast
(attained infimum, matching the book's own " iff 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 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 (Eq. 2.11) and the
material-requirement matrix — 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 replaced by an unconstrained existential (dropping the LP structure entirely) would
trivialize the chapter's actual content — the LP-feasibility characterization is what makes
checkable, and is preserved here in full.