The OR Formalization Drive

Control Theory Convex Optimization Linear algebra+3·Captain: mikedeng1

Robust Solutions to Least-Squares Problems with Uncertain Data IV: A Semidefinite Upper Bound on the Linear-Fractional Worst-Case Residual, Exact for Full PerturbationsResearch Paper

Motivation

Least-squares fitting is a standard tool in estimation, identification and data analysis, and its data $A$ , $b$ are rarely known exactly. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed to choose $x$ to minimize the worst-case residual over a set of admissible data perturbations. Earlier missions of this series treat unstructured perturbations of $[A\ b]$ and perturbations affine in a parameter vector. §5 of the paper covers a more general model, taken from robust identification (Doyle et al.): the perturbed data depend on an uncertain matrix $\Delta$ through a linear-fractional transformation. This form covers rational dependence of the data on uncertain parameters, max-norm bounds on independent parameters, and data matrices with some columns known exactly (pp. 1046–1047).

In this generality, deciding whether the worst-case residual is finite is NP-complete, and computing it is NP-hard even when the dependence is affine (§5.3, Lemma 5.1). Theorem 5.2 gives the tractable replacement: a semidefinite program whose value bounds the worst-case residual from above, and equals it when the perturbation is unstructured. The main tool is a structured form of the S-procedure. Robust control uses the same tool, with the scalings $S$ and $G$ below, to bound the real structured singular value (Fan, Tits and Doyle, 1991).

Setting

Vectors carry the Euclidean norm $\|v\|$ . For a matrix $X$ , $\|X\|$ is its largest singular value (operator norm between Euclidean spaces). Let $\mathcal D$ be a linear subspace of $\mathbb R^{N\times N}$ (the perturbation structure), and fix $A \in \mathbb R^{n\times m}$ , $b \in \mathbb R^n$ , $L \in \mathbb R^{n\times N}$ , $R_A \in \mathbb R^{N\times m}$ , $R_b \in \mathbb R^N$ , $D \in \mathbb R^{N\times N}$ . For $\Delta \in \mathcal D$ with $\det(I - D\Delta) \ne 0$ the perturbed data are

A(\Delta) = A + L\Delta(I - D\Delta)^{-1}R_A, \qquad b(\Delta) = b + L\Delta(I - D\Delta)^{-1}R_b .

