Operations Research

Motivation

A system that processes a stream of tasks can often be configured in several ways, and the configuration affects both the cost of the current task and the cost of switching before the next one: paging schemes, replicated files, server placements. When the future is unknown, the natural worst-case yardstick is competitive analysis, introduced by Sleator and Tarjan for list update and paging (Sleator–Tarjan 1985): an on-line strategy is compared with the optimal strategy that knows the whole input in advance.

Borodin, Linial and Saks (J. ACM 1992; conference version STOC 1987) proposed metrical task systems as a single model containing all such problems, and determined the exact deterministic competitive ratio of every such system. Their theorem is the starting point of the on-line-algorithms literature on metrical task systems, the $k$-server problem (Manasse–McGeoch–Sleator 1990) and their randomized variants.

Timeline. 1985: Sleator and Tarjan introduce competitive analysis for paging and list update. 1987: Borodin, Linial and Saks prove $w(S,d)=2n-1$ for every $n$-state metrical task system (journal version 1992). 1990: Manasse, McGeoch and Sleator extend the task-system model to restricted task sets and pose the $k$-server conjecture. The randomized ratio of the uniform task system, bounded in the same paper between $H(n)$ and $2H(n)$, is the subject of the companion mission.

Setting

A task system $(S,d)$ has a finite set $S$ of $n$ states and a transition-cost matrix $d$ with $d(i,i)=0$, $d(i,j)>0$ for $i\neq j$, and the triangle inequality $d(i,j)+d(j,k)\ge d(i,k)$. It is metrical if also $d(i,j)=d(j,i)$.

A task $T$ is a vector of nonnegative processing costs $T(s)$, $s\in S$. Given a task sequence $\mathbf T=T^1\cdots T^m$ and an initial state $s_0$, a schedule is a map $\sigma:\{0,\dots,m\}\to S$ with $\sigma(0)=s_0$; task $T^i$ is processed in state $\sigma(i)$, and the cost is

$$c(\mathbf T;\sigma)=\sum_{i=1}^m d(\sigma(i-1),\sigma(i))+\sum_{i=1}^m T^i(\sigma(i)).$$

The off-line optimum $c_0(\mathbf T)$ is the minimum over all schedules. An on-line algorithm $A$ chooses $\sigma(i)$ knowing only $s_0$ and $T^1,\dots,T^i$; its cost is $c_A(\mathbf T)$. For $w>0$, $A$ is $w$-competitive if there is a constant $K_w$ with $c_A(\mathbf T)\le w\,c_0(\mathbf T)+K_w$ for every finite task sequence. The competitive ratio of $A$ is $w(A)=\inf\{w: A\text{ is }w\text{-competitive}\}$, and the competitive ratio of the task system is $w(S,d)=\inf_A w(A)$.

For the upper bound the paper also uses continuous-time schedules, in which task $T^i$ occupies the interval $[i,i+1)$ and the scheduler may change state at any real time, paying $\int_i^{i+1}T^i(\sigma(t))\,dt$ for processing. For a general (possibly asymmetric) matrix $d$, the cycle offset ratio $\psi(d)$ is the maximum over closed walks $s_0,\dots,s_k=s_0$ of $\sum_i d(s_{i-1},s_i)\big/\sum_i d(s_i,s_{i-1})$; it equals $1$ when $d$ is symmetric.

Formalization targets

Goal: Theorem 1.1

For every metrical task system $(S,d)$ with $n$ states,

$$w(S,d)=2n-1 .$$

The value depends on $n$ only, not on the distances.

Milestones

• Lemma 2.1. If $c_0(T^1\cdots T^m)\to\infty$ along an infinite task sequence $\mathbf T$, then $w(A)\ge w_{\mathbf T}(A)=\limsup_m c_A/c_0$.
• Theorem 2.2. Against the cruel taskmaster $M(\varepsilon)$, which charges $\varepsilon$ in the state the algorithm currently occupies,

$$w_{\mathbf T(\varepsilon)}(A)\ge\frac{2n-1}{1+\varepsilon/\min_{i\neq j}d(i,j)} .$$

• Lemma 3.1. Every on-line continuous-time algorithm is matched, on every task sequence, by an on-line discrete-time algorithm.
• Lemmas 6.3, 6.4, 6.2. Properties of the functions $f_k$ that drive the algorithm $A^*_d$: $f_k(s)-f_k(s')\le d(s',s)$; the identity $2\sum_{s\ne s_k}f_k(s)+f_k(s_k)=C_{k-1}+\sum_{i\le k}d(s_i,s_{i-1})$; and $f_k\le h_k$, the off-line cost at the $k$-th transition time.
• Theorem 6.1 (= Theorem 1.2). For every task system, symmetric or not, $A^*_d$ has competitive ratio at most $(2n-1)\psi(d)$.

Significance

The theorem settles the deterministic competitive ratio of the whole class of metrical task systems: the lower bound says that no deterministic on-line strategy can beat $2n-1$ on any metric, and the upper bound supplies one algorithm that achieves it on every metric. For asymmetric costs the same algorithm gives $(2n-1)\psi(d)$. The $2n-1$ lower bound is also the benchmark against which restricted models, such as paging and the $k$-server problem, measure their improvements, and the randomized question it leaves open drove much of the later work on metrical task systems.

The result was proved in 1987 and is standard; to the best of our knowledge no machine-checked proof exists. A formal development would provide a reusable model of deterministic on-line algorithms and competitiveness (on-line maps from task prefixes, additive competitiveness, infima over algorithms), an adversary construction by mutual recursion with an arbitrary algorithm, and an exact treatment of continuous-time schedules with piecewise-constant task costs. These pieces are reusable for other competitive-analysis results.

Difficulty

The lower bound is not a single bad input: the adversary is built from the algorithm it plays against, so the hard task sequence exists only as a recursion interleaved with the algorithm's choices, and the bound must hold for every deterministic on-line map, including ones that behave erratically. Obtaining the exact constant $2n-1$, rather than some $\Omega(n)$ bound, requires a sharp estimate of the off-line cost of that sequence.

