All missions

Motivation

The classical Lagrange multiplier rule and its inequality-constrained form, the Karush–Kuhn–Tucker (KKT) conditions, are necessary conditions satisfied at a minimizer of a constrained problem. In finite dimensions, a continuous function bounded below on a closed bounded feasible set attains its minimum, so the rule describes an actual point. In an infinite-dimensional Banach space this fails: closed bounded sets are not compact, minimizing sequences need not converge, and a smooth function bounded below on a smooth constraint set can have no minimizer at all. The multiplier rule then has nothing to describe.

Ekeland's 1974 paper On the Variational Principle (DOI) introduced a principle (its Theorem 1.1) that replaces "a minimizer exists" with "near every almost-minimizer there is a point that strictly minimizes a slightly perturbed function". Section 3 of the paper uses this to prove that, for a problem with finitely many smooth equality and inequality constraints satisfying a linear-independence regularity condition, nearly optimal feasible points satisfy the KKT conditions up to a small error, with no compactness and no existence of a minimizer. This is the first appearance of what is now called an approximate or asymptotic KKT condition, a notion central to the convergence theory of nonlinear programming algorithms.

Setting

Let $V$ be a real Banach space with dual $V^*$ (continuous linear functionals) and dual norm $\|x^*\|_*=\sup_{\|h\|\le1}\langle x^*,h\rangle$. Let $F:V\to\mathbb R$ be Fréchet-differentiable, with derivative $F'(v)\in V^*$, and let $G_1,\dots,G_m:V\to\mathbb R$ be $C^1$ (continuously Fréchet-differentiable). Fix $0\le p\le m$ and consider

$$\inf F(v)\quad\text{subject to}\quad G_i(v)=0\ (1\le i\le p),\qquad G_i(v)\ge0\ (p+1\le i\le m). \tag{3.1}$$

The feasible set is $\mathcal C=\{v\in V : G_i(v)=0 \text{ for } i\le p,\ G_i(v)\ge0 \text{ for } i>p\}$ (3.2). At $v\in\mathcal C$ the saturated constraints are $I(v)=\{i : G_i(v)=0\}$ (3.3). The regularity assumption (3.4) is: for every $v\in\mathcal C$, the derivatives $G_i'(v)$, $i\in I(v)$, are linearly independent in $V^*$.

In the Lean development these are EkelandVP.Constraints.feasibleSet p G and EkelandVP.Constraints.IsRegular p G, with constraints indexed by Fin m.

Formalization targets

Goal: Theorem 3.1 (p. 330)

Assume (3.4), $\mathcal C\ne\emptyset$, and that $F$ is bounded below on $\mathcal C$ (3.5). Then for every $\varepsilon>0$ there are $v_\varepsilon\in\mathcal C$ and $\lambda_1,\dots,\lambda_m\in\mathbb R$ with

$$F(v_\varepsilon)\le\inf_{\mathcal C}F+\varepsilon^2,\qquad \lambda_i\ge0\ (i>p),\qquad \lambda_i=0 \text{ if } G_i(v_\varepsilon)\ne0,$$ $$\Big\|F'(v_\varepsilon)-\sum_{i=1}^m\lambda_iG_i'(v_\varepsilon)\Big\|_*\le\varepsilon.$$

Milestones, in the order of the paper's proof

1. (3.8)–(3.12): a feasible $v$ with $F(v)\le\inf_{\mathcal C}F+\varepsilon^2$ and $F(w)\ge F(v)-\varepsilon\|w-v\|$ for all $w\in\mathcal C$ (the variational principle applied to $F$ restricted to $\mathcal C$; no regularity needed).
2. (3.16): at a regular feasible point $v$, every $h$ with $\langle G_i'(v),h\rangle=0$ ($i\le p$) and $\langle G_i'(v),h\rangle\ge0$ ($i>p$, $i\in I(v)$) is the initial velocity of a $C^1$ curve $u:[0,\tau]\to\mathcal C$ with $u(0)=v$.
3. Lemma 3.2: at a point with the property of milestone 1, $\langle F'(v),h\rangle\ge-\varepsilon\|h\|$ for every such $h$.
4. Lemma 3.3: an $\varepsilon$-Farkas–Minkowski lemma in $V^*$: if $\langle w^*,h\rangle\ge-\varepsilon\|h\|$ whenever $\langle u_i^*,h\rangle=0$ and $\langle v_j^*,h\rangle\ge0$, then $\|w^*-\sum\lambda_iu_i^*-\sum\mu_jv_j^*\|_*\le\varepsilon$ for some $\lambda_i\in\mathbb R$ and $\mu_j\ge0$.

An additional item states Corollary 3.4 (p. 333), the one-constraint case: if $G(v)=0\Rightarrow G'(v)\ne0$, $\{G=0\}\neq\emptyset$ and $F$ is bounded below on $\{G=0\}$, then for every $\varepsilon>0$ there are $v_\varepsilon$ with $G(v_\varepsilon)=0$ and $\lambda_\varepsilon\in\mathbb R$ with $\|F'(v_\varepsilon)-\lambda_\varepsilon G'(v_\varepsilon)\|_*\le\varepsilon$.

Significance

The result. Theorem 3.1 is an existence theorem for approximate KKT points that needs neither compactness nor attainment of the infimum. It shows that every bounded-below problem with regular constraints has a sequence of feasible points whose objective values converge to the infimum and along which the KKT residual tends to zero. This is the property that later work calls approximate KKT or asymptotic KKT (AKKT) and uses as a stopping criterion and as a sequential optimality condition for nonlinear programming. Corollary 3.4 is the corresponding nonlinear eigenvalue statement: on a regular level set, $F'$ is approximately proportional to $G'$ at almost-minimizing points.

