Motivation

Interior-point methods are the standard polynomial-time algorithms for linear programming, and the path-following method that practitioners implement (Chapter 18 of Vanderbei's Linear Programming: Foundations and Extensions) comes without a complete convergence proof. Chapter 22 of the same book presents a closely related algorithm for which a complete analysis can be written down: the homogeneous self-dual predictor–corrector method. It combines two ideas. The first is the self-dual embedding of Ye, Todd and Mizuno (1994), which folds a linear program and its dual into one auxiliary problem that always has feasible solutions, so no feasible starting point is needed. The second is the predictor–corrector scheme of Mizuno, Todd and Ye (1993), which alternates an affine-scaling step with a centering step while keeping the iterates in a neighbourhood of the central path, and reduces the duality measure by a factor $1 - 1/(2\sqrt n)$ every two iterations. The result is an $O(\sqrt n\,L)$ iteration bound, the best known for interior-point methods on linear programs.

Setting

Let $A$ be a real $n \times n$ matrix with $n \ge 2$ that is skew symmetric, $A = -A^T$. The homogeneous self-dual problem (22.4) is

$$\text{maximize } 0 \quad \text{subject to } Ax + z = 0,\quad x, z \ge 0.$$

For $x, z \in \mathbb{R}^n$ write $X, Z$ for the diagonal matrices with the entries of $x, z$ on the diagonal and $e$ for the vector of ones. The infeasibility is $\rho(x, z) = Ax + z$ and the noncomplementarity is $\mu(x, z) = \frac1n x^T z$. For a centering parameter $0 \le \delta \le 1$, step directions $(\Delta x, \Delta z)$ solve the linear system

$$A\Delta x + \Delta z = -(1 - \delta)\rho(x, z), \qquad Z\Delta x + X\Delta z = \delta\mu(x, z)e - XZe. \qquad (22.5)\text{–}(22.6)$$

For $0 \le \beta \le 1$ the neighbourhood is

$$\mathcal N(\beta) = \{(x, z) > 0 : \|XZe - \mu(x, z)e\| \le \beta\mu(x, z)\},$$

with $\|\cdot\|$ the Euclidean norm and $(x, z) > 0$ meaning that every component is strictly positive. The algorithm starts at $x^{(0)} = z^{(0)} = e$ and alternates two steps. A predictor step starts from $(x, z) \in \mathcal N(1/4)$, uses $\delta = 0$, and takes the step length (22.10) $\theta = \max\{t : (x + t\Delta x, z + t\Delta z) \in \mathcal N(1/2)\}$. A corrector step starts from $(x, z) \in \mathcal N(1/2)$, uses $\delta = 1$ and $\theta = 1$.

A general linear program (22.1), $\max c^Tx$ subject to $Ax \le b$, $x \ge 0$ with $A$ now $m \times n$, and its dual (22.2), $\min b^Ty$ subject to $A^Ty \ge c$, $y \ge 0$, are embedded in the homogeneous self-dual problem (22.21):

$$-A^Ty + c\phi + z = 0,\quad Ax - b\phi + w = 0,\quad -c^Tx + b^Ty + \psi = 0,\quad x, y, \phi, z, w, \psi \ge 0.$$

A feasible solution of (22.21) is strictly complementary if $x_j + z_j > 0$, $y_i + w_i > 0$ and $\phi + \psi > 0$ for all $i, j$.

Formalization targets

Goal: Theorem 22.5 (p. 330)

In each predictor step, starting from $(x, z) \in \mathcal N(1/4)$ with any solution $(\Delta x, \Delta z)$ of (22.5)–(22.6) at $\delta = 0$,

$$\theta \ge \frac{1}{2\sqrt n}.$$

The formal statement asserts that every $t \in [0, 1/(2\sqrt n)]$ keeps $(x + t\Delta x, z + t\Delta z)$ in $\mathcal N(1/2)$, and that the supremum of the admissible step lengths is at least $1/(2\sqrt n)$.

Milestones

1. Theorem 22.1: (22.4) is feasible, every feasible point is optimal, and $z^Tx = 0$ on the feasible set.
2. Theorem 22.2: $\Delta z^T\Delta x = 0$, $\bar\rho = (1 - \theta + \theta\delta)\rho$, $\bar\mu = (1 - \theta + \theta\delta)\mu$, and $\bar X\bar Ze - \bar\mu e = (1 - \theta)(XZe - \mu e) + \theta^2\Delta X\Delta Ze$.
3. Lemma 22.4: $\|PQe\| \le \frac12\|r\|^2$ for the scaled directions $p = X^{-1/2}Z^{1/2}\Delta x$, $q = X^{1/2}Z^{-1/2}\Delta z$, $r = p + q$; $\|r\|^2 = n\mu$ when $\delta = 0$; $\|r\|^2 \le \beta^2\mu/(1 - \beta)$ when $\delta = 1$ and $(x, z) \in \mathcal N(\beta)$.
4. Theorem 22.3: a predictor step lands in $\mathcal N(1/2)$ with $\bar\mu = (1 - \theta)\mu$; a corrector step lands in $\mathcal N(1/4)$ with $\bar\mu = \mu$.
5. Theorem 22.7: there are constants $c_j > 0$ with $x_j + z_j \ge c_j$ for every iterate $(x, z) \in \mathcal N(\beta)$.
6. Theorem 22.8: a strictly complementary solution of (22.21) with $\bar\phi > 0$ yields optimal solutions $\bar x/\bar\phi$, $\bar y/\bar\phi$ of (22.1)–(22.2); with $\bar\phi = 0$ it certifies that the primal or the dual is infeasible.

Significance

Theorem 22.5 is the quantitative core of the method. Combined with Theorem 22.3 it gives $\mu^{(2k)} \le (1 - \frac{1}{2\sqrt n})^k$ along the iterates, and therefore at most $4L\sqrt n$ iterations to bring $\mu$ below $2^{-L}$ (§22.2.4). Since the infeasibility tracks the noncomplementarity, $\rho^{(k)} = \mu^{(k)}\rho^{(0)}$, both go to zero at that rate. Theorem 22.8 then converts the output into an answer for the original linear program: optimal primal and dual solutions, or a certificate that one of them is infeasible. Theorem 22.7 is the mechanism behind strict complementarity of the limit (Theorem 22.6, stated in the book without proof).

All results are classical and proved in the book. The mission formalizes those proofs. To the best of the curator's knowledge there is no machine-checked convergence analysis of an interior-point method for linear programming in Mathlib or on this platform; the existing platform material on interior-point methods covers a different, short-step path-following method in equality form.

Difficulty

The algebra of Theorem 22.2 is the first obstacle: the orthogonality $\Delta z^T\Delta x = 0$ is not a consequence of (22.5) alone but of skew symmetry combined with both step equations and the definition of $\mu$, and parts (3)–(4) depend on it. The second is that the book's step length (22.10) is a maximum that need not exist, so a statement about $\theta$ must be phrased about the admissible set of step lengths, and membership in $\mathcal N(1/2)$ requires strict positivity of every component along the whole segment, not only the norm bound at its end. The norm bound alone does not control positivity; an argument that ignores this proves membership in a larger set than $\mathcal N(1/2)$. Theorem 22.7 needs a strictly complementary feasible solution of (22.4), whose existence (Theorem 10.6 in the book, the Goldman–Tucker theorem) is itself a substantial result not available in Mathlib.

Formalization scope

Vectors are functions Fin n → ℝ (and Fin m → ℝ), matrices are Matrix (Fin m) (Fin n) ℝ, and all declarations sit in the namespace VanderbeiLP.SelfDual. The committed conventions are:

• The Euclidean norm is defined explicitly (euclidNorm); Mathlib's default norm on Fin n → ℝ is the sup norm and is not used.
• $\mu(x, z) = \frac1n x^Tz$ with $n \ge 2$, the standing assumption of §22.2, carried as a hypothesis by every theorem about (22.4) together with $A^T = -A$.
• Step directions are any solution of (22.5)–(22.6); existence and uniqueness of the solution are neither assumed nor claimed.
• The predictor step length is the supremum of $\{t \in \mathbb{R} : (x + t\Delta x, z + t\Delta z) \in \mathcal N(1/2)\}$. This set contains $0$ and is bounded above by $1$ along a predictor direction, so the supremum is never a default value. Theorem 22.3(1) is stated under the hypothesis that the maximum exists, as (22.10) presumes.
• Theorem 22.7 is stated for points of $\mathcal N(\beta)$ with $0 \le \beta < 1$ satisfying $\rho(x, z) = \mu(x, z)\rho(e, e)$, the relation all iterates satisfy. The constants $c_j$ are quantified before $(x, z)$ and depend only on $A$ and $\beta$. The existence of a strictly complementary solution of (22.4) is not a hypothesis.
• Theorem 22.8 is for arbitrary $m, n$ and data $(A, b, c)$; "optimal" means feasible and attaining the best objective value among feasible points.
• No explicit constants beyond those printed in the statements ($1/4$, $1/2$, $1/(2\sqrt n)$, $\beta^2/(1-\beta)$) occur; the book leaves no constant implicit in the formalized results.

A trivializing formalization is ruled out: the step length is not a default-valued supremum, $\mathcal N(\beta)$ requires strict positivity and uses the Euclidean norm, and the goal is also stated as the segment property its proof establishes.

Theorem 22.6 (convergence of the iterates to a strictly complementary solution) is stated without proof in the book and is not part of this mission; the $4L\sqrt n$ iteration count of §22.2.4 is an unnumbered corollary. Both are welcome as follow-up work, as is a proof of Theorem 10.6 for skew-symmetric systems, which Theorem 22.7 needs.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 22. https://doi.org/10.1007/978-1-4614-7630-6
• S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal–dual interior-point algorithms for linear programming, Mathematics of Operations Research 18(4), 964–981, 1993. https://doi.org/10.1287/moor.18.4.964
• Y. Ye, M. J. Todd, S. Mizuno, An $O(\sqrt n L)$-iteration homogeneous and self-dual linear programming algorithm, Mathematics of Operations Research 19(1), 53–67, 1994. https://doi.org/10.1287/moor.19.1.53
• A. J. Goldman, A. W. Tucker, Theory of linear programming, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97. https://doi.org/10.1515/9781400881987-005

Motivation

The subgradient method minimizes a convex function $f$ on $\mathbb{R}^n$ that need not be differentiable, by stepping against an arbitrary subgradient. With stepsizes $h_k \to 0$, $\sum h_k = \infty$ it converges (Shor, Theorem 2.2), but in general only slowly: no stepsize rule that ignores the structure of $f$ gives a geometric rate. Section 2.3 of N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985) identifies geometric conditions on $f$ under which a simple geometric stepsize rule does give linear convergence — convergence with the speed of a geometric progression — and computes the rate explicitly.