The upper bound needs an algorithm defined in continuous time, whose transition times are determined by accumulated processing costs; the budgets can be zero, so transitions can be instantaneous, and a formal cost must remain well defined before one knows that only finitely many transitions occur. Relating the off-line cost function at those times to the recursively defined $f_k$ (Lemma 6.2) requires reasoning about all continuous-time off-line schedules. Finally, the goal combines both directions through infima over all on-line algorithms, and the discretization of Lemma 3.1 must be composed with the continuous-time algorithm.

Formalization scope

States form a finite type S (Fintype, DecidableEq, Nonempty); the goal is stated for all $n\ge1$, where $n=1$ gives $w(S,d)=1$. Task costs are finite nonnegative reals; the paper also allows $+\infty$ entries, which are excluded (this affects neither bound). A task sequence is T : Fin m → S → ℝ, with T i the paper's $T^{i+1}$, and a schedule is σ : Fin (m+1) → S. An on-line algorithm is a map sending $(s_0,[T^1,\dots,T^i])$ to $\sigma(i)$, so on-line behaviour is built into the type. Competitiveness is written additively, $c_A\le w\,c_0+K$, with $K$ independent of the task sequence and of $s_0$.

The competitive ratio competitiveRatio d is the real infimum of the set of all $w$ for which some on-line algorithm is $w$-competitive. It is not defined as an infimum of per-algorithm real infima: a non-competitive algorithm has $W_A=\emptyset$, whose real infimum is $0$, and that would drag $w(S,d)$ to $0$ for every system. Since the goal's value $2n-1$ is at least $1$ while the empty set's real infimum is $0$, the goal cannot hold vacuously.

Continuous-time algorithms are given as lists of $(\text{state},\text{length})$ pieces per unit interval; processing integrals are exact finite sums. The algorithm $A^*_d$ minimizes over states different from the current one, as its proof requires (the printed rule ranges over all states, and would stall); ties are left arbitrary. Its budgets may be $0$, its entry times are Option ℝ, and its cost is a sum in $[0,\infty]$, so that Theorem 6.1 itself asserts that only finitely many transitions occur. The ratio $\psi(d)$ excludes closed walks that never move, and Theorems 2.2 and 6.1 require $n\ge2$, where $\min_{i\ne j}d(i,j)$ and $\psi(d)$ are defined. Lemma 3.1 is stated comparing $A$ with $A'$ (the printed statement says "as well as $A$").

A complete development needs: the discrete model and off-line optimum (finite minimum over schedules), limsup arguments in EReal, continuous-time schedules with piecewise-constant costs, and the recursion defining $A^*_d$. Proofs of any milestone, including the purely combinatorial Lemmas 6.3 and 6.4, are welcome, as is a formal composition of Lemma 3.1 with Theorem 6.1.

Selected references

• A. Borodin, N. Linial, M. E. Saks, An optimal on-line algorithm for metrical task system, Journal of the ACM 39(4):745–763, 1992. https://doi.org/10.1145/146585.146588
• D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Communications of the ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive algorithms for server problems, Journal of Algorithms 11(2):208–230, 1990. https://doi.org/10.1016/0196-6774(90)90003-W

Motivation

Minimizing a smooth function over a closed convex set $\Omega\subseteq\mathbb R^n$ on which projection is cheap (a box, a ball, a simplex) is a routine subproblem in large-scale optimization: box-constrained minimization is the inner solver of augmented Lagrangian methods, and bound-constrained least squares, image restoration and density estimation all have this form. The classical projected gradient method of Goldstein and of Levitin and Polyak is simple and needs only gradients and projections, but with constant or Armijo-type step lengths it is slow.

Spectral projected gradient (SPG) methods, introduced by Birgin, Martínez and Raydan (paper), combine three ingredients: the projected gradient direction; the Barzilai–Borwein (spectral) step length $\alpha_{k+1}=\langle s_k,s_k\rangle/\langle s_k,y_k\rangle$, an inverse Rayleigh quotient of the average Hessian along the last step; and the nonmonotone line search of Grippo, Lampariello and Lucidi, which compares a trial value with the worst of the last $M$ objective values instead of the current one. The method is widely used in practice, and its analysis is the template for many later nonmonotone projected methods.

Timeline:

• 1964–1966: Goldstein; Levitin and Polyak introduce gradient projection.
• 1976: Bertsekas analyses the Armijo rule along the projection arc.
• 1986: Grippo, Lampariello and Lucidi introduce the nonmonotone line search for unconstrained problems.
• 1988: Barzilai and Borwein propose the two-point step size; Raydan (1993, 1997) proves convergence for quadratics and combines it with nonmonotone search in the unconstrained case.
• 2000: Birgin, Martínez and Raydan define SPG1 and SPG2 for convex constraints (SIAM J. Optim. 10(4)).
• 2003: the same authors publish the convergence proof that Theorem 2.1 refers to, in the inexact setting (IMA J. Numer. Anal. 23).

Setting

Let $\Omega\subseteq\mathbb R^n$ be nonempty, closed and convex, with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $f$ have continuous partial derivatives on an open set $U\supseteq\Omega$ and write $g(x)=\nabla f(x)$. The orthogonal projection $P(z)$ is the unique point of $\Omega$ nearest to $z$. The scaled projected gradient is $g_t(x)=P(x-t\,g(x))-x$ for $x\in\Omega$, $t>0$. A point $\bar x$ is a constrained stationary point if $\langle g(\bar x),x-\bar x\rangle\ge0$ for all $x\in\Omega$.

The parameters are an integer $M\ge1$, reals $0<\alpha_{\min}<\alpha_{\max}$, a sufficient-decrease constant $\gamma\in(0,1)$ and safeguards $0<\sigma_1<\sigma_2<1$. Algorithm SPG2 starts from $x_0\in\Omega$ and $\alpha_0\in[\alpha_{\min},\alpha_{\max}]$ and at iteration $k=0,1,\dots$:

