The OR Formalization Drive

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Dual Stochastic Dominance and Related Mean-Risk Models 1: Second-Degree Stochastic Dominance Is Dominance of Absolute Lorenz CurvesResearch Paper

Motivation

Comparing uncertain outcomes is the basic problem of decision making under risk. Second-degree stochastic dominance (SSD) is the comparison that every risk-averse decision maker who prefers larger outcomes agrees with: $X$ dominates $Y$ in this sense exactly when $\mathbb E\,U(X)\ge\mathbb E\,U(Y)$ for every nondecreasing concave utility $U$ for which the expectations are finite. The relation grew out of majorization theory for finite distributions (Hardy, Littlewood and Pólya) and was extended to general distributions by Rothschild and Stiglitz and by Hadar and Russell around 1970; it is the standard consistency requirement for portfolio models and for risk measures in operations research and finance.

SSD is defined through the distribution function, which is awkward in optimization: portfolio returns are linear in the decision variables, but their distribution functions are not. Ogryczak and Ruszczyński (SIAM J. Optim. 13 (2002) 60–78) showed that SSD has an equivalent dual description through the integrated quantile function, the absolute Lorenz curve, and that the two descriptions are related by Fenchel conjugation. That dual description underlies the later theory of SSD-constrained optimization (Dentcheva and Ruszczyński, SIAM J. Optim. 14 (2003)) and the use of conditional value-at-risk as an SSD-consistent risk measure.

Setting

Fix a probability space $(\Omega,\mathcal B,\mathbb P)$ and real random variables $X,Y:\Omega\to\mathbb R$ with $\mathbb E|X|<\infty$ , $\mathbb E|Y|<\infty$ .

The distribution function is $F_X(\eta)=\mathbb P\{X\le\eta\}$ (Lean: distFun P X).
The second performance function is the area below it, $F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}F_X(\xi)\,d\xi$ (secondPerformance P X, eq. (2.1)).
SSD: $X\succeq_{SSD}Y$ iff $F_X^{(2)}(\eta)\le F_Y^{(2)}(\eta)$ for every $\eta\in\mathbb R$ (SSD P X Y, eq. (2.2)). The dominating variable has the smaller curve.
The first quantile function is the left-continuous inverse $F_X^{(-1)}(p)=\inf\{\eta:F_X(\eta)\ge p\}$ , $0<p\le1$ (leftQuantile P X). A number $q$ is a $p$ -quantile if $\mathbb P\{X<q\}\le p\le\mathbb P\{X\le q\}$ (IsPQuantile P X p q).
The second quantile function (absolute Lorenz curve) $F_X^{(-2)}:\mathbb R\to\overline{\mathbb R}$ is $F_X^{(-2)}(p)=\int_0^pF_X^{(-1)}(\alpha)\,d\alpha$ for $0\le p\le1$ and $+\infty$ otherwise (secondQuantile P X, eq. (3.2)).
The convex conjugate of $F:\mathbb R\to\overline{\mathbb R}$ is $F^*(p)=\sup_\xi\{p\xi-F(\xi)\}$ (conj F), and $\partial f(\eta)$ is the subdifferential of a real function $f$ at $\eta$ (subdiff f η).

Formalization targets

Goal: Theorem 3.2

X\succeq_{SSD}Y\iff F_X^{(-2)}(p)\ge F_Y^{(-2)}(p)\quad\text{for all }0\le p\le1.

Both directions are required, and the range of $p$ includes both endpoints (at $p=1$ the right-hand side contains $\mathbb EX\ge\mathbb EY$ ).

Milestones, in the order the argument uses them

(2.4): $F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}(\eta-\xi)\,P_X(d\xi)=\mathbb E\max(\eta-X,0)$ .
§2, p. 62: $F_X^{(2)}$ is continuous, convex, nonnegative and nondecreasing.
§3, p. 64: for $p\in(0,1)$ the $p$ -quantiles form a closed interval with left end $F_X^{(-1)}(p)$ .
(3.3): $\partial F_X^{(2)}(\eta)=[\mathbb P\{X<\eta\},\mathbb P\{X\le\eta\}]$ for every $\eta$ .
Theorem 3.1(i): $F_X^{(-2)}=[F_X^{(2)}]^*$ on all of $\mathbb R$ .
Theorem 3.1(ii): $F_X^{(2)}=[F_X^{(-2)}]^*$ on all of $\mathbb R$ .

A companion item, Corollary 3.3, states the four equivalent characterizations of a $p$ -quantile (quantile condition, attainment in either conjugate, and the Fenchel–Young equality $F_X^{(-2)}(p)+F_X^{(2)}(\eta)=p\eta$ ).

Significance

Theorem 3.2 converts a condition on distribution functions into a condition on integrated quantiles. Its consequences in the paper include the SSD consistency of the mean–risk models built on tail means (conditional value-at-risk), on the Gini mean difference and on the mean absolute deviation from a quantile, and the linear-programming representations of those models for finitely many scenarios; the companion mission Dual Stochastic Dominance and Related Mean-Risk Models 2 builds on the same objects. Theorem 3.1 is the precise statement that $F_X^{(2)}$ and $F_X^{(-2)}$ form a conjugate pair; Corollary 3.3 identifies the subgradients of each with the quantiles of $X$ .

All results here are proved in the paper, and the quantile characterization of the increasing concave order also appears in the stochastic-orders literature. None of them is formalized: Mathlib at the pinned revision has ProbabilityTheory.cdf but no convex conjugate on the extended reals, no subdifferential of a real function, no quantile function and no stochastic dominance. The mission produces a machine-checked account of the quantile side of SSD, with the conjugacy stated exactly, including the value $+\infty$ off $[0,1]$ .

Difficulty

The naive route to Theorem 3.2 compares $F_X^{(2)}$ and $F_Y^{(2)}$ through the quantile functions directly, but the first quantiles $F^{(-1)}$ need not be ordered when $X\succeq_{SSD}Y$ (the paper notes this on p. 65), so no pointwise argument on quantiles works. The equivalence rests on Theorem 3.1, and there the hard part is computing the conjugate of $F_X^{(2)}$ for a general distribution: atoms of $X$ make $F_X^{(2)}$ nondifferentiable and flat pieces of $F_X$ make the maximizer non-unique, so the subdifferential (3.3) and the interval of $p$ -quantiles must be handled as sets, and the endpoints $p=0,1$ (where the supremum need not be attained) and $p\notin[0,1]$ (where it is $+\infty$ ) must be treated separately. Part (ii) is a biconjugation statement for a closed convex function, whose general form is not in Mathlib.

Formalization scope

One probability space (Ω, P) with [IsProbabilityMeasure P] carries both $X$ and $Y$ ; nothing depends on anything but the laws, and no independence is assumed.
$F_X(\eta)$ is P.real {ω | X ω ≤ η}; $F_X^{(2)}$ is a Bochner integral over Set.Iic η; $F_X^{(-2)}$ is an interval integral over $(0,p]$ , placed in EReal, with ⊤ off $[0,1]$ .
The conjugate is ⨆ ξ, ((p * ξ : ℝ) : EReal) - F ξ in the complete lattice EReal, so terms where $F=+\infty$ contribute $-\infty$ , exactly the paper's convention.
Standing assumption. Every item using $F^{(2)}$ or $F^{(-2)}$ assumes Integrable X P (and Integrable Y P in the goal). This is the paper's own hypothesis $\mathbb E|X|<\infty$ (p. 65, and the hypothesis of Theorem 3.1), not a repair. The $p$ -quantile milestone assumes only AEMeasurable X P.
Quantile at $p=1$ . $F_X^{(-1)}$ is a real sInf. It is the true infimum for $0<p<1$ ; at $p=1$ the paper's value can be $+\infty$ while sInf ∅ = 0. This one point does not affect (3.2), and no item states anything about $F_X^{(-1)}(1)$ .
Omitted. The conditional-expectation form $\mathbb P\{X\le\eta\}\,\mathbb E\{\eta-X\mid X\le\eta\}$ in (2.4) is not stated, since it is undefined when $\mathbb P\{X\le\eta\}=0$ .
Trivializing encodings are ruled out. $F^{(2)}$ is defined by (2.1), not as $\mathbb E\max(\eta-X,0)$ , and $F^{(-2)}$ by (3.2), not as a conjugate; either shortcut would make a milestone or Theorem 3.1 true by definition.
Infrastructure and reuse. Welcome contributions: the extended-real conjugate and Fenchel–Young inequality on $\mathbb R$ , biconjugation of closed convex functions of one variable, subdifferentials of integrals of monotone functions, and the basic theory of left quantiles (the quantile transform $F_X^{(-1)}(U)\sim X$ ). These are reusable beyond this mission, in particular by mission 2 of this series and by any formalization of conditional value-at-risk. The platform's VectorSpaceOpt.fenchel_biconjugate_on and ConvexOptimization.fenchelConjugate concern real-valued conjugates on other spaces and are related but not reused.

Selected references

W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM J. Optim. 13(1) (2002) 60–78. https://doi.org/10.1137/S1052623400375075
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Theorems 12.2 and 23.5 are used in the paper's proofs). https://doi.org/10.1515/9781400873173
M. Rothschild, J. E. Stiglitz, Increasing risk: I. A definition, J. Econom. Theory 2 (1970) 225–243. https://doi.org/10.1016/0022-0531(70)90038-4
J. Hadar, W. R. Russell, Rules for ordering uncertain prospects, Amer. Econom. Rev. 59 (1969) 25–34. https://www.jstor.org/stable/1811090
D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14(2) (2003) 548–566. https://doi.org/10.1137/S1052623402420528
M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Convex Optimization Operations Research+1·Captain: mikedeng1

Existence of an Equilibrium for a Competitive Economy I: Equilibrium Exists When Every Consumer Can Trade Every GoodResearch Paper

Motivation

Walras (1874) described an economy as a system of simultaneous equations, one per market, and argued that a set of prices clearing all markets exists because the number of equations equals the number of unknowns. Counting equations proves nothing, and the question of whether competitive equilibrium exists at all remained open for eighty years. Wald (1935–36) proved existence in special production models under restrictive assumptions on demand. In 1954 Kenneth Arrow and Gérard Debreu gave the first existence proof for a general model with production, many consumers, convex technologies and preferences given by utility indicators (Econometrica 22 (1954) 265–290); McKenzie published an independent proof for a trade model in the same year (Econometrica 22 (1954) 147–161). The resulting Arrow–Debreu model is the reference model of general equilibrium theory and the starting point of market-equilibrium problems in operations research and algorithmic game theory.

The paper proves two existence theorems. This mission is the first, Theorem I, whose key assumption is that every consumer initially holds a positive amount of every commodity. A second mission treats Theorem II, which replaces that assumption by a weaker condition on labour supply.

Setting

There are $l \ge 1$ commodities; a commodity vector is an element of $\mathbb R^l$ , compared componentwise ( $x \geqq y$ means $x_h \ge y_h$ for all $h$ ; $x > y$ means $x_h > y_h$ for all $h$ ). The inner product is $p\cdot x = \sum_h p_h x_h$ .

Producers $j = 1, \dots, n$ each have a production set $Y_j \subseteq \mathbb R^l$ (outputs positive, inputs negative). The aggregate production set is $Y = \sum_j Y_j$ .
Consumers $i = 1, \dots, m$ each have a consumption set $X_i \subseteq \mathbb R^l$ , a utility indicator $u_i$ on $X_i$ , initial holdings $\zeta_i \in \mathbb R^l$ , and a share $\alpha_{ij}$ of the profit of producer $j$ .

