Operations Research

Motivation

Assortment optimization asks a retailer which products to offer when customers substitute among them. The nested logit model groups products into nests and is one of the most used choice models in revenue management, because it relaxes the independence of irrelevant alternatives of the plain multinomial logit model while keeping choice probabilities in closed form. Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) study how the tractability of the assortment problem under this model depends on two features: whether the dissimilarity parameters of the nests are at most one, and whether a customer who selects a nest always buys there (fully-captured nests).

When the dissimilarity parameters are at most one and the nests are fully captured, offering the $j$ highest-revenue products in every nest is optimal (Theorem 4 of the paper). This mission concerns what survives when a dissimilarity parameter exceeds one, the regime the paper calls possibly synergistic products. Then the problem is NP-hard (Theorem 5), and the paper shows that the same nested-by-revenue assortments still achieve an explicit, data-dependent fraction of the optimal expected revenue.

Setting

There are nests $i \in M$ and products $j \in N = \{1, \dots, n\}$ in every nest. Product $j$ of nest $i$ has a revenue $r_{ij}$ and a preference weight $v_{ij} > 0$, ordered so that $r_{i1} \ge r_{i2} \ge \dots \ge r_{in}$. Nest $i$ has a dissimilarity parameter $\gamma_i > 0$, and $v_0 \ge 0$ is the weight of leaving without choosing a nest. Throughout this mission the nests are fully captured: the within-nest no-purchase weights $v_{i0}$ are zero. For an assortment $S_i \subseteq N$ in nest $i$,

and the expected revenue of $(S_1, \dots, S_m)$ is

Problem (2) maximizes $\Pi$; its optimal value is $Z^*$. The nested-by-revenue assortment $N_{ij} = \{1, \dots, j\}$ collects the $j$ highest-revenue products of nest $i$, with $N_{i0} = \emptyset$ and $N_+ = \{0, 1, \dots, n\}$.

Problem (2) is equivalent to the linear program (3): minimize $x$ subject to $v_0 x \ge \sum_i y_i$ and $y_i \ge V_i(S_i)^{\gamma_i}(R_i(S_i) - x)$ for every nest $i$ and every $S_i \subseteq N$. Problem (4) keeps the second family of constraints only for candidate assortments; here the candidates are $\{N_{ij} : j \in N_+\}$, which gives a linear program with $1 + m$ variables and $1 + m(1 + n)$ constraints. The performance factor of the nested-by-revenue assortments is

Formalization targets

Goal: Theorem 7

Assume $v_{i0} = 0$ for every nest, $\gamma_i > 1$ for some nest, positive revenues and $n \ge 2$. If $(\hat x, \hat y)$ is an optimal solution of (4) over the nested-by-revenue assortments, then

Combined with Theorem 1 of the paper this yields $Z^* \le \alpha\, \Pi(\hat S)$ for the assortment $\hat S$ read off the small linear program; that consequence is a companion item.

Milestones

1. Problem (3) is a relaxation of the fractional problem (7), in which $y_i$ dominates $\big(\sum_j v_{ij} z_{ij}\big)^{\gamma_i}\big[\sum_j r_{ij} v_{ij} z_{ij} / \sum_j v_{ij} z_{ij} - x\big]$ for all $z_i \in [0,1]^n$.
2. Lemma 6: the inner maximization (8) of (7) has a solution of the form $z_{i1} = \dots = z_{i,k-1} = 1$, $z_{ik} \in [0,1]$, $z_{i,k+1} = \dots = z_{in} = 0$.
3. $\hat y_i \ge 0$ and $\hat x \ge 0$.
4. The inequalities (20) and (22) with the coefficients $\alpha^1_{ik} = R_i(N_{i,k-1})/R_i(N_{ik})$ and $1 \vee \alpha^2_{ik}$.
5. $R_i(N_{ij}) \le R_i(N_{i,j-1})$, and Lemma 14: $\alpha \ge 1$ when some $\gamma_i > 1$.
6. The inequalities (24) and (25): $\alpha \hat y_i$ dominates the objective of (8) at $\alpha \hat x$ for every vector of Lemma 6's shape.

Two companion statements follow the goal: the bounds $\alpha \le \rho$ and $\alpha \le 2\kappa$ when revenues, respectively preference weights, within each nest differ by at most the factors $\rho$, $\kappa$; and the guarantee $Z^* \le \alpha\, \Pi(\hat S)$.

Significance

Because problem (2) is NP-hard once a dissimilarity parameter exceeds one (Theorem 5 of the paper), an exact polynomial algorithm is not expected, and a guarantee for a polynomial-size candidate family is the natural substitute. Theorem 7 gives one with an explicit factor computed from the data: $\alpha \le \rho$ when revenues within each nest are balanced, $\alpha \le 2\kappa$ when preference weights within each nest are balanced, and the nests may differ arbitrarily from one another. The same linear-programming argument (Theorem 1) is reused for partially-captured nests in §6 of the paper.

The result is proved in the paper (Appendix A.1); no machine-checked version is known. A formalization verifies an appendix argument that is stated with little detail, and fixes the conventions that the page leaves implicit, such as the value of the objective of (8) at $z_i = 0$ and the role of the standing assumption that some $\gamma_i$ exceeds one.