1. Stop test. If $\|P(x_k-g(x_k))-x_k\|=0$, stop: $x_k$ is stationary.
2. Backtracking. Set $d_k=P(x_k-\alpha_k g(x_k))-x_k$ and $\lambda=1$. While

$$f(x_k+\lambda d_k)\le\max_{0\le j\le\min\{k,M-1\}}f(x_{k-j})+\gamma\lambda\langle d_k,g(x_k)\rangle\qquad(3)$$

fails, replace $\lambda$ by any $\lambda_{\rm new}\in[\sigma_1\lambda,\sigma_2\lambda]$. When (3) holds, $\lambda_k=\lambda$ and $x_{k+1}=x_k+\lambda_kd_k$. 3. Spectral step. With $s_k=x_{k+1}-x_k$, $y_k=g(x_{k+1})-g(x_k)$, $b_k=\langle s_k,y_k\rangle$: $\alpha_{k+1}=\alpha_{\max}$ if $b_k\le0$, else $\alpha_{k+1}=\min\{\alpha_{\max},\max\{\alpha_{\min},\langle s_k,s_k\rangle/b_k\}\}$.

In Lean the projection is a function P with the predicate IsProjOnto Ω P, $g_t$ is scaledProjGrad P f t, stationarity is IsConstrainedStationary Ω f, the maximum in (3) is nonmonotoneRef f x M k, and an infinite run is IsSPG2Run Ω f P M αmin αmax γ σ₁ σ₂ x α.

Formalization targets

Goal: Theorem 2.1, accumulation points are stationary

For every infinite run $(x_k,\alpha_k)$ of SPG2 and every accumulation point $\bar x$ of $(x_k)$,

$$\langle g(\bar x),x-\bar x\rangle\ge0\qquad\text{for all }x\in\Omega.$$

The statement fixes no parameter values and assumes neither convexity of $f$ nor a bounded level set.

Milestones

• Lemma 2.1 (ii). For $\bar x\in\Omega$ and $t\in(0,\alpha_{\max}]$: $g_t(\bar x)=0$ iff $\bar x$ is a constrained stationary point.
• Lemma 2.1 (i). For $x\in\Omega$ and $t\in(0,\alpha_{\max}]$:

$$\langle g(x),g_t(x)\rangle\le-\tfrac1t\|g_t(x)\|_2^2\le-\tfrac1{\alpha_{\max}}\|g_t(x)\|_2^2.$$

• Theorem 2.1, first clause (SPG2 is well defined). At a point where Step 1 does not stop, every admissible backtracking sequence reaches a step satisfying (3). The step is stated for an arbitrary reference value $R\ge f(x)$, which covers the maximum in (3).
• Section 2, p. 4. The iterates remain in $\Omega_0=\{x\in\Omega:f(x)\le f(x_0)\}$.

Significance

Theorem 2.1 is the global convergence guarantee for SPG2. It holds without monotone decrease of $f$ and without any restriction on the spectral step beyond the safeguards. These are the two features that make the method fast in practice, and together they mean that no classical monotone projected-gradient argument applies directly. The same statement underlies the convergence claims of the SPG software (ACM TOMS Algorithm 813) and of the many methods that reuse the nonmonotone spectral framework: inexact SPG, augmented Lagrangian inner solvers, and projected BB methods for machine learning.

Status: the theorem is proved in the literature. This paper's proof reads "See [7]", a pointer to Birgin, Martínez and Raydan (2003). No Lean formalization of this theorem, of the nonmonotone Armijo analysis, or of the projected-gradient stationarity lemma is known. The mission produces a formal proof and a reusable Lean interface for projection-based first-order methods on convex sets.

Difficulty

The obvious argument for monotone descent methods is to show that $f(x_k)$ decreases, so that the total decrease is finite and the per-iteration decrease $\gamma\lambda_k|\langle d_k,g(x_k)\rangle|$ tends to zero. Here $f(x_k)$ need not decrease. Only the reference value $\max_{0\le j\le\min\{k,M-1\}}f(x_{k-j})$ is nonincreasing, and a small decrease of this maximum along the whole sequence does not by itself give a small decrease at the iterates that approach a given accumulation point $\bar x$. A second difficulty is that the accepted step lengths $\lambda_k$ may tend to zero along the subsequence, while $f$ is $C^1$ only on a neighbourhood of $\Omega$ and no Lipschitz constant for $g$ is available, so no uniform sufficient-decrease estimate holds. The spectral steps $\alpha_k$ vary within $[\alpha_{\min},\alpha_{\max}]$, so the directions $d_k$ are not a fixed function of $x_k$.

Formalization scope

• Space and data. The space is EuclideanSpace ℝ (Fin n) with inner ℝ and the 2-norm. $f$ is a total function EuclideanSpace ℝ (Fin n) → ℝ with ContDiffOn ℝ 1 f U on an open U ⊇ Ω, and $g$ is Mathlib's gradient f. The algorithm evaluates $f$ and $g$ only at points of $\Omega$.
• Iteration and trials. Iterations are indexed from $0$. The backtracking choice (2) is universally quantified: a run carries, at each iteration, a finite trial list $\lambda^{(0)}=1$, $\lambda^{(i+1)}\in[\sigma_1\lambda^{(i)},\sigma_2\lambda^{(i)}]$, in which test (3) fails at every trial but the last and holds at the last.
• Step size. $\alpha_{k+1}$ is given by Step 3 exactly.
• Accumulation point. An accumulation point is MapClusterPt x̄ atTop x.
• Excluded simplifications. A run predicate that accepts any positive step, or lets $\alpha_{k+1}$ range freely over $[\alpha_{\min},\alpha_{\max}]$, is not SPG2. Nor is a goal stating $g_t(\bar x)=0$ instead of the variational inequality, or one that adds convexity of $f$, a Lipschitz gradient or a bounded level set.
• Non-vacuity. The hypotheses of the goal are satisfiable: for $f(x)=\|x\|^2$, $\Omega=\mathbb R^n$, $M=1$, $\alpha_{\min}=1/8$, $\alpha_{\max}=1/4$, $\gamma=1/2$ and $v\ne0$, the iterates $x_k=2^{-k}v$ with $\alpha_k=1/4$ form an infinite run with accumulation point $0$.
• Infrastructure. A complete development needs the variational characterization of the projection (Mathlib has it for the iInf form: norm_eq_iInf_iff_real_inner_le_zero), continuity properties of the projection, a mean-value estimate for $C^1$ functions on segments in $\Omega$, and the nonmonotone reference-value bookkeeping. The projection lemmas and the nonmonotone bookkeeping are reusable beyond this mission, in particular for the companion mission on SPG1, and contributions of them as separate lemmas are welcome.