Formalizing it. The result is classical and proved in the paper; to our knowledge no machine-checked version exists. Mathlib has the Fréchet derivative, the implicit function theorem for strictly differentiable maps, Banach–Alaoglu and the Hahn–Banach separation theorems, but no Ekeland principle in this form, no Lyusternik-type tangent-curve theorem for mixed equality–inequality constraints, and no Farkas lemma in a dual Banach space. Each milestone is a reusable piece of nonlinear optimization theory in Banach spaces.

Difficulty

The obvious argument, "take a minimizer and apply the Lagrange multiplier rule", fails at the first step because no minimizer need exist. The variational principle supplies a point $v_\varepsilon$ that minimizes $F+\varepsilon\|\cdot-v_\varepsilon\|$ on $\mathcal C$, but that function is not differentiable at $v_\varepsilon$, so the multiplier rule cannot be applied to it directly either. Two further gaps remain. Linearized feasible directions (those satisfying the derivative conditions on the active constraints) need not be directions along which one can actually move inside $\mathcal C$; closing this gap requires the regularity assumption and completeness of $V$, and must keep the active inequality constraints nonnegative, not just the equalities. And the resulting first-order inequality, which holds only up to $\varepsilon\|h\|$, must be turned into an approximate multiplier representation in $V^*$, an infinite-dimensional dual space in which the usual finite-dimensional Farkas lemma does not apply as stated.

Formalization scope