With the normalization $\rho = 1$ (the paper's, with no loss of generality), the worst-case residual of $x \in \mathbb R^m$ is

r_{\mathcal D}(A,b,x) = \max_{\Delta \in \mathcal D,\ \|\Delta\| \le 1} \|A(\Delta)x - b(\Delta)\|

if $\det(I - D\Delta) \ne 0$ for every such $\Delta$ , and $+\infty$ otherwise (35). The commutant scalings are $\mathcal S = \{S = S^T : S\Delta = \Delta S\ \forall \Delta \in \mathcal D\}$ and $\mathcal G = \{G = -G^T : G\Delta = \Delta G\ \forall \Delta \in \mathcal D\}$ (37). The SDP constraint is

\mathcal F(\lambda,S,G,x) = \begin{bmatrix} \Theta & \begin{matrix} Ax - b \\ R_Ax - R_b\end{matrix} \\ \begin{matrix}(Ax-b)^T & (R_Ax - R_b)^T\end{matrix} & \lambda\end{bmatrix} \succ 0, \quad \Theta = \begin{bmatrix} \lambda I - LSL^T & -LSD^T + LG \\ -DSL^T + G^TL^T & S + DG - GD^T - DSD^T\end{bmatrix}. \qquad (38),(39)

Formalization targets

Goal: Theorem 5.2 (corrected)

For all $x$ and $\lambda$ :

\text{(a)}\quad S \in \mathcal S,\ G \in \mathcal G,\ S \succ 0,\ G\Delta \text{ skew } \forall \Delta \in \mathcal D,\ \mathcal F(\lambda,S,G,x) \succ 0 \ \Longrightarrow\ \lambda > r_{\mathcal D}(A,b,x);

\text{(b)}\quad \mathcal D = \mathbb R^{N\times N},\ \lambda > r_{\mathcal D}(A,b,x) \ \Longrightarrow\ \exists s > 0:\ \mathcal F(\lambda, sI, 0, x) \succ 0 .

Part (a) says the value of the SDP $\inf\{\lambda : (\lambda, S, G) \text{ feasible}\}$ (40) is an upper bound on $r_{\mathcal D}$ . Part (b) says this upper bound is exact for full perturbations, including the case $r_{\mathcal D} = \infty$ , where (40) is infeasible.

Milestones

Lemma 2.2, both directions: the full-block S-procedure. $\det(I - T_4\Delta) \ne 0$ and $T(\Delta) \succeq 0$ for all $\|\Delta\| \le 1$ if and only if $\|T_4\| < 1$ and a one-scalar LMI (10) holds (the "only if" under $T_2 \ne 0$ or $T_3 = 0$ ).
Lemma 2.3: sufficiency of the scaled LMI for a structured $\mathcal D$ , and its strict necessity for $\mathcal D = \mathbb R^{N\times N}$ .
§5.4, p. 1047: $\lambda > r_{\mathcal D}(A,b,x)$ if and only if a linear-fractional matrix function of $\Delta$ is positive definite on the structured unit ball.
§5.4, (38)–(39): the certificate (a) in the paper's own words.

Significance

The worst-case residual under linear-fractional uncertainty cannot be computed efficiently unless P = NP. Theorem 5.2 gives an SDP-computable upper bound with an explicit certificate $(S, G)$ . Since $x$ enters (38) linearly, the same constraint can also be optimized over $x$ (Theorem 5.3, not part of this mission). For $\mathcal D = \mathbb R^{N\times N}$ the bound is exact, which covers the model $[A(\Delta)\ b(\Delta)] = [A\ b] + L\Delta[R_A\ R_b]$ and, as a special case, the unstructured problem of §3.

The results are proved in the paper (the proof of Theorem 5.2 is only indicated, through Appendix C). No machine-checked version of these statements, of Lemma 2.2 or of the structured S-procedure with commutant scalings is known. The formalization also fixes the statements. As printed, Lemma 2.2's "only if", Lemma 2.3 and the upper bound of Theorem 5.2 are each false in a boundary or structural case (see Formalization scope). The corrected forms stated here are the ones the paper's proofs support.

Difficulty

Part (a) reduces to robust positivity of a linear-fractional matrix function, and the difficulty is the inverse $(I - D\Delta)^{-1}$ . The certificate is one LMI in which $\Delta$ does not appear, while the conclusion is about a rational function of $\Delta$ over a whole structured ball. The certificate also has to guarantee that $I - D\Delta$ is invertible everywhere on that ball, and not only that the residual is small where it is defined. Evaluating $\mathcal F$ at a single point does not show this. Part (b) needs a lossless S-procedure in its strict form. The standard (non-strict) S-lemma gives only $\succeq$ , and the gap between strict and non-strict inequalities is exactly where the printed statements fail. The degenerate case $T_2 = 0$ is not covered by the S-lemma's regularity condition and has to be handled separately.

Formalization scope

Dimensions are Fin n, Fin m, Fin N; $\mathcal D$ is a Submodule ℝ (Matrix (Fin N) (Fin N) ℝ), with $\mathcal D = \mathbb R^{N\times N}$ as ⊤. The Euclidean norm is written out, because ‖·‖ on Fin n → ℝ is the sup norm. $\|\Delta\|$ is the operator norm of Matrix.toEuclideanLin Δ, the largest singular value.
$\lambda > r_{\mathcal D}(A,b,x)$ is the predicate ResidualBelow: every $\Delta \in \mathcal D$ with $\|\Delta\| \le 1$ has $\det(I - D\Delta) \ne 0$ and residual $< \lambda$ . It is false for every $\lambda$ when $r_{\mathcal D} = \infty$ . No real-valued supremum is used, so the $\infty$ branch of (35) cannot turn into a default $0$ . Matrix inverses are Mathlib's Matrix.inv, and every use carries the determinant condition.
$\rho = 1$ throughout, as in the paper; general $\rho$ follows by scaling $\Delta$ .
Corrections of the printed statements. (i) (40) must require $S \succ 0$ . Without it, $N = n = m = 1$ , $D = 2$ , $L = 1$ , $A = b = R_A = R_b = 0$ , $x = 0$ , $S = -1$ , $G = 0$ satisfy (38) for every $\lambda > 1/3$ , while $r_{\mathcal D} = \infty$ . (ii) $G$ must make $G\Delta$ skew-symmetric for every $\Delta \in \mathcal D$ , which is the identity $p^TGq = 0$ used in the proof of Lemma 2.3. For $\mathcal D = \operatorname{span}\{I, J\}$ , $J = \begin{bmatrix}0&1\\-1&0\end{bmatrix}$ , the printed bound certifies $\lambda = 3/2$ for an instance with worst-case residual $2$ . The added condition holds automatically when every element of $\mathcal D$ is symmetric (e.g. the diagonal structures (36)) and when $G = 0$ (e.g. $\mathcal D = \mathbb R^{N\times N}$ ). (iii) Lemma 2.2's "only if" is stated under $T_2 \ne 0$ or $T_3 = 0$ . (iv) Lemma 2.3's necessity is stated in strict form, and its sufficiency concludes $T(\Delta) \succ 0$ .
Not stated: "If $\Theta > 0$ at the optimum, the upper bound is also exact". The infimum over the strict LMI (38) is not attained, and the paper does not say which limit is meant. Theorem 5.3, Lemma 2.4 and Lemma 5.1 are also not stated.
Trivializing encodings ruled out: the goal is not a statement about the value of an infimum (which a junk value could satisfy), and the added hypotheses are satisfiable (for instance $S = sI$ , $G = 0$ for full $\mathcal D$ , which part (b) produces).
Infrastructure needed: the Schur complement for block matrices (in Mathlib), a lossless S-lemma for two homogeneous quadratic forms in strict and non-strict form (the platform has ConvexOptimization.s_procedure, in a different sign convention), square roots of positive definite matrices that commute with $\mathcal D$ , and compactness of the structured unit ball. The S-procedure lemmas are reusable in robust control and trust-region analysis. Proofs of the milestones in any order are welcome.

Selected references

L. El Ghaoui and H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
S. Boyd, L. El Ghaoui, E. Feron and V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
M. K. H. Fan, A. L. Tits and J. C. Doyle, Robustness in the presence of mixed parametric uncertainty and unmodeled dynamics, IEEE Trans. Automat. Control 36(1):25–38, 1991. https://doi.org/10.1109/9.62265
I. Pólik and T. Terlaky, A survey of the S-lemma, SIAM Review 49(3):371–418, 2007. https://doi.org/10.1137/S003614450444614X

8 thms2 active usersReviewed

Completed

Linear Optimization Number Theory Operations Research+1·Captain: mikedeng1

An Application of Simultaneous Diophantine Approximation in Combinatorial Optimization: A Small Integral Objective with the Same Optimal Solutions and Dual BasesResearch Paper

Motivation

An algorithm for linear programming is strongly polynomial if the number of arithmetic operations it performs is bounded by a polynomial in the dimension of the problem alone (the number of variables and constraints), independently of the bit lengths of the numbers in the input. Many combinatorial optimization problems are linear programs over polyhedra of the form $P = \{x \in \mathbb{R}^n : Ax \le b\}$ whose constraint matrix $A$ has entries $0, +1, -1$ , but whose objective vector $w$ is an arbitrary rational weight vector. Polynomial-time algorithms for such problems (for instance the ellipsoid-based algorithms of Grötschel, Lovász and Schrijver for maximum-weight cliques in perfect graphs, submodular flows, and matroid polyhedra) have running times that depend on the length of $w$ .

Frank and Tardos (Combinatorica 1987) remove this dependence once and for all: they replace $w$ by an integral objective $\tilde w$ whose entries have $O(n^3)$ bits and which has exactly the same optimal solutions and the same optimal dual bases as $w$ over every such polyhedron. Any algorithm that is polynomial in $n$ and in the length of the objective then becomes strongly polynomial. The tool is simultaneous Diophantine approximation, used through the lattice-basis-reduction algorithm of Lenstra, Lenstra and Lovász (Math. Ann. 1982). The technique extends Tardos's strongly polynomial algorithm for linear programs with small constraint matrices (Oper. Res. 1986), which applies only to explicitly given programs.

Setting

For $x \in \mathbb{R}^n$ write $\|x\|_\infty = \max_j |x(j)|$ and $\|x\|_1 = \sum_j |x(j)|$ ; $\operatorname{sign}$ takes the values $-1, 0, +1$ .

Decomposition. Fix a positive integer $N$ . A decomposition of $w \in \mathbb{R}^n$ is an expression

w = \sum_{i=1}^k \lambda_i v_i, \qquad \lambda_i > 0,\ v_i \in \mathbb{Z}^n.

It satisfies condition (iii) if for $i = 2, \dots, k$ the vector $v_i$ is nonzero and $\lambda_i/\lambda_{i-1} \le 1/(N\|v_i\|_\infty)$ : the coefficients decrease so quickly that each term is negligible against the previous one.

Preprocessing. Given a rational $w$ and $N$ , the paper's preprocessing algorithm finds a decomposition with $k \le n$ , condition (iii), and the size bound (ii)' $\|v_i\|_\infty \le 2^{n^2+n}N^n$ , and outputs

\tilde w = \sum_{i=1}^k M^{k-i} v_i, \qquad M = 2^{n^2+n} N^{n+1}.

Linear programs. Let $A$ be an $m \times n$ matrix with entries in $\{0, \pm 1\}$ and $b \in \mathbb{R}^m$ . The primal program is $\max\{wx : Ax \le b\}$ and the dual program is $\min\{yb : yA = w,\ y \ge 0\}$ . A point $\bar x \in P$ is $w$ -maximal if $w\bar x = \max(wx : x \in P)$ . A dual basis is a maximal set of row indices of $A$ whose rows are linearly independent; it determines at most one $y$ with $yA = w$ supported on it (the basic dual solution), and it is an optimal dual basis if that $y$ exists and is optimal for the dual program.

Formalization targets

Goal — Theorem 4.2 (p. 58)

For every $w \in \mathbb{Q}^n$ , with $N = (n+1)! + 1$ , there is $\tilde w \in \mathbb{Z}^n$ with

\|\tilde w\|_\infty \le 2^{4n^3} N^{n(n+2)}

such that for every $0, \pm1$ matrix $A$ with $n$ columns and every $b$ : (i) $x \in P$ is $w$ -maximal if and only if it is $\tilde w$ -maximal; (ii) a set of rows of $A$ is an optimal dual basis for $w$ if and only if it is one for $\tilde w$ . The vector $\tilde w$ depends on $w$ only, not on $A$ or $b$ .

Milestones

Dirichlet's theorem (p. 52): for $N \ge 1$ and $\alpha \in \mathbb{R}^n$ there are $p \in \mathbb{Z}^n$ and $1 \le q \le N^n$ with $|q\alpha(i) - p(i)| < 1/N$ for all $i$ .
Theorem 3.1 (p. 53): every $w \in \mathbb{R}^n$ has a decomposition with $k \le n$ , $\|v_i\|_\infty \le N^n$ and condition (iii).
Lemma 3.2 (pp. 54–55): under condition (iii), for integral $b$ with $\|b\|_1 \le N - 1$ , $\operatorname{sign}(b \cdot w) = \operatorname{sign}(b \cdot v_j)$ for the smallest $j$ with $b \cdot v_j \ne 0$ , and $b \cdot w = 0$ if there is no such $j$ .
Theorem 3.3 (p. 56): the preprocessed $\tilde w$ satisfies $\|\tilde w\|_\infty \le 2^{4n^3}N^{n(n+2)}$ and $\operatorname{sign}(w \cdot b) = \operatorname{sign}(\tilde w \cdot b)$ for all integral $b$ with $\|b\|_1 \le N-1$ .
The case $N = n+1$ (p. 55): an integral $\tilde w$ with $\|\tilde w\|_\infty \le 2^{4n^3}(n+1)^{n(n+2)}$ and $\tilde w(X) \le \tilde w(Y) \iff w(X) \le w(Y)$ for all subsets $X, Y$ of coordinates.
Lemma 4.1 (i) (p. 57): if $\operatorname{sign}(w' \cdot h) = \operatorname{sign}(w'' \cdot h)$ for all integral $h$ with $\|h\|_1 \le (n+1)!$ , then $w'$ and $w''$ have the same maximizers over $\{Ax \le b\}$ for every $0, \pm1$ matrix $A$ .
Lemma 4.1 (ii) (p. 57): under the same hypothesis, a dual basis is optimal for $w'$ if and only if it is optimal for $w''$ .

Significance

The result gives a general reduction: whenever a class of polyhedra with $0, \pm1$ constraint matrices admits an optimization algorithm that is polynomial in $n$ and in the length of the objective, it admits a strongly polynomial one. The paper applies this to maximum-weight cliques in perfect graphs, optimization over submodular flow polyhedra, and matroid polyhedra membership, and its Section 5 applies the same rounding to the integer programming algorithms of Lenstra and Kannan. The subset-sum corollary (milestone 5) is independently useful: every rational weight function on a finite set can be replaced by an integral one with $O(n^3)$ -bit entries that orders all subset sums identically.

All statements of this mission have been proved on paper since 1987. None is formalized on Prove2Me, and Mathlib contains only the one-dimensional Dirichlet approximation theorem. The mission produces a machine-checked version of the exact statements, with the explicit constants of the paper; the complexity claims (operation counts, strong polynomiality) are not part of it.

Difficulty

The goal combines two independent parts. The number-theoretic part (milestones 1–5) needs a multidimensional Dirichlet theorem, an induction producing the decomposition, and exact inequality chains with the constants $2^{n^2+n}N^n$ and $2^{4n^3}N^{n(n+2)}$ . The linear-programming part (milestones 6–7) needs bounds on the entries of inverses of nonsingular $0, \pm1$ submatrices, the existence of optimal dual solutions supported on a dual basis, LP duality and complementary slackness. The obvious first idea, scaling $w$ to an integer vector by a common denominator, preserves every sign but gives no bound on $\|\tilde w\|_\infty$ in terms of $n$ ; the bound is the content of the theorem. Likewise, rounding each coordinate of $w$ separately to a fixed precision does not preserve the sign of $w \cdot b$ when $w \cdot b$ is tiny but nonzero.

Formalization scope

Vectors are functions on Fin n: the input $w$ is rational (Fin n → ℚ) in the goal, in Theorem 3.3 and in the subset-sum corollary, as in the algorithm's input line; it is real in Theorem 3.1, Lemma 3.2 and Lemma 4.1, as on the page. Integral vectors are Fin n → ℤ, and $A$ is a Matrix (Fin m) (Fin n) ℤ with every entry in $\{-1, 0, 1\}$ , cast to $\mathbb{R}$ ; $b \in \mathbb{R}^m$ is unrestricted. Decompositions are indexed by $i \in \{1, \dots, k\} \subseteq \mathbb{N}$ as in the paper. $\|b\|_1$ is always the explicit sum $\sum_j |b(j)|$ , compared with $N - 1$ in $\mathbb{Z}$ ; $\|v\|_\infty$ of an integer vector is a natural number (supNorm). Sign equality uses SignType.sign and includes the zero case. Condition (iii) is stated multiplicatively together with $v_i \ne 0$ , which the paper's quotient presupposes; without $v_i \ne 0$ Lemma 3.2 fails. An optimal dual basis is a maximal linearly independent set of row indices together with an optimal dual solution supported on it.

Two formalizations would make the goal trivial and are excluded: dropping the bound on $\|\tilde w\|_\infty$ (a multiple of $w$ then works), and letting $\tilde w$ depend on $A$ and $b$ (the goal states $\exists \tilde w$ before $\forall A, b$ ). The $0, \pm1$ assumption on $A$ is part of every Section 4 statement.

A complete development needs a multidimensional pigeonhole argument, determinant and adjugate bounds for $0, \pm 1$ matrices, and basic LP duality (strong duality, complementary slackness, basic optimal dual solutions); the last two are reusable across linear-programming missions. Proofs of individual milestones, reusable lemmas on LP duality, and alternative proofs of Dirichlet's theorem are all welcome.

Selected references

A. Frank and É. Tardos, An application of simultaneous diophantine approximation in combinatorial optimization, Combinatorica 7(1) (1987) 49–65. https://doi.org/10.1007/BF02579200
A. K. Lenstra, H. W. Lenstra Jr. and L. Lovász, Factoring polynomials with rational coefficients, Math. Ann. 261 (1982) 515–534. https://doi.org/10.1007/BF01457454
É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Operations Research 34(2) (1986) 250–256. https://doi.org/10.1287/opre.34.2.250
M. Grötschel, L. Lovász and A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981) 169–197. https://doi.org/10.1007/BF02579273
J. W. S. Cassels, An Introduction to the Theory of Numbers (title as printed in the paper's reference [2]), Springer, Berlin, 1971; cited in the paper as [2, Sect. 1.10] for Dirichlet's theorem.

11 thms5 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Lifts of Convex Sets and Cone Factorizations I: A Proper K-Lift of a Convex Body Yields a K-Factorization of Its Slack Operator, and a K-Factorization Yields a K-LiftResearch Paper

Motivation

Many convex sets that appear in optimization have complicated descriptions in their own space but simple descriptions as projections of higher-dimensional sets. A polytope with exponentially many facets can be the shadow of a polyhedron with polynomially many; the unit disk is the projection of a slice of the cone of $2\times 2$ positive semidefinite matrices. Such a representation, a lift, turns linear optimization over the original set into a linear or semidefinite program over the lifted one, so the size of the smallest lift measures how hard the set is for conic optimization.

For polytopes and polyhedral lifts, Yannakakis (Yannakakis 1991) showed that the minimal size of a lift equals the nonnegative rank of the polytope's slack matrix. This turned questions about extended formulations into questions about matrix factorizations, and it is the basis of the lower bounds of Fiorini, Massar, Pokutta, Tiwary and de Wolf (2012) for the cut, stable set and traveling salesman polytopes. Lift-and-project hierarchies (Sherali–Adams, Lovász–Schrijver, Lasserre) all produce lifts to nonnegative orthants or positive semidefinite cones, so a criterion for the existence of a lift is also a criterion for when such a hierarchy can succeed.

Gouveia, Parrilo and Thomas (arXiv:1111.3164, Mathematics of Operations Research 38(2), 2013) extended Yannakakis' theorem from polytopes and polyhedral cones to arbitrary convex bodies and arbitrary closed convex cones. Their Theorem 2.4 is the target of this mission.

Timeline:

1991, Yannakakis: polytopes, polyhedral lifts, nonnegative factorizations of the slack matrix.
2012, Fiorini, Massar, Pokutta, Tiwary, de Wolf: superpolynomial lower bounds on polyhedral lifts via nonnegative rank; a positive semidefinite analogue for polytopes.
2011/2013, Gouveia, Parrilo, Thomas: convex bodies and general closed convex cones (Theorem 2.4), with psd rank as the semidefinite analogue of nonnegative rank.

Setting

Throughout, $\mathbb R^k$ carries the Euclidean inner product $\langle\cdot,\cdot\rangle$ .

A convex body is a set $C \subseteq \mathbb R^n$ that is convex, compact, and contains the origin in its interior. Its polar is

C^\circ = \{\, y \in \mathbb R^n : \langle x, y\rangle \le 1 \text{ for all } x \in C \,\}.

A point $p \in C$ is an extreme point if $p = (p_1+p_2)/2$ with $p_1,p_2\in C$ forces $p_1 = p_2 = p$ ; $\operatorname{ext}(C)$ is the set of extreme points. The slack operator of $C$ is

S_C : \operatorname{ext}(C)\times\operatorname{ext}(C^\circ) \to \mathbb R, \qquad S_C(x,y) = 1 - \langle x,y\rangle .

It is nonnegative, and for a polytope it is the slack matrix: rows indexed by vertices, columns by facet normals.

Let $K \subseteq \mathbb R^m$ be a full-dimensional closed convex cone: closed, convex, closed under nonnegative scaling, with nonempty interior. Its dual is $K^* = \{y : \langle x,y\rangle \ge 0 \ \forall x\in K\}$ .

A $K$ -lift of $C$ is $Q = K\cap L$ , where $L\subseteq\mathbb R^m$ is an affine subspace and $\pi:\mathbb R^m\to\mathbb R^n$ is a linear map with $C = \pi(K\cap L)$ . The lift is proper if $L$ meets the interior of $K$ (Definition 2.1).
$S_C$ is $K$ -factorizable if there are maps, not necessarily linear, $A:\operatorname{ext}(C)\to K$ and $B:\operatorname{ext}(C^\circ)\to K^*$ with $S_C(x,y) = \langle A(x), B(y)\rangle$ for all $(x,y)$ (Definition 2.2).

In Lean these are IsConvexBody, IsClosedConvexCone, HasLift, HasProperLift and SlackFactorizable in the namespace ConeLifts.Factorization, together with the series' shared ConeLifts.Shared.polar and ConeLifts.Shared.dualCone.

Formalization targets

Goal: Theorem 2.4

For $n \ge 1$ , a convex body $C\subseteq\mathbb R^n$ and a full-dimensional closed convex cone $K\subseteq\mathbb R^m$ :

\bigl(C \text{ has a proper } K\text{-lift} \Rightarrow S_C \text{ is } K\text{-factorizable}\bigr) \;\wedge\; \bigl(S_C \text{ is } K\text{-factorizable} \Rightarrow C \text{ has a } K\text{-lift}\bigr).

The two implications are not an equivalence: the forward one assumes properness, and the lift produced by the converse may be improper.

Milestones

In the order the paper's proof uses them:

(§2, p. 3) $C = \operatorname{conv}(\operatorname{ext} C)$ and $C^\circ = \operatorname{conv}(\operatorname{ext} C^\circ)$ .
(proof, p. 4) For every $c\in\operatorname{ext}(C^\circ)$ , $\max\{\langle c,x\rangle : x\in C\} = 1$ , attained.
(proof, p. 4) If $C = \pi(K\cap L)$ , $L = w_0 + L_0$ and $w_0\in\operatorname{int}K$ , then for $c \in \operatorname{ext}(C^\circ)$

1 = \min\{\langle w_0, z\rangle : z - \pi^*(c)\in K^*,\ z\in L_0^\perp\},

with the minimum attained. 4. (proof, p. 5) For $L = \{(x,z) : 1-\langle x,y\rangle = \langle z, B(y)\rangle\ \forall y\in\operatorname{ext}(C^\circ)\}$ and its projection $L_K$ to $\mathbb R^m$ : $0\notin L_K$ . 5. (proof, p. 5) If $B$ maps into $K^*$ , $z\in K$ and $(x,z)\in L$ , then $x\in C$ . 6. (proof, p. 5) For each $z\in K\cap L_K$ there is a unique $x_z$ with $(x_z,z)\in L$ .

Significance

The result. Theorem 2.4 makes the existence of a lift of a convex body to a given cone a purely algebraic question about its slack operator. Every lower bound on lift size in the paper and its successors goes through it: the nonnegative-rank bounds for polytopes (Section 4 of the paper), the proof that the stable set polytope of an $n$ -vertex graph has no lift to $\mathcal S^n_+$ (Section 5), and the later psd-rank literature. It also puts Yannakakis' theorem and its semidefinite analogue under a single statement.

Formalizing it. The theorem is proved on paper; no machine-checked version is known to exist. Formalizing it requires conic strong duality with dual attainment under a Slater condition, which Mathlib does not have, and finite-dimensional Krein–Milman for the polar body. The companion missions of this series (nonnegative-rank lower bounds; stable set polytopes and psd lifts) use the correspondence as their entry point.

Difficulty

The converse half is elementary once the extreme points of $C^\circ$ are known to generate it. The forward half is not: $B(c)$ must be an element of $K^*$ that certifies $\langle c, x\rangle \le 1$ on $C$ through the lift. A separating functional gives this certificate on $\pi(K\cap L)$ , but writing it as $z - \pi^*(c)$ with $z \perp L_0$ , $z - \pi^*(c)\in K^*$ and $\langle w_0,z\rangle = 1$ exactly is conic duality with a zero gap and an attained dual optimum. For closed convex cones the gap can be positive or the dual unattained unless a constraint qualification holds; this is why properness is assumed. Weak duality alone gives only $\ge 1$ , and a dual sequence approaching $1$ does not yield a factor. The paper notes (p. 5) that, since the proof uses strong duality, it is not obvious how to remove properness for a general closed convex cone.

Formalization scope

Conventions fixed by the Lean statements:

$\mathbb R^k$ is EuclideanSpace ℝ (Fin k); every pairing, in $S$ , in $K^*$ and in the factorization, is its inner product.
The polar is one-sided, $\langle x,y\rangle\le 1$ ; Mathlib's absolute polar is not used.
A convex body is compact, convex, with $0$ in its interior. The paper's "full-dimensional convex body in $\mathbb R^n$ " is read as including $n\ge 1$ : for $n = 0$ , $C = \{0\}$ has the proper $\mathbb R^m$ -lift $\{0\}$ while $S_C(0,0) = 1$ cannot factor through $K^* = \{0\}$ , so the forward half is false there. The goal and milestones 2–3 assume $1\le n$ .
$K$ is closed, convex, contains $0$ and is closed under nonnegative scaling; full-dimensionality is (interior K).Nonempty. Pointedness is not assumed.
$L$ is a Mathlib AffineSubspace and $\pi$ a linear map; the lift condition is the set equality $C = \pi(K\cap L)$ .
$A, B$ are total functions $\mathbb R^n\to\mathbb R^m$ constrained only on $\operatorname{ext}(C)$ , resp. $\operatorname{ext}(C^\circ)$ , which is equivalent to maps out of the extreme points. They are not required to be linear or continuous.
Milestone 3 is the second, substituted form of the paper's dual ( $z = M^{\mathsf T}y$ ), stated with L.directionᗮ and LinearMap.adjoint π; minima and maxima are stated with IsLeast/IsGreatest, so attainment is part of every claim.

Trivializing readings are excluded: $\pi$ is linear, not an arbitrary function (with an arbitrary function every set is a "lift"); $L$ is an affine subspace, not an arbitrary set; and $B$ takes values in $K^*$ , not $K$ , which for a cone that is not self-dual would be a different and generally false statement.

Needed infrastructure: finite-dimensional Krein–Milman in the form $C = \operatorname{conv}(\operatorname{ext} C)$ for compact convex sets (Mathlib has the closure form); the bipolar theorem $(C^\circ)^\circ = C$ for closed convex $C\ni 0$ with the one-sided polar; compactness of $C^\circ$ when $0\in\operatorname{int} C$ ; and conic linear programming duality with a Slater point, including dual attainment. The last two are reusable well beyond this mission. Proofs of individual milestones, and of these general facts as separate lemmas, are welcome.

Selected references

J. Gouveia, P. A. Parrilo, R. R. Thomas, Lifts of Convex Sets and Cone Factorizations, Mathematics of Operations Research 38(2):248–264, 2013. arXiv:1111.3164v2, doi:10.1287/moor.1120.0575
M. Yannakakis, Expressing combinatorial optimization problems by linear programs, Journal of Computer and System Sciences 43(3):441–466, 1991. doi:10.1016/0022-0000(91)90024-Y
S. Fiorini, S. Massar, S. Pokutta, H. R. Tiwary, R. de Wolf, Linear vs. semidefinite extended formulations: exponential separation and strong lower bounds, STOC 2012. arXiv:1111.0837

14 thms3 active usersReviewed

Completed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

Validation of Subgradient Optimization I: The Core Problem Built from the Subgradient Iterates Solves the Dual Linear ProgramResearch Paper

Motivation

Subgradient optimization maximizes a concave function that is not differentiable by stepping along an arbitrary subgradient with a prescribed sequence of step sizes. It became a standard tool of integer programming after Held and Karp used it to compute the Lagrangian 1-tree bound for the traveling-salesman problem (Held & Karp 1971). Held, Wolfe and Crowder then tested it on the assignment problem, a traveling-salesman relaxation and a multicommodity flow problem (Held, Wolfe & Crowder 1974).

The method has one practical defect that the paper names at the start of its Section 6: it contains no test of optimality. The value $w(\pi^j)$ approaches the maximum, but at no finite step does the method say that the maximum has been reached, or what the maximum is. Section 6 of the paper supplies such a test for the case where $w$ is a minimum of finitely many affine functions. The finitely many subgradients produced by the iterates define a small linear program, the core problem, and from some iteration on this linear program already solves the full dual linear program. Its optimal value is therefore the exact maximum of $w$ , obtained from quantities the method computes anyway. This is how the authors certified the optimal values reported in their experiments.

Timeline:

1967–1969: Poljak proves that the subgradient iterates satisfy $w(\pi^j)\to\max w$ when the step sizes tend to zero and have divergent sum (Poljak 1967; Poljak 1969).
1971: Held and Karp apply the method to the 1-tree bound (Held & Karp 1971).
1974: Held, Wolfe and Crowder prove that the core problem $P(J,J^*)$ solves the dual linear program (Theorem 6.3) and give a sufficient condition for bounded iterates (Theorem 6.1).
1996–1999: primal recovery from subgradient iterates is developed further, by convex combinations of the subgradients with weights derived from the step sizes (Sherali & Choi 1996; Larsson, Patriksson & Strömberg 1999).

Setting

Fix $n\ge0$ and write $E^n=\mathbb R^n$ with the Euclidean inner product $\pi\cdot v$ . The data are $K\ge1$ scalars $c_k$ and vectors $v_k\in E^n$ , and

w(\pi)=\min\{c_k+\pi\cdot v_k : k=1,\dots,K\}.\qquad(2.2)

The function $w$ is assumed bounded above, the paper's standing assumption. An index $k$ attains the minimum at $\pi$ if $c_k+\pi\cdot v_k=w(\pi)$ .

A run of the subgradient algorithm consists of a starting point $\pi^0\in E^n$ , step sizes $t_j>0$ and indices $k(j)$ such that $k(j)$ attains the minimum at $\pi^j$ , and

\pi^{j+1}=\pi^j+t_j\,v_{k(j)}\qquad(j=0,1,\dots).\qquad(2.6)

No rule for choosing among several minimizing indices is imposed. Write $v^j=v_{k(j)}$ and $c^j=c_{k(j)}$ . The step-size conditions are

t_j\to0,\qquad \sum_{j=0}^\infty t_j=\infty.\qquad(2.7)

The dual linear program of $\max w$ is

\min\Big\{\sum_k c_ky_k : y_k\ge0,\ \sum_ky_k=1,\ \sum_ky_kv_k=0\Big\}.\qquad(6.1)

For integers $J<J^*$ the core problem $P(J,J^*)$ has one variable $y_j$ for each iteration $j\in[J,J^*]$ :

\min\Big\{\sum_{j=J}^{J^*}c^jy_j : y_j\ge0,\ \sum_{j=J}^{J^*}y_j=1,\ \sum_{j=J}^{J^*}y_jv^j=0\Big\}.

An index chosen at several iterations contributes several identical columns. A point $y$ of $P(J,J^*)$ is sent to the point $\bar y_k=\sum\{y_j : J\le j\le J^*,\ k(j)=k\}$ of (6.1). This aggregation preserves feasibility and objective value.

Formalization targets

Goal: Theorem 6.3 (p. 82)

Assume $w$ is bounded above, $(t_j,\pi^j,k(j))$ is a run satisfying (2.7), and $\{\pi^j\}$ is bounded. Then

\forall J\ \exists J^*>J:\quad P(J,J^*)\text{ has a solution, and every solution of }P(J,J^*)\text{ aggregates to a solution of (6.1)}.

The goal states existence of $J^*$ , which is what the paper claims. The paper's argument in fact gives the conclusion for every sufficiently large $J^*$ . That stronger form is not the goal. Feasibility of $P(J,J^*)$ (Lemma 6.2) or the inequality $\mathrm{Value}[P(J,J^*)]\ge\mathrm{Value}[(6.1)]$ , which holds for every feasible $P(J,J^*)$ , is not a formalization of the goal. The content is optimality in (6.1).

Milestones

Eq. (2.10): if $\pi^*$ maximizes $w$ and $k$ attains the minimum at $\pi$ , then $w^*-w(\pi)\le v_k\cdot(\pi^*-\pi)$ .
§6, p. 80 (display): under (2.6), (2.7) and $w$ bounded above, $\lim_j w(\pi^j)=\max w=w(\pi^*)$ for some $\pi^*$ . The iterates are not assumed bounded.
Theorem 6.1: if every $\pi\ne0$ has some $\pi\cdot v_k<0$ , every run satisfying (2.7) is bounded.
Eq. (6.1): (6.1) has a solution, and its optimal value equals $\max w$ .
Lemma 6.2: for any $J$ there is $J^*>J$ with $P(J,J^*)$ feasible, for bounded runs.

Significance

Theorem 6.3 turns an asymptotic method into one that returns an exact answer. Solving $P(J,J^*)$ for growing $J^*$ produces a linear program of bounded size whose optimum is eventually the optimum of (6.1), and hence $\max w$ . In the Lagrangian applications, where (6.1) is the linear relaxation of a combinatorial problem, this yields both the bound and a primal solution of the relaxation. The theorem is the ancestor of the primal-recovery results listed in the timeline.

The mission produces a machine-checked version of the paper's Section 6, together with the input the paper takes on citation: Poljak's convergence theorem for divergent-series step sizes, specialized to piecewise-linear concave functions. Neither Poljak's theorem nor Theorem 6.3 is in Mathlib. The pieces are reusable: the convergence theorem applies to every Lagrangian dual solved by subgradient steps, and the duality between $\max w$ and (6.1) is linear-programming duality for a minimum of affine functions.

Difficulty

The inequality $\operatorname{Value}P(J,J^*)\ge\operatorname{Value}(6.1)$ is immediate, since aggregation maps feasible points to feasible points with the same objective. All of the content lies in the reverse inequality. That inequality ties a finite linear program to the limit of an infinite sequence, and it must hold for an arbitrary choice among tied minimizing indices. The iterates themselves need not converge, and under (2.7) the values $w(\pi^j)$ are not monotone. So an argument that inspects a single iterate, or assumes that the method settles on one face of $w$ , fails. The convergence statement of milestone 2 is not proved in the paper and is the heaviest single step. Feasibility of $P(J,J^*)$ also needs its own argument, and it fails without the boundedness hypothesis.

Formalization scope

$E^n$ is EuclideanSpace ℝ (Fin n), the index set is a finite nonempty type ι, and $w$ is the finite minimum Finset.univ.inf'. A run is the predicate IsSubgradientRun c v t π k: positive steps, a minimizing index at every step, and update (2.6). It is not a function of $\pi^0$ , so every tie-breaking rule is covered. (2.7) is StepSizeCond t: t → 0, and the partial sums tend to $+\infty$ . Iterates are indexed from $j=0$ . Boundedness is Bornology.IsBounded (Set.range π). The variables of $P(J,J^*)$ are a function on $\mathbb N$ of which only the values at $J\le j\le J^*$ enter. Optimality of $y$ in either linear program means feasibility plus an objective no larger than that of every feasible point. Suprema are never taken over unbounded sets: every maximum of $w$ is stated as attained at an explicit $\pi^*$ .

A statement that only asserts feasibility of $P(J,J^*)$ , or only $\operatorname{Value}P\ge\operatorname{Value}(6.1)$ , is not the theorem. The goal requires that the solutions of $P(J,J^*)$ be optimal for (6.1).

Theorem 6.1 is printed for the step rule (2.8), but its proof uses $w(\pi^j)\to w^*$ , the consequence of (2.7). The mission states it for (2.7), and its milestone title says so.

A complete development needs:

linear-programming duality for (6.1), including attainment;
the convergence theorem for divergent-series step sizes;
existence of a maximizer of a bounded-above minimum of finitely many affine functions;
basic facts on convex hulls of finitely many vectors in $E^n$ .

The first three are reusable well beyond this mission. Contributions of any of them, as standalone theorems, are welcome.

Selected references

M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974) 62–88. https://doi.org/10.1007/BF01580223
M. Held, R. M. Karp, The traveling-salesman problem and minimum spanning trees: Part II, Mathematical Programming 1 (1971) 6–25. https://doi.org/10.1007/BF01584070
B. T. Poljak, A general method of solving extremum problems, Soviet Mathematics Doklady 8 (1967) 593–597.
B. T. Poljak, Minimization of unsmooth functionals, USSR Computational Mathematics and Mathematical Physics 9 (1969) 14–29. https://doi.org/10.1016/0041-5553(69)90061-5
H. D. Sherali, G. Choi, Recovery of primal solutions when using subgradient optimization methods to solve Lagrangian duals of linear programs, Operations Research Letters 19 (1996) 105–113. https://doi.org/10.1016/0167-6377(96)00019-3
T. Larsson, M. Patriksson, A.-B. Strömberg, Ergodic, primal convergence in dual subgradient schemes for convex programming, Mathematical Programming 86 (1999) 283–312. https://doi.org/10.1007/s101070050090

7 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Integrating Replenishment Decisions with Advance Demand Information I: The Myopic Order-Up-To Level Is Optimal When Observed Demand Beyond the Protection Period Is LargeResearch Paper

Motivation

Many firms learn part of future demand before it has to be served: customers place orders days or weeks ahead of the date they need the goods, or commit to delivery dates in contracts. Advance demand information of this kind reduces the uncertainty the inventory manager has to protect against, and the question is how replenishment decisions should use it. Gallego and Özer (Management Science 47(10), 2001) model orders placed up to $N$ periods ahead and a supply lead time $L$ . They show that, with a fixed ordering cost, the classical $(s,S)$ structure survives with parameters that depend on the observed future demand, and they identify when that dependence disappears.

The classical theory this builds on is the finite-horizon inventory model with a set-up cost. Scarf (1960) introduced $K$ -convexity to prove that $(s,S)$ policies are optimal there. Veinott (1966) and Iglehart (1963) bounded the optimal policy parameters by myopic quantities. Gallego and Özer extend both results to a state that carries a vector of observed demands.

Setting

Periods are $t = 1, \dots, T$ . In period $t$ customers place orders $D_t = (D_{t,t}, \dots, D_{t,t+N})$ for periods $t, \dots, t+N$ ; $D_t$ is a random vector with law $\mu_t$ and nonnegative components. The lead time $L$ and the information horizon $N$ satisfy $N > L+1$ ; write $M = N - L - 1 \ge 1$ . The state at the start of period $t$ is a pair $(x_t, o_t)$ : the modified inventory position $x_t \in \mathbb{R}$ , and the vector

o_t = (o_{t,t+L+1}, \dots, o_{t,t+N-1}) \in \mathbb{R}^M

of demands already observed for the periods beyond the protection period $t, \dots, t+L$ .

The manager raises $x_t$ to an order-up-to level $y \ge x_t$ , paying a set-up cost $K_t > 0$ if $y > x_t$ . After $D_t$ is observed, the state moves to

x_{t+1} = y - \sum_{s=t}^{t+L+1} D_{t,s} - o_{t,t+L+1},\qquad o_{t+1,s} = o_{t,s} + D_{t,s}\ \ (s = t+L+2,\dots,t+N),

with $o_{t,t+N} = 0$ . With a convex single-period cost $G_t$ , discount factors $\alpha_t > 0$ and $\delta(z) = \mathbf 1\{z > 0\}$ , the optimal cost satisfies $J_{T+1} \equiv 0$ and

J_t(x, o) = \min_{y \ge x}\{K_t\delta(y - x) + V_t(y, o)\},\qquad V_t(y, o) = G_t(y) + \alpha_{t+1}\,\mathbb E\,J_{t+1}(x_{t+1}, o_{t+1}).

Let $H_t(x, o) = K_t + \min_{y\ge x}V_t(y,o) - V_t(x,o)$ . The order-up-to level $S_t(o)$ is the least minimizer of $V_t(\cdot, o)$ , and the reorder point is $s_t(o) = \max\{x : H_t(x,o) \le 0\}$ .

A function $g$ is $(a,b)$ -convex, $g \in C(a,b)$ , if $g(\theta x_1 + (1-\theta)x_2) \le \theta(a + g(x_1)) + (1-\theta)(b + g(x_2))$ for all $x_1 \le x_2$ and $\theta \in [0,1]$ ; $C(0,K)$ is Scarf's $K$ -convexity. In the stationary problem $G_t = G$ , $K_t = K$ , $\alpha_t = \alpha$ and $\mu_t = \nu$ , and the myopic levels are

S^m = \min\{y : G(y) \le G(x)\ \forall x\},\quad s^m = \max\{y \le S^m : G(y) \ge K + G(S^m)\},\quad \overline S = \inf\{y > S^m : G(y) > G(S^m) + \alpha K\}.

Formalization targets

Goal: Theorem 2 (p. 1350)

For the stationary problem, every $1 \le t \le T$ and every observed-demand vector $o_t \ge 0$ ,

o_{t,t+L+1} \ge \overline S - s^m \implies S_t(o_t) = S^m.

Only the observed demand for the first period beyond the protection period is compared with the threshold; the other components of $o_t$ are free.

Milestones

Lemma 1, Parts 1, 2, 4, 5 (p. 1349): inclusion, positive combinations, expectations, and $g(\max(x,s))$ for $(a,b)$ -convex functions.
Lemma 2 and Corollary 1 (p. 1350): for $V \in C(0,K)$ with a minimizer $S$ , $H$ changes sign once from $-$ to $+$ , and (for continuous $V$ ) $J(x) = V(\max(s,x))$ .
Theorem 1, Parts 1–3 (p. 1350): $V_t(\cdot, o_t) \in C(0, K_t)$ is coercive, a state-dependent $(s_t(o_t), S_t(o_t))$ policy is optimal, and $J_t(\cdot, o_t) \in C(0, K_t)$ with its limits at $\pm\infty$ .
Lemma 3 (p. 1351): $S^m \le S_t(o_t) \le \overline S$ and $s^m \le s_t(o_t)$ .

Significance

Theorem 1 says that advance demand information does not destroy the $(s,S)$ structure: the optimal policy is still a reorder point and an order-up-to level, now functions of $o_t$ . Theorem 2 is a horizon result. Once enough demand is already booked for period $t+L+1$ , the order-up-to level is the myopic one, computed from $G$ alone, and the rest of the information vector can be ignored. The threshold $\overline S - s^m$ grows with the set-up cost. In practice the manager then orders only to cover demand up to period $t+L$ , knowing another order will be placed in period $t+1$ , and the search for state-dependent policies is confined to states with little booked demand.

The results are proved in the paper, with some steps argued informally (the unit forward difference in Lemma 3, a minimum over an open set in the definition of $\overline S$ ). As far as the platform's catalog shows, no $(s,S)$ optimality theorem of this form has a machine-checked proof: the platform has $K$ -convexity lemmas for a single constant, not for $(a,b)$ -convexity or a dynamic program with a vector state. A formal proof would check the infinite-state induction and the conditions under which the expectation in (9) is finite. The $(a,b)$ -convexity layer and the one-period results (Lemma 2, Corollary 1) are reusable for any set-up cost model.

Difficulty

The obvious induction proves $K$ -convexity of $V_t$ and then applies Scarf's argument. The vector state makes each step conditional on facts the scalar case gets for free. The expectation in (9) mixes a random shift of $x$ with a random update of $o$ , so preserving $K$ -convexity needs Lemma 1, Part 4 rather than the scalar version. Coercivity and continuity of $V_t(\cdot, o)$ , and measurability and integrability of $D \mapsto J_{t+1}(x_{t+1}, o_{t+1})$ , must be carried through the induction jointly in $(x, o)$ . They cannot be assumed.

For Theorem 2, $V_t$ is not a function of $G$ alone, and a comparison of $S_t(o_t)$ with $S^m$ has to control $\mathbb E J_{t+1}$ . That requires the lower bound $s^m \le s_{t+1}(o_{t+1})$ at the next period, which holds only on the nonnegative state space.

Formalization scope

Everything is stated about the functional equation (8)–(9). The paper derives it in Appendix A from a control problem over history-dependent policies, citing Özer (2000); that reduction is out of scope. The demand vector is Fin (L + M + 2) → ℝ and $o$ is Fin M → ℝ, with component $j$ equal to $o_{t,t+L+1+j}$ . $J$ is defined by backward recursion, minima over $y \ge x$ are infima over $\{y : x \le y\}$ , and expectations are Bochner integrals. $G_t$ is an abstract primitive, not built from holding and penalty costs.

The paper's hypotheses are $G_t$ convex with $G_t(y) \to \infty$ as $|y| \to \infty$ (stated for $\widetilde G_t$ , used for $G_t$ ), $K_t > 0$ (Section 4), and $\alpha_{t+1}K_{t+1} \le K_t$ . The formalization adds hypotheses the paper uses without stating:

positive discount factors;
demands nonnegative almost surely;
every demand component has a finite mean, and $|G_t(y)| \le a_t + b_t|y|$ (so the expectation in (9) is finite);
continuity of $V$ in the abstract Corollary 1;
nonnegative observed demands $o_t$ in Lemma 3 and Theorem 2, where the lower bound fails for negative $o_{t,t+L+1}$ .

All hypotheses are placed on the primitives; nothing is assumed about the derived $V_t$ or $J_t$ . A Solutions/verification instance ( $G(y) = |y|$ , $K = 1$ , $\alpha = 1/2$ , zero demand) shows these hypotheses can be met together.

The definition of $\overline S$ is read as an infimum: the paper prints a minimum over an open set. $S_t(o_t)$ and $s_t(o_t)$ appear through IsLeast and IsGreatest, never as sInf/sSup values. A default value therefore cannot satisfy a conclusion, and vacuous readings (an empty minimizer set, an unbounded reorder set) are excluded. The infinite-horizon results (Lemma 4, Theorem 3, Corollary 2) and the zero set-up cost case are not part of this mission. Contributions are welcome at every level, and most of all a reusable library for $(a,b)$ -convex functions.

Selected references

G. Gallego, Ö. Özer, Integrating Replenishment Decisions with Advance Demand Information, Management Science 47(10):1344–1360, 2001. https://doi.org/10.1287/mnsc.47.10.1344.10261
H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
A. F. Veinott, On the Optimality of (s,S) Inventory Policies: New Conditions and a New Proof, SIAM Journal on Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259

15 thms4 active usersReviewed

Completed

Combinatorics Linear Optimization Operations Research+1·Captain: mikedeng1

Validation of Subgradient Optimization II: A Unique Optimal Assignment Makes the Dual Optimal Set Full-DimensionalResearch Paper

Why the assignment dual matters

The subgradient method maximizes a concave, piecewise-linear function $w(\pi)=\min_k\{c_k+\pi\cdot v_k\}$ by moving along a subgradient $v_k$ of an active piece with a prescribed step. Held, Wolfe and Crowder's 1974 paper Validation of subgradient optimization tested the method on three families of Lagrangean duals from combinatorial optimization — the assignment problem, a relaxation of the travelling salesman problem in the style of Held and Karp, and multicommodity flows — and gave the first systematic account of when the method works in practice.

On randomly generated assignment problems of order $n\le 30$ the authors observed that the method usually did not merely converge: it stopped, after finitely many steps, at an iterate whose subgradient was exactly zero. Their explanation is a structural fact about the assignment dual, Theorem 3.1 of the paper: when the optimal assignment is unique — the typical case for random integer costs — the set of optimal dual prices has full dimension $n$ , so a sequence of steps of decreasing length can land inside it. This mission formalizes that theorem and the steps of its proof.

Setting

There are $n$ men and $n$ jobs, and a real $n\times n$ cost matrix $A=(a_{ir})$ : $a_{ir}$ is the cost for which man $i$ does job $r$ . A one-to-one assignment is a permutation $\sigma$ of $\{1,\dots,n\}$ , where $\sigma(r)$ is the man doing job $r$ ; its cost is $\sum_r a_{\sigma(r)\,r}$ . The assignment problem (3.1) asks for a permutation of minimal cost; the assignment is unique if exactly one permutation attains that minimum.

The linear relaxation of (3.1), over doubly stochastic matrices $x=(x_{ir})$ , has the dual linear program (3.2), $\max\{\sum_i\pi_i+\sum_r\rho_r : \pi_i+\rho_r\le a_{ir}\}$ . For fixed prices $\pi\in\mathbb R^n$ on the men the best $\rho$ is $\rho_r=\min_s[a_{sr}-\pi_s]$ , which leaves the dual function (3.3)

w(\pi)=\sum_{i=1}^n\pi_i+\sum_{r=1}^n\min_s\,[a_{sr}-\pi_s],

the inner minimum being over the men $s$ for each job $r$ . The optimal set is $\Omega=\{\pi : w(\pi')\le w(\pi)\ \text{for all }\pi'\}$ .

To put $w$ in the form $\min_k\{c_k+\pi\cdot v_k\}$ the paper uses assignments in a weaker sense: arbitrary functions $A:\{1,\dots,n\}\to\{1,\dots,n\}$ , $n^n$ of them, with cost $c_A=\sum_r a_{A(r)\,r}$ and vector $(v_A)_i=1-\#\{r:A(r)=i\}$ (3.4). The subgradient step raises the price of a man assigned no job and lowers the price of a man assigned several; $v_A=0$ exactly when $A$ is a permutation.

In the Lean development these are assignCost, assignVec, IsOptimalAssignment, w and optSet in the namespace HeldWolfeCrowder.Assignment.

Formalization targets

Goal: Theorem 3.1 (p. 70)

If the assignment problem has a unique optimal permutation, then

\dim\operatorname{aff}\,\Omega=n .

The hypothesis is uniqueness among permutations; the conclusion is the dimension of the affine hull of the optimal set.

Milestones, in the order the proof uses them

Eq. (3.4): $w(\pi)=\min_A\{c_A+\sum_i\pi_i(v_A)_i\}$ over all $n^n$ assignments $A$ .
§3, Eqs. (3.1)–(3.3): $w$ attains its maximum, and $\max w$ equals the cost of an optimal permutation.
Eq. (3.5): if $\sigma$ is the unique optimal permutation, some maximizer $\bar\pi$ of $w$ has, for every job $r$ , the minimum $\min_s[a_{sr}-\bar\pi_s]$ attained only at $s=\sigma(r)$ .
Eq. (3.6): for an optimal permutation $\sigma$ , the set $\Pi=\{\pi : a_{ir}-\pi_i>a_{\sigma(r)\,r}-\pi_{\sigma(r)}\ \text{for all } r,\ i\ne\sigma(r)\}$ is convex and open, $v=0$ on it, and $\Pi\subseteq\Omega$ .

Significance

The theorem turns an empirical observation into a statement about the problem: finite termination of the subgradient method on assignment problems is a property of the dual, not luck. Since $w$ is unchanged by adding the same constant to every price, $\Omega$ always contains a line; Theorem 3.1 says that, under uniqueness, it is as large as it can be. The paper (p. 70) cites the argument of its Section 2 that, with a full-dimensional optimal set, termination of the method is "nearly certain".

The result is proved in the paper; none of it is known to be machine-checked. What the formalization adds is a checked link between three classical ingredients: the integrality of the assignment polytope (Birkhoff–von Neumann, which Mathlib has as doublyStochastic_eq_convexHull_permMatrix), linear-programming duality, and strict complementary slackness, which neither Mathlib nor the platform has in the form needed. The piecewise-linear representation (3.4) is reusable wherever the assignment dual appears as a Lagrangean subproblem.

Difficulty

The inclusion $\Pi\subseteq\Omega$ is elementary; the substance is that $\Pi$ is nonempty. The obvious candidate — any optimal dual solution — fails: an optimal $\pi$ may leave ties $a_{sr}-\pi_s=a_{\sigma(r)\,r}-\pi_{\sigma(r)}$ for some $s\ne\sigma(r)$ , so it sits on the boundary of $\Omega$ and shows nothing about dimension. What is needed is an optimal price vector with all these inequalities strict at once, and uniqueness of the optimal permutation is a statement about the primal side only; transferring it to the dual side goes through the linear relaxation (3.1), whose uniqueness is not the hypothesis, and through a strict complementarity property that is not available in Mathlib or on the platform.

Formalization scope

Men and jobs are both Fin n; the costs are a : Matrix (Fin n) (Fin n) ℝ with a i r the cost of man i on job r; prices are π : Fin n → ℝ (no inner product or norm is needed, so no EuclideanSpace). The inner minimum of (3.3) is Finset.univ.inf' over the men, well defined for every n. One-to-one assignments are Equiv.Perm (Fin n) with σ r the man doing job r, so the orientation of the matrix matches (3.3); arbitrary assignments are functions Fin n → Fin n. "Of dimension $n$ " is Module.finrank ℝ (vectorSpan ℝ (optSet a)) = n. The page prints the index condition of (3.6) as " $i\ne r$ "; the formalization uses $i\ne\sigma(r)$ , which is what the argument requires. The case $n=0$ is allowed and trivial.

A statement asserting only that $\Omega$ is nonempty, or that it has dimension at least one, is not this theorem: both hold for every cost matrix, the second because $\Omega$ is invariant under adding a constant to all prices. The goal requires the full value $n$ , and its hypothesis is uniqueness of the optimal permutation, not of the optimal linear-programming solution.

A complete development needs: the assignment linear program and its integrality (Mathlib's Birkhoff–von Neumann theorem), weak and strong duality between (3.1) and (3.2) or directly $\max w=\min_\sigma c_\sigma$ , and a strict complementarity statement for this primal–dual pair; the last two are reusable beyond this mission. Contributions of any of these, and of alternative arguments for (3.5) that avoid strict complementary slackness, are welcome.

Selected references

M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974) 62–88. https://doi.org/10.1007/BF01580223
M. Held, R. M. Karp, The traveling-salesman problem and minimum spanning trees: Part II, Mathematical Programming 1 (1971) 6–25. https://doi.org/10.1007/BF01584070
H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2 (1955) 83–97. https://doi.org/10.1002/nav.3800020109
A. J. Goldman, A. W. Tucker, Theory of linear programming, in H. W. Kuhn, A. W. Tucker (eds.), Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97.
Mathlib, Mathlib/Analysis/Convex/Birkhoff.lean (Birkhoff–von Neumann theorem, doublyStochastic_eq_convexHull_permMatrix). https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Analysis/Convex/Birkhoff.lean

6 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Integrating Replenishment Decisions with Advance Demand Information II: With Zero Set-up Cost the Myopic Base-Stock Policy Is Optimal When Myopic Levels Are NondecreasingResearch Paper

Motivation

Many firms learn about demand before it has to be served: customers place orders days or weeks ahead of the date they want delivery. Gallego and Özer (Management Science 47(10), 2001) model this advance demand information in a periodic-review inventory system and ask how the optimal replenishment policy should use it. Classical inventory theory (Arrow, Harris and Marschak 1951; Scarf 1959; Veinott 1965, 1966; Iglehart 1963) assumes that nothing about future demand is known when an order is placed. With advance orders the state of the system is no longer a single number, and it is not a priori clear whether the familiar policy structures survive.

This mission covers the paper's zero set-up cost case (Section 5). The companion mission Integrating Replenishment Decisions with Advance Demand Information I covers the positive set-up cost case and its $(s, S)$ policies.

Setting

Time is divided into periods $t = 1, \dots, T$ . The supply lead time is an integer $L \ge 0$ , and the information horizon is $N$ . In period $t$ customers place orders $D_t = (D_{t,t}, \dots, D_{t,t+N})$ , where $D_{t,s} \ge 0$ is demand placed in period $t$ for delivery in period $s$ . Throughout, $N > L + 1$ ; write $M = N - L - 1 \ge 1$ .

At the start of period $t$ the decision maker knows two things. The first is the modified inventory position $x_t$ : on-hand stock plus outstanding orders minus backorders, net of the demand already observed for the protection period $t, \dots, t+L$ . The second is the vector

o_t = (o_{t,t+L+1}, \dots, o_{t,t+N-1}) \in \mathbb{R}^M

of demands already observed for periods beyond the protection period. The decision maker raises the position to $y \ge x_t$ at zero fixed cost, the demand vector $D_t$ is realised, and the state moves to

x_{t+1} = y - \sum_{k=0}^{L+1} D_{t,t+k} - o_{t,t+L+1}, \qquad o_{t+1,s} = o_{t,s} + D_{t,s}\ (s = t+L+2, \dots, t+N),

with $o_{t,t+N} = 0$ .

Costs enter through a single-period cost $G_t : \mathbb{R} \to \mathbb{R}$ (holding, backorder and linear ordering cost, charged against the demand over the protection period) and one-period discount factors $\alpha_{t+1} > 0$ . The optimal cost-to-go $J_t$ and the cost $V_t$ of ordering up to $y$ satisfy

J_t(x, o) = \min_{y \ge x} V_t(y, o), \qquad V_t(y, o) = G_t(y) + \alpha_{t+1}\,\mathbb{E}\,J_{t+1}(x_{t+1}, o_{t+1}), \qquad J_{T+1} \equiv 0,

where the expectation is over $D_t$ . The base-stock level in period $t$ is the smallest minimizer

y_t(o) = \min\{y : V_t(y, o) = \min_x V_t(x, o)\},

and the myopic level is the smallest minimizer of the single-period cost,

y^m_t = \min\{y : G_t(y) = \min_x G_t(x)\}.

A function $f(x, \theta)$ has decreasing differences if $f(x_1, \theta) - f(x_2, \theta) \le f(x_1, \theta') - f(x_2, \theta')$ whenever $x_1 \ge x_2$ and $\theta \ge \theta'$ componentwise.

Formalization targets

Goal: Theorem 5 (p. 1352)

If $t \mapsto y^m_t$ is nondecreasing on $\{1, \dots, T\}$ , then for every period $t$ and every observed-demand vector $o \ge 0$ ,

y_t(o) = y^m_t .

The optimal order-up-to level then ignores all advance information beyond the protection period. A second item states the paper's stationary special case: if $G_t = G$ for all $t$ , the smallest minimizer $y^m$ of $G$ is the optimal base-stock level in every period.

Milestones: Theorem 4 (p. 1351)

For every period $t$ and every fixed $o_t$ :

$V_t(\cdot, o_t)$ is convex and $V_t(x, o_t) \to \infty$ as $|x| \to \infty$ ;
$y_t(o_t)$ exists and $J_t(x, o_t) = V_t(\max(y_t(o_t), x), o_t)$ : a state-dependent base-stock policy is optimal;
$J_t(\cdot, o_t)$ is nondecreasing and convex;
$V_t(x, o)$ has decreasing differences in $(x, o)$ ;
$J_t(x, o)$ has decreasing differences in $(x, o)$ ;
$y_t(o)$ is nondecreasing in $o$ .

Parts 1–3 are what the goal's proof uses. Parts 4–6 are the paper's second zero set-up result, monotonicity of the base-stock level in observed demand.

Significance

The theorem identifies when advance demand information beyond the protection period can be ignored. When the myopic levels do not decrease over time, which includes stationary costs and ramping-up demand, the $(1 + M)$ -dimensional dynamic program collapses to a sequence of one-dimensional newsvendor-type problems. That is both a computational simplification and a managerial statement: information about demand after the protection period does not change the order. Theorem 4, Part 5 gives the complementary monotone comparative statics. When the myopic condition fails, more observed demand never lowers the order-up-to level.

The results are proved in the paper, with the proofs in Appendix B. No machine-checked version exists. This mission produces a formal account of the finite-horizon recursion with a multi-dimensional information state, and checks the base-stock and myopic-optimality arguments against it.

Difficulty

The obvious induction carries convexity of $J_{t+1}$ backward, but here the future cost is evaluated at a random next state $(x_{t+1}, o_{t+1})$ whose first coordinate depends on the current observed demand $o_{t,t+L+1}$ . Showing that the base-stock level does not depend on $o_t$ therefore needs more than convexity. It needs to know where $J_{t+1}(\cdot, o_{t+1})$ is flat, uniformly in the random $o_{t+1}$ , and that the next position cannot exceed the current order-up-to level. The latter holds only on the reachable states, where observed demands are nonnegative. For a sufficiently negative $o_{t,t+L+1}$ the next period starts above its myopic level whatever is ordered now, and the conclusion fails. On the analytic side, every infimum and expectation in the recursion must be shown to be finite and attained before the order-theoretic argument can start.

Formalization scope

The model is parametrised by $L$ and $M \ge 1$ , with $N = L + M + 1$ . The demand vector is a function on $\{0, \dots, N\}$ and $o$ a function on $\{0, \dots, M-1\}$ , ordered componentwise. $J_t$ is defined by backward recursion with $J_t \equiv 0$ for $t > T$ . The minimum over $y \ge x$ is a real infimum and the expectation a Bochner integral against the law $\mu_t$ of $D_t$ . Attainment and finiteness are consequences proved in the theorems, not assumptions. Base-stock and myopic levels are characterised as smallest minimizers (IsLeast), never through sInf.

The single-period cost $G_t$ is a primitive rather than being assembled from $c_t$ , $g_t$ and the lead-time demand; the paper's $G_t$ has the assumed properties, so the theorems cover the paper's model. Hypotheses the paper uses without stating, all placed on primitives and labelled in the statements:

nonnegative demands, $D_{t,s} \ge 0$ almost surely;
coercivity of $G_t$ (the paper states it for $\tilde G_t$ only);
$\alpha_{t+1} > 0$ ;
finiteness of the expectation in (9), guaranteed by linear growth of $G_t$ and finite first moments of $D_t$ . This covers piecewise-linear holding and backorder costs with any finite-mean demand (including the paper's Poisson example), but excludes superlinear costs;
in the goal, $o \ge 0$ , the set of reachable states.

The goal cannot be trivialised: the hypotheses are satisfied by concrete instances (for example $G_t(y) = |y|$ with any finite-mean nonnegative demand), and the conclusion identifies the base-stock level exactly rather than asserting that some minimizer exists.

Out of scope: the reduction of the control problem to the functional equation (Appendix A, Özer 2000), the infinite-horizon Theorem 6, and Lemma 5, whose proof argues on the integers and whose real-valued form with a unit forward difference is unverified. Contributions of general lemmas are welcome: convexity and attainment for $\inf_{y \ge x}$ of a convex coercive function, and preservation of convexity and decreasing differences under expectation. All of them are reusable in other inventory models.

Selected references

G. Gallego, Ö. Özer, Integrating Replenishment Decisions with Advance Demand Information, Management Science 47(10):1344–1360, 2001. https://doi.org/10.1287/mnsc.47.10.1344.10261
A. F. Veinott, Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

9 thms2 active usersReviewed

Completed

Control Theory Convex Optimization Operations Research+1·Captain: mikedeng1

Robust Solutions to Uncertain Semidefinite Programs I: Exact SDP Reformulation of the Robust LMI under Full Linear-Fractional PerturbationsResearch Paper

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality (LMI) $F(x) = F_0 + \sum_{i=1}^m x_iF_i \succeq 0$ . SDPs model problems in control, combinatorial optimization, statistics and engineering design, and they are solved efficiently by interior-point methods. In applications the data $F_0,\dots,F_m$ are rarely known exactly: they come from measurements, from linearized models, or from rounding. A solution that is optimal for the nominal data may violate the constraint for data that differ only slightly.

El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) asked for robust solutions: points $x$ that satisfy the constraint for every admissible value of an unknown but bounded perturbation, and among them one that minimizes $c^Tx$ . Their paper, together with the contemporaneous work of Ben-Tal and Nemirovski on robust convex optimization (Math. Oper. Res. 23(4), 1998), founded robust semidefinite programming. The perturbation model they use, the linear-fractional representation (LFR), is the standard uncertainty model of robust control, where the same exact reformulation appears as the multiplier characterization of quadratic stability under norm-bounded uncertainty.

This mission formalizes the first main result of the paper: when the perturbation is full (an arbitrary matrix of bounded spectral norm), the robust problem is exactly an SDP with one extra scalar variable.

Setting

Fix natural numbers $m, n, p, q$ and a decision vector $x \in \mathbb{R}^m$ . The data are:

symmetric matrices $F_0,\dots,F_m \in \mathbb{R}^{n\times n}$ , defining the affine map $F(x) = F_0 + \sum_i x_iF_i$ ;
matrices $R_0,\dots,R_m \in \mathbb{R}^{q\times n}$ , defining $R(x) = R_0 + \sum_i x_iR_i$ ;
fixed matrices $L \in \mathbb{R}^{n\times p}$ and $D \in \mathbb{R}^{q\times p}$ ;
a level $\rho > 0$ .

For a matrix $X$ , $\|X\|$ denotes its largest singular value (the spectral norm), and $X \succeq 0$ means that $X$ is symmetric positive semidefinite. A perturbation is a matrix $\Delta \in \mathbb{R}^{p\times q}$ . The perturbed constraint matrix is the LFR (5)

\mathbf{F}(x,\Delta) = F(x) + L\Delta(I - D\Delta)^{-1}R(x) + R(x)^T(I - \Delta^TD^T)^{-1}\Delta^TL^T,

which is well defined exactly when $\det(I - D\Delta) \neq 0$ . For a linear subspace $\mathcal{D}$ of $\mathbb{R}^{p\times q}$ , the robust feasible set (2) is

\mathcal{X}_\rho = \bigl\{x \in \mathbb{R}^m : \text{for every } \Delta \in \mathcal{D} \text{ with } \|\Delta\| \le \rho,\ \mathbf{F}(x,\Delta) \text{ is well defined and } \mathbf{F}(x,\Delta) \succeq 0\bigr\},

and the robust SDP (4) is: minimize $c^Tx$ subject to $x \in \mathcal{X}_\rho$ , for a given $c \in \mathbb{R}^m \setminus \{0\}$ . In this mission $\mathcal{D} = \mathbb{R}^{p\times q}$ , the full perturbation case, and the paper's standing assumption of §3.1 is $\|D\| < \rho^{-1}$ .

Formalization targets

Goal: Theorem 3.1 (p. 36), as a set identity

Under $\rho > 0$ , $\|D\| < \rho^{-1}$ , $q \ge 1$ and $L \ne 0$ , for every $x \in \mathbb{R}^m$ ,

x \in \mathcal{X}_\rho \iff \exists\,\tau \in \mathbb{R}:\ \begin{bmatrix} F(x) - \tau LL^T & R(x)^T - \tau LD^T \\ R(x) - \tau DL^T & \tau(\rho^{-2}I - DD^T)\end{bmatrix} \succeq 0. \qquad (10)

The paper states that the robust SDP and a corresponding solution can be computed by solving the SDP "minimize $c^Tx$ subject to (10)" in the variables $(x, \tau)$ . Both problems have the objective $c^Tx$ , so the identity above, between $\mathcal{X}_\rho$ and the $x$ -projection of the feasible set of (10), is the content of that sentence. A companion item states the solution correspondence explicitly: $x$ is optimal for the robust SDP if and only if $(x,\tau)$ is optimal for (10) for some $\tau$ .

Milestones

Well-posedness (§3.1, p. 36). For $\rho > 0$ : $\det(I - D\Delta) \ne 0$ for every $\Delta$ with $\|\Delta\| \le \rho$ if and only if $\|D\| < \rho^{-1}$ .
Lemma 3.1 (p. 36). For $F = F^T$ , $q \ge 1$ and $L \ne 0$ : $\det(I - D\Delta) \ne 0$ and $F + L\Delta(I - D\Delta)^{-1}R + R^T(I - D\Delta)^{-T}\Delta^TL^T \succeq 0$ for every $\|\Delta\| \le 1$ if and only if $\|D\| < 1$ and some scalar $\tau$ satisfies

\begin{bmatrix} F - \tau LL^T & R^T - \tau LD^T \\ R - \tau DL^T & \tau(I - DD^T)\end{bmatrix} \succeq 0.

The paper cites the S-procedure as the classical result behind Lemma 3.1; it is already proved on the platform (ConvexOptimization.s_procedure) and is included as a reference item.

Significance

The robust feasible set is defined by infinitely many matrix inequalities, one per perturbation, each rational in $\Delta$ ; in general such a set is convex but has no tractable description, and the paper notes that the structured version of the problem is NP-hard. Theorem 3.1 shows that for full perturbations nothing is lost by replacing that semi-infinite constraint with a single LMI of size $n + q$ in one extra variable. Consequences: the robust problem is solved by a standard SDP solver; the largest admissible perturbation level is a generalized eigenvalue problem; and the exact result is the benchmark against which the paper's sufficient conditions for structured perturbations (Theorem 3.2) and its closed-form counterparts for unstructured perturbations (Theorem 5.1) are measured.

The result is proved in the paper (from the S-procedure, with the details deferred to a cited report). To the best of available knowledge it has no machine-checked proof. The mission produces a formal statement of the LFR model and of the robust feasible set that later missions on robust SDPs can reuse, a formal proof of the well-posedness condition, and a formal proof of the exact reformulation built on the platform's S-procedure. Formalizing it also records two points the printed statement leaves implicit: the result needs $L \ne 0$ and a nonempty perturbation output dimension $q \ge 1$ .

Difficulty

The direction from the LMI to robust feasibility is elementary. The converse is the substance: robust feasibility is a statement about a continuum of perturbations, each entering rationally, and testing the LMI against finitely many extreme perturbations does not produce a multiplier $\tau$ . The exactness of the reformulation rests on a lossless certificate for an implication between quadratic inequalities, which holds only under a strict feasibility condition; that condition is where $L \ne 0$ enters, and without it the lemma is false. The well-posedness milestone requires showing that $\|D\| < \rho^{-1}$ is also necessary, which is not a norm estimate but needs a perturbation that makes $I - D\Delta$ singular.

Formalization scope

Matrices are Mathlib Matrix (Fin a) (Fin b) ℝ. The affine maps are given by coefficient lists indexed by Fin (m + 1), the constant term first. The norm on matrices is the $\ell^2$ operator norm, opened with open scoped Matrix.Norms.L2Operator; it is the largest singular value, and no other matrix norm is used. $X \succeq 0$ is Matrix.PosSemidef, which includes symmetry. Block matrices are Matrix.fromBlocks over the index type Fin n ⊕ Fin q, with $R(x)^T - \tau LD^T$ top-right and $R(x) - \tau DL^T$ bottom-left. Mathlib's matrix inverse returns $0$ at a singular matrix, so the condition $\det(I - D\Delta) \ne 0$ appears in the robust feasible set in the same universally quantified clause as positive semidefiniteness, as the paper's "well defined" requires; dropping it, or using an entrywise matrix norm, would change the set and is excluded.

Readings and corrections of the printed statements:

"The RSDP (4) and a corresponding solution $x$ can be computed by solving the SDP" is read as the identity of $\mathcal{X}_\rho$ with the $x$ -projection of the feasible set of (10), for every $x$ , together with the solution correspondence item. A statement of equal optimal values alone would be weaker and is not used.
Correction: $L \ne 0$ is added to Lemma 3.1 and Theorem 3.1. The printed statements fail for $L = 0$ : with $n = p = q = 1$ , $F = 0$ , $L = 0$ , $D = 0$ , $R = 1$ , the perturbation does not enter, so the robust condition holds, while the LMI reads $\begin{bmatrix}0 & 1\\1 & \cdot\end{bmatrix} \succeq 0$ , which is infeasible.
$q \ge 1$ makes "matrices of appropriate size" explicit; for $q = 0$ the lower-right block is empty and the equivalence fails.
The standing assumptions $\rho > 0$ (§3) and $\|D\| < \rho^{-1}$ (§3.1) are hypotheses of the goal. In Lemma 3.1, $\|D\| < 1$ is part of the conclusion, as printed, and $\tau$ carries no sign constraint, as printed.
The paper's standing assumption that the nominal problem is feasible ( $\mathcal{X}_0 \ne \emptyset$ ) is not needed for the identity and is not added.

Welcome contributions: proofs of the well-posedness milestone (a spectral-norm and singular-vector argument, reusable wherever $I - D\Delta$ must be invertible); of Lemma 3.1 from the S-procedure (the reachability lemma for norm-bounded perturbations is reusable in robust control); of the goal from Lemma 3.1 by rescaling; and general lemmas on the spectral norm of rank-one matrices and on Schur complements of block matrices.

Selected references

L. El Ghaoui, F. Oustry and H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1), 33–52, 1998. https://doi.org/10.1137/S1052623496305717
A. Ben-Tal and A. Nemirovski, Robust Convex Optimization, Math. Oper. Res. 23(4), 769–805, 1998. https://doi.org/10.1287/moor.23.4.769
S. Boyd, L. El Ghaoui, E. Feron and V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004, Appendix B.2 (the S-procedure). https://web.stanford.edu/~boyd/cvxbook/

5 thms3 active usersReviewed

Completed

Control Theory Convex Optimization Operations Research+1·Captain: mikedeng1

Robust Solutions to Uncertain Semidefinite Programs II: An SDP Inner Approximation of the Robust Feasible Set under Structured PerturbationsResearch Paper

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality $F(x) = F_0 + \sum_{i=1}^m x_i F_i \succeq 0$ . In engineering applications the coefficient matrices are rarely known exactly: they come from measurements, from a model of a physical plant, or from a finite-precision implementation. El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) asked for solutions that remain feasible for every admissible value of the uncertain data, and showed how to compute such robust solutions by semidefinite programming. The paper appeared alongside Ben-Tal and Nemirovski's robust convex programming (Math. Oper. Res. 23(4), 1998) and is one of the two founding treatments of robust SDP.