Difficulty

Theorem 7 is a feasibility statement for the exponentially many constraints of (3), one per subset of every nest, while optimality of $(\hat x, \hat y)$ only controls the $n + 1$ nested-by-revenue constraints per nest. The obvious approach, comparing each subset directly with a nested-by-revenue assortment, fails: when $\gamma_i > 1$ the nested-by-revenue assortments are not optimal within a nest, and the example of §4.1 shows that they can lose an unbounded factor. The constant $\alpha$ must absorb the gap between a fractional assortment and its two neighbouring nested-by-revenue assortments, which the dual-style solution $(\hat x, \hat y)$ of the small program does not see.

Formalization scope

Lean 4 with Mathlib. Nests form a finite type ι; products are Fin n, indexed from $0$, so $N_{ij}$ is nbr n j = {k | k < j} and product $k$ of the page is ⟨k - 1, _⟩. Powers are real powers (Real.rpow), and division is total ($x / 0 = 0$), which gives $R_i(\emptyset) = 0$ and value $0$ for the objective of (8) at $z_i = 0$.

Standing assumptions in every statement: $v_0 \ge 0$, $v_{i0} \ge 0$, $v_{ij} > 0$, $r_{ij} \ge 0$, $\gamma_i > 0$, revenues ordered within each nest (§1); $v_{i0} = 0$ for every nest and $\gamma_i > 1$ for some nest (§4, p. 16). Added and disclosed: $r_{ij} > 0$ wherever (6) appears, so that no denominator of (6) vanishes; $n \ge 2$, the nonempty range of (6); $v_0 > 0$ only in the guarantee $Z^* \le \alpha\,\Pi(\hat S)$, inherited from Theorem 1. The factor $\alpha$ enters as a real number with the hypothesis that it is the greatest element of the set of terms of (6). An optimal solution of (4) is a feasible pair whose $x$ is minimal among feasible pairs.

A trivializing formalization is ruled out: $\alpha$ is the maximum of (6), not an arbitrary upper bound, and the goal states feasibility for the full program (3) over every subset of every nest, not for (7) or for the candidate collection.

Needed infrastructure: maximization of a continuous function on $[0,1]^n$, the greedy solution of a continuous knapsack, monotonicity of weighted averages and elementary real-power calculus. These are reusable beyond this mission. Proofs of any milestone, of the companions, and of the §4.1 example are welcome.

Selected references

• J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 2014. https://doi.org/10.1287/opre.2014.1256 (formalized from the revised manuscript of June 18, 2013).
• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147

Motivation

A portfolio manager who maximizes expected utility needs the distribution of asset returns, but in practice only estimates of its first two moments are available, and these estimates are themselves noisy. Distributionally robust optimization handles this by optimizing against the worst distribution in a set of plausible ones. Delage and Ye (Operations Research 58(3), 2010) proposed a set of distributions defined by confidence bounds on the mean and on the second-moment matrix, showed that the resulting problems are solvable in polynomial time for a large class of costs, and applied the framework to portfolio selection.

The set contains an upper bound on the covariance but no lower bound. Remark 1 of the paper says a lower bound "leads to important computational difficulties" and argues it should be unnecessary: for a concave utility, a less predictable market can only reduce expected utility, so the worst distribution should already have the largest covariance allowed. Proposition 3 in §5.2 turns this argument into a theorem for piecewise-linear concave utilities and unconstrained support. This mission formalizes Proposition 3 and the steps of its proof.

Setting

Let $n$ assets have a random return vector $\xi\in\mathbb R^n$, and let $x\in\mathbb R^n$ be a portfolio, so the return is $\xi^{\mathsf T}x$. A distribution of $\xi$ is a Borel probability measure on $\mathbb R^n$ with finite second moments. For symmetric matrices, $A\preceq B$ (the Loewner order) means $B-A$ is positive semidefinite.

Given a support set $S$, a centre $\mu_0$, a positive definite matrix $\Sigma_0\succ0$ and $\gamma_1\ge0$, $\gamma_2>0$, the distributional set of Assumption 3 is

The second constraint, (1b), is the covariance constraint.

The utility is piecewise linear concave, $u(y)=\min_{k\in\{1,\dots,K\}}a_ky+b_k$ with $K\ge1$ pieces, and the cost of a return is $-u$:

With estimates $\hat\mu$, $\hat\Sigma\succ0$ of the mean and covariance, the inner problem of the robust portfolio problem with unconstrained support and an exactly known mean ($\gamma_1=0$) is

The proof relates (18) to a semidefinite program in variables $\Lambda_k\in\mathbb R^{n\times n}$, $\lambda_k\in\mathbb R^n$, $\nu_k\in\mathbb R$:

Formalization targets

Goal: Proposition 3

For every $\gamma_1\ge0$ (the mean-uncertainty radius of the robust portfolio problem (16); (18) is the case $\gamma_1=0$),

The worst-case expectation is attained, and at a distribution for which the covariance constraint holds with equality. The statement holds for every portfolio $x$, every $K\ge1$, every $a,b$, every $\hat\mu$, every $\hat\Sigma\succ0$, every $\gamma_1\ge0$ and every $\gamma_2>0$.