The results are the origin of what is now studied as sharpness or error-bound conditions for nonsmooth optimization. Their practical content is that nonsmooth problems whose level sets are not too elongated near the minimum (piecewise-linear functions, maxima of finitely many well-conditioned pieces, positive definite quadratics) can be solved by the subgradient method at a linear rate, with a stepsize rule that needs only one or two scalar parameters.

Timeline. Shor proposed the subgradient method in 1962. The book presents the geometric stepsize rule under an angle condition (Theorem 2.7) and its level-surface form (Theorem 2.8), and attributes the block-halving rule of Theorem 2.9 to its reference [94]. Goffin (Math. Programming 13, 1977) gave the sharp rate in terms of a condition number of the level sets. The book compares the quadratic case with L. V. Kantorovich's rate for steepest descent.

Setting

Let $E_n$ be the $n$-dimensional Euclidean space with inner product $(x, y)$ and $f : E_n \to \mathbb{R}$ convex. A vector $g$ is a subgradient of $f$ at $x$ if $f(y) - f(x) \ge (g, y - x)$ for all $y$; $g_f(x)$ denotes an arbitrary subgradient at $x$, chosen once for each $x$. Let $M^*$ be the set of minimum points of $f$, assumed nonempty; for $x \in E_n$, $x^*(x)$ is the point of $M^*$ nearest to $x$.

Given a starting point $x_0$ and positive stepsizes $h_1, h_2, \dots$, the normalized subgradient method is

$$x_{k+1} = x_k - h_{k+1}\frac{g_f(x_k)}{\|g_f(x_k)\|}, \qquad k = 0, 1, 2, \dots,$$

stopped when $g_f(x_k) = 0$ (then $x_k \in M^*$).

Two shape conditions are used. The angle condition (2.12) with angle $0 \le \varphi < \pi/2$ asks that every subgradient make an angle at most $\varphi$ with the direction to the nearest minimum point:

$$(g_f(x), x - x^*(x)) \ge \cos\varphi\,\|g_f(x)\|\,\|x - x^*(x)\|.$$

The level-surface ratio condition (2.20), for a function with unique minimum point $x^*$, asks that on a ball $Y$ around $x^*$ any two points $x, z$ on a common level surface $f(x) = f(z) \ne f(x^*)$ satisfy $\|x - x^*\| \le \sigma\|z - x^*\|$.

Formalization targets

Goal: Theorem 2.8 (p. 32)

If $f$ has a unique minimum point $x^*$, $\sigma \ge \sqrt2$, $h_1 \ge \|x_0 - x^*\|/\sigma$, and (2.20) holds on $Y = \{y : \|y - x^*\| \le \sigma h_1\}$, then with $h_{k+1} = h_k\sqrt{\sigma^2-1}/\sigma$

$$\|x_k - x^*\| \le h_{k+1}\,\sigma, \qquad k = 0, 1, 2, \dots$$

Milestones

1. Theorem 2.7 (pp. 30–31): under (2.12) and the geometric rule $h_{k+1} = h_k r(\varphi)$ with $r(\varphi) = \sin\varphi$ for $\varphi \ge \pi/4$ and $r(\varphi) = 1/(2\cos\varphi)$ for $\varphi < \pi/4$,

$$\|x_k - x^*(x_k)\| \le h_{k+1}/\cos\varphi \quad\text{resp.}\quad 2h_{k+1}\cos\varphi .$$

2. Remark after Theorem 2.7 (p. 32): the same conclusion when (2.12) holds only at the iterates.
3. Inequality (2.22) (p. 33): (2.20) on $Y$ implies $(g, x - x^*) \ge \sigma^{-1}\|g\|\,\|x - x^*\|$ for every $x \in Y$ and every subgradient $g$ at $x$.
4. Example (p. 33): for $A$ symmetric positive definite with extreme eigenvalues $\lambda \le \mu$,

$$\min_{x \ne 0}\frac{(Ax, x)}{\|Ax\|\,\|x\|} = \frac{2\sqrt{\lambda\mu}}{\lambda + \mu},$$

attained at $x = \sqrt{\mu/(\lambda+\mu)}\,s_1 + \sqrt{\lambda/(\lambda+\mu)}\,s_2$. 5. Theorem 2.9 (p. 34): under the assumptions of Theorem 2.8 with $\sigma \ge 2$, the rule $h_{k+1} = h_0 2^{-[(k+1)/N]}$ with $N \ge 3\sigma^2 + 1$ gives $\|x_k - x^*\| \le 2\sigma h_{k+1}$.

Significance

