All missions

Motivation

Robust regression guards a linear model against errors in the data matrix. The observations $b \in \mathbb R^n$ are fitted by $Ax$, but the features (the columns $a_1,\dots,a_m$ of $A$) are only known up to a disturbance $\Delta A$ from an uncertainty set $\mathcal U$. The robust estimator minimizes the worst-case residual,

$$\min_{x \in \mathbb R^m}\ \max_{\Delta A \in \mathcal U} \|b - (A+\Delta A)x\| .$$

Xu, Caramanis and Mannor (arXiv:0811.1790v1; IEEE Trans. Inf. Theory 56(7), 2010) showed that when each column is perturbed independently within a Euclidean ball of radius $c_i$, this problem is exactly the weighted $\ell_1$-regularized problem $\min_x \|b - Ax\|_2 + \sum_i c_i|x_i|$, an un-squared Lasso (their Theorem 1, the subject of the first mission of this series). Robustness then explains regularization: the penalty is the price of the worst disturbance.

Section III of the paper asks which regularizers arise when the disturbances of different features are coupled, that is, when a single budget limits all columns jointly. The answer it gives is that every norm-based regularizer arises this way: a norm budget on the vector of column-disturbance sizes produces the dual norm as the penalty. This links robust optimization (Ben-Tal, El Ghaoui, Nemirovski 2009) and regularized estimation, and it recovers the robust least-squares formulation of El Ghaoui and Lebret (1997) as the Euclidean special case.

Setting

Fix $n \ge 1$, $m \ge 0$, and an arbitrary norm $\|\cdot\|_a$ on $\mathbb R^n$. The data are the columns $a_1,\dots,a_m \in \mathbb R^n$ of $A$ and the response $b \in \mathbb R^n$; for $x \in \mathbb R^m$, $Ax = \sum_i x_i a_i$. A disturbance is $\Delta A = (\delta_1,\dots,\delta_m)$ with $\delta_i \in \mathbb R^n$; the perturbed matrix $A + \Delta A$ has columns $a_i + \delta_i$. For an uncertainty set $\mathcal U$ the robust objective is

$$R_{\mathcal U}(x) = \sup_{\Delta A\in\mathcal U} \|b - (A+\Delta A)x\|_a \in [-\infty,+\infty].$$

Three families of uncertainty sets appear.

1. Feature-wise (Theorem 3): for budgets $c_i \ge 0$, $\mathcal U_a = \{(\delta_1,\dots,\delta_m) : \|\delta_i\|_a \le c_i\}$.
2. Coupled (p. 6): for functions $f_1,\dots,f_k:\mathbb R^m\to\mathbb R$, $\mathcal U' = \{(\delta_1,\dots,\delta_m) : f_j(\|\delta_1\|_a,\dots,\|\delta_m\|_a) \le 0,\ j=1,\dots,k\}$, with the budget set $\mathcal Z = \{z \in \mathbb R^m : f_j(z) \le 0\ \forall j,\ z \ge 0\}$.
3. Norm budget (Corollary 1): for a norm $\|\cdot\|_s$ on $\mathbb R^m$ and $l \ge 0$, $\mathcal U' = \{(\delta_1,\dots,\delta_m) : \|(\|\delta_1\|_a,\dots,\|\delta_m\|_a)\|_s \le l\}$. The dual norm is $\|y\|_s^* = \sup\{y^\top z : \|z\|_s \le 1\}$. A norm is absolute if $\|(|z_1|,\dots,|z_m|)\|_s = \|z\|_s$ for all $z$.

A fourth, polytope set, $\{(\delta_1,\dots,\delta_m) : \exists c \ge 0,\ Tc \le s,\ \|\delta_j\|_a \le c_j\}$ for $T \in \mathbb R^{k\times m}$, $s\in\mathbb R^k$, is the subject of Corollary 2. Write $|x| = (|x_1|,\dots,|x_m|)$.

Formalization targets

Goal: Corollary 1 (p. 7)

For an absolute norm $\|\cdot\|_s$ and $l \ge 0$, for every $x \in \mathbb R^m$ the worst case over the norm-budget set is attained and