Milestones

1. Every value of (18) is dominated by the value of a feasible point of (19).
2. (19) has an optimal solution at which $\sum_k\Lambda_k=\gamma_2\hat\Sigma+\hat\mu\hat\mu^{\mathsf T}$.
3. If $\begin{bmatrix}\Lambda&\lambda\\\lambda^{\mathsf T}&\nu\end{bmatrix}\succeq0$ and $\nu>0$, a random vector with mean $\lambda/\nu$ and second moment $\Lambda/\nu$ exists.
4. The mixture $\sum_k\nu_kP_k$ of such vectors, built from a tight feasible point with all $\nu_k>0$, lies in $\mathcal D_1$ and has second moment $\gamma_2\hat\Sigma$ about $\hat\mu$.
5. The expected cost under that mixture is at least the objective value of (19) at the point.
6. (18) and (19) have the same attained optimal value.

Significance

The proposition justifies a modelling decision of the whole paper: for portfolio problems with piecewise-linear concave utility, adding a lower bound $\gamma_3\Sigma_0\preceq\mathbb E[(\xi-\mu_0)(\xi-\mu_0)^{\mathsf T}]$ (display (2)) to the distributional set cannot change the robust decision, so the computational difficulty that lower bound would cause is avoided at no loss. It also shows that, under these assumptions and with $\gamma_2=1$, the paper's semidefinite formulation solves the known-moment portfolio problem of Popescu (2007) in polynomial time (Remark 4). The worst case is explicit: a finite mixture of distributions with prescribed first and second moments, read off an optimal solution of (19).

The result is proved in the paper; no machine-checked version is known. Formalizing it requires a moment-problem argument (from a distribution to a feasible point of an SDP) and its converse (from an SDP solution to a distribution), both of which are reusable for other moment-based distributionally robust results. The proposition concerns the robust portfolio problem with $\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,\gamma_1,\gamma_2)$; the paper's proof writes out only $\gamma_1=0$ "for simplicity of our derivations". The goal states the proposition for every $\gamma_1\ge0$; the milestones follow the written proof and are stated for $\gamma_1=0$.

Difficulty

The obvious argument, "a concave utility prefers less spread, so the adversary maximizes spread", does not prove anything by itself: increasing the second-moment matrix of a given distribution in the Loewner order does not determine its law, and the expected cost depends on the whole law, not on the moments. The proof goes through the semidefinite program (19). Two steps carry the weight. First, every distribution in $\mathcal D_1$ must be mapped to a feasible point of (19) with no smaller value, although the cost is only piecewise affine in $\xi$. Second, an optimal point of (19) must be turned back into a distribution in $\mathcal D_1$; this needs the existence of random vectors with prescribed first and second moments, and care with blocks where $\nu_k=0$, which the paper sets aside "without loss of generality" although such a block can carry a nonzero $\Lambda_k$ that the mixture would lose.

Formalization scope