The results. Theorem 2.7 shows that the subgradient method, often dismissed as sublinear, converges linearly once the geometry of $f$ is controlled and the stepsizes decrease geometrically at the right ratio; the rate $r(\varphi)$ depends only on the angle. Theorem 2.8 restates the hypothesis in terms of the shape of level surfaces, a condition that can be checked for concrete functions, and gives rate $\sqrt{\sigma^2-1}/\sigma$. The Example computes the angle for positive definite quadratics, yielding rate $(\varrho - 1)/(\varrho + 1)$ with $\varrho = \mu/\lambda$ the condition number — the same rate as steepest descent with exact line search in Kantorovich's analysis, obtained with less storage. Theorem 2.9 removes the need to know $\sigma$ exactly in the stepsize ratio.

Formalizing them. All five results are proved in the book; none is formalized, and no linear-rate result for a nonsmooth first-order method is on the platform. The formalization pins the constants (2.13)–(2.19), the stepsize indexing, and the treatment of the stopped iteration; the Example is a Kantorovich-type inequality for symmetric operators that is reusable beyond this mission.

Difficulty

The obvious one-step estimate $\|x_{k+1} - x^*\|^2 = \|x_k - x^*\|^2 - 2h_{k+1}(g, x_k - x^*)/\|g\| + h_{k+1}^2$ alone does not contract: the step length is fixed in advance and does not shrink with the distance, so a step may overshoot the minimum. The rate argument has to track the ratio between the current distance and the current stepsize, and the admissible ratio of stepsizes is dictated by the worst case of this quadratic in the distance; in the two regimes $\varphi \ge \pi/4$ and $\varphi < \pi/4$ the worst case sits at different ends. For Theorem 2.8, the shape condition is only assumed on the ball $Y$, so the iterates must be shown to stay in $Y$, and the passage from level surfaces to subgradients needs the distance from $x^*$ to a level surface, which is not a quantity the iteration computes. Theorem 2.9's constant stepsize blocks are not monotone in distance at all, and the count $3\sigma^2 + 1$ must be matched against a worst-case phase.

Formalization scope

The space $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued and ConvexOn ℝ Set.univ. A subgradient selection is an arbitrary function g with g x a subgradient at every x, quantified universally. Stepsizes are h : ℕ → ℝ with h (k+1) used at step k; the recursions $h_{k+1} = h_k r$ are imposed for $k \ge 1$, $h_1$ being the chosen initial step (the book's "$k = 0, 1, 2, \dots$" in Theorem 2.8 is read this way). The iteration stops at $g_f(x_k) = 0$ by an explicit branch that repeats $x_k$, never through $x/0 = 0$; the bounds are asserted for every $k$, which implies the book's "either the method stops or …" form. $x^*(x)$ is a definition (the nearest point of the set of minima), and the set of minima is assumed nonempty. Unique minimum is stated as $M^* = \{x^*\}$. The ball $Y$ is closed, and (2.20) is assumed only for pairs in $Y$ with a common value different from $f(x^*)$. In (2.16) the ratio is $1/(2\cos\varphi)$, as the proof requires, where the page prints "1/2 cos φ". In Theorem 2.9, "the assumptions of Theorem 2.8" are taken with $h_1 = h_0$, which fixes $h_0 \ge \|x_0 - x^*\|/\sigma$ and $Y$ of radius $\sigma h_0$. In the Example, the extreme eigenvalues are pinned by $\lambda\|x\|^2 \le (Ax,x) \le \mu\|x\|^2$ together with unit eigenvectors, and the minimum is stated with IsLeast.

A statement in which the stepsizes or the bound constants could be chosen after the iterates, or in which the shape condition quantified over an empty set of pairs, would be trivially true; here every constant is fixed by the hypotheses before the sequence is generated, and the conditions are the book's.

Needed infrastructure: the subgradient inequality, continuity of convex functions on $\mathbb{R}^n$, nearest points of closed convex sets, and elementary trigonometry. The nearest-point map and the stepsize ratio are defined within the mission; the subgradient inequality, the set of minima and the iteration come from the series' shared definitions. Contributions welcome: proofs of the milestones, and a reusable Kantorovich-type cosine bound for symmetric positive definite operators.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer 1985, §2.3, pp. 30–36. https://doi.org/10.1007/978-3-642-82118-9
• J.-L. Goffin, On convergence rates of subgradient optimization methods, Mathematical Programming 13 (1977) 329–347. https://doi.org/10.1007/BF01584346
• L. V. Kantorovich, Functional analysis and applied mathematics, Uspekhi Mat. Nauk 3 (1948) 89–185 (steepest descent rate for quadratics, cited by Shor as [45]).

Motivation

Spare-parts inventory models for repairable items rest on Palm's theorem: if demands arrive as a Poisson process with constant rate $\lambda$ and each demanded unit spends an independent, identically distributed resupply time with mean $\bar\tau$ in the pipeline, the number of units in resupply is Poisson with mean $\lambda\bar\tau$ in steady state. Stock levels, backorders and fill rates are all computed from that distribution.

Both assumptions fail in practice. Military flying programmes ramp up and down within weeks, repair shops close for periods, and commercial parts distribution centres see demand that varies by day of the week. Chapter 9 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) extends Palm's theorem to a nonstationary Poisson demand process with time-dependent resupply-time distributions, gives the compound (multi-unit order) version, and uses the result to compute, at any time $t$, the distribution of units in repair at the depot of a two-echelon system.

Timeline: Palm (1938) proved the stationary result for telephone traffic; Feeney and Sherbrooke (1966) extended it to compound Poisson demand; Hillestad and Carrillo (RAND, 1980) and Crawford (RAND, 1981) developed the time-dependent extensions, summarized by Carrillo (RAND, 1989). The chapter presents these results.

Setting

A single item is stocked at one location, and every demand is for one unit.

• Demand rate $\lambda(s) \ge 0$, integrable on bounded intervals, with mean function $m(t) = \int_0^t \lambda(s)\,ds$.
• Demand process: a nonstationary Poisson process with mean function $m$, with $N(0) = 0$. $N(t)$ counts demands in $[0,t]$ and $T_0 < T_1 < \cdots$ are the demand epochs.
• Resupply times: a unit demanded at time $s$ is resupplied within $w$ time units with probability $G_s(w)$. Resupply times are nonnegative, have finite expectations, are independent from unit to unit, and are independent of the demand process.
• $X(t)$ is the number of units in resupply at time $t$: demands in $[0,t]$ whose resupply is not complete at $t$.

The mean of $X(t)$ is

$$\alpha(t) = \int_0^t \bigl(1 - G_s(t-s)\bigr)\lambda(s)\,ds.$$

In the compound version (Section 9.2), orders arrive as above and each order is for $Q \ge 1$ units, with a time-stationary law $u_j = P(Q = j)$. All units of an order share its resupply time, $Y(t)$ counts units demanded in $[0,t]$, and $u^{(n)}_k$ is the $n$-fold convolution of $(u_j)$.

In the two-echelon version (Section 9.3), base $i$ has failure rate $\lambda_i$. A failure is repaired at the base with probability $r_i$ and at the depot otherwise. Depot repair of a failure occurring at time $u$ takes a deterministic time $D(u)$ with $D(t) + t \ge D(s) + s$ for $s < t$ (no crossing). Write $\tilde t = \inf\{u \ge 0 : D(u) + u > t\}$.

Formalization targets

Goal: Theorem 13 (p. 216)

For every $t \ge 0$,

$$P\{X(t) = k\} = e^{-\alpha(t)}\frac{\alpha(t)^k}{k!}, \qquad k = 0,1,2,\dots$$

This is an exact statement at each finite time, not a limit. With constant $\lambda$ and $G_s = G$ it reduces to the finite-time step of Palm's theorem.

Milestones