Selected references

• E. G. Birgin, J. M. Martínez, M. Raydan, Nonmonotone spectral projected gradient methods on convex sets, SIAM J. Optim. 10(4) (2000) 1196–1211; authors' updated version, July 2004. https://doi.org/10.1137/S1052623497330963, https://www.ime.unicamp.br/~martinez/bmr.pdf
• E. G. Birgin, J. M. Martínez, M. Raydan, Inexact spectral projected gradient methods on convex sets, IMA J. Numer. Anal. 23 (2003) 539–559. https://doi.org/10.1093/imanum/23.4.539
• J. Barzilai, J. M. Borwein, Two-point step size gradient methods, IMA J. Numer. Anal. 8 (1988) 141–148. https://doi.org/10.1093/imanum/8.1.141
• L. Grippo, F. Lampariello, S. Lucidi, A nonmonotone line search technique for Newton's method, SIAM J. Numer. Anal. 23 (1986) 707–716. https://doi.org/10.1137/0723046
• M. Raydan, The Barzilai and Borwein gradient method for the large scale unconstrained minimization problem, SIAM J. Optim. 7 (1997) 26–33. https://doi.org/10.1137/S1052623494266365
• D. P. Bertsekas, On the Goldstein–Levitin–Polyak gradient projection method, IEEE Trans. Automat. Control 21 (1976) 174–184. https://doi.org/10.1109/TAC.1976.1101194

Motivation

Robust optimization protects a decision against every scenario in an uncertainty set. When the uncertain data are probabilities, a natural uncertainty set is a ball around a nominal distribution measured by a φ-divergence (Kullback–Leibler, Burg entropy, χ², Hellinger and others). Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) show that the robust counterpart of a linear constraint over such a set is a finite convex system, and then ask whether that system is computationally tractable: can an interior-point method solve it in polynomial time?

For the Burg and Kullback–Leibler divergences the reformulated constraints (Eqs. (29) and (32) of the paper) have the shape $\lambda f(s_i/\lambda)\le\dots$, a perspective constraint. Polynomial-time solvability by interior-point methods follows once the constraint set carries a self-concordant barrier in the sense of Nesterov and Nemirovski (Interior-Point Polynomial Algorithms in Convex Programming, SIAM 1994). Theorem 2 of the paper supplies such a barrier for every perspective constraint whose generating function satisfies a one-dimensional differential inequality. The same question arises for perspective and relative-entropy cones in conic optimization generally, so the criterion is of interest beyond φ-divergences.

Setting

A function $\varphi:F\to\mathbb R$ on an open convex set $F\subseteq\mathbb R^n$ is $\kappa$-self-concordant ($\kappa\ge0$) if it is three times continuously differentiable on $F$ and for every $y\in F$ and every direction $h\in\mathbb R^n$

$$\bigl|\nabla^3\varphi(y)[h,h,h]\bigr|\le 2\kappa\,\bigl(h^{\mathsf T}\nabla^2\varphi(y)h\bigr)^{3/2},$$

where $\nabla^k\varphi(y)[h,\dots,h]$ is the $k$-th differential of $\varphi$ at $y$ in direction $h$ (Definition 1, p. 350). In Lean this is PhiDivRobust.Barrier.IsSelfConcordant κ F φ.

Let $f$ be a real function on $(0,\infty)$. Its perspective is $g(s,y)=y\,f(s/y)$ for $s,y>0$ (perspective f). The constraint set (34) is

$$\{(s,y,z):\ y f(s/y)\le z,\ s\ge0,\ y\ge0\},$$

and its logarithmic barrier (35) is

$$\varphi_B(s,y,z)=-\ln\bigl(z-yf(s/y)\bigr)-\ln s-\ln y$$

(logBarrier f), finite on the open set $F_f=\{(s,y,z): s>0,\ y>0,\ yf(s/y)<z\}$ (barrierDomain f). Directions are $h=(h_1,h_2)$ for $g$, with $h_1$ along $s$ and $h_2$ along $y$, and $h\in\mathbb R^3$ for $\varphi_B$.

Formalization targets

Goal: Theorem 2 (p. 350)

If $f$ is convex on $(0,\infty)$ and, for some $\kappa>0$,

$$|f'''(s)|\le\kappa\,\frac{f''(s)}{s}\qquad(s>0),\tag{33}$$

then $\varphi_B$ is $\bigl(2+\tfrac{\sqrt2}{3}\kappa\bigr)$-self-concordant on $F_f$.

Milestones (the displayed steps of the proof)

1. Eq. (37): $\nabla^2 g(s,y)[h,h]=f''(s/y)\bigl(h_1^2/y-2sh_1h_2/y^2+s^2h_2^2/y^3\bigr)$.
2. The third differential of $g$ in terms of $f''(s/y)$ and $f'''(s/y)$.
3. Under (33), inequality (36) with $\beta=3+\kappa\sqrt2$:

$$\bigl|\nabla^3 g(s,y)[h,h,h]\bigr|\le\beta\,h^{\mathsf T}\nabla^2 g(s,y)h\,\sqrt{h_1^2/s^2+h_2^2/y^2}.$$

4. Lemma A.2 of den Hertog (1994), as quoted in the proof: if (36) holds with $\beta\ge0$, then $\varphi_B$ is $(1+\beta/3)$-self-concordant on $F_f$.