• Vectors are Fin n → ℝ; all Euclidean quantities are dot products, never the sup norm. Matrices are Matrix (Fin n) (Fin n) ℝ; $A\preceq B$ is (B - A).PosSemidef; $\Sigma_0^{-1}$ is Mathlib's matrix inverse, used only with $\Sigma_0\succ0$.
• A distribution is a Measure (Fin n → ℝ) that is a probability measure and whose coordinates are in $L^2$ (MemLp _ 2). This makes every mean, second moment and expected cost a genuine integral; without it a non-integrable expectation would evaluate to $0$.
• $P(\xi\in S)=1$ is an almost-everywhere statement; the goal uses $S=\mathbb R^n$ ("infinite support constraint"). The convexity of $S$, $\mu_0\in\operatorname{int}S$ and the separation oracle of Assumption 3 concern the paper's algorithms and are not part of the set.
• The maximum of (18) is never a real supremum: the goal asserts a maximizer that dominates every member of the set. The cost uses a finite maximum over $K\ge1$ pieces ([NeZero K]).
• Standing hypotheses: $\hat\Sigma\succ0$ (Assumption 3's $\Sigma_0\succ0$, and endnote 1), $\gamma_2>0$ (§3), $\gamma_1\ge0$ (Assumption 3) in the goal; the milestones fix $\gamma_1=0$ as the proof does. The portfolio $x$ ranges over all of $\mathbb R^n$; the simplex constraint (16b) plays no role in the inner problem, so dropping it only strengthens the statements.
• The objective of (19) has the sign of the proof's final computation (p. 21), $\sum_k(-a_kx^{\mathsf T}\lambda_k-b_k\nu_k)$; display (19a) on p. 19 prints the opposite signs, a misprint.
• Ruling out trivial readings: the goal requires both membership in $\mathcal D_1$ with tight covariance and domination of every member of $\mathcal D_1$. A distribution with covariance $\gamma_2\hat\Sigma$ alone, or a maximizer alone, would not suffice. The goal does not claim that every maximizer is tight; for $K=1$ the cost is linear and every member of $\mathcal D_1$ is a maximizer.
• Infrastructure needed: existence of distributions with prescribed mean and covariance (for instance multivariate Gaussians, or degenerate laws on a subspace), finite mixtures of measures and their moments, Schur complements of positive semidefinite block matrices, and compactness of the feasible set of (19). Proofs of the milestones in any order are welcome.

The source is the authors' draft of 20 February 2008 of the Operations Research paper; every page, display and label in this mission refers to that draft.

Selected references

• E. Delage and Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3):595–612, 2010 (authors' draft of 20 February 2008 used here). https://doi.org/10.1287/opre.1090.0741
• I. Popescu, Robust mean-covariance solutions for stochastic optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
• Y. Nesterov and A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

Motivation

Maximum pressure policies schedule a stochastic processing network by choosing, at each decision time, an allocation of processors to activities that maximizes a linear "pressure" built from the current buffer levels and the network's input-output matrix. Dai and Lin (Oper. Res. 53(2), 2005) prove that such policies are throughput optimal: they stabilize the network whenever any policy can. The policies descend from the back-pressure rule of Tassiulas and Ephremides (IEEE TAC 37(12), 1992) for wireless networks and are now standard in switching, manufacturing and data-center scheduling.

The general theory lets a processor split its capacity among several activities at once. In many systems this is impossible: a machine works on one job type at a time. Section 7 of the paper shows that with this restriction Harrison's static planning LP no longer characterizes stability, and Section 8 shows that forbidding preemption can make a maximum pressure policy unstable. Both difficulties disappear for one structural class, the reversed Leontief networks, in which every activity needs exactly one processor. This mission formalizes the two lemmas that make that class work: extreme allocations are integral (Lemma 1), and a maximum pressure allocation is found processor by processor (Lemma 3).

Setting

A network has buffers $0,1,\dots,I$, where Buffer $0$ is the outside world and $\mathcal I=\{1,\dots,I\}$ are the internal buffers; activities $\mathcal J=\{1,\dots,J\}$; and processors $\mathcal K=\{1,\dots,K\}$. The resource consumption matrix $A$ has $A_{kj}=1$ if activity $j$ requires processor $k$ and $0$ otherwise. The constituency indicator $B_{ji}=1$ records that activity $j$ processes buffer $i$. An input activity processes only Buffer $0$; a service activity never processes Buffer $0$. Each processor runs input activities only (an input processor) or service activities only (a service processor). Each activity $j$ has a mean processing requirement $m_j$, rate $\mu_j=1/m_j$, and a routing matrix $P^j$.

The input-output matrix is

An allocation is $a\in\mathbb R^J_+$ with $\sum_j A_{kj}a_j\le1$ for every processor and $\sum_j A_{kj}a_j=1$ for every input processor; $\mathcal A$ is the set of allocations, $\mathcal E$ its set of extreme points, and $\mathcal N\subseteq\mathcal A$ the allocations with integer coordinates. For a buffer-level vector $z\in\mathbb R^I_+$, the network pressure is $p(a,z)=z\cdot Ra$ and the activity pressure is $p(j,z)=\sum_{i\in\mathcal I}R_{ij}z_i$, with $p(0,z)=0$ for the idle Activity $0$.

The network is reversed Leontief if each activity requires exactly one processor. The possible activities of processor $k$ are $\mathcal J(k)=\{j:A_{kj}=1\}$ for an input processor and $\mathcal J(k)=\{0\}\cup\{j:A_{kj}=1\}$ for a service processor. Under an integer allocation $a$, $j_k(a)$ is the activity processor $k$ works on, or $0$ if $k$ is idle.

Formalization targets

Goal: Lemma 3 (p. 208)

For a reversed Leontief network, $z\in\mathbb R^I_+$ and $a\in\mathcal E$,

Milestones

• the pressure identity $p(a,z)=\sum_j a_j\,p(j,z)$ (§8, p. 208);
• $\mathcal N\subseteq\mathcal E$ (proof of Lemma 1, p. 215);
• Lemma 1 (p. 207): for a reversed Leontief network, $\mathcal E=\mathcal N$;
• for $a\in\mathcal E$: $j_k(a)\in\mathcal J(k)$ and $p(a,z)=\sum_k p(j_k(a),z)$ (proof of Lemma 3);
• the single-processor exchange $\tilde a=a-e_{j_k(a)}+e_j$ stays in $\mathcal E$ and shifts the pressure by $p(j,z)-p(j_k(a),z)$ (proof of Lemma 3).

A further supporting item, not a milestone, states the decomposition $a=\sum_{j\in\mathcal J(\tilde k)}a_j b^j$ of an allocation along one processor (proof of Lemma 1, p. 215).

Significance

The result. Lemma 1 says that, in a reversed Leontief network, the maximum pressure policies of the processor-splitting theory are automatically non-processor-splitting, so the paper's throughput optimality theorem holds in the setting where machines cannot be shared. Lemma 3 says that the maximization over the (exponentially large) set $\mathcal E$ decouples into one small maximization per processor: each processor picks an activity of largest activity pressure among its own options. This separability is what makes the nonpreemptive version of the policy well defined and is the key step towards Theorem 9 (throughput optimality of nonpreemptive maximum pressure policies). It also covers multiclass queueing networks with alternate routes (§9.1), which are reversed Leontief.

Formalizing it. Both lemmas are proved in the paper; to our knowledge neither is machine-checked. The mission produces a reusable Lean model of the allocation polytope of a processing network with input processors, its integer and extreme points, and the activity and network pressures. The integrality of $\mathcal E$ is a total-unimodularity-type fact for a block structure that is not available in Mathlib in this form.

Difficulty

The pressure is linear, so maximizing over $\mathcal E$ equals maximizing over $\mathcal A$; the substance is the description of $\mathcal E$. The polytope $\mathcal A$ is not a box: input processors carry equality constraints and service processors inequality constraints, and in general networks (an activity needing several processors) $\mathcal E$ contains fractional points, as the paper's example in §7 shows. The step that fails for general networks is the decomposition of a fractional allocation along a single processor: it needs every activity of that processor to use no other processor. In Lean, extreme points must be handled through Mathlib's Set.extremePoints, and the argmax over $\mathcal J(k)$ must keep track of the idle option, which exists for service processors and not for input processors.

Formalization scope

Indices are 0-based: internal buffers Fin I, buffers with Buffer $0$ Fin (I+1) (Buffer $0$ is 0, internal buffer $i$ is i.succ), activities Fin J, processors Fin K. The idle Activity $0$ is none : Option (Fin J), with activity pressure $0$ and unit vector $e_0=0$. $\mathcal E$ is Set.extremePoints ℝ 𝒜. "Maximizes the pressure over $\mathcal E$" is stated by domination ($p(a',z)\le p(a,z)$ for all $a'\in\mathcal E$), never through a supremum. $j_k(a)$ is defined by choice of an activity of $k$ at level $1$; it is used only for $a\in\mathcal E$, where it is unique.

The standing assumptions of §2 are carried as one hypothesis: $A$ and $B$ are $0$–$1$, constituencies are nonempty, every activity is an input or service activity and needs a processor, processors are input-only or service-only, at least one input activity exists, $P^j\ge0$ and $P^j_{00}=0$. Two disclosed additions: every input processor has at least one activity (otherwise (2) is infeasible and $\mathcal A=\emptyset$), and $m_j>0$ (needed for $\mu_j=1/m_j$). The goal keeps $z\ge0$ as on the page; two milestones drop it, which strengthens them.

A trivializing formalization would make $\mathcal E$ empty or give input processors an idle option; both are excluded: $\mathcal E$ is the extreme-point set of the real polytope $\mathcal A$, which is nonempty for a reversed Leontief network under the standing assumptions, and the idle option belongs to $\mathcal J(k)$ only for service processors, as in (60).

Contributions welcome: proofs of the milestones, a general lemma that $0$–$1$ points of a subset of the unit cube are extreme, and the separable description of extreme points of products of simplices, which is reusable beyond this mission.

Selected references

• J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. https://doi.org/10.1287/opre.1040.0170
• J. M. Harrison, Brownian models of open processing networks: canonical representation of workload, Annals of Applied Probability 10(1):75–103, 2000. https://doi.org/10.1214/aoap/1019737665
• 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(12):1936–1948, 1992. https://doi.org/10.1109/9.182479

Motivation

Second-order stochastic dominance constraints let a decision maker require that a random outcome of a decision be preferred to a fixed benchmark outcome by every risk-averse expected-utility maximizer, without choosing a utility function in advance. Dentcheva and Ruszczyński introduced optimization under such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim., 2003), for the case where the decision enters the outcome linearly (the pure-dominance case). Their follow-up paper, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program., 2004), allows the decision to affect many random outcomes in a nonlinear, concave way, and derives optimality and duality theory in which the Lagrange multipliers of the dominance constraints are utility functions.