1. $E[N(t)] = m(t)$ (Section 9.1, p. 216).
2. Theorem 12 (p. 216): given $N(t) = n$, the epochs $T_0, \dots, T_{n-1}$ are distributed as the order statistics of $n$ i.i.d. variables with distribution function $F(x) = m(x)/m(t)$ on $[0,t)$.
3. The binomial step of the proof of Theorem 13 (pp. 216–217): $P\{X(t) = k \mid N(t) = n\} = \binom nk p^k(1-p)^{n-k}$, with $p = \int_0^t (1 - G_s(t-s))\lambda(s)/m(t)\,ds$.
4. Section 9.2 (p. 218): $E[Y(t)] = m(t)E[Q]$ and $\operatorname{Var}[Y(t)] = m(t)E[Q^2]$.
5. Theorem 14 (p. 218): $P[X(t) = k] = \sum_{n\ge1} u^{(n)}_k e^{-\alpha(t)}\alpha(t)^n/n!$ for $k \ge 1$, and $e^{-\alpha(t)}$ at $k = 0$.
6. Section 9.3.2 (p. 221): $P\{X_0(t) = k\} = e^{-m_0(\tilde t,t)} m_0(\tilde t,t)^k/k!$ with $m_0(\tilde t,t) = \int_{\tilde t}^t \sum_i \lambda_i(u)(1-r_i)\,du$.

A plain supporting item states that $N(t)$ is Poisson with mean $m(t)$, the factor the proof of Theorem 13 uses.

Significance

Theorem 13 gives the full distribution of the pipeline at every instant. Time-dependent expected backorders, $\sum_{x > s(t)} (x - s(t)) P\{X(t) = x\}$, and fill rates $P\{X(t) < s(t)\}$ follow from it, so stock levels can be planned against a surge or a repair outage without a steady-state approximation. Theorem 14 does the same for multi-unit orders. The depot result feeds the base-level convolution of Section 9.3.3, which in turn gives time-dependent performance measures for a two-echelon system.

These results are proved in the literature, and the chapter reproduces the proofs of Theorems 13 and 14. It cites Theorem 12 without proof ("similar to the one given in Chapter 3"). No machine-checked version of any of them is known, and neither Mathlib nor this platform has a Poisson process, stationary or not, a thinning theorem, or an order-statistics theorem. The formal content of this mission therefore includes the construction and the first distributional facts of the nonstationary Poisson process.

Difficulty

The algebra of the proof is a Poisson mixture of binomials and is short. The difficulty is Theorem 12 and its use. The obvious argument treats "the $n$ demands in $[0,t]$" as $n$ independent draws from $F$ and assigns each an independent resupply time with law $G_{\text{draw}}$. Making this rigorous requires identifying the conditional joint law of the epochs given $N(t) = n$. The resupply time of the $j$-th demand is not independent of its epoch: its law depends on the epoch. So it must be shown that, after conditioning, the marks attached to sorted epochs behave like marks attached to unsorted i.i.d. draws. The book's constant-rate argument (Chapter 3) uses the uniform density $n!/t^n$ on the simplex. Here the density involves $\lambda$, which may vanish on intervals, and $m$ need not be invertible.

Formalization scope

• Demand process. The nonstationary Poisson process is constructed, not postulated. With i.i.d. exponential(1) gaps and unit-rate points $\Gamma_k = A_0 + \cdots + A_k$, the $k$-th demand occurs at $T_k = \inf\{s \ge 0 : m(s) \ge \Gamma_k\}$, and $N(t) = \#\{k : \Gamma_k \le m(t)\}$.
• Resupply times. Resupply times are $\rho(T_k, U_k)$ for a jointly measurable $\rho \ge 0$ and i.i.d. marks $U_k$ independent of the gaps, with $G_s(w) = \nu\{\rho(s,\cdot) \le w\}$. Every measurable family $G_s$ arises this way, and joint measurability makes $\alpha(t)$ a genuine integral. Independence of resupply times from the demand process is not written in Theorem 12 or 13 but is used in the proof; it is part of the model.
• Pinnings and conventions.
  • "$\lambda$ integrable" is read as integrable on bounded intervals.
  • Time is $t \ge 0$.
  • Theorem 12 assumes $m(t) > 0$, since $F$ is $0/0$ otherwise, and sets $F = 0$ on $(-\infty,0)$.
  • Conditional probabilities are written as joint probabilities.
  • $E[Y(t)]$ is stated in $[0,\infty]$; the variance identity assumes $E[Q^2] < \infty$.
  • $\tilde t$ is an infimum over $u \ge 0$, and $D \ge 0$.
  • Counts are cardinalities, and are $0$ on the null event where they would be infinite.
• Corrections. Theorem 14's printed sum starts at $n = 1$, which gives $P[X(t) = 0] = 0$. The statement keeps the book's formula for $k \ge 1$ and adds $P[X(t) = 0] = e^{-\alpha(t)}$. The depot's Poisson demand stream with rate $\sum_i \lambda_i(1-r_i)$ is generated from the bases' processes and independent repair-location choices, not assumed.
• Not stated.
  • Eqs. (9.1)–(9.2), the FCFS depot backorders owed to base $i$: the derivation on p. 221 is informal, and (9.1) prints the exponent $s_0(t-1)$ for $s_0(t)-1$.
  • The base analysis of Section 9.3.3.
  • The compound law of $Y(t)$ on p. 217, which has the same $n = 0$ omission.
• Trivialization ruled out. $X(t)$ is computed from the demand epochs and resupply times, not defined by its law, and resupply times cannot depend on the demand epochs except through the prescribed $G_s$. Either shortcut would make the goal empty or false.
• Infrastructure. The time-changed Poisson construction, its count law, the order-statistics property and marked thinning are reusable well beyond this chapter: in queueing ($M_t/G_t/\infty$), in reliability, and in the stationary Palm mission of this series. Contributions of these general lemmas are welcome.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Chapter 9, pp. 215–222. https://doi.org/10.1007/b138879
• C. Palm, "Analysis of the Erlang traffic formulae for busy-signal arrangements", Ericsson Technics 5, 1938, 39–58.
• G. J. Feeney and C. C. Sherbrooke, "The (s−1, s) inventory policy under compound Poisson demand", Management Science 12(5), 1966, 391–411. https://doi.org/10.1287/mnsc.12.5.391
• R. J. Hillestad and M. J. Carrillo, Models and techniques for recoverable item stockage when demand and the repair processes are nonstationary — Part I: Performance measurement, Report N-1482-AF, RAND Corporation, 1980.
• G. B. Crawford, Palm's theorem for nonstationary processes, Report R-2750-RC, RAND Corporation, 1981.
• M. J. Carrillo, Generalizations of Palm's theorem and Dyna-METRIC's demand and pipeline variability, Report R-3698-AF, RAND Corporation, 1989.

Strassen's Theorems and the Stochastic Ordering of Queues

Background

Chapters 1–3 of Baccelli and Brémaud's Elements of Queueing Theory compute exact quantities: Palm identities, stability criteria, PASTA, Pollaczek–Khinchin. Chapter 4 asks a different question. When you cannot compute a queue, can you at least say it is better than another one?

That requires an order on distributions. The chapter builds a family of them — integral orders — by choosing a class ℒ of test functions and declaring F ≤_ℒ G when ∫f dF ≤ ∫f dG for all f ∈ ℒ. Three matter: {i} the non-decreasing functions, giving the strong (stochastic) order; {cx} the convex functions, giving the convex order; and their intersection {icx}.

The goal

An integral order compares two distributions that need not live on the same probability space, and that is both its convenience and its difficulty. Strassen's theorems say each of these orders is secretly a statement about a coupling.

Theorem 4.2.2 (p.278), Strassen's ≤_cx theorem:

F ≤_cx G   ⟺   ∃ X ~ F, Y ~ G on one space with  E[Y | X] = X  a.s.
F ≤_icx G  ⟺   the same with  E[Y | X] ≥ X  a.s.

The convex order holds exactly when G is a martingale dilation of F — obtained by spreading each point out without moving its conditional mean. That is what makes the order usable: comparison results for queues become induction arguments on a coupling instead of analytic manipulations of convolutions of c.d.f.'s.