Milestones 3 and 4 give the goal, since $1+\tfrac13(3+\kappa\sqrt2)=2+\tfrac{\sqrt2}{3}\kappa$. A further item records the paper's application: $f(s)=-\log s$ (the Burg case) satisfies (33) with $\kappa=2$.

Significance

The result. Theorem 2 turns a two-line calculus check on a scalar function into a certificate of polynomial-time solvability for a three-dimensional convex constraint. The paper uses it to conclude that the robust counterparts for the Burg entropy and Kullback–Leibler uncertainty sets are tractable, and the criterion applies to any other convex $f$ satisfying (33); for example $f(s)=s\log s$ satisfies it with $\kappa=1$, which covers the relative-entropy cone. The constant $2+\tfrac{\sqrt2}{3}\kappa$ enters the complexity bound of any path-following method through the barrier parameter.

Formalizing it. The theorem is proved in the paper, but the decisive step is delegated to Lemma A.2 of den Hertog's monograph, which in turn belongs to the compatibility theory of Nesterov and Nemirovski. As far as is known none of these statements has a machine-checked proof. The mission produces a checked version of the compatibility lemma for perspective constraints, which is reusable for any barrier of the form $-\ln(z-g)-\ln s-\ln y$, together with explicit second- and third-differential formulas for perspectives in Mathlib's iteratedFDeriv language. The printed third-differential display contains a typo (see below); the formal statements fix it.

Difficulty

The differential identities (milestones 1 and 2) are routine but heavy: they require computing iterated Fréchet derivatives of a composition with a quotient in two variables and matching them with one-variable iterated derivatives of $f$. The inequality (milestone 3) is elementary real-variable algebra once the differentials are available.

The central difficulty is den Hertog's lemma. The obvious approach, bounding the three terms of $\nabla^3\varphi_B$ separately against $(\nabla^2\varphi_B)^{3/2}$, fails: the cross term $-3\,(\nabla\omega\cdot h)\,\nabla^2 g[h,h]/\omega^2$ with $\omega=z-g$ couples the first and second differentials, and bounding it separately loses the constant $1+\beta/3$. A further practical difficulty is that $F_f$ is open and convex only because the perspective of a convex function is jointly convex and continuous, which must itself be established.

Formalization scope

Points are $(s,y,z)\in\mathbb R\times\mathbb R\times\mathbb R$ and directions for $g$ are in $\mathbb R\times\mathbb R$. Differentials are iteratedFDeriv ℝ k applied to the constant tuple $(h,\dots,h)$; $f''$ and $f'''$ are iteratedDeriv 2 f and iteratedDeriv 3 f. The power $x^{3/2}$ is Real.rpow, which is $0$ for $x<0$; this makes the Lean definition of self-concordance no weaker than the paper's. Real.log and division have junk values outside $F_f$, but $F_f$ is open, so no differential at a point of $F_f$ sees them.

Committed conventions and disclosed deviations:

• "$f:\mathbb R^+\to\mathbb R$" is read as $f$ convex on the open half-line $(0,\infty)$; the Burg case $f=-\log$ is undefined at $0$, and $f$ is only evaluated at $s/y$ with $s,y>0$.
• $f$ is assumed $C^3$ on $(0,\infty)$. The page does not say so, but (33) uses $f'''$ and Definition 1 requires the barrier to be $C^3$.
• The printed third-differential display ends in $s^3h_x^3/y^5$; the correct term is $s^3h_2^3/y^5$, and the Lean statement uses it. The milestone text keeps the printed version.
• Lemma A.2 is stated with $\beta\ge0$ added. The quoted text says "if there exists a $\beta$", which is false for $\beta<0$: with $f\equiv0$, (36) holds for every $\beta$ and $\beta=-3$ would give a $0$-self-concordant $-\ln z-\ln s-\ln y$. The goal uses $\beta=3+\kappa\sqrt2>0$ and is unaffected.

A trivializing formalization is excluded. The self-concordance predicate requires $C^3$ regularity and quantifies over all directions $h\in\mathbb R^3$, the domain is exactly $F_f$ (not a subset such as $\emptyset$), and $\kappa>0$ is as printed. The constant of the conclusion is tied to the same $\kappa$ as in (33).

Useful infrastructure, reusable beyond this mission: iterated derivatives of perspectives, joint convexity of perspectives, and the calculus of self-concordance (sums, $-\ln$ of a concave function composed with an affine map). Proofs of the milestones independently of the goal are welcome, as are proofs of the Burg item's consequence and of the analogous statement for $f(s)=s\log s$.

Selected references

• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
• D. den Hertog, Interior Point Approach to Linear, Quadratic and Convex Programming: Algorithms and Complexity, Kluwer Academic Publishers, 1994. https://doi.org/10.1007/978-94-011-1134-8
• Yu. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. https://doi.org/10.1137/1.9781611970791

Motivation

Many decision problems contain a constraint whose coefficients are an expectation under a probability vector that is not known exactly: an expected cost under uncertain scenario probabilities, an expected payoff of an asset under an estimated distribution, the expected demand in a newsvendor model. The probabilities are usually estimated from data, and a solution that is feasible for the estimate can be infeasible for the true distribution. Robust optimization protects against this by requiring the constraint to hold for every probability vector in an uncertainty region around the estimate.

A natural region is a ball in a φ-divergence, a family of statistical distances between probability vectors that contains the Kullback–Leibler divergence, the Burg entropy, the χ² distances, the Hellinger distance and the variation distance. Such balls arise as asymptotic confidence sets for the true distribution given observed frequencies (Pardo 2006), so the radius has a statistical meaning. Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) showed that the robust version of a linear constraint over such a ball is equivalent to a finite convex system involving the convex conjugate of φ. This reformulation is a standard tool in the later literature on distributionally robust optimization.

Setting