$$\max_{\Delta A\in\mathcal U'} \|b-(A+\Delta A)x\|_a = \|b - Ax\|_a + l\,\|x\|_s^*,$$

and the robust problem and $\min_x \|b-Ax\|_a + l\|x\|_s^*$ have the same minimizers.

Milestone: Theorem 3 (p. 6)

For $c \ge 0$ and every $x$: $\max_{\Delta A\in\mathcal U_a}\|b-(A+\Delta A)x\|_a = \|b-Ax\|_a + \sum_i c_i|x_i|$, attained, with the same minimizers.

Milestone: Eq. (13) (proof of Theorem 4, Appendix B, p. 19)

For every $x$, in the extended reals,

$$\sup_{\Delta A\in\mathcal U'} \|b-(A+\Delta A)x\|_a = \|b-Ax\|_a + \sup_{c\in\mathcal Z} |x|^\top c .$$

Milestone: Corollary 2 (p. 7)

If some $c \ge 0$ has $Tc \le s$, then for every $x$ the worst case over the polytope set equals $\|b-Ax\|_a + \inf\{s^\top\lambda : x \le T^\top\lambda,\ -x\le T^\top\lambda,\ \lambda\ge0\}$ (both sides $+\infty$ when the constraints are infeasible), the infimum is attained when feasible, and robust minimizers are exactly the $x$-parts of optimal solutions of that linear program.

The paper's general result, Theorem 4 (p. 6), expresses the coupled robust problem through a Lagrangian function $v(\lambda,\kappa,x)$ under the assumption that $\mathcal Z$ has nonempty relative interior. The mission does not pose it: that assumption is not Slater's condition, and the statement fails without one (an explicit counterexample with $\mathcal Z = \{0\}\times[0,\infty)$ is recorded in the series plan). The mission poses the decomposition (13), on which Theorem 4 rests, and the two corollaries, which are true as stated under the readings below.

Significance

The result. Corollary 1 says that any norm penalty $l\|x\|_s^*$ is the worst-case cost of column disturbances whose sizes are jointly bounded in the dual norm. Taking $\|\cdot\|_s = \ell_\infty$ gives the $\ell_1$ penalty (budget per column), $\ell_1$ gives $\ell_\infty$ (a shared budget), and both Euclidean gives the Frobenius-ball model of robust least squares. Corollary 2 shows that polytope budgets keep the problem a linear program apart from the loss, which allows modeling, for instance, corruption of an unknown subset of features. Eq. (13) is the common reduction behind these: the coupled worst case is the uncoupled one maximized over the admissible budget vectors.

Formalizing it. None of these statements has a machine-checked proof. The mission makes precise two points the paper leaves implicit: which "symmetric" norms the corollary is true for, and in what sense "max" holds when the budget set is empty or unbounded. The finished development is a self-contained library of worst-case residual identities for arbitrary norms on finite-dimensional or general normed spaces. Related platform items, credited and not reused: SPOBounds.StronglyConvex.dual_norm_ball_max (maximum of a linear functional over a norm ball, with the continuous-dual norm), and RobustLS.Unstructured.worst_case_residual_closed_form (El Ghaoui–Lebret, which perturbs $[A\ b]$ in a Frobenius ball, a different set).

Difficulty

The upper bound of every identity is a triangle inequality. The content is in the matching lower bound: a disturbance must be exhibited that aligns all perturbed columns with the residual direction, and in (13) each column disturbance must have norm exactly $c_i$, including columns with $x_i = 0$, which is where $n \ge 1$ enters. The paper's first line of the proof of (13) rewrites $\mathcal U'$ as $\{\Delta A : \exists c \in \mathcal Z,\ \|\delta_i\|_a \le c_i\}$; that set identity is false unless $\mathcal Z$ is downward closed, so the obvious route through it does not work for (13) as stated. For Corollary 1 the remaining step is the identity $\sup\{|x|^\top c : c\ge0,\ \|c\|_s\le l\} = l\|x\|_s^*$, which needs the absolute property and fails for norms that are only permutation invariant. For Corollary 2 the remaining step is linear programming duality, which Mathlib does not yet provide in this form.

Formalization scope

$(\mathbb R^n, \|\cdot\|_a)$ is an arbitrary real normed space $E$ with Nontrivial E (the paper's implicit $n\ge1$); finite dimension is not imposed, a harmless generalization. Columns are a family a : Fin m → E, disturbances δ : Fin m → E, coefficients Fin m → ℝ, and $Ax = \sum_i x_i \cdot a_i$. Explicit readings:

1. The robust objective is a supremum over the uncertainty set, computed in EReal; it is never defined by its closed form. "Max" is stated as IsGreatest of the set of residual values (attained) in Theorem 3 and Corollary 1, where the maximum exists, and as an EReal supremum in (13) and Corollary 2, where it need not.
2. "Is equivalent to" / "the resulting regularized regression problem is" means: equal objectives at every $x$ and equal sets of minimizers. Existence of a minimizer is not claimed.
3. "Symmetric norm" is read as absolute; $\|\cdot\|_s$ is a Mathlib Seminorm on Fin m → ℝ with $N z = 0 \Rightarrow z = 0$ (the type already carries the sup norm, so the notation $\|\cdot\|$ is not used for it). The dual norm is a real sSup of $\{y^\top z : N z \le 1\}$, a nonempty set that is bounded above because $N$ is a norm on $\mathbb R^m$.
4. $l \ge 0$ is added to Corollary 1, and feasibility of $c\ge0$, $Tc\le s$ to Corollary 2; without them the sets are empty.
5. Eq. (13) is stated for $\mathcal U'$ as defined on p. 6 (not through the paper's set rewriting); the convexity of the $f_j$ is kept as the paper's standing assumption and is not used.

A trivializing formalization is ruled out: the robust objective is the EReal supremum (or the residual-value set) over the uncertainty set, so no identity holds by unfolding, and no real sSup junk value enters a robust objective. Welcome contributions: the explicit worst-case disturbance in an arbitrary normed space, the absolute-norm duality lemma, and a finite-dimensional LP strong duality theorem, each reusable beyond this mission.

Selected references

• H. Xu, C. Caramanis, S. Mannor, Robust Regression and Lasso, arXiv:0811.1790v1, 2008; IEEE Transactions on Information Theory 56(7):3561–3574, 2010. https://arxiv.org/abs/0811.1790v1, https://doi.org/10.1109/TIT.2010.2048503
• L. El Ghaoui, H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM Journal on Matrix Analysis and Applications 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• R. Tibshirani, Regression shrinkage and selection via the lasso, Journal of the Royal Statistical Society B 58(1):267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x

Motivation

Facility networks fail: plants close after floods, distribution centres lose power, suppliers go bankrupt. The reliable uncapacitated facility location problem (RUFL) of Cui, Ouyang and Shen (UCTC-FR-2010-02, February 2010; published as Operations Research 58(4), 2010, doi:10.1287/opre.1090.0801) chooses which facilities to open and, for every customer, an ordered list of backup facilities, so as to minimize fixed cost plus expected transportation and penalty cost when facilities fail independently with site-dependent probabilities. It extends the uniform-probability model of Snyder and Daskin (Transportation Science, 2005).

RUFL is solved by Lagrangian relaxation in the sense of Fisher (Management Science, 1981): dualizing the constraints that link assignments to open facilities splits the problem into one relaxed subproblem (RSP$_i$) per customer. Every evaluation of the Lagrangian dual solves all $I$ subproblems, and (RSP$_i$) is itself a hard combinatorial problem, because the probability that a backup facility is used depends on which facilities sit above it. The paper therefore replaces (RSP$_i$) by a fixed-probability reformulation (RRSP$_i$), an assignment problem, and Proposition 4 asserts that its optimal value is a valid lower bound. A Lagrangian bound computed from (RRSP$_i$) is a valid bound on RUFL only if this holds.

Setting

Fix one customer $i$ and drop the index $i$ from the variables. The data are: the demand rate $\lambda_i \ge 0$; regular facilities $j = 0, \dots, J-1$ with unit costs $d_{ij}$ and failure probabilities $0 \le q_j < 1$; an emergency facility $J$ with $d_{iJ} = \varphi_i$ (the penalty per unit of unserved demand) and $q_J = 0$; multipliers $\mu_{ij}$; and levels $r = 0, \dots, R$ with $R \ge 1$.

A level assignment is a binary array $Y_{jr}$ ($Y_{jr} = 1$: facility $j$ serves at level $r$) such that the customer has distinct regular facilities at levels $0, \dots, s-1$, the emergency facility at a level $s \le R$, and nothing after it. In the paper's constraints:

$$\sum_{j=0}^{J} Y_{jr} + \sum_{s<r} Y_{Js} = 1 \ (\forall r),\qquad \sum_{r<R} Y_{jr} \le 1 \ (j<J),\qquad \sum_{r\le R} Y_{Jr} = 1 .$$

The level-$r$ facility serves exactly when all facilities at the levels above it have failed. The transitional probabilities are $P_{j0} = 1 - q_j$ and $P_{jr} = (1-q_j)\sum_{k<J} \frac{q_k}{1-q_k} W_{k,r-1}$, with $W_{jr} = P_{jr} Y_{jr}$ imposed through linear constraints. The relaxed subproblem is

$$\text{(RSP}_i)\qquad \min\ \sum_{j\le J}\sum_{r\le R} \lambda_i d_{ij} W_{jr} + \sum_{j<J}\sum_{r<R} \mu_{ij} Y_{jr}.$$

Order the regular facilities by reliability, $q_{j_0} \le q_{j_1} \le \dots \le q_{j_{J-1}}$, and set $\beta_r = \prod_{\ell<r} q_{j_\ell}$ and $\alpha_r = (1 - q_{j_r})\beta_r$. The reformulation freezes the probabilities at these values:

$$\text{(RRSP}_i)\qquad \min\ \sum_{j<J}\sum_{r<R} (\lambda_i d_{ij}\alpha_r + \mu_{ij}) Y_{jr} + \sum_{r\le R} \lambda_i d_{iJ}\beta_r Y_{Jr}$$

over the same level assignments.

The proof works through a split formulation: $Y$ chooses whose distance is paid at each level, a second level assignment $Z$ chooses whose failure probability is used, and the cost is $G = \sum_r \lambda_i d_{i,y(r)} P_{z(r),r} + \sum \mu_{i,y(r)}$. Imposing $Y = Z$ gives back (RSP$_i$).

Formalization targets

Goal: Proposition 4

With $\lambda_i \ge 0$, $0 \le q_j < 1$, $\mu_{ij} \ge 0$, $R \ge 1$ and any reliability ordering: for every (RSP$_i$)-feasible $(Y, P, W)$ there is an (RRSP$_i$)-feasible $Y'$ with

$$\mathrm{obj}_{\text{RRSP}}(Y') \le \mathrm{obj}_{\text{RSP}}(Y, W), \qquad\text{that is,}\qquad \min(\text{RRSP}_i) \le \min(\text{RSP}_i).$$

Milestones, in proof order

1. Swap identity (A.4, p. 39). Exchanging the probability facilities $j$, $k$ of two consecutive levels $r$, $r+1$ while keeping $Y$ changes the cost by $\frac{q_j - q_k}{1 - q_j}\lambda_i P_{jr}(d_{iu} - d_{iv})$.
2. Lemma 1 (p. 38). The split formulation has an optimal solution whose probability facilities are ordered by $q$ on the regular levels.
3. Relaxation (A.4, p. 39). Every (RSP$_i$)-feasible point gives a split-feasible point with $Z = Y$ and the same cost.

Significance

The result. Proposition 4 makes (RRSP$_i$) usable as a lower-bounding oracle. (RRSP$_i$) is an assignment problem with $J+1$ rows and $R+1$ levels, so it can be solved in strongly polynomial time by the Hungarian method (Kuhn, 1955). The exact subproblem algorithm of §3.3.1 needs branch and bound over subsets. With the bound, every subgradient iteration of the paper's Lagrangian scheme still yields a valid lower bound on RUFL, which is what the gap-closing branch and bound relies on.

Formalizing it. The proposition has a printed proof, but the proof is incomplete (see below), and to our knowledge no machine-checked version exists. A formal proof certifies the bound, settles which hypotheses it needs, and gives a reusable model of multi-level backup assignment with transitional probabilities.

Difficulty

The obvious argument says that $\alpha_r$ is the largest probability any facility can have of serving at level $r$, so freezing the probabilities at $\alpha_r$ can only lower the cost. That is false as stated: transport costs $d_{ij}$ and the penalty $\varphi_i$ may be negative, and a larger serving probability then means a higher cost. What is needed is a comparison of the whole cost profile, not level by level.

The paper's route is the split formulation. Lemma 1 shows that the probability facilities of some optimal split solution can be taken in increasing order of $q$. The proof then ends with "without loss of generality, we can fix $Z = Z^*$ and $P = P^*$ … which leads to the (RRSP) formulation". This step has a gap. Lemma 1 only says that $Z^*$ is ordered. Turning its probabilities into $\alpha_r$, $\beta_r$ also needs $Z^*$ to use the facilities $j_0, j_1, \dots$ with the globally smallest failure probabilities, and the paper never shows this. A complete proof has to replace $Z^*$'s facilities by the most reliable ones and show that the cost does not increase. That replacement raises every cumulative service probability $1 - \prod_{\ell\le r} q$, so the comparison is a rearrangement argument over the ordered distances. Lemma 1 alone does not close the proposition.

The sign of the multipliers matters. With $\mu_{ij}$ of mixed sign the proposition is false, for instance with $J = 2$, $R = 1$, $d = (3.09, 4.73)$, $q = (0.62, 0.86)$, $\varphi_i = -0.93$, $\mu = (2.18, -2.99)$, $\lambda_i = 2.3$. There $\min(\text{RSP}_i) = -3.306$ while $\min(\text{RRSP}_i) = -2.139$. Lemma 1, by contrast, holds for multipliers of either sign.

Formalization scope

Facilities are Fin (J+1) with Fin.last J the emergency facility, levels are Fin (R+1), and every variable is a real array, with $Y$ constrained to $\{0,1\}$. The customer index is dropped. The ordering $j_\ell$ is a bijection $\sigma$ of Fin J with $q \circ \sigma$ monotone, and the goal quantifies over every such $\sigma$. "Lower bound" is stated as for-all/exists, so no infimum of a possibly empty set is taken; both feasible sets are finite and contain the emergency-only assignment.

Conventions fixed in Lean, each recorded in the docstrings:

• The level constraints (4b), (7b), (19c) sum over all facilities $j = 0, \dots, J$. The printed upper limit $J-1$ is a typo: with it, a regular facility would have to share the emergency facility's level.
• $\alpha_r = 0$ for $r \ge J$, and $\beta_r$ for $r > J$ is the product of all $q_j$. These values are never multiplied by a nonzero assignment, and $R \le J$ is not assumed.
• The split cost is the $G$ used in the proof of Lemma 1, not the printed (19a), which would charge the $Z$-facility's distance. $Y$ and $Z$ must put the emergency facility at the same level.
• $\mu_{ij} \ge 0$ is a hypothesis of the goal only. $\lambda_i \ge 0$, $0 \le q_j < 1$ and $R \ge 1$ are the paper's standing assumptions. No sign is assumed on $d_{ij}$ or $\varphi_i$.

The statements are not trivial. A sanity-check file exhibits a two-facility instance satisfying every hypothesis, together with feasible points of all three formulations.

A complete development needs finite sums and products over Fin, the explicit form of $P$ along a level assignment (a product of failure probabilities), and a rearrangement inequality for ordered sequences. All three are reusable for the other missions of this series and for reliability models in general. Contributions are welcome on the milestones, on a corrected proof of the final step, and on lemmas such as "the transitional probabilities of a level assignment are products of the $q$'s".

Selected references

• L. Cui, Y. Ouyang, Z.-J. M. Shen, Reliable Facility Location Design under the Risk of Disruptions, UCTC-FR-2010-02, University of California Transportation Center, February 2010; published in Operations Research 58(4):998–1011, 2010. https://doi.org/10.1287/opre.1090.0801
• L. V. Snyder, M. S. Daskin, Reliability Models for Facility Location: The Expected Failure Cost Case, Transportation Science 39(3):400–416, 2005. https://doi.org/10.1287/trsc.1040.0107
• M. L. Fisher, The Lagrangian Relaxation Method for Solving Integer Programming Problems, Management Science 27(1):1–18, 1981. https://doi.org/10.1287/mnsc.27.1.1
• H. W. Kuhn, The Hungarian Method for the Assignment Problem, Naval Research Logistics Quarterly 2(1–2):83–97, 1955. https://doi.org/10.1002/nav.3800020109
• H. D. Sherali, A. Alameddine, A New Reformulation-Linearization Technique for Bilinear Programming Problems, Journal of Global Optimization 2:379–410, 1992. https://doi.org/10.1007/BF00122429

Motivation

Many operations models contain terms of the form $E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big)$: expected shortfall or overflow of an affine function of an uncertain vector. Inventory and newsvendor costs, penalties for violated soft constraints, and the Conditional Value-at-Risk of a linear decision rule all reduce to it. In practice the distribution $\mathbb P$ of the uncertainty is rarely known; what is known are a few descriptive statistics, such as a range for the mean and an estimate of the covariance. Distributionally robust optimization then replaces the expectation by its supremum over every distribution consistent with that information.

The question goes back to Scarf (1958), who solved a single-product newsvendor problem against the worst distribution with known mean $\mu$ and variance $\sigma^2$, using the fact that $\sup E(X^+) = \tfrac12\big(\mu + \sqrt{\mu^2 + \sigma^2}\big)$ over such laws; Gallego and Moon (1993) simplified the argument. El Ghaoui, Oks and Oustry (2003) obtained conic representations of worst-case Value-at-Risk under mean and covariance information, and Delage and Ye (2010) studied stochastic programs with uncertain mean and covariance. Goh and Sim (2010) use bounds of this kind inside a general framework for linear optimization under uncertainty with recourse: after a piecewise-linear decision rule is introduced, every expectation in the reformulated problem is of the form above, and the framework needs a tractable, ideally exact, value for its worst case. Section 5.2 of the paper provides it when the information consists of a set containing the mean and the exact covariance.

Setting

A primitive uncertainty $\tilde z \in \mathbb R^{N}$ is represented through a segregated uncertainty $\tilde\zeta \in \mathbb R^{N_E}$, $N_E \ge N$, and a fixed matrix $F \in \mathbb R^{N\times N_E}$ and vector $g \in \mathbb R^{N}$ with $\tilde z = F\tilde\zeta + g$ (equation (9) of the paper). The paper notes that $F$ has full row rank. Write $n = N_E$.

The distributional information is:

• a set $\hat{\mathcal V} \subseteq \mathbb R^{n}$ known to contain the mean $\hat\zeta = E_{\mathbb P}(\tilde\zeta)$ (the mean is uncertain, its "support" is $\hat{\mathcal V}$);
• the exact covariance $\Sigma \in \mathbb R^{N \times N}$ of the primitive vector $\tilde z$.

The family is

$$\mathbb F_2 = \Big\{\mathbb P :\ \hat\zeta = E_{\mathbb P}(\tilde\zeta) \in \hat{\mathcal V},\ E_{\mathbb P}\big(F(\tilde\zeta - \hat\zeta)(\tilde\zeta - \hat\zeta)'F'\big) = \Sigma\Big\}.$$

For $r^0 \in \mathbb R$ and $r \in \mathbb R^{n}$ the worst-case expected positive part is $\sup_{\mathbb P \in \mathbb F_2} E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big)$, and the bound of (22) is

$$\pi^2(r^0, r) = \inf_{y:\, F'y = r}\ \sup_{\hat\zeta \in \hat{\mathcal V}} \Big\{ \tfrac12 (r^0 + r'\hat\zeta) + \tfrac12 \sqrt{(r^0 + r'\hat\zeta)^2 + y'\Sigma y} \Big\}.$$

Following the paper (p. 909), an infeasible minimization has value $+\infty$; all values are in $[-\infty, +\infty]$.

Formalization targets

Goal: Theorem 2 (p. 910)

For $F$ of full row rank, $\Sigma$ positive semidefinite and $\hat{\mathcal V}$ nonempty,

$$\sup_{\mathbb P \in \mathbb F_2} E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big) = \pi^2(r^0, r) \qquad \text{for all } r^0, r.$$