Its companion Theorem 4.2.1 is the ≤_st version, where the coupling is the simpler X ≤ Y a.s. In dimension one both are explicit — take X = F⁻¹(U), Y = G⁻¹(U) for a uniform U. In dimension n there is no such formula, and that is why these are Strassen's theorems. The book attributes both to Strassen (1965) and proves neither.

Why FIFO is optimal

§4.1 is a different kind of comparison: not between two queues, but between two service disciplines for the same queue. The order there is majorization ≺, which compares how spread out two vectors of the same total are.

The answer is that FIFO minimizes E⁰[f(V)] for every convex f (Property 4.1.3), and the proof is an interchange argument. Under any non-preemptive discipline that uses no information on the service times, customer k effectively receives service σ_{γ(k)} for some permutation γ; Lemma 4.1.3 shows the same queue is produced by FIFO fed with that reordered input, and that the reordering does not change the law of the input. Lemma 4.1.4 passes to the limit, which needs ρ < 1. Lemmas 4.1.1 and 4.1.2 then do the combinatorics: undoing one inversion of γ makes the waiting-time vector less spread out, so the identity permutation — FIFO — is extremal.

Feller's paradox, and what survives it

§4.4 compares time-stationary queues, and opens with a warning. T_n[P⁰] ≤_i T̃_n[P̃⁰] for every n does not imply T_n[P] ≤_i T̃_n[P̃]: Example 4.4.1, "Feller's paradox revisited", exhibits a Poisson process and a renewal process where the Palm order holds and the stationary one fails. The order does not pass from the Palm probability to the stationary one.

For ≤_cx it does. Lemma 4.4.1 is why: it expands E_P[f(N[0,x))] as a series of second differences of f against Palm expectations, and a convex f makes every coefficient non-negative. Lemma 4.4.2 handles the S-orders, built by dividing Palm integrals by the mean cycle length, and shows that the normalisation does not hide the comparison it normalises by.

Formalization scope

• Orders. ≤_i, ≤_cx, ≤_icx on distributions on ℝⁿ are integral orders over the book's test classes (§4.2.1), with the page's qualification that only test functions with well-defined integrals count. Majorization ≺ is (4.1.2) with increasing reorderings of both vectors.
• Strassen. Both theorems are stated as equivalences, with the coupling existential over the probability space. Theorem 4.2.2 carries both clauses — E[Y | X] = X for ≤_cx, E[Y | X] ≥ X for ≤_icx, as conditional expectations given σ(X) — and assumes both distributions integrable; Theorem 4.2.1 has no integrability hypothesis. A one-directional statement (the Jensen half) is not the theorem.
• The queue of §4.1.3 is constructed: a GI/GI input (i.i.d. inter-arrival and service times, independent), a single work-conserving server started empty, and any non-preemptive discipline whose choices are measurable in the information the book's σ-field 𝒢_t carries (arrivals, service times of customers already started) plus external randomisation. FIFO is one such discipline. The interchange permutations γ_n and their limit γ are built from the schedule as on pp.268–270; Lemma 4.1.4 assumes ρ = E[σ₀]/E[τ₀] < 1.
• Lemma 4.4.1 is stated with the exact second-difference series and assumes that series converges absolutely; the page states it for all f, which fails for heavy-tailed counts and sparse f.
• The S-orders test against {I-ℒ} — primitives ∫_0^t f(u, x) du of test functions — and apply only to distributions whose first coordinate is a.s. positive with a finite mean.

What this mission provides

None of it exists. Mathlib has no stochastic order, no convex order, no increasing-convex order, no majorization, no Schur-convexity and no Strassen theorem; the platform returns zero hits for q=stochastic ordering. Everything in this chapter is new substrate — and §§4.1–4.2 need nothing from Palm calculus, so this mission can be read on its own.

Motivation

Interior-point methods solve linear programs by moving through the interior of the feasible region instead of along its edges, as the simplex method does. The methods used in practice are path-following methods: they track a curve, the central path, that runs through the interior of the feasible region and ends at an optimal solution. Before any such method can be analysed, the curve has to exist. This mission formalizes Chapter 17 of R. J. Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014), which defines the central path through the logarithmic barrier problem and proves that it exists exactly when the primal and the dual problem both have strictly positive feasible points.

The chapter's results have a short history. Barrier methods for nonlinear programming go back to Fiacco and McCormick (1968). Interest in interior-point methods for linear programming began with Karmarkar (1984), whose projective algorithm does not mention a central path; the connection between Karmarkar's method and the primal–dual central path was found by Megiddo (1989), with central points traced back to Huard (1967) and an extended study of the path by Bayer and Lagarias (1989). The chapter is the textbook entry point to this line of work and the foundation for the path-following algorithm of Chapter 18.

Setting

Let $A$ be a real $m \times n$ matrix, $b \in \mathbb{R}^m$ and $c \in \mathbb{R}^n$. The primal linear program is to maximize $c^T x$ subject to $Ax \le b$, $x \ge 0$; its dual is to minimize $b^T y$ subject to $A^T y \ge c$, $y \ge 0$. With slack variables $w \in \mathbb{R}^m$ and $z \in \mathbb{R}^n$ they read (17.1)

$$Ax + w = b,\ x, w \ge 0 \qquad\text{and}\qquad A^T y - z = c,\ y, z \ge 0.$$

For a vector $\xi$, $\xi > 0$ means that every component is strictly positive. The primal feasible region has nonempty interior when some $(\bar x, \bar w)$ satisfies $A\bar x + \bar w = b$ with $\bar x > 0$, $\bar w > 0$; the dual feasible region has nonempty interior when some $(\bar y, \bar z)$ satisfies $A^T \bar y - \bar z = c$ with $\bar y > 0$, $\bar z > 0$.

For a parameter $\mu > 0$, the barrier function (17.7) is

$$f(x, w) = c^T x + \mu \sum_{j=1}^n \log x_j + \mu \sum_{i=1}^m \log w_i ,$$

and the barrier problem (17.2) is to maximize $f(x, w)$ subject to $Ax + w = b$, over the domain $x > 0$, $w > 0$ where the logarithms are finite. A solution of the barrier problem is a point of that domain at which $f$ attains its maximum over the domain.

Writing $X, Z, Y, W$ for the diagonal matrices carrying $x, z, y, w$ and $e$ for the all-ones vector, the primal–dual central-path system (17.6) is

$$Ax + w = b, \qquad A^T y - z = c, \qquad XZe = \mu e, \qquad YWe = \mu e,$$

with $x, w, y, z > 0$. The last two equations say $x_j z_j = \mu$ and $y_i w_i = \mu$ for all $j$ and $i$. The set of its solutions $(x_\mu, w_\mu, y_\mu, z_\mu)$, $\mu > 0$, is the primal–dual central path.

The chapter also uses one fact from nonlinear programming: for the problem "maximize $f(x)$ subject to $g_i(x) = 0$, $i = 1, \dots, m$", a critical point is a feasible $x^*$ with $\nabla f(x^*) = \sum_i y_i \nabla g_i(x^*)$ for some Lagrange multipliers $y_i$ (17.3), and $H_f(x^*)$ is the Hessian of $f$ at $x^*$.

Formalization targets

Goal: Theorem 17.2 (p. 265)

For each fixed $\mu > 0$,

$$\exists\, (x, w) \text{ solving the barrier problem} \iff \big(\exists\, \bar x, \bar w > 0 : A\bar x + \bar w = b\big) \wedge \big(\exists\, \bar y, \bar z > 0 : A^T\bar y - \bar z = c\big).$$

Both directions are part of the goal. The statement fixes no constants and no rate; it asserts only when the barrier problem is solvable.

Milestones