• $V$ is a real Banach space: [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V]. $V^*$ is V →L[ℝ] ℝ with the operator norm; $F'(v)$ is fderiv ℝ F v.
• Constraints are one family G : Fin m → V → ℝ, 0-based: the paper's constraint $i$ is Lean index $i-1$, an equality constraint iff its index is $<p$. p ≤ m is assumed in the goal.
• $C^1$ is ContDiff ℝ 1; $F$ is Differentiable ℝ F (Fréchet-differentiable everywhere).
• No infimum over $\mathcal C$ is formed: "bounded below" is BddBelow (F '' 𝒞) and "$F(v)\le\inf_{\mathcal C}F+\varepsilon^2$" is "$F(v)\le F(w)+\varepsilon^2$ for all $w\in\mathcal C$". A real infimum over an empty or unbounded set would be a junk value.
• Added hypotheses, disclosed in each item: $\mathcal C\ne\emptyset$ (goal and milestone 1) and $\{G=0\}\ne\emptyset$ (Corollary 3.4). Without them the paper's hypotheses hold vacuously ($\inf\emptyset=+\infty$) while the conclusion asks for a feasible point.
• Lemma 3.3 is stated with $\le\varepsilon$. The paper prints $<\varepsilon$ in (3.20), which fails for $V=\mathbb R$, no constraints and $w^*=\varepsilon\,\mathrm{id}$; its proof gives $\le$, and Theorem 3.1 uses $\le$.
• Lemma 3.2 and milestone 2 assume the linear independence (3.4) only at the point $v$ under consideration, and Lemma 3.2 is stated for any feasible $v$ with property (3.12); this is exactly what the paper's proof uses.
• Regularity is a linear independence of the indexed family $(G_i'(v))_{i\in I(v)}$, so a repeated saturated constraint violates it; the constraint qualification cannot be trivialized by collapsing duplicates.

Contributions welcome: a general Ekeland principle with the strict-minimizer conclusion, a Lyusternik–Graves tangent-curve theorem for $C^1$ maps with surjective derivative onto $\mathbb R^k$, and a closedness result for finitely generated cones in $V^*$.

Selected references

• I. Ekeland, On the Variational Principle, J. Math. Anal. Appl. 47 (1974) 324–353. https://doi.org/10.1016/0022-247X(74)90025-0
• I. Ekeland, Nonconvex minimization problems, Bull. Amer. Math. Soc. (N.S.) 1 (1979) 443–474. https://doi.org/10.1090/S0273-0979-1979-14595-6
• R. Andreani, G. Haeser, J. M. Martínez, On sequential optimality conditions for smooth constrained optimization, Optimization 60 (2011) 627–641. https://doi.org/10.1080/02331930903578700

Motivation

A function that is bounded below need not attain its infimum: $e^x$ on $\mathbb{R}$ has infimum $0$ and no minimizer. The classical "variational principle" says that at a minimizer $\bar u$ of a differentiable functional, $F'(\bar u)=0$. Without compactness there may be no minimizer, and the principle has nothing to say. In 1974 Ivar Ekeland showed that a weaker statement survives in every complete metric space: next to any approximate minimizer lies a point that is the exact, strict minimizer of a slightly perturbed function (Ekeland 1974).

The result is now a standard tool in nonlinear analysis, optimization and the calculus of variations. It yields approximate first-order conditions ($\|F'(v)\|_*\le\varepsilon$) without existence of minimizers, approximate Lagrange multiplier rules, and approximate maximum principles in optimal control; Ekeland's survey (Ekeland 1979) collects many of these uses.

Timeline. Bishop and Phelps introduced the partial order on a Banach space times $\mathbb{R}$ that underlies the proof, in their study of support functionals of convex sets (Bishop–Phelps, The support functional of a convex set, Proc. Symp. Pure Math. 7, AMS, 1963). Brøndsted and Rockafellar used it in 1965 to obtain subdifferentiability properties of convex functions on Banach spaces (Brøndsted–Rockafellar 1965), and Browder applied it to nonconvex subsets of Banach spaces (Bull. AMS 79, 1973). Ekeland's 1974 article, formalized here, isolates the device as a principle valid in every complete metric space for lower semicontinuous functions with values in $\mathbb{R}\cup\{+\infty\}$, and applies it to Gâteaux-differentiable functions, constrained optimization, Plateau's problem, geodesics and optimal control.

Setting

Let $(V,d)$ be a complete metric space. Let $F:V\to\mathbb{R}\cup\{+\infty\}$ be lower semicontinuous (for every $c$ the set $\{F\le c\}$ is closed), not identically $+\infty$, and bounded from below:

$$\inf F > -\infty. \tag{1.1}$$

For $\varepsilon>0$, a point $u\in V$ is an $\varepsilon$-minimizer if

$$\inf F \le F(u) \le \inf F + \varepsilon. \tag{1.2}$$

For $\alpha>0$, the Bishop–Phelps order on $V\times\mathbb{R}$ is

$$(v_1,a_1)\prec(v_2,a_2)\iff (a_2-a_1)+\alpha\,d(v_1,v_2)\le 0. \tag{1.6}$$

In Lean it is EkelandVP.General.bpLE α p q, read $p\prec q$. The epigraph of $F$ is $S=\{(v,a)\mid a\ge F(v)\}\subseteq V\times\mathbb{R}$ (1.15).

In §2, $V$ is a real Banach space with dual $V^*$, and $F$ is Gâteaux-differentiable with derivative $F':V\to V^*$ (EkelandVP.General.IsGateauxDiff F F'): at every $u_0$ with $F(u_0)<+\infty$, $\frac{d}{dt}F(u_0+tv)|_{t=0}=\langle F'(u_0),v\rangle$ for every $v$ (2.1).

Formalization targets

Goal: Theorem 1.1 (p. 324)

For every $u$ satisfying (1.2) and every $\lambda>0$ there is $v\in V$ with

$$F(v)\le F(u),\qquad d(u,v)\le\lambda,\qquad \forall w\ne v:\ F(w)>F(v)-\frac{\varepsilon}{\lambda}\,d(v,w). \tag{1.3–1.5}$$

The parameters $\varepsilon$ and $\lambda$ are free; the trade-off between closeness to $u$ and the size of the perturbation is the content of the theorem.

Milestones (§1)

1. For $\alpha>0$, $\prec$ is reflexive, antisymmetric and transitive (p. 325).
2. For every $(v_1,a_1)$, the set $\{(v,a)\mid (v_1,a_1)\prec(v,a)\}$ is closed in $V\times\mathbb{R}$ (p. 325).
3. Lemma 1.2 (p. 325): if $S\subseteq V\times\mathbb{R}$ is closed and $a\ge m$ on $S$ for some $m$ (1.7), then every $(v_1,a_1)\in S$ lies below a $\prec$-maximal element of $S$.

Consequences (§2)

• Corollary 2.3 (p. 328): for $V$ Banach, $F$ l.s.c. and Gâteaux-differentiable with $-\infty<\inf F<+\infty$, and every $\varepsilon>0$, there is $v_\varepsilon$ with $F(v_\varepsilon)-\inf F\le\varepsilon^2$ and $\|F'(v_\varepsilon)\|_*\le\varepsilon$.
• Corollary 2.4 (p. 328): if moreover $F(v)\ge k\|v\|+c$ with $k>0$, then $F'(V)$ is dense in $kB^*$.
• Corollary 2.5 (p. 329): if $F(v)\ge\Phi(\|v\|)$ with $\Phi$ continuous and $\Phi(t)/t\to\infty$, then $F'(V)$ is dense in $V^*$.

Significance

The result. Theorem 1.1 replaces "a minimizer exists" by "a strict minimizer of a Lipschitz perturbation exists nearby", with explicit control of both the distance and the perturbation. With $\lambda=\sqrt{\varepsilon}$ this gives a point that is $\varepsilon$-optimal, $\sqrt{\varepsilon}$-close to $u$, and $\sqrt{\varepsilon}$-stationary in the metric sense. Corollary 2.3 is the form announced in the paper's abstract: a differentiable function with a finite lower bound has points where $F$ is almost minimal and $\|F'\|_*$ is arbitrarily small. Later sections of the same paper use Theorem 1.1 for approximate Lagrange multiplier rules (§3) and an approximate Pontryagin maximum principle (§7), which are the subjects of missions II and III of this series.

Formalizing it. The theorem is proved; this mission formalizes the paper's own route (the order (1.6), Lemma 1.2, then Theorem 1.1) and its first applications in §2. The pinned Mathlib has no statement of Ekeland's principle, of the Caristi fixed point theorem, or of the Bishop–Phelps order, and the platform has none either. A machine-checked Theorem 1.1 for extended-real-valued functions would be directly reusable by every later mission that needs approximate optimality without compactness.

Difficulty

The obvious argument — take a minimizing sequence and pass to a limit — fails because nothing makes a minimizing sequence converge: $V$ is not compact, and a minimizing sequence of $e^x$ escapes to $-\infty$. Completeness only helps for Cauchy sequences, so one must construct a sequence that is Cauchy. The limit must moreover be maximal for the order (1.6), not merely a limit point, and that maximality is what produces the strict inequality (1.5). Lemma 1.2 is where this difficulty sits. In §2, the passage from the metric statement (1.5) to a bound on $\|F'(v)\|_*$ requires $F$ to be finite near $v$ along every line, which the Gâteaux hypothesis supplies.

Formalization scope

• $V$ is a MetricSpace with CompleteSpace; $d(u,v)$ is dist u v. $V\times\mathbb{R}$ carries the product topology; only closedness of subsets of it is used.
• $F:V\to$ EReal. "Bounded from below" (1.1) is $\bot<\inf_v F(v)$; it also excludes the value $-\infty$, which the paper's codomain does not contain. "Not identically $+\infty$" is $\exists v_0,\ F(v_0)\ne\top$. Lower semicontinuity is Mathlib's LowerSemicontinuous.
• (1.2) is assumed in the form $F(u)\le\inf F+\varepsilon$ with $\varepsilon>0$ real (the left half is automatic). $\lambda$ is named lam.
• (1.5) is $F(v)-\frac{\varepsilon}{\lambda}d(v,w)<F(w)$ for all $w\ne v$, strict, with the paper's argument order $d(v,w)$. Since $F(v)$ is finite under the hypotheses, the EReal subtraction is ordinary.
• A trivializing formalization is ruled out: $F$ is not real-valued (the value $+\infty$ is what lets §3 apply the theorem to $F$ plus the indicator of a closed set), (1.5) is strict and quantified over all $w\ne v$, and the conclusion is not weakened to $d(u,v)<\infty$ or $\le$ in (1.5).
• In §2, $V$ is a real NormedSpace with CompleteSpace, $F'$ is a function $V\to(V\to_L\mathbb{R})$, and Gâteaux differentiability requires $t\mapsto F(u_0+tv)$ to be finite near $t=0$ before taking a real derivative; without this, EReal.toReal $(\pm\infty)=0$ would let an infinite function have a junk derivative. Density of $F'(V)$ is stated for derivatives taken at points where $F<+\infty$.
• Theorem 2.2 is not part of this mission: its conclusion (2.4) is printed as the strict $\|v-u\|<\lambda$, while its one-line proof from Theorem 1.1 gives only $\le\lambda$. Corollaries 2.3–2.5 do not depend on the strict form.

Contributions welcome: proofs of the milestones (the first two are short; Lemma 1.2 is the core), of Theorem 1.1, and of the §2 corollaries; a reusable Caristi fixed point theorem built on the same order would be a natural addition.

Selected references

• I. Ekeland, On the Variational Principle, J. Math. Anal. Appl. 47 (1974), 324–353. https://doi.org/10.1016/0022-247X(74)90025-0
• I. Ekeland, Nonconvex minimization problems, Bull. Amer. Math. Soc. (N.S.) 1 (1979), 443–474. https://doi.org/10.1090/S0273-0979-1979-14595-6
• E. Bishop, R. R. Phelps, The support functional of a convex set, in Convexity (V. Klee, ed.), Proc. Symp. Pure Math. 7, Amer. Math. Soc., 1963, 27–35. (Reference [4] of Ekeland 1974.)
• A. Brøndsted, R. T. Rockafellar, On the subdifferentiability of convex functions, Proc. Amer. Math. Soc. 16 (1965), 605–611. https://doi.org/10.1090/S0002-9939-1965-0178103-8
• F. E. Browder, Normal solvability for nonlinear mappings into Banach spaces, Bull. Amer. Math. Soc. 79 (1973), 328–350. https://doi.org/10.1090/S0002-9904-1973-13152-9

Motivation

A call center with $N$ agents facing Poisson arrivals at rate $\lambda$ and exponential service at rate $\mu$ is the M/M/N (Erlang-C) queue. Choosing $N$ trades the cost of agents against the cost of customers waiting, and in practice it is done with the square-root safety-staffing rule $N \approx R + y\sqrt R$, where $R = \lambda/\mu$ is the offered load. Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published in Operations Research 52(1), 2004, doi:10.1287/opre.1030.0081) turned that rule of thumb into an optimization result: for a general convex staffing cost and a general waiting-cost function, they identify the safety factor $y$ that makes the rule asymptotically optimal as the arrival rate grows.