This is an exact identity; it contains no constants that later work could improve.

Milestones

1. Upper-bound part of Theorem 2: $\sup_{\mathbb F_2} E_{\mathbb P}((r^0 + r'\tilde\zeta)^+) \le \pi^2(r^0, r)$, with no hypotheses.
2. Remark after Theorem 2: for $\Sigma \succeq 0$, $f(u) = \tfrac12 u + \tfrac12\sqrt{u^2 + y'\Sigma y}$ is nondecreasing in $u$.
3. (23): for $\Sigma \succeq 0$ and $\hat{\mathcal V} \neq \emptyset$,

$$\pi^2(r^0, r) = \inf_{u,\, y}\Big\{\tfrac12 u + \tfrac12\sqrt{u^2 + y'\Sigma y} :\ r^0 + \sup_{\hat\zeta \in \hat{\mathcal V}} r'\hat\zeta \le u,\ F'y = r\Big\}.$$

4. Tightness part of Theorem 2: $\pi^2(r^0, r) \le \sup_{\mathbb F_2} E_{\mathbb P}((r^0 + r'\tilde\zeta)^+)$ under the goal's hypotheses.

Significance

Theorem 2 says that the deterministic problem (22) evaluates the worst case exactly, not merely bounds it. Through (23) it becomes a second-order cone program whenever $\hat{\mathcal V}$ is conic representable, so distributionally robust constraints and objectives with mean–covariance information can be handed to an off-the-shelf conic solver without loss. In the paper, $\pi^2$ is one of three building blocks (with the mean–support bound $\pi^1$ and the directional-deviation bound $\pi^3$) that are combined by infimal convolution into the unified bound of Theorem 4, which in turn prices the deflected linear decision rules of §6. Specialized to $N = n$, $F = I$ and a singleton mean set, it recovers Scarf's mean–variance bound.

The theorem is proved in the paper's online appendix; no machine-checked proof of it, nor of Scarf's bound in this multivariate form, is known to exist. A formalization would certify the exact value, including the cases the printed statement treats only implicitly: $r$ outside the range of $F'$ (both sides $+\infty$), a degenerate quadratic form $y'\Sigma y = 0$, and unbounded mean sets.

Difficulty

The upper bound is a moment inequality and is the easier half. The difficulty is tightness. The supremum over $\mathbb F_2$ is in general not attained, so the proof must exhibit, for every point of $\hat{\mathcal V}$, distributions on $\mathbb R^{n}$ that meet the full covariance constraint on $F\tilde\zeta$ exactly while driving the expected positive part of the single linear functional $r'\tilde\zeta$ to the bound. The constraint fixes $N(N+1)/2$ second moments, not just the variance of $r'\tilde\zeta$, so the scalar extremal laws behind Scarf's bound do not directly give members of $\mathbb F_2$. The case $F'y = r$ infeasible requires showing that the worst case is $+\infty$, i.e. that $\mathbb F_2$ contains distributions with arbitrarily large expectations; this is where the full-rank assumption on $F$ enters.

Formalization scope

The random vector is the identity on Fin n → ℝ and a distribution is a measure P on it. The mean, the covariance matrix and the finite-second-moment condition come from the published definition MomentDRO_Conf_Setting (meanVec, covMat, HasSecondMoments). The covariance condition is $F\,\mathrm{Cov}_{\mathbb P}(\tilde\zeta)\,F' = \Sigma$, which equals the paper's $E_{\mathbb P}(F(\tilde\zeta - \hat\zeta)(\tilde\zeta - \hat\zeta)'F')$ by linearity; it constrains the covariance of the primitive vector, an $N \times N$ matrix, not the covariance of $\tilde\zeta$. The positive part is max · 0. The worst case and $\pi^2$ take values in EReal: an infimum over an empty set is $+\infty$ and a supremum over an empty set is $-\infty$, matching the paper's convention for infeasible problems. The paper's "inf" and "sup" are not claimed to be attained.

Readings fixed by this mission, each implicit in the paper:

• Full row rank of $F$ (p. 906, "F has to be full rank"), stated as surjectivity of $x \mapsto Fx$;
• $\Sigma$ positive semidefinite, as a covariance matrix must be;
• $\hat{\mathcal V}$ nonempty.

Each is needed for the equality: without it $\mathbb F_2$ can be empty (worst case $-\infty$) while $\pi^2$ is finite or $+\infty$. No convexity or closedness of $\hat{\mathcal V}$ is assumed; the theorem does not need it. A formalization that takes the infimum in $\mathbb R$ (where an empty infimum is $0$) or states only the inequality $\le$ would trivialize or weaken the theorem and is ruled out.

A complete development needs a Scarf-type mean–variance inequality for $E(X^+)$, constructions of multivariate distributions with a prescribed mean and covariance (Gaussian or finitely supported laws), and the monotonicity and continuity facts behind (23). The scalar inequality and the constructions of distributions with given first two moments are reusable well beyond this mission. Proofs of any milestone, and supporting lemmas on moment-constrained families, are welcome.

Selected references

• J. Goh and M. Sim, Distributionally Robust Optimization and Its Tractable Approximations, Operations Research 58(4), 902–917, 2010. https://doi.org/10.1287/opre.1090.0795
• H. Scarf, A min-max solution of an inventory problem, in K. Arrow (ed.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 201–209, 1958.
• G. Gallego and I. Moon, The distribution free newsboy problem: Review and extensions, Journal of the Operational Research Society 44(8), 825–834, 1993. https://doi.org/10.1057/jors.1993.141
• L. El Ghaoui, M. Oks and F. Oustry, Worst-case value-at-risk and robust portfolio optimization: A conic programming approach, Operations Research 51(4), 543–556, 2003. https://doi.org/10.1287/opre.51.4.543.16101
• E. Delage and Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3), 595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• X. Chen, M. Sim, P. Sun and J. Zhang, A linear decision-based approximation approach to stochastic programming, Operations Research 56(2), 344–357, 2008. https://doi.org/10.1287/opre.1070.0441

Motivation

In machine scheduling, preemption means that a job may be interrupted and resumed later, possibly on a different machine. Allowing it can only lower the optimal cost, and a basic question for every scheduling model is how much it can lower it: the ratio between the best nonpreemptive and the best preemptive schedule, often called the power of preemption. For identical parallel machines and the total weighted completion time, McNaughton (1959) showed that preemption does not help at all (doi:10.1287/mnsc.6.1.1). For unrelated machines, where every job has its own processing time on every machine, and with release dates, it does help, and no exact relation is known.

Skutella's paper (J. ACM 48 (2001), doi:10.1145/375827.375840) gives approximation algorithms for unrelated-machine scheduling based on convex quadratic programming relaxations. Its §4 adapts the relaxation of §3 to preemptive schedules and rounds it to a nonpreemptive schedule. A by-product is a constant bound on the power of preemption for $R\mid r_{ij}\mid\sum w_jC_j$: the factor $3$, and $2$ without release dates. This mission formalizes that bound together with the steps of §4 that produce it.

Setting

There are $n$ jobs $j$ and $m$ unrelated machines $i$. Job $j$ has a weight $w_j\ge0$, and on machine $i$ a processing time $p_{ij}>0$ and a release date $r_{ij}\ge0$ before which it may not be processed there.

A preemptive schedule is a finite list of pieces: job $j$ runs on machine $i$ during $[s,e]$. Running job $j$ for $\ell$ time units on machine $i$ completes the fraction $\ell/p_{ij}$ of it. A schedule is feasible if every piece of $j$ on $i$ starts no earlier than $r_{ij}$, two pieces on the same machine never overlap, two pieces of the same job never overlap, and the fractions of every job add up to exactly $1$. The completion time $C_j$ is the end of the last piece of $j$, and the objective is $\sum_j w_jC_j$. A schedule is nonpreemptive if every job consists of a single piece.

Smith's order $\prec_i$ on machine $i$ orders the jobs by nonincreasing ratio $w_j/p_{ij}$, ties broken by index. On each machine the release dates sorted nondecreasingly are $\rho_{i_1}\le\dots\le\rho_{i_n}$, with $\rho_{i_{n+1}}:=\infty$, and the time slot $i_k$ is $[\rho_{i_k},\rho_{i_{k+1}})$. For a preemptive schedule, $a_{i_kj}$ is the fraction of job $j$ processed on machine $i$ inside slot $i_k$. The convex quadratic program $(CQP'_p)$ asks for $a\ge0$ and $Z$ with $\sum_{i,k}a_{i_kj}=1$, slot capacities $\sum_j a_{i_kj}p_{ij}\le\rho_{i_{k+1}}-\rho_{i_k}$, $a_{i_kj}=0$ when $\rho_{i_k}<r_{ij}$, and

$$Z\ \ge\ \sum_j w_j\sum_{i,k}a_{i_kj}\Bigl(\rho_{i_k}+\frac{a_{i_kj}}{2}p_{ij}+\sum_{j'\prec_ij}a_{i_kj'}p_{ij'}\Bigr),\qquad Z\ \ge\ \sum_j w_j\sum_{i,k}a_{i_kj}p_{ij}.$$

Randomized rounding puts job $j$ into slot $i_k$ with probability $a_{i_kj}$, pairwise independently over jobs, and schedules each slot's jobs back to back in Smith's order from the slot's start.

Formalization targets

Goal: Corollary 4.6, the power of preemption

For every feasible preemptive schedule $P$ there is a feasible nonpreemptive schedule $S$ with

$$\sum_j w_jC_j(S)\ \le\ 3\sum_j w_jC_j(P),$$

and if all $r_{ij}=0$, one with $\sum_j w_jC_j(S)\le 2\sum_j w_jC_j(P)$. This is the paper's ratio of optima, stated so that no existence of optimal schedules is needed.

Milestones

1. (24): $\sum_j w_jC_j\ge\sum_j w_j\sum_{i,k}a_{i_kj}p_{ij}$ for every preemptive schedule.
2. Exchange inequality (proof of Lemma 4.2): inside one slot, Smith's order minimizes $\sum_j a_jw_j\sum_{j'\text{ before }j}a_{j'}p_{ij'}$ over all orders.
3. (25): the bound (23) with $\prec_i$ replaced by the order of completion times in the schedule.
4. Lemma 4.2: every preemptive schedule satisfies (23) and (24).
5. $(CQP'_p)$ is a relaxation: the fractions of every preemptive schedule, with $Z=\sum_j w_jC_j$, are feasible.
6. Lemma 4.3: rounding any feasible $(\bar a,Z)$ yields feasible nonpreemptive schedules with $\mathbb E[\sum_j w_jC_j]\le 3Z$, and $\le 2Z$ when all release dates are $0$.

Significance

The result gives a constant bound on how much preemption can help on unrelated machines with release dates, a model in which both the preemptive and the nonpreemptive problems are NP-hard (for the preemptive problem even without weights and release dates, by Sitters, J. Algorithms 57 (2005), doi:10.1016/j.jalgor.2004.06.011). The bound comes from an algorithm: a single relaxation that is valid for preemptive schedules, rounded to a nonpreemptive one. The same rounding is a randomized $3$-approximation for $R\mid r_{ij},pmtn\mid\sum w_jC_j$ and a $2$-approximation for $R\mid pmtn\mid\sum w_jC_j$ (Theorem 4.5), and since it never preempts, these bounds hold under any communication delays between machines.

The paper proves all of this on paper. As far as a search of the platform shows, none of it is formalized: the only formal preemption result found is McNaughton's theorem for identical machines. The mission produces a machine-checked model of preemptive schedules on unrelated machines with release dates, a checked lower bound on such schedules by a convex quadratic function of their slot fractions, and a checked analysis of pairwise-independent rounding into nonpreemptive schedules.

Difficulty

The natural first idea is to reuse the nonpreemptive relaxation $(CQP)$ of §3, which already allows fractional assignments. It fails. Example 4.1 of the paper gives two jobs on two machines where an optimal preemptive schedule costs $7$ but the corresponding $(CQP)$ value is $7.25$, so $(CQP)$ is not a relaxation of the preemptive problem. The relaxation must be weakened: the term $(1+a_{i_kj})/2$ of §3 becomes $a_{i_kj}/2$, and this weakening is what raises the factor from $2$ to $3$.

Proving that the weaker program is a relaxation (Lemma 4.2) takes real work. The fractions of a job inside a slot of an arbitrary preemptive schedule are scattered, so the bound needs a rearrangement inside each slot by completion times, then an exchange argument that compares this order with Smith's order slot by slot. On the rounding side, Lemma 4.3 reduces to the analysis of §3 (each job's expected completion time is at most twice its value in the relaxation) and, without release dates, to Theorem 2.1 of §2. Both have to be redone here on the slot model.

Formalization scope

Jobs, machines and slots are Fin n, Fin m, Fin n (0-based). The standing assumptions $p_{ij}>0$, $w_j\ge0$, $r_{ij}\ge0$ of p. 2 are hypotheses of every theorem. Smith's order is cross-multiplied ($w_jp_{ik}>w_kp_{ij}$), equivalent to the ratio form because $p>0$. Sorted release dates come from Tuple.sort. The last slot of each machine has no right end, so $\rho_{i_{n+1}}=\infty$ is never a real number, and the slot capacity constraint is imposed only for slots with a successor. A preemptive schedule is a List of pieces with migration allowed and any number of pieces; nonpreemptive means one piece per job. Completion time is the latest end time among a job's pieces.

Added constraint. The display of $(CQP'_p)$ on p. 22 omits the condition $a_{i_kj}=0$ if $\rho_{i_k}<r_{ij}$ (constraint (18) of §3). Without it the rounding can place a job in a slot that opens before its release date, and "computes a nonpreemptive schedule" in Lemma 4.3 fails. It is included here. The fractions of every feasible preemptive schedule satisfy it, so the program remains a relaxation.

Randomized rounding is a probability weight on the finite set of slot assignments with marginals $\bar a$ and pairwise products $\bar a\bar a'$. Pairwise independence is required, full independence is not, and the expectation is a finite sum. "Without nontrivial release dates" is read as $r_{ij}=0$ for all $i,j$. Communication delays are not modelled: without them the preemptive class is the largest, so the goal implies the bound for every delay model.

Not formalized: polynomial running time, solving $(CQP'_p)$ within an additive error $\varepsilon$, derandomization by conditional probabilities (Theorem 4.5), and Corollary 4.4.

The goal is not trivial. Feasible preemptive schedules exist and are not vacuous, since each job's fractions must sum to $1$ and no machine runs two pieces at once. The nonpreemptive schedule is required to be feasible in the same model, and its value is compared with the given schedule's real objective, not with a relaxation value.

A complete development needs: the slot schedule (15)–(17) and its feasibility, the bound $\mathbb E[C_j]\le2\bar C_j$ of §3 (Lemma 3.5) and Theorem 2.1 of §2, both restated on this slot model, and a product-measure argument showing that pairwise-independent rounding exists. The preemptive-schedule model and the slot machinery are reusable for other unrelated-machine results. Contributions to any milestone are welcome, and so are alternative proofs of Lemma 4.2.

Selected references

• M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, J. ACM 48(2) (2001) 206–242. https://doi.org/10.1145/375827.375840
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106
• R. McNaughton, Scheduling with deadlines and loss functions, Management Science 6(1) (1959) 1–12. https://doi.org/10.1287/mnsc.6.1.1
• A. S. Schulz and M. Skutella, Scheduling unrelated machines by randomized rounding, SIAM J. Discrete Math. 15(4) (2002) 450–469. https://doi.org/10.1137/S0895480199357078
• R. Sitters, Complexity of preemptive minsum scheduling on unrelated parallel machines, J. Algorithms 57(1) (2005) 37–48. https://doi.org/10.1016/j.jalgor.2004.06.011

Motivation

In a road or communication network, traffic is routed by its users, not by a central planner. Each user picks the route that is cheapest for itself, and the resulting equilibrium can be much more expensive for the network as a whole than the best centrally planned routing. Roughgarden and Tardos, How Bad is Selfish Routing? (J. ACM 2002), quantified this loss. Their basic model is nonatomic: infinitely many users, each controlling a negligible amount of traffic. There, the cost of a Nash flow can exceed the optimum by an unbounded factor, but it never exceeds the cost of an optimal flow that routes twice as much traffic (their Theorem 3.1).

Many networks are not like that. A few large operators (internet service providers, freight companies, a navigation app routing its whole user base) each control a strictly positive share of the traffic and can split it over many paths. Section 5.2 of the paper treats this finite splittable model and proves the analogue of the bicriteria bound, Theorem 5.4. This mission formalizes that theorem and the three steps of its proof.

Setting

A network has a finite set $E$ of edges. Each edge $e$ carries a latency function $\ell_e$, nonnegative, nondecreasing and continuous on $[0,\infty)$: the delay on $e$ when $x$ units of flow use it is $\ell_e(x)$.

There are $k$ agents. Agent $i$ must send $r_i>0$ units of flow from a source $s_i$ to a destination $t_i$, over its set $\mathcal P_i$ of paths. Distinct agents may have the same source and destination; their path sets are then separate copies. A flow $f$ assigns a nonnegative amount $f_P$ to each path; agent $i$'s part is $f^{(i)}$, the restriction of $f$ to $\mathcal P_i$. The flow is feasible for the rates $r$ if $\sum_{P\in\mathcal P_i} f_P = r_i$ for every $i$, and feasible for $2r$ if each agent instead sends $2r_i$.

The edge flow $f_e=\sum_{P\ni e} f_P$ is the flow of all agents through $e$. The latency of a path is $\ell_P(f)=\sum_{e\in P}\ell_e(f_e)$, and

$$C(f)=\sum_P \ell_P(f)\,f_P,\qquad C_i(f)=\sum_{P\in\mathcal P_i}\ell_P(f)\,f^{(i)}_P$$

are the cost of the flow (its total latency) and the cost of agent $i$. A feasible flow $f$ is at Nash equilibrium if no agent can lower its own cost by rerouting its own flow: for each $i$, $f^{(i)}$ minimizes $C_i$ given $f^{(j)}$ for $j\neq i$.

In Lean, edges, paths and agents are Fin J, Fin R and Fin Sd; a path is a $0/1$ incidence column A j r, s r is the agent owning path r, and rate i is $r_i$. The edge flow linkFlow and the feasible set wardropFeasible come from the published definition KellyStochasticNetworks_Wardrop; pathLatency, cost and the modified latencies barLatency come from the series' shared model definitions (SelfishRouting.Bicriteria), and agentCost and IsSplittableNash are defined in this mission.

Formalization targets

Goal: Theorem 5.4 (p. 20)

If $x\cdot\ell_e(x)$ is convex on $[0,\infty)$ for every edge, $f$ is at Nash equilibrium for the finite splittable instance $(G,r,\ell)$, and $f^*$ is feasible for $(G,2r,\ell)$, then

$$C(f)\le C(f^*).$$

The comparison flow $f^*$ is arbitrary, so the statement implies the bound against an optimal flow for $2r$ without naming one.

Milestones (proof of Theorem 5.4, p. 20)

The proof uses the modified latencies $\bar\ell_e(x)=\ell_e(f_e)$ for $x\le f_e$ and $\bar\ell_e(x)=\ell_e(x)$ for $x\ge f_e$, built from the Nash flow $f$ (p. 12). Writing $\bar C(g)=\sum_P\bar\ell_P(g)g_P$:

1. $\bar C(f^*) - C(f^*)\le C(f)$ for any flows with nonnegative path flows;
2. $f$ is optimal for $(G,r,\bar\ell)$: $\bar C(f)\le\bar C(g)$ for every $g$ feasible for $r$;
3. every $g$ feasible for $2r$ has $\bar C(g)\ge 2C(f)$.

Significance

Theorem 5.4 says that in a network shared by finitely many traffic-splitting operators, the inefficiency of selfish routing can always be offset by doubling the network's capacity to carry traffic, whatever the network topology and whatever the (convexity-qualified) delay functions. Theorem 3.1 is its limit as the number of agents grows and each share shrinks to zero. The finite splittable model is the setting of later work on atomic splittable routing games and their price of anarchy, which this mission's definitions can serve.

On the formalization side, the result is proved on paper but, as far as a search of the platform and of Mathlib shows, no part of selfish-routing equilibrium theory with finitely many agents has been formalized. The mission provides a reusable encoding of the finite splittable model (per-agent costs, per-agent best responses with all other agents fixed) on top of the published Wardrop definitions, and the three proof steps as separately provable milestones. Milestone 2 is the one with independent content: it turns a game-theoretic equilibrium into the optimum of a convex program.

Difficulty

The obvious attempt copies the proof of Theorem 3.1. That proof uses the nonatomic equilibrium condition: every used path of a commodity has the same, minimal latency $L_i(f)$, so $\bar\ell_P(g)\ge L_i(f)$ for every path and the lower bound $\bar C(g)\ge 2C(f)$ follows path by path. In the finite splittable model this fails: an agent at equilibrium balances marginal costs $\ell_P(f)+f^{(i)}_P\cdot(\text{slope})$, not latencies, and its used paths can have different latencies. The proof must go through the optimality of $f$ for the modified program $(G,r,\bar\ell)$, and that needs both the convexity of $x\cdot\ell_e(x)$ and a comparison between the change of agent $i$'s cost and the change of the $\bar\ell$-cost under the same local move. The paper invokes a first-order optimality lemma (its Lemma 2.4) for $\bar\ell$, which is not differentiable at $f_e$; a formal proof has to handle one-sided derivatives or argue by convexity directly.

Formalization scope

• Routes, not graphs. Paths are arbitrary $0/1$ incidence columns with an owner map; the paper's simple-path families are one instance. The proof never uses graph structure. Two agents with the same source and destination have disjoint index sets of routes.
• Latency hypotheses on $[0,\infty)$ only: 0 ≤ ℓ j t for 0 ≤ t, MonotoneOn and ContinuousOn on Set.Ici 0, and ConvexOn ℝ (Set.Ici 0) (fun t => t * ℓ j t). Continuity replaces the differentiability of §2.1, as footnote 3 (p. 7) and §5.2 allow; this weakens a hypothesis.
• Rates are positive (0 < rate i). The case of zero agents is allowed and trivial, as in the paper.
• Nash equilibrium is the precise form printed on p. 19: each agent's part minimizes its cost among feasible flows that agree with $f$ on every other agent's paths. A deviating agent keeps its total at $r_i$ and cannot change others' flows; the agent's cost is evaluated at the total edge flow of all agents.
• No ratios. The theorem is the inequality $C(f)\le C(f^*)$ for every $f^*$ feasible for $2r$; no division by an optimal cost appears.
• Feasible for $2r$ is wardropFeasible s (fun i => 2 * rate i).
• The existence of a Nash flow (Rosen) is neither assumed nor claimed. A sorry-free check shows the definition is satisfiable: in the two-link Pigou network with one agent of rate 1 and latencies $1$ and $x$, the flow $(1/2,1/2)$ is a Nash flow.
• A trivializing formalization is excluded: the equilibrium is not the Wardrop condition, deviations are restricted to the deviating agent's own feasible flows, and the theorem quantifies over every feasible comparison flow rather than over an assumed optimum.

Contributions welcome: proofs of the three milestones and the goal; a general lemma that a feasible flow minimizing a convex separable edge cost has no improving two-path move, and its converse; a proof that $x\mapsto\bar\ell_e(x)\,x$ is convex when $x\,\ell_e(x)$ is.

Selected references

• T. Roughgarden and É. Tardos, How Bad is Selfish Routing?, Journal of the ACM 49(2):236–259, 2002. https://doi.org/10.1145/506147.506153
• J. B. Rosen, Existence and Uniqueness of Equilibrium Points for Concave N-Person Games, Econometrica 33(3):520–534, 1965. https://doi.org/10.2307/1911749
• F. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 4. https://doi.org/10.1017/CBO9781139565363

Motivation

In a road or communication network carrying a large population of users, each user picks a route that is fastest for itself given the congestion caused by everyone else. The resulting traffic pattern, a Wardrop or Nash equilibrium, need not minimize the total travel time: Braess's paradox shows that adding a road can make every user slower. Transportation science has modelled such equilibria since Wardrop (1952) and Beckmann, McGuire and Winsten (1956), and the question of how much efficiency selfish behaviour costs was posed in computer science by Koutsoupias and Papadimitriou (1999).

Roughgarden and Tardos, How Bad is Selfish Routing? (J. ACM, 2002) gave the first general answers for networks with many infinitesimal users. This mission formalizes the first of them, from §2.5 of the paper: when every edge latency is a polynomial of degree at most $p$ with nonnegative coefficients, the total latency at equilibrium is at most $p+1$ times the optimum. The argument goes through the convex program of Beckmann et al., whose optimal solutions are exactly the equilibria (Dafermos and Sparrow, 1969).

Timeline. 1952: Wardrop states the equilibrium principle. 1956: Beckmann, McGuire and Winsten characterize equilibria as minimizers of a convex potential and prove existence. 1969: Dafermos and Sparrow reprove existence and essential uniqueness for general networks. 1999: Koutsoupias and Papadimitriou introduce the worst-case ratio between equilibrium and optimum. 2000–2002: Roughgarden and Tardos prove the bounds $p+1$ for polynomials (Corollary 2.8) and $4/3$ for linear latencies. 2002–2003: Roughgarden shows the worst ratio for degree-$p$ polynomials is $\Theta(p/\ln p)$, attained already on two parallel links.

Setting

An instance consists of finitely many edges $e$, finitely many commodities $i\in\{1,\dots,k\}$ and finitely many routes $P$. Each route is a set of edges, recorded by a $0/1$ incidence matrix $A$ ($A_{eP}=1$ iff $e\in P$), and serves exactly one commodity; $\mathcal P_i$ is the set of routes serving commodity $i$. Commodity $i$ has a rate $r_i>0$.

A flow assigns a value $f_P$ to each route. It induces the edge flows $f_e=\sum_{P\ni e}f_P$ and is feasible if $f_P\ge0$ for all $P$ and $\sum_{P\in\mathcal P_i}f_P=r_i$ for all $i$. Each edge has a latency function $\ell_e$, nonnegative, nondecreasing and continuous on $[0,\infty)$. The latency of a route is $\ell_P(f)=\sum_{e\in P}\ell_e(f_e)$ and the cost of a flow is

$$C(f)=\sum_P\ell_P(f)\,f_P=\sum_e\ell_e(f_e)\,f_e .$$

A feasible flow is at Nash equilibrium (Definition 2.1) if moving any amount $\delta\in[0,f_{P_1}]$ of commodity $i$ from a used route $P_1$ to another route $P_2\in\mathcal P_i$ leaves $P_2$ at least as slow, after the move, as $P_1$ was before. Lemma 2.2 shows that this is the Wardrop condition: every route that carries flow has minimum latency among the routes of its commodity.

The Beckmann potential of a flow is $\Phi(f)=\sum_e\int_0^{f_e}\ell_e(t)\,dt$, the objective of the program (NLP2) of the paper.

Formalization targets

Goal: Corollary 2.8

For latencies $\ell_e(x)=\sum_{i=0}^{p}a_{e,i}x^i$ with $p\ge1$ an integer and $a_{e,i}\ge0$, every flow $f$ at Nash equilibrium and every feasible flow $f^*$ satisfy

$$C(f)\le(p+1)\,C(f^*).$$

This is the paper's $\rho(G,r,\ell)=C(f)/C(f^*)\le p+1$ written without division.

Milestones

1. Lemma 2.2: Nash equilibrium (Definition 2.1) $\iff$ the Wardrop condition.
2. Proof of Lemma 2.6: the flows at Nash equilibrium are exactly the feasible minimizers of $\Phi$.
3. Lemma 2.6: a Nash flow exists, and all Nash flows have the same cost.
4. Corollary 2.7: if $x\,\ell_e(x)\le\alpha\int_0^x\ell_e(t)\,dt$ for every edge and every $x>0$, with $\alpha\ge1$, then

$$C(f)\le\alpha\,C(f^*)\quad\text{for every Nash flow } f \text{ and feasible } f^* .$$

Significance

The result. Corollary 2.8 was, according to the authors, the first bound of its kind for polynomial latencies (p. 11). It shows that for the latency functions used in practice (the Bureau of Public Roads function $\ell(x)=a+bx^4$ has $p=4$) uncoordinated routing loses at most a bounded factor, independent of the network size, the number of commodities and the rates. Corollary 2.7 isolates the mechanism: a single scalar property of each latency function, how far the cost $x\ell(x)$ can exceed the potential $\int_0^x\ell$, controls the efficiency loss of the whole network.

Formalizing it. The results are proved in the paper (and the bound $p+1$ has since been sharpened); none of them is machine-checked on the platform. The mission produces a reusable Lean development of nonatomic selfish routing: Definition 2.1 in its deviation form, its equivalence with the Wardrop condition, the Beckmann characterization of equilibria with an honest integral potential, existence and cost-uniqueness of equilibria, and the potential-based efficiency bound. The same layer is used by the companion missions on the bicriteria bound and the $4/3$ bound for linear latencies.

Difficulty

The bound itself is a short chain of inequalities once the equilibrium is known to minimize the potential $\Phi$. That step is the substance: it requires showing that the Wardrop condition is a first-order optimality condition of a convex program over the polytope of feasible flows, with latencies that are only continuous, so $\Phi$ is differentiable but its derivative may have kinks. Passing from Definition 2.1 (finite deviations) to the Wardrop condition needs a limit $\delta\to0$, which fails without continuity of the latencies. Mathlib has no Karush–Kuhn–Tucker theory for such programs, so the optimality characterization has to be built from first principles.

Formalization scope

• Encoding. Edges, routes and commodities are Fin J, Fin R, Fin Sd. Edge flows, feasibility, the Wardrop condition and the potential $\Phi$ are the published KellyStochasticNetworks.linkFlow, wardropFeasible, IsWardropEquilibrium and wardropObjective, reused unchanged.
• Routes, not graphs. Routes are arbitrary $0/1$ incidence columns rather than the simple $s_i$–$t_i$ paths of a graph, a generalization the paper's arguments never use. Two copies of one path serving two commodities are two routes.
• Definition 2.1 is read with $P_1\ne P_2$ and $f_{P_1}>0$. As printed, $P_1=P_2$ makes the condition fail for strictly increasing latencies, and $f_{P_1}=0$ forces unused routes to have the same latency as used ones; either reading would make Nash flows nonexistent in simple instances.
• Latencies are nonnegative, nondecreasing and continuous on $[0,\infty)$ only. Continuity replaces the paper's differentiability, as its footnote 3 allows; it also makes $\int_0^x\ell_e$ a genuine integral.
• Rates are positive. In Lemma 2.6's existence part every commodity must be served by a route, the route-encoding meaning of "an instance".
• No ratios. Every bound $\rho\le c$ is stated as $C(f)\le c\,C(f^*)$ for every feasible $f^*$, which is what each proof shows and which avoids division by a zero cost.
• Polynomials share one degree bound $p\ge1$; leading coefficients may vanish; coefficients are required nonnegative for $i\le p$.

A statement in which Nash flows cannot exist (the literal Definition 2.1), or in which $\int_0^x\ell_e$ is the junk value of a non-integrable function, would make the goal vacuous; the guards above rule both out, and the sorry-free check that two small instances admit Nash flows confirms it.

Contributions welcome: proofs of the milestones, in particular the first-order characterization of minimizers of $\Phi$ over the feasible polytope, which is reusable for every potential game on flows.

Selected references

• T. Roughgarden and É. Tardos, How Bad is Selfish Routing?, J. ACM 49(2):236–259, 2002. https://doi.org/10.1145/506147.506153
• M. Beckmann, C. B. McGuire and C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956 (RAND RM-1488). https://www.rand.org/pubs/research_memoranda/RM1488.html
• S. C. Dafermos and F. T. Sparrow, The traffic assignment problem for a general network, J. Res. Nat. Bur. Standards 73B(2):91–118, 1969. https://doi.org/10.6028/jres.073B.010
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proc. Inst. Civil Engineers, Part II, 1:325–378, 1952. https://doi.org/10.1680/ipeds.1952.11259
• E. Koutsoupias and C. Papadimitriou, Worst-case equilibria, STACS 1999, LNCS 1563, 404–413. https://doi.org/10.1007/3-540-49116-3_38
• T. Roughgarden, The price of anarchy is independent of the network topology, J. Comput. System Sci. 67(2):341–364, 2003. https://doi.org/10.1016/S0022-0000(03)00044-8