1. Theorem 17.1 (p. 261), second-order sufficiency under linear constraints: if the constraints are linear, a critical point $x^*$ with $\xi^T H_f(x^*)\xi < 0$ for every $\xi \ne 0$ satisfying $\xi^T \nabla g_i(x^*) = 0$ for all $i$ is a local maximum on the feasible set.
2. Exercise 10.7 (p. 150): if the primal is feasible and its feasible set $\{x : Ax \le b,\ x \ge 0\}$ is bounded, then there are $y > 0$, $z > 0$ with $A^T y - z = c$.
3. Corollary 17.3 (p. 266): if the primal feasible set (or the dual feasible set) has nonempty interior and is bounded, then for each $\mu > 0$ the system (17.6) has exactly one solution with $x, w, y, z > 0$.

The corollary is stronger than the goal in one direction (it adds uniqueness and the dual variables) and weaker in another (it assumes boundedness).

Significance

The result itself. Theorem 17.2 gives an exact criterion for the barrier problem to be solvable for a fixed $\mu$, and Corollary 17.3 turns it into the statement that the central path is a well-defined curve $\mu \mapsto (x_\mu, w_\mu, y_\mu, z_\mu)$ for all $\mu > 0$. Every path-following method, including the one analysed in Chapter 18 of the same book, targets points on this curve; without existence and uniqueness the "target" of an iteration is undefined. The system (17.6) is also the starting point of the primal–dual Newton step.

Formalizing it. These results are classical and proved in the book; none is formalized in the $Ax \le b$, $x \ge 0$ form used here. The platform has the converse fact in the standard form $Ax = b$, $x \ge 0$ (a solution of the central-path conditions minimizes the barrier, Introduction to Linear Optimization), but not existence. A formal proof of Theorem 17.2 and Corollary 17.3 produces a reusable existence theorem for the central path that downstream missions on path-following and self-dual methods can import.

Difficulty

The "if" direction of Theorem 17.2 is an existence claim on a set that is neither closed nor bounded: the domain $x > 0$, $w > 0$ is open, and the feasible region itself may be unbounded, so the obvious appeal to "a continuous function on a compact set attains its maximum" does not apply directly. The example "maximize $0$ subject to $x \ge 0$" (p. 264), whose barrier $\mu \log x$ has no maximum, shows that the dual hypothesis cannot be dropped. The "only if" direction, which the book calls trivial and does not prove, needs first-order conditions at a maximizer over a relatively open set.

Theorem 17.1 needs a second-order Taylor expansion with a remainder that is $o(\|\xi\|^2)$ uniformly along the constraint subspace, not along individual lines. Exercise 10.7 is a theorem of the alternative and is not a consequence of weak duality alone. Uniqueness in Corollary 17.3 requires the positivity of the solution: the equations $x_j z_j = \mu$, $y_i w_i = \mu$ admit sign-flipped solutions.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ; $A$ is a Matrix (Fin m) (Fin n) ℝ. The book's primal–dual pair in $Ax \le b$, $x \ge 0$ form with slacks is used throughout; there are no explicit constants in this chapter.

Conventions committed to:

• "Nonempty interior" means a feasible point with every component strictly positive, as the proof of Theorem 17.2 says. The topological interior of $\{(x, w) : Ax + w = b,\ x, w \ge 0\}$ in $\mathbb{R}^{n+m}$ is empty whenever $m \ge 1$; reading the theorem that way would make its right-hand side always false for $m \ge 1$, and that reading is ruled out.
• The barrier problem is posed over $x > 0$, $w > 0$ explicitly; Real.log returns $0$ at nonpositive arguments and is never evaluated there.
• Solutions of (17.6) are required to be strictly positive, as in Exercise 17.3 (p. 267).
• "Bounded" is Bornology.IsBounded of the feasible set in $\mathbb{R}^n$ (resp. $\mathbb{R}^m$).
• In Theorem 17.1 the constraints are $Gx = \beta$; $f$ is differentiable near $x^*$ with derivative differentiable at $x^*$, and $\xi^T H_f(x^*) \xi$ is the second Fréchet derivative applied to $(\xi, \xi)$. The local maximum is relative to the feasible set.

Infrastructure a complete development needs: attainment of maxima on compact sets (IsCompact.exists_isMaxOn in Mathlib), first-order conditions on relatively open sets, a theorem of the alternative for Exercise 10.7, and concavity facts about the logarithm. A second-order sufficient condition under affine constraints is not in Mathlib and is reusable beyond linear programming. Proofs of any milestone, including the "only if" half of the goal separately, are welcome contributions.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 17 and Exercise 10.7. https://doi.org/10.1007/978-1-4614-7630-6
• A. V. Fiacco and G. P. McCormick, Nonlinear Programming: Sequential Unconstrained Minimization Techniques, Wiley, 1968. https://doi.org/10.1137/1.9781611971316
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4 (1984), 373–395. https://doi.org/10.1007/BF02579150
• N. Megiddo, Pathways to the optimal set in linear programming, in Progress in Mathematical Programming, Springer, 1989, 131–158. https://doi.org/10.1007/978-1-4613-9617-8_8
• D. A. Bayer and J. C. Lagarias, The nonlinear geometry of linear programming I, II, Transactions of the AMS 314 (1989), 499–526 and 527–581. https://doi.org/10.1090/S0002-9947-1989-1005525-6

Motivation

Every linear program comes with a second linear program, its dual, and most of what is known about linear programming is a statement about how the two interact. Weak duality gives certificates of optimality; strong duality says those certificates always exist; complementary slackness turns optimality into a system of equations. These three facts are the core of any first course in optimization and of every correctness argument for the simplex method.

Strict complementarity is the sharpest statement of the same kind. Complementary slackness says that in each pair (a primal variable and its dual slack, a dual variable and its primal slack) at least one member vanishes at optimality. Strict complementarity says that some optimal pair can be chosen so that exactly one member vanishes in each pair. The result is due to Goldman and Tucker (1956). It is what identifies the optimal face of a linear program and its partition of the variables into those that can be positive at an optimum and those that cannot, and it is a standing ingredient in the analysis of interior-point methods, which approach this strictly complementary optimum rather than a vertex.

This mission formalizes the chain from duality to strict complementarity as it is developed in Chapters 5 and 10 of Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014, doi:10.1007/978-1-4614-7630-6). It is the second mission of a series on that book.

Timeline:

• 1902 — Farkas publishes the lemma on the solvability of linear inequality systems.
• 1947–1951 — von Neumann, and Gale, Kuhn and Tucker, establish linear programming duality.
• 1956 — Goldman and Tucker prove the existence of strictly complementary optimal solutions (in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38).

Setting

Fix integers $m, n \ge 0$, a real $m \times n$ matrix $A = (a_{ij})$, a vector $b \in \mathbb{R}^m$ and a vector $c \in \mathbb{R}^n$. The primal problem is

$$\text{maximize } c^T x \quad\text{subject to}\quad Ax + w = b,\quad x \ge 0,\ w \ge 0, \qquad (10.9)$$

where $w = b - Ax$ is the primal slack. The dual problem is

$$\text{minimize } b^T y \quad\text{subject to}\quad A^T y - z = c,\quad y \ge 0,\ z \ge 0, \qquad (10.10)$$

where $z = A^T y - c$ is the dual slack. A vector $x$ is primal feasible if $x \ge 0$ and $w \ge 0$; it is primal optimal if it is feasible and $c^T x' \le c^T x$ for every feasible $x'$. Dual feasibility and dual optimality are defined in the same way, with minimization. Inequalities between vectors are componentwise, and $\xi > 0$ means that every component of $\xi$ is strictly positive.

A halfspace of $\mathbb{R}^n$ is a set $\{x : a^T x \le \beta\}$ with $a \ne 0$; a polyhedron is a set $\{x : Ax \le b\}$ for some $m$, $A$ and $b$.