Timeline of the asymptotic regime the paper builds on:

• 1917. Erlang's delay formula $\pi(N,\nu)$ for the M/M/N queue.
• 1981. Halfin and Whitt (Oper. Res. 29(3)) show that with $N = R + \beta\sqrt R$ servers the probability of waiting converges to a limit $P(\beta) \in (0,1)$, the quality-and-efficiency-driven regime.
• 2000/2004. Borst, Mandelbaum and Reiman classify cost structures into a rationalized, an efficiency-driven and a quality-driven regime, and prove asymptotic optimality of an explicit staffing rule in each.

This mission is the first of a series of four on that paper and covers the rationalized regime (Section 5), where staffing and waiting costs are of the same order.

Setting

The service rate $\mu > 0$ is fixed and the arrival rate $\lambda$ grows. A staffing cost $F$, defined on $(0,\infty)$, is convex and strictly increasing; it does not depend on $\lambda$. For each $\lambda > 0$ a waiting-cost function $D_\lambda$ satisfies $D_\lambda(0)=0$, is strictly increasing on $[0,\infty)$, and makes

$$G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)\,e^{-(N\mu-\lambda)t}\,dt$$

finite for every $N > \lambda/\mu$. With the Erlang-C formula

$$\pi(N,\nu) = \frac{\nu^N}{N!}\Big\{\big(1-\tfrac{\nu}{N}\big)\sum_{n=0}^{N-1}\frac{\nu^n}{n!}+\frac{\nu^N}{N!}\Big\}^{-1},$$

the expected total cost of staffing $N > \lambda/\mu$ agents is $C(N,\lambda) = F(N) + \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda)$, and $N^*_\lambda$ is any integer $N > \lambda/\mu$ minimizing it (7).

In normalized units $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$ the paper defines $F_\lambda(x) = F(N_\lambda(x)) - F(\lambda/\mu)$, $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$, the continuous delay probability $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$ with

$$H(M,\alpha) = \Big\{\alpha\int_0^\infty e^{-\alpha t}\,t\,(1+t)^{M-1}\,dt\Big\}^{-1},$$

and $C_\lambda(x) = F_\lambda(x) + \pi_\lambda(x)G_\lambda(x)$, minimized at $x^*_\lambda$ (8). A surrogate $C[z;\hat F,\hat\pi,\hat G] = \hat F(z)+\hat\pi(z)\hat G(z)$ approximates it. Rounding is measured by

$$S_\lambda(x) = \min\{C(\lfloor N_\lambda(x)\rfloor,\lambda),\,C(\lceil N_\lambda(x)\rceil,\lambda)\}. \tag{10}$$