When the uncertainty has structure (a block-diagonal perturbation, repeated scalar parameters, a symmetric matrix), the exact robust problem is NP-hard (El Ghaoui and Lebret, SIAM J. Matrix Anal. Appl. 18, 1997). This is the same obstacle that robust control meets in computing the structured singular value, and the remedy the paper uses, scaling matrices that commute with the perturbation structure, goes back to that literature (Doyle, IEE Proc. D 129, 1982; Fan, Tits and Doyle, IEEE Trans. Automat. Control 36, 1991). This mission formalizes the resulting tractable conservative approximation, Theorem 3.2 of the paper, together with the lemma it rests on and an application to integer feasibility problems.

Setting

Fix natural numbers $m, n, p, q$ . The decision variable is $x \in \mathbb{R}^m$ . The nominal data are affine maps

F(x) = F_0 + \sum_{i=1}^m x_i F_i \in \mathbb{R}^{n\times n}, \qquad R(x) = R_0 + \sum_{i=1}^m x_i R_i \in \mathbb{R}^{q\times n},

with every $F_i$ symmetric, and fixed matrices $L \in \mathbb{R}^{n\times p}$ , $D \in \mathbb{R}^{q\times p}$ . A perturbation is a matrix $\Delta \in \mathbb{R}^{p\times q}$ , and the perturbed constraint matrix is the linear-fractional representation (LFR)