In the Lean development these objects live in the namespace VanderbeiLP.StrictComp: primalSlack A b x, dualSlack A c y, PrimalFeasible, DualFeasible, PrimalOptimal, DualOptimal, IsHalfspace, IsPolyhedron.

Formalization targets

Goal: Strict Complementary Slackness (Theorem 10.7)

If the primal (10.9) has an optimal solution, then there exist a primal optimal $x^*$ and a dual optimal $y^*$, with slacks $w^* = b - Ax^*$ and $z^* = A^T y^* - c$, such that

$$x^* + z^* > 0 \qquad\text{and}\qquad y^* + w^* > 0.$$

The only hypothesis is primal optimality; the existence of a dual optimum is part of the conclusion.

Milestones

1. Theorem 5.1 (Weak Duality). Primal feasible $x$ and dual feasible $y$ satisfy $c^T x \le b^T y$.
2. Theorem 5.2 (Strong Duality). If the primal has an optimal $x^*$, the dual has an optimal $y^*$ with $c^T x^* = b^T y^*$.
3. Theorem 5.3 (Complementary Slackness). Feasible $x$, $y$ are both optimal if and only if $x_j z_j = 0$ for all $j$ and $w_i y_i = 0$ for all $i$.
4. Lemma 10.5 (Farkas' Lemma). $Ax \le b$ has no solution if and only if some $y$ satisfies $A^T y = 0$, $y \ge 0$, $b^T y < 0$.
5. Theorem 10.4 (Separation of polyhedra). Two disjoint nonempty polyhedra lie in two disjoint halfspaces.
6. Theorem 10.6. If both problems are feasible, there are feasible $\bar x$, $\bar y$ with $\bar x + \bar z > 0$ and $\bar y + \bar w > 0$.

Theorem 10.6 is the feasible-solution version of the goal; Theorem 10.4 is a further consequence of Farkas' Lemma in the same chapter.

Significance

Strict complementarity determines the optimal partition: the set of indices $j$ for which some optimal $x^*$ has $x^*_j > 0$ is exactly the complement of the set for which some optimal dual slack $z^*_j$ is positive. This partition describes the optimal faces of both problems, is the object that interior-point methods recover in the limit, and is the starting point of sensitivity analysis beyond a single optimal basis. Farkas' Lemma and the separation theorem are the linear-algebraic form of convex separation and are reused across optimization, game theory and polyhedral combinatorics.

All results of this mission are classical and proved in the literature. What the mission adds is a machine-checked version of them in one fixed linear-programming form, the inequality form with explicit slacks used throughout Vanderbei's book. Weak duality, strong duality and complementary slackness are already formalized on this platform for other forms (Bertsimas–Tsitsiklis's general form, a minimization, and a covering pair with the roles of primal and dual exchanged). Those statements are equivalent to the ones here only after a transformation (negating the objective, swapping primal and dual), so they are not the same theorems. The Farkas variant for inequality systems, the separation theorem for two polyhedra, and both strict complementarity theorems have no formal counterpart on the platform.

Difficulty

Weak duality and the converse direction of complementary slackness are short computations. The substance lies elsewhere. Strong duality and Farkas' Lemma require a genuine existence argument; the book obtains them from the simplex method, whose termination is itself a nontrivial fact, and any other route needs an independent theorem of the alternative.

For strict complementarity the obvious attempt fails. Complementary slackness gives, for each optimal pair, only that one member of each complementary pair vanishes; nothing in a single optimal basic solution forces the other member to be positive, and in degenerate problems every basic optimal pair can fail strictness. A strictly complementary pair is in general not a vertex of either optimal face, so it cannot be found by inspecting basic solutions. The goal also asks for more than Theorem 10.6: the positivity must be achieved within the optimal sets, which are faces cut out by an additional objective-level constraint, so the feasible-solution argument does not transfer verbatim.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ; the constraint matrix is Matrix (Fin m) (Fin n) ℝ; m and n are arbitrary natural numbers, including zero. The slacks are functions of the solution (primalSlack A b x = b - A *ᵥ x, dualSlack A c y = Aᵀ *ᵥ y - c), never free variables, so a "solution $(x, w)$" of the book is the vector $x$ with the slack it determines. Optimality is attainment of the maximum (minimum) over the feasible set; no supremum, value function or extended reals are involved. The strict inequality $\xi > 0$ is written componentwise as ∀ j, 0 < x j + dualSlack A c y j and ∀ i, 0 < y i + primalSlack A b x i.

A halfspace carries a nonzero normal vector. Without that requirement the empty set would be a halfspace and the separation theorem would be trivial; the formal definition rules this out.

The book states every result in this mission with its hypotheses explicit, and none of them asserts the existence of an unspecified constant, so no explicit-constant instantiation was needed. The remark after Theorem 10.7 refers to "the complementary slackness theorem (Theorem 5.1)"; the complementary slackness theorem is Theorem 5.3, and the milestones follow the theorem numbering.

A complete development needs a theorem of the alternative for real linear inequality systems (Mathlib has Farkas-type results for cones and the geometric Hahn–Banach theorem, but no ready-made matrix version of Lemma 10.5) and elementary convex-combination arguments on feasible sets. The definitions of this mission are self-contained and reusable for any later chapter that works in Vanderbei's inequality form. Proofs of any milestone are welcome, as are proofs that avoid the simplex method.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014. doi:10.1007/978-1-4614-7630-6
• J. Farkas, "Theorie der einfachen Ungleichungen", Journal für die reine und angewandte Mathematik 124 (1902), 1–27. doi:10.1515/crll.1902.124.1
• A. J. Goldman and A. W. Tucker, "Theory of linear programming", in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97.
• D. Gale, H. W. Kuhn and A. W. Tucker, "Linear programming and the theory of games", in Activity Analysis of Production and Allocation, Wiley, 1951, 317–329.

Motivation

Large convex programs often have a block structure: a small set of "complicating" variables $x$ couples otherwise separate subproblems in the remaining variables $y$. Decomposition with respect to variables fixes $x$, solves the subproblem in $y$, and treats the optimal subproblem value as a function of $x$ alone. The outer problem in $x$ is then small but nonsmooth, because the optimal value of a constrained program is generally not differentiable in its parameters. Shor's Chapter 4 (Shor 1985, Ch. 4) presents this reduction as a principal application of subgradient methods: once a subgradient of the outer function can be read off from the subproblem, the methods of Chapters 2–3 apply directly. The same construction underlies Benders decomposition (Benders 1962) and its convex generalization (Geoffrion 1972), and parametric decomposition schemes for linear programs.

The chapter's other numbered results serve the same programme from the dual side: the Lagrangian dual function of a program over a compact set gives a lower bound usable in branch and bound (Theorem 4.3), exact nonsmooth penalty functions turn a constrained convex program into one unconstrained nonsmooth minimization (Theorem 4.2; nonsmooth penalties were first studied systematically by I. I. Eremin, 1967), and a stochastic transportation model is shown to be a convex program before being solved through its dual (Lemma 4.3).

Setting

The variables split into $x \in E^x_l$ and $y \in E^y_m$ (Euclidean spaces, inner product $(\cdot,\cdot)$). The problem is

$$\min_{x,y} f_0(x,y) \quad \text{s.t.} \quad f_i(x,y) \le 0,\quad i = 1,\dots,n, \qquad (4.1)\text{–}(4.2)$$

with $f_0, f_1, \dots, f_n$ convex functions of $z = (x,y)$ (jointly convex), finite everywhere. For a fixed $\bar x$, the subproblem (4.3)–(4.4) is $\min_{y \in D(\bar x)} f_0(\bar x, y)$ with $D(\bar x) = \{y : f_i(\bar x,y) \le 0\}$. Where it has a solution $y(\bar x)$, the value function is

$$\Phi(\bar x) = \min_{y \in D(\bar x)} f_0(\bar x,y). \qquad (4.5)$$