The Halfin–Whitt delay function is $P(x) = \big(1 + x/h(-x)\big)^{-1}$, with $h = \phi/(1-\Phi)$ the standard normal hazard rate (11). Asymptotic equality $a_\lambda \stackrel{\infty}{\approx} b_\lambda$ means $a_\lambda/b_\lambda \to 1$ as $\lambda\to\infty$.

Formalization targets

Goal: Theorem 5.1

Assume the rationalized condition (18): for some $\kappa > 0$, $F_\lambda(\kappa)/G_\lambda(\kappa) \to \gamma \in (0,\infty)$. Let $y^*_\lambda$ minimize $F_\lambda(y) + P(y)G_\lambda(y)$ over $y>0$ (19). Then

$$\lim_{\lambda\to\infty}\frac{S_\lambda(y^*_\lambda) - F(\lambda/\mu)}{C(N^*_\lambda,\lambda) - F(\lambda/\mu)} = 1.$$

The goal fixes no constant and no rate: it asserts only that the excess cost of the explicit rule is asymptotically the optimal excess cost.

Milestones

• Lemma C.1: $G_\lambda$ is strictly convex and strictly decreasing on $(0,\infty)$.
• Section 3, p. 12: $H(N,\nu) = \pi(N,\nu)$ at integers $N > \nu > 0$.
• Lemma 3.1, Lemma 3.2, Corollary 3.3: the approximation principle. If the surrogate approximates $C_\lambda$ at both $x^*_\lambda$ and its own minimizer $z^*_\lambda$, then rounding $N_\lambda(z^*_\lambda)$ is asymptotically optimal.
• Eqs. (13)–(14): $F_\lambda$ preserves $\limsup$-separation of ratios.
• Lemma 4.1 (Halfin & Whitt): for bounded $x_\lambda$, $\pi_\lambda(x_\lambda)/P(x_\lambda) \to 1$.

Significance

The theorem justifies the square-root staffing rule from first principles for a broad cost class. In Example 5.3 of the paper (linear staffing cost $c$ per agent, linear waiting cost $a$ per unit time) it gives $N^* \approx R + y^*(a/c)\sqrt R$, with $y^*(r)$ the minimizer of $y + rP(y)/y$, a one-dimensional rule computable once for all loads. Corollary 3.3 is reused verbatim by the efficiency-driven and quality-driven theorems of the paper (missions II and III of this series), and Lemma 4.1 is the analytic input of all three.

The result has been proved since 2000; no machine-checked proof of it, or of the Halfin–Whitt limit for the continuous extension $\pi_\lambda$, is known to exist. The mission produces a formal proof of the regime theorem together with reusable formal statements of the Erlang-C function, its integral representation, and the Halfin–Whitt limit.

Difficulty

The reduction from discrete to continuous staffing (Lemmas 3.1–3.2) is elementary once unimodality of $C_\lambda$ is available, but unimodality rests on convexity of $\pi_\lambda$, which the paper cites rather than proves, and on Lemma C.1, which needs differentiation under an improper integral. The central difficulty is Lemma 4.1: the paper derives it from Halfin and Whitt's limit theorem, which is stated for integer server counts, while $\pi_\lambda$ is evaluated at non-integer $N_\lambda(x_\lambda)$; a proof needs a uniform Laplace-type asymptotic for the integral defining $H$. A further obstacle is bounding $x^*_\lambda$: the obvious route through continuity of the optimizer fails because nothing converges, and the paper instead argues by contradiction via (14).

Formalization scope

All objects live in DimCallCenters.Rationalized. The arrival rate is a real lam, and every limit is Filter.atTop on $\mathbb R$ with $\mu$ fixed. The queue itself is not modelled; the paper's theorems are statements about the closed-form cost $C(N,\lambda)$, and so are these. Committed conventions:

1. The standing assumptions are a structure WaitModel ($\mu>0$; $D_\lambda(0)=0$; $D_\lambda$ strictly increasing on $[0,\infty)$; $t\mapsto D_\lambda(t)e^{-\theta t}$ integrable on $(0,\infty)$ for every $\theta>0$, which is the paper's finiteness of $G$). $F$ is convex and strictly increasing on $(0,\infty)$.
2. Staffing levels in $C(N,\lambda)$ are natural numbers; $G$ and $H$ take real $N$.
3. Argmins ($N^*_\lambda$, $x^*_\lambda$, $z^*_\lambda$, $y^*_\lambda$) are hypotheses that a given function is a minimizer, for every $\lambda>0$; ties are allowed and the theorems hold for every choice.
4. In $S_\lambda$ the floor term is omitted when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$, where $C$ is undefined.
5. $\limsup$ and $\liminf$ relations are written with ∃ᶠ/∀ᶠ, not Filter.limsup on $\mathbb R$.
6. Added hypothesis. The goal assumes $G(N,\lambda)\to\infty$ as $N\downarrow\lambda/\mu$. The paper asserts this limit on p. 12, but it does not follow from its assumptions (it fails for bounded $D_\lambda$); it is equivalent to $D_\lambda$ being unbounded and is what makes the continuous optimum exist.

The hypotheses are met by linear staffing and waiting costs ($F(N)=cN$, $D_\lambda(t)=at$), for which (18) holds with $\gamma = c\kappa^2/a$, so the goal is not vacuous. It is not trivialized by junk values either: the ratio's denominator is positive at every $\lambda>0$, and $S_\lambda$ never evaluates $C$ at an unstable level.

Needed infrastructure: Laplace asymptotics for $\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt$, differentiation under the integral sign for $G$, and convexity of $\pi_\lambda$. All of these are reusable for missions II–IV. Proofs of the milestones in any order are welcome, as are proofs of the convexity facts the paper cites from its references [9], [10].

Selected references

• S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000; Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
• S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektroteknikeren 13, 1917.

Motivation

The single-server queue with general independent interarrival and service times, the G/G/1 queue, is the basic model of a congested resource: a machine, a link, a checkout. For Markovian arrivals or services the mean wait has a closed form (the Pollaczek–Khintchine formula for M/G/1, the geometric law for G/M/1). For general distributions it has none, and the mean wait depends on the whole distributions of the interarrival and service times, not only on their moments. Capacity planning still needs numbers. Bounds that use only the first two moments are therefore the practical tool. They say how bad congestion can be for any queue with a given arrival rate, service rate and variabilities, and they become exact as the traffic intensity approaches one.

This mission formalizes Chapter 7, §7.1 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), together with the heavy-traffic Theorem 7.1 of §7.2.3.