In applications (portfolio selection against a benchmark index is the paper's own example in §6) the probability space is a finite set of scenarios. Section 5 of the paper specialises the theory to that case. This mission formalizes that section: the reduction of the dominance constraints to finitely many inequalities, and the optimality and duality theorems (Theorems 6 and 7) in which the multipliers become piecewise-linear concave utilities.

Setting

There are $n$ scenarios $\omega_1,\dots,\omega_n$ with probabilities $p_j \ge 0$, $\sum_j p_j = 1$, and $m$ benchmark constraints, indexed by $i \in I = \{1,\dots,m\}$; $J = \{1,\dots,n\}$. A decision $z$ ranges over a convex set $Z \subseteq \mathbb R^N$. For each scenario $j$, $h_j:\mathbb R^N\to\mathbb R$ is the objective contribution and $g_{ij}:\mathbb R^N\to\mathbb R$ the $i$th outcome, all concave. The benchmark $Y_i$ has realizations $y_{ij}$. Write $(t)_+=\max(t,0)$.

The second-order dominance of a finitely distributed $X_i$ (realizations $x_{ij}$) over $Y_i$ on an interval $[a_i,b_i]$ reads

The split-variable problem (38)–(41) is

for all $i\in I$, $k\in J$, over $z$ and $X=(x_{ij})\in\mathbb R^{mn}$. The Slater condition asks for $\tilde z \in \operatorname{relint} Z$ and $\tilde X$ satisfying the dominance constraints (39) with $\tilde x_{ik} < g_{ik}(\tilde z)$ for all $i,k$.

The utility set $V_i$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave, nondecreasing, piecewise linear with break points only at the $y_{ik}$, and zero on $[\max_k y_{ik},\infty)$. With $\theta_{ij}\ge 0$ multipliers for the splitting constraints $x_{ij}\le g_{ij}(z)$, the Lagrangian is

Multipliers $\mu_{ik}$ of the inequalities (39) generate the utility $u_i(t)=-\sum_k\mu_{ik}(y_{ik}-t)_+$ (46). The dual functional is $D(u,\theta)=\sup_{z\in Z,\,X}L(z,X,u,\theta)$ (47).

Formalization targets

Goal: Theorem 6

Under the Slater condition, $(\hat z,\hat X)$ optimal for (38)–(41) implies that there are $\hat u_i\in V_i$ and $\hat\theta\ge 0$ with

conversely, these conditions together with feasibility imply optimality.

Milestones

1. Lemma 2 (p. 15): if $a_i\le y_{ij}\le b_i$, then (36) is equivalent to the $mn$ inequalities (37) at the realizations $\eta=y_{ik}$, and also to (36) on the whole line.
2. Eq. (46) (p. 17): for any $\mu$, the standard Lagrangian $\Lambda(z,X,\mu,\theta)$ equals $L(z,X,u,\theta)$ with $u$ given by (46).
3. p. 18: for $\mu_i\ge0$, the utility (46) lies in $V_i$.
4. pp. 16–17: under Slater, an optimal solution admits Kuhn–Tucker multipliers $\mu\ge0$, $\theta\ge0$ for (38)–(41) with complementarity.
5. p. 18: every $v\in V_i$ is of the form (46) with $\mu_i\ge0$.
6. Theorem 7 (p. 18), after the goal: the dual problem $\min\{D(u,\theta): u\in V_1\times\dots\times V_m,\ \theta\ge0\}$ has a solution and no duality gap.

Significance

Theorem 6 says that, for finitely many scenarios, the infinite-dimensional multiplier of the general theory (a concave utility in a cone of functions, Theorem 2 of the paper) can always be taken piecewise linear with kinks exactly at the benchmark's realizations. The multiplier space becomes finite-dimensional, $V_i$ is a polyhedral cone, and the dual problem of Theorem 7 is a finite-dimensional convex program. The paper's decomposition (49)–(51) of the dual functional and its numerical method in §6 rest on this. Lemma 2 is the standard reduction that makes dominance against a finitely distributed benchmark a finite set of polyhedral constraints, used throughout the later literature on dominance-constrained portfolio optimization.

The results are proved in the paper; none of them is formalized. The mission produces machine-checked statements of the finite-scenario theory, a Lean model of the utility set $V_i$ and of the correspondence between nonnegative multipliers and piecewise-linear utilities, and a Kuhn–Tucker theorem for concave programs with polyhedral constraints and a relative-interior Slater point.

Difficulty

The obvious route to Theorem 6 is to invoke a Kuhn–Tucker theorem. The available formal versions require every inequality constraint to hold strictly at the Slater point and range over all of $\mathbb R^N$. Neither fits: the dominance constraint at the smallest realization $y_{i,[1]}$ has right-hand side $0$ and a nonnegative left-hand side, so it can never hold strictly, and $Z$ may be lower-dimensional (a simplex), so only its relative interior is available. The polyhedral structure of (39) must be used, as in Rockafellar's Theorem 28.2. The second obstacle is the converse direction of the multiplier–utility correspondence: a utility in $V_i$ must be written as a nonnegative combination of the kinks $(y_{ik}-t)_+$, which requires handling repeated realizations and the one-sided slopes at each break point.

Formalization scope

• $\mathbb R^N$ is Fin N → ℝ; $X$, $\theta$, $\mu$ are Fin m → Fin n → ℝ; expectations are finite sums and positive parts are max t 0. No measure theory is used.
• Probabilities satisfy $p_j\ge0$, $\sum_jp_j=1$; $p_j=0$ is allowed, as on the page.
• Standing assumptions of p. 2 are explicit hypotheses: $Z$ convex and $h_j$, $g_{ij}$ concave on $\mathbb R^N$. Continuity is not stated, since finite concave functions on $\mathbb R^N$ are continuous.
• The relative interior is intrinsicInterior ℝ Z, not the topological interior. In the Slater condition only the splitting constraints are strict; the dominance constraints hold non-strictly.
• $V_i$ is defined by concavity, monotonicity, affinity on every interval whose interior contains no $y_{ik}$, and $u=0$ on $[\max_ky_{ik},\infty)$. This last clause is the page's $u(y_{i,[n]})=0$ combined with $V_i\subset\mathcal U_1([a_i,b_i])$. No positive slope is required, because the printed "$c>0$" in $\mathcal U_1$ is a misprint for $c\ge0$.
• "max" in (43) is an attained maximum over all of $Z\times\mathbb R^{mn}$, with no constraints on $X$. The dual functional (47) is an EReal supremum.
• Theorem 6 keeps the Slater condition as a hypothesis of the whole statement, as printed, although its converse part does not use it.
• A trivializing formalization is ruled out. $V_i$ is not defined as the set of functions of the form (46), which would make milestones 3 and 5 true by definition. Slater does not require strict dominance constraints, which would make it unsatisfiable. A sorry-free check confirms that the goal's hypotheses hold on an instance ($n=2$, $Z=[0,1]$).
• Reusable beyond this mission: the Kuhn–Tucker theorem with polyhedral constraints and relative-interior Slater point (milestone 4), and Lemma 2. Proofs of any item, and alternative proofs of the goal that avoid milestone 4, are welcome.
• The pure-dominance case is the earlier paper of Dentcheva–Ruszczyński (2003). The function $F_2$ and its expected-shortfall form are due to Ogryczak–Ruszczyński. The general Lagrange duality on the platform (ConvexOptimization.slater_strong_duality, Boyd–Vandenberghe §5.3.2) assumes a strict Slater point for every constraint and no set constraint, so it does not cover milestone 4.

Selected references

• D. Dentcheva, A. Ruszczyński, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints, Math. Program., 2004 (cited here from the authors' revised manuscript, April 2003). https://doi.org/10.1007/s10107-003-0453-z
• D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14 (2003) 548–566. https://doi.org/10.1137/S1052623402420528
• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM J. Optim. 13 (2002) 60–78. https://doi.org/10.1137/S1052623400375075
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §28. https://doi.org/10.1515/9781400873173

Why throughput matters

A processing network must decide which activities receive scarce processor capacity while jobs move among buffers. Such decisions matter in manufacturing, service systems, and switches: one activity can consume several processors at once, and a job can be routed to another buffer after processing. A policy that sees current buffer levels but does not need to know arrival or routing rates is easier to operate when those rates are difficult to estimate. Dai and Lin's 2005 paper studies whether a maximum pressure policy, which uses the buffer vector and an input-output matrix, can stabilize every network that is stabilizable in their model. Their Theorems 1 and 2 give, respectively, a necessary planning condition for any stabilizing policy and a sufficient condition for maximum pressure under the extreme-allocation-available assumption. Dai and Lin (2005)

Here pathwise stability means that each internal buffer grows sublinearly in time almost surely. This is a rate statement about sample paths. It does not assert positive recurrence of a Markov chain, nor does it require a stationary distribution. The paper allows general primitive processing and routing processes with almost-sure long-run averages. Dai and Lin (2005), §§2–4

Network and allocations

There are $I$ internal buffers, $J$ activities, and $K$ processors. Buffer $0$ represents the outside world. The $K\times J$ matrix $A$ records resource use: $A_{kj}=1$ when activity $j$ requires processor $k$. The $J\times(I+1)$ matrix $B$ records which buffers an activity processes. An input activity processes Buffer $0$; a service activity does not. Input processors serve only input activities and must be fully used, while all processors have at most unit capacity.

For activity $j$, the processing requirements have mean $m_j$ and the routing counts have long-run matrix $P^j$. Write $\mu_j=1/m_j$. The input-output matrix is

Positive $R_{ij}$ means activity $j$ consumes net material from internal buffer $i$; negative means it produces net material there. An allocation $a\in\mathcal A$ assigns nonnegative activity levels subject to the processor capacity bounds and the equality for every input processor. The finite set $\mathcal E$ consists of the extreme points of this allocation set. At buffer vector $z$, allocation $a$ has network pressure $p(a,z)=z\cdot Ra$. The maximum pressure rule chooses an allocation of greatest pressure among the currently feasible members of $\mathcal E$. Feasibility depends on jobs actually available to each constituent buffer. Dai and Lin (2005), §§2–3

The extreme-allocation-available assumption (EAA) says that for every nonnegative $z$, a pressure maximizer in $\mathcal E$ can be chosen whose constituent buffers all have positive levels. It links the static pressure maximization to the jobs that a policy can process. The static planning LP asks for activity fractions $x\ge0$ and a service-processor load $\rho$ such that $Rx=0$, every input processor has load one, and every service processor has load at most $\rho$. Dai and Lin (2005), p. 202

Formalization targets

The goal is Theorem 2. For a network satisfying EAA and run by a preemptive, processor-splitting maximum pressure policy, LP feasibility with $\rho\le1$ implies

The milestones follow the paper's route from stochastic paths to deterministic fluid limits. A fluid limit is a uniform-on-compact limit of $(Z(rt),T(rt))/r$ along positive scales $r\to\infty$. The milestones state that fluid limits satisfy (14)–(18), weak stability of the corresponding fluid model transfers to pathwise stability (Theorem 3), maximum pressure adds (52)–(55) and (20) (Lemmas 5 and 4), quadratic fluid energy obeys (22)–(23), and LP feasibility with EAA makes the maximum-pressure fluid model weakly stable (Theorem 4). Dai and Lin (2005), pp. 203, 213–214

What the result gives

Theorem 2 identifies a policy whose almost-sure buffer growth rate vanishes whenever the planning LP permits load at most one and EAA holds. Together with the paper's necessary condition in Theorem 1, it characterizes the feasibility boundary for this policy class under EAA. Its scope includes networks in which an activity uses multiple processors and processes multiple buffers simultaneously. It does not claim that all such networks satisfy EAA. Dai and Lin (2005), Theorems 1–2

The result is proved in the 2005 article. This mission asks for a machine-checked proof of that known theorem and its selected intermediate claims. The Lean statements are open draft targets. Reusable outcomes include a model of cumulative routing and service counts, a uniform-on-compact fluid-limit interface, and the weak-fluid-stability transfer theorem for networks without a Markov assumption.

Why the proof is difficult

Maximizing pressure over the static allocation polytope does not by itself describe an executable service policy. An allocation can demand work from an empty buffer. EAA addresses the existence of a maximizing allocation supported by positive buffer levels, but the stochastic policy acts on actual jobs and completion times. The proof must connect those discrete, pathwise decisions to the limiting differential equation (20). At a regular fluid time, the maximum-pressure equation is decisive; away from regular times, derivatives need not exist. The fluid model therefore carries a time qualifier that cannot simply be dropped. Dai and Lin (2005), pp. 201–203, 214

Formalization scope

The Lean model uses finite index types for buffers, activities, and processors. Internal buffers are Fin I; Buffer 0 is the zero index of Fin (I+1), and an internal buffer maps to its successor index. Activity and processor labels use zero-based Fin. Time is real but all network equations are asserted for nonnegative time. The shared Bell–Williams Paths definition supplies the renewal count in $\mathbb N\cup\{\infty\}$ and uniform-on-compact distance using the $\ell^1$ norm. The completion count is required finite wherever the network equations convert it to a natural number; this prevents infinity from becoming a zero count. Bell and Williams (2001)

The network standing assumptions record binary incidence matrices, nonempty constituencies, processor coverage, activity types, and an input activity. Two refinements are explicit: each input processor has an activity, so its mandatory unit allocation is feasible, and $m_j>0$, so $\mu_j=1/m_j$ is defined as the intended positive rate. Routing counts are cumulative and nonnegative. Their row sums are constrained only for buffers an activity processes: the printed sentence requiring the same sum for every buffer conflicts with its immediately preceding statement that the count vanishes when the activity does not process that buffer. The corresponding rows of $P^j$ sum to one for processed buffers and vanish for unprocessed buffers, as follows from (4). Dai and Lin (2005), pp. 199–200

The policy predicate records allocation-time decomposition (49)–(51) and the non-employment consequence of Definition 1 used in (56)–(58). It checks feasibility of a competing extreme allocation through the paper's threshold $J$ at every time of the interval. Individual job states and tie breaking are outside the pathwise interface. The goal retains EAA, the exact $\rho\le1$ bound, and all network and policy equations, so an empty allocation set or an unconstrained service path cannot make the target automatic. Contributions formalizing the finite extreme-point set, fluid-limit compactness, Lemmas 4–5, and the weak-stability transfer are welcome.

Selected references

• J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. DOI.
• S. L. Bell and R. J. Williams, Dynamic scheduling of a system with two parallel servers in heavy traffic with resource pooling: asymptotic optimality of a threshold policy, Annals of Applied Probability 11(3):608–649, 2001. DOI.

Motivation

A stochastic processing network (Harrison 2000) models a system in which processors carry out activities and each activity draws jobs from one or more buffers. Manufacturing lines, call centers with cross-trained agents, and data switches all fit this model. A central question is which scheduling policies are throughput optimal, meaning they stabilize the network whenever any policy can.

Dai and Lin (Oper. Res. 53(2), 2005) show that maximum pressure policies are throughput optimal. These policies generalize the back-pressure rule of Tassiulas and Ephremides (1992) for wireless and switch networks, and at each moment they choose the allocation that maximizes a linear "network pressure". Their main theorem (Theorem 2) has one structural hypothesis, the extreme-allocation-available (EAA) assumption (Assumption 1). It holds for many familiar networks and fails for some (§6.2 gives a counterexample). Theorem 6 identifies a broad class where it always holds: strict Leontief networks, in the sense of Bramson and Williams (2003). This mission formalizes that theorem.

Setting

A network has internal buffers $\mathcal I=\{1,\dots,I\}$, an outside Buffer $0$, activities $\mathcal J=\{1,\dots,J\}$ and processors $\mathcal K=\{1,\dots,K\}$.

• $A_{kj}=1$ if activity $j$ needs processor $k$, and $0$ otherwise.
• $B_{ji}=1$ if activity $j$ processes buffer $i\in\mathcal I\cup\{0\}$, and $0$ otherwise. The set $\mathcal B_j=\{i:B_{ji}=1\}$ is the constituency of $j$.
• An input activity has $\mathcal B_j=\{0\}$; a service activity has $0\notin\mathcal B_j$. Every activity is one of the two.
• Each processor serves input activities only (an input processor) or service activities only.
• Activity $j$ has processing rate $\mu_j=1/m_j$ and a nonnegative routing matrix $P^j$.