\mathbf{F}(x,\Delta) = F(x) + L\Delta(I - D\Delta)^{-1}R(x) + R(x)^T(I - \Delta^TD^T)^{-1}\Delta^TL^T,

which is defined when $\det(I - D\Delta) \neq 0$ . The perturbation ranges over a linear subspace $\mathcal{D} \subseteq \mathbb{R}^{p\times q}$ , which encodes the structure, and is bounded by a level $\rho > 0$ in the spectral norm $\|\Delta\|$ (the largest singular value). The robust feasible set is

\mathcal{X}_\rho = \{x : \text{for every } \Delta \in \mathcal{D} \text{ with } \|\Delta\| \le \rho,\ \det(I - D\Delta) \neq 0 \text{ and } \mathbf{F}(x,\Delta) \succeq 0\},

and the robust SDP (RSDP) is to minimize $c^Tx$ over $\mathcal{X}_\rho$ .

The scaling set of $\mathcal{D}$ is the linear subspace

\mathcal{B} = \{(S,T,G) \in \mathbb{R}^{p\times p}\times\mathbb{R}^{q\times q}\times\mathbb{R}^{p\times q} : S\Delta = \Delta T,\ G\Delta^T = -\Delta G^T \text{ for every } \Delta \in \mathcal{D}\}.

Formalization targets

Goal: Theorem 3.2 (p. 37), as an inclusion of feasible sets

For every $x$ : if some $(S,T,G) \in \mathcal{B}$ has $S \succ 0$ , $T \succ 0$ and

\begin{bmatrix} F(x) - LSL^T & R(x)^T - LSD^T + LG \\ R(x) - DSL^T + G^TL^T & \rho^{-2}T - DSD^T + DG + G^TD^T\end{bmatrix} \succ 0,

then $x \in \mathcal{X}_\rho$ , and in fact $\mathbf{F}(x,\Delta) \succ 0$ for every $\Delta \in \mathcal{D}$ with $\|\Delta\| \le \rho$ . A companion item states the consequence for optimal values: the SDP value is an upper bound on the RSDP value, with both infima taken in the extended reals.

Milestones

Lemma 3.2 (p. 37): the same implication for constant $F$ , $R$ and $\rho = 1$ , with the matrix (13).
The full-perturbation case (p. 37): for $\mathcal{D} = \mathbb{R}^{p\times q}$ and $p, q \ge 1$ , $\mathcal{B}$ consists exactly of the triples $(\tau I_p, \tau I_q, 0)$ , with $\tau \ge 0$ when $S \succeq 0$ .
Theorem 5.6 (p. 48): if $F_i = 2L_iR_i$ with $r_i = \operatorname{rank} F_i$ , and $x_{\mathrm{feas}}$ satisfies, for some $\lambda \ge 0$ and block-diagonal $S = S^T$ , $G = -G^T$ ,

\begin{bmatrix} F(x_{\mathrm{feas}}) - \lambda I - LSL^T & \tfrac12R^T + LG \\ \tfrac12R - GL^T & S\end{bmatrix} \succ 0,

then every integer vector closest to $x_{\mathrm{feas}}$ in the maximum norm satisfies $F(z) \succeq 0$ .

Significance

The result. Theorem 3.2 replaces an NP-hard semi-infinite constraint, one matrix inequality for each admissible perturbation, by a single linear matrix inequality in the enlarged variable $(x, S, T, G)$ . Every point it certifies is robustly feasible, so its optimal value is a certified upper bound on the robust optimum and its optimizer is a usable robust solution. In the full case the scalings collapse to one multiplier $\tau$ (milestone 2), which connects the bound to the exact reformulation of Section 3.1 of the paper. Theorem 5.6 shows the same machinery at work on a combinatorial problem: robustness against perturbations of size $1/2$ in each coordinate of $x$ turns an SDP-feasible point into an integer solution by rounding.

Formalizing it. The results are proved in the paper (Lemma 3.2 with the proof deferred to [16]); none of them has a machine-checked proof that this mission is aware of, and the platform has no linear-fractional or structured-perturbation results. The formalization also settles the exact form of the certificate: as printed, the matrix (13) and the LMI of Theorem 3.2 contain products that are dimensionally undefined, and this mission states the condition the proof actually yields (see the scope section).

Difficulty

The inequality to be proved is a statement about infinitely many perturbations, and $\mathbf{F}(x,\Delta)$ depends on $\Delta$ through a matrix inverse. The natural first step, eliminating $\Delta$ by an exact S-procedure as in the full case, is not available: with a structured $\mathcal{D}$ the set of pairs of vectors linked by some $\Delta \in \mathcal{D}$ is not described by one quadratic inequality, and losslessness fails. The scalings in $\mathcal{B}$ give several valid quadratic inequalities instead, and one must show that their combination controls every $\Delta$ in the norm ball, including the well-posedness claim $\det(I - D\Delta) \neq 0$ , which is part of the conclusion rather than an assumption. The commutation condition $S\Delta = \Delta T$ must be turned into an inequality for $\|\Delta\| \le 1$ , which requires more than the definition of the spectral norm. For Theorem 5.6 the block-diagonal perturbation family and the rescaling between $\rho = 1/2$ and the stated matrix must be matched to the general lemma.

Formalization scope

Matrices are Matrix (Fin a) (Fin b) ℝ; $\succ 0$ and $\succeq 0$ are Matrix.PosDef and Matrix.PosSemidef (both include symmetry); block matrices are Matrix.fromBlocks on Fin n ⊕ Fin q. The norm of a perturbation is the $\ell^2$ operator norm (open scoped Matrix.Norms.L2Operator), i.e. the largest singular value; the maximum norm in Theorem 5.6 is Mathlib's sup norm on Fin m → ℝ. $\mathcal{D}$ is a Submodule. Affine maps are given by coefficient families indexed by Fin (m+1). Mathlib's matrix inverse is $0$ at a singular matrix, so every statement pairs the LFR with $\det(I - D\Delta) \neq 0$ . The standing assumption $\rho > 0$ of Section 3 is a hypothesis.

Readings and corrections of the printed statements:

(13) as printed is dimensionally inconsistent; we state the condition the proof yields, which coincides with the printed one when $G$ is square and skew-symmetric and $\mathcal{D}$ consists of symmetric matrices. Concretely, (11) prints $G \in \mathbb{R}^{q\times p}$ with $G\Delta = -\Delta^TG^T$ and (13) prints the blocks $R - DSL - GL^T$ and $T - GD^T + DG - DSD^T$ ; the mission uses $G \in \mathbb{R}^{p\times q}$ with $G\Delta^T = -\Delta G^T$ and the blocks $R - DSL^T + G^TL^T$ and $T - DSD^T + DG + G^TD^T$ . The same correction applies to the LMI of Theorem 3.2 (with $\rho^{-2}T$ ). Theorem 5.6 is stated as printed.
"An upper bound on the RSDP (4) and a corresponding solution $x$ can be computed by solving the SDP" is read as the inclusion of the SDP's feasible projection in $\mathcal{X}_\rho$ , for every $x$ ; the goal states it with the strict conclusion $\mathbf{F}(x,\Delta) \succ 0$ as well. The value form is a separate item.
In the full-perturbation remark, "for some $\tau \ge 0$ " is stated under $S \succeq 0$ , and "We then recover the exact results of section 3.1" is not formalized.
In Theorem 5.6, $\mathcal{S}$ 's index range " $i = 1,\dots,n$ " is read as $i = 1,\dots,m$ ; the hypothesis $r_i = \operatorname{rank}F_i$ is kept.

Trivializing formalizations are ruled out: $(0,0,0) \in \mathcal{B}$ always, so the hypotheses $S \succ 0$ and $T \succ 0$ are kept outside $\mathcal{B}$ ; $\mathcal{D}$ is a subspace, not an arbitrary set; and the norm is the spectral norm, not Mathlib's default entrywise norm.

A complete development needs the square root of a positive definite matrix and its commutation with $S$ and $T$ , the spectral-norm characterization $\Delta\Delta^T \preceq \|\Delta\|^2 I$ , Schur-complement and congruence facts for block matrices, and a linear-fractional identity relating $(I - D\Delta)^{-1}$ to an auxiliary vector. These are reusable well beyond this mission; contributions of any of them, and of the value and rounding corollaries, are welcome.

Selected references

L. El Ghaoui, F. Oustry, H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1):33–52, 1998. https://doi.org/10.1137/S1052623496305717
L. El Ghaoui, H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18:1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
M. K. H. Fan, A. L. Tits, J. C. Doyle, Robustness in the presence of mixed parametric uncertainty and unmodeled dynamics, IEEE Trans. Automat. Control 36:25–38, 1991. https://doi.org/10.1109/9.62265
J. C. Doyle, Analysis of feedback systems with structured uncertainties, IEE Proc. D 129(6):242–250, 1982. https://doi.org/10.1049/ip-d.1982.0053
A. Ben-Tal, A. Nemirovski, Robust convex optimization, Math. Oper. Res. 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777

5 thms2 active usersReviewed

Completed

Convex Optimization Linear algebra Operations Research+1·Captain: mikedeng1

Robust Solutions to Uncertain Semidefinite Programs III: Quadratic Growth and Uniqueness of the Robust SDP SolutionResearch Paper

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality $F(x) = F_0 + \sum_i x_i F_i \succeq 0$ . When the data $F_i$ are uncertain, El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) proposed to optimize against the worst case over a norm-bounded family of perturbations: the robust SDP. Their Theorem 3.1 shows that, for unstructured ("full") perturbations, the robust SDP is itself an SDP in the enlarged variable $(x,\tau)$ . Section 4 of the paper then asks what robustification does to the solution. Nominal SDPs are often ill-posed: the optimal set can be a whole face, and optimal points can jump under small data changes. Section 4 shows that, under explicit hypotheses, the robust problem has a unique solution with quadratic growth, which is the sense in which the paper describes robustness as a regularization of SDPs. This mission formalizes that result, Theorem 4.2.

Setting

Fix natural numbers $m, n, p, q$ , matrices $F_0, \dots, F_m \in \mathbb{R}^{n\times n}$ (symmetric), $R_0, \dots, R_m \in \mathbb{R}^{q\times n}$ , $L \in \mathbb{R}^{n\times p}$ , and an objective vector $c \in \mathbb{R}^m$ , $c \neq 0$ . Write $F(x) = F_0 + \sum_{i=1}^m x_iF_i$ and $R(x) = R_0 + \sum_{i=1}^m x_iR_i$ .

With full perturbations, uncertainty level $\rho = 1$ and $D = 0$ (the standing choices of §4), the robust SDP is the SDP

\text{minimize } c^Tx \quad\text{subject to}\quad \mathcal{F}(x,\tau) = \begin{bmatrix} F(x) - \tau LL^T & R(x)^T \\ R(x) & \tau I\end{bmatrix} \succeq 0 \tag{15}

in the variables $y = (x,\tau) \in \mathbb{R}^m \times \mathbb{R}$ . A point is feasible if $\mathcal{F}(x,\tau) \succeq 0$ (symmetric positive semidefinite) and optimal if it is feasible and minimizes $c^Tx$ over all feasible $(x',\tau')$ . The solution is the pair $(x,\tau)$ .

The paper's hypotheses (§4.1):

H1 (Slater): $\mathcal{F}(x,\tau) \succ 0$ for some $(x,\tau)$ .
H2 (inf-compactness): every sublevel set $\{(x,\tau)\ \text{feasible} : c^Tx \le M\}$ is bounded.
H3(a): the nullspace of the pencil $\lambda R_0 + \sum_i x_iR_i$ is one and the same proper subspace $N \subsetneq \mathbb{R}^n$ for every $(\lambda,x) \neq (0,0)$ .
H3(b): for every $x$ the stacked matrix $\begin{bmatrix} L^T \\ R(x)\end{bmatrix}$ has full column rank.

For $\tau > 0$ put $G(x,\tau) = F(x) - \tau LL^T - \frac{1}{\tau}R(x)^TR(x)$ , the Schur complement of the block $\tau I$ in $\mathcal{F}(x,\tau)$ .

The quadratic growth condition (QGC) holds at an optimal point $y^\star = (x^\star,\tau^\star)$ if there are $\alpha, \varepsilon > 0$ with

c^Tx \ \ge\ c^Tx^\star + \alpha\,\|y - y^\star\|^2 \qquad \text{for every feasible } y = (x,\tau),\ \|y - y^\star\| < \varepsilon .

Formalization targets

Goal: Theorem 4.2 (p. 39)

Under $c \neq 0$ , symmetry of the $F_i$ , H1, H2, H3(a) and H3(b):

\bigl(\forall\, y^\star \text{ optimal for (15)}:\ \text{QGC holds at } y^\star\bigr)\quad\text{and}\quad \exists!\, y = (x,\tau) \text{ optimal for (15)} .

Both halves are stated; uniqueness is of the pair $(x,\tau)$ , and existence is part of the claim.

Milestones, in the order the paper's proof uses them

§4.1 (p. 38): H3(a) implies $R(x) \neq 0$ for every $x$ .
§4.2 (p. 39): under H3(a), every feasible $\tau$ is positive; in particular $\tau_{\mathrm{opt}} > 0$ .
§4.2, Eq. (16): for $\tau > 0$ , $\mathcal{F}(x,\tau) \succeq 0 \iff G(x,\tau) \succeq 0$ .
Appendix A (p. 49): at every optimal $(x,\tau)$ there is a dual matrix $Z \succeq 0$ , $Z \neq 0$ , with $\operatorname{Tr} ZG(x,\tau) = 0$ , $\operatorname{Tr} Z\,\partial G/\partial x_i = c_i$ and $\tau^2\operatorname{Tr}LL^TZ = \operatorname{Tr}R(x)^TR(x)Z$ .
Appendix A (p. 49): H3(b) rules out $\operatorname{Tr}LL^TZ = \operatorname{Tr}R(x)^TR(x)Z = 0$ for $Z \succeq 0$ , $Z \neq 0$ , hence $\operatorname{Tr}R(x)^TR(x)Z > 0$ .
Appendix A (pp. 49–50): under H3(a), with $\tau > 0$ , $Z \succeq 0$ and $\operatorname{Tr}R(x)^TR(x)Z > 0$ , the Hessian of the Lagrangian $c^Tx - \operatorname{Tr} Z\,G(x,\tau)$ is positive definite.

Significance

The result. Theorem 4.2 turns the robust SDP into a well-posed problem: a unique solution with quadratic growth. Quadratic growth is the property from which the paper's Hölder-stability results (Theorem 4.3, Corollaries 4.1–4.2) follow through the perturbation theory of Bonnans, Cominetti and Shapiro, and it is what justifies using the robust SDP as a regularization of ill-conditioned SDPs (§5.4). The remark after the theorem notes a geometric reading: the growth holds for every objective, so the boundary of the robust feasible set contains no facets.

Formalizing it. The theorem has a published proof (Appendix A), which relies on a second-order sufficient condition for nonlinear SDPs cited from Bonnans, Cominetti and Shapiro. There is no machine-checked proof of it or of any second-order optimality result for SDPs that we know of. A formalization provides a complete account of the dual attainment, complementarity and second-order steps for this concrete problem class, and it checks the paper's computations; one of them, the intermediate display for the second derivative in Appendix A, has a factor error in its cross term that does not affect the conclusion.

Difficulty

The feasible set of (15) is a spectrahedron, and linear objectives over spectrahedra do not in general have unique minimizers, since optimal faces can be flat. Uniqueness therefore cannot come from convexity alone. It has to come from curvature of the boundary at the optimum, and that curvature is carried only by the nonlinear term $\frac{1}{\tau}R(x)^TR(x)$ of the Schur complement, which is degenerate along some directions. Positive definiteness of the Hessian must be recovered from the structural hypotheses H3(a) and H3(b), which interact with a dual matrix $Z$ that is known only to exist. The natural first attempt is to use $\tau > 0$ and the positive semidefiniteness of $Z$ directly. That attempt fails: the second derivative is $\operatorname{Tr} Z\,\mathcal{R}^T\mathcal{R}$ for a direction-dependent matrix $\mathcal{R}$ , which vanishes on the kernel of $Z$ , so it is not positive without H3(a) relating the kernels of all members of the pencil. Dual attainment and complementarity for (15) also have to be established, and the local second-order bound then has to be converted into a statement about every nearby feasible point.

Formalization scope

Representation. Data are bundled in RobustSDP.Uniqueness.SDPData m n p q; decision points are pairs y : (Fin m → ℝ) × ℝ; the coefficient Fs i, i : Fin m, is the paper's $F_{i+1}$ . $\succeq 0$ and $\succ 0$ are Mathlib's Matrix.PosSemidef and Matrix.PosDef, which include symmetry, as the paper's notation does.
Conventions fixed. §4's standing choices $D = 0$ and $\rho = 1$ are built into (15). The standing assumptions $c \neq 0$ and symmetric $F_i$ (p. 33) are explicit hypotheses. H2 is read as bounded sublevel sets of the feasible set in $(x,\tau)$ ; the paper's wording ("any unbounded sequence of feasible points produces an unbounded sequence of objectives") is meant in this sense, as its claim that H1 and H2 give existence of optimal points shows. H3(b)'s full column rank is injectivity of $\xi \mapsto (L^T\xi, R(x)\xi)$ . The QGC uses the Euclidean norm on $\mathbb{R}^{m+1}$ in its local form, which is equivalent to the paper's $o(\|y - y_{\mathrm{opt}}\|^2)$ form. It is stated for (15) rather than for the paper's reformulation (16), with which (15) coincides near the optimum because $\tau_{\mathrm{opt}} > 0$ . The auxiliary constraint $\tau \ge 0.99\,\tau_{\mathrm{opt}}$ of (16) is not formalized. $G$ uses Lean's τ⁻¹, which is $0$ at $\tau = 0$ , so every statement about $G$ assumes $\tau > 0$ or $\tau \ne 0$ .
No trivializing reading. The goal cannot be satisfied by stating only uniqueness of $x$ , by reading H2 as "the objective is bounded below", or by reading H3(a) as " $R(x) \neq 0$ ". The statement quantifies over the pair $(x,\tau)$ , and both the quadratic growth and the existence and uniqueness halves are required. The hypotheses are jointly satisfiable: for example $m = 1$ , $n = p = 2$ , $q = 4$ , $F(x) = \mathrm{diag}(3+x, 3-x)$ , $L = I_2$ , $R(x) = [1; x]\otimes I_2$ and $c = 1$ .
Infrastructure. A complete development needs Schur complements for positive semidefinite block matrices (available in Mathlib), strong duality with dual attainment for inequality-form SDPs under Slater's condition (ConvexOptimization.sdp_strong_duality on the platform, in another Mathlib environment), existence of minimizers on closed bounded sets, second derivatives of matrix-valued maps, and a local second-order argument for convex problems. The duality and second-order parts can be reused beyond this mission. Contributions to any milestone, or alternative proofs that avoid the general Bonnans–Cominetti–Shapiro theory, are welcome.

Selected references

L. El Ghaoui, F. Oustry and H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1), 33–52, 1998. https://doi.org/10.1137/S1052623496305717
J. F. Bonnans, R. Cominetti and A. Shapiro, Sensitivity analysis of optimization problems under second order regular constraints, Math. Oper. Res. 23(4), 806–831, 1998 (the paper's reference [10]). https://doi.org/10.1287/moor.23.4.806
A. Shapiro, First and second order analysis of nonlinear semidefinite programs, Math. Programming Ser. B 77, 301–320, 1997. https://doi.org/10.1007/BF02614439
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

10 thms4 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Robust Solutions to Uncertain Semidefinite Programs IV: Closed-Form Robust Counterparts under Unstructured PerturbationsResearch Paper

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality (LMI) $F(x) = F_0 + \sum_{i=1}^m x_i F_i \succeq 0$ . In applications the coefficient matrices $F_i$ are measured, estimated or rounded. A solution that is feasible for the nominal data can become infeasible for data that differ from it by an arbitrarily small amount.

El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) introduced robust semidefinite programs (RSDPs): the constraint must hold for every admissible perturbation of the data, and the robust solution is the best point that survives all of them. Their §5 works out the examples in which the robust counterpart has a closed form. The simplest and most widely quoted is the case where every coefficient matrix is perturbed independently and without structure (§5.1): the robust LMI becomes the single convex constraint $F(x) \succeq 2\rho\sqrt{\|x\|^2+1}\,I$ . The same computation gives closed-form robust versions of linear programs (§5.3), of largest-eigenvalue minimization (§5.4) and of matrix-norm minimization (§5.6), each of which is the nominal problem plus a Tikhonov-type term $\rho\sqrt{\|x\|^2+1}$ . Robust linear programming under ellipsoidal uncertainty was developed at the same time by Ben-Tal and Nemirovski (Math. Oper. Res., 1998); robust least squares, the prototype of §5.6, by El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl., 1997).

Setting

Fix $m, n \in \mathbb{N}$ , a level $\rho > 0$ , and symmetric matrices $F_0, \dots, F_m \in \mathbb{R}^{n\times n}$ . For $x \in \mathbb{R}^m$ write $F(x) = F_0 + \sum_{i=1}^m x_i F_i$ and $\|x\|^2 = \sum_{i=1}^m x_i^2$ (the Euclidean norm). For a matrix $M$ , $\|M\|$ is its spectral norm, the largest singular value, and $X \succeq 0$ means that $X$ is symmetric positive semidefinite.

An unstructured perturbation is a block row $\Delta = [\Delta_0 \ \cdots \ \Delta_m]$ of $n\times n$ blocks, viewed as one $n \times n(m+1)$ matrix. It perturbs each coefficient independently:

\mathbf{F}(x,\Delta) = F(x) + \Delta_0 + \Delta_0^T + \sum_{i=1}^m x_i(\Delta_i + \Delta_i^T).

The robust feasible set is

\mathcal{X}_\rho = \{x \in \mathbb{R}^m : \mathbf{F}(x,\Delta) \succeq 0 \text{ for every } \Delta \text{ with } \|\Delta\| \le \rho\},