A φ-divergence function is a function $\phi:\mathbb R\to\mathbb R\cup\{+\infty\}$ that is convex on $[0,\infty)$, finite on $(0,\infty)$, and satisfies $\phi(1)=0$; the value $\phi(0)$ may be $+\infty$. Examples are $\phi(t)=t\log t-t+1$ (Kullback–Leibler), $\phi(t)=-\log t+t-1$ (Burg), $\phi(t)=(t-1)^2$ (modified χ²) and $\phi(t)=|t-1|$ (variation). For $p,q\in\mathbb R^m$ with $q>0$ the φ-divergence is

$$I_\phi(p,q)=\sum_{i=1}^m q_i\,\phi\!\left(\frac{p_i}{q_i}\right),$$

and the conjugate of $\phi$ is $\phi^*(s)=\sup_{t\ge0}\{st-\phi(t)\}$, a function with values in $\mathbb R\cup\{+\infty\}$.

Fix $a\in\mathbb R^n$, $B\in\mathbb R^{n\times m}$ with columns $b_i$, $\beta\in\mathbb R$, $C\in\mathbb R^{k\times m}$ with columns $c_i$, $d\in\mathbb R^k$, a nominal vector $q\in\mathbb R^m$ and a radius $\rho>0$. The uncertainty region is

$$U=\{p\in\mathbb R^m\mid p\ge0,\ Cp\le d,\ I_\phi(p,q)\le\rho\},$$

where the linear constraints $Cp\le d$ can encode $e^\top p=1$ and any further information on $p$. A decision $x\in\mathbb R^n$ satisfies the robust linear constraint if

$$(a+Bp)^\top x\le\beta\qquad\text{for all }p\in U. \tag{11}$$

Inequalities between vectors are componentwise throughout.

Formalization targets

Goal: Theorem 1

Assume $q>0$ and $q\in U$. Then $x$ satisfies (11) if and only if there are $\eta\in\mathbb R^k$ and $\lambda\in\mathbb R$ with

$$a^\top x+d^\top\eta+\rho\lambda+\lambda\sum_{i}q_i\,\phi^*\!\left(\frac{b_i^\top x-c_i^\top\eta}{\lambda}\right)\le\beta,\qquad\eta\ge0,\ \lambda\ge0, \tag{13}$$

where $0\phi^*(s/0):=0$ for $s\le0$ and $0\phi^*(s/0):=+\infty$ for $s>0$. The statement fixes no constants and no particular φ; it holds for the whole class.

Milestones

The proof in the paper has three displayed steps, which are the milestones. With the Lagrange function $L(p,\lambda,\eta)=(a+Bp)^\top x+\rho\lambda-\lambda I_\phi(p,q)+\eta^\top(d-Cp)$ and the dual objective $g(\lambda,\eta)=\sup_{p\ge0}L(p,\lambda,\eta)$:

1. Closing identity. For $\lambda\ge0$, $(\lambda\phi)^*(s)=\sup_{t\ge0}\{st-\lambda\phi(t)\}$ equals $\lambda\phi^*(s/\lambda)$, with the convention above at $\lambda=0$.
2. Eq. (15). For $q>0$ and $\lambda\ge0$,

$$g(\lambda,\eta)=a^\top x+d^\top\eta+\rho\lambda+\sum_{i=1}^m q_i(\lambda\phi)^*(b_i^\top x-c_i^\top\eta).$$

3. Duality. Under the hypotheses of Theorem 1, $x$ satisfies (11) if and only if $g(\lambda,\eta)\le\beta$ for some $\lambda\ge0$, $\eta\ge0$. This is split into the weak-duality direction and the strong-duality direction with attainment.

An additional item states Corollary 1, the specialization to $U=\{p\ge0,\ e^\top p=1,\ I_\phi(p,q)\le\rho\}$, where the multiplier $\eta\in\mathbb R$ of the normalization is free in sign.

Significance

Theorem 1 turns a semi-infinite constraint, one inequality for each $p$ in a convex set, into a single convex inequality in $(x,\lambda,\eta)$. The left side of (13) is jointly convex because $\lambda\phi^*(s/\lambda)$ is the perspective of a convex function. For the divergences of Table 4 of the paper the conjugate has a closed form, and the robust constraint becomes a linear, conic quadratic or self-concordant-barrier-representable constraint. The paper's applications (robust asset pricing, a robust newsvendor, and the tractability results of its §5) all start from this theorem, as do its Corollaries 2–5.

The theorem is proved in the paper; no machine-checked proof of it is known. Formalizing it adds a checked robust-counterpart theorem for φ-divergence regions, a reusable encoding of φ-divergences with extended values, and a strong-duality statement with attainment for convex programs whose constraint function takes the value $+\infty$ on the boundary of the orthant. It also records a correction: the paper states the theorem for $q\ge0$, and that version is false (see Formalization scope).

Difficulty

The separation step (15) and the conjugate identity are elementary manipulations of suprema, but in extended arithmetic: $\phi$ may be $+\infty$ at $0$, the conjugate may be $+\infty$, and the case $\lambda=0$ follows its own convention. The central difficulty is the duality step. The worst-case problem is a convex program whose constraint $I_\phi(p,q)\le\rho$ is not a finite convex function on a closed set: for the Burg or χ² divergence it is $+\infty$ on the boundary of the orthant, and $U$ itself need not be closed. Textbook statements of Slater-type strong duality usually assume finite-valued convex functions on a closed domain, so they do not apply as stated. The statement also requires attainment of the dual minimum, not only the absence of a duality gap, and this is the part a naive limiting argument does not give.

Formalization scope

Conventions:

• Vectors are Fin n → ℝ with the componentwise order; $B$ and $C$ are Matrix (Fin n) (Fin m) ℝ and Matrix (Fin k) (Fin m) ℝ; $b_i$ and $c_i$ are the columns fun j => B j i and fun j => C j i.
• $\phi$ is ℝ → EReal, never $-\infty$, finite on $(0,\infty)$, with $\phi(1)=0$ and convexity on $[0,\infty)$ written out in EReal. $\phi(0)=+\infty$ is allowed, so the Burg, χ² and J divergences are covered.
• $I_\phi(p,q)$, $\phi^*$, $(\lambda\phi)^*$, $L$, $g$ and the left side of (13) are EReal-valued. $\lambda\phi(t)$ is the EReal product, in which $0\cdot(+\infty)=0$. The term $\lambda\phi^*(s/\lambda)$ is defined by an explicit case split at $\lambda=0$, and $\lambda\sum_i q_i\phi^*(\cdot/\lambda)$ in (13) is read as $\sum_i q_i\,(\lambda\phi^*(\cdot/\lambda))$ with the convention applied term by term.
• The paper's $\max_{p\ge0}$ in $g$ is a supremum; $\min_{\lambda,\eta\ge0}g\le\beta$ is stated in its attained form, $\exists\,\lambda\ge0,\eta\ge0$ with $g(\lambda,\eta)\le\beta$.
• $m$ and $k$ may be $0$.

Corrected slip. The paper's standing assumption is $q\ge0$. The third equality of (15) substitutes $p_i=q_it$, which needs $q_i>0$, and Theorem 1 is false for $q\ge0$: with $m=k=2$, $n=1$, $\phi(t)=|t-1|$, $q=(1,0)$, both columns of $C$ equal to $(1,-1)^\top$, $d=(1,-1)$, $a=0$, $B=(0\ \ 1)$, $x=1$, $\rho=1$, $\beta=0$, the vector $p=(1/2,1/2)$ lies in $U$ and violates (11), while $\eta=0$, $\lambda=0$ satisfy (13). Every statement of the mission therefore assumes $q_i>0$ for all $i$. The hypothesis $q\in U$ (the paper's "such that $q\in U$") and $\rho>0$ are kept.

Ruled-out trivializations: a conjugate taken as a supremum over all $t\in\mathbb R$ of a real-valued φ with junk values at $t<0$ is a different function; computing the $\lambda=0$ term as $0\cdot\phi^*(s/0)$ with Lean's $s/0=0$ makes it identically $0$; a real-valued, everywhere finite φ silently excludes the Burg, χ² and J divergences; dropping $q\in U$ or $\rho>0$ removes the Slater point and changes the theorem. The mission's definitions avoid all four.

Needed infrastructure: suprema of EReal-valued families over half-lines and orthants, the interchange of a supremum over a product with a finite sum, and a Lagrangian strong-duality theorem with attainment for a convex program with finitely many affine inequality constraints and one convex, possibly infinite-valued, inequality constraint with a Slater point in the interior of its domain. That duality theorem, and the φ-divergence definitions, are reusable beyond this mission, in particular for the paper's Corollaries 2–5 and for other distributionally robust formulations. Contributions of any of these pieces as separate theorems are welcome.

Selected references

• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
• L. Pardo, Statistical Inference Based on Divergence Measures, Chapman & Hall/CRC, 2006. https://doi.org/10.1201/9781420034813
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Networks of queues model computer systems, communication networks and manufacturing lines: customers (jobs, packets, parts) move between service centers, wait, receive service and move on. Their equilibrium behaviour determines throughputs, utilizations and response times, and for most networks it can only be computed by solving the full balance equations of a continuous-time Markov chain whose state space grows combinatorially with the number of centers and customers. A product-form network is one whose equilibrium distribution factorizes over the centers; for such networks performance measures can be computed exactly by efficient algorithms (convolution, mean value analysis), and this is the basis of much of classical computer-performance modelling.

Timeline of the main product-form results:

• 1957–1963, Jackson (Oper. Res. 5, 1957; Manag. Sci. 10, 1963): open networks of exponential FCFS queues, one customer class, Poisson arrivals.
• 1967, Gordon and Newell (Oper. Res. 15): the closed single-class exponential case.
• 1975, Baskett, Chandy, Muntz and Palacios (J. ACM 22): several customer classes with class switching, four service disciplines (FCFS, processor sharing, infinite server, preemptive-resume LCFS), service times with rational Laplace transforms at the last three, and open, closed or mixed networks with state-dependent Poisson arrivals. This is the BCMP theorem, the subject of this mission.
• 1975–1979, Kelly (J. Appl. Prob. 12, 1975; Reversibility and Stochastic Networks, Wiley 1979): symmetric queues and quasi-reversibility, a general framework containing the BCMP disciplines.

Setting

A network has $N$ service centers and $R$ customer classes. A class-$r$ customer finishing service at center $i$ next requires center $j$ in class $s$ with probability $p_{i,r;j,s}$ and leaves the network with probability $1-\sum_{j,s}p_{i,r;j,s}$. The pairs $(i,r)$ are partitioned into subchains $E_1,\dots,E_m$ that routing never leaves. Each center has one of four types:

1. FCFS, with an exponential service time of rate $\mu_i$ common to all classes;
2. a single processor-sharing server (each of $n$ customers is served at rate $1/n$);
3. an infinite-server center;
4. a single preemptive-resume LCFS server.

At types 2–4 the class-$r$ service time is Coxian: $u_{ir}\ge1$ exponential stages of rates $\mu_{irl}$, and after stage $l$ the customer continues with probability $a_{irl}$ or finishes with probability $b_{irl}=1-a_{irl}$. The state $S=(x_1,\dots,x_N)$ records the FCFS order of classes at type 1, the number $m_{irl}$ of class-$r$ customers in stage $l$ at types 2 and 3, and the LCFS order of (class, stage) pairs at type 4. External arrivals are Poisson, either with rate $\lambda(M(S))$ depending on the total population $M(S)$ (process A) or with one stream per subchain of rate $\lambda_k(M(S/E_k))$ (process B); an arrival joins center $j$ in class $s$ with probability $q_{js}$. A subchain with $q\equiv0$ is closed and keeps a fixed population $K_k$.

With relative arrival rates $e_{ir}\ge0$ solving the traffic equations $\sum_{(i,r)}e_{ir}p_{i,r;j,s}+q_{js}=e_{js}$ and $A_{irl}=\prod_{j<l}a_{irj}$ (the probability of reaching stage $l$, stages numbered from 0), the paper defines $f_i(x_i)$ per center type and a factor $d(S)$ from the arrival rates.