Timeline. Lindley (Proc. Cambridge Philos. Soc., 1952) derived the recursion for successive waiting times and characterized the stationary law. Kingman (Proc. Cambridge Philos. Soc., 1961, 1962) proved the heavy-traffic exponential limit. In "Some inequalities for the queue GI/G/1" (Biometrika, 1962) he proved the two-moment upper bound. Marshall (1968) derived further moment relations and bounds (Operations Research, 1968). Marchal (Operations Research, 1978) gave the lower bound (7.14).

Setting

A G/G/1 queue is specified by two probability laws on $[0,\infty)$: the law $A$ of an interarrival time $T$ and the law $B$ of a service time $S$. Both have finite second moments, and

$$E[T] = \frac1\lambda,\quad E[S] = \frac1\mu,\quad \sigma_A^2 = \mathrm{Var}[T],\quad \sigma_B^2 = \mathrm{Var}[S],\quad \rho = \frac{\lambda}{\mu}.$$

The pairs $(S^{(n)}, T^{(n)})$ are independent and identically distributed, and $S^{(n)}$ is independent of $T^{(n)}$. Customers are served first come, first served. The line delay $W_q^{(n)}$ of the $n$th customer obeys Lindley's recursion

$$W_q^{(n+1)} = \max\bigl(0,\ W_q^{(n)} + U^{(n)}\bigr), \qquad U^{(n)} = S^{(n)} - T^{(n)}, \tag{7.1}$$

and $W_q^{(n)}$ is independent of $(S^{(n)}, T^{(n)})$. The idle gap $X^{(n)} = -\min(0, W_q^{(n)} + U^{(n)})$ is the time between the $n$th departure and the next start of service.

The queue is stationary when the law $\nu$ of $W_q^{(n)}$ does not depend on $n$, that is, when one step of (7.1) maps $\nu$ to itself. The mean stationary line delay is $W_q = E[W_q^{(n)}] = \int w\,d\nu(w)$. In the Lean development these objects are IsGG1Input A B lam mu, lindley, idleX, IsStationaryWaitLaw A B ν and meanWait ν, in the namespace QueueingFundamentals.Bounds.

Formalization targets

Goal: Kingman's upper bound (7.13)

For every stationary G/G/1 queue with $\rho < 1$, $W_q$ is finite and

$$W_q \le \frac{\lambda(\sigma_A^2 + \sigma_B^2)}{2(1-\rho)}.$$

Milestones

• the idle-gap identity $E[X] = -E[U] = 1/\lambda - 1/\mu$ (7.4), and the mean-wait formula (7.7)

$$W_q = \frac{E[X^2] - E[U^2]}{2E[U]};$$

• the variance of the interdeparture time $D = S^{(n+1)} + X^{(n)}$ (7.12): $\mathrm{Var}[D] = 2\sigma_B^2 + \sigma_A^2 - 2W_q(1/\lambda - 1/\mu)$;
• Marchal's lower bound (7.14), $W_q \ge (\lambda^2\sigma_B^2 + \rho(\rho-2))/(2\lambda(1-\rho))$;
• the distributional lower bound $W_q \ge r_0$, with $r_0$ the unique nonnegative root of $f(z) = z - \int_{-z}^\infty [1 - U(t)]\,dt$ and $U(t)$ the CDF of $S - T$ ((7.15), (7.16));
• the two-sided estimate (7.17), $\max\bigl(0, r_0, \tfrac{\lambda^2\sigma_B^2 + \rho(\rho-2)}{2\lambda(1-\rho)}\bigr) \le W_q \le \tfrac{\lambda(\sigma_A^2+\sigma_B^2)}{2(1-\rho)}$;
• Theorem 7.1 (heavy traffic): for a sequence of G/G/1 queues with $\rho_j \to 1$, $\alpha_j = -E[S_j - T_j]$ and $\beta_j^2 = \mathrm{Var}[S_j - T_j]$, under convergence of the input laws, $\mathrm{Var}[S - T] > 0$ and uniformly bounded $(2+\delta)$-moments,

$$\frac{2\alpha_j}{\beta_j^2}\,W_{q,j} \xrightarrow{d} \mathrm{Exp}(1).$$

The goal is (7.13) rather than the stronger (7.17) because it depends only on the first two moments of the input.

Significance

Kingman's bound is the most widely used performance estimate for single-server queues. It needs no distributional form, only two means and two variances. It yields the "Kingman formula" approximation used across manufacturing and service operations, and it is asymptotically exact as $\rho \to 1$ (Theorem 7.1). The departure variance (7.12) drives the decomposition approximations for networks of §7.3. The heavy-traffic theorem is the entry point to diffusion approximations of queues.

All results here are proved in the literature (Theorem 7.1 is stated in the book without proof). This mission produces the first machine-checked versions. As far as a search of the platform shows, none of these statements, and no stationary Lindley recursion, has been formalized. The substrate it needs is reusable for any mission on G/G/1, G/G/c or random walks: stationary laws of a recursion on distributions, moment identities for $\max(0,\cdot)$, and convergence in distribution.