and the RSDP is: minimize $c^Tx$ over $\mathcal{X}_\rho$ . With $R(x) = [1;\,x]\otimes I$ , the $n(m+1)\times n$ matrix whose $i$ -th block is $\tilde x_i I$ for $\tilde x = (1, x_1, \dots, x_m)$ , the perturbation reads $\mathbf{F}(x,\Delta) = F(x) + \Delta R(x) + R(x)^T\Delta^T$ (the paper's (19)).

Three further models use the same pattern. In a robust LP, the data $[a_i^T\ b_i]^T$ of each constraint $a_i^Tx \ge b_i$ are shifted by an independent $\delta_i \in \mathbb{R}^{m+1}$ with $\|\delta_i\|_2 \le \rho$ . In robust eigenvalue minimization one minimizes the worst case over $\|\Delta\|\le\rho$ of $\lambda_{\max}(\mathbf{F}(x,\Delta))$ . In robust maximum-norm minimization, $H(x) = H_0 + \sum_i x_i H_i$ with $H_i \in \mathbb{R}^{p\times q}$ , $\mathbf{H}(x,\Delta) = H_0 + \Delta_0 + \sum_i x_i(H_i + \Delta_i)$ , and one minimizes $\max_{\|\Delta\|\le\rho}\|\mathbf{H}(x,\Delta)\|$ .

Formalization targets

Goal: Theorem 5.1 (first sentence)

For every $x \in \mathbb{R}^m$ ,

x \in \mathcal{X}_\rho \iff F(x) \succeq 2\rho\sqrt{\|x\|^2+1}\; I .

The RSDP and problem (21), "minimize $c^Tx$ subject to $F(x) \succeq 2\rho\sqrt{\|x\|^2+1}\,I$ ", therefore have the same feasible set, optimal value and solutions. The goal fixes no numerical data: $F_0, \dots, F_m$ , $m$ , $n$ and $\rho > 0$ are arbitrary.

Milestones on the way (§5.1)

(19)–(20): $x \in \mathcal{X}_\rho$ iff there is $\tau \in \mathbb{R}$ with $\begin{bmatrix} F(x) - \tau I & \rho R(x)^T \\ \rho R(x) & \tau I\end{bmatrix} \succeq 0$ .
Positivity of $\tau$ and the Schur form (for $n \ge 1$ ): that block matrix is $\succeq 0$ iff $\tau > 0$ and $F(x) \succeq \bigl(\tau + \rho^2(1+\|x\|^2)/\tau\bigr) I$ .
(21): some $\tau > 0$ satisfies the Schur form iff $F(x) \succeq 2\rho\sqrt{\|x\|^2+1}\, I$ .

Further milestones: the value halves of Theorems 5.2–5.4

Theorem 5.2: the robust LP constraints hold iff $a_i^Tx - \rho\sqrt{\|x\|_2^2+1} \ge b_i$ for all $i$ (problem (23)).
Theorem 5.3: for every $t$ , $tI \succeq \mathbf{F}(x,\Delta)$ for all $\|\Delta\| \le \rho$ iff $\bigl(t - 2\rho\sqrt{\|x\|^2+1}\bigr) I \succeq F(x)$ ; that is, the worst-case largest eigenvalue is $\lambda_{\max}(F(x)) + 2\rho\sqrt{\|x\|^2+1}$ (problem (25)).
Theorem 5.4: for $p, q \ge 1$ , $\max_{\|\Delta\|\le\rho}\|\mathbf{H}(x,\Delta)\| = \|H(x)\| + \rho\sqrt{\|x\|^2+1}$ , and the maximum is attained (problem (29)).

Significance

The goal shows that robustness against unstructured perturbations costs no more than the nominal problem: the robust counterpart is an LMI of the same size $n\times n$ , with a right-hand side that is a convex function of $x$ and grows like $2\rho\|x\|$ . The sets $\mathcal{X}_\rho$ have no flat faces, which the paper's §5.2 uses to define the robust center of an LMI and which underlies the uniqueness and continuity of the robust solution (the second sentences of Theorems 5.1–5.4, from §4 under hypotheses H1–H3). Theorems 5.3 and 5.4 exhibit robustification as a Tikhonov regularization with parameter $2\rho$ or $\rho$ , and Theorem 5.2 turns a robust LP into a second-order cone program.

All four closed forms are proved in the paper, partly by appeal to the general SDP reformulation of its §3. No machine-checked version of any of them exists, to our knowledge. The mission produces the robust counterparts as identities of feasible sets, stated for every $x$ , together with the three intermediate steps of §5.1, so that later missions on the uniqueness and stability halves can import them.

Difficulty

The goal is an exchange of a universal quantifier over an infinite family of matrices with a single matrix inequality. The inequality $\mathbf{F}(x,\Delta) \succeq F(x) - 2\rho\sqrt{\|x\|^2+1}\,I$ bounds each perturbation, but the converse needs, for each failing direction, one admissible perturbation that attains the bound; the constant $2$ comes from the two copies $\Delta R(x)$ and $R(x)^T\Delta^T$ , and the constant $\sqrt{\|x\|^2+1}$ is the spectral norm of $R(x)$ , which holds only because $\Delta$ is normed as one block row. Normed block by block, the worst case and the constant change. In the milestone route, the positivity of $\tau$ needs a separate argument before any Schur complement can be taken, since the Schur complement with respect to $\tau I$ is undefined at $\tau = 0$ , and the elimination of $\tau$ needs the attainment of $\min_{\tau>0} \tau + a/\tau$ . For Theorem 5.4 the difficulty is the attainment: an upper bound on the maximum is immediate, while the lower bound requires exhibiting an admissible perturbation that attains it.

Formalization scope

Matrices are Matrix (Fin r) (Fin c) ℝ. Coefficients are indexed by Fin (m + 1) with index 0 the constant term. A block row $\Delta$ is one matrix with columns indexed by pairs (i, b) : Fin (m + 1) × Fin n (or Fin q), and $\|\Delta\|$ is Mathlib's $\ell^2$ operator norm (open scoped Matrix.Norms.L2Operator), the largest singular value, never the default entrywise norm. The vector norm $\|x\|^2$ is written as $\sum_i x_i^2$ , never as Mathlib's sup norm on Fin m → ℝ. $A \succeq B$ is (A - B).PosSemidef. Standing assumptions made explicit: $F_0, \dots, F_m$ symmetric; $\rho > 0$ (§3, p. 36); $n \ge 1$ in milestone 2 (at $n = 0$ every $\tau$ is feasible); $p, q \ge 1$ in Theorem 5.4 (empty matrices have norm $0$ ).

Readings and corrections of the printed text:

"The optimal value of the RSDP can be computed by solving (21)" is stated as the identity of the two feasible sets for every $x$ , which implies equality of values and of solutions. Theorems 5.2 and 5.4 are stated the same way (5.4 through the pointwise worst-case value, with attainment), and Theorem 5.3 in epigraph form, $\lambda_{\max}(M) \le t \iff tI - M \succeq 0$ .
Only the first sentence of each theorem is in scope. Uniqueness, regularity, Lipschitz stability and the limit $\rho \to 0$ rest on Theorem 4.3 and on external results ([31], [3]) and are not stated.
In (19) the paper writes $\mathcal D = \mathbb R^{n\times nm}$ and "the representation in section 5"; $\Delta$ has $m+1$ blocks, so $\mathcal D = \mathbb R^{n\times n(m+1)}$ , and the representation is that of §2.2.
The paper derives (20) from Lemma 3.2 and (29) from Theorem 3.2, which give only sufficient conditions; the exact equivalences are the full-perturbation Lemma 3.1 / Theorem 3.1.
Before (21) the paper says "the scalar in the left-hand side" (it is on the right) and "the RSDP (1)" (it means the RSDP (4)). Theorem 5.3's "min-max problem (24)" is the robust version of the nominal problem (24).

A formalization in which $\|\Delta\|$ is an entrywise or blockwise norm, $\|x\|$ is the sup norm, or the robust set quantifies over a single block, changes the constant $2\rho\sqrt{\|x\|^2+1}$ and is not this theorem; the statements here rule these out by construction.

Useful, reusable infrastructure: the spectral norm of $[1;\,x] \otimes I$ , Schur complements for positive semidefinite block matrices, and spectral norms of rank-one matrices. Proofs of the three §5.1 milestones and direct proofs of the goal are both welcome.

Selected references

L. El Ghaoui, F. Oustry, H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1):33–52, 1998. https://doi.org/10.1137/S1052623496305717
L. El Ghaoui, H. Lebret, Robust Solutions to Least-Squares Problems with Uncertain Data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
A. Ben-Tal, A. Nemirovski, Robust Convex Optimization, Math. Oper. Res. 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769

8 thms3 active usersReviewed

Discrete Geometry Number Theory Operations Research·Captain: mikedeng1

Minkowski's Convex Body Theorem and Integer Programming: Lattice-Free Convex Bodies Meet Few Translates of an Integral SubspaceResearch Paper

Motivation

Integer programming asks whether a system of linear inequalities $Ax\le b$ has a solution $x\in\mathbb Z^n$ . In fixed dimension $n$ it is solvable in polynomial time: Lenstra (1983) proved this by showing that a convex body without integer points is "flat" in some integral direction, so that the search splits into few lower-dimensional subproblems. Kannan's 1987 paper in Mathematics of Operations Research sharpened this approach. It computes a Korkine–Zolotarev ("reduced") basis of a lattice, solves the shortest and closest vector problems exactly in $n^{O(n)}$ operations, and runs integer programming in $O(n^{9n/2}s)$ arithmetic operations. Underneath the algorithm sits a purely geometric statement, Theorem (5.5): a lattice-free convex body meets only boundedly many integer translates of some integral subspace.

Timeline.

Korkine and Zolotareff (1873): the reduced bases used here.
Minkowski (1896): a symmetric convex body of volume greater than $2^n$ contains a nonzero integer point.
Khinchine (1948): lattice-free convex bodies have lattice width bounded by a function of $n$ alone (the flatness theorem).
Lenstra (1983): integer programming in fixed dimension is polynomial, via a flat direction.
Kannan (1987, this paper): Theorem (5.5), with subspaces $V$ of any dimension between $1$ and $n-1$ and an explicit bound $n^{2(n-\dim V)}$ .
Kannan and Lovász (1988), Banaszczyk et al. (1999), and later work: polynomial bounds on the flatness constant.

Setting

$\mathcal R^n$ is Euclidean space with dot product $(a,b)$ and length $|a|$ , and $\mathbb Z^n$ is the set of integer vectors. For linearly independent $b_1,\dots,b_m\in\mathcal R^k$ , the lattice $L(b_1,\dots,b_m)$ is the set of integer combinations $\sum_j\lambda_jb_j$ , $\lambda_j\in\mathbb Z$ , and $b_1,\dots,b_m$ is a basis. Gram–Schmidt orthogonalisation gives $b_1^*,\dots,b_m^*$ and unit vectors $u_j=b_j^*/|b_j^*|$ , and $b_i(j)=(b_i,u_j)$ , so $b_i=\sum_jb_i(j)u_j$ and $b_j(j)=|b_j^*|$ . The determinant is $d(L)=\prod_j|b_j^*|$ . $\Lambda_1(L)$ is the length of a shortest nonzero vector of $L$ . The projected lattice $L_j(b_1,\dots,b_m)$ is the image of $L$ under orthogonal projection onto the complement of $\operatorname{span}(b_1,\dots,b_{j-1})$ . A basis is reduced (Definition 2.6) if $b_j(j)=\Lambda_1(L_j)$ for every $j$ and $|b_i(j)|\le b_j(j)/2$ for $i>j$ .

A convex body is a convex set of positive volume, which for a convex set means nonempty interior. A subspace $V$ has a basis of integer vectors if it is the real span of integer vectors. Its integer translates are the sets $z+V$ with $z\in\mathbb Z^n$ .

In Lean, $\mathcal R^k$ is EuclideanSpace ℝ (Fin k), a basis is b : Fin m → EuclideanSpace ℝ (Fin k), the lattice is lattice b = Submodule.span ℤ (Set.range b), $|b_j^*|$ is gsLen b j, $b_i(j)$ is gsCoeff b i j, $d(L)$ is latticeDet b, $\Lambda_1$ is lambdaOne, $L_{j+1}$ is projLattice b j, and a reduced basis is IsReduced b.

Formalization targets

Goal: Theorem (5.5), corrected reading

For $n\ge2$ and every bounded convex set $K\subseteq\mathcal R^n$ with nonempty interior and $K\cap\mathbb Z^n=\emptyset$ there is a subspace $V$ spanned by integer vectors with $1\le\dim V\le n-1$ and

\#\{\,z+V : z\in\mathbb Z^n,\ (z+V)\cap K\ne\emptyset\,\}\ \le\ n^{2(n-\dim V)}.

The printed theorem allows "an $i$ dimensional space $V$ " with $1\le i\le n$ and bound $n^{2(n-i+1)}$ . Taken literally that is trivial ( $V=\mathcal R^n$ , one translate). The proof on the same page takes $V=\operatorname{span}(b_1,\dots,b_{i-1})$ , of dimension $i-1$ , and remarks that this "ensures that the subspace $V$ is always of dimension at least 1". The goal states that reading.

Milestones

Theorem (1.11), Minkowski's convex body theorem (referenced from the platform, in Mathlib's general form).
Theorem (1.12): every $m$ -dimensional lattice has a nonzero vector with $|v|\le\sqrt m\,d(L)^{1/m}$ .
Proposition 1.9: a primitive lattice vector belongs to some basis.
Proposition 2.16, existence form: every lattice has a reduced basis.
Proposition 4.2: for any $b_0$ with projection $\bar b_0$ onto the span, some $b\in L$ has $|b-\bar b_0|\le\frac12(\sum_jb_j(j)^2)^{1/2}\le\frac{\sqrt m}2\max_jb_j(j)$ .
Proposition 4.3: for a reduced basis and $i$ maximising $b_i(i)$ , the tail $(\lambda_i,\dots,\lambda_m)$ of every closest lattice point to $b_0$ lies in an explicit set of at most $m^{m-i+1}$ integer vectors.

Significance

Theorem (5.5) is a structural form of the flatness theorem. For $\dim V=n-1$ it says that a lattice-free convex body meets fewer than $n^2$ consecutive integer hyperplanes of some integral direction. For smaller $\dim V$ it gives a finer decomposition of $\mathbb Z^n$ into translates, each a lower-dimensional integer program. This is the recursion behind fixed-dimension integer programming, and statements of this form are used in lattice-point enumeration, in the geometry of numbers (covering minima), and in cutting-plane theory (lattice-free bodies define split and intersection cuts). Propositions 4.2 and 4.3 are the correctness core of exact closest-vector enumeration.

The results are proved in the literature, though Theorem (5.5) is proved "albeit sketchily" in the paper itself. As far as is known, none of them is formalized: Mathlib has Minkowski's convex body theorem and the ZLattice API, but not Gram–Schmidt lattice invariants, Korkine–Zolotarev bases, Hermite-type bounds, nearest-plane rounding, or any flatness theorem. This mission produces the first machine-checked versions. It also corrects three statements that are wrong as printed (below), so the formal statements are the ones that can be relied on.

Difficulty

The naive route to (5.5) is to take a flat direction directly: bound the lattice width of $K$ and count hyperplanes. That needs a flatness theorem with an explicit bound below $n^2$ , which is itself the hard part. The paper's argument instead needs John's theorem (every convex body lies between an ellipsoid and its $n$ -fold dilation), a reduced basis of the transformed lattice, and a counting argument across projected lattices that combines Minkowski's bound on each $L_i$ with the covering estimate of Proposition 4.2. None of John's theorem, reduced bases or the projected-lattice counting is in Mathlib.

Proposition 4.3 is also delicate as printed: the per-coordinate count on p. 24 undercounts the integers in a closed interval, so the printed arithmetic cannot be transcribed as it stands. Proposition 2.16 in the paper is the correctness of the algorithm SHORTEST. Here only the existence of a reduced basis is needed, which requires attainment of $\Lambda_1$ on every projected lattice and a lifting argument (Proposition 1.9).

Formalization scope

Conventions: indices are 0-based (Fin m), so the paper's $L_j$ is projLattice b (j-1) and its bound $n^{n-i+1}$ is m ^ (m - i). Gram–Schmidt is Mathlib's unnormalised gramSchmidt. Lattices are Submodule ℤs of a real Euclidean space generated by a linearly independent family, and $m\le k$ is allowed, because (1.12) and 4.2 are applied to projected lattices. The goal counts translates as sets with Set.encard, so the bound includes finiteness. $K$ is assumed convex, bounded and with nonempty interior, but not closed.

Three printed statements are corrected, and the corrections are recorded in each item's Formalization Note.

(1.12)'s constant $\frac12\sqrt n$ is false for $n\le7$ (for example $L=\mathbb Z$ , or the hexagonal lattice) and is replaced by $\sqrt n$ , the constant the paper's own later proofs use.
Proposition 4.2's second sentence is stated for $\bar b_0$ instead of $b_0$ .
Proposition 4.3 fails at $n=1$ and is stated for $m\ge2$ with the proof's explicit candidate set $T$ , since an existential $T$ is satisfied by the set of tails of closest points and says nothing.

Trivializing formalizations are ruled out: the goal forbids $\dim V=n$ , which gives one translate, and $\dim V=0$ , where no translate meets $K$ . It requires nonempty interior (the empty set would satisfy everything) and counts with encard (an infinite count cannot become $0$ ).

Out of scope: the paper's algorithms (SHORTEST, SELECT-BASIS, ENUMERATE, CLP, CLP′, ILP) and their operation and bit counts (Theorems 2.17, 3.9, 4.5, 5.4), because Mathlib has no cost model. Also out of scope is §6 (NP-completeness of the $L_2$ closest vector problem and Cook reductions), because Mathlib has no complexity classes. The definitions of this mission (lattice, gsLen, gsCoeff, latticeDet, lambdaOne, projLattice, IsReduced) are reusable for any later work on lattice reduction. Contributions are welcome at every level: John's theorem, Hermite-type bounds, Korkine–Zolotarev existence, and the counting lemmas.

Selected references

R. Kannan, Minkowski's Convex Body Theorem and Integer Programming, Mathematics of Operations Research 12(3):415–440, 1987. https://doi.org/10.1287/moor.12.3.415
H. W. Lenstra Jr., Integer programming with a fixed number of variables, Mathematics of Operations Research 8(4):538–548, 1983. https://doi.org/10.1287/moor.8.4.538
R. Kannan, L. Lovász, Covering minima and lattice-point-free convex bodies, Annals of Mathematics 128(3):577–602, 1988. https://doi.org/10.2307/1971436
A. K. Lenstra, H. W. Lenstra Jr., L. Lovász, Factoring polynomials with rational coefficients, Mathematische Annalen 261:515–534, 1982. https://doi.org/10.1007/BF01457454
F. John, Extremum problems with inequalities as subsidiary conditions, Studies and Essays presented to R. Courant, 1948, 187–204.

9 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Worst-Case Value-At-Risk and Robust Portfolio Optimization: A Conic Programming Approach 1: Exact Worst-Case VaR under Known Mean and Covariance and Its SDP RepresentationsResearch Paper

Motivation

Value-at-Risk (VaR) is the standard regulatory measure of downside risk of a portfolio: the loss level that is exceeded only with a prescribed small probability $\varepsilon$ . Computing it requires the full distribution of asset returns, which is rarely known. In practice one estimates a mean vector and a covariance matrix and then assumes a Gaussian distribution, which understates the probability of large losses when returns are heavy-tailed or skewed.

El Ghaoui, Oks and Oustry (Oper. Res. 51(4), 2003) replace the distributional assumption by a worst case: the VaR is computed against every distribution consistent with the known moments. For known mean and covariance they obtain an exact closed form and several semidefinite (SDP) representations of this worst-case VaR. The SDP forms are what make the approach extend to moment uncertainty (moments only known to lie in a set, §2.2 of the paper) and to robust portfolio optimization. The equivalence between the probabilistic statement and the closed form is also a multivariate one-sided Chebyshev bound, related to Bertsimas and Popescu (SIAM J. Optim. 15(3), 2005; working paper 2000).

Setting

There are $n$ assets. Their returns over one period form a random vector $x \in \mathbb R^n$ , and a portfolio $w \in \mathbb R^n$ earns $r(w,x) = w^\top x$ . The paper restricts $w$ to an admissible set that does not contain $0$ ; only $w \neq 0$ is used.

The distribution of $x$ is unknown except for its mean $\hat x \in \mathbb R^n$ and covariance matrix $\Gamma$ , with $\Gamma \succ 0$ (positive definite). Let $\mathcal P$ be the set of all probability distributions on $\mathbb R^n$ with these two moments. For a loss level $\gamma$ , the loss set is $\mathcal S = \{x \mid \gamma \le -x^\top w\}$ . The worst-case VaR at level $\varepsilon$ is (Eq. (4))

V_{\mathcal P}(w) = \min\Big\{\gamma \;:\; \sup_{P\in\mathcal P} P(\mathcal S) \le \varepsilon\Big\}.

Further notation: $\kappa(\varepsilon) = \sqrt{(1-\varepsilon)/\varepsilon}$ (Eq. (8)); for symmetric matrices, $A \succeq B$ means $A - B$ is positive semidefinite and $\langle A, B\rangle = \operatorname{Tr}(AB)$ . The second-moment matrix is (Eq. (6))

\Sigma = \begin{bmatrix} S & \hat x \\ \hat x^\top & 1\end{bmatrix}, \qquad S = \Gamma + \hat x\hat x^\top.

Formalization targets

Goal: Theorem 1 (pp. 545–546)

For $\Gamma \succ 0$ , $w \neq 0$ , $\varepsilon \in (0,1)$ and $\gamma \in \mathbb R$ , the following five propositions are equivalent:

$\sup_{P \in \mathcal P} P\{\gamma \le -w^\top x\} \le \varepsilon$ ;
$\kappa(\varepsilon)\,\|\Gamma^{1/2} w\|_2 - \hat x^\top w \le \gamma$ ;
there are a symmetric $M$ and $\tau \in \mathbb R$ with $\langle M, \Sigma\rangle \le \tau\varepsilon$ , $M \succeq 0$ , $\tau \ge 0$ , and $M + \begin{bmatrix} 0 & w\\ w^\top & -\tau + 2\gamma\end{bmatrix} \succeq 0$ ;
every $x$ with $\begin{bmatrix}\Gamma & x - \hat x\\ (x-\hat x)^\top & \kappa(\varepsilon)^2\end{bmatrix} \succeq 0$ satisfies $-x^\top w \le \gamma$ ;
there are a symmetric $\Lambda$ and $v \in \mathbb R$ with $\langle \Lambda, \Gamma\rangle + \kappa(\varepsilon)^2 v - \hat x^\top w \le \gamma$ and $\begin{bmatrix}\Lambda & w/2\\ w^\top/2 & v\end{bmatrix} \succeq 0$ .

In particular

V_{\mathcal P}(w) = \kappa(\varepsilon)\,\|\Gamma^{1/2}w\|_2 - \hat x^\top w.