Formalization targets

Goal: the BCMP theorem (§3.2, pp. 253–254)

$$\pi(S)=d(S)\,f_1(x_1)\,f_2(x_2)\cdots f_N(x_N)$$

satisfies the global balance equations of the network, and, under the paper's assumption that the equilibrium distribution is unique, every equilibrium distribution equals $\pi/Z$ whenever $Z=\sum_S\pi(S)$ is finite and positive. The goal covers all four center types, open, closed and mixed networks, and both arrival processes.

Milestones

• §3.1 (p. 252): independent balance implies global balance.
• §3.2 (p. 254): the product form satisfies the independent balance equations.
• §4.1 (p. 254): the aggregate-state probabilities are $C\,d(S)\,g_1(y_1)\cdots g_N(y_N)$.

A further supporting item, also from §4.1 (p. 254), states that summing $f_i$ over local states with fixed class counts gives $g_i$. So $g_i$ depends on the service times only through their means $1/\mu_{ir}=\sum_lA_{irl}/\mu_{irl}$.

Significance

The theorem places the four disciplines, class switching and mixed open/closed populations under one formula. Its corollary in §4.1, that aggregate probabilities depend on service time distributions only through their means (insensitivity), is what makes the model usable with measured mean service times, and it underlies the convolution and mean value analysis algorithms for normalizing constants.

The result is classical and proved on paper. As far as the platform's catalogue shows, it is not formalized: the platform has Kelly's single-class migration process with exponential service, a special case. A machine-checked BCMP theorem would provide a verified multiclass queueing-network model (states, event-driven transition rates, balance equations) on which later results can build: mean value analysis, the state-dependent rates of §5, and the open-network marginals of §4.2.

The printed statement contains an error. The paper defines $A_{irl}=\prod_{j=1}^{l}a_{irj}$ (p. 253). With the branching of its Figs. 1 and 3, this product includes the branch out of stage $l$. For exponential service ($u_{ir}=1$) it gives $A_{ir1}=a_{ir1}=0$, so every $f_i$ of a type 2–4 center with a customer present vanishes, and a closed network of such centers would have no normalizable solution. The mission states the corrected theorem with $A_{irl}=\prod_{j<l}a_{irj}$, which the mean-service-time identity of §4.1 also requires. The type-2 factor $1/m_{ikl}!$ is read as $1/m_{irl}!$.

Difficulty

The algebra of the paper's proof is local: each independent balance equation reduces to the traffic equations. The difficulty is in making that statement precise for a real state space. The independent balance equations need a consistent labelling of each moving customer by the "stage" it leaves and enters. That labelling has to cover FCFS centers, where per-class labels are inconsistent (p. 253), the outside world of each open subchain, and LCFS preemption. Every in-flow into a state is a sum over predecessor states, and those states differ by list operations (appending at an FCFS tail, pushing on an LCFS head) or by stage-count updates. The factorials in the processor-sharing and infinite-server factors, and the telescoping identity $\sum_lA_{irl}b_{irl}=1$ for departures, must line up exactly with the rates. The obvious shortcut is to check global balance directly for a single class with exponential service. That covers neither class switching, nor Coxian stages, nor mixed networks.

Formalization scope

Centers are Fin N, classes Fin R and subchains Fin m. The class-$r$ stages at center $i$ are Fin (u i r) with u i r : ℕ+, numbered from 0. A local state is an inductive type with three shapes (FCFS list, stage-count array, LCFS list of (class, stage) pairs). The state space is the subtype of configurations whose shapes match the center types and whose closed subchains hold their fixed populations. Transition rates are the sums of the rates of explicit events (arrivals, FCFS completions, stage moves and completions, LCFS moves and completions). Global balance uses tsum; every state has finitely many successors and predecessors with nonzero rate, so these sums are finite. The standing assumptions (substochastic routing closed on subchains, closed subchains with no arrivals and no departures, positive rates, continuation probabilities in $[0,1]$ vanishing at the last stage) are collected in Network.IsValid. Irreducibility of subchains is not assumed, and any nonnegative solution of the traffic equations is allowed. Under process B the product in $d(S)$ runs over open subchains only. Uniqueness of the equilibrium is a hypothesis, as in the paper. The type-1 rate is constant, and the state-dependent rates of Condition 1 and §5 are not covered.

The following formalizations would trivialize the mission and are ruled out: stating only global balance of $\pi$ (satisfied by $\pi\equiv0$), quantifying over arbitrary rate functions instead of the rates built from the network data, and restricting the goal to exponential service or to a single class.

Needed infrastructure: finite-support tsum manipulations, multinomial identities for the §4.1 sums over orderings and stage assignments, and bookkeeping for list and array updates. The model and the balance-equation layer can be reused for later queueing missions. Contributions are welcome on each milestone, on the per-center-type pieces of the independent balance check, and on helper lemmas about the event system.

Selected references

• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, Closed, and Mixed Networks of Queues with Different Classes of Customers, J. ACM 22(2):248–260, 1975. https://doi.org/10.1145/321879.321887
• J. R. Jackson, Networks of Waiting Lines, Operations Research 5(4):518–521, 1957. https://doi.org/10.1287/opre.5.4.518
• J. R. Jackson, Jobshop-like Queueing Systems, Management Science 10(1):131–142, 1963. https://doi.org/10.1287/mnsc.10.1.131
• W. J. Gordon, G. F. Newell, Closed Queuing Systems with Exponential Servers, Operations Research 15(2):254–265, 1967. https://doi.org/10.1287/opre.15.2.254
• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979. http://www.statslab.cam.ac.uk/~frank/rsn.html
• D. R. Cox, A Use of Complex Probabilities in the Theory of Stochastic Processes, Proc. Cambridge Phil. Soc. 51:313–319, 1955. https://doi.org/10.1017/S0305004100030231