Difficulty

The book's derivation squares (7.3) and takes expectations, using $E[(W_q^{(n+1)})^2] = E[(W_q^{(n)})^2]$. That step is valid only if the stationary wait has a finite second moment. It is not assumed here and fails in general: with finite second moments of $S$ and $T$ the stationary wait has a finite mean, but its second moment is finite only if $E[S^3] < \infty$. So the moment identity (7.7) cannot be obtained by cancelling second moments. A truncation or limiting argument is needed, and even the finiteness of $W_q$ has to be proved rather than assumed. The lower bound $W_q \ge r_0$ further needs a Jensen argument for the conditional mean of one Lindley step. Theorem 7.1 needs a uniform-integrability argument across a sequence of queues.

Formalization scope

Conventions committed to in Lean:

• laws, not random variables: $A$, $B$ and the stationary law $\nu$ are Measure ℝ; independence of $W_q^{(n)}, S^{(n)}, T^{(n)}$ (and $S^{(n+1)}$ for $D$) is the product measure;
• the input laws are probability measures on $[0,\infty)$ with finite second moments (MemLp id 2), $E[T] = 1/\lambda$, $E[S] = 1/\mu$, $\lambda, \mu > 0$, $\rho = \lambda/\mu < 1$;
• stationarity is invariance of the whole law $\nu$ under one step of (7.1), not equality of means;
• $W_q$, the variances (Mathlib variance) and $f_1$ are Lebesgue integrals. Every theorem therefore asserts, as part of its conclusion, that $\nu$ has a finite mean, and none assumes a finite second moment of $\nu$;
• $U(t)$ is Mathlib's cdf of the law of $S - T$;
• convergence in distribution is convergence of $\int g$ for all bounded continuous $g$, and $\mathrm{Exp}(1)$ is expMeasure 1.

Closed forms carried by the statements: (7.4), (7.7), (7.12), (7.13), (7.14) and (7.17) exactly as printed, and the scaling $2\alpha_j/\beta_j^2$ of Theorem 7.1.

Stating (7.13) with $W_q$, $E[X^2]$ or the idle probability as free real numbers constrained by (7.7) would reduce it to algebra. Here $W_q$ is always the mean of a stationary law of the queue.

Not formalized: (7.5) and (7.8), which need the idle-period law $I$ and the arrival-point probability $q_0$ as separate objects, and the multiserver bounds of §7.1.3. Proofs of any milestone are welcome, as are reusable lemmas on stationary laws of Lindley's recursion (existence, uniqueness, and finiteness of the mean under $E[S^2] < \infty$).

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
• D. V. Lindley, The theory of queues with a single server, Math. Proc. Cambridge Philos. Soc. 48 (1952)
• J. F. C. Kingman, The single server queue in heavy traffic, Math. Proc. Cambridge Philos. Soc. 57 (1961)
• J. F. C. Kingman, Some inequalities for the queue GI/G/1, Biometrika 49 (1962)
• K. T. Marshall, Some inequalities in queuing, Operations Research 16 (1968)
• W. G. Marchal, Some simpler bounds on the mean queuing time, Operations Research 26 (1978)

Motivation

Two-stage stochastic linear programs model decisions taken before uncertainty is resolved (first stage) and corrected afterwards at a cost (second stage, the recourse). The standard solution method for problems with finitely many scenarios is the L-shaped method of Van Slyke and Wets (1969), an outer linearization in the style of Benders decomposition: a master program approximates the expected recourse function by cutting planes, one cut per iteration. Birge and Louveaux (1988) proposed the multicut variant, which approximates the recourse function of each realization separately and can add several cuts per iteration, and compared the two methods by worst-case counts of major iterations.

The paper's §5 treats the special case of simple recourse, where the second stage only penalizes shortage and surplus of each component of the first-stage output against a random target. Simple recourse arises in production planning, inventory and capacity models, and is the case in which the recourse function separates into one-dimensional pieces. There the paper derives an explicit LP (25) equivalent to the problem, a dedicated multicut algorithm for it, and the bound of $Jm_2+1$ iterations quoted below. This mission formalizes that section.

Setting

First-stage data are $c\in\mathbb R^{n_1}$, $A\in\mathbb R^{m_1\times n_1}$, $b\in\mathbb R^{m_1}$, and the first-stage feasible set is $K_1=\{x\mid Ax=b,\ x\ge0\}$. A deterministic technology matrix $T\in\mathbb R^{m_2\times n_1}$, with rows $T_i$, maps $x$ to the tender $\chi=Tx\in\mathbb R^{m_2}$. Problem (3) of the paper is

$$\min\ z(x)=cx+\Psi(Tx)\quad\text{s.t. } x\in K_1 .$$

For each row $i=1,\dots,m_2$ the random vector $\xi_i=(q_i^+,q_i^-,h_i)$ takes $J$ values $\xi_{ij}=(q^+_{ij},q^-_{ij},h_{ij})$ with probabilities $p_{ij}$. The simple recourse cost (20) of row $i$ is the optimal value of a one-row LP,

$$\psi_i(\chi_i,\xi_{ij})=\min\{q^+_{ij}y^+ + q^-_{ij}y^- \mid y^+-y^-=h_{ij}-\chi_i,\ y^+,y^-\ge0\},$$

and by separability (19) the expected recourse function is $\Psi(\chi)=\sum_i\Psi_i(\chi_i)$ with $\Psi_i(\chi_i)=\sum_j p_{ij}\psi_i(\chi_i,\xi_{ij})$. Write $q_{ij}=q^+_{ij}+q^-_{ij}$.

The multicut algorithm for simple recourse problems (p. 389) keeps a set $I$ of identified pairs $l=(i,j)$, initially empty. Step 1 solves the master program (26),