Milestones (the steps of the paper's proof)

Condition C.1 ( $l(x) = [x^\top\,1] M [x^\top\,1]^\top \ge 0$ for all $x$ ) is equivalent to $M \succeq 0$ (p. 546).
Conditions C.1 and C.2 are equivalent to the existence of $\tau \ge 0$ with $M \succeq 0$ and $M + \begin{bmatrix} 0 & \tau w\\ \tau w^\top & -1+2\tau\gamma\end{bmatrix} \succeq 0$ (p. 546).
The worst-case probability $\sup_{P\in\mathcal P} P(\mathcal S)$ equals the value of the SDP $\inf \langle M, \Sigma\rangle$ under the constraints above (Eq. (14), pp. 546–547).
The Schur-complement reduction (19)–(20) of the constraints of the dual problem (18) (p. 547).
The closed form of $\phi(y)$ and its maximum at $y = \varepsilon$ (p. 547).
Condition (10) describes the ellipsoid $\{x \mid (x-\hat x)^\top\Gamma^{-1}(x-\hat x) \le \kappa(\varepsilon)^2\}$ , and the maximal loss $-x^\top w$ over it is $\kappa(\varepsilon)\sqrt{w^\top\Gamma w} - \hat x^\top w$ (p. 546).

Significance

The result. Proposition 2 turns the worst-case VaR into a second-order cone function of $w$ , so minimizing it over a polytope of portfolios is a second-order cone program (Eq. (12)). The SDP forms 3 and 5 are the basis of the paper's §2.2–§3: they extend, with the moments only known to lie in a convex set, to a single SDP whose value is the worst-case VaR over that set. Proposition 4 gives a deterministic reading: the worst-case VaR is the largest loss when the return vector is only known to lie in an ellipsoid, which connects distributional robustness to robust optimization with ellipsoidal uncertainty.

Formalizing it. The result is proved in the paper, with two imported steps: strong duality for the moment problem (Smith 1995; Bonnans and Shapiro 2000) and a Slater-type strong duality for the one-constraint quadratic condition. No machine-checked version is known. A formal proof would supply these steps with explicit hypotheses and would produce a Lean statement of the multivariate one-sided Chebyshev (Cantelli) bound with tightness over the full moment class.

Difficulty

The matrix equivalences (2 ⇔ 4 ⇔ 5 and 2 ⇔ 3) are Schur complements and finite-dimensional SDP duality. The difficulty is Proposition 1. The upper bound (Cantelli's inequality for $w^\top x$ ) handles one direction, but the converse requires tightness: for every $\gamma$ below the closed form, a distribution on $\mathbb R^n$ with exactly the prescribed mean and full covariance matrix $\Gamma$ that puts probability more than $\varepsilon$ on the loss set. A scalar extremal distribution for $w^\top x$ does not by itself have the right covariance in the other directions, and a Gaussian does not reach the bound. The paper's route through the moment problem instead needs strong duality between a supremum over measures and an infimum over matrices, which is where the positive definiteness of $\Sigma$ enters.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin n); $x^\top w$ is the inner product, and matrices are Matrix (Fin n) (Fin n) ℝ. Matrices of size $n+1$ are indexed by Fin n ⊕ Fin 1 and built with Matrix.fromBlocks (the helper bordered A v c is $[[A, v],[v^\top, c]]$ ). $A \succeq 0$ is PosSemidef, $\Gamma \succ 0$ is PosDef, $\langle A, B\rangle$ is (A * B).trace, and $\|\Gamma^{1/2}w\|_2$ is written $\sqrt{w^\top\Gamma w}$ .
The class $\mathcal P$ (HasMeanCov) contains every Borel probability measure on $\mathbb R^n$ whose coordinates are square-integrable, with mean $\hat x$ and centred covariance $\Gamma$ . It is not restricted to densities or to Gaussians: the Gaussian class gives a different constant, $-\Phi^{-1}(\varepsilon)$ .
Sup, inf and max: " $\sup_{P\in\mathcal P}P(\mathcal S) \le \varepsilon$ " is stated as " $P(\mathcal S) \le \varepsilon$ for every $P \in \mathcal P$ ". The worst-case probability SDP is stated as IsLUB/IsGLB of one real number (no attainment is claimed). The maxima over $v$ , over $y \in [\varepsilon,1]$ and over the ellipsoid are IsGreatest.
Corrections to the printed statement. The paper prints $\varepsilon \in (0,1]$ ; at $\varepsilon = 1$ Proposition 1 holds for every $\gamma$ while Propositions 2–5 require $\gamma \ge -\hat x^\top w$ , so the goal assumes $0 < \varepsilon < 1$ . The goal also assumes $w \neq 0$ , the paper's standing assumption; with $w = 0$ , $\gamma = 0$ Proposition 1 fails and Proposition 2 holds. Milestones that remain true at $\varepsilon = 1$ keep $\varepsilon \le 1$ .
A goal that omits Proposition 1 would only be matrix algebra and is not this theorem. The five-way equivalence must be proved with the probabilistic statement included.
Useful infrastructure, reusable beyond this mission: the homogenization lemma for quadratic functions, the S-lemma with one affine constraint, the Schur-complement criteria for bordered PSD matrices, and duality for the moment problem. Proofs of any milestone, and of lemmas building a distribution with prescribed mean and covariance, are welcome.

Selected references

L. El Ghaoui, M. Oks, F. Oustry, Worst-Case Value-at-Risk and Robust Portfolio Optimization: A Conic Programming Approach, Operations Research 51(4):543–556, 2003. https://doi.org/10.1287/opre.51.4.543.16101
D. Bertsimas, I. Popescu, Optimal Inequalities in Probability Theory: A Convex Optimization Approach, SIAM J. Optim. 15(3):780–804, 2005. https://doi.org/10.1137/S1052623401399903
J. E. Smith, Generalized Chebychev Inequalities: Theory and Applications in Decision Analysis, Operations Research 43(5):807–825, 1995. https://doi.org/10.1287/opre.43.5.807
J. F. Bonnans, A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
L. Vandenberghe, S. Boyd, K. Comanor, Generalized Chebyshev Bounds via Semidefinite Programming, SIAM Review 49(1):52–64, 2007. https://doi.org/10.1137/S0036144504440543

8 thms5 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: mikedeng1

The Structure of Dynamic Programing Models: A Solution of the Principle of Optimality with Vanishing Tail Is the Optimal ReturnResearch Paper

Motivation

Dynamic programming, as introduced by Bellman in the early 1950s, solves sequential decision problems through a functional equation: the value of a problem started in a given state equals the best one-stage return plus the value of the problem started in the state that decision leads to. In practice the argument usually runs backwards. One writes down the functional equation, finds or characterizes a solution, and reads off the structure of optimal decisions from that solution. This is legitimate only if two things hold: an optimal policy exists at all, and the solution of the functional equation that was found is the optimal value, not some other solution of the same equation.

Samuel Karlin's 1955 paper The Structure of Dynamic Programing Models (Naval Research Logistics Quarterly 2(4):285–294) gives an abstract deterministic model in which both questions can be posed precisely. It proves existence of optimal strategies by a compactness argument (Theorem 1), derives the functional equation, which it calls the Principle of Optimality, and identifies the condition under which a solution of that equation is the optimal return: a tail term must vanish. Later treatments of dynamic programming on general state spaces, such as Blackwell's discounted and positive programming (1965–1967) and the monographs of Bertsekas and Shreve, state their verification theorems in the same form, with a solution of the optimality equation plus a condition at infinity.

Setting

The model has a state space $\Omega$ , a Hausdorff topological space, and a decision space $D$ , a nonempty compact Hausdorff space. A strategy is a sequence $s = (\delta_1, \delta_2, \dots)$ of decisions, one per stage. The strategy space $S = D \times D \times \cdots$ carries the product topology and is compact by Tychonoff's theorem.

The data are:

a return function $L : \Omega \times D \to \mathbb{R}$ , continuous and non-negative, where $L(\omega, \delta)$ is the return for taking decision $\delta$ in state $\omega$ ;
a transition $(\delta, \omega) \mapsto T_\delta\,\omega \in \Omega$ , the state faced at the next stage after decision $\delta$ in state $\omega$ ;
a normalization factor $P : D \to \mathbb{R}$ , continuous and positive.

From an initial state $\omega$ , a strategy $s$ generates the trajectory $\omega_1 = \omega$ , $\omega_n = T_{\delta_{n-1}}\,\omega_{n-1}$ , and the weights $P_n(s) = \prod_{i=1}^{n-1} P(\delta_i)$ with $P_1(s) = 1$ . The total yield is

\Phi(\omega, s) = \sum_{n=1}^{\infty} L(\omega_n, \delta_n)\, P_n(s),

and the optimal return is $K(\omega) = \max_{s \in S} \Phi(\omega, s)$ . The standing assumption of the paper, display (1), is that the partial sums $\sum_{n=1}^{k} L(\omega_n, \delta_n) P_n(s)$ converge uniformly in $s \in S$ for each $\omega$ .

Formalization targets

Goal: uniqueness of solutions with vanishing tail

Let $M : \Omega \to \mathbb{R}$ solve the functional equation

M(\omega) = \max_{\delta \in D} \bigl\{ L(\omega, \delta) + P(\delta)\, M(T_\delta\,\omega) \bigr\} \quad \text{for all } \omega,

with the maximum attained, and suppose that for every $\omega$

\lim_{n \to \infty} \ \sup_{\delta_1, \dots, \delta_n} |M(\omega_n)| \prod_{i=1}^{n-1} P(\delta_i) = 0.

Then $M(\omega) = \max_{s \in S} \Phi(\omega, s)$ for every $\omega$ , and the maximum is attained (pp. 290–291, §Uniqueness).

Milestones

Theorem 1 (p. 287). If the series (1) converges uniformly in $S$ , an optimal strategy $s^*$ exists: $\Phi(\omega, s^*) = \max_S \Phi(\omega, s)$ .
Shift identity (p. 290, first display). For a strategy $s$ with convergent yield series and the shift $s' = (\delta_2, \delta_3, \dots)$ ,

\Phi(\omega, s) = L(\omega, \delta_1) + P(\delta_1)\, \Phi(T_{\delta_1}\,\omega, s').

Principle of Optimality, eq. (2) (p. 290). $K(\omega) = \max_{\delta_1} \{ L(\omega, \delta_1) + P(\delta_1) K(T_{\delta_1}\,\omega) \}$ .
n-step expansion (p. 291, first display). A solution $M$ of (2) satisfies, for every $n$ ,

M(\omega) = \max_{\delta_1, \dots, \delta_n} \Bigl\{ \sum_{m=1}^{n} L(\omega_m, \delta_m) P_m(s) + M(\omega_{n+1}) P_{n+1}(s) \Bigr\}.

Significance

Milestone 3 says that the optimal return solves the functional equation. The goal gives the converse on a class of candidate solutions: any solution with a vanishing tail is the optimal return. Together they justify solving a dynamic program by solving its functional equation. The paper's two examples, a two-operation allocation problem with discounting and a resource allocation model driving the state to the origin, obtain uniqueness among bounded solutions and among continuous solutions vanishing at the origin respectively, by checking the tail condition. Without the tail condition the conclusion fails; the paper notes that the limit term "need not be true in general for any solution to the functional equation".

All four milestones and the goal are classical results with published proofs. None of them has a machine-checked proof on this platform: its existing Bellman-equation theorems concern finite-state stochastic models with a constant discount factor, and this model has neither restriction. The mission produces a formal version of the general deterministic model on topological state spaces, with optimality characterized by a verification theorem, which later missions on the paper's examples can reuse.

Difficulty

Existence rests on continuity of $s \mapsto \Phi(\omega, s)$ on the product space. Each term $L(\omega_n, \delta_n) P_n(s)$ depends on the first $n$ decisions through the composite map $\omega_n = T_{\delta_{n-1}} \circ \cdots \circ T_{\delta_1}\,\omega$ , and continuity of that composite in all decisions at once does not follow from separate continuity of $T_\delta\,\omega$ in $\delta$ and in $\omega$ . The limit of the series is continuous only because the convergence is uniform.

For uniqueness, the paper's display " $M(\omega) = \max_S \Phi(\omega, s) + \lim_n \max M(\omega_n) \prod P(\delta_i)$ " is not an identity: a maximum of a sum is not the sum of the maxima. A proof has to bound $M$ from above by the yield of every strategy and from below by the yield of one particular strategy, and the lower bound fails if the tail term is controlled only from above. Attainment of the maximum in the conclusion needs a strategy to be exhibited, not only a supremum computed.

Formalization scope

A strategy is a function s : ℕ → D, with the product topology. Lean's 0-based index $k$ is the paper's stage $k+1$ : s 0 is $\delta_1$ , trajectory T ω s 0 is $\omega_1 = \omega$ , and weight P s k is $P_{k+1}(s)$ , so weight P s 0 = 1. The total yield is a tsum and the optimal return a supremum over all strategies. "Maximum" is encoded as IsGreatest of a range, so every stated maximum is attained. Uniform convergence of (1) is TendstoUniformly of the partial sums to $\Phi(\omega, \cdot)$ along atTop.

The formalization commits to the following, relative to the page:

The model's assumptions (1)–(3) of p. 286, non-negativity of $L$ , and positivity and continuity of $P$ appear as hypotheses of every statement.
A single return function $L$ is used, not stage-dependent $L_n$ , as in display (1) and as the functional equation (2) requires. $P_n$ has the product form, which the paper adopts "unless stated to the contrary".
Assumption (4), separate continuity of $T_\delta\,\omega$ in $\delta$ and in $\omega$ , is strengthened to joint continuity of $(\delta, \omega) \mapsto T_\delta\,\omega$ . This supports the paper's assertion (p. 287) that each term is a continuous function of $s$ , which separate continuity does not give.
$D$ is assumed nonempty. With $D$ empty there is no strategy and Theorem 1 is false.
The paper leaves the class of admissible solutions open ("an appropriate class of M's for which the lim = 0"). The goal fixes it as the two-sided condition: for every $\omega$ and $\varepsilon > 0$ there is $N$ with $|M(\omega_n)|\,P_n(s) \le \varepsilon$ for all $n \ge N$ and all $s$ . Both of the paper's examples verify this form.

Lean's tsum of a non-summable series is $0$ , and a supremum of an unbounded family is $0$ . Neither default can make a statement trivially true. The uniform-convergence hypothesis forces the series to converge, and under Theorem 1's hypotheses $\Phi(\omega, \cdot)$ is continuous on a compact space, so the supremum is a maximum. The goal's conclusion is stated without a supremum. A sorry-free check confirms that all hypotheses of the goal hold on a concrete instance with non-zero return: two decisions, constant return $1$ , $P \equiv 1/2$ , and $M \equiv 2$ .

Needed infrastructure: Tychonoff's theorem, continuity of uniform limits, and attainment of maxima on compact spaces, all in Mathlib. The mission's own definitions are the trajectory, weights, partial and total yield, and the optimal return. Contributions of intermediate lemmas are welcome, for example continuity of $s \mapsto \omega_n$ , summability from uniform convergence, and the upper and lower tail estimates for $M$ . So are formalizations of the paper's Remarks 1 and 3 (Dini's theorem and convergence of the $k$ -stage optimal returns).

Selected references

S. Karlin, The Structure of Dynamic Programing Models, Naval Research Logistics Quarterly 2(4):285–294, 1955. https://doi.org/10.1002/nav.3800020408
R. Bellman, Dynamic Programming, Princeton University Press, 1957. https://press.princeton.edu/books/paperback/9780691146683/dynamic-programming
D. Blackwell, Discounted Dynamic Programming, Annals of Mathematical Statistics 36(1):226–235, 1965. https://doi.org/10.1214/aoms/1177700285
D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html

6 thms3 active usersReviewed

Completed

Information Theory Operations Research Optimization+1·Captain: mikedeng1

Worst-Case Value-At-Risk and Robust Portfolio Optimization: A Conic Programming Approach 2: Closed Form of the Entropy-Constrained Worst-Case VaRResearch Paper

Motivation

Value-at-Risk (VaR) is the loss level that a portfolio exceeds with probability at most $\varepsilon$ . It is the standard risk measure of banking regulation, and its classical computation assumes Gaussian returns: for a Gaussian return vector with mean $\hat x$ and covariance $\Gamma$ it equals $-\Phi^{-1}(\varepsilon)\sqrt{w^\top\Gamma w} - \hat x^\top w$ , where $\Phi$ is the standard normal distribution function. Real returns are not exactly Gaussian, and a VaR computed from a misspecified distribution can badly understate risk.

El Ghaoui, Oks and Oustry (Oper. Res. 51(4), 2003) replace the single distribution by a class $\mathcal P$ of distributions and define the worst-case VaR as the smallest loss level whose probability is at most $\varepsilon$ under every distribution of the class. Their first class, distributions with a given mean and covariance, leads to the Chebyshev-type bound of their Theorem 1, whose worst case is attained by discrete distributions. §4.2 of the paper asks instead for distributions that stay close to a Gaussian, measured by relative entropy (Kullback–Leibler divergence). Such balls are the basic uncertainty sets of distributionally robust optimization and of robust control in economics (Hansen and Sargent's multiplier and constraint preferences), and they give a smooth worst case. Theorem 9 computes the resulting worst-case VaR in closed form.

Setting

Returns are random vectors $x \in \mathbb R^n$ and a portfolio is a vector $w \in \mathbb R^n$ with $w \neq 0$ ; its return is $r(w,x) = w^\top x$ . For a level $\gamma \in \mathbb R$ the loss set is $\mathcal S_\gamma = \{x : \gamma \le -x^\top w\}$ (Eq. 13 of the paper).

Given a class $\mathcal P$ of probability distributions on $\mathbb R^n$ and $\varepsilon \in (0,1)$ , the worst-case Value-at-Risk (Eq. 4) is

V_{\mathcal P}(w) = \min\Big\{\gamma \in \mathbb R : \sup_{P \in \mathcal P} P(\mathcal S_\gamma) \le \varepsilon\Big\}.

Fix a mean $\hat x \in \mathbb R^n$ and a positive definite covariance $\Gamma \succ 0$ , and let $P_0 = \mathcal N(\hat x, \Gamma)$ be the reference Gaussian. For $d \ge 0$ the relative-entropy class (Eq. 43) is

\mathcal P_d = \Big\{P \text{ probability on } \mathbb R^n : \mathrm{KL}(P, P_0) = \int \log\frac{dP}{dP_0}\,dP \le d\Big\},

with $\mathrm{KL}(P,P_0) = +\infty$ unless $P$ is absolutely continuous with respect to $P_0$ .

The risk factor (Eq. 45) is

f(\varepsilon,d) = \sup_{\lambda>0}\frac{e^{\varepsilon/\lambda - d} - 1}{e^{1/\lambda} - 1}, \qquad \kappa(\varepsilon,d) = -\Phi^{-1}\big(f(\varepsilon,d)\big),

and the Gaussian tail of the loss set is $\phi(\gamma) = P_0(\mathcal S_\gamma) = 1 - \Phi\big((\gamma + w^\top\hat x)/\sqrt{w^\top\Gamma w}\big)$ .

Formalization targets

Goal: Theorem 9 (p. 553)

For $\Gamma \succ 0$ , $w \neq 0$ , $d \ge 0$ and $0 < \varepsilon < 1$ , the minimum in (4) over $\mathcal P_d$ exists and

V_{\mathcal P_d}(w) = \kappa(\varepsilon,d)\sqrt{w^\top\Gamma w} - \hat x^\top w. \tag{44}

Milestones

The milestones follow the proof of Theorem 9 on pp. 553–554, in attack order.

Eq. (45). The two expressions of $f$ agree: $\sup_{\lambda>0}\frac{e^{\varepsilon/\lambda-d}-1}{e^{1/\lambda}-1} = \sup_{v>0}\frac{e^{-d}(v+1)^\varepsilon - 1}{v}$ .
Gaussian tail. $P_0(\mathcal S_\gamma) = 1 - \Phi\big((\gamma + w^\top\hat x)/\sqrt{w^\top\Gamma w}\big)$ .
Eq. (47). For $\lambda > 0$ , the Lagrangian $L(Q) = Q(\mathcal S_\gamma) + \lambda_0(1 - Q(\mathbb R^n)) + \lambda(d - \mathrm{KL}\text{-integral})$ is maximised over finite measures $Q \ll P_0$ by the exponentially tilted density $dQ^\star/dP_0 = \exp((\chi_{\mathcal S} - \lambda_0)/\lambda - 1)$ , with value

\theta(\lambda_0,\lambda) = \lambda_0 + \lambda d + \lambda e^{-\lambda_0/\lambda - 1}\big((e^{1/\lambda}-1)\phi(\gamma) + 1\big).

Eq. (48). $\min_{\lambda_0\in\mathbb R}\theta(\lambda_0,\lambda) = \lambda d + \lambda\log\big((e^{1/\lambda}-1)\phi(\gamma)+1\big)$ .
Duality. $\sup_{P\in\mathcal P_d} P(\mathcal S_\gamma) = \inf_{\lambda>0}\big(\lambda d + \lambda\log((e^{1/\lambda}-1)\phi(\gamma)+1)\big)$ .
Inversion. For $d > 0$ : some $\lambda > 0$ makes the dual value at most $\varepsilon$ if and only if $\gamma \ge \kappa(\varepsilon,d)\sqrt{w^\top\Gamma w} - w^\top\hat x$ .
Remark after Theorem 9. $f(\varepsilon, 0) = \varepsilon$ , so $\kappa(\varepsilon,0) = -\Phi^{-1}(\varepsilon)$ . The risk factor $\kappa(\varepsilon, d)$ is strictly increasing in $d \ge 0$ .

Significance

Theorem 9 says that an entropy ball around a Gaussian leaves the form of the Gaussian VaR unchanged: only the risk factor moves, from $-\Phi^{-1}(\varepsilon)$ to $\kappa(\varepsilon,d)$ , a scalar computed by a one-dimensional maximisation. The worst-case VaR therefore stays a convex function of $w$ whenever $\kappa \ge 0$ , and minimising it over a polytope of portfolios is a second-order cone program (problem (3) of the paper). The number $f(\varepsilon,d)$ is the largest $p$ with $\mathrm{KL}(\mathrm{Bernoulli}(\varepsilon)\,\|\,\mathrm{Bernoulli}(p)) \le d$ , which ties the result to the binary-divergence bounds used throughout information theory.

The theorem was proved in 2003. The worst-case-probability step (milestone 5) is an instance of the Donsker–Varadhan / Gibbs variational duality for relative-entropy balls, which the paper imports from the literature (Smith 1995). No machine-checked proof of Theorem 9 or of this duality on $\mathbb R^n$ is known. A formalization would give a verified closed form for a relative-entropy distributionally robust chance constraint, and the duality and tilting lemmas would serve any mission on KL-ball robust optimization.

Difficulty

The obvious argument is Lagrangian duality for the infinite-dimensional problem $\sup\{P(\mathcal S_\gamma) : \mathrm{KL}(P,P_0) \le d\}$ . Weak duality and the pointwise maximisation that produces the tilted density are elementary. The difficulty is the step the paper cites rather than proves: that the duality gap is zero, and that the supremum over distributions equals the infimum of the dual over $\lambda > 0$ . The feasible set is a set of measures, the objective is an indicator, and the constraint is a divergence that is $+\infty$ off a set of absolutely continuous measures, so a finite-dimensional Slater argument does not apply as stated.

The second difficulty is at the boundary of the parameters. At $d = 0$ the supremum defining $f(\varepsilon,0)$ is approached only as $\lambda \to \infty$ , so the final inversion step behaves differently from $d > 0$ . At $\varepsilon = 1$ the theorem is false, since every level $\gamma$ is feasible and (4) has no minimum.

Formalization scope

Returns live in EuclideanSpace ℝ (Fin n). $P_0$ is Mathlib's multivariateGaussian xhat Γ with Γ.PosDef, and $\mathrm{KL}$ is InformationTheory.klDiv, which is $\infty$ unless $P \ll P_0$ with integrable log-likelihood ratio and equals $\int\log\frac{dP}{dP_0}\,dP$ otherwise for probability measures. The class $\mathcal P_d$ requires IsProbabilityMeasure P. $\Phi$ is cdf (gaussianReal 0 1), and $\Phi^{-1}(p)$ is defined as $\inf\{t : p \le \Phi(t)\}$ , which inverts $\Phi$ on $(0,1)$ . The quadratic form $w^\top\Gamma w$ is a double sum, and $\|\Gamma^{1/2}w\|_2$ is written $\sqrt{w^\top\Gamma w}$ .

Conventions the Lean statements commit to:

"min" in (4) is IsLeast of the feasible set $\{\gamma : P(\mathcal S_\gamma) \le \varepsilon \ \forall P \in \mathcal P_d\}$ . " $\sup_{P}P(\mathcal S_\gamma) \le \varepsilon$ " is written "for every $P$ ", with probabilities compared in $[0,\infty]$ .
The paper prints $\varepsilon \in (0,1]$ . The mission assumes $0 < \varepsilon < 1$ , because the goal is false at $\varepsilon = 1$ .
$w \neq 0$ is the paper's assumption that the admissible set of portfolios excludes $0$ .
$f(\varepsilon,d)$ is a Lean sSup of a set that is nonempty and bounded above by $1$ for $\varepsilon \le 1$ , $d \ge 0$ .
The duality of milestone 5 is stated as the existence of one real number that is both the least upper bound of the worst-case probabilities and the greatest lower bound of the dual values, not as an equality of Lean's sSup and sInf.
Eq. (48) is stated as an attained minimum (IsLeast), which the calculus gives.
Milestone 3 works with finite measures $Q \ll P_0$ with integrable log-likelihood ratio in place of the paper's densities $p$ . It uses the complement of $\mathcal S_\gamma$ where the paper writes $\{\gamma \ge -x^\top w\}$ , which differs by a $P_0$ -null hyperplane.
Milestone 6 assumes $d > 0$ ; the goal keeps $d \ge 0$ .

Restricting $\mathcal P_d$ to $\{P_0\}$ , dropping IsProbabilityMeasure, or taking an arbitrary reference measure would trivialize or change the theorem. The class is the full KL ball around the nondegenerate Gaussian.

Infrastructure a complete development needs: the pushforward of a multivariate Gaussian under a linear functional (a one-dimensional Gaussian), the Gibbs variational principle for relative entropy, the strong duality for KL balls, and properties of $\Phi$ and its quantile (continuity, strict monotonicity, symmetry $\Phi(-t) = 1 - \Phi(t)$ ). The Gaussian-quantile and KL-ball duality lemmas are reusable beyond this mission. Contributions of any of these as separate lemmas are welcome.

Selected references

L. El Ghaoui, M. Oks, F. Oustry, Worst-Case Value-at-Risk and Robust Portfolio Optimization: A Conic Programming Approach, Operations Research 51(4):543–556, 2003. https://doi.org/10.1287/opre.51.4.543.16101
J. E. Smith, Generalized Chebychev Inequalities: Theory and Applications in Decision Analysis, Operations Research 43(5):807–825, 1995. https://doi.org/10.1287/opre.43.5.807
M. D. Donsker, S. R. S. Varadhan, Asymptotic evaluation of certain Markov process expectations for large time, I, Communications on Pure and Applied Mathematics 28(1):1–47, 1975. https://doi.org/10.1002/cpa.3160280102
L. P. Hansen, T. J. Sargent, Robust Control and Model Uncertainty, American Economic Review 91(2):60–66, 2001. https://doi.org/10.1257/aer.91.2.60

9 thms4 active usersReviewed

Completed

Operations Research Probability Statistics·Captain: mikedeng1

Are Call Center and Hospital Arrivals Well Modeled by Nonhomogeneous Poisson Processes?: Combining k Equal Subintervals of a Linear Arrival Rate Bounds the Degree of Nonhomogeneity by C/kResearch Paper

Motivation

Arrival processes to call centers and hospital emergency departments are routinely modeled as nonhomogeneous Poisson processes (NHPPs): Poisson processes whose arrival rate varies over the day. Staffing and queueing models built on this assumption are only as good as the assumption itself, so practitioners test it on data. The standard test, going back to Brown et al. (2005, doi:10.1198/016214504000001808), divides the day into short subintervals, treats the rate as constant on each, rescales the arrival times within each subinterval to $[0,1]$ , combines all the rescaled data, and applies a Kolmogorov–Smirnov (KS) test of uniformity.

Kim and Whitt (2014, doi:10.1287/msom.2014.0490) ask when this piecewise-constant approximation is justified. If the true rate is not constant on a subinterval, the rescaled arrival times are not uniform, and with enough data the KS test rejects the Poisson hypothesis even when the process really is an NHPP. Section 3 of the paper quantifies this effect through a single number, the degree of nonhomogeneity, and shows how it behaves when the interval is cut into $k$ equal pieces. This mission formalizes that section's exact computations for a linear arrival rate.

Setting

An arrival rate function $\lambda$ on an interval $[0,T]$ , $T > 0$ , is nonnegative, integrable, and strictly positive except at finitely many points. Its cumulative arrival rate is

\Lambda(t) = \int_0^t \lambda(s)\,ds .

Conditionally on $n$ arrivals in $[0,T]$ , the arrival times of an NHPP with rate $\lambda$ , divided by $T$ , are distributed as the order statistics of $n$ independent random variables on $[0,1]$ with the conditional cdf

F(t) = \frac{\Lambda(tT)}{\Lambda(T)}, \qquad 0 \le t \le 1 .

The degree of nonhomogeneity is the Kolmogorov distance of $F$ from the uniform cdf,

D = \sup_{0 \le t \le 1} |F(t) - t| .

It is zero exactly when $\lambda$ is constant, and it is the limit of the KS test statistic as the amount of data grows.

For $k \ge 1$ , divide $[0,T]$ into $k$ subintervals of length $T/k$ . For $1 \le j \le k$ the $j$ -th subinterval has cumulative rate $\Lambda_j(t) = \Lambda((j-1)T/k + t) - \Lambda((j-1)T/k)$ , conditional cdf $F_j(t) = \Lambda_j(tT/k)/\Lambda_j(T/k)$ , and share of arrivals $p_j = (\Lambda(jT/k) - \Lambda((j-1)T/k))/\Lambda(T)$ . The data of all subintervals, each rescaled to $[0,1]$ and combined, have the conditional cdf $F = \sum_{j=1}^k p_j F_j$ (LEMMA 1).

The linear arrival rate is $\lambda(t) = a + bt$ with $b \ge 0$ and $a \ge 0$ , not identically zero. When $a > 0$ its relative slope is $r = b/a$ ; on the $j$ -th subinterval the relative slope is $r_j = b/\lambda((j-1)T/k)$ .

In the Lean development these are cumRate, condCdf, degree, subCum, subCdf, weight, mixCdf, linRate and subSlope, in the namespace NHPPArrivals.LinearRate.

Formalization targets

Goal: THEOREM 5, combining equally spaced subintervals

For the linear rate, there is a constant $C$ such that for every $k \ge 1$

D = \sup_{0 \le t \le 1}|F(t) - t| = \sum_{j=1}^k p_j D_j = \sum_{j=1}^k p_j \sup_{0 \le t \le 1}|F_j(t) - t|, \tag{20}

with, if $a > 0$ ,

D = \sum_{j=1}^k \frac{p_j\, r_j T/k}{8 + 4 r_j T/k}, \tag{21}

and, if $a = 0$ ,

D = \frac{p_1}{4} + \sum_{j=2}^k \frac{p_j/(j-1)}{8 + 4/(j-1)}, \tag{22}

and in both cases $D \le C/k$ . The constant $C$ may depend on $a$ , $b$ and $T$ , but not on $k$ ; its value is left open, as in the paper.

Milestones

LEMMA 1, (17): for a general rate, the rescaled combined data have cdf $\sum_j p_j F_j$ , and the $p_j$ form a probability vector.
THEOREM 4, $a > 0$ , (14), (16): $F(t) = (tT + r(tT)^2/2)/(T + rT^2/2)$ and $D = |F(1/2) - 1/2| = rT/(8 + 4rT)$ .
THEOREM 4, $a = 0$ , (15): $F(t) = t^2$ and $D = 1/4$ .
LEMMA 1, (18): closed forms of $\Lambda_j$ , $F_j$ , $p_j$ , $r_j$ when $a > 0$ .
LEMMA 1, (19): closed forms of $\Lambda_j$ , $F_j$ , $p_j$ , $r_j$ when $a = 0$ .
THEOREM 5, (20): $D = \sum_j p_j D_j$ for one fixed $k$ .

Significance

The result gives a quantitative criterion for the piecewise-constant approximation: for a linear rate, cutting the interval into $k$ equal pieces reduces the degree of nonhomogeneity of the combined data by a factor of order $1/k$ . Since the KS critical value at sample size $n$ is of order $1/\sqrt n$ , this tells a practitioner how fine the subintervals must be, relative to the amount of data, before a KS test of the Poisson hypothesis stops rejecting merely because the rate varies within subintervals. The paper's later THEOREM 6 and its practical guidelines (§3.4, §3.6) rest on these formulas.

The results are proved in the paper by direct calculation; none of them has a machine-checked proof. The mission produces a verified library of the conditional-cdf calculus for NHPPs on an interval (the conditional cdf, its degree of nonhomogeneity, the subinterval decomposition) and the exact linear-rate formulas that the testing literature cites.

Difficulty

The computations are elementary, but two steps are not immediate. First, the supremum of $|F(t) - t|$ over $[0,1]$ is a supremum of a nonsmooth function; showing that it is attained at $t = 1/2$ requires knowing the sign of $F(t) - t$ on the whole interval, and for the combined cdf it requires that all the pieces $F_j$ attain their maximal deviation at the same point, which is special to linear rates. For a general rate the naive identity $D = \sum_j p_j D_j$ fails: the sup of a sum is at most the sum of the sups, with equality only when the maximizers coincide. Second, LEMMA 1 is a statement about the law of a rescaled random variable (the fractional part of $kX/T$ ), which requires splitting a measure along the $k$ subintervals and handling their boundary points.

Formalization scope

Rates are real functions $\lambda : \mathbb R \to \mathbb R$ ; only their values on $[0,T]$ enter. $\Lambda$ is an interval integral, subintervals are indexed by $j \in \{1, \dots, k\}$ with $k, j$ natural numbers cast to reals, and $(j-1)$ is computed in $\mathbb R$ . All quotients are real divisions; the hypotheses of every statement ( $T > 0$ , $k \ge 1$ , $b \ge 0$ , and $a > 0$ or $b > 0$ for the linear rate; integrability, nonnegativity and a finite zero set for a general rate) make every denominator $\Lambda(T)$ and $\Lambda_j(T/k)$ positive. $b \ge 0$ is the paper's standing assumption of §3.3; excluding $a = b = 0$ is §3.2's requirement that the rate be positive except at finitely many points. The degree of nonhomogeneity is sSup of the image of $[0,1]$ , and every statement that uses it also asserts that the supremum is attained, so no default value of sSup can make a statement true. The constant $C$ of THEOREM 5 is quantified before $k$ ; choosing it after $k$ would make the bound empty. The statements are about the general definitions of (17) applied to $\lambda(t) = a + bt$ , not about the closed forms (18)–(19), which are separate milestones. The formula for $r_j$ in (19) is stated for $2 \le j \le k$ only: $r_1 = b/\lambda(0)$ is undefined when $a = 0$ .

The Poisson process itself is not formalized. LEMMA 1's "i.i.d. random variables" is the paper's THEOREM 1 (the conditioning property) applied to each arrival; LEMMA 1 is stated for the law of one arrival time, the probability measure with density $\lambda/\Lambda(T)$ on $[0,T]$ . THEOREM 1, THEOREMS 2–3 and COROLLARY 1 (limits of the empirical cdf and of the KS statistic) are out of scope: they need a point-process layer, the Glivenko–Cantelli theorem and KS critical values, none of which exists in Mathlib. THEOREM 6 is out of scope because the paper gives only a sketch comparing $D$ with the KS critical value.

Contributions welcome: proofs of the milestones, general lemmas on sups of $|F(t) - t|$ for convex cdfs, and the measure-splitting argument of LEMMA 1, which is reusable for any subinterval-based test of the Poisson hypothesis.

Selected references

S.-H. Kim and W. Whitt, Are call center and hospital arrivals well modeled by nonhomogeneous Poisson processes?, Manufacturing & Service Operations Management 16(3):464–480, 2014. doi:10.1287/msom.2014.0490
L. Brown, N. Gans, A. Mandelbaum, A. Sakov, H. Shen, S. Zeltyn, L. Zhao, Statistical analysis of a telephone call center: a queueing-science perspective, Journal of the American Statistical Association 100(469):36–50, 2005. doi:10.1198/016214504000001808
F. J. Massey, The Kolmogorov–Smirnov test for goodness of fit, Journal of the American Statistical Association 46(253):68–78, 1951. doi:10.1080/01621459.1951.10500769

8 thms3 active usersReviewed

Algorithmic Game Theory Operations Research Optimization+1·Captain: mikedeng1

A Supply Chain Theory of Factoring and Reverse Factoring 1: The Supplier's Equilibrium Choice Among Recourse, Non-Recourse and Reverse FactoringResearch Paper

Motivation

Small and medium-sized suppliers that sell to large retailers typically ship first and are paid weeks or months later. Until the invoice is paid, the supplier's cash is trapped in accounts receivable, while production has to be financed up front. Factoring (selling or pledging the receivable to a financial intermediary for immediate cash) and reverse factoring (a buyer-initiated program in which the retailer approves the invoice and the supplier is paid early by the retailer's bank) are the standard remedies, and reverse factoring programs of large buyers are often coupled with an extension of payment terms. Which of these instruments a supplier should use, and how the answer depends on the credit ratings of the two firms, is the question addressed by Kouvelis and Xu, "A Supply Chain Theory of Factoring and Reverse Factoring", Management Science 67(10):6071–6088, 2021 (doi:10.1287/mnsc.2020.3788). The paper embeds each financing scheme in the pull wholesale-price game of Cachon (2004) and compares the resulting equilibria.

Setting

A retailer (the Stackelberg leader) offers a wholesale price $w$ to a capital-constrained supplier (the follower), who then chooses a production quantity $q \ge 0$ and carries the inventory; the retail price $p$ is fixed, and $0 < c < p$ is the unit production cost. Demand $D \ge 0$ has density $f$ , complementary distribution function $\bar F$ , finite mean, $f > 0$ on $[0, \mathbb Z]$ ( $\mathbb Z \le +\infty$ ), and a strictly increasing failure rate $z = f/\bar F$ (strict IFR). Expected sales are $S(q) = \int_0^q \bar F(\xi)\,d\xi$ , and $k(q) = S(q)/\bar F(q)$ .

Each firm $j \in \{s, r\}$ has a credit rating $C_j \in (C_{\min}, C_{\max})$ . The default probability $\rho_j = \rho(C_j) \in [0,1]$ is strictly decreasing in the rating, and the interest-rate premium $\eta_j = \eta(C_j) > 0$ is decreasing. Production takes a lead time $t_1$ , payment follows after a term $t_2$ , and the supplier faces a Poisson liquidity shock of rate $\lambda_s$ during production (the retailer, rate $\lambda_r$ ). Under a scheme $i \in \{\mathcal F, \mathcal N, \mathcal R\}$ (recourse, non-recourse, reverse factoring, the last with a payment extension $\tau \ge 0$ ), the supplier's expected profit is

\pi_i(q; w) = (1-\rho_s)\big(\Lambda_i e^{-\lambda_s t_1} w S(q) - c q e^{\eta_s t_1}\big),

with coefficients $\Lambda_{\mathcal F} = (1-\rho_r) + (1-\rho_s) - e^{\eta_s t_2}$ , $\Lambda_{\mathcal N} = e^{-\eta_r t_2}(1-\rho_r)$ , $\Lambda_{\mathcal R} = e^{-\eta_r(t_2+\tau)}$ , and effective unit cost $c_i = c\,e^{(\eta_s+\lambda_s)t_1}/\Lambda_i$ . The retailer's profit is $e^{-\lambda_s t_1}(1-\rho_r)(p-w)S(q)$ under factoring and carries the extra factor $2 - e^{-\lambda_r \tau}$ under reverse factoring.

Formalization targets

Goal: Proposition 5

For a given $\tau \ge 0$ , let $\mathbb C_3$ be the unique supplier rating with $\Lambda_{\mathcal F} = \Lambda_{\mathcal R}$ , $\mathbb C_1$ the one with $\Lambda_{\mathcal F} = \Lambda_{\mathcal N}$ , and $\mathbb C_{\mathcal F}, \mathbb C_{\mathcal N}, \mathbb C_{\mathcal R}$ the feasibility thresholds ( $c_i = p$ ). With all three schemes available,

e^{-\eta_r\tau} < 1-\rho_r:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_1,\qquad \mathcal N \text{ adopted} \iff \mathbb C_{\mathcal N} < C_s \le \mathbb C_1;

1-\rho_r \le e^{-\eta_r\tau}:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_3,\qquad \mathcal R \text{ adopted} \iff \mathbb C_{\mathcal R} < C_s \le \mathbb C_3.

Milestones

Proposition 2 (p. 6078): recourse factoring is feasible iff $C_s > \mathbb C_{\mathcal F}$ , and then the unique equilibrium solves $p\bar F(q) = c_{\mathcal F}[1+z(q)k(q)]$ , $w = c_{\mathcal F}/\bar F(q)$ .
Proposition 3 (p. 6079): the same for non-recourse factoring with $c_{\mathcal N}$ .
§5.2 (p. 6082, Proposition EC.2): the same for reverse factoring with $c_{\mathcal R}(\tau)$ .
§4.4 (p. 6080, Lemma EC.2): between feasible schemes, the supplier's equilibrium profits are ordered as the $\Lambda_i$ .
Proposition 4 (p. 6080): the choice between $\mathcal F$ and $\mathcal N$ alone.

A follow-on item states Corollary 1(i) (p. 6081): when the retailer's rating is at least the supplier's, non-recourse factoring strictly dominates recourse factoring whenever the latter is feasible.

Significance

Proposition 5 is the paper's main prediction: non-recourse factoring is the choice of medium-rated suppliers, recourse factoring of highly rated ones, and reverse factoring with a fixed payment extension is chosen only by low-to-medium-rated suppliers and only if the retailer's rating is not too high relative to the extension. The paper uses it to explain the documented reluctance of suppliers to join reverse-factoring programs that come with extended payment terms (Wuttke, Rosenzweig and Heese 2019; Corsten 2010, a teaching case), and it is the starting point of the paper's Proposition 6 on the retailer's optimal payment extension, which is the subject of the second mission of this series.

The results are proved in the paper's Online Appendix B. To the best of available knowledge none of them, and no model of supply chain finance, has a machine-checked proof. A formal development would also supply a reusable treatment of the pull wholesale-price game under a strictly IFR demand with an arbitrary effective unit cost, of which Propositions 2, 3 and EC.2 are three instances.

Difficulty

The case analysis of Proposition 5 is short once the milestones are available; the substance lies in them. Proposition 2 requires solving a bilevel problem: the follower's best response has to be identified for every wholesale price, including prices at which the supplier produces nothing, and the leader's objective has to be shown to have a single maximizer. The natural route through the first-order condition needs the IFR property to exclude multiple stationary points, and it has to cope with a support end $\mathbb Z$ that may be finite (where $\bar F$ vanishes and $k$ , $z$ lose meaning) or infinite. Lemma EC.2 requires the equilibrium supplier profit as an explicit function of the effective cost and a monotonicity argument for it; comparing the $\Lambda_i$ directly, without the equilibrium, does not prove it. The proofs themselves are not in the main text.

Formalization scope

Demand is a probability measure μ on ℝ with a density f, the support end Z : EReal, and the complementary distribution function Fbar μ x = μ((x, ∞)). The model data, the coefficients coef, the effective costs cF, cN, cR, the two profit functions, best responses, equilibria, feasibility and adoption are definitions; all theorems are for arbitrary data satisfying Params.Valid and DemandModel. Readings fixed by the formalization:

"Feasible": some wholesale price $w \ge 0$ with a supplier best response gives the retailer strictly positive profit. It is not defined as $c_i < p$ , which is what Propositions 2 and 3 prove.
"Adopted" / "should be adopted": the scheme is feasible and its equilibrium supplier profit is best among the feasible available schemes, with ties resolved $\mathcal R \succ \mathcal N \succ \mathcal F$ , the order forced by the paper's boundaries ( $C_s = \mathbb C_1$ , $C_s = \mathbb C_3$ , $C_r = \mathbb C_2$ ). Profits are compared, not the $\Lambda_i$ .
"The unique value of $C_s$ that satisfies …": a point of $(C_{\min}, C_{\max})$ satisfying the equation and the only such point. The equation $c_{\mathcal F} = p$ is cross-multiplied, $c\,e^{(\eta_s+\lambda_s)t_1} = p\Lambda_{\mathcal F}$ , since $\Lambda_{\mathcal F}$ may be $\le 0$ .
" $C_r > \mathbb C_2$ " is read through the paper's equivalence $\tau > -\eta_r^{-1}\ln(1-\rho_r)$ , i.e. $e^{-\eta_r\tau} < 1-\rho_r$ : the stated assumptions give no single crossing in $C_r$ .
"The unique equilibrium can be derived from …": the equilibrium exists and is unique, and it is exactly the solution of the system with $q \in (0, \mathbb Z)$ ; this part is stated under feasibility.
"Increasing/decreasing" is weak unless stated (p. 6075); $\rho$ is strictly decreasing, $\eta$ weakly.
Continuity of $f$ is read on $[0,\mathbb Z]$ , and $\mathbb Z$ as the upper end of the support.
Additions: wholesale prices are nonnegative; the retailer's reverse-factoring profit is the last line of the p. 6082 display (the middle line has a stray factor $w$ ).
Corollary 1(i): "higher credit rating" is read as $C_r \ge C_s$ , "dominates" as a strictly larger equilibrium supplier profit whenever recourse is feasible.

A formalization in which feasibility or adoption is defined by the inequalities being proved ( $c_i < p$ , largest $\Lambda_i$ ) makes the propositions trivial and is ruled out by the definitions above. The profit functions (7), (10) and the p. 6082 display are taken as the model; the derivation from bank and factor pricing (Eqs. (1), (5), (6), Lemma 1) is not formalized, and the unstated assumptions of Table EC.2 are not included. Contributions of reusable lemmas on $S$ , $k$ and $z$ under strict IFR are welcome.

Selected references

P. Kouvelis and F. Xu, A Supply Chain Theory of Factoring and Reverse Factoring, Management Science 67(10):6071–6088, 2021. https://doi.org/10.1287/mnsc.2020.3788
G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0189
D. A. Wuttke, E. Rosenzweig, H. S. Heese, An Empirical Analysis of Supply Chain Finance Adoption, Journal of Operations Management 65(3):242–261, 2019.
P. Kouvelis and W. Zhao, Who Should Finance the Supply Chain? Impact of Credit Ratings on Supply Chain Decisions, Manufacturing & Service Operations Management 20(1):19–35, 2018.

8 thms1 active userReviewed

Algorithmic Game Theory Operations Research Optimization+1·Captain: mikedeng1

A Supply Chain Theory of Factoring and Reverse Factoring 2: The Retailer's Optimal Reverse Factoring Payment ExtensionResearch Paper

Motivation

Large retailers pay their suppliers weeks or months after delivery, and small suppliers fill the gap with short-term finance. In factoring the supplier sells the receivable to a factor for immediate cash; in reverse factoring the retailer arranges the program with a bank, which pays the supplier early at a rate priced on the retailer's credit rating. Retailers commonly attach a condition: the supplier must accept a longer payment term. Wuttke et al. (Journal of Operations Management, 2019) report that buyers extended payment terms by 54 days on average on adopting reverse factoring and that many suppliers delayed adoption; Corsten (2010) reports suppliers resisting a program because of the demanded payment delay (both as cited by Kouvelis and Xu, pp. 6082–6083). How long an extension a retailer can demand, and what it gains by demanding it, is therefore a practical design question.

Kouvelis and Xu (Management Science 67(10), 2021) answer it inside a Stackelberg supply chain model with credit and liquidity risk. This mission formalizes their answer, Proposition 6 of §5.3: the retailer's optimal payment extension when she keeps the existing wholesale price.

Setting

Demand $D\ge0$ has density $f$ , distribution function $F$ and $\bar F=1-F$ ; $f>0$ on $[0,\mathbb Z]$ with $\mathbb Z\le+\infty$ the upper end of the support, $f$ is continuous there, the mean is finite, and the failure rate $z(\xi)=f(\xi)/\bar F(\xi)$ is strictly increasing. Write $S(q)=\int_0^q\bar F(\xi)\,d\xi$ for expected sales and $k(q)=S(q)/\bar F(q)$ .

A retailer (the leader) sets a wholesale price $w$ , and a capital-constrained supplier (the follower) chooses a production quantity $q\ge0$ ; the retail price $p$ exceeds the unit cost $c$ . Each firm $j\in\{s,r\}$ has a credit rating $C_j\in(C_{\min},C_{\max})$ , a default probability $\rho_j=\rho(C_j)\in[0,1]$ with $\rho$ strictly decreasing, and an interest premium $\eta_j=\eta(C_j)>0$ with $\eta$ decreasing. The lead time is $t_1$ , the payment term $t_2$ , and $\lambda_s,\lambda_r\ge0$ are the liquidity risks.

Under a post-shipment scheme with coefficient $\Lambda$ the supplier earns

\pi(q;w)=(1-\rho_s)\bigl(\Lambda e^{-\lambda_s t_1}wS(q)-c\,q\,e^{\eta_s t_1}\bigr),

with $\Lambda_{\mathcal F}=(1-\rho_r)+(1-\rho_s)-e^{\eta_s t_2}$ (recourse factoring), $\Lambda_{\mathcal N}=e^{-\eta_r t_2}(1-\rho_r)$ (non-recourse factoring) and $\Lambda_{\mathcal R}=e^{-\eta_r(t_2+\tau)}$ (reverse factoring with payment extension $\tau\ge0$ ). The retailer earns $\Pi=e^{-\lambda_s t_1}(1-\rho_r)(p-w)S(q)$ under factoring and

\Pi_{\mathcal R}(w,\tau)=e^{-\lambda_s t_1}(1-\rho_r)(2-e^{-\lambda_r\tau})(p-w)S(q_{\mathcal R})

under reverse factoring, where $q_{\mathcal R}$ is the supplier's best response. Its first-order condition is $w\bar F(q_{\mathcal R})=c_{\mathcal R}(\tau)=c\,e^{(\eta_s+\lambda_s)t_1+\eta_r(t_2+\tau)}$ (Eq. (12)).

Before reverse factoring, the supplier uses the better of the two factoring schemes. By Proposition 4 this is non-recourse, with equilibrium $(w^*_{\mathcal N},q^*_{\mathcal N})$ , when $\mathbb C_{\mathcal N}<C_s\le\mathbb C_1$ , and recourse, with $(w^*_{\mathcal F},q^*_{\mathcal F})$ , when $C_s>\mathbb C_{\mathcal F}\vee\mathbb C_1$ . The retailer keeps the existing wholesale price $w_s$ and solves problem (13): maximize $\Pi_{\mathcal R}(w_s,\tau)$ over $\tau\ge0$ , subject to the supplier's acceptance (his reverse factoring profit is at least his existing one). $\mathbb C^{\max}_{\mathcal R}$ is the rating at which $\Lambda_{\mathcal F}=e^{-\eta_r t_2}$ , and $\Xi_{[0,z]}(x)=\max\{0,\min\{z,x\}\}$ .

Formalization targets

Goal: Proposition 6

(i) If $C_s\ge\mathbb C^{\max}_{\mathcal R}$ , reverse factoring is dominated by recourse factoring. (ii) If $\mathbb C_{\mathcal N}<C_s<\mathbb C^{\max}_{\mathcal R}$ , reverse factoring should be offered with

\tau^*_{\mathcal R}=\Xi_{[0,\tau_s]}(\tau^*_0),\qquad \lambda_r k(q)z(q)+\eta_r=2\eta_r e^{\lambda_r\tau^*_0},\quad w_s\bar F(q)=c_{\mathcal R}(\tau^*_0),

where $\tau_s=-\eta_r^{-1}\ln(1-\rho_r)$ with $w_s=w^*_{\mathcal N}$ in the non-recourse case, and $\tau_s=-\eta_r^{-1}\ln[(1-\rho_r)+(1-\rho_s)-e^{\eta_s t_2}]-t_2$ with $w_s=w^*_{\mathcal F}$ in the recourse case.

Milestones, in attack order

Eq. (12): the supplier's best response under reverse factoring.
Proposition 4: which factoring scheme is in force before reverse factoring.
§5.3, $\tau_s$ : acceptance holds exactly on $[0,\tau_s]$ .
§5.3, $\tau^*_0$ : the retailer's unconstrained profit is unimodal around $\tau^*_0$ .

A follow-on item states Corollary 3(ii): the retailer's profit strictly increases, and the supplier's profit is unchanged when $\tau^*_0\ge\tau_s$ .

Significance

Proposition 6 is the paper's prescription for program design. It says which suppliers should be offered reverse factoring: every supplier below the indifference rating $\mathbb C^{\max}_{\mathcal R}$ and above the non-recourse feasibility threshold. It also gives the extension in closed form, the unconstrained optimum clipped to the supplier's acceptance limit. Two consequences are drawn in the paper: non-recourse factoring is dominated once the extension is optimized, and reverse factoring may leave the supplier exactly as well off as before, so it is not necessarily a win-win (Corollary 3).

The proofs are in the paper's Online Appendix B and have not been machine-checked. A formal proof here produces a checked derivation of the projection formula from the model's primitives. It covers the strict-IFR analysis of the follower's response, the reduction of the acceptance constraint to an interval, and the unimodality of the retailer's objective. The same analysis of the pull game with an effective unit cost recurs across the supply chain finance literature.

Difficulty

The retailer's objective depends on $\tau$ through two opposing channels: the liquidity factor $2-e^{-\lambda_r\tau}$ increases, while expected sales $S(q_{\mathcal R}(\tau))$ decrease because the supplier's effective cost rises. Neither factor is concave in $\tau$ , and the objective need not be concave. The natural move, to set the derivative to zero and call the root a maximum, proves nothing without a sign analysis. That analysis needs the monotonicity of $k\cdot z$ along the implicitly defined response $q_{\mathcal R}(\tau)$ , which is where strict IFR enters. The acceptance constraint compares the supplier's profits in two different games (reverse factoring at $\tau$ against the existing equilibrium). Reducing it to $\tau\le\tau_s$ requires the supplier's best-response profit as an explicit increasing function of his quantity. Identifying the existing equilibrium requires Proposition 4, whose "adopted" compares equilibrium profits of two Stackelberg games.

Formalization scope

The model is a single Lean structure SupplyChainFactoring.Extension.Model. Demand is a probability measure on $\mathbb R$ with a density $f$ , and $\mathbb Z$ is an extended real. "Continuous p.d.f. with $f>0$ in $[0,\mathbb Z]$ " is read as continuity on $[0,\mathbb Z]$ , with $f=0$ outside the support. Credit functions $\rho,\eta$ are real functions constrained on $(C_{\min},C_{\max})$ . The finance derivations behind the profit functions (Eqs. (1), (5), (6), Lemma 1) are not formalized: the profit functions are the model.

Readings of informal words, each also recorded in the item's Formalization Note:

Best response: a maximizer of the supplier's profit over $q\ge0$ ; equilibrium: a best response pair from which no nonnegative wholesale price with a best response gives the retailer more. Neither is defined through first-order conditions.
Feasible: some $w\ge0$ with a best response gives the retailer positive profit; adopted (Proposition 4): feasible, with equilibrium supplier profit at least (non-recourse) or strictly above (recourse) the other feasible scheme's.
Thresholds "the unique value of $C_s$ that satisfies …" are hypotheses in exactly that form; $c_{\mathcal N}=p$ and $c_{\mathcal F}=p$ are cross-multiplied because $\Lambda_{\mathcal F}$ can be $\le0$ .
In (13) $w$ is fixed at $w_s$ (§5.3's first sentence, footnote 23). $\pi^*_{\mathcal R}$ is the supplier's best-response profit under reverse factoring at $(w_s,\tau)$ , and $\max\{\pi^*_{\mathcal F},\pi^*_{\mathcal N}\}$ is his profit in the existing equilibrium.
Dominated (Proposition 6(i)): at every $\tau\ge0$ and every $w$ , the supplier's reverse factoring best-response profit is at most his recourse one. Should be offered (6(ii)): $\tau^*_{\mathcal R}$ solves (13) and the retailer's profit is at least her existing equilibrium profit.
$\tau^*_0$ is a hypothesis: it and some $q\in(0,\mathbb Z)$ solve the paper's two equations (the paper does not argue existence). Its optimality "without the nonnegativity constraint" is stated as unimodality of $\Pi_{\mathcal R}$ on the set of real $\tau$ with $c_{\mathcal R}(\tau)<w$ .
Always increases (Corollary 3(ii)) is strict; may remain unchanged when $\tau^*_0\ge\tau_s$ is read as "is unchanged whenever $\tau^*_0\ge\tau_s$ ".

Three misprints of the paper are corrected: $\Xi_{[0,z]}(x)=0$ "if $x<z$ " is read as "if $x<0$ "; "the retailer's maximization problem in (16)" refers to (13); the middle line of the $\Pi_{\mathcal R}$ display on p. 6082 carries a stray factor $w$ , and the last line is used.

The hypotheses on $\tau^*_0$ cannot be met when $\lambda_r=0$ , and the goal then says nothing about the case, as in the paper. The existing equilibrium, $\tau_s$ and $\tau^*_0$ are never free parameters: $\tau_s$ is the paper's explicit formula, and the reduction of acceptance to $\tau\le\tau_s$ is a milestone to be proved, not an assumption. Every logarithm is applied to a quantity the hypotheses force positive. A formalization that assumed acceptance equivalent to $\tau\le\tau_s$ or assumed unimodality would be trivial and is excluded.

The pull game with an effective cost has the same structure as Cachon's pull contract without salvage value (platform items CachonPushPull.*), but those items assume IGFR demand with a salvage value, so they are not reused. Reusable infrastructure welcome: the strict-IFR lemmas ( $k$ , $k\cdot z$ and $k(q)-q$ increasing) and the explicit best response of a newsvendor-type follower.

Selected references

P. Kouvelis, F. Xu, A Supply Chain Theory of Factoring and Reverse Factoring, Management Science 67(10):6071–6088, 2021. https://doi.org/10.1287/mnsc.2020.3788
G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
D. A. Wuttke, E. S. Rosenzweig, H. S. Heese, An Empirical Analysis of Supply Chain Finance Adoption, Journal of Operations Management 65(3):242–261, 2019. https://doi.org/10.1002/joom.1023

6 thms3 active usersReviewed

Completed

Graph Theory Operations Research Optimization+1·Captain: mikedeng1

A New Approach to the Maximum-Flow Problem 1: The Generic Push-Relabel Algorithm and Its Operation BoundResearch Paper

Motivation

The maximum-flow problem asks how much of a commodity can be sent from a source to a sink through a network whose edges have capacities. It is a basic model in operations research (transportation, scheduling, bipartite matching) and a standard subroutine in combinatorial optimization.

Classical algorithms, from Ford and Fulkerson (1956) through Edmonds–Karp and Dinic (1970–1972) and Karzanov (1974), increase a feasible flow along augmenting paths or blocking flows. Goldberg and Tarjan, A New Approach to the Maximum-Flow Problem (J. ACM 35(4), 1988, doi:10.1145/48014.61051), replaced this global view by a local one: the push-relabel method maintains a preflow, which may violate conservation at intermediate vertices, and moves excess along edges toward vertices with smaller distance labels. The generic method, with the basic operations applied in any order, is the starting point of the FIFO, highest-label and dynamic-tree implementations analysed later in the same paper, and push-relabel codes remain among the fastest practical maximum-flow solvers.

This mission formalizes §2–§3 of the paper: the generic algorithm is correct, and it stops after a number of basic operations bounded by an explicit polynomial in the numbers of vertices and edges, whatever order of operations is chosen.

Setting

A flow network has a finite vertex set $V$ with $n = |V|$ , a source $s$ and a sink $t \ne s$ , and a capacity $c(v,w) \ge 0$ for every ordered pair of vertices, positive exactly on the edges $E = \{(v,w) : c(v,w) > 0\}$ ; $m = |E|$ , and there are no loops, $c(v,v) = 0$ .

Flows are real functions on all vertex pairs. A function $f$ satisfies the capacity constraint if $f(v,w) \le c(v,w)$ and antisymmetry if $f(v,w) = -f(w,v)$ for all pairs. The excess of $v$ is $e(v) = \sum_{u} f(u,v)$ . A flow also has $e(v) = 0$ for $v \notin \{s,t\}$ ; a preflow only $e(v) \ge 0$ for $v \ne s$ . The value of a flow is $|f| = \sum_v f(v,t)$ , and a maximum flow is a flow of maximum value.

The residual capacity is $r_f(v,w) = c(v,w) - f(v,w)$ ; pairs with $r_f(v,w) > 0$ are the edges of the residual graph $G_f$ . A valid labeling is $d : V \to \mathbb{N} \cup \{\infty\}$ with $d(s) = n$ , $d(t) = 0$ and $d(v) \le d(w) + 1$ on every residual edge. A vertex $v$ is active if $v \notin \{s,t\}$ , $d(v) < \infty$ and $e(v) > 0$ .

The two basic operations (Fig. 1 of the paper) are:

Push $(v,w)$ , applicable when $v$ is active, $r_f(v,w) > 0$ and $d(v) = d(w)+1$ : send $\delta = \min(e(v), r_f(v,w))$ , i.e. $f(v,w) \mathrel{+}= \delta$ , $f(w,v) \mathrel{-}= \delta$ . It is saturating if $r_f(v,w) = 0$ afterwards and nonsaturating otherwise.
Relabel $(v)$ , applicable when $v$ is active and $d(v) \le d(w)$ for every residual edge $(v,w)$ : set $d(v) \leftarrow \min\{d(w)+1 : (v,w) \in E_f\}$ ( $\infty$ if there is none).

The generic algorithm (Fig. 2) starts from the preflow that saturates every edge leaving $s$ and is zero elsewhere, with the simple labeling $d(s) = n$ , $d(v) = 0$ otherwise, and applies applicable basic operations in any order while one exists. An execution with $K$ basic operations is a sequence of states $(f_0,d_0),\dots,(f_K,d_K)$ from the initial state, each obtained from the previous one by one applicable operation.

Formalization targets

Goal: Theorems 3.11 and 3.4

Assume the paper's standing assumption $m \ge n-1$ . For every execution with $K$ basic operations,

K \le (2n-1)(n-2) + 2nm + 4n^2 m,

and if no basic operation applies in the final state, then $f_K$ is a maximum flow. The paper states the bound as $O(n^2m)$ and proves it as "immediate from Lemmas 3.8, 3.9, and 3.10"; the goal states the sum of those three printed bounds. Since every execution is this short, no order of operations runs forever.

Milestones

In the order the proof uses them: Lemma 2.1 (at an active vertex a push or a relabel applies); Lemma 3.1 (the labeling stays valid); Theorem 3.2 (Ford–Fulkerson: a flow is maximum iff $t$ is unreachable from $s$ in $G_f$ ); Lemma 3.3 (under a valid labeling $t$ is unreachable from $s$ ); Lemma 3.5 (from any vertex with positive excess, $s$ is reachable); Lemma 3.6 (labels never decrease; a relabeling increases the label); Lemma 3.7 ( $d(v) \le 2n-1$ throughout); Theorem 3.4 (termination with finite labels gives a maximum flow); Lemma 3.8 ( $\le 2n-1$ relabelings per vertex, $\le (2n-1)(n-2) < 2n^2$ in total); Lemma 3.9 ( $\le 2nm$ saturating pushes); Lemma 3.10 ( $\le 4n^2m$ nonsaturating pushes, under $m \ge n-1$ ). A further, non-milestone item states the unnumbered invariant that every $f_k$ is a preflow.

Significance

The generic bound shows that push-relabel terminates in a polynomial number of steps without any rule for choosing the next operation; the specific orderings of §4–§5 of the paper (first-in first-out, $O(n^3)$ ; dynamic trees, $O(nm\log(n^2/m))$ ) refine only the count of nonsaturating pushes, and reuse Lemmas 3.1–3.9 unchanged. The correctness argument, a valid labeling excludes augmenting paths, is the template for the push-relabel minimum-cost flow and assignment algorithms that followed.

These results are proved in the paper and are textbook material. Their machine-checked counterparts are, as far as is known here, not on the Prove2Me platform: the platform's network-flow statements (from Introduction to Linear Optimization, e.g. LinearOptimization.max_flow_min_cut) use a different model, with arc-indexed nonnegative flows and extended-real capacities, and contain nothing about preflows, labels or operation counts. This mission produces a formal account of the antisymmetric-flow model, of Ford–Fulkerson in that model, and of the amortized counting arguments, with the constants the paper prints.

Difficulty

The correctness half is short once the invariants are in place; the difficulty is in the counting. The label bound (Lemma 3.7) is a statement about the whole execution, and it depends on a structural fact about preflows (Lemma 3.5) whose truth rests on antisymmetry and on the nonnegativity of excesses. The obvious first idea for the push counts, bounding pushes per edge or per vertex locally, fails for nonsaturating pushes: flow pushed across a pair can be pushed back later, and nothing local limits how often this happens, so Lemma 3.10 holds only as an amortized statement over the entire execution and depends on both earlier counts. Saturating pushes on a pair can also recur, in both directions, and Lemma 3.9 has to control the interaction between the two directions.

Formally, all of this is reasoning about arbitrary interleavings of operations, with labels in $\mathbb{N} \cup \{\infty\}$ and real-valued flows.

Formalization scope

Vertices form a finite type with decidable equality; $n$ is its cardinality, $s \ne t$ , so $n \ge 2$ and the natural-number subtractions $2n-1$ and $n-2$ are exact. Capacities are a real function on all pairs, nonnegative, zero on the diagonal; $E$ is its support and $m$ its cardinality.
Flows and preflows are antisymmetric real functions on all pairs (not nonnegative arc flows); the excess is computed from $f$ , never stored. A maximum flow is a flow whose value is at least that of every flow.
Labels live in ℕ∞, with $\infty + 1 = \infty$ ; the relabel value is an infimum, which is $\infty$ on the empty set.
An execution is a sequence of states σ : ℕ → State V with a length $K$ , starting at the Fig. 2 state with the simple labeling (the paper's own assumption for its proofs), each step an applicable push or relabel. "Terminates" means that no basic operation applies, the loop guard of Fig. 2. The three counts are cardinalities of the sets of step indices of each kind.
Explicit constants: $2n-1$ per-vertex relabelings, $(2n-1)(n-2) < 2n^2$ total relabelings, $2nm$ saturating pushes, $4n^2m$ nonsaturating pushes, label bound $2n-1$ , and the total $(2n-1)(n-2)+2nm+4n^2m$ . The standing assumption $m \ge n-1$ appears only on Lemma 3.10 and the goal.
A trivializing formalization is ruled out: the step relation fixes the pushed amount $\delta = \min(e(v), r_f(v,w))$ and the new label exactly as in Fig. 1, termination is the loop guard rather than "the result is a flow", and a sorry-free check exhibits a concrete network $s \to a \to t$ with a two-step execution (relabel $a$ , then push $(a,t)$ ), so the run hypotheses are satisfiable.

Welcome contributions: proofs of the invariants (preflow, valid labeling, label monotonicity), of Ford–Fulkerson for antisymmetric flows (reusable beyond this mission), and of the counting lemmas. The FIFO bound of §4 is the subject of a companion mission.

Selected references

A. V. Goldberg, R. E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4):921–940, 1988. doi:10.1145/48014.61051
L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, Journal of the ACM 19(2):248–264, 1972. doi:10.1145/321694.321699
R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows: Theory, Algorithms, and Applications, Prentice Hall, 1993.

17 thms3 active usersReviewed

Completed

Graph Theory Operations Research Optimization+1·Captain: mikedeng1

A New Approach to the Maximum-Flow Problem 2: The Nonsaturating-Push Bound for FIFO Push-RelabelResearch Paper

Motivation

The maximum-flow problem asks how much of a commodity can be sent from a source to a sink through a network whose edges carry capacities. It is a basic model of operations research. Transportation, scheduling, bipartite matching and image segmentation reduce to it, and it is the inner step of many combinatorial algorithms.

Goldberg and Tarjan introduced the push–relabel (preflow) method in A New Approach to the Maximum-Flow Problem (J. ACM 35(4), 1988). Ford–Fulkerson-type algorithms augment along whole source–sink paths. The push–relabel method instead moves excess flow across single edges, guided by integer distance labels on the vertices. Whatever order its local operations are applied in, it is correct and performs $O(n^2 m)$ of them (§3 of the paper). Section 4 shows that one particular order, processing the active vertices first-in, first-out, cuts the dominant term, the number of nonsaturating pushes, to $O(n^3)$ . The method and its FIFO and highest-label variants are the standard practical maximum-flow codes.

Timeline:

1956: Ford and Fulkerson, augmenting paths and max-flow min-cut.
1970–72: Dinic, and Edmonds and Karp, give polynomial augmenting-path bounds.
1974: Karzanov introduces preflows and obtains $O(n^3)$ .
1982: Shiloach and Vishkin give a parallel $O(n^2 \log n)$ preflow algorithm with a first-in, first-out flavour.
1988: Goldberg and Tarjan, the generic push–relabel method, the FIFO bound of this mission, and $O(nm \log(n^2/m))$ with dynamic trees.

Setting

A flow network has a finite vertex set $V$ with $n = |V|$ , a capacity $c(v,w) \ge 0$ on every ordered pair, a source $s$ and a sink $t \neq s$ . The edges are the pairs with $c(v,w) > 0$ , and there are no loops. A preflow is a function $f$ on vertex pairs with $f(v,w) \le c(v,w)$ and $f(v,w) = -f(w,v)$ . Its excess $e(v) = \sum_u f(u,v)$ must be nonnegative at every $v \neq s$ . The residual capacity is $r_f(v,w) = c(v,w) - f(v,w)$ . A labeling $d$ assigns each vertex a value in $\mathbb{N} \cup \{\infty\}$ . A vertex $v \notin \{s,t\}$ is active if $d(v) < \infty$ and $e(v) > 0$ .

The two basic operations (Fig. 1 of the paper) are:

push $(v,w)$ , applicable when $v$ is active, $r_f(v,w) > 0$ and $d(v) = d(w)+1$ . It sends $\delta = \min(e(v), r_f(v,w))$ from $v$ to $w$ . The push is saturating if $r_f(v,w) = 0$ afterwards and nonsaturating otherwise.
relabel $(v)$ , applicable when $v$ is active and $d(v) \le d(w)$ for every residual edge $(v,w)$ . It sets $d(v) \leftarrow \min\{d(w)+1 : r_f(v,w) > 0\}$ .

The algorithm starts by saturating every edge leaving $s$ , with $d(s) = n$ and $d(v) = 0$ for $v \neq s$ .

In the first-in, first-out algorithm (§4), each vertex $v$ scans a fixed list $L(v)$ of its neighbours through a current edge. The push/relabel $(v)$ operation pushes through the current edge if possible. Otherwise it advances the current edge, or, at the end of the list, returns to the first edge and relabels $v$ . Active vertices wait in a queue $Q$ , initially $\{v \in V - \{s,t\} : c(s,v) > 0\}$ . The discharge operation removes the front vertex $v$ and repeats push/relabel $(v)$ until $e(v) = 0$ or $d(v)$ increases. Every vertex that becomes active meanwhile is appended to $Q$ , and $v$ is appended too if it is still active. Passes over the queue are defined inductively. Pass 1 consists of the discharges of the initially queued vertices. Pass $i+1$ consists of the discharges of vertices added during pass $i$ .

Formalization targets

Goal: Corollary 4.4 (p. 931)

For every network, every edge-list order, every initial queue order, and every run of the FIFO algorithm,

\#\{\text{nonsaturating pushes}\} \le 4n^3 .

The constant is the printed one.

Milestones

Lemma 4.1 (p. 929): the push/relabel operation relabels only when relabeling is applicable.
Lemma 3.5 (p. 926): from any vertex with positive excess, the source is reachable in the residual graph.
Lemma 3.7 (p. 927): at any time, $d(v) \le 2n-1$ for every vertex.
Lemma 3.8 (p. 927): at most $2n-1$ relabelings per vertex and at most $(2n-1)(n-2) < 2n^2$ in total.
Lemma 4.3 (p. 930): at most $4n^2$ passes over the queue.

Significance

Corollary 4.4 is the combinatorial core of Theorem 4.5, which states that the FIFO algorithm runs in $O(n^3)$ time. Theorem 4.2 shows that the remaining work of the implementation is $O(nm)$ plus constant time per nonsaturating push. The bound of Corollary 4.4 is therefore what separates the $O(n^3)$ FIFO method from the $O(n^2 m)$ bound of the generic method, which matters on dense networks. The same pass-counting argument is reused for the parallel algorithm of §6 and underlies later analyses of highest-label and wave variants.

The results are proved in the paper. Formalizing them adds an analysis of a push–relabel algorithm, which the platform does not yet have. Its existing network-flow material states max-flow min-cut and Ford–Fulkerson termination in an arc-based model with nonnegative flows (the Introduction to Linear Optimization missions). The mission builds a precise operational model of the FIFO implementation, with edge lists, current edges and a queue carrying pass numbers, and states an explicit operation count for it. A companion mission in this series treats the generic algorithm's correctness and its $(2n-1)(n-2) + 2nm + 4n^2m$ operation bound.

Difficulty

The obvious argument is the potential-function count of §3, over the sum of the labels of active vertices. It yields only $4n^2 m$ and does not use the queue discipline at all. The $4n^3$ bound has to charge nonsaturating pushes to passes over the queue, and then bound the number of passes by the total growth of the labels. Neither step is visible in the generic algorithm, because both depend on the order in which vertices are processed.

Making this rigorous requires invariants of the implementation that the paper uses silently:

a vertex is in the queue exactly when it is active, and at most once;
pass numbers are nondecreasing along the queue;
current edges only move forward between relabelings.

Lemma 4.1 in particular depends on the current-edge scan: an edge passed over earlier stays inadmissible until $v$ is relabeled.

Formalization scope

The Lean development works in namespace GoldbergTarjan.FIFO. Vertices form a type V with [Fintype V] [DecidableEq V], and $n$ is Fintype.card V. Capacities are c : V → V → ℝ with c ≥ 0 and c v v = 0. Flows are antisymmetric real functions on all ordered pairs, not nonnegative arc flows. Excess is computed from the flow. Labels are in ℕ∞, and the empty minimum in relabel is ⊤.

The state of the algorithm consists of the flow, the labels, the current-edge index cur v into the edge list L v, and the queue Q : List (V × ℕ), each entry tagged with its pass number. Push/relabel (Fig. 3) is a total function, and a discharge (Fig. 4) is a relation carrying the number of push/relabel operations it performs. A run consists of the states S 0, …, S K with S 0 the initial state and consecutive states related by one discharge. The printed variant of Fig. 4, which stops as soon as $v$ is relabeled, is the one formalized. Counts are natural numbers over all push/relabel operations of all discharges. The number of passes is the largest pass tag of a discharged entry.

All constants are explicit, exactly as printed:

$2n-1$ (Lemmas 3.7, 3.8);
$(2n-1)(n-2)$ and $2n^2$ (Lemma 3.8);
$4n^2$ (Lemma 4.3);
$4n^3$ (Corollary 4.4).

No asymptotic notation is used, and no $m \ge n-1$ assumption is made.

A model without current edges, where relabeling happens whenever no push applies, would make Lemma 4.1 vacuous and change the algorithm. Pass numbers that are not propagated by the "added during pass $i$ " rule would make the pass count arbitrary. Both are ruled out by the definitions. A sorry-free check, outside the proposal, exhibits a three-vertex network with two legal discharges, two passes and no nonsaturating push, so the run hypotheses are satisfiable.

Reusable beyond this mission are the network, preflow, push and relabel definitions and Lemma 3.5, which is about an arbitrary preflow. Contributions welcome: invariants of FIFO runs (preflow, valid labeling, queue = active set, cur within bounds), proofs of the milestones, and the reduction of Corollary 4.4 to Lemma 4.3.

Selected references

A. V. Goldberg, R. E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4):921–940, 1988. https://doi.org/10.1145/48014.61051
A. V. Karzanov, Determining the maximal flow in a network by the method of preflows, Soviet Math. Doklady 15:434–437, 1974.
Y. Shiloach, U. Vishkin, An O(n² log n) parallel max-flow algorithm, Journal of Algorithms 3(2):128–146, 1982. https://doi.org/10.1016/0196-6774(82)90013-X
L. R. Ford, D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5
J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, Journal of the ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699

10 thms3 active usersReviewed

The OR Formalization Drive

Missions

Robust Solutions to Least-Squares Problems with Uncertain Data IV: A Semidefinite Upper Bound on the Linear-Fractional Worst-Case Residual, Exact for Full PerturbationsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.2 (corrected)

Milestones

Significance

Difficulty

Formalization scope

Selected references

An Application of Simultaneous Diophantine Approximation in Combinatorial Optimization: A Small Integral Objective with the Same Optimal Solutions and Dual BasesResearch Paper

Motivation

Setting

Formalization targets

Goal — Theorem 4.2 (p. 58)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Lifts of Convex Sets and Cone Factorizations I: A Proper K-Lift of a Convex Body Yields a K-Factorization of Its Slack Operator, and a K-Factorization Yields a K-LiftResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Validation of Subgradient Optimization I: The Core Problem Built from the Subgradient Iterates Solves the Dual Linear ProgramResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.3 (p. 82)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Integrating Replenishment Decisions with Advance Demand Information I: The Myopic Order-Up-To Level Is Optimal When Observed Demand Beyond the Protection Period Is LargeResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 1350)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Validation of Subgradient Optimization II: A Unique Optimal Assignment Makes the Dual Optimal Set Full-DimensionalResearch Paper

Why the assignment dual matters

Setting

Formalization targets

Goal: Theorem 3.1 (p. 70)

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Integrating Replenishment Decisions with Advance Demand Information II: With Zero Set-up Cost the Myopic Base-Stock Policy Is Optimal When Myopic Levels Are NondecreasingResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5 (p. 1352)

Milestones: Theorem 4 (p. 1351)

Significance

Difficulty

Formalization scope

Selected references

Robust Solutions to Uncertain Semidefinite Programs I: Exact SDP Reformulation of the Robust LMI under Full Linear-Fractional PerturbationsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.1 (p. 36), as a set identity

Milestones

Significance

Difficulty