The Slater condition at $\bar x$ asks for a $y$ with $f_i(\bar x,y) < 0$ for all $i$. The Lagrange function is $L_U(x,y) = f_0(x,y) + \sum_i U_i f_i(x,y)$, and $U \ge 0$ are Kuhn–Tucker multipliers at $\bar x$ when $\Phi(\bar x) = \min_y L_U(\bar x,y)$. A subgradient of a function of $(x,y)$ is written through its projections $(g^x, g^y)$ on the two blocks; a subgradient of $\Phi$ at $\bar x$ is a $g$ with $\Phi(x) - \Phi(\bar x) \ge (x - \bar x, g)$.

Formalization targets

Goal: Theorem 4.1 (p. 94)

If $W$ is a convex set of $x$-values at which the subproblem has a solution, then $\Phi$ is convex on $W$; and if $\bar x \in W$ satisfies the Slater condition, then for every optimal $y(\bar x)$, multipliers $U$ exist, $L_U$ has a subgradient at $(\bar x, y(\bar x))$ with vanishing $y$-projection, and the $x$-projection of any such subgradient satisfies

$$g_\Phi(\bar x) = g^x_{L_U}(\bar x, y(\bar x)) \in \partial \Phi(\bar x). \qquad (4.6)$$

Milestones for the goal

1. Convexity of $\Phi$ on $W$ (Theorem 4.1, first assertion).
2. Existence of Kuhn–Tucker multipliers for the subproblem under Slater (p. 95, display).
3. Existence of a subgradient of $L_U$ with vanishing $y$-projection (p. 95).
4. Formula (4.6) for a given multiplier vector and such a subgradient (p. 95, final display).

Further results of the chapter

5. Corollary (4.7): if each $f_\alpha(x,\cdot)$ is continuously differentiable in $y$, then $g^x_{f_0} + \sum_i U_i g^x_{f_i}$, built from arbitrary subgradients of the $f_\alpha$, is a subgradient of $\Phi$.
6. Lemma 4.3: the stochastic transportation problem (4.163)–(4.165) is a convex program.
7. Theorem 4.2: with nonsmooth penalties $p_i$ whose slopes $c_i = \lim_{t\to0+} p_i(t)/t$ exceed a Lagrange multiplier vector $\bar y$, the minimizers of $S = f_0 + \sum p_i \circ f_i$ are exactly the solutions of the constrained program; and if a minimizer of $S$ solves the program, some multiplier vector satisfies $\bar y \le c$.
8. Theorem 4.3: for $\Phi(u) = \min_{x\in X}[f_0 + \sum u_i f_i]$ over a compact $X$, $Q = \max_{u\ge0}\Phi(u) \le f^*$.

Significance

The result itself. Theorem 4.1 is what makes decomposition with respect to variables an instance of convex nonsmooth minimization: the outer problem is convex, and one subproblem solve returns both $\Phi(\bar x)$ and a subgradient. The algorithm on p. 96 — solve the subproblem at $x_k$, form $g_\Phi(x_k)$ by (4.6) or (4.7), take a subgradient step — is exactly this, and the step-size theory of Chapter 2 then gives convergence. The Corollary is the version used in practice for linear and quadratic subproblems, where multipliers and partial subgradients are computed directly. Theorem 4.2 justifies replacing constraints by nonsmooth penalties of finite slope, and Theorem 4.3 is the weak-duality bound behind Lagrangian relaxation in branch and bound.

Formalizing it. All results are classical and proved in the book; none is formalized as stated here. The platform already has related statements with different shapes: convexity of the perturbation value function in the constraint right-hand side (VectorSpaceOpt.perturbationValue_convex, Luenberger), Slater strong duality over the whole space (ConvexOptimization.slater_strong_duality), weak duality with an unconstrained domain (ConvexOptimization.weak_duality), weak Lagrangean duality for integer programs (LinearOptimization.integer_program_weak_lagrangean_duality), and the LP special case of convexity of the optimal cost (LinearOptimization.lp_optimal_cost_convex_in_rhs). This mission adds the partial-minimization form in which one block of variables is minimized out under joint convexity, its subgradient calculus, exact nonsmooth penalties, and weak duality over a compact domain.

Difficulty

Convexity of $\Phi$ is elementary once the minimum is attained. The subgradient formula is where the obvious argument fails: an arbitrary subgradient of $L_U$ at $(\bar x, y(\bar x))$ does not project to a subgradient of $\Phi$, because its $y$-projection contributes a term $(y(x) - y(\bar x), g^y)$ of unknown sign. The theorem needs a subgradient whose $y$-projection vanishes, and its existence is a separate fact about partial minimization of a jointly convex, everywhere-finite function. The multipliers come from the Kuhn–Tucker theorem for the subproblem, which requires the Slater condition. In the Corollary, the difficulty is to show that differentiability in $y$ forces the $y$-projection of any combination $g_{f_0} + \sum U_i g_{f_i}$ to vanish. In Theorem 4.2 the necessity part needs a subdifferential chain rule for $p_i \circ f_i$.

Formalization scope

• $E^x_l$, $E^y_m$ and $E_N$ are EuclideanSpace ℝ (Fin l), EuclideanSpace ℝ (Fin m), EuclideanSpace ℝ (Fin N); constraints are indexed by Fin n (or Fin m). All functions are real-valued and finite everywhere; joint convexity is convexity on the product $E^x_l \times E^y_m$.
• $\Phi$ is a real infimum over $D(x)$. It is the book's minimum wherever the minimum is attained, and every statement assumes attainment at each point of $W$. A statement about $\Phi$ at points where the subproblem has no solution would be about Lean's default value $0$, and is ruled out by these hypotheses.
• "Convex on some convex subset $W$ of $E_n$" is read as convexity on every convex $W$ on which $\Phi$ is defined. A formalization quantifying over a single unspecified $W$ (e.g. a singleton) would be trivially true.
• Formula (4.6) is stated for subgradients of $L_U$ whose $y$-projection is zero, as the book's proof uses it; the subgradient inequality for $\Phi$ is stated on all of $W$.
• Kuhn–Tucker multipliers relative to an optimal $\bar y$: $U \ge 0$, $U_i f_i(\bar x,\bar y) = 0$, and $\bar y$ minimizes $L_U(\bar x,\cdot)$ over all $y$.
• Theorem 4.2: a Lagrange multiplier vector is $\bar y \ge 0$ with $f_0 + \sum\bar y_i f_i \ge f^*$ everywhere, $f^*$ the finite optimal value; the necessity clause is read as "for some multiplier vector" (for all multiplier vectors it is false); the limits $c_i$ are given as hypotheses.
• Theorem 4.3: the minimum (4.187) attained for every $u \ge 0$ (the book's "min"; no continuity assumed); $f^*$ attained; $Q$ attained as the book's "max" presupposes.
• Lemma 4.3: demands with densities and finite mean, penalty coefficients $r_j \ge 0$.

Useful infrastructure beyond this mission: partial minimization of jointly convex functions, subgradients on product spaces, and a Kuhn–Tucker saddle-point theorem for convex programs with inequality constraints. Proofs of any milestone, and reusable lemmas for these, are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, Ch. 4, pp. 93–96, 131–133, 146–148. https://doi.org/10.1007/978-3-642-82118-9
• J. F. Benders, Partitioning procedures for solving mixed-variables programming problems, Numerische Mathematik 4, 1962, 238–252. https://doi.org/10.1007/BF01386316
• A. M. Geoffrion, Generalized Benders decomposition, Journal of Optimization Theory and Applications 10, 1972, 237–260. https://doi.org/10.1007/BF00934810
• I. I. Eremin, The penalty method in convex programming, Soviet Mathematics Doklady 8, 1967, 459–462 (Shor's reference [22]).
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §29 (partial minimization and perturbation functions). https://doi.org/10.1515/9781400873173