$$\min\ cx+\sum_{i,j}p_{ij}q^-_{ij}(T_ix)+\sum_{l\in I}u_l\quad\text{s.t. } Ax=b,\ x\ge0,\ u_l\ge e_l-E_lx,\ u_l\ge0\ (l\in I),$$

with $E_l=p_{ij}q_{ij}T_i$ and $e_l=p_{ij}q_{ij}h_{ij}$. Step 2 adds to $I$ every pair for which the constraint $0\ge p_{ij}q_{ij}(h_{ij}-T_ix^\nu)$ (27) is violated at the master's solution $x^\nu$, and returns to Step 1; when no pair is added the algorithm stops.

Formalization targets

Goal: the $Jm_2+1$ bound, with correctness

The paper states (p. 389): "The initial problem (26) involves $m_1$ constraints and $n_1$ variables. For this problem, the worst-case situation is when at each iteration, only one constraint (27) is violated in Step 2. Then, the maximal number of iterations is $Jm_2+1$." The goal asserts, for every run of the algorithm (any optimal solution of (26) may be used at each Step 1):

$$\nu\text{-th solve of Step 1 takes place}\ \Longrightarrow\ \nu\le Jm_2+1,$$

and, when the algorithm stops at $x^\nu$, $x^\nu\in K_1$ and $cx^\nu+\Psi(Tx^\nu)\le cx+\Psi(Tx)$ for all $x\in K_1$.

Milestones

1. (22)–(23): for $q^++q^-\ge0$ the LP (20) attains its minimum $\max\{q^-(\chi-h),q^+(h-\chi)\}$, so each $\theta_{ij}$ has only two cuts.
2. (24)–(25): the simple recourse problem is equivalent to the LP (25): same optimal $x$, and the value of (25) at $x$ with the best slacks is $z(x)$.
3. Relaxation and stopping: (26) is a relaxation of (25), and if no unidentified pair violates (27) at an optimum of (26), that optimum (extended by zero slacks) is optimal for (25).
4. Facets: each $\Psi_i$ is a maximum of $J+1$ affine functions, so $\Psi$ is a maximum of at most $(J+1)^{m_2}$ affine functions.

Significance

The bound is linear in $m_2$ and $J$, while the L-shaped method may need as many iterations as $\Psi$ has facets, up to $(J+1)^{m_2}$ (milestone 4). This is the paper's clearest instance of the multicut method's worst-case advantage, and the equivalence (25) shows that simple recourse problems are LPs of size linear in $m_2J$, a fact used throughout the later literature on simple and integrated recourse.

The results are proved in the paper, briefly. To our knowledge none has a machine-checked proof. Formalizing them produces a checked reduction of simple recourse to an explicit LP, a checked correctness proof of a constraint-generation algorithm with an explicit iteration bound, and the piece count of a sum of one-dimensional convex piecewise linear functions.

Difficulty

The counting argument is short once the algorithm is pinned down; the difficulty lies in the rest. Correctness at stopping requires relating three optimization problems (3), (25) and (26) whose objectives differ by a constant and by slack variables that are only present for identified pairs, and doing so for an arbitrary optimal solution of the master. The step from (20) to (22)–(23) requires solving an LP in closed form, as an infimum that must first be shown finite. The facet count requires showing that a sum of $J$ convex functions, each with one breakpoint, is a maximum of exactly $J+1$ affine functions, which is not a consequence of convexity alone.

Formalization scope

All vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, realizations are indexed by Fin J, and pairs $(i,j)$ by Fin m2 × Fin J. The second-stage value $\psi$ is the EReal infimum of the LP (20), not its closed form; expectations are finite sums weighted by $p_{ij}\ge0$ with $\sum_jp_{ij}=1$.

Readings pinned down, each recorded in the item statements:

• $q_{ij}\ge0$. The paper never states it, but without it (20) is unbounded below and (25) is not equivalent to (3). It is a field of the model.
• $x\ge0$ belongs to (3) and is omitted in the displays of (25) and (26); it is kept in both.
• Step 2 ranges over unidentified pairs. The paper writes "for each $i$ and $j$"; read literally, an identified pair whose $u_l$ already covers it could be re-added forever. The paper's remark that (27) "identifies any constraints in (25) that are not met" fixes the reading. The state of the algorithm is the set of identified pairs; the order of identification, and so the index $t$, is immaterial.
• Stopping rule. It is implicit in the paper: stop when (27) is violated for no pair.
• Counting. The paper writes "the maximal number of iterations is $Jm_2+1$"; we count solves of Step 1, the stopping solve included, which is what its argument counts.
• Constant. The objective of (26) omits the constant $-\sum p_{ij}q^-_{ij}h_{ij}$ of (25), as printed.
• Facets. "$\Psi_i$ contains $J+1$ facets" is read as "is a maximum of $J+1$ (not necessarily distinct) affine functions".

A formalization in which the master step could fire without a violated, unidentified pair, or in which the algorithm's optimal solutions were fixed in advance, would make the bound either false or empty; the definitions exclude both. The goal includes optimality at stopping so that it is not only a statement about a set growing inside a finite set.

Needed infrastructure: elementary LP feasibility and optimality, finite sums in EReal, and piecewise linear convex functions on $\mathbb R$. Contributions of any of the milestones, in any order, are welcome; milestone 1 is the natural first step.

Selected references

• J.R. Birge and F.V. Louveaux, A multicut algorithm for two-stage stochastic linear programs, European Journal of Operational Research 34 (1988) 384–392. https://doi.org/10.1016/0377-2217(88)90159-2
• R.M. Van Slyke and R. Wets, L-shaped linear programs with applications to optimal control and stochastic programming, SIAM Journal on Applied Mathematics 17 (1969) 638–663. https://doi.org/10.1137/0117061
• J.R. Birge and F.V. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4