Assumptions I–IV are: (I.a) each $Y_j$ is closed, convex and contains $0$ ; (I.b) $Y \cap \Omega = \{0\}$ with $\Omega = \{x \geqq 0\}$ ; (I.c) $Y \cap (-Y) = \{0\}$ ; (II) each $X_i$ is closed, convex and bounded from below; (III.a) $u_i$ is continuous on $X_i$ ; (III.b) no $x_i \in X_i$ is a satiation point; (III.c) if $u_i(x_i) > u_i(x_i')$ and $0 < t < 1$ then $u_i[t x_i + (1-t) x_i'] > u_i(x_i')$ ; (IV.a) some $x_i \in X_i$ satisfies $x_i < \zeta_i$ ; (IV.b) $\alpha_{ij} \ge 0$ and $\sum_i \alpha_{ij} = 1$ .

A competitive equilibrium is a tuple $(x_1^*, \dots, x_m^*, y_1^*, \dots, y_n^*, p^*)$ such that

each $y_j^*$ maximizes $p^*\cdot y_j$ over $Y_j$ ;
each $x_i^*$ maximizes $u_i$ over $\{x_i \in X_i : p^*\cdot x_i \leqq p^*\cdot\zeta_i + \sum_j \alpha_{ij}\, p^*\cdot y_j^*\}$ ;
$p^* \in P = \{p \geqq 0 : \sum_h p_h = 1\}$ ;
$z^* = \sum_i x_i^* - \sum_j y_j^* - \sum_i \zeta_i$ satisfies $z^* \leqq 0$ and $p^*\cdot z^* = 0$ .

An abstract economy (§2) is a game in which each player's feasible set $A_\iota(\bar a_\iota)$ depends on the other players' actions $\bar a_\iota$ ; an equilibrium point is a profile at which every player maximizes its pay-off over its feasible set. The proof builds an abstract economy $E$ with the consumers, the producers and a fictitious market participant who chooses $p \in P$ and receives $p\cdot z$ , and a truncated version $\tilde E$ in which all choices are restricted to a large cube $C$ .

Formalization targets

Goal: Theorem I

\text{Assumptions I–IV} \implies \exists\, (x^*, y^*, p^*) \text{ satisfying Conditions 1–4.}

The statement fixes no constants; its only added hypothesis is $l \ge 1$ .

Milestones

In the order of the paper's argument:

§1.3.1: under II, III.a and III.c, each $u_i$ is quasi-concave on $X_i$ .
§1.4.2 (1): Condition 2 together with II, III.b and III.c gives $p^*\cdot x_i^* = p^*\cdot\zeta_i + \sum_j \alpha_{ij}\, p^*\cdot y_j^*$ .
Lemma 2.5: an abstract economy with compact convex action sets, continuous pay-offs that are quasi-concave in the player's own action, and continuous constraint correspondences with closed graphs and nonempty convex values has an equilibrium point.
§3.1.2 (2): at an equilibrium point of $E$ , Condition 2 holds.
§3.2: every equilibrium point of $E$ is a competitive equilibrium.
§3.3.1 (7) and §3.3.2 (2): the attainable sets $\hat Y_j$ and $\hat X_i$ (choices compatible with $z \leqq 0$ ) are bounded.
Remark §3.3.5: if $p\cdot\zeta_i > \min_{\tilde X_i} p\cdot x_i$ , the truncated budget correspondence $\tilde A_i$ is continuous at that point.
§3.4.0: for a cube $C$ containing every $\hat X_i$ and $\hat Y_j$ in its interior, $\tilde E$ has an equilibrium point.
§3.4.1: every equilibrium point of $\tilde E$ is an equilibrium point of $E$ .

Significance

Theorem I shows that the competitive model is consistent: under convexity, continuity, non-satiation and survival assumptions, prices exist at which profit maximization, utility maximization and market clearing hold simultaneously. The welfare theorems, comparative statics, and algorithms that compute equilibria (Scarf's method, market-equilibrium algorithms) presuppose it. Lemma 2.5, Debreu's social-equilibrium theorem (PNAS 38 (1952) 886–893), is also used on its own for generalized Nash equilibrium problems with coupled constraints.

The theorem is proved and textbook material (Debreu, Theory of Value, 1959). To the best of the catalog search, no proof assistant library contains Theorem I, Lemma 2.5, or a Kakutani-type fixed-point theorem for correspondences; on this platform the only related results are Brouwer's fixed-point theorem (AGT.brouwer_fixed_point, proved) and Nash's theorem for finite games (AGT.nash_existence), a special case of Lemma 2.5 with constant constraint sets. The mission produces a machine-checked proof of the paper's argument and, along the way, reusable statements about abstract economies and their equilibria.

Difficulty

The central difficulty is Lemma 2.5. The paper does not prove it but cites Debreu (1952), whose proof uses the Eilenberg–Montgomery fixed-point theorem for correspondences with contractible values. Brouwer's theorem alone does not suffice: the best-response correspondence of an abstract economy is set-valued, and its closed graph must be established from the continuity of the feasible-set correspondences, which is a maximum-theorem argument that Mathlib does not contain. A Kakutani-type fixed-point theorem, or an approximation argument reducing to Brouwer, is needed.

A second difficulty is non-compactness. The economy $E$ has unbounded action sets, so the Lemma does not apply to it directly. The boundedness of the attainable sets (§3.3.1) is an asymptotic argument using the irreversibility and no-free-production assumptions I.b and I.c, and the passage from $\tilde E$ back to $E$ (§3.4.1) needs the attainable choices to lie in the interior of the cube, so that local optimality implies global optimality through III.c. A fixed-point argument on an excess-demand function does not apply directly: demand need not be single-valued or even defined at every price.

Formalization scope

Commodity space is Fin l → ℝ with its componentwise order; the paper's strict vector inequality is written coordinatewise (∀ h, x h < ζ i h), not with the order-theoretic strict inequality on functions. Consumers are Fin m, producers Fin n, and the players of $E$ are Fin m ⊕ Fin n ⊕ Unit. Utilities are total functions, and every assumption on them quantifies over $X_i$ only. "Maximizes" is always written as membership plus an inequality against every feasible alternative, never through a supremum. Continuity of a constraint correspondence is the paper's sequential definition (§2.4), a lower-hemicontinuity condition, required at every point of the other players' action space; convergence is asked only in the other players' coordinates.

Two hypotheses are made explicit because the formal statements would otherwise be false: Theorem I and §3.4.0 assume $l \ge 1$ (for $l = 0$ the price simplex is empty), and Lemma 2.5 assumes every action set nonempty (otherwise, with two or more players and all action sets empty, every hypothesis holds vacuously). The Remark of §3.3.5 carries, as a hypothesis, the nonemptiness of $\tilde A_i$ established in §3.3.4. A formalization that makes Theorem I trivial, for instance by taking $P$ to contain $0$ , by reading IV.a with the order-theoretic strict inequality, or by allowing an empty commodity space, is ruled out by these definitions.

A complete development needs: Kakutani's fixed-point theorem (or a Brouwer-based substitute) for compact convex subsets of $\mathbb R^l$ ; Berge's maximum theorem for the best-response correspondence; the asymptotic-cone argument for §3.3.1; and elementary convex analysis for the budget sets. The abstract-economy definitions and Lemma 2.5 are reusable beyond this mission, including by the Theorem II mission. Contributions of any of these components are welcome, as are alternative proofs of Lemma 2.5.

Selected references

K. J. Arrow and G. Debreu, Existence of an Equilibrium for a Competitive Economy, Econometrica 22(3) (1954) 265–290. https://doi.org/10.2307/1907353
G. Debreu, A Social Equilibrium Existence Theorem, Proceedings of the National Academy of Sciences 38(10) (1952) 886–893. https://doi.org/10.1073/pnas.38.10.886
L. W. McKenzie, On Equilibrium in Graham's Model of World Trade and Other Competitive Systems, Econometrica 22(2) (1954) 147–161. https://doi.org/10.2307/1907539
J. Nash, Equilibrium Points in n-Person Games, Proceedings of the National Academy of Sciences 36(1) (1950) 48–49. https://doi.org/10.1073/pnas.36.1.48
S. Kakutani, A Generalization of Brouwer's Fixed Point Theorem, Duke Mathematical Journal 8(3) (1941) 457–459. https://doi.org/10.1215/S0012-7094-41-00838-4
G. Debreu, Theory of Value: An Axiomatic Analysis of Economic Equilibrium, Wiley, 1959 (Cowles Foundation Monograph 17).

16 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks IV: Fluid Equations for Non-Idling, Priority and FCFS ControlTextbook

Motivation

Mission III's Theorem 6.2 — "fluid limit stability implies SPN stability" — converts a probabilistic stability question into a real-analysis question, but it only supplies the generic fluid equations (6.1)-(6.6), which hold under any control policy and therefore say nothing policy-specific: (6.1)-(6.6) alone never force a fluid path to reach zero. To actually prove a concrete queueing network stable, one must first identify the extra fluid equation a specific policy forces on every fluid limit path, and prove that this extra equation genuinely holds — a task the book calls "justifying" the equation "through the same fluid limit procedure used in the proof of Theorem 6.5." 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) carries out this derivation for four control-policy families in Chapter 7, laying the groundwork every later stability chapter of the book (feedforward networks, the Rybko–Stolyar boundary, back-pressure, proportional fairness, task allocation) builds on.

The first-come-first-served (FCFS) analysis traces to Rybko and Stolyar's 1992 fluid-scaling argument and was first stated in closed form as Eq. (2.6) of M. Bramson's 1996 paper on FCFS queueing networks; Bramson also showed by example (1994) that FCFS networks can be unstable even under the standard load condition, motivating the need for a precise fluid-equation characterization rather than an informal one.

Setting

A queueing network (Section 2.6) is an SPN with one activity per buffer: buffer/class $i$ is served by a unique pool $p(i)$ , and on completion a class- $i$ job becomes class $j$ with probability $P_{ij}$ (the routing matrix). $I(k)$ denotes the set of classes served by pool $k$ . The fluid equations (6.1)-(6.6) specialize accordingly: consumption is the identity ( $\hat D = \hat F$ ) and the output matrix is $\Gamma_{ij} = P_{ji}$ .

Three control-policy families are studied. A policy is non-idling if no server sits idle while a job waits in one of its buffers. A static buffer priority (SBP) policy is non-idling and additionally orders same-pool classes by a fixed priority permutation $\sigma$ , always serving the highest-priority non-empty class first; it is non-preemptive if a job's service, once begun, is never interrupted by a later higher-priority arrival. Under FCFS, jobs at a pool are served strictly in arrival order — the workload-based analysis of Section 7.3. Section 7.4 studies a fourth, more general family: a unitary network (one service type per class) under a relaxed control policy $\beta = h(\hat z)$ , where $\hat z$ is the updated job-count vector and $h$ is any capacity-respecting, degree-zero-homogeneous function (Assumption 7.6) — a family general enough to include non-idling and SBP policies as special cases, and to anticipate the proportionally fair allocation studied in Chapters 9-10.

Formalization targets

Goal: Theorem 7.5 — the FCFS fluid equation

For a queueing network under FCFS control, every fluid limit path $(\hat D, \hat F, \hat T, \hat Z)$ satisfies (6.1)-(6.6) and

\hat D_i\big(t + \hat W_k(t)\big) = \hat G_i(t), \qquad t \ge 0,\ i \in I(k),\ k \in K,

where $\hat G_i(t) = \lambda_i t + \sum_j P_{ji}\hat D_j(t)$ is the fluid arrival rate into class $i$ and $\hat W_k(t) = \sum_{i \in I(k)} m_i \hat Z_i(t)$ is pool $k$ 's fluid-scaled immediate workload. This is the weakest natural target: an identity that pins down exactly the time-shift FCFS imposes, without asserting anything about how quickly or whether the fluid model reaches zero (that is left to the Lyapunov arguments of later chapters, once this equation is in hand).

Supporting milestones

Theorem 7.2 (non-idling): $\sum_{i\in I(k)} \hat Z_i(t) > 0$ forces pool $k$ 's aggregate service rate to run at full capacity $b_k$ . Theorem 7.3 (non-preemptive SBP): the same conclusion with $I(k)$ sharpened to the priority set $H(j)$ (Eq. 7.5), for every buffer $j$ . Theorem 7.8 (general relaxed control): under Assumption 7.6, $\hat Z_i(t) > 0$ forces $\hat T_i$ 's derivative to equal $h_i(\hat Z(t))$ exactly — the common generalization from which the non-idling and SBP fluid equations both follow as special cases of a suitable $h$ .

Significance

The result itself. Theorem 7.5 is the precise bridge that lets FCFS-specific stability questions be attacked by the Lyapunov-function method Theorem 6.2 licenses: without a closed-form fluid equation, "does an FCFS network satisfy the standard load condition stably?" has no tractable deterministic reformulation. Bramson's 1994 example (an FCFS network unstable despite satisfying the standard load condition) shows the equation's content is not vacuous — FCFS fluid limits genuinely can misbehave, and this equation is precisely what any subsequent stability or instability argument for FCFS networks must reason about.

Formalizing it. No result about FCFS, non-idling, static-buffer-priority, or general relaxed control policies exists on Prove2Me (q=first-come-first-served, q=FCFS, q=priority policy all return zero hits, consistent with triage.json's record that none of this book's Chapters 6-14 machinery is on the platform). This mission is a from-scratch formalization of queueing networks, their three named control-policy families, and the four policy-specific fluid equations Chapter 7 derives for them.

Difficulty

The obvious shortcut for Theorem 7.3 — reuse Theorem 7.2's hypothesis and conclusion verbatim with $I(k)$ replaced by $H(j)$ — conflates the preemptive and non-preemptive SBP policies: Remark 7.4 explicitly notes the underlying pathwise identity (7.4) (used directly by Theorem 7.2) holds unconditionally under preemption but only asymptotically, via a vanishing-remainder argument bounding the leftover processing time of interrupted-but-continuing jobs, under non-preemption — the theorem actually being formalized is about the harder, non-preemptive case. For Theorem 7.5, the central difficulty is that FCFS's defining property is a genuinely time-shifted identity (departures at $t + \hat W_k(t)$ match arrivals at $t$ ), not a same-instant conditional statement like the non-idling and SBP equations — an approach that tried to state FCFS as a same-instant condition on $\hat T$ or $\hat D$ alone, without introducing the auxiliary workload process $\hat W$ , could not express the theorem's actual content. A further subtlety Theorem 7.8's proof flags directly (Remark 7.9) is that the tempting converse — " $\hat Z_i(t) = 0$ implies zero service rate" — is false in general (a corrected version appears only later, as Lemma 8.9); this mission's goal and milestone statements are careful to assert only the one-directional implication the book actually proves.

Formalization scope

Mission III's fluid-limit-path apparatus (Definition 6.6, u.o.c. convergence) is restated locally in this chapter's own namespace rather than imported, since drafts in this series do not import one another; the restatement is trimmed to the four raw processes $(D^x,F^x,T^x,Z^x)$ this chapter's proofs need, omitting mission III's "delayed random walk" machinery. The non-idling and non-preemptive-SBP hypotheses are both formalized via one shared predicate, FullyUtilized, applied to different index sets ( $I(k)$ vs. $H(j)$ ) — the pathwise full-utilization identity (7.4) that each policy's proof establishes for its own priority classes, taken as a hypothesis rather than re-derived from a lower-level model of server scheduling (Chapter 2's construction of the service-starting mechanism is out of scope for this chapter, exactly as it was for mission III's SPNProcessFamily). Likewise, the FCFS goal theorem hypothesizes the raw identity (7.12) (rewritten via the material-balance equation to avoid needing the raw arrival process) and the fluid-scaled limit of the raw workload process (7.17), rather than re-deriving either from the "delayed random walk" $V$ of Eq. (6.47). A formalization that dropped the workload shift $\hat W_k(t)$ from Theorem 7.5's conclusion, or that stated Theorem 7.8's converse implication (which Remark 7.9 explicitly disclaims), would each be an unfaithful trivialization or overstatement ruled out here. QueueingNetworkData, ProcessFamily, FullyUtilized, and SatisfiesAssumption76 are the primary reusable contributions of this mission; contributions completing the four by sorry proofs — each of which needs the u.o.c.-convergence and dominated-convergence arguments mission III's own proofs still lack — are welcome.

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
M. Bramson, "Convergence to equilibria for fluid models of FIFO queueing networks," Queueing Systems 22 (1996), 5–45.
M. Bramson, "Instability of FIFO queueing networks," Annals of Applied Probability 4 (1994), 414–431.
A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.

9 thms2 active usersReviewed

Completed

Convex Optimization Functional Analysis Operations Research+1·Captain: mikedeng1

A Dynamical Approach to an Inertial Forward-Backward Algorithm for Convex Minimization: The IFB Iterates Minimize the Objective and Converge Weakly to a MinimizerResearch Paper

Motivation

Many problems in signal processing, statistics and operations research ask to minimize a sum $\Theta = \Phi + \Psi$ of a nonsmooth convex term $\Phi$ (a constraint indicator, an $\ell^1$ penalty) and a smooth term $\Psi$ . The standard method is the forward-backward (proximal-gradient) algorithm: an explicit gradient step on $\Psi$ followed by a proximal step on $\Phi$ . Its classical convergence theory requires $\Psi$ to be convex and the step size to stay below $2/L_\Psi$ , where $L_\Psi$ is the Lipschitz constant of $\nabla\Psi$ .

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 $2/L_\Psi$ and a smooth part $\Psi$ that is not convex, provided the sum $\Theta$ is.

Timeline of the relevant results:

Heavy-ball-with-friction methods, the inertial discretizations of $\ddot u + \alpha\dot u + \nabla\Phi(u) = 0$ , were introduced by Polyak (1964) and developed by Alvarez and Attouch (2001) for proximal schemes.
Hessian-driven damping for one potential: Alvarez, Attouch, Bolte and Redont (2002); for a nonsmooth potential plus a smooth one, the continuous dynamics underlying (IFB): Attouch, Maingé and Redont (2012).
The discrete algorithm (IFB) and its weak convergence in Hilbert spaces: Attouch, Peypouquet and Redont (2014), the paper of this mission.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ . Let $\Phi : H \to \mathbb R\cup\{+\infty\}$ and $\Psi : H \to \mathbb R$ , and write $\Theta = \Phi + \Psi$ and $\mathcal S = \operatorname{Argmin}\Theta$ . A vector $g$ is a subgradient of $\Phi$ at $u$ , written $g \in \partial\Phi(u)$ , if $\Phi(u) < +\infty$ and $\Phi(u) + \langle g, v - u\rangle \le \Phi(v)$ for all $v$ .

Hypothesis H fixes positive constants $L_\Psi$ , $a$ , $b$ and a step size $\lambda$ with:

$H_\Phi$ : $\Phi$ is proper, lower semicontinuous and convex;
$H_\Psi$ : $\Psi$ is differentiable and $\nabla\Psi$ is $L_\Psi$ -Lipschitz;
$H_\lambda$ : $0 < \lambda < \Lambda = \min\{1/a,\ 2(a+b)/(bL_\Psi)\}$ ;
$H_\Theta$ : $\Theta$ is convex and bounded from below.

Algorithm (IFB). From any $(u_0, y_0) \in H \times H$ , compute for $k \ge 0$

0 \in \frac{u_{k+1}-u_k}{\lambda} + \partial\Phi(u_{k+1}) + a u_k - b y_k, \qquad 0 = \frac{y_{k+1}-y_k}{\lambda} + \nabla\Psi(u_{k+1}) - a u_{k+1} + b y_{k+1}.

A sequence $u_k$ converges weakly to $p$ , written $u_k \rightharpoonup p$ , if $\langle u_k, v\rangle \to \langle p, v\rangle$ for every $v \in H$ . The analysis uses the velocity $\xi_k = u_k - u_{k-1}$ , the energy $E_k = \Theta(u_k) + \gamma\|\xi_k\|^2$ with $\gamma = (1-a\lambda)/(2b\lambda^2)$ , and two auxiliary real sequences $G_k(q)$ and $F_k(q)$ , defined from $u$ , $y$ and a reference point $q$ by (17) and (18) of the paper.

Formalization targets

Goal: Theorem 1

Under Hypothesis H, for every sequence generated by (IFB),

\lim_{k\to\infty}\Theta(u_k) = \inf\Theta;

if $\mathcal S \ne \emptyset$ and one of (i) $\mathcal S$ is a singleton, (ii) $\Phi$ is differentiable with weak-to-weak sequentially continuous gradient, (iii) $\nabla\Psi$ is weak-to-weak sequentially continuous, (iv) $\Psi$ is convex, holds, then

u_k \rightharpoonup p \quad\text{for some } p \in \mathcal S;

and if $\mathcal S = \emptyset$ , then $\|u_k\| \to +\infty$ .

Milestones

In the order of the paper's argument: Proposition 2 (energy decrease, $\sum\|\xi_k\|^2 < \infty$ ); Proposition 3 (the identity and inequality (19) for $F_k(q)$ ); Proposition 4 ( $G_k(q)$ is bounded above for $q\in\operatorname{dom}\Phi$ ); the lower bound (28) on $F_k(q)$ ; Lemma 5 (a real-sequence lemma); Proposition 6 ( $\Theta(u_k)\to\inf\Theta$ , weak cluster points lie in $\mathcal S$ ); Lemma 7 (a boundedness lemma); Proposition 8 (boundedness of $(u_k)$ and convergence of $F_k(q)$ when $\mathcal S \ne\emptyset$ ).

Significance

The result gives convergence of a forward-backward type method under a step-size bound $\Lambda$ that can be made arbitrarily large by choosing $a$ small, and for a smooth term $\Psi$ that need not be convex. The special case $\Phi = \delta_C$ (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 $\ell^1$ 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.

Difficulty

The energy $E_k$ controls the values $\Theta(u_k)$ and the velocities $\xi_k$ , but not the iterates themselves. The first idea, proving that $\|u_k - q\|$ is nonincreasing for every $q \in \mathcal S$ (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 $y_k$ couples consecutive steps, and the distance to a minimizer is not a Liapunov function. The paper's replacement, the sequence $F_k(q)$ , carries the auxiliary sum $G_k(q)$ , whose upper bound already requires the full Hypothesis H. Because $H$ is infinite-dimensional, bounded sequences have only weakly convergent subsequences, so the minimizing property has to pass through weak lower semicontinuity of $\Theta$ , 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.

Formalization scope

$H$ is a general real Hilbert space (InnerProductSpace ℝ H with CompleteSpace H); nothing is specialized to finite dimension.
$\Phi$ and $\Theta$ take values in EReal. Properness excludes $-\infty$ . Convexity of an extended-valued function is convexity of its epigraph in $H\times\mathbb R$ , because Mathlib's ConvexOn needs a scalar action that EReal lacks. The subgradient predicate requires $\Phi(u) < +\infty$ , so $\partial\Phi(u) = \emptyset$ off $\operatorname{dom}\Phi$ .
(IFB) is encoded as the subgradient inclusion, not through the proximity operator. Weak convergence is convergence of all inner products $\langle u_k, v\rangle$ ; weak cluster points are weak limits along strictly increasing subsequences.
$L_\Psi > 0$ is assumed (harmless: a Lipschitz gradient is Lipschitz with every larger constant). The step size $\lambda$ is written lam.
$\xi_k$ , $z_k$ , $E_k$ , $G_k$ , $F_k$ are defined on all natural indices, and each statement quantifies $k \ge 1$ (or $k \ge 2$ for $G_k$ ) as the paper does. Energies and values are never truncated to real numbers, so no statement becomes true through the convention EReal.toReal ⊤ = 0.
Deviation from the printed text: Proposition 4 is printed under $H_\Phi$ and $H_\Psi$ only, but its proof invokes Proposition 2, which needs all of Hypothesis H, and the printed statement is false for step sizes above $\Lambda$ (e.g. $H=\mathbb R$ , $\Phi = x^2/2$ , $\Psi = 3x^2/2$ , $a=2$ , $b=0.02$ , $\lambda = 10$ ). The milestone is stated under the full Hypothesis H.
A formalization in which $\partial\Phi(u)$ is nonempty at points of infinite value, in which the energy is converted to a real number, or in which Hypothesis H cannot be satisfied, would make these statements trivial or vacuous, and is ruled out by the definitions above.

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.

Selected references

H. Attouch, J. Peypouquet, P. Redont, A Dynamical Approach to an Inertial Forward-Backward Algorithm for Convex Minimization, SIAM J. Optim. 24(1), 2014 (statements cited from the authors' manuscript of Aug 2013). https://doi.org/10.1137/130910294
H. Attouch, P.-E. Maingé, P. Redont, A second-order differential system with Hessian-driven damping; application to non-elastic shock laws, Differential Equations and Applications 4(1), 2012. https://doi.org/10.7153/dea-04-02
F. Alvarez, H. Attouch, An inertial proximal method for maximal monotone operators via discretization of a nonlinear oscillator with damping, Set-Valued Analysis 9, 2001. https://doi.org/10.1023/A:1011253113155
F. Alvarez, H. Attouch, J. Bolte, P. Redont, A second-order gradient-like dissipative dynamical system with Hessian-driven damping, J. Math. Pures Appl. 81(8), 2002. https://doi.org/10.1016/S0021-7824(01)01253-3
B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Comput. Math. Math. Phys. 4(5), 1964. https://doi.org/10.1016/0041-5553(64)90137-5
Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73, 1967. https://doi.org/10.1090/S0002-9904-1967-11761-0

12 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

On the Optimality of Generalized (s, S) Policies: A Generalized (s, S) Policy Is Optimal in Every Period of the Finite-Horizon Inventory ProblemResearch Paper

Motivation

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

Timeline:

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 3

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Added hypotheses and conventions:

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

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

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

Selected references

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

13 thms3 active usersReviewed

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

On the Optimal Dividend Problem for a Spectrally Negative Lévy Process I: Optimality of the Barrier Strategy at c* in the Classical Dividend ProblemResearch Paper

Motivation

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 $+\infty$ 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 $a$ 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 $c^*$ . They also gave a verification condition under which the barrier at $c^*$ is optimal among all strategies. Loeffen (2008) later showed that the condition holds whenever the Lévy measure has a completely monotone density.

Setting

Let $X=(X_t)_{t\ge0}$ be a spectrally negative Lévy process on a filtered probability space $(\Omega,\mathcal F,\mathbb F,P)$ with $X_0=0$ and Lévy triplet $(c,\sigma,\nu)$ . Its Laplace exponent is $\psi(\theta)=\log\mathbf E[e^{\theta X_1}]$ , finite for $\theta\ge0$ :

\psi(\theta)=c\theta+\tfrac{\sigma^2}{2}\theta^2+\int_{(-\infty,0)}\bigl(e^{\theta y}-1-\theta y\mathbf 1_{\{|y|<1\}}\bigr)\nu(dy).

Increments after time $s$ are independent of $\mathcal F_s$ . Initial capital $x$ is added to $X$ . The standing assumptions are the following: $X$ does not have monotone paths, $\mathbf E[X_1]>-\infty$ , and either $\sigma>0$ , $\int_{(-1,0)}|y|\,\nu(dy)=\infty$ , or $\nu$ has a density.

A dividend strategy is a nondecreasing, left-continuous, adapted process $L$ with $L_0=0$ . The risk process is $U_t=x+X_t-L_t$ and the ruin time is $\sigma^L=\inf\{t\ge0:U_t<0\}$ . The strategy is admissible ( $L\in\Pi$ ) if no lump sum exceeds the current reserves. Its value is

v_L(x)=\mathbf E\Bigl[\int_0^{\sigma^L}e^{-qt}\,dL_t\Bigr],\qquad v_*(x)=\sup_{L\in\Pi}v_L(x),

with discount rate $q>0$ . For $C\in[0,\infty]$ , $\Pi_{\le C}$ consists of the admissible strategies that keep $U_t\le C$ for $t>0$ .

The $q$ -scale function $W=W^{(q)}$ is the unique continuous nondecreasing function on $[0,\infty)$ with $\int_0^\infty e^{-\theta y}W(y)\,dy=1/(\psi(\theta)-q)$ for large $\theta$ . It is extended by $W=0$ on $(-\infty,0)$ . The barrier strategy $\pi_a$ reflects $x+X$ at the level $a$ , paying $(x-a)^+$ at time $0$ . The paper computes its value

v_a(x)=\frac{W(x)}{W'(a)}\ (0\le x\le a),\qquad v_a(x)=x-a+\frac{W(a)}{W'(a)}\ (x>a),

and the optimal barrier level is $c^*=\inf\{a>0: W'(a)\le W'(x)\ \forall x>0\}$ , read as $0$ when this set is empty and $W'(0+)\le W'(x)$ for all $x>0$ . The generator is

\Gamma f(x)=\tfrac{\sigma^2}{2}f''(x)+cf'(x)+\int_{(-\infty,0)}[f(x+y)-f(x)-f'(x)y\mathbf 1_{\{|y|<1\}}]\,\nu(dy).

Formalization targets

Goal: Theorem 2 (p. 14)

Assume $\sigma>0$ , or $X$ has bounded variation, or $v_{c^*}\in C^2(0,\infty)$ . Then $c^*<\infty$ and:

\text{(i)}\quad \pi_{c^*}\in\Pi_{\le c^*},\qquad v_{\pi_{c^*}}(x)=v_{c^*}(x)=\sup_{\pi\in\Pi_{\le c^*}}v_\pi(x)\quad(x\ge0);

\text{(ii)}\quad (\Gamma v_{c^*}-qv_{c^*})(x)\le0\ \ \forall x>c^*\ \Longrightarrow\ v_*(x)=v_{c^*}(x)\ (x\ge0),\ \ \pi_*=\pi_{c^*}.

The goal fixes no constants: the barrier level and the value function are both given by the scale function of the given process.

Milestones

Proposition 1 (p. 7): $v_{\pi_a}(x)=W(x)/W'(a)$ for $a>0$ , $x\in[0,a]$ .
Lemma 2(i) (p. 15): $c^*<\infty$ .
Proposition 3(i) (p. 15): $v_a(x)\le v_{c^*}(x)$ for $x\in[0,c^*]$ , $a\ge0$ .
Lemma 3(i) (p. 16): $v_{c^*}'(x)\ge1$ for $x>0$ .
Proposition 4(i) (p. 18): a $C^2$ (unbounded variation) or $C^1$ (bounded variation) solution $w$ of $\max\{\Gamma w-qw,1-w'\}=0$ on $(0,C)$ dominates $\sup_{\Pi_{\le C}}v_\pi$ .
Lemma 4 (p. 20): $(\Gamma v_{c^*}-qv_{c^*})(x)=0$ on $(0,c^*)$ when $c^*>0$ .

Significance

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, $W^{(q)}$ , and optimality over all strategies reduces to one inequality on $(c^*,\infty)$ . 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.

Difficulty

The analytic part is elementary once the value formula (5.1) is available: the choice of $c^*$ , Proposition 3(i) and Lemma 3(i) follow from the shape of $W'$ . The difficulty lies in the two probabilistic steps. Proposition 1 identifies the value of a reflected process through exit identities for $X$ . Those identities rest on excursion theory, or on the martingale property of $e^{-qt}W(X_t)$ up to exit. The verification step, Proposition 4(i), needs Itô's formula for $w(U_t)$ . Here $U$ 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 $C^1$ regularity when $X$ has bounded variation. Just proving that $\Gamma w-qw\le0$ and $w'\ge1$ imply a supermartingale inequality does not settle the question: the lump-sum payments and the jumps of $X$ enter the Itô expansion separately and must each be bounded.

Formalization scope

Time is $[0,\infty)$ (ℝ≥0). $X$ is a structure carrying the triplet $(c,\sigma,\nu)$ 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 $\mathbf E[e^{\theta X_t}]=e^{t\psi(\theta)}$ for $\theta\ge0$ . The standing assumptions of §2 and (3.3) are bundled as one predicate. The scale function is a hypothesis on a function argument $W$ (it is unique). $W'(0+)$ is an extended real, since it is $+\infty$ for unbounded variation without a Gaussian part.

Values of strategies and value functions lie in $[0,\infty]$ . The dividend integral is a Lebesgue–Stieltjes integral over $[0,\sigma^L)\cup\{0\}$ : it counts the lump sum at time $0$ and excludes a payment at the ruin instant.

Several conventions are fixed, and each is disclosed in the item it affects:

Admissibility. The paper requires $L_{t+}-L_t<U_t$ . The formalization uses $\le$ , because the paper's own strategy of paying out everything at once needs it.
Barrier level (5.2). Printed over $a>0$ and "all $x$ ", the defining set is empty for Brownian motion with nonpositive drift. The printed set (with $x>0$ ) is kept whenever it is nonempty; when it is empty and $W'(0+)\le W'(x)$ for all $x>0$ — the second alternative in the proof of Lemma 2(i) — $c^*=0$ , and otherwise $c^*=\infty$ .
Printed slips. The integral $\int_{-1}^0 x\,\nu(dx)$ in (3.3) is read as $\int|x|\,\nu(dx)$ . In (3.4), $e^{-\theta x}$ is read as $e^{-\theta y}$ , and in Theorem 2(i), $\pi^*_c$ is read as $\pi_{c^*}$ .
Proposition 4(i) is stated for initial capital $x\le C$ . Beyond $C$ , $w$ is unconstrained and the printed claim fails.
Lemma 4 carries the smoothness proviso of Theorem 2 on $(0,c^*)$ .

A trivializing encoding is ruled out: the value is not a real supremum, the barrier strategy is constructed rather than assumed, and $c^*<\infty$ is a conclusion.

A complete development needs:

Lévy processes and their Laplace exponents;
scale functions and the exit identity $\mathbf E_x[e^{-qT}\mathbf 1_{\{X_T=a\}}]=W(x)/W(a)$ ;
reflected processes;
Itô's formula for jump semimartingales with finite-variation controls.

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.

Selected references

F. Avram, Z. Palmowski, M. R. Pistorius, On the optimal dividend problem for a spectrally negative Lévy process, Ann. Appl. Probab. 17 (2007) 156–180. https://arxiv.org/abs/math/0702893
P. Azcue, N. Muler, Optimal reinsurance and dividend distribution policies in the Cramér–Lundberg model, Math. Finance 15 (2005) 261–308.
M. Jeanblanc-Picqué, A. N. Shiryaev, Optimization of the flow of dividends, Russian Math. Surveys 50 (1995) 257–277.
R. L. Loeffen, On optimality of the barrier strategy in de Finetti's dividend problem for spectrally negative Lévy processes, Ann. Appl. Probab. 18 (2008) 1669–1680.
A. E. Kyprianou, Introductory Lectures on Fluctuations of Lévy Processes with Applications, Springer, 2006. https://doi.org/10.1007/978-3-540-31343-4

147 thms6 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks V: Lyapunov Stability Criteria for Fluid ModelsTextbook

Motivation

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

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

Setting

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

Formalization targets

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

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

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

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

Supporting milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

13 thms3 active usersReviewed

Completed

Convex Optimization Functional Analysis Operations Research·Captain: mikedeng1

On the Maximal Monotonicity of Subdifferential Mappings I: The Subdifferential of a Lower Semicontinuous Proper Convex Function on a Banach Space Is Maximal MonotoneResearch Paper

Motivation

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

Timeline:

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

Setting

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

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

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

\partial f(x) = \{\, x^* \in E^* \mid f(y) \ge f(x) + \langle y - x, x^* \rangle \ \ \forall y \in E \,\}.

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

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

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

Formalization targets

Goal: Theorem A (p. 210)

f \text{ lower semicontinuous proper convex on } E \quad\Longrightarrow\quad \partial f : E \to E^* \text{ is maximal monotone.}

No reflexivity, inner product or finite dimension is assumed.

Milestones, in attack order

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

Significance

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

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

Difficulty

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

Formalization scope

Lean representation and committed conventions:

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

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

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

Selected references

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

13 thms3 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks VI: Feedforward and Generalized Jackson Network StabilityTextbook

Motivation

Mission V supplied the general Lyapunov machinery — the extinction criteria of Lemmas 8.5, 8.6 and 8.11 — but a Lyapunov function does not construct itself. For a specific network structure and control policy, one must exhibit a concrete function and verify the drift condition. 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 the second half of Chapter 8 to two such constructions, chosen to illustrate the two basic templates every later stability chapter follows: a piecewise-linear Lyapunov function tailored to a structural network property (feedforward routing), and a linear one that works for an unrestricted network but is tailored to a specific control policy (head-of-line proportional service, HLSPS). Together they cover, as a corollary, the generalized Jackson network — the classical multiclass queueing network with one server per class — under ordinary non-idling FCFS.

Setting

A queueing network (Section 2.6, restated from mission IV) is feedforward (Definition 8.13) if its stations admit a numbering under which no station routes work to a lower-numbered one (feedback to the same station is still allowed). The workload operator $W(z) := AM(I-P')^{-1}z$ (Eq. 8.24) gives, for any buffer-contents vector $z$ , the total service effort each pool would need to drain $z$ to emptiness with no further arrivals; the load vector of the standard load condition is $\rho = W(\lambda)$ (Eq. 8.25), and the total arrival rate vector $\alpha$ (including internally routed traffic) is the unique solution of the traffic equations $\alpha = \lambda + P'\alpha$ . A queueing network under HLSPS control (Definition 8.17) splits each pool's capacity among its classes in fixed proportions $\gamma_i := \alpha_i m_i/\rho_{p(i)}$ (Eq. 8.30) — a policy general enough to reduce, for a generalized Jackson network (one class per pool), to ordinary non-idling FCFS.

Formalization targets

Goal: Theorem 8.18 — HLSPS control is stable under the standard load condition

For any queueing network under HLSPS control with proportion vector $\gamma$ , if

\rho < b \qquad (\text{the standard load condition, Eq. 5.1}),

the corresponding fluid model is stable, and hence (Theorem 6.2) the network itself is stable under HLSPS control. This is the weaker of the two possible capstones only in the sense that it fixes one specific policy; it is chosen over Theorem 8.14 as the goal because it needs the full generality of the workload-based linear Lyapunov argument (Lemma 8.20) with no structural restriction on the network's routing, whereas Theorem 8.14 trades policy generality for a feedforward restriction.

Supporting milestones

Lemma 8.15 isolates the workload derivative identity $\dot W_k(Z(t)) = \rho_k - b_k$ at a busy station under any non-idling policy — the calculational engine both Theorem 8.14 and (via Lemma 8.20's analogous linear-potential argument) Theorem 8.18 rely on. Theorem 8.14 shows a feedforward network is stable under any non-idling policy, via a piecewise-linear Lyapunov function built from the routing matrix's block-triangular structure. Lemma 8.20 (numbered in the book but omitted from this mission's planning brief — added here, see STATUS.md) is the direct structural engine behind the goal theorem: a uniform excess departure rate over the total arrival rate at every non-empty class forces extinction. Corollary 8.19 specializes Theorem 8.18 to generalized Jackson networks, where HLSPS provably reduces to non-idling FCFS.

Significance

The result itself. Theorem 8.18 is the book's demonstration that dropping a structural network restriction (feedforward) is possible at the cost of committing to one specific, practically implementable control policy — and Corollary 8.19 shows this specific policy's stability theorem recovers, as a special case, the folklore stability result for the classical multiclass Jackson network under FCFS, arguably the single most studied queueing model in the field. Theorem 8.14, in turn, is the sharpest possible policy-agnostic statement: for feedforward networks, subcriticality alone (with no assumption at all beyond non-idling) suffices.

Formalizing it. Searches for "Jackson network" and "workload" (q=Jackson%20network, q=workload) return no relevant results (per triage.json); this mission is a from-scratch formalization of feedforward networks, the workload operator, HLSPS control, and their stability theorems, building directly on mission III's Theorem 6.2 and mission V's Lyapunov criteria.

Difficulty

Theorem 8.14's proof needs a genuinely delicate construction: a sequence of positive weights $\delta_k$ , chosen via the routing matrix's block-triangular structure (guaranteed by feedforwardness) so that the piecewise-linear function $H(z) = \max_k \delta_k W_k(z)$ is positive-definite and has the right drift everywhere — an inductive argument over stations that does not generalize to non-feedforward networks, which is exactly why Theorem 8.18 needs an entirely different (linear, policy-specific) argument rather than a direct strengthening of 8.14's. A second, more subtle difficulty is that Theorem 8.14 and Theorem 8.18 are not related as special case and generalization in the book's own proof structure, despite their overlapping conclusions on feedforward networks under FCFS-like policies: 8.14 is agnostic to policy but needs feedforward structure, while 8.18 is agnostic to structure but needs the specific HLSPS policy — formalizing one as a corollary of the other would misrepresent the book's actual logical dependencies.

Formalization scope

Mission IV's queueing-network model data and fluid-equation specialization are restated locally (drafts in this series do not import one another). The workload operator's matrix inverse $(I-P')^{-1}$ is supplied as external data with its defining two-sided-inverse property, rather than derived from substochasticity/transience hypotheses on $P$ (Chapter 2 material, out of series scope) — the same convention mission III used for its process-family apparatus. The non-idling and HLSPS fluid models are each packaged as their own predicate plus a Definition-6.3-style stability specialization, and Corollary 8.19 deliberately reuses the non-idling stability object (not a separately restated "FCFS fluid model") since the book's own remark identifies the two exactly for generalized Jackson networks. A formalization that stated Theorem 8.14 as a corollary of Theorem 8.18, or vice versa, would misrepresent the chapter's actual proof architecture (see Difficulty); this mission keeps them as independent milestones/ goal, per BRIEF.md's own instruction. Lemma 8.20, numbered and within this chunk's page range but absent from the planning brief's disposition table, is added as a milestone rather than silently dropped, since it is the structural step the goal theorem's own proof cites by name. QueueingNetworkData, workloadOperator, IsFeedforward, and the non-idling/HLSPS fluid-model predicates are the primary reusable contributions; contributions completing the five by sorry proofs are welcome.

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.
M. Bramson, "Convergence to equilibria for fluid models of FIFO queueing networks," Queueing Systems 22 (1996), 5–45.

10 thms2 active usersReviewed

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

On the Optimal Dividend Problem for a Spectrally Negative Lévy Process II: Optimality of the Double-Barrier Strategy at d* with Bail-Out LoansResearch Paper

Dividends, ruin and bail-out loans

An insurance company's surplus in the Cramér–Lundberg model grows linearly with premiums and falls by claims arriving as a compound Poisson process. When premium income exceeds the expected claims, the surplus drifts to infinity. De Finetti (1957) proposed that the surplus above a barrier should instead be paid to shareholders as dividends, and the resulting optimal dividend problem — maximize the expected discounted dividends — is a central problem of risk theory. A barrier policy, however, drives the surplus below zero with probability one. Harrison and Taylor (1978) and Løkka and Zervos studied, for Brownian motion, a variant with bail-out loans: ruin is forbidden, and the shareholders must inject capital whenever the surplus would become negative, at a cost $\varphi>1$ per unit.

Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007)) solved the bail-out problem when the surplus is a general spectrally negative Lévy process, which includes the Cramér–Lundberg model, Brownian motion with drift and their sums. They showed that the optimal policy is a double barrier policy for every initial capital. This mission formalizes that result, Theorem 3 of the paper.

Timeline:

1957 — de Finetti introduces dividend barriers.
1978 — Harrison and Taylor: optimal control of a Brownian storage system with two reflecting barriers.
1995 — Jeanblanc and Shiryaev: optimal dividends for Brownian motion with drift.
2004 — Avram, Kyprianou and Pistorius: exit problems for spectrally negative Lévy processes reflected at their infimum and supremum, in terms of scale functions.
2007 — Avram, Palmowski and Pistorius: Theorems 1 and 3 of the present paper; Pistorius' pathwise construction of the doubly reflected process is used.

Setting

A spectrally negative Lévy process $X=\{X_t\}_{t\ge0}$ on a filtered probability space $(\Omega,\mathcal F,\mathbb F,P)$ starts at $X_0=0$ , has càdlàg paths, is $\mathbb F$ -adapted, and has stationary increments with $X_t-X_s$ independent of $\mathcal F_s$ . Its jumps are all negative, and $E[e^{\theta X_t}]=e^{t\psi(\theta)}$ for $\theta\ge0$ , where the Laplace exponent is

\psi(\theta)=c\theta+\tfrac{\sigma^2}{2}\theta^2+\int_{(-\infty,0)}(e^{\theta y}-1-\theta y\mathbf 1_{\{|y|<1\}})\,\nu(dy).

With initial capital $x\ge0$ the surplus is $x+X$ . The standing assumptions are: $X$ does not have monotone paths; $E[X_1]>-\infty$ (so $\psi'(0+)=E[X_1]$ is finite); $\sigma>0$ , or $\int_{(-1,0)}|y|\nu(dy)=\infty$ , or $\nu$ has a density (condition (3.3)).

A policy $\bar\pi=(L,R)$ consists of nondecreasing adapted processes with $L_0=R_0=0$ : cumulative dividends $L$ (left-continuous) and cumulative injected capital $R$ (right-continuous). The controlled surplus is $V_t=x+X_t-L_t+R_t$ . The policy is admissible if $V_t\ge0$ for $t>0$ and $\int_0^\infty e^{-qt}dR_t<\infty$ almost surely. Its value and the value function are

\bar v_{\bar\pi}(x)=E\Bigl[\int_0^\infty e^{-qt}dL_t-\varphi\int_0^\infty e^{-qt}dR_t\Bigr],\qquad \bar v_*(x)=\sup_{\bar\pi\ \text{admissible}}\bar v_{\bar\pi}(x),

with discount rate $q>0$ and cost $\varphi>1$ . The double-barrier strategy $\bar\pi_{0,a}$ pays out $(x-a)^+$ at once and then the minimal dividends and injections that keep $V$ in $[0,a]$ : $dL$ is carried by $\{V=a\}$ and $dR$ by $\{V=0\}$ .

The $q$ -scale function $W=W^{(q)}$ vanishes on $(-\infty,0)$ , is continuous and nondecreasing on $[0,\infty)$ , and satisfies $\int_0^\infty e^{-\theta y}W(y)dy=1/(\psi(\theta)-q)$ for $\theta>\Phi(q)$ , the largest root of $\psi=q$ . Set $\overline W(y)=\int_0^yW$ , $Z=1+q\overline W$ , $\overline Z(y)=\int_0^yZ$ . The candidate value of $\bar\pi_{0,a}$ is

\bar v_a(x)=\varphi\bigl(\overline Z(x)+\psi'(0+)/q\bigr)+Z(x)\frac{1-\varphi Z(a)}{qW(a)}\quad(0\le x\le a),\qquad \bar v_a(x)=x-a+\bar v_a(a)\quad(x>a),

and the barrier level is $d^*=\inf\{a>0:[\varphi Z(a)-1]W'(a)-\varphi qW(a)^2\le0\}$ , with $\inf\emptyset=\infty$ .

Formalization targets

Goal: Theorem 3

d^*<\infty,\qquad \bar v_*(x)=\bar v_{d^*}(x)\ \ (x\ge0),\qquad \bar\pi_{0,d^*}\ \text{exists, is admissible and attains }\bar v_*(x).

Milestones

Lemma 1: $\overline W(y)/\overline W(a)\le W(y)/W(a)$ for $0\le y\le a$ .
Proposition 2, (3.17): the expected discounted undershoot $E_x[e^{-qT_0^-}X_{T_0^-}]$ in closed form.
Theorem 1: the expected discounted dividends and injections of $\bar\pi_{0,a}$ , $a>0$ , in closed form; hence $\bar v_{\bar\pi_{0,a}}=\bar v_a$ .
Lemma 2(ii): $d^*=0$ if and only if $\sigma=0$ and $\nu(-\infty,0)\le q/(\varphi-1)$ .
Proposition 3(ii): $d^*<\infty$ and $\bar v_a\le\bar v_{d^*}$ for all levels $a$ .
Lemma 3(ii)–(iv): $1\le\bar v_{d^*}'\le\varphi$ with boundary slopes; $a\mapsto\bar v_a(x)$ nonincreasing for $a>d^*$ ; $\bar v_{d^*}$ concave.
Lemma 5: $(\Gamma\bar v_{d^*}-q\bar v_{d^*})\le0$ on $(0,\infty)$ , with equality on $(0,d^*)$ .
Proposition 4(ii): any $C^2$ solution of the variational inequality (5.9) dominates $\bar v_*$ .

Significance

Theorem 3 answers the bail-out problem completely: for every initial capital and every spectrally negative Lévy surplus, the optimal policy is a double barrier with an explicit level and an explicit value in terms of scale functions. In the classical problem without injections (Theorem 2 of the same paper) the analogous conclusion needs an extra generator condition, and Azcue and Muler exhibited Cramér–Lundberg models where barrier policies are not optimal. The result is the basis of later work on dividends with capital injection, transaction costs and Parisian ruin.

The result has a published proof. What this mission adds is a machine-checked version. As far as is known, no part of the theory used — Lévy processes, scale functions, doubly reflected processes, the generator of a Lévy process, singular stochastic control — has been formalized in Lean's Mathlib.

Difficulty

The value function is a supremum over all adapted singular controls. Its upper bound requires a verification argument: Itô's formula for $e^{-qt}w(V_t)$ with a semimartingale $V$ that has jumps, a controlled bounded-variation part and a possibly nonzero continuous martingale part, followed by localization and limits. A function that satisfies the variational inequality only in the viscosity sense is not enough, so the candidate $\bar v_{d^*}$ must be shown to be regular enough and to satisfy $\Gamma\bar v_{d^*}-q\bar v_{d^*}\le0$ everywhere on $(0,\infty)$ . Above the barrier this inequality does not follow from a martingale property: the paper derives it from concavity and a comparison with higher barriers, through the resolvent of the doubly reflected process. The lower bound requires the existence and value of the doubly reflected process, and computing that value needs fluctuation identities (two-sided exit, overshoot) that are themselves theorems about scale functions.

Formalization scope

Time is indexed by $\mathbb R_{\ge0}$ . The process is a structure carrying the triplet $(c,\sigma,\nu)$ , the paths, adaptedness, independence of future increments from $\mathcal F_s$ , stationarity, the Laplace-exponent identity, and the usual conditions on the filtration. $P_x$ is the law of $x+X$ . Policy values are computed as $E[\int e^{-qt}dL]-\varphi E[\int e^{-qt}dR]$ in the extended reals from two $[0,\infty]$ -valued expectations, and the value function is a supremum in the extended reals; a policy with both expectations infinite gets $-\infty$ . Stieltjes integrals include the jump at time $0$ . The scale function is a hypothesis IsScaleFunction (it is unique), and $d^*$ lives in $[0,\infty]$ , so an empty defining set gives $\infty$ . The double-barrier strategy is characterized by the two-sided Skorokhod conditions plus mutual singularity of $dL$ and $dR$ , which pins the level- $0$ policy of bounded-variation processes. These conditions hold almost surely, and they are stated on the post-decision surplus $V_{t+}=x+X_t-L_{t+}+R_t$ : $dL$ is carried by $\{V_{t+}=a\}$ and $dR$ by $\{V_{t+}=0\}$ . This is the paper's "minimal amount" (p. 4) and matches its construction on pp. 10–11. The closure-of-support wording of (4.2) on its own would also admit non-minimal lump dividends. Admissibility, $V_t\ge0$ for $t>0$ together with (2.3), is likewise required almost surely.

Printed slips corrected (milestone texts are verbatim):

Theorem 3 and Proposition 3(ii) print " $\psi'(0+)<\infty$ ", which always holds; the intended $\psi'(0+)>-\infty$ is used.
(3.3) prints $\int_{-1}^0x\,\nu(dx)=\infty$ for $\int_{(-1,0)}|x|\,\nu(dx)=\infty$ .
(3.4) prints $e^{-\theta x}$ in a $dy$ -integral.
p. 20 prints the extension $\bar v_{d^*}(x)+\varphi x$ for $\bar v_{d^*}(0)+\varphi x$ .
Lemma 3(iv) is printed for every $a>0$ but proved and used only for $a=d^*$ , and is stated for $a=d^*$ .
Proposition 3(ii) at $a=0$ is stated only for bounded variation, where $\bar v_0$ is defined.

The goal cannot be satisfied trivially. It asserts equality of the value function with $\bar v_{d^*}$ , not only an inequality. Existence of the optimal policy is part of the conclusion. Generator statements carry integrability of the jump integrand, so a non-integrable integrand cannot make them true with the junk value $0$ .

A complete development needs Lévy processes and their Laplace exponents, scale functions, first-passage and two-sided exit identities, reflected and doubly reflected processes, Itô's formula for semimartingales with jumps, and a verification theorem for singular control. All of these are reusable well beyond this mission. Contributions of any of these foundations are welcome, as are proofs of the analytic milestones (Lemma 3, Proposition 3(ii)) from the scale-function properties.

Selected references

F. Avram, Z. Palmowski, M. R. Pistorius, On the optimal dividend problem for a spectrally negative Lévy process, Ann. Appl. Probab. 17 (2007) 156–180. https://arxiv.org/abs/math/0702893
F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14 (2004) 215–238. https://doi.org/10.1214/aoap/1075828052
M. R. Pistorius, On doubly reflected completely asymmetric Lévy processes, Stochastic Process. Appl. 107 (2003) 131–143. https://doi.org/10.1016/S0304-4149(03)00065-9
J. M. Harrison, A. J. Taylor, Optimal control of a Brownian storage system, Stochastic Process. Appl. 6 (1978) 179–194. https://doi.org/10.1016/0304-4149(78)90059-5
A. E. Kyprianou, Introductory Lectures on Fluctuations of Lévy Processes with Applications, Springer, 2006. https://doi.org/10.1007/978-3-540-31343-4

15 thms1 active userReviewed

Operations Research Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks VII: Global Stability, Rings, and the Rybko–Stolyar BoundaryTextbook

Motivation

Mission VI showed that two structural families of queueing networks — feedforward routing, and any network under HLSPS control — are stable throughout their entire subcritical region: no extra condition beyond the standard load condition is ever needed. Until the early 1990s it was widely conjectured that this held for every queueing network. Rybko and Stolyar's 1992 example disproved it: a specific, entirely reasonable two-station network, still subcritical, whose buffer contents grow without bound under a particular non-idling policy. 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 the third part of Chapter 8 to mapping the boundary this discovery opened up: which network structures still enjoy subcriticality-implies-stability (unidirectional rings), and, for a network that does not, exactly what extra condition restores it (the two-station, five-class re-entrant line, the book's own worked instance of the Rybko–Stolyar phenomenon).

Setting

A queueing network is globally stable (Definition 8.22) if it is Markov-chain stable under every simply structured, non-idling control policy — the strongest policy-independent notion of stability a network can have. At the fluid-model level (Definition 8.23, restricting to single-server stations, $b \equiv 1$ ), this becomes: every solution of the fluid equations (8.20)-(8.23) plus the non-idling condition (8.42) is driven to the origin, uniformly in its starting size. A unidirectional ring network routes each customer type through a fixed cyclic sequence of stations; a two-station, five-class re-entrant line (Figure 8.3) routes its single input stream through five classes in a fixed order, alternating between two stations.

Formalization targets

Goal: Theorem 8.25 — the Rybko–Stolyar-style boundary for a re-entrant line

The two-station, five-class re-entrant network's fluid model is globally stable if and only if

\lambda_1(m_1+m_3+m_5) < 1, \qquad \lambda_1(m_2+m_4) < 1, \qquad \lambda_1(m_2+m_5) < 1.

The first two conditions together are the standard load condition; the third is a genuinely new "virtual station condition," the direct analogue of the Rybko–Stolyar network's own extra requirement. This is the weakest possible target for the phenomenon it captures: a two-sided iff, so it cannot be strengthened by dropping either the necessity or the sufficiency direction, and it isolates the exact extra condition rather than a merely sufficient one.

Supporting milestones

Lemma 8.20 (restated from mission VI, since this chunk's page range overlaps mission VI's at page 164) is a general departure-rate extinction criterion. Theorem 8.21 proves stability of an "assembly with complementary side business" network via a first two-dimensional piecewise-linear Lyapunov function. Theorem 8.24 shows unidirectional ring networks are globally stable throughout their entire subcritical region — no extra condition needed, in sharp contrast to the goal theorem's network. Lemma 8.26 gives four algebraic sufficient conditions for the workload derivative inequalities the goal theorem's Lyapunov argument needs; Lemma 8.27 shows these conditions are simultaneously satisfiable exactly when (8.47)-(8.49) hold — the geometric core of the sufficiency direction.

Significance

The result itself. Theorem 8.25 is the book's own fully worked instance of the field's most cited stability-boundary phenomenon: it pins down, for a specific and analyzable network, exactly how much more than subcriticality is required, and shows the extra requirement (8.49) is not an artifact of the proof technique but a genuine necessary condition, via an explicit unstable sample path under the "extreme" priority policy that violates it. Theorem 8.24, by contrast, demonstrates that the ring topology is not automatically pathological in this way, delineating the boundary from the other side.

Formalizing it. Searches for "re-entrant line," "Rybko-Stolyar," and "virtual station" (q=re-entrant%20line, q=Rybko-Stolyar, q=virtual%20station) return no results specific to this material; this mission is a from-scratch formalization of global stability at both the Markov-chain and fluid-model tiers, unidirectional ring networks, the two-station five-class re-entrant line, and the assembly-with-side-business network.

Difficulty

Theorem 8.25's necessity direction needs an entirely different proof technique from its sufficiency direction: rather than a Lyapunov argument, it requires exhibiting an explicit unstable fluid model solution under a specific "extreme" static-buffer-priority policy — a sample-path construction, echoing the divergent-cycle construction mission III's own chapter (Section 6.2) gives for the original Rybko–Stolyar network, that the book itself says is "omitted" as analogous. A formalization that stated only the sufficiency direction (dropping the "only if") would misrepresent the theorem entirely, since sufficiency alone is not what makes this result the field's canonical boundary-of-stability statement. A second difficulty is genuinely geometric: Lemma 8.27's proof intersects a parallelogram of admissible $(x_2,x_4)$ pairs with a wedge region, then separately solves an analogous system for $(x_1,x_3,x_5)$ — reducing a five-dimensional existence claim to two two-dimensional geometric arguments, each depending on (8.47)-(8.49) in a way that is not visible from the inequalities' surface form alone.

Formalization scope

Missions IV/VI's queueing-network model data, fluid-equation specialization, and workload operator are restated locally (drafts in this series do not import one another), as is mission VI's non-idling fluid model (renamed to track Definition 8.23's own name, FluidModelGloballyStable, even though defeq in shape). Definition 8.22 (network-level global stability) is stated abstractly over an uninterpreted policy type and two predicates, since the concrete "simply structured non-idling policy" and "positive recurrence under a policy" notions belong to mission I's apparatus, not a dependency of this chunk. The unidirectional ring network is characterized as a structural property of an ordinary flat-indexed queueing network (a partial successor function encoding the deterministic route) rather than by re-introducing the book's own two-index type/stage bookkeeping — a faithful re-encoding, since every ring network in the book's sense is representable this way. The re-entrant line's routing (station 1 serves classes 1,3,5; station 2 serves classes 2,4) was recovered from the explicit computations in Lemma 8.26's own proof, not read off Figure 8.3 directly, though the two are cross-checked as consistent. The assembly-with-side-business network, which needs a genuinely multi-input activity outside Chapter 2's "unitary network" vocabulary, is packaged directly via its already-derived fluid equations (8.36)-(8.39) rather than a general SPN activity structure. Theorem 8.25 is stated as a bare ↔, exposing neither the sufficiency direction's Lyapunov witnesses nor the necessity direction's instability construction — a formalization that dropped either direction of the iff, or that conflated the unidirectional ring's cyclic structure with an unrestricted deterministic routing graph, would each be an unfaithful weakening. IsGloballyStable, FluidModelGloballyStable, IsUnidirectionalRing, and the re-entrant line's Lyapunov ingredients (reentrantG1/reentrantG2/ reentrantH1/reentrantH2) are the primary reusable contributions; contributions completing the six by sorry proofs — Theorem 8.25's necessity direction in particular, which needs machinery this mission does not otherwise build — are welcome.

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.
J. G. Dai and J. H. Vande Vate, "The stability of two-station multitype fluid networks," Operations Research 48 (2000), 721–744.

13 thms2 active usersReviewed

Discrete Geometry Linear Optimization Number Theory+2·Captain: mikedeng1

Maximal Lattice-Free Convex Sets in Linear Subspaces I: Characterization of Maximal Lattice-Free Convex Sets in a SubspaceResearch Paper

Motivation

Cutting planes for mixed-integer linear programs are often derived from convex sets that contain no integer point in their interior. Balas observed in 1971 that every such lattice-free convex set containing the current fractional LP solution in its interior yields a valid inequality, the intersection cut (Balas, Intersection cuts, Oper. Res. 19, 1971). The strongest cuts come from sets that are inclusionwise maximal, so the shape of maximal lattice-free convex sets matters to multi-row cut generation.

The case where the set lives in a subspace arises in practice. Taking $q$ rows of an optimal simplex tableau restricts the integer points to an affine subspace $f+W$ of $\mathbb R^q$ spanned by the tableau columns. When $W$ is irrational, its integer points span only a proper subspace $V\subsetneq W$ . The classical theory does not cover this case, and it is the case that the second mission of this series (minimal valid inequalities of the relaxation $R_f(W)$ ) needs.

Timeline.

Lovász (Geometry of numbers and integer programming, 1989) stated the characterization for rational subspaces (Proposition 3.1) and gave only a sketch of the proof. The irrational-hyperplane case is not visible in that sketch.
Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543v1; Math. Oper. Res. 35(3), 2010, doi:10.1287/moor.1100.0461) gave a complete proof of Lovász's theorem for an arbitrary lattice of a linear space (Theorem 10). They also extended it to a space $W$ strictly larger than the span $V$ of the lattice (Theorem 9, equivalently Theorem 1 for $\mathbb Z^n$ ).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product and the open balls $B_\varepsilon(x)$ . For $X\subseteq\mathbb R^n$ , $\langle X\rangle$ denotes its linear span.

A lattice of a linear space $V$ is an additive group $\Lambda=\{\lambda_1a_1+\dots+\lambda_ma_m\mid\lambda_i\in\mathbb Z\}$ generated by linearly independent vectors $a_1,\dots,a_m$ with $\langle a_1,\dots,a_m\rangle=V$ (Definition 6, IsLatticeOf Λ V). A linear subspace $L\subseteq V$ is a $\Lambda$ -subspace if it has a basis contained in $\Lambda$ (Definition 7, IsLambdaSubspace Λ V L). For $\mathbb Z^2$ , the line $x_2=2x_1$ is a $\Lambda$ -subspace and the line $x_2=\sqrt2x_1$ is not.

For sets $W,S$ the interior relative to $W$ is $\mathbf{int}_W(S)=\{x\in S\mid B_\varepsilon(x)\cap W\subseteq S\text{ for some }\varepsilon>0\}$ (intW W S). The relative interior is $\mathbf{relint}(S)=\mathbf{int}_{\operatorname{aff}(S)}(S)$ .

Let $W\supseteq V$ be a linear space. A set $S$ is a $\Lambda$ -free convex set of $W$ if $S\subseteq W$ , $S$ is convex and $\Lambda\cap\mathbf{int}_W(S)=\emptyset$ . It is maximal if no other $\Lambda$ -free convex set of $W$ properly contains it (Definition 8, IsLambdaFree, IsMaxLambdaFree).

The statements also use a polyhedron in $W$ ( $W$ intersected with finitely many closed half-spaces), a polytope (convex hull of a finite set), the dimension $\dim(S)$ of the affine hull with $\dim\emptyset=-1$ (affDim), and a facet: a nonempty face $S\cap\{\langle a,x\rangle=b\}$ of a valid inequality with $\dim F=\dim S-1$ . The recession cone is $\operatorname{rec}(S)=\{r\mid x+tr\in S\ \forall x\in S,\ t\ge0\}$ and the lineality space is $\operatorname{rec}(S)\cap-\operatorname{rec}(S)$ .

Formalization targets

Goal: Theorem 9 (p. 8)

For a lattice $\Lambda$ of $V$ and a linear space $W\supseteq V$ with $\dim W\ge1$ , a set $S$ is a maximal $\Lambda$ -free convex set of $W$ if and only if

\text{(i) } S \text{ is a full-dimensional polyhedron in } W,\ S\cap V \text{ is maximal } \Lambda\text{-free in } V,\ F\mapsto F\cap V \text{ is a bijection of facets};

\text{(ii) } S=v+L \text{ is a hyperplane of } W \text{ with } L\cap V \text{ a hyperplane of } V \text{ that is not a } \Lambda\text{-subspace};

\text{(iii) } S \text{ is a half-space of } W \text{ containing } V \text{ on its boundary.}

Main milestone: Theorem 10 (p. 8)

For $\dim V\ge1$ , $S$ is a maximal $\Lambda$ -free convex set of $V$ if and only if either $S=P+L$ is a polyhedron with $P$ a polytope, $L$ a $\Lambda$ -subspace and $\dim S=\dim P+\dim L=\dim V$ , with no lattice point in $\mathbf{int}_V(S)$ and a lattice point in the relative interior of every facet; or $S=v+L$ is an affine hyperplane of $V$ whose direction $L$ is not a $\Lambda$ -subspace.

Supporting milestones

Lemma 13 (bounded full-dimensional case), Lemma 15 (lattice points near half-lines), Lemma 16 ( $S+\langle\operatorname{rec}S\rangle$ stays $\Lambda$ -free), Lemma 17 (projection along a $\Lambda$ -subspace is a lattice), Lemma 18 (lattice points near non-lattice subspaces), Lemma 19 (maximal hyperplanes), Claims 1 and 2 in the proof of Theorem 10, and identity (6), $\mathbf{int}_W(S)\cap V=\mathbf{int}_V(S\cap V)$ .

Significance

Theorem 10 says that maximal lattice-free sets are cylinders over polytopes with a lattice point on every facet, apart from the irrational hyperplanes. This is the structural fact behind the finiteness of facet counts (at most $2^{\dim P}$ ) and behind every classification of maximal lattice-free sets in low dimension, such as the triangles and quadrilaterals of the two-row relaxation. Theorem 9 extends it to irrational subspaces. There the new cases are the half-spaces of (iii), which have $V$ on their boundary, and the hyperplanes of (ii), whose trace on $V$ is a hyperplane of $V$ that is not a $\Lambda$ -subspace. Theorem 9 is the geometric input to the paper's Theorem 3: every minimal valid inequality of $R_f(W)$ is the gauge of a maximal lattice-free convex set of $f+W$ .

These results are proved on paper. No machine-checked version of Lovász's theorem, of Theorem 9, or of the lattice-approximation Lemmas 15 and 18 is known to exist. The mission produces the definitions of lattices of subspaces, relative interiors and lattice-free sets on which the second mission of the series builds.

Difficulty

The obvious argument separates each lattice point from $S$ by a half-space and intersects the half-spaces. It gives a polyhedron only when finitely many lattice points matter, that is, when $S$ is bounded. For unbounded $S$ , the recession directions must be shown to be lineality directions and to be spanned by lattice vectors. Both steps rest on simultaneous Diophantine approximation (Dirichlet's theorem) applied in irrational directions, and on a density argument for the projected lattice when the lineality space is not a $\Lambda$ -subspace. In the subspace setting of Theorem 9, one must also track the interiors relative to $W$ and to $V$ separately. Identity (6) holds only when $\mathbf{int}_W(S)$ meets $V$ , and the half-space case (iii) is exactly the case where it does not.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), linear spaces are Submodule ℝ, and $\Lambda$ is an AddSubgroup. All declarations live in the namespace MaxLatticeFree.Geometry. Every interior is relative (intW, relint). With the ambient topological interior, every subset of a proper subspace would be trivially lattice-free, and the classification would collapse. A lattice must have a linearly independent generating family; a dense finitely generated subgroup such as $\mathbb Z+\sqrt2\mathbb Z$ is excluded. Dimensions are integers with $\dim\emptyset=-1$ , and facets are nonempty, so no dimension equation holds through truncated subtraction.

Two readings of the page are fixed.

Theorem 9 assumes $\dim W\ge1$ and Theorem 10 assumes $\dim V\ge1$ . For $W=V=\{0\}$ the only maximal set is $\emptyset$ , which satisfies none of the listed cases, so the printed statements are false there.
Identity (6) is stated under the three hypotheses its proof uses, not inside the case analysis of Theorem 9.

The paper's Theorem 1 (the same result for $\mathbb Z^n$ and affine $W$ ) is not included, and neither are the cited results of Barvinok and Dirichlet (Theorems 11, 14, Corollary 12). They are welcome as supporting lemmas. Infrastructure that is useful beyond this mission includes Dirichlet's simultaneous approximation theorem in $\mathbb R^m$ , discreteness of lattices of subspaces, and the relation between intW/relint and Mathlib's intrinsicInterior.

Selected references

A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543
L. Lovász, Geometry of numbers and integer programming, in: Mathematical Programming: Recent Developments and Applications, 1989, pp. 177–210.
E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
A. Barvinok, A Course in Convexity, Graduate Studies in Mathematics 54, AMS, 2002. https://doi.org/10.1090/gsm/054

18 thms2 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks VIII: Maximal Stability of Back-Pressure ControlTextbook

Motivation

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

Setting

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

Formalization targets

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

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

Supporting milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

14 thms3 active usersReviewed

Completed

Algorithmic Game Theory Linear Optimization Operations Research·Captain: mikedeng1

The Assignment Game I: The Core 1: The Core Is the Set of Optimal Solutions of the Dual Assignment LPResearch Paper

Motivation

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

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

Setting

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

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

v(S) = \max_{P} \sum_{(i,j) \in P} a_{ij},

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

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

\sum_{i\in M} u_i + \sum_{j \in N} v_j = v(M \cup N) \quad (3.5), \qquad \sum_{i\in S\cap M} u_i + \sum_{j \in S\cap N} v_j \ge v(S)\ \text{ for all } S \quad (3.6).

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

Formalization targets

Goal: Theorem 2 (p. 118)

\operatorname{core}(a) = \{(u,v) : (u,v) \text{ is an optimal solution of the dual LP (3.3)–(3.4)}\}.

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

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

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

Further results on the same definitions

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

Selected references

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

6 thms3 active usersReviewed

Completed

Discrete Geometry Linear Optimization Operations Research+1·Captain: mikedeng1

Maximal Lattice-Free Convex Sets in Linear Subspaces II: Minimal Valid Inequalities Come from Maximal Lattice-Free Convex SetsResearch Paper

Cutting planes from lattice-free convex sets

Cutting planes for mixed-integer linear programs are often derived from a few rows of an optimal simplex tableau. Keeping $q$ rows for basic integer variables $x_1,\dots,x_q$ , dropping the nonnegativity of $x$ (Gomory's corner polyhedron, Gomory 1969) and then the integrality of the nonbasic variables leaves the set of $s\ge0$ with $f+\sum_j r^js_j\in\mathbb Z^q$ . Balas observed in 1971 that convex sets with no integral point in their interior give valid inequalities for such sets (Balas 1971). Andersen, Louveaux, Weismantel and Wolsey (2007) for two rows, and Borozan and Cornuéjols (2009) for any number of rows, showed that for rational data the irredundant valid inequalities correspond to maximal lattice-free convex sets. Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543; Math. Oper. Res. 35(3), 2010) removed the rationality assumption. This mission formalizes that result, Theorem 3 of their paper.

Setting

Fix $q\ge0$ , a point $f\in\mathbb R^q$ and a linear subspace $W\subseteq\mathbb R^q$ , and assume that the affine space $f+W$ contains an integral point. Products such as $ry$ are standard inner products.

$\mathcal W$ is the space of real functions $s=(s_r)_{r\in W}$ with finite support. The semi-infinite relaxation is

R_f(W)=\Big\{s\in\mathcal W \ \Big|\ f+\sum_{r\in W}rs_r\in\mathbb Z^q,\ s_r\ge0\ (r\in W)\Big\}.

A linear inequality is a pair $(\psi,\alpha)$ with $\psi:W\to\mathbb R$ an arbitrary function and $\alpha\in\mathbb R$ , read as $\Psi(s)=\sum_{r\in W}\psi(r)s_r\ge\alpha$ . It is valid if every $s\in R_f(W)$ satisfies it.
$V$ is the affine hull of $(f+W)\cap\mathbb Z^q$ , and $\mathcal V=\{s\in\mathcal W\mid f+\sum_r rs_r\in V\}$ . A linear inequality is trivial if every $s\in\mathcal V$ with $s\ge0$ satisfies it. When $W$ is irrational (not spanned by the integral points it contains, up to translation), $V$ is a proper affine subspace of $f+W$ .
$\sum\psi(r)s_r\ge\alpha$ dominates $\sum\psi'(r)s_r\ge\alpha$ if $\psi\le\psi'$ pointwise. A valid inequality is minimal if no valid inequality with the same $\alpha$ and a different $\psi'\le\psi$ exists.
Choose $C\in\mathbb R^{\ell\times q}$ and $d\in\mathbb R^\ell$ with $V=\{x\in f+W\mid Cx=d\}$ . Two valid inequalities are equivalent if $\psi(r)=\rho\psi'(r)+\lambda^TCr$ for all $r\in W$ and $\alpha=\rho\alpha'+\lambda^T(d-Cf)$ , for some $\rho>0$ , $\lambda\in\mathbb R^\ell$ .
A maximal lattice-free convex set in $f+W$ is a convex $B\subseteq f+W$ with no integral point in its interior relative to $f+W$ , inclusionwise maximal with these properties.
For $K\subseteq W$ closed, convex, with $0$ in its interior relative to $W$ : the polar $K^*=\{y\in W\mid ry\le1\ \forall r\in K\}$ , $\hat K=\{y\in K^*\mid\exists x\in K,\ xy=1\}$ , and $\rho_K(r)=\sup_{y\in\hat K}ry$ . For such a $B$ with $f$ in its interior, $\psi_B=\rho_{B-f}$ ; for a polyhedral $B=\{x\in f+W\mid a_i(x-f)\le1\}$ with tight rows this is $\psi_B(r)=\max_ia_ir$ .

A function $\sigma:W\to\mathbb R$ is sublinear if $\sigma(\lambda r)=\lambda\sigma(r)$ for $\lambda\ge0$ and $\sigma(r+r')\le\sigma(r)+\sigma(r')$ .

Formalization targets

Goal: Theorem 3 (p. 6)

Every nontrivial valid linear inequality for $R_f(W)$ is dominated by a nontrivial minimal valid linear inequality for $R_f(W)$ .
Every nontrivial minimal valid linear inequality for $R_f(W)$ is equivalent to one of the form

\sum_{r\in W}\psi_B(r)s_r\ \ge\ 1

with $\psi_B\ge0$ on $W$ and $B$ a maximal lattice-free convex set in $f+W$ with $f$ in its interior.

The goal is stated as one conjunction. It fixes no constants and makes no rationality assumption on $f$ or $W$ .

Milestones

In the order in which the proof on pp. 15–21 uses them:

Lemma 23 (a sublinear valid inequality below any valid one)
Lemma 26 (invariance under equivalence)
Claims 1 and 2 in the proof of Theorem 3
Theorem 28 (Basu–Cornuéjols–Zambelli: $\rho_K$ is the smallest sublinear function with $1$ -sublevel set $K$ )
Remark 30 and Claim 4 (the inequality $\sum\rho_K(r)s_r\ge1$ )
Remark 29 ( $\rho_K=\max_ia_ir$ for tight rows)
Claim 6 (a shift by $\lambda^TC$ making $\psi$ nonnegative)
Claim 7 ( $\psi_B$ below a nonnegative sublinear $\psi''$ )
Lemma 31 (maximal lattice-free sets give minimal inequalities)

Significance

Theorem 3 says that the minimal valid inequalities of $R_f(W)$ are exactly those produced by maximal lattice-free convex sets, up to the equivalence forced by the affine hull $\mathcal V$ . It also says that for irrational $W$ , where valid inequalities can have negative coefficients, some equivalent form always has nonnegative coefficients. The paper derives two further results from it: a description of the closure of $\operatorname{conv}(R_f(W))$ in a suitable norm (Theorem 4), and a reduction of extreme inequalities of the infinite model to finite ones (Theorem 5). Both results remain unproved without it.

The result has a complete proof in the paper, which relies on the cited Theorem 28 from Basu, Cornuéjols, Zambelli. To our knowledge none of it is machine-checked. A formalization would provide a definitional layer for corner relaxations, lattice-free sets and valid inequalities, which is currently absent from Mathlib. It would also expose where the page is imprecise; see the scope section.

Difficulty

For rational data every valid inequality can be written with right-hand side $1$ and nonnegative coefficients, and $\psi$ is then the gauge of $B_\psi$ . For irrational $W$ this fails. Since $R_f(W)\subseteq\mathcal V$ , adding $\lambda^TCr$ to $\psi$ changes nothing on $R_f(W)$ , so coefficients can be negative, and $B_\psi=\{x\in f+W\mid\psi(x-f)\le\alpha\}$ may have a full-dimensional recession cone. A maximal lattice-free set containing $B_\psi$ then yields a $\psi_B$ that need not lie below $\psi$ (the example on pp. 21–22 shows this). One must first pass to an equivalent inequality whose set has no full-dimensional recession cone within $V$ . This step combines the structure theorem for maximal lattice-free sets in irrational subspaces (Theorem 9 of the paper) with a duality argument. A second obstacle is that $\psi$ is an arbitrary function: validity alone gives no convexity or continuity, and Lemma 23 is needed to recover them.

Formalization scope

Ambient space. $\mathbb R^q$ is EuclideanSpace ℝ (Fin q), $W$ is a Submodule, and $\mathcal W$ is W →₀ ℝ. The printed phrase "the set $\{r\mid s_r>0\}$ has finite cardinality" is read as ordinary finite support.
Standing hypothesis. Every statement assumes that $f+W$ contains an integral point. Without it $R_f(W)=\emptyset$ and every inequality is valid, so this hypothesis rules out the trivializing formalization. The equivalence predicate carries the hypothesis $V=\{x\in f+W\mid Cx=d\}$ together with validity of both inequalities. With $C,d$ unconstrained, equivalence would be rescaling only, and part 2 of the goal would be false for irrational $W$ .
Interiors. All interiors are relative: to $f+W$ for $B$ and $B_\psi$ , to $W$ for $K$ .
$\psi_B$ . It is defined as $\rho_{B-f}$ , independent of any description of $B$ .

The paper is imprecise in three places, and the formalization departs from the page in each:

Remark 29 is false without tight rows: for $K=(-\infty,1]\subseteq\mathbb R$ written with $a_1=1$ , $a_2=1/2$ , $\rho_K(r)=r\ne\max(r,r/2)$ for $r<0$ . It is stated with the tightness the paper arranges before using it.
The identity $\operatorname{int}(B_\psi)=\{x\mid\psi(x-f)<\alpha\}$ on p. 17 fails at $\alpha=0$ , for example for $\psi\equiv0$ . Claims 1 and 2 use the strict sublevel set, and Claim 2 is false for the topological interior.
Claims 5 and 7 invoke Corollary 20 in $f+W$ , although it is proved only for a lattice of a linear space. Corollary 20 and Claim 5 are therefore not milestones.

Two kinds of contributions are especially welcome: reusable infrastructure for polars of convex sets relative to a subspace and for sublinear functions on submodules, and a proof of Theorem 28.

Selected references

A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543v1
A. Basu, G. Cornuéjols, G. Zambelli, Convex sets and minimal sublinear functions, J. Convex Anal. 18(2), 2011 (reference [9]).
V. Borozan, G. Cornuéjols, Minimal valid inequalities for integer constraints, Math. Oper. Res. 34(3), 2009. https://doi.org/10.1287/moor.1090.0400
K. Andersen, Q. Louveaux, R. Weismantel, L. Wolsey, Inequalities from two rows of a simplex tableau, IPCO 2007. https://doi.org/10.1007/978-3-540-72792-7_1
E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra Appl. 2, 1969. https://doi.org/10.1016/0024-3795(69)90017-2

16 thms2 active usersReviewed

Completed

Algorithmic Game Theory Linear Optimization Operations Research·Captain: mikedeng1

The Assignment Game I: The Core 2: The High-Price and Low-Price Corners of the CoreResearch Paper

Motivation

A two-sided market in which each seller owns one indivisible good (a house, in the paper's example) and each buyer wants at most one is the simplest model in which prices emerge from bargaining between individuals rather than from a supply curve. Shapley and Shubik, The Assignment Game I: The Core (Int. J. Game Theory 1 (1971)), treat this market as a cooperative game with transferable utility and describe its core, the set of payoff divisions that no group of traders can improve upon by trading among themselves. The paper is the foundation of the literature on assignment markets, auctions of heterogeneous items, and two-sided matching with money.

This mission formalizes the paper's structural result on the shape of the core, Theorem 3 (p. 121): among all core outcomes there is a high-price corner in which every seller simultaneously receives the highest payoff available in the core and every buyer the lowest, and a low-price corner with the roles reversed; these two corners are the farthest-apart pair of core points. The authors note (p. 121, footnote 2) that a similar theorem for markets without money is proved by Gale and Shapley (1962), where it becomes the existence of seller-optimal and buyer-optimal stable matchings.

Setting

Let $M$ be a finite set of sellers and $N$ a finite set of buyers, with $m = |M|$ and $n = |N|$ not necessarily equal. For each seller $i$ and buyer $j$ a number $a_{ij} \ge 0$ is given: the gain the pair can realize by trading (Eq. (2.5), p. 114; Sec. 2.3, p. 116).

A coalition $S \subseteq M \cup N$ is described by its seller part $A = S \cap M$ and buyer part $B = S \cap N$ . A matching inside $(A, B)$ is a set $P \subseteq A \times B$ of seller–buyer pairs in which no player occurs twice. The characteristic function (Eq. (2.6), p. 115) gives the coalition the best total gain it can realize by pairing its members:

\operatorname{worth}(A, B) = \max_{P \text{ matching in } (A,B)} \sum_{(i,j) \in P} a_{ij}.

A matching of the whole market attaining $\operatorname{worth}(M, N)$ is an optimal assignment.

A payoff vector is a pair $(u, v)$ with $u \in \mathbb{R}^M$ (sellers' payoffs) and $v \in \mathbb{R}^N$ (buyers' payoffs). The core (p. 118) consists of the payoff vectors with

\sum_{i \in M} u_i + \sum_{j \in N} v_j = \operatorname{worth}(M, N) \quad (3.5), \qquad \sum_{i \in A} u_i + \sum_{j \in B} v_j \ge \operatorname{worth}(A, B) \ \text{ for all } A \subseteq M,\ B \subseteq N \quad (3.6).

Singleton coalitions have worth $0$ , so core vectors are nonnegative; the paper calls them "imputations in the core".

For a seller $i$ , write $u^*_i$ and $u_{*i}$ for the highest and lowest value of $u_i$ over the core; for a buyer $j$ , write $v^*_j$ and $v_{*j}$ likewise.

Formalization targets

Goal: Theorem 3 (p. 121)

The low-price corner $(u_*, v^*)$ and the high-price corner $(u^*, v_*)$ are in the core, and for all core vectors $(u', v')$ , $(u'', v'')$ ,

\sum_{i \in M} (u'_i - u''_i)^2 + \sum_{j \in N} (v'_j - v''_j)^2 \le \sum_{i \in M} (u_{*i} - u^*_i)^2 + \sum_{j \in N} (v^*_j - v_{*j})^2 .

Milestones, in attack order

Sec. 3.2, p. 118 — the core is nonempty.
Sec. 3.3, p. 120 — the core is closed, convex and bounded (a polytope).
Sec. 3.3, proof of the Lemma, p. 121 — on an optimal assignment $P$ , every core vector has $u_i + v_j = a_{ij}$ for $(i, j) \in P$ and pays $0$ to players $P$ leaves unassigned.
Lemma, p. 121 — for core vectors $(u', v')$ , $(u'', v'')$ , the vectors $(\min(u', u''), \max(v', v''))$ and $(\max(u', u''), \min(v', v''))$ (coordinatewise) are in the core.
Sec. 3.3, p. 122 — any two core vectors satisfy $|u'_i - u''_i| \le u^*_i - u_{*i}$ and $|v'_j - v''_j| \le v^*_j - v_{*j}$ for every $i$ and $j$ .

Milestone 5 is the strongest form of the distance clause of the goal: it gives the same conclusion for every distance that depends only on the absolute values of the coordinate differences, as the paper remarks on p. 122.

Significance

The result. Theorem 3 says that the core of an assignment market is elongated along the direction of market-wide price movements: "intergroup allocations are relatively indeterminate, intragroup allocations are relatively precise" (p. 121). The high-price corner is the outcome most favourable to all sellers at once, and the low-price corner the one most favourable to all buyers; that such simultaneous optima exist is a property of this game, not of cores in general. The low-price corner, the buyers' optimum, is the outcome reached by the ascending multi-item auction of Demange, Gale and Sotomayor (J. Polit. Econ. 94 (1986)), and the lattice structure underlies the incentive analysis of assignment mechanisms.

Formalizing it. The theorem is classical and fully proved in the paper; Prove2Me has no formalization of it, and nothing on the platform treats transferable-utility assignment games (the platform's stable-matching material concerns the non-transferable-utility model). The mission produces a reusable definition of the assignment game and its core, the lattice property of the core, and the extremal-corner theorem, stated with the core's extrema defined intrinsically rather than as parameters.

Difficulty

The proof in the paper takes a finite family of core vectors realizing all the extremal values and applies the Lemma repeatedly (p. 122). That argument presupposes that each extremum $u^*_i$ , $u_{*i}$ , $v^*_j$ , $v_{*j}$ is attained by some core vector, which the paper takes from the core being a nonempty polytope without stating it separately. Nonemptiness is itself the substantive result of the paper's linear-programming analysis (Theorem 2, via the duality theorem and the integrality of the assignment polytope), and it is not available here as a black box. The other nontrivial point is the Lemma's efficiency claim: that the coordinatewise min/max vectors still distribute exactly $\operatorname{worth}(M, N)$ , which depends on the structure of an optimal assignment and fails for the naive combination $(\max(u', u''), \max(v', v''))$ .

Formalization scope

Players and matrix. $M$ and $N$ are arbitrary finite types (Fintype); either may be empty and $m \ne n$ is allowed. The matrix is a : M → N → ℝ, and every theorem carries the paper's standing assumption $a_{ij} \ge 0$ as a hypothesis. No other hypothesis is added.
Coalitions are pairs (A, B) : Finset M × Finset N. Matchings are finsets of pairs with injective projections. The paper maximizes over exactly $k = \min(|S \cap M|, |S \cap N|)$ disjoint pairs; the formalization maximizes over matchings of every size, which gives the same value because $a_{ij} \ge 0$ .
Naming. The characteristic function is worth, since v denotes buyers' payoffs.
Core is a Set ((M → ℝ) × (N → ℝ)) defined by (3.5) and (3.6) over all coalitions, with no separate nonnegativity clause (it follows from singleton coalitions).
Extremal payoffs uHi, uLo, vHi, vLo are sSup/sInf in ℝ of the image of the core under a coordinate. On an empty or unbounded set these return $0$ ; the goal does not assume the core nonempty or bounded, so it is not vacuous and does not hide milestones 1–2 as hypotheses. The goal's membership clauses imply attainment of the extrema.
Distance. The goal uses the Euclidean distance on $\mathbb{R}^M \times \mathbb{R}^N$ through sums of squared coordinate differences. Lean's default dist on a product of function types is the sup-distance and is not used.
Ruled out. A formalization in which $u^*, u_*, v^*, v_*$ are free parameters constrained only by the conclusion, or in which the goal assumes a nonempty bounded core, would trivialize or weaken Theorem 3; the extrema here are computed from the core.
Not formalized. The dimension statements of p. 120 ("typically equal to min(m,n)") are informal. The LP characterization of the core (Theorem 2) is the subject of the companion mission of this series and is not restated.
Welcome contributions. Lemmas about matchings inside coalitions (injectivity, sums over images), the implication "dual feasible $\Rightarrow$ coalitionally rational", and general facts about sSup/sInf of compact coordinate images are reusable for any assignment-market or TU-matching development.

Selected references

L. S. Shapley and M. Shubik, The Assignment Game I: The Core, International Journal of Game Theory 1 (1971), 111–130. https://doi.org/10.1007/BF01753437
D. Gale and L. S. Shapley, College Admissions and the Stability of Marriage, American Mathematical Monthly 69 (1962), 9–15. https://doi.org/10.2307/2312726
G. Demange, D. Gale and M. Sotomayor, Multi-Item Auctions, Journal of Political Economy 94 (1986), 863–872. https://doi.org/10.1086/261393
G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963. https://doi.org/10.1515/9781400884179

7 thms4 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks IX: Fluid Stability of the Proportionally Fair AllocationTextbook

Motivation

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

Setting

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

Formalization targets

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

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

Supporting milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

12 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Optimization+1·Captain: mikedeng1

Robust solutions of Linear Programming problems contaminated with uncertain data: A Violation-Probability Bound for the Robust CounterpartResearch Paper

Motivation

Linear programs solved in practice carry data that are measured, estimated or rounded. Ben-Tal and Nemirovski (Math. Program. 88, 2000) examined the NETLIB collection of real-world LPs and found that in 13 of them a relative perturbation of only 0.01% in the "ugly" coefficients of the inequality constraints can make the nominal optimal solution more than 50% infeasible (§2.3). Their remedy is the robust counterpart methodology: replace the nominal problem by a deterministic problem whose feasible solutions remain nearly feasible for every, or for all but a small probability of, data realizations.

The paper made the approach concrete for entry-wise uncertainty and gave the probabilistic guarantee that became a standard tool of robust and chance-constrained optimization. The main steps of the history are:

1973, A. L. Soyster: the interval (worst-case, "box") counterpart, here called (IRC).
1998–1999, Ben-Tal and Nemirovski (Math. Oper. Res. 23; Oper. Res. Lett. 25), and independently El Ghaoui and co-authors: robust optimization with ellipsoidal uncertainty sets.
2000, this paper: the ellipsoid-plus-box counterpart (RC[ε, δ, Ω]) and Proposition 1, which bounds each constraint's violation probability by $\exp\{-\Omega^2/2\}$ under independent symmetric perturbations.
2004, Bertsimas and Sim (Oper. Res. 52): the budgeted counterpart, with an analogous probability bound.

Setting

An uncertain linear program is

\text{minimize } c^Tx\quad\text{s.t.}\quad Ex=e,\qquad Ax\le b,\qquad \ell\le x\le u,\tag{LP}

with $x\in\mathbb{R}^n$ , $E\in\mathbb{R}^{p\times n}$ , $A=(a_{ij})\in\mathbb{R}^{m\times n}$ , and bounds $\ell_j\in\mathbb{R}\cup\{-\infty\}$ , $u_j\in\mathbb{R}\cup\{+\infty\}$ . For each inequality row $i$ a set $J_i\subseteq\{1,\dots,n\}$ lists the uncertain entries $a_{ij}$ , $j\in J_i$ . Only these entries are uncertain; $E,e,b,\ell,u,c$ are exact.

Given an uncertainty level $\epsilon>0$ and a feasibility tolerance $\delta>0$ , write $b_i^+=b_i+\delta\max[1,|b_i|]$ .

$x$ is reliable if it is feasible for (LP) and $\sum_{j\notin J_i}a_{ij}x_j+\sum_{j\in J_i}\tilde a_{ij}x_j\le b_i^+$ for every $i$ and every choice of $\tilde a_{ij}$ with $|\tilde a_{ij}-a_{ij}|\le\epsilon|a_{ij}|$ .
In the random symmetric uncertainty model, the true coefficients are $\tilde a_{ij}=(1+\epsilon\xi_{ij})a_{ij}$ , where $\xi_{ij}=0$ for $j\notin J_i$ and, for each row $i$ , $\{\xi_{ij}\}_{j\in J_i}$ are independent random variables, each symmetrically distributed in $[-1,1]$ .
$x$ is almost reliable with level $\kappa$ if it is feasible for (LP) and $\Pr\{\sum_j\tilde a_{ij}x_j>b_i^+\}\le\kappa$ for every $i$ .

The robust counterpart (RC[ε, δ, Ω]), with a safety parameter $\Omega>0$ , has variables $x_j$ , $y_{ij}$ , $z_{ij}$ and constraints $Ex=e$ , $Ax\le b$ , $\ell\le x\le u$ , $-y_{ij}\le x_j-z_{ij}\le y_{ij}$ for all $i,j$ , and

\sum_j a_{ij}x_j+\epsilon\Big[\sum_{j\in J_i}|a_{ij}|y_{ij}+\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2z_{ij}^2}\Big]\le b_i^+\qquad\forall i.

The interval robust counterpart (IRC[ε, δ]) has variables $x_j,y_j$ and the constraint $\sum_ja_{ij}x_j+\epsilon\sum_{j\in J_i}|a_{ij}|y_j\le b_i^+$ with $-y_j\le x_j\le y_j$ , besides the nominal ones. Problem (∗) is the same with $y_j$ replaced by $|x_j|$ .

Formalization targets

Goal: Proposition 1 (pp. 418–419)

If $x$ extends to a feasible solution $(x,y,z)$ of (RC[ε, δ, Ω]), then $x$ is feasible for (LP) and, for every $i$ ,

\Pr\Big\{\sum_j(1+\epsilon\xi_{ij})a_{ij}x_j>b_i+\delta\max[1,|b_i|]\Big\}\le\exp\{-\Omega^2/2\}.

Milestones

The reduction in the proof of Proposition 1 (p. 419), in corrected pointwise form: a violation of row $i$ forces $\sum_{j\in J_i}\xi_{ij}a_{ij}z_{ij}>\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2z_{ij}^2}$ .
Eq. (1), p. 419: for independent symmetric $\eta_j\in[-1,1]$ and reals $p_j$ ,

\Pr\Big\{\sum_j\eta_jp_j>\Omega\sqrt{\textstyle\sum_jp_j^2}\Big\}\le\exp\{-\Omega^2/2\}.

$x$ is reliable iff it is feasible for (∗) (p. 417).
(∗) is equivalent to (IRC[ε, δ]) (pp. 417–418).
Every feasible solution of (IRC) yields one of (RC) with $y_{ij}=y_j$ , $z_{ij}=0$ (p. 420).
Feasibility for (LP) together with $\sum_ja_{ij}x_j+\epsilon\beta_i(x)\le b_i^+$ , $\beta_i(x)=\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2x_j^2}$ , suffices to extend $x$ to (RC) (p. 420).
The ratio $\alpha_i(x)/\beta_i(x)$ , $\alpha_i(x)=\sum_{j\in J_i}|a_{ij}||x_j|$ , is at most $\sqrt{\mathrm{card}(J_i)}/\Omega$ , with equality attained (p. 420, corrected).

Significance

Proposition 1 turns a probabilistic requirement, which is hard to handle directly, into a single convex (second-order-cone) program. The bound $\exp\{-\Omega^2/2\}$ does not depend on the dimension, on the number of uncertain entries, or on which symmetric distributions the perturbations follow, so $\Omega$ can be chosen from the desired reliability level alone. Together with milestones 3–6, the mission certifies the whole chain: the worst-case notion of reliability is exactly Soyster's linear program (IRC), and (RC) is never more conservative than (IRC), with an advantage that can reach the factor $\sqrt{\mathrm{card}(J_i)}/\Omega$ .

The results are proved in the paper; to our knowledge none of them is machine-checked. A formal development produces a reusable model of entry-wise uncertain LPs, the counterparts (∗), (IRC) and (RC) as Lean predicates, and a Hoeffding-type bound for weighted sums of symmetric bounded variables in the exact form (1). The platform's HighDimProb.Concentration.hoeffding_rademacher covers the Rademacher special case only.

Difficulty

The deterministic parts (milestones 1, 3–7) are elementary: worst cases of interval perturbations, and the Cauchy–Schwarz inequality. The obstacle lies in the probabilistic step. The printed proof passes from $\xi_{ij}a_{ij}$ to $\xi_{ij}|a_{ij}|$ with an equality that holds only in distribution, and contains index misprints, so it cannot be transcribed line by line; the reduction has to be restated pointwise. Eq. (1) is a tail bound for general symmetric variables in $[-1,1]$ , not only for random signs; the step (c) of the printed proof of (1) is written as an equality that holds only for random signs, so that proof too needs repair. The degenerate case $\sum_jp_j^2=0$ must be handled rather than assumed away.

Formalization scope

Data are a structure UncertainLP n p m over Fin indices (0-based), with A : Matrix (Fin m) (Fin n) ℝ, J : Fin m → Finset (Fin n) arbitrary, and EReal bounds so that infinite bounds are expressible. The objective $c$ is omitted: no statement involves it.
The probability space is $(S,\mathbb P)$ with IsProbabilityMeasure; the name $S$ avoids a clash with the safety parameter $\Omega$ . Symmetry is equality of the laws of $\xi_{ij}$ and $-\xi_{ij}$ ; values lie in $[-1,1]$ at every outcome; independence is required within each row only, with no identical distribution (§3.1 says only "independent", which is weaker than the "iid" of §2.2). Probabilities are P.real.
The hypotheses $\epsilon>0$ , $\delta>0$ , $\Omega>0$ are the paper's standing assumptions and are carried by every theorem that mentions the parameter.
Corrections of the printed text: $a_{ij}x_i\to a_{ij}x_j$ in (IRC); $\sum_{j\in J}\to\sum_{j\in J_i}$ in (RC); the reduction of milestone 1 is stated with $a_{ij}$ and $z_{ij}$ in place of the printed $|a_{ij}|$ , $x_i-y_{ij}$ and $y_j$ , $y_{ij}$ ; and the ratio of milestone 7 carries the factor $1/\Omega$ that the printed " $\sqrt{\mathrm{card}(J_i)}$ " omits.
Ruling out trivializations: the violation event uses the signed multiplicative model $(1+\epsilon\xi_{ij})a_{ij}$ , never $|a_{ij}|$ or an additive perturbation; the goal concludes both nominal feasibility (i) and the probability bound (ii′) for every row; no hypothesis excludes the degenerate case $\sum_{j\in J_i}a_{ij}^2z_{ij}^2=0$ ; and the probability model is satisfiable (e.g. by $\xi\equiv0$ or by Rademacher signs), so the goal is not vacuous.
The numerical remarks of the paper (0.92, 5.24, $10^{-6}$ , "at least 30") and the NETLIB case study are not formalized.
Reusable beyond this mission: the uncertain-LP model and the three counterparts, and the tail bound (1). Contributions of general lemmas about symmetric bounded random variables are welcome.

Selected references

A. Ben-Tal, A. Nemirovski, Robust solutions of Linear Programming problems contaminated with uncertain data, Math. Program. Ser. A 88 (2000) 411–424. https://doi.org/10.1007/s101070000163
A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Oper. Res. 21 (1973) 1154–1157. https://doi.org/10.1287/opre.21.5.1154
A. Ben-Tal, A. Nemirovski, Robust convex optimization, Math. Oper. Res. 23 (1998) 769–805. https://doi.org/10.1287/moor.23.4.769
A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Oper. Res. Lett. 25 (1999) 1–13. https://doi.org/10.1016/S0167-6377(99)00016-4
D. Bertsimas, M. Sim, The price of robustness, Oper. Res. 52 (2004) 35–53. https://doi.org/10.1287/opre.1030.0065
W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

12 thms4 active usersReviewed

Combinatorics Linear Optimization Operations Research+1·Captain: mikedeng1

Santa Claus Schedules Jobs on Unrelated Machines: The Configuration LP Has Integrality Gap at Most 33/17Research Paper

Motivation

Scheduling jobs on unrelated machines so as to minimize the makespan (the time at which the last machine finishes) is one of the central problems of approximation algorithms. For the general problem, Lenstra, Shmoys and Tardos (1990) gave a 2-approximation and showed that no polynomial-time algorithm achieves a factor below $3/2$ unless P = NP; closing the gap between $3/2$ and $2$ has been open since.

The restricted assignment problem is the special case in which every job $j$ has a single size $p_j$ and may only run on a given set $\Gamma(j)$ of machines. The $3/2$ hardness already holds here, and the best known algorithms were still $2$ -approximations. Every linear program previously used for the problem has integrality gap $2$ , so a better LP lower bound was the natural target.

Svensson (2011) showed that the configuration LP of Bansal and Sviridenko (2006), whose variables assign whole sets of jobs to machines, has integrality gap at most $33/17 \approx 1.9412$ . Its optimum therefore gives a polynomial-time estimate of the optimal makespan within a factor strictly better than $2$ .

1990: Lenstra, Shmoys, Tardos, 2-approximation for unrelated machines, and $3/2$ hardness already for restricted assignment.
2006: Bansal and Sviridenko introduce the configuration LP for the max–min variant (the Santa Claus problem).
2008: Feige shows the configuration LP has constant integrality gap for restricted Santa Claus, and Asadpour, Feige and Saberi (2008) give a local search proof of a factor-4 gap.
2011: Svensson adapts that local search to makespan and proves the gap $33/17$ for restricted assignment (arXiv:1011.1168).

Setting

An instance consists of finite sets $J$ (jobs) and $M$ (machines), sizes $p_j \ge 0$ , and for each job a set $\Gamma(j) \subseteq M$ . A schedule is a map $\sigma : J \to M$ with $\sigma(j) \in \Gamma(j)$ . The load of machine $i$ is $\sum_{j : \sigma(j) = i} p_j$ , and the makespan is the largest load. $\mathrm{OPT}$ is the least makespan of a schedule.

For a target makespan $T$ , a configuration for machine $i$ is a set $C \subseteq J$ of jobs that may all run on $i$ ( $i \in \Gamma(j)$ for $j \in C$ ) with $p(C) = \sum_{j \in C} p_j \le T$ . Write $\mathcal C(i,T)$ for the set of configurations. The configuration LP asks for $x_{i,C} \ge 0$ with

\text{[C-LP]}\qquad \sum_{C \in \mathcal C(i,T)} x_{i,C} \le 1 \quad (i \in M), \qquad \sum_{i \in M}\ \sum_{C \in \mathcal C(i,T),\ C \ni j} x_{i,C} \ge 1 \quad (j \in J).

Its dual has variables $y_i, z_j \ge 0$ and constraints $y_i \ge \sum_{j \in C} z_j$ for all $i$ and $C \in \mathcal C(i,T)$ . $\mathrm{OPT}_{LP}$ is the least $T$ at which [C-LP] is feasible, and $\mathrm{OPT}_{LP} \le \mathrm{OPT}$ .

In the Lean development these are configs Γ p T i, CLPFeasible Γ p T, CLPDualFeasible Γ p T y z and schedLoad p σ i, in the namespace RestrictedAssignment.Svensson.

Formalization targets

Goal: Theorem 4.1

For every instance with $p \ge 0$ and every $T \ge 0$ ,

\text{[C-LP] feasible at } T \ \Longrightarrow\ \exists\, \sigma : J \to M,\ \ \sigma(j) \in \Gamma(j)\ \forall j,\quad \sum_{j : \sigma(j) = i} p_j \le \tfrac{33}{17}\, T \ \ \forall i .

Equivalently $\mathrm{OPT} \le \tfrac{33}{17}\,\mathrm{OPT}_{LP}$ . The statement is scale-free and does not define $\mathrm{OPT}_{LP}$ .

Milestones

The milestones follow the paper's proof, which normalizes $\mathrm{OPT}_{LP} = 1$ and sets $R = 16/17$ :

a dual solution with $\sum_i y_i < \sum_j z_j$ makes [C-LP] infeasible;
the local search, Algorithm 2 (ExtendSchedule), keeps its partial schedule valid (load at most $1 + R$ , at most one big job per machine);
when the algorithm has no potential move, an explicit pair $(y^*, z^*)$ is dual feasible (Claim 4.7) and has $\sum y^* < \sum z^*$ (Claim 4.8);
hence, if [C-LP] is feasible, a potential move always exists (Lemma 4.6);
the algorithm has no infinite run (Lemma 4.9);
[C-LP] feasible at $T = 1$ gives a schedule of makespan at most $1 + 16/17$ .

Three facts from Section 2 complete the list: normalization by scaling, $\mathrm{OPT}_{LP} \le \mathrm{OPT}$ , and monotonicity of feasibility in $T$ .

Significance

The theorem shows that the configuration LP is a strictly stronger relaxation than those behind the factor- $2$ algorithms. With the known polynomial-time approximate solvability of the LP, it gives a polynomial-time algorithm that estimates the optimal makespan of restricted assignment within $33/17 + \epsilon$ . The local search in the proof finds a schedule of the same quality, but it is not known to run in polynomial time. Later work lowered the constant to $11/6$ (Jansen and Rohwedder, 2017) along the same lines.

The result is proved on paper. As far as known, no part of it has a machine-checked proof. Formalizing it gives:

a reusable definition of the configuration LP and its dual certificate;
a precise, nondeterministic model of a local search whose termination rests on a lexicographic potential;
a check of a proof that has many cases. The formalization already exposed two edge cases:
- Claim 4.8 fails when $j_{\mathrm{new}}$ has size $0$ and no admissible machine;
- the termination proof needs positive job sizes. With a job of size $0$ , the algorithm can move it back and forth between two tied machines forever.

The milestones are stated with the corresponding hypotheses.

Difficulty

The obvious approach, rounding a fractional configuration solution, loses a factor $2$ . If each machine takes one configuration and the collisions of jobs chosen twice or not at all are repaired, the repair can double a load. This is where every earlier LP-based bound stalls.

The milestones along the paper's route are hard for two reasons. First, the dual pair $(y^*, z^*)$ rounds job sizes down by class (big to $11/17$ , medium to $9/17$ ). Proving $\sum y^* < \sum z^*$ requires a case analysis over how each blocked machine came to be blocked. The two claims are therefore false for arbitrary states of the search and hold only for states the algorithm actually reaches, so the invariants of reachable states have to be formalized too. Second, the search both adds and removes blockers, so no simple quantity decreases at every step. Termination needs a potential defined on the whole history of the search.

Formalization scope

Jobs and machines are finite types with decidable equality, sizes are real numbers with $p_j \ge 0$ , and admissible machines are a Finset per job. Schedules are total maps $J \to M$ with $\sigma(j) \in \Gamma(j)$ stated explicitly. Partial schedules are maps $J \to$ Option M. Constants are exact rationals in $\mathbb R$ . Values of moves live in Lex (ℝ × ℝ).

Algorithm 2 is a step relation Step, not a function. The move of minimum lexicographic value is a hypothesis on the chosen pair, so every tie-breaking rule is covered. The blocker tree is stored as its list of blockers in insertion order. Claims 4.7, 4.8 and Lemma 4.6 quantify over states reachable from the initial state, as their proofs require. Lemma 4.9 asserts that no infinite run exists.

Three statements would trivialize the goal, and the formalization rules them out:

a schedule allowed to use machines outside $\Gamma(j)$ ;
a target $T < 0$ ;
an LP missing either constraint row.

Theorem 1.1 (polynomial time), the separation oracle, and Section 3's two-size case are not part of the mission.

Useful contributions include:

the weak-duality certificate;
the scaling and monotonicity facts;
the invariants of reachable states (each job lies in at most one blocker, blockers on a machine are never reassigned while present);
the two claims and the termination argument.

The configuration LP definitions are reusable for the Santa Claus problem and for bin packing.

Selected references

O. Svensson, Santa Claus Schedules Jobs on Unrelated Machines, arXiv:1011.1168v2, 2011; SIAM J. Comput. 41(5), 2012. https://arxiv.org/abs/1011.1168
J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Math. Programming 46, 1990. https://doi.org/10.1007/BF01585745
N. Bansal, M. Sviridenko, The Santa Claus problem, STOC 2006. https://doi.org/10.1145/1132516.1132522
A. Asadpour, U. Feige, A. Saberi, Santa Claus meets hypergraph matchings, APPROX 2008; ACM Trans. Algorithms 8(3), 2012. https://doi.org/10.1145/2229163.2229168
K. Jansen, L. Rohwedder, On the configuration-LP of the restricted assignment problem, SODA 2017. https://arxiv.org/abs/1611.01934

13 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Decomposition and Partitioning Methods for Multistage Stochastic Linear Programs: Binding Cuts Force Degenerate Descendant Problems in Nested DecompositionResearch Paper

Motivation

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

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

Setting

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

\min\ c^\top x + \theta \quad\text{s.t.}\quad A x = \xi + B x^{a},\quad D_l^\top x \ge d_l\ (l \le r),\quad E_l^\top x + \theta \ge e_l\ (l \le s),\quad x \ge 0,

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

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

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

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

Formalization targets

Goal: Proposition 4

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

\exists\, j' \in J' : \ z_{j'} \text{ is a degenerate basic solution of the problem (7) of } j' \text{ at } \bar x .

Milestone: Proposition 3

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

\text{every basic feasible solution of the problem (7) of } j' \text{ with } \bar x \text{ in (7.2) is degenerate.}

Significance

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

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

Difficulty

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

Formalization scope

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

Readings of informal words, each stated in the items:

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

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

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

Selected references

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

5 thms3 active usersReviewed