Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.99942Formalized record

2 provers on it1 of 1 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.606309Formalized record

6 provers on it7 of 7 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 87Formalized record

3 provers on it5 of 5 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 85Formalized record≤ 5Open frontier

35 provers on it10 of 12 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.37134Formalized record≤ 2.371177Open frontier

16 provers on it7 of 8 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.99942Formalized record

2 provers on it1 of 1 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.606309Formalized record

6 provers on it7 of 7 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 87Formalized record

3 provers on it5 of 5 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 85Formalized record≤ 5Open frontier

35 provers on it10 of 12 missions formalized

Matrix multiplication exponent

≤ 2.37134Formalized record≤ 2.371177Open frontier

16 provers on it7 of 8 missions formalized

All missions

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

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

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

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 algebra Numerical Analysis+2·Captain: mikedeng1

Robust Solutions to Least-Squares Problems with Uncertain Data III: Structured Robust Least Squares Is Solved Exactly by a Semidefinite ProgramResearch Paper

Motivation

Least squares fits a model $Ax \approx b$ as if the data $(A, b)$ were exact. In practice they are measured, rounded or estimated, and the least-squares solution can be very sensitive to such errors. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed to treat the errors as deterministic, unknown but bounded, and to choose $x$ minimizing the worst-case residual over all admissible data. For unstructured perturbations of $[A\ b]$ bounded in Frobenius norm this leads to a second-order cone program (missions I and II of this series).

In many applications the perturbations have a known structure: a Toeplitz matrix stays Toeplitz, a parameter enters several entries at once, or only some entries are uncertain. An unstructured bound then over-estimates the worst case. The paper's §4 treats perturbations that are affine in a parameter vector $\delta$ bounded in Euclidean norm, and shows that the resulting structured robust least-squares (SRLS) problem is still solved exactly, now by a semidefinite program (SDP). This model of uncertainty (an ellipsoid of affinely parametrized data) is the one later adopted as the basic uncertainty set of robust optimization; see Ben-Tal and Nemirovski, Math. Oper. Res. 23(4), 1998.

Setting

Vectors carry the Euclidean norm $\|v\| = \sqrt{v^Tv}$ . Given matrices $A_0, A_1, \dots, A_p \in \mathbb{R}^{n\times m}$ and vectors $b_0, b_1, \dots, b_p \in \mathbb{R}^n$ , define for every $\delta \in \mathbb{R}^p$

\mathbf A(\delta) = A_0 + \sum_{i=1}^p \delta_i A_i, \qquad \mathbf b(\delta) = b_0 + \sum_{i=1}^p \delta_i b_i .

For $\rho \ge 0$ and $x \in \mathbb{R}^m$ the structured worst-case residual is

r_S(\mathbf A, \mathbf b, \rho, x) = \max_{\|\delta\| \le \rho} \|\mathbf A(\delta)x - \mathbf b(\delta)\|,

and $x$ is an SRLS solution if it minimizes $r_S(\mathbf A, \mathbf b, \rho, \cdot)$ over $\mathbb{R}^m$ . The paper takes $\rho = 1$ throughout §4 and writes $r_S(\mathbf A, \mathbf b, x)$ .

For fixed $x$ let $M(x) = [A_1x - b_1\ \cdots\ A_px - b_p] \in \mathbb{R}^{n\times p}$ and

F = M(x)^TM(x), \qquad g = M(x)^T(A_0x - b_0), \qquad h = \|A_0x - b_0\|^2 .

Since $\mathbf A(\delta)x - \mathbf b(\delta) = (A_0x - b_0) + M(x)\delta$ , the squared residual at $\delta$ is the quadratic function $h + 2g^T\delta + \delta^TF\delta$ . Finally, for scalars $\lambda, \tau$ ,

\mathcal F(\lambda, \tau) = \begin{bmatrix} \lambda - \tau - h & -g^T \\ -g & \tau I - F \end{bmatrix}.

Formalization targets

Goal: Theorem 4.2

With $p \ge 1$ and $\rho = 1$ , consider the SDP in $(\lambda, \tau, x)$

\text{minimize } \lambda \quad \text{subject to} \quad \begin{bmatrix} \lambda - \tau & 0 & (A_0x - b_0)^T \\ 0 & \tau I & M(x)^T \\ A_0x - b_0 & M(x) & I \end{bmatrix} \succeq 0. \tag{32}

The goal states that (a) for all $x$ and $\lambda$ , some $\tau$ makes $(\lambda, \tau, x)$ feasible if and only if $r_S(\mathbf A, \mathbf b, x)^2 \le \lambda$ ; and (b) $(\lambda, \tau, x)$ is optimal for (32) if and only if $x$ is an SRLS solution, $\lambda = r_S(\mathbf A, \mathbf b, x)^2$ , and $(\lambda, \tau, x)$ is feasible. This is the precise content of the paper's "the SRLS can be solved by computing an optimal solution of (32)".

Milestones

Lemma 2.1 (S-procedure), in two items: the multiplier condition is sufficient for every $p$ ; for $p = 1$ it is also necessary when $F_1(\zeta_0) > 0$ for some $\zeta_0$ .
Eq. (28): $r_S(\mathbf A, \mathbf b, x)^2 = \max_{\delta^T\delta \le 1} [1;\delta]^T \begin{bmatrix} h & g^T \\ g & F\end{bmatrix} [1;\delta]$ .
Eq. (29): for $\lambda \ge 0$ , that quadratic form is $\le \lambda$ on the unit ball if and only if $\mathcal F(\lambda, \tau) \succeq 0$ for some $\tau$ .
Theorem 4.1, first assertion: $r_S(\mathbf A, \mathbf b, x)^2 = \min\{\lambda : \exists \tau,\ \mathcal F(\lambda, \tau) \succeq 0\}$ , the minimum attained.
§4.2, Schur-complement step: the matrix of (32) is positive semidefinite if and only if $\mathcal F(\lambda, \tau)$ is.

Significance

The result shows that a min–max problem over a nonconvex worst case (the inner problem maximizes a convex quadratic over a ball) is equivalent to a single convex SDP whose size is linear in $n$ , $m$ and $p$ , and hence solvable in polynomial time by interior-point methods. It covers as special cases the unstructured problem of §3, least squares with uncertainty in selected entries, and Toeplitz or otherwise patterned perturbations. The exactness contrasts with the next section of the paper, where the linear-fractional and $\ell_\infty$ -bounded versions are in general only bounded from above, or shown NP-hard.

The result is proved in the paper; to the best of current knowledge it has not been formalized. The platform already has the one-constraint S-procedure (ConvexOptimization.s_procedure, proved, in a different sign and block convention); this mission adds the robust least-squares objects, the reduction to the S-procedure, the Schur-complement step, and the optimal-solution correspondence of Theorem 4.2. The worst-case residual and SDP (32) definitions are reusable by later robust-regression missions.

Difficulty

The obvious approach is to compute the inner maximum directly. The function $\delta \mapsto h + 2g^T\delta + \delta^TF\delta$ is convex, so its maximum over the unit ball is attained on the boundary, but it is not given by any closed-form expression in general, and maximizing a convex function is not a convex problem. Exactness therefore rests on the lossless S-procedure for one quadratic constraint, a nonconvex duality statement that fails for two or more constraints; the sufficient direction alone only yields an upper bound.

A second point is passing from "for fixed $x$ " (Theorem 4.1) to "optimal over $x$ " (Theorem 4.2): $\mathcal F(\lambda, \tau)$ is quadratic in $x$ , and only the Schur-complement lift (32) is jointly affine in $(\lambda, \tau, x)$ . The correspondence of optimal solutions must then be checked in both directions, including that the optimal $\lambda$ is the squared residual and not the residual.

Formalization scope

Data are A0 : Matrix (Fin n) (Fin m) ℝ, A : Fin p → Matrix (Fin n) (Fin m) ℝ, b0 : Fin n → ℝ, b : Fin p → Fin n → ℝ; A i is the paper's $A_{i+1}$ (0-based index). Vectors live in Fin k → ℝ with the Euclidean norm written out as $\sqrt{\sum_i v_i^2}$ , never Mathlib's sup norm.
The maximum defining $r_S$ is sSup of the set of attained residuals over the closed ball; for $\rho \ge 0$ this set is nonempty and bounded, so sSup is the true maximum. The theorems use $\rho = 1$ , as the paper does; the paper derives general $\rho$ by scaling and that is not stated here.
Block matrices are Matrix.fromBlocks in the printed order (scalar block first: Unit ⊕ Fin p; for (32), (Unit ⊕ Fin p) ⊕ Fin n). " $\succeq 0$ " is Mathlib's PosSemidef, which includes symmetry; all matrices here are symmetric by construction.
$p \ge 1$ is assumed in (29), Theorem 4.1 and Theorem 4.2, although the paper does not state it: for $p = 0$ the block $\tau I$ is empty, $\tau$ is unconstrained, every $\lambda$ is feasible and both SDPs lose their meaning. Eq. (28), Lemma 2.1 and the Schur-complement step hold for every $p$ and are stated without it.
Optimality in (32) is stated as feasibility plus $\lambda \le \lambda'$ for every feasible $(\lambda', \tau', x')$ . A formalization that only proves existence of some feasible $\tau$ , or only an inequality between the optimal values, is weaker than Theorem 4.2 and does not close the goal.
Theorem 4.1's second and third assertions (the one-dimensional reformulation (30)–(31) and the worst-case perturbation) are not included: they use the notion " $(F, g)$ -controllable", which the paper does not define.
Useful infrastructure: Mathlib's Schur-complement lemmas (Matrix.PosSemidef.fromBlocks₂₂ and relatives in LinearAlgebra.Matrix.SchurComplement); the platform's ConvexOptimization.s_procedure and ConvexOptimization.single_constraint_quadratic_strong_duality with their definitions ConvexOptimization_quadraticForms, included as reference items. A bridge lemma between the platform's block convention and this mission's is a welcome contribution, as is a general- $\rho$ version.

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 (the S-procedure, p. 24). https://doi.org/10.1137/1.9781611970777
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
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

11 thms3 active usersReviewed

Completed

Convex Optimization Linear algebra Numerical Analysis+2·Captain: mikedeng1

Robust Solutions to Least-Squares Problems with Uncertain Data I: The Worst-Case Residual and Its Unique MinimizerResearch Paper

Motivation

The least-squares (LS) problem $\min_x \|Ax - b\|$ assumes that the data $A \in \mathbb{R}^{n\times m}$ , $b \in \mathbb{R}^n$ are exact. In applications they rarely are: they come from measurements, from linearizations, or from models with neglected dynamics. A classical response is sensitivity analysis or regularization (Tikhonov), where a weight trades the size of the solution against the fit, and the choice of that weight is left to the user. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) take a deterministic view instead: the true data lie in a known ball around $(A, b)$ , and the solution should minimize the residual it can be forced to have in the worst case over that ball. The paper shows that this robust least-squares (RLS) problem is solvable exactly, in the unstructured case by a second-order cone program (SOCP). The same worst-case idea, applied to regression, underlies the later equivalence between robustness and regularization (Xu, Caramanis and Mannor, 2009) and is a standard entry point to robust optimization (Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization, 2009).

This mission formalizes the first main result of the paper, Theorem 3.1: the worst-case residual has a closed form, its minimizer is unique, and minimizing it is an SOCP.

Setting

Vectors carry the Euclidean norm $\|v\| = (\sum_i v_i^2)^{1/2}$ . For a matrix $X$ , $\|X\|_F = (\sum_{i,j} X_{ij}^2)^{1/2}$ is the Frobenius norm and $\|X\|$ the largest singular value, i.e. the smallest $c \ge 0$ with $\|Xv\| \le c\|v\|$ for all $v$ .

Fix $A \in \mathbb{R}^{n\times m}$ and $b \in \mathbb{R}^n$ . A perturbation is a pair $\Delta A \in \mathbb{R}^{n\times m}$ , $\Delta b \in \mathbb{R}^n$ , collected in the augmented matrix $\Delta = [\Delta A\ \Delta b] \in \mathbb{R}^{n\times(m+1)}$ . For a bound $\rho \ge 0$ and $x \in \mathbb{R}^m$ , the worst-case residual is (paper, eq. (1))

r(A,b,\rho,x) = \max_{\|[\Delta A\ \Delta b]\|_F \le \rho} \|(A+\Delta A)x - (b+\Delta b)\|,

and $x$ is an RLS solution if it minimizes $r(A,b,\rho,\cdot)$ . The bound constrains the augmented matrix jointly, not $\Delta A$ and $\Delta b$ separately. The paper normalizes $\rho = 1$ and writes $r(A,b,x) = r(A,b,1,x)$ . Finally, $[x;1] \in \mathbb{R}^{m+1}$ denotes $x$ stacked over $1$ . In the Lean development these are RobustLS.Unstructured.eucNorm, frobNorm, specNorm, augment, stackOne, worstCaseResidual A b ρ x, its largest-singular-value variant worstCaseResidualSpec, and the SOCP constraint predicate SocpFeasible A b x λ τ.

Formalization targets

Goal: Theorem 3.1 (p. 1040)

For $n \ge 1$ , every $A$ , $b$ :

r(A,b,x) = \|Ax-b\| + \sqrt{\|x\|^2+1} \quad \text{for all } x \in \mathbb{R}^m,

the problem $\min_{x \in \mathbb{R}^m} r(A,b,x)$ has exactly one solution $x_{\mathrm{RLS}}$ , and it is the SOCP

\text{minimize } \lambda \quad\text{subject to}\quad \|Ax-b\| \le \lambda-\tau,\quad \|[x;1]\| \le \tau, \tag{15}

in the sense that $r(A,b,x)$ is the least $\lambda$ for which some $\tau$ makes $(x,\lambda,\tau)$ feasible.

Milestones

Eq. (16). Every perturbation with $\|[\Delta A\ \Delta b]\|_F \le 1$ has residual at most $\|Ax-b\| + \sqrt{\|x\|^2+1}$ .
The worst-case perturbation. For a unit vector $u$ aligned with $Ax - b$ (arbitrary if $Ax = b$ ), the rank-one matrix $\Delta = u[x^T\ {-1}]/\sqrt{\|x\|^2+1}$ has $\|\Delta\|_F = \|\Delta\| = 1$ and attains the bound.
Spectral norm. The worst case over the larger ball $\|[\Delta A\ \Delta b]\| \le 1$ is the same value.
Strict convexity. $x \mapsto r(A,b,x)$ is strictly convex on $\mathbb{R}^m$ .
The SOCP (15). For every $x$ , $r(A,b,x)$ is the optimal $\lambda$ of (15) with $x$ fixed, and $x$ is an RLS solution exactly when it is the $x$ -part of an optimal solution of (15).

Significance

The closed form replaces a maximization over a matrix ball of dimension $n(m+1)$ by two Euclidean norms. It shows that the RLS objective is the LS residual plus a penalty $\sqrt{\|x\|^2+1}$ that does not depend on $A$ or $b$ , which is the starting point for the paper's Theorem 3.2 (the RLS solution is a Tikhonov-regularized LS solution with a data-dependent weight) and its analysis of continuity and conditioning. The SOCP formulation places the problem in the class solved by interior-point methods, at a cost the paper compares with one singular value decomposition of $A$ . The spectral-norm statement says the worst case does not depend on which of the two standard matrix norms bounds the perturbation.

The result is proved in the paper; the proof is short. To the best of the planning survey (September 2026), no machine-checked proof exists, and Prove2Me has no statement about worst-case residuals or robust least squares. The mission produces a verified closed form that later missions of this series (Tikhonov form of the solution, structured and linear-fractional perturbations) and any formalization of robust regression can import.

Difficulty

The upper bound alone does not give the theorem: the statement is an equality, and the equality needs an explicit maximizer. The paper's printed maximizer is wrong by a sign: with $[x^T\ 1]$ in place of $[x^T\ {-1}]$ the perturbation does not attain the bound (for $A = 0$ , $x = 0$ , $b = e_1$ it gives residual $0$ instead of $2$ ), so a transcription of the printed proof fails. Two further points are silent in the paper. The operator norm of a rank-one matrix has to be computed from the definition of the largest singular value. Uniqueness of the minimizer needs existence first, which follows from growth of $r$ at infinity and is not stated. Working with the sSup definition of the worst case requires showing the set of residuals is bounded, which is milestone 1.

Formalization scope

Dimensions are Fin n, Fin m; $A$ is Matrix (Fin n) (Fin m) ℝ, $b$ and $x$ are functions Fin n → ℝ, Fin m → ℝ. The augmented matrix $[\Delta A\ \Delta b]$ is indexed by Fin m ⊕ Unit, and so is $[x;1]$ .
Vector norms are the Euclidean norm written as $\sqrt{\sum_i v_i^2}$ (eucNorm), never Mathlib's ‖·‖ on Fin n → ℝ, which is the sup norm. The Frobenius norm and the largest singular value are explicit definitions (frobNorm, specNorm); specNorm is the infimum of admissible operator constants.
The maximum in (1) is sSup of the set of attained residuals. For $\rho \ge 0$ the set is nonempty and bounded, so this is the true maximum; milestones 1 and 2 state the bound and the attaining perturbation directly, so no statement relies on the value of sSup on an unbounded set.
The paper's normalization $\rho = 1$ is kept; general $\rho > 0$ follows from the scaling $\phi(A,b,\rho) = \rho\,\phi(A/\rho,b/\rho,1)$ the paper records on p. 1039 and is not a target.
The goal assumes $n \ge 1$ . For $n = 0$ the only perturbation is the empty matrix, the worst case is $0$ , and the closed form fails; the paper's setting ( $Ax \simeq b$ with data $b \in \mathbb{R}^n$ ) has $n \ge 1$ . Milestones 3–5 carry the same hypothesis.
Milestone 2 states the corrected perturbation $[x^T\ {-1}]$ ; the printed $[x^T\ 1]$ is false.
A trivializing formalization — an upper bound in place of the equality, a worst case over $\Delta A$ and $\Delta b$ bounded separately, or uniqueness among critical points only — is ruled out: the goal is the equality for the jointly bounded augmented matrix and ∃! of a global minimizer over all of $\mathbb{R}^m$ .

Contributions welcome: lemmas on Frobenius and operator norms of rank-one matrices, the inequality $\|Mz\| \le \|M\|_F\|z\|$ in this explicit setting, and strict convexity of $x \mapsto \sqrt{\|x\|^2+1}$ ; these are reusable beyond the mission.

Selected references

L. El Ghaoui and H. Lebret, Robust Solutions to Least-Squares Problems with Uncertain Data, SIAM Journal on Matrix Analysis and Applications 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
A. Ben-Tal, L. El Ghaoui and A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
H. Xu, C. Caramanis and S. Mannor, Robust Regression and Lasso, Journal of Machine Learning Research 10:1485–1510, 2009 (IEEE Trans. Inf. Theory 56(7), 2010). https://jmlr.org/papers/v10/xu09b.html
M. S. Lobo, L. Vandenberghe, S. Boyd and H. Lebret, Applications of Second-Order Cone Programming, Linear Algebra and its Applications 284:193–228, 1998. https://doi.org/10.1016/S0024-3795(98)10032-0

7 thms3 active usersReviewed

Completed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

Competitive Paging Algorithms III: No Randomized Paging Algorithm Is Better than H_k-CompetitiveResearch Paper

Motivation

Paging is the problem of managing a two-level memory: a cache holds $k$ of the $n$ pages a program uses, every request must find its page in the cache, and a request to a page outside the cache (a page fault) forces the algorithm to bring the page in and evict another. An on-line algorithm chooses what to evict without seeing future requests. Sleator and Tarjan (CACM 1985) measured on-line paging algorithms against the optimal off-line algorithm, which knows the whole request sequence, and showed that no deterministic on-line algorithm can be within a factor smaller than $k$ of it.

Randomization changes that picture. Fiat, Karp, Luby, McGeoch, Sleator and Young (J. Algorithms 1991; arXiv:cs/0205038) gave a randomized algorithm, the marking algorithm, whose expected number of faults is within $2H_k$ of the optimum, where $H_k = 1 + \tfrac12 + \dots + \tfrac1k \approx \ln k$ . This mission formalizes the other half of their paper's picture: no randomized paging algorithm can do better than $H_k$ . The bound says that the logarithmic behaviour is not an artefact of one algorithm but a property of the problem.

Timeline:

1985 — Sleator and Tarjan: deterministic paging algorithms have competitive factor at least $k$ ; LRU and FIFO achieve $k$ .
1988 — Karlin, Manasse, Rudolph and Sleator (Algorithmica 3, 1988) introduce the term competitive; Manasse, McGeoch and Sleator (STOC 1988; J. Algorithms 1990) extend it to randomized algorithms and pose the $k$ -server problem, of which paging is the uniform-metric case.
1991 — Fiat et al.: the marking algorithm is $2H_k$ -competitive, and no randomized algorithm is better than $H_k$ -competitive (Theorem 4 and Corollary 5 of the paper). Raghavan gave an alternative proof of the lower bound through Yao's minimax principle.
1991 — McGeoch and Sleator give an $H_k$ -competitive randomized paging algorithm (Algorithmica 6, 1991), so the lower bound is tight.

Setting

Let $M$ be a set of $n$ vertices with the uniform metric: any two distinct vertices are at distance $1$ . A configuration of $k$ servers is a map $C : \{1,\dots,k\} \to M$ ; server $s$ sits at $C(s)$ , and a vertex is covered when some server sits on it. A request sequence $\sigma$ is a finite list of vertices. A deterministic on-line algorithm assigns to every prefix of requests the configuration after serving it, in such a way that the vertex just requested is covered; its cost on $\sigma$ is the total distance travelled by its servers, which on the uniform metric is the number of server moves. Paging with $k$ cache slots and $n$ pages is exactly this $k$ -server problem on $n$ uniform vertices.

The optimal off-line cost $\mathrm{OPT}_{C_0}(\sigma)$ is the least cost of any schedule of configurations that starts at $C_0$ and covers each request of $\sigma$ in turn.

A randomized on-line algorithm $A$ is a probability space $(\Omega,\mu)$ of coin outcomes together with a deterministic on-line algorithm $A_\omega$ for each outcome $\omega$ . Its expected cost $C_A(\sigma)$ is the average of the cost of $A_\omega$ on $\sigma$ over $\omega$ . The request sequence is fixed in advance and does not depend on the coins (an oblivious adversary). Following the paper, $A$ is $c$ -competitive from the initial configuration $C_0$ if there is a constant $a$ such that

C_A(\sigma) \;\le\; c \cdot \mathrm{OPT}_{C_0}(\sigma) + a \qquad \text{for every request sequence } \sigma .

For the lower-bound argument, the probability vector $p=(p_i)_{i\in M}$ after a prefix $\sigma$ has $p_i$ equal to the probability, over $\omega$ , that vertex $i$ is not covered by $A_\omega$ after serving $\sigma$ . A set $S$ of marked vertices and the number $u = n - |S|$ of unmarked vertices are bookkeeping of the adversary, updated as the marking algorithm would update them.

Formalization targets

Goal: Corollary 5

For $1 \le k \le n-1$ , every randomized on-line algorithm $A$ with $k$ servers on $n$ uniform vertices, every initial configuration $C_0$ and every real $c$ ,

c < H_k \;\Longrightarrow\; A \text{ is not } c\text{-competitive from } C_0 .

Theorem 4 (milestone)

The case $k = n-1$ : no randomized algorithm for the uniform $(n-1)$ -server problem on $n$ vertices is $c$ -competitive with $c < H_{n-1}$ .

Claims of the proof of Theorem 4 (milestones)

With $p$ the probability vector, $S$ the marked set, $P = \sum_{i\in S} p_i$ and $u = n - |S|$ :

\sum_i p_i = 1 \quad(\text{servers on distinct vertices}),\qquad C_A(\sigma\,i) \ge C_A(\sigma) + p_i,

P = 0 \Rightarrow \exists\, i\notin S,\ p_i \ge \tfrac1u, \qquad P > \epsilon > 0 \Rightarrow \max_{j\in S} p_j \ge \tfrac{\epsilon}{|S|} > 0,

p_j = \max_{j'\notin S} p_{j'} \Rightarrow p_j \ge \tfrac{1-P}{u}, \qquad P \le \epsilon \Rightarrow \epsilon + p_j \ge \epsilon + \tfrac{1-P}{u} \ge \epsilon + \tfrac{1-\epsilon}{u} \ge \tfrac1u .

Significance

The result. Together with the marking algorithm's $2H_k$ upper bound, the corollary pins the randomized competitive ratio of paging to $\Theta(\log k)$ , an exponential improvement over the deterministic ratio $k$ that no randomized algorithm can push below $H_k$ . For $k = n-1$ the marking algorithm itself is $H_{n-1}$ -competitive, so Theorem 4 makes it optimal there. The $H_k$ bound is the benchmark every later randomized paging algorithm is measured against, including the $H_k$ -competitive algorithm of McGeoch and Sleator, and it is the uniform-metric base case of the randomized $k$ -server conjecture.

Formalizing it. The theorem is proved and classical; no machine-checked proof is known to exist. The platform already has the deterministic bound (KServer.uniform_not_competitive_below_k, ratio $k$ ) and a formal Yao averaging principle for randomized $k$ -server algorithms (KServer.randomized_yao_averaging), but no randomized paging lower bound. This mission produces the first formal $H_k$ lower bound, stated against the published randomized $k$ -server model, and a formal version of the paper's adversary argument. Either route — the paper's adaptive construction of a nemesis sequence from the probability vector, or Raghavan's distributional argument through Yao's principle — is welcome.

Difficulty

The adversary may not look at the coins, yet it must build one fixed sequence against which the expected cost is high in every phase. Requesting an uncovered vertex is not available, since which vertex is uncovered depends on the coins; requesting the vertex with the largest uncovered probability gives only $1/n$ per request and loses the harmonic sum. Lifting the per-phase bound to the asymptotic statement also requires handling the additive constant $a$ , the initial configuration of the off-line algorithm, and, for Corollary 5, the reduction from $n$ vertices to $k+1$ of them for an algorithm that may still place servers on the others.

Formalization scope

The Lean development reuses the published definitions KServer_model (configurations Fin k → M, deterministic on-line algorithms as functions of the request prefix, offlineCost) and KServer_randomized (RandomizedAlgorithm: a probability measure on coin outcomes, a deterministic algorithm per outcome, measurable costs; expCost as a lower Lebesgue integral in $[0,\infty]$ ; IsCompetitiveFrom C₀ c: every drawn algorithm starts at $C_0$ and there is one constant $a$ , fixed before the sequence, with expCost σ ≤ ENNReal.ofReal (c * offlineCost C₀ σ + a)). The clamp at $0$ in ENNReal.ofReal only weakens the property the goal refutes. The vertex set is an abstract type $M$ with an equivalence Fin n ≃ M and the uniform metric as a hypothesis, never the line metric of Fin n. $H_k$ is Mathlib's harmonic k cast to $\mathbb R$ . The goal quantifies over every algorithm and every initial configuration, with no laziness or distinct-positions assumption, and over every real $c < H_k$ , including $c \le 0$ .

A formalization in which competitiveness is vacuous (a model with no algorithms, or a cost that is always infinite), in which the adversary may choose the sequence after seeing the coins, or which fixes $c$ or the additive constant, would be a different statement and is ruled out by the published definitions used here.

The probability vector is the one new definition, uncoveredProb A σ i. Milestones about it assume the uncovered events measurable, the standing convention that $p_i$ is a probability; the model itself only guarantees measurable costs. The milestone $\sum_i p_i = 1$ assumes the $n-1$ servers occupy distinct vertices, as in the paper; in general $\sum_i p_i \ge 1$ . The arithmetic milestones are stated for an arbitrary probability vector on a finite set. Reusable pieces: the probability vector and the cost lemma apply to any randomized $k$ -server algorithm on a uniform metric, and a restriction lemma (from $n$ vertices to $k+1$ ) would serve other paging lower bounds.

Selected references

A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991. https://doi.org/10.1016/0196-6774(91)90041-V ; preprint arXiv:cs/0205038v1 (cited version). https://arxiv.org/abs/cs/0205038
D. D. Sleator, R. E. Tarjan, Amortized Efficiency of List Update and Paging Rules, Comm. ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, J. Algorithms 11(2):208–230, 1990. https://doi.org/10.1016/0196-6774(90)90003-W
L. A. McGeoch, D. D. Sleator, A Strongly Competitive Randomized Paging Algorithm, Algorithmica 6:816–825, 1991.
P. Raghavan, Lecture Notes on Randomized Algorithms, IBM Research Report, Yorktown Heights, 1990 (the alternative proof of the lower bound, pp. 118–119).

11 thms3 active usersReviewed

Completed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

Competitive Paging Algorithms II: Algorithm EATR Is 3/2-Competitive for Two ServersResearch Paper

Motivation

Paging is the problem of managing a two-level memory: a fast cache holding $k$ pages and a slow memory holding the rest. When a requested page is not in the cache (a page fault), it must be brought in and, if the cache is full, some page must be evicted. An on-line paging algorithm decides which page to evict without knowing future requests. Sleator and Tarjan (CACM 1985) compared on-line algorithms with the optimal off-line algorithm on every request sequence and showed that the best deterministic algorithms (LRU, FIFO) lose a factor of exactly $k$ , and that no deterministic on-line algorithm does better.

Randomization changes this picture. Fiat, Karp, Luby, McGeoch, Sleator and Young (J. Algorithms 1991; arXiv:cs/0205038) showed that the randomized marking algorithm is $2H_k$ -competitive, where $H_k=1+\tfrac12+\dots+\tfrac1k$ , and that no randomized algorithm is better than $H_k$ -competitive. For $k<n-1$ the marking algorithm does not reach $H_k$ , already for $k=2$ and $n=4$ . For two servers the same paper gives a different algorithm, EATR ("end after twice requested"), and proves it $3/2$ -competitive. Since $H_2=3/2$ , EATR is strongly competitive for $k=2$ : no randomized algorithm has a smaller competitive factor. This mission formalizes that result.

Timeline:

1985: Sleator and Tarjan, deterministic paging: factor $k$ , and $k$ is optimal.
1988: Karlin, Manasse, Rudolph and Sleator introduce the term competitive (Algorithmica 3:79–119); Manasse, McGeoch and Sleator formulate the $k$ -server problem and extend competitiveness to randomized algorithms (J. Algorithms 1990).
1991: Fiat et al.: the marking algorithm is $2H_k$ -competitive, the lower bound $H_k$ , and EATR is $3/2$ -competitive for $k=2$ .
1991: McGeoch and Sleator give an $H_k$ -competitive algorithm for every $k$ (Algorithmica 6, 1991; reference [12] of the paper).

Setting

The uniform $2$ -server problem has a finite set $M$ of $n\ge 2$ vertices, any two distinct vertices at distance $1$ , and two servers. A request sequence $\sigma=\sigma(0),\sigma(1),\dots$ is a list of vertices; each request must be covered by a server when it is served, and the cost is the number of server moves. This is paging with a cache of two pages: vertices are pages and the covered vertices are the cache.

A deterministic algorithm $B$ has a cost $C_B(\sigma)$ ; a randomized algorithm $A$ has an expected cost $C_A(\sigma)$ , averaged over its random choices. $A$ is $c$ -competitive if there is a constant $a$ such that for every request sequence $\sigma$ and every deterministic algorithm $B$ (on-line or off-line),

C_A(\sigma)\le c\cdot C_B(\sigma)+a.

Algorithm EATR. The servers start on the vertices $1$ and $2$ . The algorithm divides $\sigma$ into phases; the first phase starts at the first request to a vertex other than $1$ and $2$ . Let $P$ be the set of vertices occupied by the servers at the end of the previous phase ( $\{1,2\}$ before the first phase). During a phase, a vertex is clean if it is not in $P$ and has not been requested during this phase; a vertex is stale if it is neither clean nor the most recently requested vertex $\ell$ . EATR keeps one server on $\ell$ and the other uniformly at random on the stale set. When a stale vertex $r$ is requested, the servers are placed on $\ell$ and $r$ and the phase ends; the next phase starts at the next request to a vertex not covered by a server. Requests between phases, and repeated requests to $\ell$ , move nothing.

For a phase, $l$ denotes the number of clean vertices requested in it. For a deterministic algorithm $A$ , $d$ and $d'$ denote the numbers of $A$ 's servers that do not coincide with any of EATR's servers at the beginning and at the end of the phase. An algorithm is lazy if it moves no server on a request to a covered vertex and exactly one server on a request to an uncovered one.

Formalization targets

Goal: Theorem 3

With $\mathrm{OPT}(\sigma)$ the optimal off-line cost of serving $\sigma$ from the servers' starting position $(1,2)$ , there is a constant $c$ such that for all $\sigma$

C_{\mathrm{EATR}}(\sigma)\le \tfrac32\,\mathrm{OPT}(\sigma)+c.

The constant $c$ is left free; the factor $3/2$ is the paper's and is optimal.

Milestones, in the order of the proof

Laziness (p. 4): every deterministic algorithm is dominated by a lazy one (a published theorem, reused).
Adversary bound for structured phases (p. 5): in a complete EATR phase with $l$ clean requests, a lazy $A$ pays at least $l-d+d'$ .
Stale set before the terminating request (p. 6): it has $l+1$ elements, each covered with probability $1/(l+1)$ .
Expected cost of a phase to EATR (p. 6): exactly $l+\frac{l}{l+1}$ .
Per-phase ratio (p. 6): EATR's expected phase cost is at most $\tfrac32(C_A+d-d')$ , since $\frac{l+l/(l+1)}{l}=1+\frac{1}{l+1}\le\frac32$ .

Significance

The result. Theorem 3 settles the randomized competitive ratio of paging with two cache slots: combined with the paper's lower bound $H_k$ (Corollary 5, the subject of a companion mission), the optimal factor for $k=2$ is exactly $3/2$ , against $2$ for every deterministic algorithm. The general case was settled later by McGeoch and Sleator's $H_k$ -competitive partitioning algorithm, which is considerably more complicated.

Formalizing it. The result has been proved since 1991; no machine-checked proof of it is on the platform (a search for EATR, randomized paging and two-server results on 2026-09-26 found only deterministic $k$ -server theorems). The mission produces a formal model of a randomized on-line algorithm as a probability distribution over states evolving with the request sequence, a formal treatment of the phase decomposition and of the telescoping amortization that relates expected on-line cost to the optimal off-line cost, and a first strongly competitive randomized paging result on the platform, alongside the deterministic $k$ -server results already there.

Difficulty

The per-phase computations are short. The main difficulty is the global accounting. The adversary's cost in a phase is bounded only in amortized form, $l-d+d'$ , where $d$ and $d'$ compare the adversary's servers with EATR's at the phase boundaries; the bound becomes a statement about $\mathrm{OPT}$ only after the $d$ and $d'$ terms telescope across phases. This needs care with the requests that lie outside every phase (before the first phase, between phases, and in an unfinished last phase), during which the adversary may move. A further difficulty is that the off-line optimum ranges over arbitrary schedules, which may move several servers on one request, while the phase bound is proved for lazy on-line algorithms: the reduction from one to the other must be made explicit. Finally, the uniform law of the stale server is an invariant of a Markov chain on states that must be tracked through the whole phase.

Formalization scope

The vertices are an abstract metric space $M$ with an enumeration $e:\mathrm{Fin}\,n\simeq M$ , $2\le n$ , and the hypothesis that distinct points are at distance $1$ ; the metric of $\mathrm{Fin}\,n$ is not used. The starting vertices $1,2$ are $e(0),e(1)$ . $\mathrm{OPT}$ is KServer.offlineCost of the published KServer model: the infimum of total movement over all schedules serving $\sigma$ from $(e(0),e(1))$ . Comparing with this infimum covers every deterministic $B$ starting from EATR's position; a $B$ starting elsewhere differs by at most $2$ , which the constant absorbs. The constant is quantified before $\sigma$ .

EATR is a PMF over states: a deterministic record (the set $P$ , whether a phase is in progress, the last requested vertex, the vertices requested in the phase) and the random position of the second server. Its expected cost is the expected number of server moves, summed over the requests. The paper fixes only that the second server is uniform on the stale set; when a clean request enlarges the stale set, the formalization moves one server by a fixed coupling that keeps the law uniform, and this choice is stated in the definition. A formalization that defines EATR's expected cost by the closed formula of the proof, or that restricts $\sigma$ to complete phases, would make the goal a different statement; neither is done here. The pre-phase prefix and an unfinished last phase belong to $\sigma$ and are covered by the constant.

Needed infrastructure: finite probability distributions (Mathlib's PMF), the published KServer model and its laziness theorem, and bookkeeping lemmas on the deterministic phase record. The phase record and the amortization argument are reusable for the marking algorithm of the companion mission. Proofs of any milestone, and alternative decompositions of the goal, are welcome.

Selected references

A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, Journal of Algorithms 12(4):685–699, 1991. https://doi.org/10.1016/0196-6774(91)90041-V ; arXiv:cs/0205038v1, https://arxiv.org/abs/cs/0205038
D. D. Sleator, R. E. Tarjan, Amortized Efficiency of List Update and Paging Rules, Communications of the ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, Journal of Algorithms 11(2):208–230, 1990. https://doi.org/10.1016/0196-6774(90)90003-W
L. A. McGeoch, D. D. Sleator, A Strongly Competitive Randomized Paging Algorithm, Algorithmica 6:816–825, 1991 (reference [12] of the paper).
A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3(1):79–119, 1988 (reference [9] of the paper).

8 thms3 active usersReviewed

Combinatorics Complexity Theory Operations Research+2·Captain: mikedeng1

A Threshold of ln n for Approximating Set Cover II: The Inapproximability of Max k-CoverResearch Paper

Motivation

Max $k$ -cover is the basic coverage problem of combinatorial optimization. The input is a collection of subsets of a finite ground set and a number $k$ ; the task is to choose $k$ subsets that together cover as many points as possible. It models facility and sensor placement, the selection of a small committee or feature set representing a population, and budgeted versions of set cover. It is also the prototype of maximizing a monotone submodular function under a cardinality constraint.

The greedy algorithm covers at least a $1-1/e\approx 0.632$ fraction of the optimum. This bound goes back to Hochbaum and Pathria and, for general submodular functions, to Nemhauser, Wolsey and Fisher (1978). For two decades it was not known whether a polynomial-time algorithm could do better. Uriel Feige answered the question in A Threshold of ln n for Approximating Set Cover (J. ACM 45(4), 1998, pp. 634–652, doi:10.1145/285055.285059), Section 5. His Theorem 5.3 (p. 648) states: "For any $\epsilon > 0$ , max $k$ -cover cannot be approximated in polynomial time within a ratio of $(1 - 1/e + \epsilon)$ , unless $P = NP$ ." Together with the greedy bound, it makes $1-1/e$ the exact approximation threshold of max $k$ -cover.

Timeline:

1978: Nemhauser, Wolsey and Fisher prove the greedy $1-1/e$ bound for monotone submodular maximization.
1992: Arora, Lund, Motwani, Sudan and Szegedy prove the PCP theorem. With Papadimitriou–Yannakakis (1991) it gives Theorem 2.1.1 of the paper: MAX 3SAT-B has a constant gap unless P = NP.
1994: Lund and Yannakakis introduce partition-system reductions from multi-prover proof systems to set cover.
1995: Raz proves the parallel repetition theorem (Theorem 2.2.2 of the paper).
1998: Feige proves the ln n threshold for set cover (the subject of mission I of this series) and the $1-1/e$ threshold for max $k$ -cover.

Setting

An instance consists of $n$ points $\{0,\dots,n-1\}$ , a list of subsets $S_1,\dots,S_s$ of the points, and a number $k$ . Its value $\mathrm{opt}$ is the largest number of points covered by at most $k$ of the sets. Instances are written over a three-letter alphabet:

$n$ in unary;
each set as its characteristic bit-vector;
$k$ in unary.

Following p. 648, a polynomial-time algorithm approximates max $k$ -cover within a ratio $\delta$ if on every input it outputs a number $v$ with

\delta\cdot\mathrm{opt}\le v\le\mathrm{opt}.

The algorithm need not name the sets. This is the non-constructive notion of approximation.

The proof is a reduction from the MAX 3SAT-5 problem. A 3CNF-5 formula has exactly three literals per clause, over three distinct variables, and every variable occurs in exactly five clauses. The reduction goes through a $k$ -prover proof system for such a formula $\varphi$ with $M$ clauses:

The verifier picks $\ell$ clauses at random, and a distinguished variable in each; there are $R=(3M)^\ell$ random strings $r$ .
Each prover $P_i$ is attached to a code word of length $\ell$ and weight $\ell/2$ ; distinct words are at Hamming distance at least $\ell/3$ .
On coordinate $j$ , prover $P_i$ receives the clause if its bit is 1, and the distinguished variable if its bit is 0.
Answers are satisfying assignments of the received clauses and bits for the received variables.
Two provers are consistent if they assign the same values to the distinguished variables. The verifier weakly accepts if some pair of distinct provers is consistent, and strongly accepts if every pair is.

The max $k'$ -cover instance of §5 attaches to every random string $r$ a copy $B_r$ of the explicit partition system. Its points are the vectors in $\{0,\dots,k-1\}^L$ with $L=2^\ell$ , so $m=k^L$ . Its $L$ partitions are labelled by the $\ell$ -bit strings, and each splits the points by the value of one coordinate. There are $N=mR$ points in all. For each prover $i$ , question $q$ and answer $a$ , the set $S_{(q,a,i)}$ collects, for every $r$ on which $P_i$ receives $q$ , the $i$ th part of the partition of $B_r$ labelled by the values that $a$ gives to the distinguished variables of $r$ . The budget is $k'=kQ$ , where $Q$ is the number of questions a single prover can receive.

Formalization targets

Goal: Theorem 5.3

\forall\varepsilon>0:\quad \text{max } k\text{-cover is approximable within } 1-\tfrac1e+\varepsilon \ \Longrightarrow\ \mathrm{P}=\mathrm{NP},

conditional on the two cited results below. The ratio is left free (any $\varepsilon>0$ ), so the goal records the shape of the threshold and not a particular constant.

Milestones

Proposition 2.1.2 (p. 640): for some $\varepsilon>0$ it is NP-hard to distinguish satisfiable 3CNF-5 formulas from those in which at most a $(1-\varepsilon)$ -fraction of the clauses can be satisfied simultaneously.
Lemma 2.3.1 (p. 643): a satisfiable $\varphi$ admits a strategy that always strongly accepts; on a far-from-satisfiable $\varphi$ the weak acceptance probability is at most $k^2\,2^{-c\ell}$ .
Coverage of the explicit partition system (p. 649): $j$ subsets from pairwise different partitions cover exactly $(1-(1-1/k)^j)m$ points.
Proposition 5.4 (p. 649): if at most $kQ$ sets cover a $(1-1/e+\varepsilon)$ -fraction of the points, then at least an $\varepsilon/3$ -fraction of the random strings are good. Here $r$ is good if $w_r\le3k/\varepsilon$ sets meet $B_r$ and two of them from different provers lie in the same partition.
Decoding (p. 649): such a covering yields a strategy that weakly accepts with probability at least $(\varepsilon/3)(\varepsilon/3k)^2$ .
Gap (p. 649): a satisfiable formula gives a cover of all $N$ points by $kQ$ sets. If at most a $(1-\varepsilon')$ -fraction of the clauses are satisfiable, $kQ$ sets cover at most $(1-1/e+g(k))N$ points, where $g(k)\to0$ , for all large $\ell$ .
Proposition 5.1 (p. 647): every greedy run covers at least $(1-1/e)\,\mathrm{opt}$ points.

Significance

The result closes the approximability of max $k$ -cover: the greedy algorithm cannot be beaten by any constant unless P = NP. Consequences:

Submodular maximization. Coverage functions are monotone submodular, so the bound transfers to monotone submodular maximization under a cardinality constraint, whenever the function is given in a form that encodes a coverage instance.
Other problems. Hardness results for facility location, budgeted allocation, and welfare maximization with coverage valuations reduce from it.
The reduction itself. The $\ell$ -fold $k$ -prover system combined with a partition system that is exactly countable is the template for later $1-1/e$ hardness proofs.

Status: the theorem has been proved since 1998. It has not been formalized; neither the reduction nor the underlying proof systems exist in Mathlib or on this platform. This mission produces:

a machine-checked reduction from MAX 3SAT-5 to max $k$ -cover;
an exact counting lemma for product partition systems;
the averaging and concavity argument of Proposition 5.4;
a formal statement of the greedy bound for coverage.

The cited PCP-based gap (Theorem 2.1.1) and parallel repetition (Theorem 2.2.2) remain hypotheses. They are separate, much larger formalization projects.

Difficulty

The obvious argument uses the soundness of the proof system directly: a large cover should force consistent answers. It fails because a cover may spend many sets on a few random strings and cover them completely, while covering the rest partially without any two sets from the same partition. What saves the argument is exact counting. For sets from pairwise different partitions, coverage is exactly $h(j)=(1-(1-1/k)^j)m$ , a concave function of the number $j$ of sets used. Since the sets meet a random string $k$ times on average, Jensen's inequality caps the total coverage of such "unstructured" strings at about $(1-(1-1/k)^k)$ , which tends to $1-1/e$ . A further obstacle is that the reduction must run in polynomial time. The paper therefore takes $\ell$ and $k$ constant (unlike the set-cover reduction, where $\ell=\Theta(\log\log n)$ ), and the soundness bound $k^2 2^{-c\ell}$ must beat $(\varepsilon/3)(\varepsilon/3k)^2$ at a constant $\ell$ . The quantifier order ( $k$ large first, then $\ell$ large) is part of the difficulty.

A second obstacle is the machine model. The goal is a statement about polynomial-time Turing machines, so the reduction and the decision procedure built from a hypothetical approximation algorithm must be compiled into Cook's one-tape machines.

Formalization scope

Machine model. CookPvsNP_defs (a published platform definition): one-tape Turing machines, $\mathrm{P}$ , $\mathrm{NP}$ , polynomial-time computable functions, CNF formulas and their encoding. "P = NP" is P Bool = NP Bool, the form in which CookPvsNP.P_ne_NP states the open problem.
Cited results as hypotheses. Theorem 2.1.1 enters as Thm211. Raz's theorem enters as RazRepetition, its consequence stated on p. 642: the $\ell$ -fold clause–variable game on a far-from-satisfiable 3CNF-5 formula has acceptance probability at most $2^{-c\ell}$ . This is weaker than Raz's general theorem, so the conditional statement is stronger. No hypothesis about max $k$ -cover is assumed.
Approximation. The value form above, with no size threshold. For $\varepsilon>1/e$ the ratio exceeds one and the hypothesis is unsatisfiable on any instance with $\mathrm{opt}>0$ ; those values are vacuous, as in the paper.
$\mathrm{opt}$ . Taken over at most $k$ sets. This agrees with the paper's "exactly $k$ " whenever $k\le s$ .
Probability and counting. Probabilities are uniform counts over the $(3M)^\ell$ random strings. Fractions in lower-bound statements are written as counts compared with multiples of $R$ .
Canonical answers. The type of answers is restricted to satisfying assignments of the received clauses, following the paper's "without loss of generality" (p. 643). All indices are 0-based.
Partition system. The §4 construction is defined for any partition system with $\ell$ -bit partition labels and instantiated with the explicit product system. Its $L=2^\ell$ coordinates are the $\ell$ -bit strings themselves.
Not formalized. The running time of the greedy algorithm, and the constructive variant (Proposition 5.2), which belongs to the set-cover mission.

A trivializing formalization is ruled out: every cited input is a named, satisfiable proposition about 3CNF formulas or the two-prover game, never about max $k$ -cover, and the approximation hypothesis is satisfiable for ratios up to $1$ .

Needed infrastructure, reusable beyond this mission:

composition and simulation lemmas for Cook's machines;
the uniformity of the verifier's questions on 3CNF-5 formulas;
concavity of $j\mapsto 1-(1-1/k)^j$ ;
$(1-1/k)^k\to 1/e$ bounds.

Contributions to any of these, or to either cited theorem, are welcome.

Selected references

U. Feige, A threshold of ln n for approximating set cover, J. ACM 45(4) (1998) 634–652. https://doi.org/10.1145/285055.285059
R. Raz, A parallel repetition theorem, SIAM J. Comput. 27(3) (1998) 763–803 (STOC 1995). https://doi.org/10.1137/S0097539795280895
S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3) (1998) 501–555. https://doi.org/10.1145/278298.278306
C. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. System Sci. 43(3) (1991) 425–440. https://doi.org/10.1016/0022-0000(91)90023-X
C. Lund, M. Yannakakis, On the hardness of approximating minimization problems, J. ACM 41(5) (1994) 960–981. https://doi.org/10.1145/185675.306789
G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions—I, Math. Programming 14 (1978) 265–294. https://doi.org/10.1007/BF01588971
S. Cook, The P versus NP problem, Clay Mathematics Institute. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

13 thms3 active usersReviewed

Completed

Information Theory Operations Research Probability·Captain: mikedeng1

Conditional and Dynamic Convex Risk Measures II: The Conditional Entropic Risk Measure and Conditional Relative EntropyResearch Paper

Motivation

A risk measure assigns to a random financial position $X$ a capital requirement $\rho(X)$ : the amount of cash that must be added to $X$ to make it acceptable. The axiomatic theory of convex risk measures (Föllmer–Schied 2002; Frittelli–Rosazza Gianin 2002) treats this number as computed with no information beyond the model. In practice a regulator or a risk manager revises the requirement as information arrives, so the requirement becomes a random variable measurable with respect to the information available at the time of measurement. Detlefsen and Scandolo (SFB 649 Discussion Paper 2005-006; published in Finance and Stochastics 9(4), 2005, doi:10.1007/s00780-005-0159-6) develop this conditional theory: axioms, a robust representation, and a treatment of dynamic risk measurement.

The entropic risk measure is the standard example of a convex risk measure that is not coherent. It is the capital requirement of an agent with exponential utility $u_\gamma(x)=1-e^{-\gamma x}$ , and its penalty function in the robust representation is the relative entropy $\frac1\gamma H(Q\mid P)$ (Föllmer–Schied, Stochastic Finance, Example 4.60, as cited by the paper). Section 5 of the paper carries this example to the conditional setting and shows that its penalty is a conditional relative entropy. The same identity appears in dynamic entropic risk measures, exponential-utility indifference pricing and recursive utility, where one-period conditional entropic measures are composed over time.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ and a sub- $\sigma$ -algebra $\mathcal G\subseteq\mathcal F$ , the information available at the time of measurement. $L^\infty$ is the space of essentially bounded random variables and $L^\infty_{\mathcal G}$ its $\mathcal G$ -measurable part. All equalities and inequalities between random variables hold $P$ -almost surely.

A conditional convex risk measure is a map $\rho:L^\infty\to L^\infty_{\mathcal G}$ that is translation invariant ( $\rho(X+Z)=\rho(X)-Z$ for $Z\in L^\infty_{\mathcal G}$ ), monotone ( $X\le Y\Rightarrow\rho(X)\ge\rho(Y)$ ), conditionally convex ( $\rho(\Lambda X+(1-\Lambda)Y)\le\Lambda\rho(X)+(1-\Lambda)\rho(Y)$ for $\Lambda\in L^\infty_{\mathcal G}$ , $0\le\Lambda\le1$ ), and satisfies $\rho(0)=0$ .

The relevant probability models are

\mathcal P_{\mathcal G}=\{Q \text{ probability on } (\Omega,\mathcal F) : Q\ll P,\ Q(A)=P(A)\ \text{for all } A\in\mathcal G\}.

The essential supremum of a family $\mathcal X$ of $[-\infty,+\infty]$ -valued random variables is the a.s. smallest random variable that dominates every member a.s.; the essential infimum is defined symmetrically. The minimal penalty of $\rho$ is

\alpha^*(Q)=\operatorname{ess.sup}_{X\in L^\infty}\{-E_Q(X\mid\mathcal G)-\rho(X)\},\qquad Q\in\mathcal P_{\mathcal G}.

For a risk aversion $\gamma>0$ , the conditional entropic risk measure is

\rho_\gamma(X)=\frac1\gamma\log E_P\big(e^{-\gamma X}\mid\mathcal G\big),

the capital requirement for the acceptance set $A_\gamma=\{X\in L^\infty : E_P(e^{-\gamma X}\mid\mathcal G)\le1\}$ . For $Q\in\mathcal P_{\mathcal G}$ with density $\varphi=dQ/dP$ , the conditional relative entropy is

H_{\mathcal G}(Q\mid P)=E_P(\varphi\log\varphi\mid\mathcal G)\in[0,+\infty],\qquad 0\log0=0.

Formalization targets

Goal: Proposition 5.4

For every $\gamma>0$ :

\rho_\gamma(X)=\operatorname{ess.sup}_{Q\in\mathcal P_{\mathcal G}}\Big\{-E_Q(X\mid\mathcal G)-\tfrac1\gamma H_{\mathcal G}(Q\mid P)\Big\}\quad(X\in L^\infty),\qquad \alpha^*(Q)=\tfrac1\gamma H_{\mathcal G}(Q\mid P)\quad(Q\in\mathcal P_{\mathcal G}).

The first identity is representability with the minimal penalty as the penalty; the second identifies that penalty.

Milestones

(Section 5, p. 12) $\rho_\gamma$ is a conditional convex risk measure.
(Section 5, p. 12) $\rho_\gamma(X)=\operatorname{ess.inf}\{Y\in L^\infty_{\mathcal G}: X+Y\in A_\gamma\}=\operatorname{ess.inf}\{Y\in L^\infty_{\mathcal G}: E_P(e^{-\gamma X}\mid\mathcal G)\le e^{\gamma Y}\}$ .
(Proof of Proposition 5.4) $\rho_\gamma$ is continuous from above: $X_n\searrow X$ implies $\rho_\gamma(X_n)\nearrow\rho_\gamma(X)$ .
(Section 5, p. 13) For $Q\in\mathcal P_{\mathcal G}$ : $E_P(\varphi\mid\mathcal G)=1$ and $H_{\mathcal G}(Q\mid P)=E_Q(\log\varphi\mid\mathcal G)$ .
(Proof of Proposition 5.4) $\alpha^*(Q)=\frac1\gamma\operatorname{ess.sup}_{Z\in L^\infty}\{E_Q(Z\mid\mathcal G)-\log E_P(e^Z\mid\mathcal G)\}$ .
(Lemma 5.5) The conditional Donsker–Varadhan formula

\operatorname{ess.sup}_{Z\in L^\infty}\{E_Q(Z\mid\mathcal G)-\log E_P(e^Z\mid\mathcal G)\}=H_{\mathcal G}(Q\mid P),\qquad Q\in\mathcal P_{\mathcal G}.

Significance

The result gives the conditional entropic risk measure an explicit dual description: the capital requirement is a worst case over conditional models, each penalized by its conditional relative entropy. This duality is what makes entropic risk measures computable in dynamic settings. Recursive compositions of $\rho_\gamma$ over a filtration are time consistent, and their penalties add up by the chain rule for conditional relative entropy. Lemma 5.5 is also the conditional form of the Donsker–Varadhan (Gibbs) variational principle, which is used on its own in large deviations and in PAC-Bayesian bounds.

On status: the results are proved in the paper, and the unconditional versions are textbook material. Mathlib has unconditional Kullback–Leibler divergence, tilted measures, conditional Jensen's inequality and a $[0,+\infty]$ -valued conditional expectation. As far as the platform search could establish, neither the conditional relative entropy nor the conditional Donsker–Varadhan formula nor any conditional risk measure has been formalized. This mission produces the first machine-checked conditional version, with $H_{\mathcal G}$ allowed to be infinite.

Difficulty

In the unconditional case both sides of Lemma 5.5 are numbers, and the supremum is a supremum over reals. Conditionally, both sides are random variables. The supremum over the uncountable family indexed by $L^\infty$ must be taken in the essential sense, and a pointwise supremum is neither measurable nor meaningful. The conditional relative entropy can be $+\infty$ on a set of positive probability. The integrand $\varphi\log\varphi$ need not be integrable, so the usual conditional expectation of $L^1$ is not available for it, and the " $\ge$ " direction must reach an unbounded target through bounded test variables while controlling $\log E_P(e^{Z}\mid\mathcal G)$ at the same time. The ess.sup in the goal ranges over measures, not random variables, and each $E_Q(\cdot\mid\mathcal G)$ is a conditional expectation under a different measure. These are identified with $P$ -a.s. objects through the condition $Q=P$ on $\mathcal G$ .

Formalization scope

$(\Omega,\mathcal F,P)$ is a probability space (IsProbabilityMeasure P), and $\mathcal G$ is m : MeasurableSpace Ω with hm : m ≤ mΩ. Payoffs are real functions with MemLp X ⊤ P. $L^\infty_{\mathcal G}$ membership is StronglyMeasurable[m] plus MemLp ⊤. Every (in)equality between random variables is $P$ -a.e.
$\mathcal P_{\mathcal G}$ is the subtype of probability measures $Q\ll P$ with $Q(A)=P(A)$ for all $A\in\mathcal G$ . This is equality on $\mathcal G$ , not equivalence of measures.
$E_P(\cdot\mid\mathcal G)$ and $E_Q(\cdot\mid\mathcal G)$ on bounded variables are Mathlib's conditional expectations P[·|m] and Q[·|m]. Bounded variables are integrable under every $Q\ll P$ , so no junk value arises.
$\rho_\gamma$ is the paper's closed form $\frac1\gamma\log E_P(e^{-\gamma X}\mid\mathcal G)$ . The ess.inf descriptions are a milestone, and no positivity hypothesis on $X$ is imposed.
$\varphi$ is the real part of the Radon–Nikodym derivative Q.rnDeriv P. $H_{\mathcal G}(Q\mid P)$ and $E_Q(\log\varphi\mid\mathcal G)$ are generalized conditional expectations, $E(f^+\mid\mathcal G)-E(f^-\mid\mathcal G)$ , built from Mathlib's $[0,+\infty]$ -valued condLExp and valued in EReal. The negative parts are integrable, so $+\infty-(+\infty)$ never arises. In EReal, a real number minus $+\infty$ is $-\infty$ , which is how a model with infinite entropy drops out of the supremum.
Essential suprema and infima are predicates (IsEssSup, IsEssInf) on a candidate $P$ -a.e. measurable EReal-valued function. The candidate must dominate every member a.s. and lie a.s. below every a.s. upper bound.
Continuity from above means: a.s. monotone convergence $X_n\searrow X$ in $L^\infty$ implies a.s. monotone convergence $\rho(X_n)\nearrow\rho(X)$ .
$\gamma$ is a real constant with $\gamma>0$ . The random risk aversion of Remark 5.6 is not formalized.
Ruled out: defining $H_{\mathcal G}$ through the Bochner conditional expectation P[φ * log φ | m] (which returns $0$ when $\varphi\log\varphi$ is not integrable) or $\alpha^*$ through a pointwise supremum would make the goal false or vacuous, and so would stating it for an abstract convex risk measure in place of $\rho_\gamma$ . The formalization uses the extended-valued $H_{\mathcal G}$ , the essential supremum, and the explicit $\rho_\gamma$ .
The mission is self-contained. It redefines conditional convex risk measures, $\mathcal P_{\mathcal G}$ and the essential supremum in its own namespace CondConvexRisk.Entropic and does not assume the general representation theorem (Theorem 3.2). The generalized conditional expectation and the conditional Donsker–Varadhan formula are reusable beyond risk measures. Contributions are welcome on the ess.sup API (existence, upward-directed families), on conditional monotone convergence for condExp, and on the conditional Jensen step for $x\log x$ .

Selected references

S. Detlefsen, G. Scandolo, Conditional and Dynamic Convex Risk Measures, SFB 649 Discussion Paper 2005-006, Humboldt-Universität zu Berlin, 2005 (the version formalized; published in Finance and Stochastics 9(4), 2005, https://doi.org/10.1007/s00780-005-0159-6).
H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, de Gruyter, Berlin, 2002 (reference [8] of the paper).
H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6:429–447, 2002. https://doi.org/10.1007/s007800200072
M. D. Donsker, S. R. S. Varadhan, Asymptotic evaluation of certain Markov process expectations for large time, III, Comm. Pure Appl. Math. 29:389–461, 1976. https://doi.org/10.1002/cpa.3160290405

9 thms3 active usersReviewed

Combinatorics Complexity Theory Operations Research+1·Captain: mikedeng1

A Threshold of ln n for Approximating Set Cover I: The ln n Inapproximability of Set CoverResearch Paper

Motivation

Set cover is the problem of covering a finite ground set with as few members of a given family of subsets as possible. It models facility location, crew scheduling, test-suite minimization and many other selection problems in operations research, and it is one of the canonical NP-hard problems. The greedy algorithm, which repeatedly picks the subset covering the most uncovered points, finds a cover at most about $\ln n$ times larger than the optimum on an instance with $n$ points (Johnson 1974; Lovász 1975; Chvátal 1979). Whether any efficient algorithm does substantially better was open for two decades.

Timeline of the lower bounds:

1992. The PCP theorem (Arora, Lund, Motwani, Sudan, Szegedy) implies that set cover cannot be approximated within some constant $1+\varepsilon$ unless P = NP.
1994. Lund and Yannakakis showed that set cover cannot be approximated within $\tfrac14\log_2 n$ unless $\mathrm{NP}\subseteq\mathrm{TIME}(n^{O(\mathrm{polylog}\, n)})$ , and within $\tfrac12\log_2 n\approx 0.72\ln n$ under a randomized assumption.
1998. Feige showed that for every $\varepsilon>0$ , set cover cannot be approximated within $(1-\varepsilon)\ln n$ unless $\mathrm{NP}\subseteq\mathrm{TIME}(n^{O(\log\log n)})$ (J. ACM 45(4), 634–652). This matches the greedy bound up to lower-order terms.
2014. Dinur and Steurer replaced the assumption by P ≠ NP (STOC 2014).

This mission formalizes Feige's theorem, the result that fixed $\ln n$ as the threshold.

Setting

An instance consists of $n$ points $\{0,\dots,n-1\}$ and a list of subsets $S_1,\dots,S_s$ . A cover is a set of indices whose subsets together contain every point. The instance is coverable if every point lies in some $S_i$ . It is written as a string: $n$ in unary, then each subset as its characteristic vector.

A deterministic polynomial-time algorithm approximates set cover within $\rho(n)$ if, for some threshold $n_0$ and every coverable instance with $n \ge n_0$ points, the value $v$ it outputs satisfies $\mathrm{OPT}\le v\le\rho(n)\cdot\mathrm{OPT}$ , where $\mathrm{OPT}$ is the size of a smallest cover.

$\mathrm{TIME}(n^{O(\log\log n)})$ is the class of languages that a deterministic one-tape Turing machine decides within $|w|^{c(\log_2\log_2|w|+1)}+c$ steps, for some constant $c$ . Machines, $\mathrm{P}$ and $\mathrm{NP}$ are those of the published definition CookPvsNP_defs.

The proof passes through three objects, each defined in the mission:

3CNF-5 formulas: CNF formulas in which every clause has three literals on distinct variables and every variable occurs in exactly five clauses.
The $k$ -prover proof system of §2.3. A verifier picks $\ell$ random clauses and a distinguished variable in each. Each prover, according to its code word, receives some of these clauses and the distinguished variables of the others. Under the weak acceptance predicate, some two provers give consistent answers on the distinguished variables. Under the strong acceptance predicate, all provers do.
Partition systems $B(m,L,k,d)$ (Definition 3.1). These are $L$ partitions of $m$ points, each into $k$ parts, such that covering the points with parts taken from pairwise different partitions needs at least $d$ parts.

Formalization targets

Goal: Theorem 4.4

\exists\,\varepsilon>0:\ \text{set cover is approximable within }(1-\varepsilon)\ln n\ \Longrightarrow\ \mathrm{NP}\subseteq\mathrm{TIME}\big(n^{O(\log\log n)}\big).

The statement fixes no constant beyond $\varepsilon$ . The parameters $k$ , $\ell$ and $m$ of the reduction are choices made inside the proof. The goal carries three cited results as hypotheses: Theorem 2.1.1 (MAX 3SAT-B gap), the consequence of Raz's parallel repetition theorem for the clause–variable game, and the Naor–Schulman–Srinivasan construction of partition systems.

Milestones, in the order the proof uses them

Proposition 2.1.2: MAX 3SAT-5 is gap NP-hard.
Proposition 2.2.1: the one-round clause–variable game has value $1-\varepsilon/3$ .
Lemma 2.3.1: the $k$ -prover system is complete with strong acceptance and has soundness $k^2 2^{-c\ell}$ for weak acceptance.
Lemma 3.2: partition systems with $d=(1-2/k)k\ln m$ exist.
Propositions 4.2 and 4.3: a cover with $(1-\delta)kQ\ln m$ subsets yields a prover strategy that is weakly accepted with probability at least $2\delta/(k\ln m)^2$ .
Lemma 4.1: the gap between $kQ$ and $(1-2f(k))kQ\ln m$ .

Significance

The result. Combined with the greedy algorithm, Theorem 4.4 shows that $\ln n$ is the approximation threshold of set cover under a mild complexity assumption. Set cover reduces approximation-preservingly to many covering problems, so the threshold transfers to them. Examples are dominating set, several facility-location and group Steiner problems, and hitting-set formulations used in scheduling and testing. The $k$ -prover system with two acceptance predicates and the partition-system gadget became standard tools for later hardness-of-approximation proofs.

Formalizing it. The theorem is proved and has been strengthened (Dinur–Steurer 2014), but no machine-checked proof of any $\Omega(\log n)$ inapproximability of set cover is known. This mission contributes:

a Lean model of multi-prover proof systems with uniform-count probabilities;
partition systems and their probabilistic existence proof;
a gap-preserving reduction whose running time is analysed on Turing machines, not merely asserted.

Difficulty

The ratio comes from two gaps at once. One is a gap in acceptance probability. The other is a gap between strong and weak acceptance. A reduction from a two-prover system, as in Lund–Yannakakis, loses a constant factor because a cheating cover can use two parts of the same partition. Feige's analysis must turn every small cover into a strategy under which some pair of provers is consistent (Proposition 4.3), and this averaging argument has to lose only a factor $(k\ln m)^2$ .
Parameters interlock. $\ell=\Theta(\log\log n)$ must make $k^2 2^{-c\ell}$ smaller than $2\delta/(k\ln m)^2$ while keeping the instance of size $n^{O(\log\log n)}$ . The time bound must hold for a one-tape machine, including the deterministic partition-system construction.
Encoding. The reduction must be computed by an explicit machine on string encodings. Showing that a "clearly polynomial" construction meets the time bound on such a machine is substantial work.

Formalization scope

Cited results as hypotheses. Theorem 2.1.1, Raz's theorem and the Naor et al. construction are not proved in the mission; each is a named proposition (Thm211, RazRepetition, NaorPartitionSystems) and a hypothesis of the goal.
- RazRepetition is only the consequence of Raz's theorem that the paper uses (p. 642): a $2^{-c\ell}$ error bound for the repeated clause–variable game on 3CNF-5 formulas far from satisfiable.
- NaorPartitionSystems relaxes "time linear in $m$ " to polynomial time and renders " $L$ polynomial in $d$ " as $L\le\lfloor\log_2 m\rfloor^a$ . Both relaxations weaken the hypothesis.
Approximation in value form. The algorithm outputs a number $v$ with $\mathrm{OPT}\le v\le\rho(n)\mathrm{OPT}$ , and only on coverable instances with $n\ge n_0$ . Any algorithm that outputs a cover yields such a value, so this hypothesis is weaker than the paper's. The guard $n\ge n_0$ is needed because $(1-\varepsilon)\ln n<1$ for small $n$ .
Machine model. The machines are Cook's deterministic one-tape machines. Multi-tape simulation costs a quadratic factor, which the class absorbs.
Probabilities are uniform counts over the $(5n)^\ell$ random strings. Strategies are deterministic. Answers are canonical (satisfying on clause coordinates), as the paper assumes without loss of generality.
Not formalized. Randomized classes (ZTIME) are not defined here, so the following are omitted: the last sentence of Lemma 3.2, Proposition 6.1, and the randomized variants.
Ruling out a trivial formalization. The gap notion requires far-from-satisfiable formulas to have at least one clause. Otherwise the empty formula would be both a yes-instance and a no-instance, and Theorem 2.1.1 would hold trivially.
Infrastructure and reuse. The shared layer can serve other PCP-based hardness proofs: 3CNF-5 formulas, the $k$ $k$ -prover system, partition systems, and the gap-NP-hardness notion. Welcome contributions include:
- time bounds for list and table manipulations on one-tape machines;
- a Hadamard-code construction satisfying the weight and distance conditions;
- the union-bound and averaging lemmas behind Lemma 2.3.1 and Proposition 4.2.

Selected references

U. Feige, A threshold of ln n for approximating set cover, J. ACM 45(4), 634–652, 1998. https://doi.org/10.1145/285055.285059
C. Lund, M. Yannakakis, On the hardness of approximating minimization problems, J. ACM 41(5), 960–981, 1994. https://doi.org/10.1145/185675.306789
R. Raz, A parallel repetition theorem, SIAM J. Comput. 27(3), 763–803, 1998 (STOC 1995). https://doi.org/10.1137/S0097539795280895
M. Naor, L. J. Schulman, A. Srinivasan, Splitters and near-optimal derandomization, FOCS 1995, 182–191. https://doi.org/10.1109/SFCS.1995.492475
S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3), 501–555, 1998. https://doi.org/10.1145/278298.278306
C. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. Syst. Sci. 43(3), 425–440, 1991. https://doi.org/10.1016/0022-0000(91)90023-X
V. Chvátal, A greedy heuristic for the set-covering problem, Math. Oper. Res. 4(3), 233–235, 1979. https://doi.org/10.1287/moor.4.3.233
I. Dinur, D. Steurer, Analytical approach to parallel repetition, STOC 2014, 624–633. https://doi.org/10.1145/2591796.2591884

15 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Optimizing Static Linear Feedback: Gradient Method III: Gradient Descent with the Hessian Step Size Converges Linearly on Strongly Convex FunctionsResearch Paper

Motivation

Gradient descent needs a step size, and the classical choices each ask for something the user may not have. A constant step $1/L$ needs the Lipschitz constant $L$ of the gradient, which is rarely known and often pessimistic. Backtracking needs repeated function evaluations. The exact line search needs a one-dimensional minimization at every iteration. Fatkhullin and Polyak (arXiv:2004.09875v2, SIAM J. Control Optim. 2021, doi:10.1137/20M1329858) proposed a step size for the static linear-quadratic regulator (their rule (4.8), §4.3, p. 11). In §6.1 they point out that the same rule applies to any smooth unconstrained problem $\min_{x\in\mathbb{R}^n} f(x)$ . The rule divides the squared gradient norm by the Hessian quadratic form along the gradient. It needs one Hessian–vector product per iteration and neither $L$ nor the strong convexity constant $\mu$ . In the paper's LQR experiment (§5, Figure 8, p. 13) the algorithm built on this step converges much faster than gradient descent with a constant step tuned at the first iterations.

The paper proves the method converges linearly for strongly convex functions (Theorem 6.1, p. 13). The proof takes one page (Appendix D.4, p. 19). This mission formalizes that theorem. It is the third mission of a series on this paper; the other two concern the LQR gradient method and gradient flow, and this one uses none of their control-theoretic objects.

Setting

Let $f:\mathbb{R}^n\to\mathbb{R}$ be twice differentiable, with gradient $\nabla f(x)$ and Hessian $\nabla^2 f(x)$ . Three constants describe it.

$f$ is $\mu$ -strongly convex, $\mu>0$ : $f(ax+by)\le af(x)+bf(y)-ab\,\frac{\mu}{2}\|x-y\|^2$ for all $x,y$ and $a,b\ge0$ with $a+b=1$ .
$\nabla f$ is Lipschitz with constant $L$ : $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ .
$\nabla^2 f$ is Lipschitz with constant $M$ : $\|\nabla^2 f(x)-\nabla^2 f(y)\|\le M\|x-y\|$ in the operator norm.

Let $x_*$ be the global minimizer of $f$ . The Hessian step size at a point $x$ is

\gamma(x)=\frac{\|\nabla f(x)\|^2}{\langle\nabla^2 f(x)\nabla f(x),\nabla f(x)\rangle},

the minimizer of the second-order Taylor model of $f$ along $-\nabla f(x)$ . The method (6.1) runs

x_{j+1}=x_j-\gamma_j\nabla f(x_j),\qquad\gamma_j=\gamma(x_j),

from a starting point $x_0$ . The damped method with factor $\sigma>0$ runs $x_{j+1}=x_j-\sigma\gamma_j\nabla f(x_j)$ . For a quadratic $f(x)=\langle Hx,x\rangle$ the method (6.1) is steepest descent with exact line search.

Formalization targets

Goal: Theorem 6.1 (p. 13), both parts

Under the hypotheses above:

If $\delta>0$ and $M\sqrt{2L(f(x_0)-f(x_*))}\le3\mu^2(1-\delta)$ (condition (6.2)), the iterates of (6.1) satisfy

f(x_j)-f(x_*)\le\bigl(f(x_0)-f(x_*)\bigr)\Bigl(1-\frac{\mu\delta}{L}\Bigr)^j\quad\text{for all }j.\tag{6.3}

If $0<\sigma\le\mu/L$ , the damped iterates from any $x_0$ satisfy

f(x_j)-f(x_*)\le\bigl(f(x_0)-f(x_*)\bigr)\Bigl(1-\frac{\mu\sigma}{L}\Bigr)^j\quad\text{for all }j.\tag{6.4}

The constants are the paper's, stated exactly.

Milestones (Appendix D.4, p. 19)

Cubic Taylor bound (first display): $\bigl|f(x+y)-f(x)-\langle\nabla f(x),y\rangle-\frac12\langle\nabla^2 f(x)y,y\rangle\bigr|\le\frac M6\|y\|^3$ .
One-step inequality (third display): with $\varphi_j=f(x_j)$ , $\varphi_{j+1}\le\varphi_j-\frac12\gamma_j\|\nabla f(x_j)\|^2\bigl(1-\frac{M\gamma_j^2}{3}\|\nabla f(x_j)\|\bigr)$ .
(D.1): $f(y)\le f(x)+\langle\nabla f(x),y-x\rangle+\frac{L}{2\mu}\langle\nabla^2 f(x)(y-x),y-x\rangle$ .
(D.2): one damped step gives $f(x_{j+1})\le f(x_j)-\frac{\sigma\gamma_j}{2}\|\nabla f(x_j)\|^2$ .

Significance

Theorem 6.1 gives a rate for a step size computed from local second-order information alone. Part 1 says that near the minimizer the method converges at least as fast as gradient descent with step $\delta/L$ , with no step-size parameter to tune. Part 2 gives convergence from every starting point, at the price of knowing a lower bound on $\mu/L$ for the damping. The same step appears in the paper's LQR method (rule (4.8)) and in gradient projection methods (p. 13, citing [37]), so the one-step inequalities are reusable beyond this theorem.

The result is proved in the paper. As of this writing none of it has a machine-checked proof. The formal work is the full development: the cubic Taylor bound from a Lipschitz second derivative on $\mathbb{R}^n$ , the two one-step inequalities, and the inductions that give the rates.

Difficulty

The obvious argument for gradient descent uses the quadratic upper bound $f(y)\le f(x)+\langle\nabla f(x),y-x\rangle+\frac L2\|y-x\|^2$ and a step no larger than $2/L$ . The Hessian step can be as large as $1/\mu$ , far outside that range, so the quadratic bound in the Euclidean norm gives no decrease. Two different replacements are needed. For the undamped method, the cubic Taylor error must be controlled along the whole trajectory, and condition (6.2) is imposed only on $x_0$ : the proof must show the gradient stays small enough at every later iterate. For the damped method, the upper bound must be measured in the local Hessian norm (D.1), which trades the step's size for the condition number $L/\mu$ .

On the Lean side, Mathlib has Taylor's theorem in one variable. The cubic bound for a function on $\mathbb{R}^n$ with a Lipschitz Fréchet second derivative must be assembled from it or from the integral form along a segment. Mathlib has no ready-made link between strong convexity and a lower bound on the Hessian either.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). The gradient is Mathlib's gradient f. The Hessian quadratic form $\langle\nabla^2 f(x)v,v\rangle$ is fderiv ℝ (fderiv ℝ f) x v v. Twice differentiability is differentiability of f and of fderiv ℝ f everywhere. The Lipschitz constant of the Hessian is in the operator norm of the bilinear map, not the Frobenius norm. Strong convexity is StrongConvexOn Set.univ μ f with 0 < μ; Mathlib's modulus is $\frac\mu2\|x-y\|^2$ . $L$ and $M$ are real constants in the Lipschitz inequalities. The minimizer $x_*$ is a hypothesis ( $f(x_*)\le f(y)$ for all $y$ ), not constructed.

Deviations from the page, all recorded in the items' Formalization Notes:

The damping positivity $0<\sigma$ is added. It is implicit on the page.
The damped claim is stated under the full hypotheses of Theorem 6.1, including the Lipschitz Hessian, although its proof does not use $M$ .
The one-step inequality for (6.1) is stated under the strong convexity of Theorem 6.1, which keeps $\gamma\ge0$ . The gradient's Lipschitz constant is not assumed there.

At a stationary point the step is $0/0$ ; Lean evaluates it to $0$ , so the method stays at the minimizer, and both rates remain true.

The iterates are those of the defined recursions (6.1) and its damped version. A statement about an arbitrary sequence satisfying a descent inequality would be a different, weaker theorem and does not discharge the goal. Condition (6.2) is imposed on $x_0$ only; a version assuming it at every iterate is also not the goal.

Contributions welcome: the multivariate cubic Taylor bound (reusable wherever a Lipschitz Hessian appears, e.g. in cubic regularization of Newton's method); the Hessian bounds $\mu I\preceq\nabla^2 f\preceq LI$ from strong convexity and a Lipschitz gradient; and the inequality $\frac12\|\nabla f(x)\|^2\le L(f(x)-f(x_*))$ .

Selected references

I. Fatkhullin, B. Polyak, Optimizing Static Linear Feedback: Gradient Method, arXiv:2004.09875v2, 2020; SIAM J. Control Optim. 59(5), 2021. https://arxiv.org/abs/2004.09875 · https://doi.org/10.1137/20M1329858
Yu. Nesterov, B. T. Polyak, Cubic regularization of Newton method and its global performance, Math. Program. 108, 2006 (the cubic Taylor bound for Lipschitz Hessians). https://doi.org/10.1007/s10107-006-0706-8
B. T. Polyak, Introduction to Optimization, Optimization Software, 1987 (gradient methods, strong convexity).

6 thms3 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

The Generalized Quasi-Variational Inequality Problem I: Existence for the Generalized Implicit Complementarity Problem under Strong CopositivityResearch Paper

Motivation

Variational inequalities and complementarity problems are the standard formulation of equilibrium in operations research and mathematical economics: traffic equilibria, spatial price equilibria, Nash equilibria of convex games, and the optimality conditions of constrained optimization all take this form. Many applications have two features that the classical theory does not cover. The feasible set of a player or a flow can depend on the current state (a quasi-variational inequality, as in generalized Nash games with shared constraints), and the response map can be set-valued (a subdifferential, or a best-response correspondence). D. Chan and J. S. Pang (Math. Oper. Res. 7 (1982) 211–222) introduced the generalized quasi-variational inequality covering both, proved existence theorems for it, and derived existence for a new generalized implicit complementarity problem.

Timeline of the results this mission builds on:

1966: Hartman and Stampacchia prove existence for the variational inequality on a compact convex set.
1973: Bensoussan, Goursat and Lions introduce quasi-variational inequalities for impulse control.
1976: Saigal extends the complementarity problem to set-valued maps.
1974: Moré gives coercivity conditions for nonlinear complementarity problems; a special version of the lemma of §3 appears there.
1979: Fang and Peterson prove a general existence theorem for generalized variational inequalities (report, University of Maryland Baltimore County); the lemma of §3 and the constant- $K$ case of Theorem 3.2 are taken from there.
1982: Chan and Pang prove existence for the generalized quasi-variational inequality using the Eilenberg–Montgomery fixed point theorem, and derive existence for the generalized implicit complementarity problem under strong copositivity (Theorem 4.2), the goal of this mission.

Setting

Throughout, $\mathbb R^n$ carries the Euclidean inner product $x^T y$ and norm $\|x\|$ . A point-to-set mapping $K$ assigns to each $x\in\mathbb R^n$ a set $K(x)\subseteq\mathbb R^n$ . Given point-to-set mappings $K$ and $f$ , the problem $\mathrm{GQVI}(K,f)$ asks for vectors $x,y$ with

x\in K(x),\qquad y\in f(x),\qquad (x'-x)^T y\ge 0\ \text{ for all } x'\in K(x).

A cone is a convex set containing $0$ and closed under nonnegative scaling. The dual cone of a set $S$ is $S^*=\{y : y^T x\ge 0 \text{ for all } x\in S\}$ . For a point-to-point map $m$ , a cone-valued map $L$ and a point-to-set map $f$ , the problem $\mathrm{GICP}(L,m,f)$ asks for $x,y$ with

x\in m(x)+L(x),\qquad y\in f(x)\cap L(x)^*,\qquad y^T\big(x-m(x)\big)=0 .

A mapping $f$ is upper semicontinuous on a set $C$ at $x\in C$ if for each open $G\supseteq f(x)$ there is a neighbourhood $N$ of $x$ with $f(y)\subseteq G$ for $y\in N\cap C$ ; lower semicontinuous if for each open $G$ meeting $f(x)$ , $f(y)$ meets $G$ for all $y$ near $x$ in $C$ ; continuous if both. A set $S$ is contractible if some point $x\in S$ and a continuous $g:S\times[0,1]\to S$ satisfy $g(x',0)=x'$ , $g(x',1)=x$ . $B_r$ is the closed ball of radius $r$ about the origin, $C_r$ its boundary sphere. For point-to-set maps $\mu$ and $K$ , the coercivity function is

C_{\mu,K}(r,x^0)=\inf_{x\in K(x)\cap C_r}\Big[\inf_{y\in\mu(x)}(x-x^0)^T y\Big]\Big/(r+\|x^0\|),

with $\inf\emptyset=+\infty$ . The map $\mu$ is strongly copositive with respect to $K$ at $x^0$ if $x^0\in K(x^0)$ and for some $\alpha>0$ and $y^0\in\mu(x^0)$ , $(y-y^0)^T(x-x^0)\ge\alpha\|x-x^0\|^2$ for all $x\in K(x)$ and $y\in\mu(x)$ . For $\mu$ and $q\in\mathbb R^n$ , $(\mu+q)(x)=\{y+q : y\in\mu(x)\}$ .

Formalization targets

Goal: Theorem 4.2 (p. 218)

Let $\tilde L$ be a closed cone with nonempty interior, $m$ continuous, $K(x)=m(x)+\tilde L$ , and $\mu$ a mapping with nonempty contractible compact values, upper semicontinuous on $\mathbb R^n$ . If some $\tilde u$ satisfies $\tilde u-m(x)\in\tilde L$ for all $x$ , and $\mu$ is strongly copositive with respect to $K$ at $\tilde u$ , then for every $q$

\exists\, x,y:\quad x-m(x)\in\tilde L,\quad y\in\mu(x)+q,\quad y\in\tilde L^*,\quad y^T(x-m(x))=0 .

Milestones, in the order the proof uses them

Theorem 3.1 (p. 214): for continuous $\varphi$ quasi-concave in its first argument on a nonempty compact convex $C$ , some $u^*\in V(u^*)=K(u^*)\cap C$ and $w^*\in f(u^*)$ satisfy $\varphi(v,u^*,w^*)\le\varphi(u^*,u^*,w^*)$ for all $v\in V(u^*)$ .
Lemma of §3 (p. 215): a variational inequality on $W\cap E$ at a point of $W\cap E^0$ extends to $W$ .
Theorem 3.2 (p. 215): existence for $\mathrm{GQVI}(K,f)$ from a compact truncation $C=U\cap E$ and a boundary condition on $\partial E$ .
Theorem 4.1 (p. 217): if $C_{\mu,K}(r,x^0)\ge 0$ , then $\mathrm{GQVI}(K,\mu+q)$ has a solution in $B_r$ whenever $\|q\|\le C_{\mu,K}(r,x^0)$ .
Corollary 4.1 (pp. 217–218): under the coercivity condition (4), $\mathrm{GQVI}(K,\mu+q)$ is solvable for every $q$ , with bounded solution set.
Lemma 4.1 (p. 218): strong copositivity at $x^0$ implies coercivity (4) at $x^0$ .
Proposition 2.1 (p. 213): $\mathrm{GICP}(L,m,f)$ and $\mathrm{GQVI}(m+L,f)$ have the same solutions.

Significance

Theorem 4.2 gives existence for complementarity problems whose cone is translated by a state-dependent map $m$ and whose response map is set-valued. It contains existence for the implicit complementarity problem of Capuzzo-Dolcetta, Mosco and Pang ( $\tilde L=\mathbb R^n_+$ ) with strongly monotone data (Corollary 4.2 of the paper), and Saigal's generalized complementarity problem ( $m\equiv0$ ). Theorems 3.2 and 4.1 are general-purpose existence tools for quasi-variational inequalities with set-valued maps; Theorem 3.2 reduces to the Fang–Peterson theorem when $K$ is constant, and Corollary 3.1 to the Hartman–Stampacchia theorem when in addition $f$ is single-valued.

All results of the paper are proved; none is open. To our knowledge none of them has been formalized: no proof assistant library contains quasi-variational inequalities with set-valued maps, and Mathlib has neither Kakutani's nor the Eilenberg–Montgomery fixed point theorem (nor Brouwer's). A formal proof of the goal therefore also produces a reusable library of set-valued existence theory.

Difficulty

The whole chain rests on Theorem 3.1, whose proof applies the Eilenberg–Montgomery fixed point theorem for upper semicontinuous maps with acyclic (here contractible) compact values; this in turn needs either singular homology or an approximation argument, neither of which is available in Mathlib. Replacing "contractible" by "convex" to use Kakutani's theorem would prove a strictly weaker theorem: the paper states contractible values deliberately. The second difficulty is that the fixed point only solves the problem on the truncation $V(x)=K(x)\cap C$ ; turning it into a solution over all of $K(x)$ needs the boundary argument of Theorem 3.2, and for Theorem 4.2 the continuity of $x\mapsto (m(x)+\tilde L)\cap B_\rho$ , which is where the solidity of $\tilde L$ is used. The obvious approach of applying Theorem 3.2 directly with $C=\mathbb R^n$ fails because $C$ must be compact.

Formalization scope

The space is EuclideanSpace ℝ (Fin n), so all norms and balls are Euclidean (not the sup norm of Fin n → ℝ). Point-to-set mappings are functions into Set; semicontinuity "on $C$ " is Mathlib's UpperHemicontinuousOn/LowerHemicontinuousOn with neighbourhoods relative to $C$ , and "on $\mathbb R^n$ " is UpperHemicontinuous. Cones are PointedCone ℝ _ (convex, containing $0$ , as footnote 1 of the paper says). Balls are centred at the origin.

Conventions that the Lean statements make explicit:

The paper takes its semicontinuity from Berge, whose upper semicontinuous maps have compact values. Theorems 3.1, 3.2, 4.1 and Corollary 4.1 are false without this ( $K(x)\equiv(0,1)$ , $C=[0,1]$ , $f\equiv\{1\}$ ), so each one carries an explicit closedness hypothesis on $K(x)\cap C$ or $K(x)\cap B_\rho$ . Theorem 4.2 needs none, since $m(x)+\tilde L$ is closed.
Every infimum uses $\inf\emptyset=+\infty$ . Bounds of the form $C_{\mu,K}(r,x^0)\ge c$ , condition (v) of Theorem 3.2, and the limit (4) are stated in universally quantified form. A real-valued $C_{\mu,K}$ would be wrong: it returns $0$ on an empty set.
Lemma 4.1 is stated at the same point $x^0$ , which is what its proof gives. In Corollary 4.1 the bound $r$ on the solutions is chosen after $q$ .
Three glyphs are illegible in the scan and are read from the proofs: $\le$ in Theorem 3.1, $\ge 0$ in Theorem 3.2(v), and $\ge$ in the Lemma of §3.

A trivializing formalization is ruled out: the GQVI solution tests over all of $K(x)$ , not over $V(x)=K(x)\cap C$ , and the GICP solution keeps both the dual-cone condition and the complementarity equation. Dropping any of these would turn the goal into a restatement of Theorem 3.1.

A complete development needs: an Eilenberg–Montgomery (or at least Kakutani plus an acyclicity argument) fixed point theorem for set-valued maps, Berge's maximum theorem, and basic facts on hemicontinuity of intersections and translates of set-valued maps. The fixed point theorems, the maximum theorem and the hemicontinuity lemmas are reusable far beyond this mission. Contributions of any of these as separate theorems are welcome.

Selected references

D. Chan, J. S. Pang, The generalized quasi-variational inequality problem, Mathematics of Operations Research 7(2) (1982) 211–222. https://doi.org/10.1287/moor.7.2.211
S. Eilenberg, D. Montgomery, Fixed point theorems for multi-valued transformations, American Journal of Mathematics 68 (1946) 214–222. https://doi.org/10.2307/2371832
C. Berge, Topological Spaces, Macmillan, New York, 1963.
S. C. Fang, E. L. Peterson, Generalized variational inequalities, Mathematics Research Report 79-10, Department of Mathematics, University of Maryland Baltimore County, 1979 (no public link).
J. J. Moré, Coercivity conditions in nonlinear complementarity problems, SIAM Review 16(1) (1974) 1–16. https://doi.org/10.1137/1016001
P. Hartman, G. Stampacchia, On some non-linear elliptic differential-functional equations, Acta Mathematica 115 (1966) 271–310. https://doi.org/10.1007/BF02392210
R. Saigal, Extension of the generalized complementarity problem, Mathematics of Operations Research 1(3) (1976) 260–266. https://doi.org/10.1287/moor.1.3.260

12 thms3 active usersReviewed

Completed

Convex Optimization Numerical Analysis Operations Research+1·Captain: mikedeng1

Projected Gradient Methods for Linearly Constrained Problems I: The Gradient Projection Method Drives the Projected Gradients to ZeroResearch Paper

Motivation

The gradient projection method minimizes a continuously differentiable function over a closed convex set by alternating a gradient step with a projection back onto the set. It was proposed by Goldstein (1964) and by Levitin and Polyak (1966), and it is the basic step of many algorithms for bound constrained and linearly constrained optimization, including large-scale quadratic programming codes.

The classical convergence results either need a Lipschitz constant for the gradient to choose the step (Goldstein; Levitin–Polyak), or assume a bounded sequence of iterates and conclude only that limit points are stationary (Bertsekas, 1976, for the Armijo rule on a box; Dunn, 1981). Calamai and Moré (1987) introduced a general step-size rule that contains the Armijo procedure, and proved a convergence statement that needs no boundedness of the iterates: the projected gradients tend to zero. This statement is what later results on finite identification of the active constraints use as their hypothesis, so it is the natural entry point to the paper.

Setting

Let $E$ be a finite-dimensional real inner product space with norm $\|\cdot\|$ , let $\Omega \subseteq E$ be nonempty, closed and convex, and let $f : E \to \mathbb R$ be continuously differentiable on $\Omega$ , with gradient $\nabla f$ taken with respect to the inner product. The problem is

\min\{f(x) : x \in \Omega\}. \qquad (1.1)

The projection into $\Omega$ is $P(x) = \operatorname{argmin}\{\|z - x\| : z \in \Omega\}$ , the unique nearest point of $\Omega$ to $x$ (Eq. (1.3)).
A point $x^* \in \Omega$ is stationary if $\langle \nabla f(x^*), x - x^* \rangle \ge 0$ for all $x \in \Omega$ (Eq. (1.5)).
A direction $v$ is feasible at $x \in \Omega$ if $x + \tau v \in \Omega$ for all sufficiently small $\tau > 0$ ; the tangent cone $T(x)$ is the closure of the set of feasible directions.
The projected gradient is $\nabla_\Omega f(x) = \operatorname{argmin}\{\|v + \nabla f(x)\| : v \in T(x)\}$ (Eq. (3.1)), the nearest point of $T(x)$ to $-\nabla f(x)$ .

A run of the gradient projection method is a pair of sequences $(x_k)_{k\ge0}$ , $(\alpha_k)_{k \ge 0}$ with $x_0 \in \Omega$ , $\alpha_k > 0$ and $x_{k+1} = x_k(\alpha_k)$ , where $x_k(\alpha) = P(x_k - \alpha \nabla f(x_k))$ . For fixed constants $\gamma_1, \gamma_2 > 0$ and $\mu_1, \mu_2 \in (0,1)$ , the steps satisfy the sufficient decrease condition

f(x_{k+1}) \le f(x_k) + \mu_1 \langle \nabla f(x_k), x_{k+1} - x_k\rangle \qquad (2.1)

and the condition that the step is not too small: either $\alpha_k \ge \gamma_1$ , or $\alpha_k \ge \gamma_2 \bar\alpha_k > 0$ for some $\bar\alpha_k$ at which sufficient decrease fails,

f(x_k(\bar\alpha_k)) > f(x_k) + \mu_2 \langle \nabla f(x_k), x_k(\bar\alpha_k) - x_k \rangle. \qquad (2.2)\text{–}(2.3)

In Lean these objects are proj, projGrad and IsGradientProjectionRun in the namespace CalamaiMore.Convergence, together with the shared definitions tangentCone and IsStationaryPoint in CalamaiMore.Shared.

Formalization targets

Goal: Theorem 3.2

If, in addition, the steps are bounded, $\alpha_k \le \gamma_3$ for some constant $\gamma_3$ (3.2), $f$ is bounded below on $\Omega$ , and $\nabla f$ is uniformly continuous on $\Omega$ , then

\lim_{k \to \infty} \|\nabla_\Omega f(x_k)\| = 0.

No boundedness of $\{x_k\}$ is assumed, and no specific step rule beyond (2.1)–(2.3).

Milestones

Lemma 2.1: $P$ satisfies the variational inequality $\langle P(x) - x, z - P(x)\rangle \ge 0$ for $z \in \Omega$ , is monotone (strictly when $P(y) \ne P(x)$ ) and nonexpansive.
Eqs. (2.4)–(2.5): $\langle \nabla f(x_k), x_k - x_k(\alpha)\rangle \ge \|x_k(\alpha) - x_k\|^2/\alpha$ for $\alpha > 0$ , and its instance at $\alpha = \alpha_k$ .
Lemma 2.2: $\alpha \mapsto \|P(x + \alpha d) - x\|/\alpha$ is nonincreasing on $(0, \infty)$ .
Theorem 2.3: under the hypotheses of the goal without (3.2), $\|x_{k+1} - x_k\|/\alpha_k \to 0$ .
Lemma 3.1: $-\langle \nabla f(x), \nabla_\Omega f(x) \rangle = \|\nabla_\Omega f(x)\|^2$ ; $\min\{\langle \nabla f(x), v\rangle : v \in T(x), \|v\| \le 1\} = -\|\nabla_\Omega f(x)\|$ ; and $x$ is stationary if and only if $\nabla_\Omega f(x) = 0$ .
Theorem 2.4: if some subsequence $\{x_k : k \in K\}$ is bounded, $\|x_{k+1} - x_k\|/\alpha_k \to 0$ along $K$ , and every limit point of $\{x_k\}$ is stationary.
Lemma 3.3: $x \mapsto \|\nabla_\Omega f(x)\|$ is lower semicontinuous on $\Omega$ .
Theorem 3.4: with (3.2) and a bounded subsequence $\{x_k : k \in K\}$ , $\|\nabla_\Omega f(x_{k+1})\| \to 0$ along $K$ .

Significance

By Lemma 3.1, $\|\nabla_\Omega f(x)\|$ vanishes exactly at stationary points, so Theorem 3.2 says that the method approaches stationarity in a quantitative sense even when the iterates are unbounded. With Lemma 3.3 it gives that every limit point is stationary. For polyhedral $\Omega$ it is the hypothesis of the paper's Theorem 4.1: any sequence with $\nabla_\Omega f(x_k) \to 0$ converging to a nondegenerate point identifies the active constraints in finitely many iterations, which is the basis of active-set methods that switch between gradient projection steps and subspace minimization.

The results are proved in the paper. To our knowledge they have no machine-checked proof. This mission produces a formal account of the gradient projection method with a general step rule, a reusable projected gradient and tangent cone on a general finite-dimensional inner product space, and the standard projection estimates of §2, which are also the starting point of the paper's other two main results.

Difficulty

The obvious argument fails at two places. First, the continuity of $\nabla_\Omega f$ cannot be used: the map $x \mapsto \nabla_\Omega f(x)$ is not continuous, and $\|\nabla_\Omega f\|$ can be bounded away from zero in every neighborhood of a stationary point, because the tangent cone changes discontinuously at the boundary of $\Omega$ . So $x_k \to x^*$ with $x^*$ stationary does not by itself force $\nabla_\Omega f(x_k) \to 0$ , and here the iterates need not converge at all. Second, the steps $\alpha_k$ may tend to zero along a subsequence; the step rule gives information only through a trial step $\bar\alpha_k$ , at a point other than $x_{k+1}$ , and comparing the two projected steps is where the argument must work.

Formalization scope

The space is a type E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]; $\nabla f$ is Mathlib's gradient f. "Continuously differentiable on $\Omega$ " is ∀ x ∈ Ω, DifferentiableAt ℝ f x together with ContinuousOn (gradient f) Ω. Bounded below is BddBelow (f '' Ω), uniform continuity is UniformContinuousOn (gradient f) Ω. Sequences are ℕ → E indexed from $0$ ; a subsequence is an infinite K : Set ℕ with limits along atTop ⊓ 𝓟 K; a limit point is a MapClusterPt. The projection and the projected gradient are total functions through a nearest-point map that returns $0$ when no nearest point exists; every theorem assumes $\Omega$ nonempty, closed and convex, and evaluates $\nabla_\Omega f$ only at points of $\Omega$ , where the nearest point exists and is unique. The step rule is a predicate on the pair of sequences, so the theorems cover every rule satisfying (2.1)–(2.3); the auxiliary condition $\mu_1 \le \mu_2$ , which the paper uses only to show that an admissible step exists, is not imposed.

The run predicate is satisfiable: for a constant $f$ , the constant sequence $x_k = x_0 \in \Omega$ with $\alpha_k = \gamma_1$ is a run, so the goal is not vacuous. A formalization that states the goal for an arbitrary map in place of the projection, drops the bound $\alpha_k \le \gamma_3$ , or replaces $\|\nabla_\Omega f(x_k)\|$ by $\|x_{k+1} - x_k\|/\alpha_k$ proves a different theorem and is not accepted.

Contributions welcome: the projection estimates (reusable for any projection-based method), existence and uniqueness of the projected gradient, the characterization of stationarity, and the two limit theorems.

Selected references

P. H. Calamai, J. J. Moré, Projected gradient methods for linearly constrained problems, Mathematical Programming 39 (1987) 93–116. https://doi.org/10.1007/BF02592073
A. A. Goldstein, Convex programming in Hilbert space, Bulletin of the AMS 70 (1964) 709–710. https://doi.org/10.1090/S0002-9904-1964-11178-2
E. S. Levitin, B. T. Polyak, Constrained minimization methods, USSR Computational Mathematics and Mathematical Physics 6 (1966) 1–50. https://doi.org/10.1016/0041-5553(66)90114-5
D. P. Bertsekas, On the Goldstein–Levitin–Polyak gradient projection method, IEEE Transactions on Automatic Control 21 (1976) 174–184. https://doi.org/10.1109/TAC.1976.1101194
J. C. Dunn, Global and asymptotic convergence rate estimates for a class of projected gradient processes, SIAM Journal on Control and Optimization 19 (1981) 368–400. https://doi.org/10.1137/0319022
E. M. Gafni, D. P. Bertsekas, Two-metric projection methods for constrained optimization, SIAM Journal on Control and Optimization 22 (1984) 936–964. https://doi.org/10.1137/0322061

15 thms3 active usersReviewed

Completed

Combinatorics Linear Optimization Operations Research+1·Captain: mikedeng1

Proximity Results and Faster Algorithms for Integer Programming Using the Steinitz Lemma: ℓ1-Proximity of Integer and LP OptimaResearch Paper

Motivation

Integer programs are routinely solved by first solving their linear programming (LP) relaxation and then searching for an integer optimum near the fractional one. How near an integer optimum must be is the subject of proximity theorems. They bound the search region of branch-and-bound and of dynamic programming, and they turn a fractional optimum into a starting point for exact algorithms.

The classical bound is due to Cook, Gerards, Schrijver and Tardos (Math. Programming 34, 1986): for an integer program in inequality form $\max\{c^Tx : Ax\le b,\ x\in\mathbb Z^n\}$ that is feasible and bounded, every optimal LP solution $x^*$ has an optimal integer solution $z^*$ with $\|x^*-z^*\|_\infty\le n\cdot\delta$ , where $\delta$ is the largest absolute value of a subdeterminant of $A$ . For programs in standard form $Ax=b$ with $m$ rows this gives, via the Hadamard bound, $\|z^*-x^*\|_1\le n^2\cdot m^{m/2}\Delta^m$ , which grows with the number of variables $n$ .

Eisenbrand and Weismantel (ACM Trans. Algorithms 16(1), Article 5, 2019; conference version SODA 2018) removed the dependence on $n$ altogether, using the Steinitz lemma on rearranging vectors so that all partial sums stay short. Their bound depends only on $m$ and on the largest absolute value $\Delta$ of an entry of $A$ , and it is the basis of their faster algorithms for integer programs with few constraints.

Setting

Fix natural numbers $m$ (rows) and $n$ (variables). The data are a matrix $A\in\mathbb Z^{m\times n}$ , a right-hand side $b\in\mathbb Z^m$ , an objective $c\in\mathbb Z^n$ and upper bounds $u\in\mathbb N^n$ . A natural number $\Delta$ bounds the entries: $|a_{ij}|\le\Delta$ for all $i,j$ . The integer program (10) is

\max\{c^Tx : Ax=b,\ 0\le x\le u,\ x\in\mathbb Z^n\},

and its LP relaxation is the same problem over $x\in\mathbb R^n$ . Its feasible region $P=\{x\in\mathbb R^n: Ax=b,\ 0\le x\le u\}$ is a polytope, lpPolytope A b u. An optimal vertex solution is an optimal solution of the LP relaxation (IsLPOptimal) that is an extreme point of $P$ . An optimal integer solution is IsIPOptimal. Both are maxima.

Distances are measured in the $\ell_1$ -norm $\|z-x\|_1=\sum_i|z_i-x_i|$ .

A vector $y\in\mathbb Z^n$ is a cycle of $z^*-x^*$ (Eq. (14)) if $Ay=0$ and, for every $i$ , $|y_i|\le|(z^*-x^*)_i|$ and $y_i(z^*-x^*)_i\ge0$ : an integer kernel vector that is sign-compatible with $z^*-x^*$ and dominated by it (IsCycle).

The Steinitz lemma (Theorem 1.1) concerns vectors $x_1,\dots,x_n$ in an $m$ -dimensional normed space with $\sum_i x_i=0$ and $\|x_i\|\le1$ . It asserts a permutation $\pi$ with $\|\sum_{j\le k}x_{\pi(j)}\|\le c(m)$ for all $k$ , and the paper uses Sevast'anov's constant $c(m)=m$ .

Formalization targets

Goal: Theorem 3.3 (p. 5:8)

If (10) has an integer feasible point and $x^*$ is an optimal vertex solution of its LP relaxation, then there is an optimal solution $z^*$ of (10) with

\|z^*-x^*\|_1\ \le\ m\cdot(2m\Delta+1)^m .

The constant is the paper's. The goal holds for all $m$ , $n$ , $b$ , $c$ and $u$ ; only $m$ and $\Delta$ enter the bound.

Milestones, in the order the proof uses them

Lemma 3.1 (p. 5:8): for an LP optimum $x^*$ , an integer optimum $z^*$ and a cycle $y$ of $z^*-x^*$ , the vector $z^*-y$ is integer feasible, $x^*+y$ is LP feasible, and $c^Ty\le0$ .
Lemma 3.2 (p. 5:8): if $z^*$ minimizes $\|z^*-x^*\|_1$ among the optimal integer solutions, then $z^*-x^*$ has no nonzero cycle.
Theorem 1.1 with $c(m)=m$ (p. 5:4): the Steinitz lemma in any $m$ -dimensional real normed space.
Proof of Theorem 3.3 (pp. 5:8–5:9): round a vertex $x^*$ towards an integer vector and write $\{x^*\}$ for the remainder. Then $\|-A\{x^*\}\|_\infty\le\Delta m$ and $-A\{x^*\}=w_1+\dots+w_m$ with integer $w_j$ , $\|w_j\|_\infty\le\Delta$ .
Proof of Theorem 3.3, Eq. (20) (p. 5:9): a sequence of integer vectors of $\ell_\infty$ -norm at most $m\Delta$ in which no value repeats $m+1$ times has length at most $m(2m\Delta+1)^m$ .
Eq. (21) (p. 5:9), a consequence: $c^T(x^*-z^*)\le\|c\|_\infty\cdot m(2m\Delta+1)^m$ for every optimal integer solution $z^*$ .

Significance

The bound is independent of the number of variables. Combined with the paper's dynamic program, it gives the paper's running-time results for integer programs with upper bounds: an optimal LP vertex is computed, and the integer optimum is searched for within an $\ell_1$ -ball of radius $m(2m\Delta+1)^m$ around it. Eq. (21) bounds the absolute integrality gap by the same quantity, scaled by $\|c\|_\infty$ . The Steinitz lemma with constant $m$ is a general tool in discrepancy theory and in scheduling algorithms.

All of these results have published proofs. No machine-checked proof of Theorem 3.3 or of the Steinitz lemma is known to this mission, and Mathlib has no Steinitz lemma. The mission asks for complete Lean proofs of the milestones and of the goal. A proof of the Steinitz lemma with constant $m$ for arbitrary norms is reusable well beyond integer programming.

Difficulty

Lemmas 3.1 and 3.2 and the counting step are elementary. The substance lies in two places. The first is the Steinitz lemma with the linear constant $m$ for an arbitrary norm: the bound must hold uniformly in the number $n$ of vectors, and the constant must be exactly $m$ , because the goal's constant $(2m\Delta+1)^m$ counts integer points of $\ell_\infty$ -norm at most $m\Delta$ . The second is the passage from a vertex to at most $m$ fractional coordinates. The paper argues this in one sentence (" $x^*$ has at most $m$ positive entries"), which is not literally true for (10) with upper bounds: coordinates at their upper bound $u_i>0$ are positive. The correct fact concerns coordinates strictly between $0$ and $u_i$ , and it has to be derived from the extreme-point property of $P$ .

Formalization scope

All declarations live in the namespace IPProximity.Eisenbrand. The data are integral: A : Matrix (Fin m) (Fin n) ℤ, b : Fin m → ℤ, c : Fin n → ℤ, u : Fin n → ℕ (entries $u_i=0$ allowed), Δ : ℕ. They are cast to ℝ once, inside the LP definitions. $m=0$ and $n=0$ are allowed.
"Vertex" is Mathlib's Set.extremePoints ℝ (lpPolytope A b u). It is not defined through bases or by counting fractional coordinates.
The $\ell_1$ -distance is the explicit sum ∑ i, |(z i : ℝ) - x i|. Mathlib's norm on Fin n → ℝ is the sup norm, and it is used only where the paper has $\|\cdot\|_\infty$ (the $\|c\|_\infty$ of Eq. (21)).
The goal adds one hypothesis the paper leaves implicit: (10) has an integer feasible point. The paper's proof begins with "Let $z^*$ be an optimal integer solution"; without this hypothesis the conclusion is false.
Eq. (14) is formalized literally, so $y=0$ is a cycle, and Lemma 3.2 is stated for nonzero cycles, which is what its proof establishes. Dropping the vertex hypothesis would make the goal false, so the goal keeps it. The constant is exactly $m(2m\Delta+1)^m$ , with no hidden existential constant.
The Steinitz milestone is stated for any finite-dimensional real normed space of dimension $m$ with the explicit constant $m$ . The goal needs only the $\ell_\infty$ case on $\mathbb R^m$ .
Out of scope: the dynamic program and the running-time theorems of Sections 2 and 4, and the refinement $\|z^*-x^*\|_1\le2\Delta$ for $m=1$ .

Contributions welcome: proofs of any milestone, in particular the Steinitz lemma, and a proof of the goal from the milestones.

Selected references

F. Eisenbrand, R. Weismantel, Proximity Results and Faster Algorithms for Integer Programming Using the Steinitz Lemma, ACM Transactions on Algorithms 16(1), Article 5, 2019. https://doi.org/10.1145/3340322
W. Cook, A. M. H. Gerards, A. Schrijver, É. Tardos, Sensitivity theorems in integer linear programming, Mathematical Programming 34, 251–264, 1986. https://doi.org/10.1007/BF01582230
E. Steinitz, Bedingt konvergente Reihen und konvexe Systeme, Journal für die reine und angewandte Mathematik 143, 128–176, 1913. https://doi.org/10.1515/crll.1913.143.128
S. Sevast'janov, Approximate solution of some problems of scheduling theory (in Russian), Metody Diskretnogo Analiza 32, 66–75, 1978 (reference [31] of the paper).
V. S. Grinberg, S. V. Sevast'yanov, Value of the Steinitz constant, Functional Analysis and Its Applications 14(2), 125–126, 1980 (reference [16] of the paper).

12 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems 2: The Augmentation Bound for Maximum-Augmentation PathsResearch 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 arcs have capacities. It underlies bipartite matching, transportation, scheduling and many reductions in combinatorial optimization. The classical method for it, the labeling method of Ford and Fulkerson (Flows in Networks, 1962), repeatedly finds an augmenting path and pushes flow along it. With integer capacities it terminates, but the number of augmentations can be as large as the maximum flow value itself, and Edmonds and Karp exhibit a four-node network on which this happens (p. 250). With irrational capacities the method need not terminate at all.

Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, J. ACM 19(2):248–264, 1972 (doi:10.1145/321694.321699), showed that two simple rules for choosing the augmenting path repair this. The first, augmenting along a path with fewest arcs, is the subject of mission 1 of this series. This mission covers the second (§1.3): augment along a path that gives the largest possible augmentation. For integer capacities the number of augmentations then grows only logarithmically in the maximum flow value.

Setting

A network $N$ has a finite set $V$ of nodes, a source $s$ and a sink $t \neq s$ , and a set of arcs, ordered pairs $(u,v)$ with $u \neq v$ , at most one from each node to another. One arc is the return arc $(t,s)$ ; the other arcs form the set $A$ , and each $(u,v) \in A$ has a capacity $c(u,v) > 0$ . A flow is a nonnegative function $f$ on the arcs of $N$ with $f(u,v) \le c(u,v)$ on $A$ and flow conservation at every node, $s$ and $t$ included. Its value is $f(t,s)$ , the flow returned along the return arc; a maximum flow has the largest value among all flows, and $f^*(t,s)$ denotes that value.

The residual network $N^f$ has an arc $(u,v)$ whenever $(u,v) \in A$ and $c(u,v) - f(u,v) > 0$ , or $(v,u) \in A$ and $f(v,u) > 0$ . An augmenting path is a directed path $s = u_1, \dots, u_p = t$ of distinct nodes in $N^f$ . Each of its arcs $(u,v)$ has a residual amount $e(u,v)$ , equal to $c(u,v) - f(u,v)$ , $f(v,u)$ , or $c(u,v) - f(u,v) + f(v,u)$ according to which of $(u,v)$ , $(v,u)$ lie in $A$ , and the path's augmentation is $\varepsilon = \min e(u_i, u_{i+1})$ . Augmenting increases $f(t,s)$ by $\varepsilon$ and changes the flow on the arcs of the path accordingly, with the paper's own rule when both $(u,v)$ and $(v,u)$ are arcs. The labeling method produces flows $f^0, f^1, \dots$ by augmenting along a path relative to $f^k$ as long as one exists.

The rule studied here chooses, at every step, an augmenting path whose $\varepsilon$ is at least that of every other augmenting path relative to the current flow. The bound involves an integer $M > 1$ such that every partition of the nodes into $X \ni s$ and $\bar X \ni t$ has at most $M$ arcs of $N$ with one end on each side.

Formalization targets

Goal: Theorem 2 (p. 253)

For a network with integer capacities, $M$ as above, and a run $f^0, \dots, f^K$ of the labeling method with maximum augmentations started from an integer-valued flow,

K \;\le\; 1 + \log_{M/(M-1)} f^*(t,s),

and if no augmenting path relative to $f^K$ exists, then $f^K$ is a maximum flow.

Milestones

The milestone list follows the paper's argument:

augmentation produces a flow of value $f(t,s) + \varepsilon$ (§1.1, p. 249);
a flow is maximum if and only if it has no augmenting path (§1.1, pp. 249–250);
with integer capacities, $\varepsilon$ is a positive integer and the flows of the method stay integer-valued (§1.1, p. 250);
the cut inequality $c(X,\bar X) \ge f(X,\bar X) - f(\bar X,X) = f(t,s)$ (p. 254);
$f^*(t,s) - f^k(t,s) \le \varepsilon^k M$ , where $\varepsilon^k = f^{k+1}(t,s) - f^k(t,s)$ (p. 254);
$f^*(t,s) - f^{k+1}(t,s) \le [f^*(t,s) - f^k(t,s)](1 - M^{-1})$ (p. 254);
$f^*(t,s) - f^k(t,s) \le f^*(t,s)(1 - M^{-1})^k$ (p. 254).

Significance

Theorem 2 was among the first bounds showing that a maximum flow algorithm can be made polynomial in the size of the numbers rather than in their values: since $M \le n^2/2$ and $f^*(t,s)$ is at most $n^2$ times the average capacity, the bound is $O(n^2 \log(n^2 \bar c))$ in terms of the number of nodes $n$ and the average capacity $\bar c$ (p. 254). The largest-augmentation rule, often called the fattest-path or maximum-capacity augmenting path rule, is a standard textbook variant, and its geometric-decrease argument is the model for later capacity-scaling methods, including the scaling algorithm for the Hitchcock problem in §2 of the same paper (mission 3 of this series).

The theorem has been proved since 1972 and appears in standard texts. As far as a platform search shows (2026-09-26), no machine-checked proof of it exists on Prove2Me. The platform does contain LinearOptimization.max_flow_min_cut and LinearOptimization.max_flow_ford_fulkerson_integer_termination, which state max-flow min-cut and termination of the generic method in a different network model (parallel arcs, extended nonnegative capacities, no return arc); they give no count of augmentations and are related work only. This mission would contribute a formal proof of the counting bound together with the general labeling-method facts (milestones 1–3), which mission 1 needs as well.

Difficulty

The obvious argument, that each augmentation raises the value by at least 1, gives only the bound $f^*(t,s)$ , and on the four-node example of p. 250 that bound is attained by an arbitrary choice of paths. The logarithmic bound needs a lower bound on the size of the largest augmentation in terms of the remaining gap $f^*(t,s) - f^k(t,s)$ . The largest augmentation is defined by comparison with all augmenting paths relative to the current flow, while the gap is a global quantity of the network, and neither integrality nor the maximum-augmentation rule alone controls it. Milestone 2's converse, that a non-maximum flow always admits an augmenting path, is itself the max-flow min-cut theorem in this model, and the formal proof has to establish it for the paper's return-arc model rather than import it from a different one.

Formalization scope

Nodes form a finite type V with decidable equality. A : Finset (V × V) contains no loops and not $(t,s)$ . Capacities are real, c : V → V → ℝ, positive on A. Integrality is the hypothesis IntegralCaps N, and for the initial flow IsIntegralOn N (f 0) (integer values on the arcs of $N$ , the return arc included).
Flows are functions V → V → ℝ constrained only on the arcs of $N$ . A maximum flow is the predicate IsMaxFlow, comparing $f(t,s)$ with every flow, not a supremum. The goal takes a maximum flow g as a hypothesis and sets $f^*(t,s) = g(t,s)$ ; every network has one.
Augmenting paths are duplicate-free node lists whose consecutive pairs are arcs of $N^f$ . The page prints Case (b) of the definition of $\varepsilon_i$ with the same hypothesis as Case (c); the corrected Case (b), $(u,v) \notin A$ and $(v,u) \in A$ , is used, as the definition of $N^f$ (p. 251) and the list for $e(u,v)$ (p. 253) confirm.
A run is IsMaxAugRun N K f P. Its initial flow is arbitrary except for integrality, and each later flow is the augmentation of the previous one along a path of maximum $\varepsilon$ among all augmenting paths.
The crossing bound CrossArcsBounded N M counts the arcs of $N$ , return arc included, with one end on each side of every $s$ – $t$ partition. This is the literal reading of p. 253.
Explicit constants. The bound is exactly $1 + \log_{M/(M-1)} f^*(t,s)$ , written (K : ℝ) ≤ 1 + Real.logb ((M : ℝ) / ((M : ℝ) - 1)) (g N.t N.s) with $M > 1$ a natural number. When $f^*(t,s) = 0$ , Real.logb gives $0$ and the bound reads $K \le 1$ . The contraction factor is 1 - (M : ℝ)⁻¹.
A statement that bounds only runs of an unsatisfiable step predicate, drops the integrality of $f^0$ or of the capacities (the bound is false without them), or compares $\varepsilon$ only among paths of some restricted class does not formalize Theorem 2. A sorry-free check exhibits a four-node network with integer capacities and a valid maximum-augmentation step.
Reusable beyond this mission: the return-arc network model, the augmentation step with the paper's opposite-arc rule, the integrality lemma, and the cut inequality. Proofs of any milestone are welcome, as are proofs of the converse in milestone 2 that could later be shared with mission 1.

Selected references

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
L. R. Ford, D. R. Fulkerson, Flows in Networks, RAND report R-375-PR, 1962; Princeton University Press, 1962. https://www.rand.org/pubs/reports/R375.html

11 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

An Analog of the Minimax Theorem for Vector Payoffs: A Closed Convex Set Is Approachable If and Only If It Meets Every T(q), and Is Otherwise ExcludableResearch Paper

Motivation

Von Neumann's minimax theorem says that in a zero-sum game with real payoffs, Player I can guarantee an expected gain of at least the value $v$ and Player II can hold it to at most $v$ . In a long series of plays, the law of large numbers turns this into a statement about the average payoff: I can make it exceed $v-\varepsilon$ , II can keep it below $v+\varepsilon$ , with probability approaching one.

Blackwell's 1956 paper asks the same question when the payoff of each play is a vector in $\mathbb R^N$ rather than a number. A single player then cannot optimize "the" payoff, and the natural question becomes geometric: can a player force the running average of the payoff vectors to converge to a prescribed set $S$ , whatever the opponent does? The resulting notion, approachability, became a basic tool in repeated games with incomplete information (Aumann–Maschler), in the theory of calibration and regret minimization (Foster–Vohra; Hart–Mas-Colell), and in online learning, where no-regret algorithms and Blackwell approachability are known to be equivalent (Abernethy–Bartlett–Hazan 2011).

Timeline.

1928: von Neumann's minimax theorem for matrix games.
1954: Blackwell's maximal inequality for sums with negative conditional drift (On optimal systems, Ann. Math. Statist.), quoted in this paper as THEOREM 2.
1956: this paper. A sufficient condition for approachability (THEOREM 1), a complete characterization for closed convex sets (THEOREM 3) and for $N=1$ , an example of a set that is neither approachable nor excludable, and a conjecture on weak approachability.
1992: Vieille proved Blackwell's conjecture that every set is weakly approachable or weakly excludable.

Setting

Fix integers $N\ge0$ and $r,s\ge1$ , and a closed, bounded, convex set $X\subseteq\mathbb R^N$ . The game is an $r\times s$ matrix $M=\|m(i,j)\|$ whose entries are probability distributions concentrated on $X$ . Write $\bar m(i,j)$ for the mean of $m(i,j)$ , $P$ for the simplex of mixed actions $p=(p_1,\dots,p_r)$ of Player I, and $Q$ for that of Player II.

A strategy $f=\{f_n\}_{n\ge0}$ of I is a sequence of measurable maps from the $n$ -tuples $(x_1,\dots,x_n)$ of past outcomes to $P$ ; $f_0$ is a point of $P$ . Strategies $g=\{g_n\}$ of II take values in $Q$ . A play of $(f,g)$ is a sequence of random vectors $x_1,x_2,\dots$ such that, given $x_1,\dots,x_n$ , the players draw $i$ and $j$ independently from $f_n(x_1,\dots,x_n)$ and $g_n(x_1,\dots,x_n)$ , and $x_{n+1}$ is drawn from $m(i,j)$ . The average payoff is $\bar x_n=\frac1n\sum_{i=1}^n x_i$ , and $\delta_n$ is its distance from $S$ .

A set $S\subseteq\mathbb R^N$ is approachable with $f^*$ if for every $\varepsilon>0$ there is $N_0$ such that for every strategy $g$ of II,

\mathrm{Prob}\{\delta_n\ge\varepsilon\text{ for some }n\ge N_0\}<\varepsilon .

It is excludable with $g^*$ if there is $d>0$ such that for every $\varepsilon>0$ there is $N_0$ such that for every strategy $f$ of I,

\mathrm{Prob}\{\delta_n\ge d\text{ for all }n\ge N_0\}>1-\varepsilon .

$S$ is approachable (excludable) if some strategy approaches (excludes) it. Finally, for $p\in P$ and $q\in Q$ ,

R(p)=\operatorname{conv}\Big\{\textstyle\sum_i p_i\bar m(i,j)\Big\}_{j=1}^{s},\qquad T(q)=\operatorname{conv}\Big\{\textstyle\sum_j q_j\bar m(i,j)\Big\}_{i=1}^{r}:

$R(p)$ is the set of expected payoffs I can guarantee to stay in by playing $p$ , and $T(q)$ the set II can confine them to by playing $q$ .

Formalization targets

Goal: THEOREM 3

For a closed convex set $S\subseteq\mathbb R^N$ ,

S\text{ is approachable}\iff S\cap T(q)\neq\emptyset\ \text{ for every }q\in Q,

and if $S\cap T(q_0)=\emptyset$ then $S$ is excludable with the stationary strategy $g_n\equiv q_0$ . In particular every closed convex set is either approachable or excludable. Both sentences are part of the goal.

Milestones, in the paper's order

THEOREM 2: for $|z_k|\le1$ with $E(z_k\mid z_1,\dots,z_{k-1})\le-u\,E(|z_k|\mid z_1,\dots,z_{k-1})$ and $0<u<1$ ,

\mathrm{Prob}\{z_1+\dots+z_k\ge t\text{ for some }k\}\le\Big(\tfrac{1-u}{1+u}\Big)^t .

The LEMMA: a sequence satisfying the almost-supermartingale conditions (5), (6), (7) converges to $0$ at a rate depending only on the constants $a,b,c$ .
In the proof of THEOREM 1, the squared distances $\delta_n^2$ satisfy (5)–(7) uniformly in II's strategy.
THEOREM 1: if every $x\notin S$ admits $p(x)\in P$ such that the hyperplane through a closest point $y\in S$ , perpendicular to $xy$ , separates $x$ from $R(p(x))$ , then $S$ is approachable with any strategy playing $p(\bar x_n)$ when $\bar x_n\notin S$ .
No set is both approachable and excludable.
If a closed $S$ is approachable in the transpose $M'$ with $f$ , then every closed $T$ disjoint from $S$ is excludable in $M$ with $f$ .
A closed convex $S$ meeting every $T(q)$ satisfies THEOREM 1's hypothesis.
Every $T(q_0)$ is approachable in $M'$ with $f_n\equiv q_0$ .

Significance

The result. THEOREM 3 is the vector analogue of the minimax theorem. For a closed convex target it reduces an infinite-horizon stochastic question, about every strategy of the opponent over all histories, to a finite family of one-shot conditions on the mean matrix $\bar M$ , and it shows that the game is determined for convex targets: one of the two players always wins. Its sufficient condition, THEOREM 1, is the origin of the "Blackwell strategy", which steers the average toward the target by playing, at each step, a mixed action that pushes the expected next payoff across the supporting hyperplane. Regret-matching, calibration algorithms and the reductions between online linear optimization and approachability are instances of this construction.

Formalizing it. The result is proved in the paper; to the best of available knowledge no machine-checked proof of it exists. This mission produces one: the stochastic model of a repeated game with vector payoffs, the probabilistic estimates (THEOREM 2 and the LEMMA) with the uniform rate the paper claims, and the minimax reduction for convex sets. A related platform mission, Introduction to Online Convex Optimization XIII, states a deterministic, sufficiency-only textbook variant for bounded sets; the present mission covers the stochastic model, unbounded convex targets, and the excludability half.

Difficulty

The obvious argument shows that the expected squared distance $E\delta_n^2$ decreases like $1/n$ . That is not approachability: the definition asks for the probability that the average is ever again $\varepsilon$ -far after time $N_0$ , uniformly over the opponent's strategies. Controlling the whole tail of the path, with a threshold $N_0$ that does not depend on the opponent, is the step that fails for a naive expectation bound and is why the paper needs a maximal inequality for sums with negative conditional drift. On the geometric side, the "only if" direction is not automatic: it requires that approachability and excludability be incompatible, which in turn requires that a play of every pair of strategies exists.

Formalization scope

Points live in EuclideanSpace ℝ (Fin N); pure actions are Fin r and Fin s; mixed actions are elements of stdSimplex. The game is a structure carrying $X$ (closed, bounded, convex) and the distributions $m(i,j)$ (probability measures with $m(i,j)(X^{c})=0$ ). A play is described by the conditional law of the next outcome given the past, and approachability and excludability quantify over every probability space in Type carrying such a play. Distances are extended (Metric.infEDist), equal to $+\infty$ to the empty set.

Conventions and disclosed additions:

$r,s\ge1$ where a statement needs both players to have strategies;
strategies are measurable in the history;
outcomes are indexed from $1$ ; (5) and (7) start at $n=2$ , (6) at $n=1$ ;
"the closest point" in THEOREM 1 is some closest point, and "separates" is weak separation;
THEOREM 2 is stated with $E(|z_k|\mid\cdot)$ in place of the printed "max" (the weaker hypothesis, as in the cited source), and with $u<1$ so that $((1-u)/(1+u))^t$ is a real power.

$S$ is not assumed bounded or nonempty. With the real-valued distance, the empty set would be approachable with every strategy and THEOREM 3 would be false; the extended distance rules this out. Stating only the sufficiency direction, fixing the approaching strategy in the hypotheses, or assuming a play exists would each trivialize the goal, and none is done.

A complete development needs: conditional laws of the next outcome from a strategy pair (Ionescu–Tulcea, Kernel.traj in Mathlib), a nonnegative-supermartingale maximal inequality, the metric projection onto closed convex sets, and the minimax theorem (Mathlib's Sion theorem). The maximal inequality of THEOREM 2 and the LEMMA are reusable beyond this mission. Contributions to any milestone, and to a construction of plays, are welcome.

Selected references

D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific J. Math. 6(1):1–8, 1956. https://doi.org/10.2140/pjm.1956.6.1
D. Blackwell, On optimal systems, Ann. Math. Statist. 25(2):394–397, 1954. https://doi.org/10.1214/aoms/1177728796
N. Vieille, Weak approachability, Math. Oper. Res. 17(4):781–791, 1992. https://doi.org/10.1287/moor.17.4.781
J. Abernethy, P. Bartlett, E. Hazan, Blackwell approachability and no-regret learning are equivalent, COLT 2011. https://arxiv.org/abs/1011.1936
S. Hart, A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68(5):1127–1150, 2000. https://doi.org/10.1111/1468-0262.00153

12 thms3 active usersReviewed

Completed

Combinatorics Dynamic Programming Graph Theory+1·Captain: mikedeng1

The Steiner Problem in Graphs: Algorithm A Computes the Length of the Steiner TreeResearch Paper

Motivation

The Steiner problem in graphs asks for the cheapest way to connect a prescribed set of nodes of a network, where intermediate nodes may be used freely. It is the network version of the classical Euclidean Steiner tree problem surveyed by Gilbert and Pollak (SIAM J. Appl. Math. 16, 1968), and it arises wherever a few sites must be joined through an existing network at minimum total cost: communication and pipeline layout, VLSI routing, and phylogenetics. With two terminals it is the shortest-path problem; with all nodes as terminals it is the minimum spanning tree problem; in between it is NP-hard.

Dreyfus and Wagner (Networks 1(3):195–207, 1971) gave the first exact algorithm whose running time is exponential only in the number $k$ of terminals and polynomial in the number $n$ of nodes. The paper states it, as Algorithm A, together with its proof of correctness and an exact count of its elementary operations.

Timeline. 1968: Gilbert and Pollak survey Steiner minimal trees. 1971: Dreyfus and Wagner, a dynamic program over subsets of terminals running in time proportional to $n^3/2 + n^2(2^{k-1}-k-1) + n(3^{k-1}-2^k+3)/2$ . 1987: Erickson, Monma and Veinott give the same subset recursion for general network flow problems. 2007: Björklund, Husfeldt, Kaski and Koivisto (STOC 2007) improve the exponential dependence on $k$ for small integer weights. The Dreyfus–Wagner recursion remains the standard exact method and the basis of the fixed-parameter tractability of the problem in $k$ .

Setting

A graph $G = (N, A)$ has a finite set $N$ of nodes and a set $A$ of undirected arcs, each arc $a$ having a positive length $|a|$ ; $G$ is connected. For a set $S \subseteq A$ of arcs, $|S| = \sum_{s \in S} |s|$ . A set $S$ connects a node set $X$ if all members of $X$ are joined by paths composed only of arcs in $S$ .

Given $Y \subseteq N$ , a Steiner path (or Steiner tree) connecting $Y$ is a set $S \subseteq A$ that connects $Y$ with $|S|$ minimum. Its length is the Steiner length $\operatorname{St}(Y)$ . For nodes $i, j$ , $D(i,j)$ is the length of a shortest path from $i$ to $j$ ; $D(i,j) = \operatorname{St}(\{i,j\})$ .

Algorithm A fixes a linear order of $N$ (so that each nonempty set $D$ has a first element $D[1]$ ), picks $q \in Y$ , sets $C = Y - \{q\}$ , and fills a table $S[D, I]$ for nonempty $D \subsetneq C$ and $I \in N$ :

S[\{t\}, I] = D(t, I), \qquad S[D, I] = \min_{J \in N}\Big(D(I,J) + \min_{D[1] \in E \subsetneq D}\big(S[E,J] + S[D-E,J]\big)\Big),

and returns

v = \min_{J \in N}\Big(D(q,J) + \min_{C[1] \in E \subsetneq C}\big(S[E,J] + S[C-E,J]\big)\Big).

A minimum over an empty set is $+\infty$ . In the Lean development these objects are steinerLength, pathDist, tableA and algorithmA in the namespace DreyfusWagner.Steiner.

Formalization targets

Goal: Algorithm A is exact

For every finite connected graph with positive arc lengths, every linear order on its nodes, every $Y$ with $\|Y\| \ge 3$ and every $q \in Y$ ,

v = \operatorname{St}(Y).

This is the caption of Algorithm A ("Computes the length of the Steiner tree connecting $Y$ ", p. 203). The statement is an equality, not a bound.

Milestones

In the order the proof uses them:

A Steiner path is a tree (§1, p. 197): a minimum connecting arc set contains no cycle.
The two-node case (Appendix A, p. 205): $\operatorname{St}(\{i,j\}) = D(i,j)$ .
Theorem 1 (Appendix A, p. 206): for a Steiner tree $S$ , a node $x$ on it, and a set $C$ of arcs of $S$ at $x$ , the arcs of $S$ connecting $x$ to the terminals reached through $C$ form a Steiner tree for those terminals together with $x$ .
Optimal Decomposition Theorem (Appendix A, p. 206): if $\|Y\| \ge 3$ and $q \in Y$ , a Steiner tree for $Y$ splits into three disjoint Steiner paths, for $\{p,q\}$ , $\{p\} \cup D$ and $\{p\} \cup (Y - D - \{q\})$ , where $p \in N$ and $\emptyset \ne D \subsetneq Y - \{q\}$ .
The recurrence (§2, pp. 199–200): for $\|D\| \ge 2$ and any node $m$ ,

\operatorname{St}(\{m\} \cup D) = \min_{k \in N}\Big(D(m,k) + \min_{\emptyset \ne E \subsetneq D}\big(\operatorname{St}(\{k\} \cup E) + \operatorname{St}(\{k\} \cup (D - E))\big)\Big).

The table invariant (§2, p. 200): $S[D, I] = \operatorname{St}(\{I\} \cup D)$ for every nonempty $D$ and every $I$ .

Two companion items accompany the goal: the numerical illustration of §3 (seven nodes, $\operatorname{St}(Y) = 5$ , Algorithm A returns $5$ ), and the exact count of elementary statements of §5, $n^2(2^{k-1}-k-1) + n(3^{k-1}-2^k+3)/2$ .

Significance

The result turns the Steiner problem with few terminals into a polynomial computation in the size of the network: for fixed $k$ the running time is $O(n^3)$ including all-pairs shortest paths. It is the reference exact algorithm against which heuristics and approximation algorithms for Steiner trees are evaluated, a standard example of dynamic programming over subsets, and the origin of the fixed-parameter tractability of the Steiner tree problem parameterized by the number of terminals. The subset recurrence reappears in group Steiner, prize-collecting and directed Steiner variants.

The paper's proof is complete and the result is classical; it has not, to our knowledge, been machine-checked. This mission produces a checked account of the exactness of the recursion: the structural facts about minimum connecting arc sets (acyclicity, optimality of branches, the three-way decomposition) and the passage from these to the algorithm's table. These facts about weighted graphs, minimum connecting arc sets and shortest paths are reusable well beyond this paper.

Difficulty

The upper bound $v \ge \operatorname{St}(Y)$ is routine: each term of each minimum is the length of some connecting arc set, so no term can beat the optimum. The content is the reverse inequality, which needs the Optimal Decomposition Theorem: one must show that some optimal tree actually splits at a single node $p$ into a shortest path to $q$ and two optimal subtrees whose terminal sets partition $Y - \{q\}$ into two nonempty parts. The naive choice $p = q$ fails when $q$ is a leaf, and the choice of the first branching node fails when the path from $q$ meets another terminal first; the paper handles these as separate cases. A second difficulty is the passage from arc sets to trees: minimum connecting sets are forests only because lengths are positive, and "the arcs of $S$ involved in connecting" a set of terminals must be identified with a subtree. Finally the table recursion must be matched with the recurrence, including the restriction $D[1] \in E$ that enumerates each splitting once.

Formalization scope

Nodes are a finite type V with a LinearOrder (the paper's "(ordered) set"; the goal holds for every order). The graph is a SimpleGraph V with decidable adjacency, arcs are unordered pairs Sym2 V, and lengths are ℓ : Sym2 V → ℝ. Every theorem assumes the paper's standing hypotheses of p. 195: all arcs of $G$ have positive length (∀ e ∈ G.edgeSet, 0 < ℓ e) and $G$ is connected. The paper allows several arcs between the same two nodes; the simple-graph model keeps one, which does not change any Steiner length since an optimal set uses only the shortest of parallel arcs. Connecting means reachability in the graph formed by the arcs of $S$ . Steiner lengths, $D(i,j)$ and all minima of the algorithm take values in WithTop ℝ, where ⊤ is $+\infty$ , ⊤ + x = ⊤ and an empty minimum is ⊤; no real-valued infimum with a junk value is used. $D(i,j)$ is a minimum over paths of $G$ .

The goal assumes $\|Y\| \ge 3$ , the paper's own hypothesis (Appendix A, p. 205). For $\|Y\| = 2$ Algorithm A as printed returns $+\infty$ because line (18) admits no set $E$ ; the two-node case is covered by milestone 2. The algorithm is defined from $D(i,j)$ , addition and minima only: a formalization in which tableA or algorithmA refers to Steiner lengths, or in which the goal only asserts $v \ge \operatorname{St}(Y)$ , would be trivial and is ruled out. The loop order of lines (4)–(14) is replaced by recursion on $\|D\|$ , which the paper states is immaterial (p. 203).

Useful infrastructure: sums of lengths along walks and paths, reachability in edge-subgraphs, acyclicity of minimum connecting sets, and splitting a tree at a node. Contributions of these as reusable lemmas are welcome, as are proofs of individual milestones in any order. Tree reconstruction (§2, p. 200) and the empirical running times (p. 205) are out of scope.

Selected references

S. E. Dreyfus, R. A. Wagner, The Steiner Problem in Graphs, Networks 1(3):195–207, 1971. https://doi.org/10.1002/net.3230010302
E. N. Gilbert, H. O. Pollak, Steiner Minimal Trees, SIAM Journal on Applied Mathematics 16(1):1–29, 1968. https://doi.org/10.1137/0116001
R. W. Floyd, Algorithm 97: Shortest Path, Communications of the ACM 5(6):345, 1962. https://doi.org/10.1145/367766.368168
R. E. Erickson, C. L. Monma, A. F. Veinott Jr., Send-and-Split Method for Minimum-Concave-Cost Network Flows, Mathematics of Operations Research 12(4):634–664, 1987. https://doi.org/10.1287/moor.12.4.634
A. Björklund, T. Husfeldt, P. Kaski, M. Koivisto, Fourier Meets Möbius: Fast Subset Convolution, STOC 2007, 67–74. https://doi.org/10.1145/1250790.1250801

10 thms3 active usersReviewed

Completed

Control Theory Dynamic Programming Operations Research+1·Captain: mikedeng1

Monotone Mappings with Application in Dynamic Programming II: Convergence of the DP Algorithm under Uniform DecreaseResearch Paper

Motivation

Infinite-horizon sequential decision problems (deterministic optimal control, Markov decision processes, minimax control) share one computational question: does the dynamic programming (DP) algorithm, which starts from a terminal cost and repeatedly applies the Bellman operator, converge to the optimal cost? For discounted problems with bounded costs the answer is yes, by the contraction mapping theorem (Blackwell 1965; Denardo 1967). Without discounting and boundedness the answer depends on the sign structure of the problem. Strauch's negative programming model (Strauch 1966) and Blackwell's positive programming model behave differently, and in the former the DP algorithm can fail to converge to the optimal cost even for simple deterministic problems.

Bertsekas (1977) recast these models in one abstract framework: a monotone mapping $H$ that encodes the one-stage problem, with no probabilistic or additive structure assumed. Two sign conditions organise the theory: uniform increase (Assumption I, containing Strauch's model) and uniform decrease (Assumption D, containing the deterministic version of Blackwell's positive model, e.g. deterministic problems with nonpositive stage costs). This mission formalizes the uniform-decrease half of Section 5: under D, the finite-horizon problems are solved by the DP algorithm, $J^*$ is the limit of the finite-horizon values, Bellman's equation holds, and the DP algorithm converges to $J^*$ . The same framework became the basis of Bertsekas–Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978) and of Bertsekas's Abstract Dynamic Programming (2013, 3rd ed. 2022).

Setting

States, controls, policies. $S$ (nonempty) and $C$ are sets. Each $x\in S$ has a nonempty constraint set $U(x)\subseteq C$ . $M$ is the set of selectors $\mu:S\to C$ with $\mu(x)\in U(x)$ for all $x$ , and a policy is a sequence $\pi=\{\mu_0,\mu_1,\dots\}$ of selectors. The policy is stationary if $\mu_k=\mu$ for all $k$ .

Functions and the mapping $H$ . $F$ is the set of functions $J:S\to[-\infty,\infty]$ , ordered pointwise, and $e$ is the constant function $1$ . A mapping $H:S\times C\times F\to[-\infty,\infty]$ is given, and it is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for every $x$ and $u\in U(x)$ . It defines

T_\mu(J)(x)=H(x,\mu(x),J),\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J).

$T^k$ is the $k$ -fold composition, with $T^0$ the identity, and $(T_{\mu_0}\cdots T_{\mu_{N-1}})$ applies $T_{\mu_{N-1}}$ first.

Costs. A terminal function $\bar J\in F$ with $\bar J(x)>-\infty$ is given. The cost of a policy, the optimal cost, the $N$ -stage optimal cost and the limit of the DP algorithm are

J_\pi=\lim_{N\to\infty}(T_{\mu_0}\cdots T_{\mu_{N-1}})(\bar J),\quad J^*=\inf_{\pi}J_\pi,\quad J_N=\inf_{\pi}(T_{\mu_0}\cdots T_{\mu_{N-1}})(\bar J),\quad J_\infty=\lim_{N\to\infty}T^N(\bar J),

all pointwise. $J_\mu$ denotes the cost of the stationary policy $\{\mu,\mu,\dots\}$ .

Assumptions. D: $H(x,u,\bar J)\le\bar J(x)$ for all $x$ , $u\in U(x)$ . Under D every sequence above is nonincreasing, so the limits exist in $[-\infty,\infty]$ . D.1: for every sequence with $J_{k+1}\le J_k\le\bar J$ , $\lim_k H(x,u,J_k)=H(x,u,\lim_k J_k)$ . D.2: there is $\alpha>0$ such that $H(x,u,J)-\alpha r\le H(x,u,J-re)\le H(x,u,J)$ for all $r>0$ and $J\le\bar J$ .

Formalization targets

Goal: convergence of the DP algorithm (Proposition 9)

If D holds, and either D.1 holds or $J_N=T^N(\bar J)$ for every $N\ge1$ , then

J_\infty=J^*.

Milestones

Lemma 1. Under D, $J^*(x)=\lim_{N\to\infty}J_N(x)$ for every $x$ .
Proposition 3. Under D, and either D.1 or (D.2 and $T^N(\bar J)>-\infty$ everywhere), $J_N=T^N(\bar J)$ for a given $N\ge1$ .
Proposition 6. Under D and D.1, $J^*=T(J^*)$ , and every $J'\le\bar J$ with $J'\le T(J')$ satisfies $J'\le J^*$ .
Corollary 6.2. Under D and D.1, $J_\mu=T_\mu(J_\mu)$ for every stationary policy, and every $J'\le\bar J$ with $J'\le T_\mu(J')$ satisfies $J'\le J_\mu$ .
Proposition 8. Under D and D.1, a stationary policy $\{\mu^*,\mu^*,\dots\}$ is optimal if and only if $T_{\mu^*}(J_{\mu^*})=T(J_{\mu^*})$ .

The goal is the paper's answer, in the uniform-decrease case, to the question it poses in the introduction: when is $\lim_N T^N(\bar J)=J^*$ ?

Significance

The result. Proposition 9 justifies value iteration from $\bar J$ for every problem that fits Assumption D, including deterministic and stochastic control with nonpositive costs (reward maximization with nonnegative rewards) and minimax problems satisfying D.1. Propositions 6 and 8 characterise $J^*$ as the largest solution of Bellman's equation below $\bar J$ and give a verification test for stationary policies. The hypotheses are sharp in the sense the paper documents: its Counterexamples 2 and 3 show $J_N\ne T^N(\bar J)$ when D.1 is dropped together with D.2 or with the finiteness condition $T^N(\bar J)>-\infty$ . Under the mirror assumption I, $J_\infty=J^*$ can fail, so the asymmetry between the two sign conditions is part of the content.

Formalizing it. All results are proved in the 1977 paper and reappear in later monographs. No machine-checked version of this abstract framework is known. The platform's existing dynamic programming items are finite-state, real-valued and contraction-based, so this mission would add the first formal treatment of extended-real-valued, non-contractive dynamic programming, and a model definition that other results of the same theory can reuse.

Difficulty

The obvious argument for Proposition 9, " $J_N=T^N(\bar J)$ and $J_N\to J^*$ ", hides two separate interchanges of limits and infima. Lemma 1 interchanges $\inf_\pi$ with $\lim_N$ , which works only because every sequence is monotone in the right direction under D. Proposition 3 is where the work is: the $N$ -stage infimum over policies must be matched by the iterated infimum $T^N$ , which requires building near-optimal selectors stage by stage and passing a limit through $H$ $N$ times, using D.1, or controlling accumulated errors through D.2. The latter breaks down when values reach $-\infty$ , which is why that branch needs $T^N(\bar J)>-\infty$ . All arithmetic is in $[-\infty,\infty]$ , where expressions such as $\infty-\infty$ are not defined, and $J^*$ , $J_N$ , $T^N(\bar J)$ may equal $-\infty$ even though $\bar J$ does not.

Formalization scope

The model is a Lean structure MonotoneDP.Decrease.Model S C with fields U, U_nonempty, H, mono, Jbar, Jbar_ne_bot and S_nonempty; $F$ is S → EReal. Policies are ℕ → Selector, where a selector is a function with values in the constraint sets. $T$ is an infimum over U x only, and $J^*$ , $J_N$ are infima over admissible policies. $J_\pi$ and $J_\infty$ are limUnder atTop; every theorem assumes D, under which both sequences are nonincreasing and converge, so these are the paper's limits. In D.1 both limits are limUnder. D.2 carries its scalar as a parameter, and "D.2 holds" is ∃ α, AssumptionD2 α. Only real scalars are ever subtracted from extended reals.

$J_N$ is defined for every $N$ , and Propositions 3 and 9 quantify over $N\ge1$ as the paper does. In Proposition 3 the condition $T^N(\bar J)>-\infty$ belongs to the D.2 branch only. No hypothesis beyond the page is added. Nonempty constraint sets and $\bar J>-\infty$ are the paper's standing assumptions, stated in the model, not in the theorems. Without nonempty constraint sets there would be no policies, $J^*$ and $J_N$ would be $+\infty$ , and several statements would hold trivially; the model rules this out.

Useful contributions: general lemmas about monotone sequences in EReal (interchanging ⨅ and limits), the monotonicity facts (25) and $T^{N+1}(\bar J)\le T^N(\bar J)$ under D, and reusable constructions of near-optimal selectors. Corollary 6.1 (the finite-state D.2 variant) is not included.

Selected references

D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15(3), 438–464, 1977. https://doi.org/10.1137/0315031
E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9(2), 165–177, 1967. https://doi.org/10.1137/1009030
R. E. Strauch, Negative dynamic programming, Ann. Math. Statist. 37(4), 871–890, 1966. https://doi.org/10.1214/aoms/1177699147
D. Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36(1), 226–235, 1965. https://doi.org/10.1214/aoms/1177700285
D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific, 2022. https://www.mit.edu/~dimitrib/abstractdp_MIT.html

8 thms3 active usersReviewed

Completed

Convex Optimization Functional Analysis Operations Research+1·Captain: mikedeng1

A Three-Operator Splitting Scheme and its Optimization Applications 3: Accelerated Convergence under Strong MonotonicityResearch Paper

Motivation

Many problems in convex optimization, variational inequalities and signal processing reduce to finding a zero of a sum of three monotone operators, one of which is single-valued and smooth. Davis and Yin (Set-Valued Var. Anal. 25, 2017) introduced a splitting scheme that evaluates each of the three operators separately: the two set-valued ones through their resolvents, the single-valued one through a forward step. With a fixed stepsize, their Algorithm 1 converges weakly but can be slow: the paper's Section 3.4 constructs examples where the squared distance of the iterates to the solution decays no faster than $(k+1)^{-(1+\epsilon)}$ for every $\epsilon > 0$ .

When one of the operators is strongly monotone (for example the subdifferential of a strongly convex function), first-order splitting methods can be accelerated by letting the stepsize shrink like $1/k$ ; the paper relates its stepsizes to those of Chambolle and Pock's accelerated primal–dual method (J. Math. Imaging Vis. 40, 2011, Algorithm 2) and of Boţ, Csetnek, Heinrich and Hendrich (Math. Program. 150, 2015, Algorithm 5). Section 3.3 of Davis–Yin carries this device over to three-operator splitting and obtains an $O(1/(k+1)^2)$ rate for the squared distance. This mission formalizes that result.

Setting

Let $H$ be a real Hilbert space. A set-valued operator $A : H \to 2^H$ is monotone if $\langle x - y, u - v\rangle \ge 0$ for all $u \in Ax$ , $v \in Ay$ , and maximal monotone if its graph is not properly contained in the graph of another monotone operator. It is $\mu$ -strongly monotone if $\langle x - y, u - v\rangle \ge \mu\|x-y\|^2$ for all such pairs. A single-valued $C : H \to H$ is $\beta$ -cocoercive if $\beta\|Cx - Cy\|^2 \le \langle Cx - Cy, x - y\rangle$ , and $L_C$ -Lipschitz if $\|Cx - Cy\| \le L_C\|x - y\|$ .

The problem is to find $x^* \in \operatorname{zer}(A + B + C)$ , that is, $0 \in Ax^* + Bx^* + Cx^*$ , where $A$ , $B$ are maximal monotone and $C$ is monotone and single-valued. For $\gamma > 0$ the resolvent $J_{\gamma A} = (I + \gamma A)^{-1}$ is the map with $x \in J_{\gamma A}x + \gamma A(J_{\gamma A}x)$ .

Algorithm 3 fixes stepsizes $(\gamma_k)_{k\ge 0} \subseteq (0,\infty)$ and an initial point $x_A^0 \in H$ , sets $x_B^0 = J_{\gamma_0 B}(x_A^0)$ , $u_B^0 = \gamma_0^{-1}(x_A^0 - x_B^0)$ , and iterates for $k \ge 0$

x_B^{k+1} = J_{\gamma_k B}(x_A^k + \gamma_k u_B^k),\quad u_B^{k+1} = \tfrac{1}{\gamma_k}(x_A^k + \gamma_k u_B^k - x_B^{k+1}),\quad x_A^{k+1} = J_{\gamma_{k+1}A}(x_B^{k+1} - \gamma_{k+1}u_B^{k+1} - \gamma_{k+1}Cx_B^{k+1}).

The stepsize changes in the middle of an iteration. Two stepsize rules are considered, each defined recursively from $\gamma_0$ :

\text{(3.6)}\quad \gamma_{k+1} = \frac{-2\gamma_k^2\mu_C\eta + \sqrt{(2\gamma_k^2\mu_C\eta)^2 + 4(1+2\gamma_k\mu_B)\gamma_k^2}}{2(1+2\gamma_k\mu_B)}, \qquad \text{(3.7)}\quad \gamma_{k+1} = \frac{\gamma_k}{\sqrt{1 + 2\gamma_k(\mu_B - \gamma_kL_C^2/2)}}.

Formalization targets

Goal: Theorem 3.3, both parts

Let $B$ be $\mu_B$ -strongly monotone with $\mu_B \ge 0$ .

If $C$ is $\beta$ -cocoercive and $\mu_C$ -strongly monotone ( $\mu_C > 0$ ), $\eta \in (0,1)$ , $\gamma_0 \in (0, 2\beta(1-\eta))$ and the stepsizes follow (3.6), then for every $x^* \in \operatorname{zer}(A+B+C)$

\exists K\ \forall k \ge 0:\quad \|x_B^k - x^*\|^2 \le \frac{K}{(k+1)^2}.

If $C$ is $L_C$ -Lipschitz, $\mu_B > 0$ , $\gamma_0 \in (0, 2\mu_B/L_C^2)$ and the stepsizes follow (3.7), the same conclusion holds.

The goal asserts the shape of the rate only; the constant $K$ is not fixed.

Milestones

Proposition 3.1, Parts 1 and 2: the one-step inequalities (3.9) and (3.10) for Algorithm 3 with arbitrary admissible stepsizes.
Stepsize facts from the proof of Theorem 3.3: the identities that make (3.9) and (3.10) telescope, the monotonicity of the stepsizes (3.6), and the limits $(k+1)\gamma_k \to 1/(\mu_C\eta + \mu_B)$ for (3.6) and $(k+1)\gamma_k \to 1/\mu_B$ for (3.7).

Significance

The theorem shows that strong monotonicity of $B$ or $C$ can be converted into a quadratically decaying distance bound without knowledge of the solution, with stepsizes that are computable from the strong monotonicity and cocoercivity (or Lipschitz) constants alone. Since the rate is established for $x_B^k$ , it applies directly to splitting schemes for strongly convex composite problems $\min f + g + h$ with $h$ smooth, where $x_B^k$ is the proximal point of $g$ .

The result is proved in the paper; no machine-checked version is known. The formalization adds a precise statement of the admissible parameter ranges, a check of the index conventions of a scheme whose stepsize changes mid-iteration, and a correction of the one-step inequalities at the first iteration (see Formalization scope). The stepsize limits are statements about explicit real recursions and are of independent use for other accelerated schemes.

Difficulty

The one-step inequalities (3.9) and (3.10) are long but elementary chains of inner-product identities and Young's inequality; the work lies in bookkeeping two stepsizes per iteration. The rate itself does not follow from the one-step inequality alone: telescoping gives a bound of the form $\|x_B^{k}-x^*\|^2 \lesssim \gamma_k^2$ , and one must then show $\gamma_k$ decays exactly like $1/k$ . The rules (3.6) and (3.7) are nonlinear recursions without closed form, so their asymptotics require a Stolz–Cesàro type argument, which is not available in Mathlib under that name. Choosing a stepsize sequence of the form $c/k$ instead is a different algorithm and not covered by the theorem.

Formalization scope

$H$ is an arbitrary real Hilbert space (InnerProductSpace ℝ H, CompleteSpace H), not a Euclidean space.
Resolvents are not constructed. They are families JA JB : ℝ → H → H required to satisfy the resolvent inclusion $\gamma^{-1}(x - J(\gamma)x) \in A(J(\gamma)x)$ for every $\gamma > 0$ ; for maximal monotone operators such maps exist and are unique, so nothing is lost.
Algorithm 3 is a single recursive definition of the triple $(x_A^k, x_B^k, u_B^k)$ from $x_A^0$ , the stepsizes, the resolvent families and $C$ ; the paper's loop index $k = 1, 2, \dots$ matches recursion (3.8) shifted by one.
The stepsize rules (3.6) and (3.7) are recursive real sequences, used verbatim; each theorem assumes the paper's parameter ranges.
$O(1/(k+1)^2)$ is rendered as $\exists K\,\forall k,\ \|x_B^k - x^*\|^2 \le K/(k+1)^2$ , with $K$ chosen after all data (initial point, operators, constants, $\gamma_0$ , $x^*$ ) and before $k$ . No explicit constant is stated.
Strong monotonicity of $C$ means $\mu_C > 0$ ; only $\mu_B = 0$ is allowed, as on the page. With $\mu_B = \mu_C = 0$ rule (3.6) keeps $\gamma_k$ constant and the rate fails, so a formalization allowing $\mu_C = 0$ would be false. In Part 2, $L_C > 0$ is assumed so that the stepsize interval is meaningful, and $C$ is assumed monotone, as in problem (1.1) and as used in the paper's proof of (3.10).
The paper states (3.9) and (3.10) for all $k \ge 0$ ; at $k = 0$ the initial point $x_A^0$ is not a resolvent output, and both inequalities fail in general. The milestones state them for $k \ge 1$ . Theorem 3.3 is unaffected, since finitely many initial terms do not change an $O(\cdot)$ bound.
The display $\gamma_k^2 - \gamma_{k+1}^2 = \gamma_k\gamma_{k+1}(2\gamma_k\mu_B + 2\gamma_{k+1}\mu_C\eta)$ on p. 845 has $\gamma_k$ and $\gamma_{k+1}$ swapped inside the bracket; the milestone states the corrected identity $\gamma_k\gamma_{k+1}(2\gamma_{k+1}\mu_B + 2\gamma_k\mu_C\eta)$ .
A trivializing formalization, such as one in which the resolvent hypothesis is unsatisfiable, the stepsize interval is empty, or the rate constant may depend on $k$ , is ruled out: the hypotheses are met by $A = 0$ , $B = \mu_B I$ (with resolvents $J_{\gamma A} = I$ , $J_{\gamma B} = (1+\gamma\mu_B)^{-1}I$ ) and $C = cI$ with $c > 0$ , and $K$ is quantified before $k$ .

Contributions are welcome at every level: proofs of the real-sequence milestones (a general Stolz–Cesàro lemma would be reusable well beyond this mission), of the two one-step inequalities, and of the telescoping argument that assembles the goal.

Selected references

D. Davis and W. Yin, A Three-Operator Splitting Scheme and its Optimization Applications, Set-Valued and Variational Analysis 25 (2017), 829–858. https://doi.org/10.1007/s11228-017-0421-z (preprint: https://arxiv.org/abs/1504.01032)
R. I. Boţ, E. R. Csetnek, A. Heinrich and C. Hendrich, On the convergence rate improvement of a primal-dual splitting algorithm for solving monotone inclusion problems, Mathematical Programming 150 (2015), 251–279. https://doi.org/10.1007/s10107-014-0766-0
A. Chambolle and T. Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, Journal of Mathematical Imaging and Vision 40 (2011), 120–145. https://doi.org/10.1007/s10851-010-0251-1
H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5

11 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

On Polyhedral Approximations of the Second-Order Cone III: Closeness of the Relaxed Feasible SetResearch Paper

Motivation

Conic quadratic problems (also called second-order cone programs) arise directly in applications such as contact problems with Coulomb friction, and a wide range of nonlinear convex problems can be rewritten in this form (Lobo, Vandenberghe, Boyd and Lebret 1998). Interior-point methods solve them in polynomial time, but around 2000 the available software for conic quadratic problems handled far fewer variables than linear programming software. Ben-Tal and Nemirovski (2001) therefore asked whether a conic quadratic problem can be replaced by a linear program of comparable size. Their construction replaces each second-order cone by a polyhedral cone that is exact up to a factor $1+\varepsilon$ . The feasible set of the resulting linear program, projected back to the original variables, lies between the feasible set of the original problem and that of its $\varepsilon$ -relaxation.

This sandwich is only useful if the relaxed problem is close to the original one, and in general it is not: the paper notes that (CQP) can be infeasible while every relaxation with $\varepsilon>0$ is feasible. Proposition 4.1 of the paper, the target of this mission, gives a sufficient condition under which the two feasible sets are $O(\varepsilon)$ -close.

Setting

For $y\in\mathbb R^k$ let $\|y\|_2=\sqrt{y^Ty}$ be the Euclidean norm. A conic quadratic problem in the variable $x\in\mathbb R^n$ is

\text{(CQP)}\qquad \min_x\bigl\{e^Tx \bigm| Ax\ge b,\ \|A_\ell x-b_\ell\|_2\le c_\ell^Tx-d_\ell,\ \ell=1,\dots,m\bigr\},

where $A$ is a $k_0\times n$ matrix and $b\in\mathbb R^{k_0}$ (the inequality $Ax\ge b$ is componentwise), and for each $\ell$ the matrix $A_\ell$ is $k_\ell\times n$ , $b_\ell\in\mathbb R^{k_\ell}$ , $c_\ell\in\mathbb R^n$ and $d_\ell\in\mathbb R$ . For $\varepsilon>0$ the $\varepsilon$ -relaxation is

\text{(CQP}_\varepsilon)\qquad \min_x\bigl\{e^Tx \bigm| Ax\ge b,\ \|A_\ell x-b_\ell\|_2\le (1+\varepsilon)\bigl[c_\ell^Tx-d_\ell\bigr],\ \ell=1,\dots,m\bigr\}.

$\mathrm{Feas}(P)$ denotes the feasible set of a problem $(P)$ ; in Lean these are feas P and feasRelaxed P ε, subsets of Fin n → ℝ, for a problem datum P : CQP n k₀ m.

Two conditions on (CQP) are used.

Strict feasibility: there are $\bar x$ and $r>0$ with $A\bar x\ge b$ and $\|A_\ell\bar x-b_\ell\|_2\le[c_\ell^T\bar x-d_\ell]-r$ for every $\ell$ (IsStrictlyFeasible P x̄ r).
Semiboundedness: there is $R$ such that every feasible $x$ of (CQP) satisfies $c_\ell^Tx-d_\ell\le R$ for every $\ell$ (IsSemibounded P R).

Put $\gamma(\varepsilon)=R\varepsilon/r$ .

Formalization targets

Goal: Proposition 4.1

If (CQP) has $m\ge1$ conic constraints and is strictly feasible and semibounded, then for every $\varepsilon>0$ with $\gamma(\varepsilon)<1$ ,

\gamma(\varepsilon)\bar x+(1-\gamma(\varepsilon))\,\mathrm{Feas}(\mathrm{CQP}_\varepsilon)\ \subseteq\ \mathrm{Feas}(\mathrm{CQP})\ \subseteq\ \mathrm{Feas}(\mathrm{CQP}_\varepsilon). \tag{14}

The left-hand side is the image of $\mathrm{Feas}(\mathrm{CQP}_\varepsilon)$ under $y\mapsto\gamma(\varepsilon)\bar x+(1-\gamma(\varepsilon))y$ , not a Minkowski sum.

Milestones

The milestones follow the paper's proof in order.

The right inclusion $\mathrm{Feas}(\mathrm{CQP})\subseteq\mathrm{Feas}(\mathrm{CQP}_\varepsilon)$ for $\varepsilon>0$ .
For $y\in\mathrm{Feas}(\mathrm{CQP}_\varepsilon)$ and $t_\ell=c_\ell^Ty-d_\ell$ , every $\delta\in[0,1]$ with $\delta\ge\varepsilon t_\ell/(r+\varepsilon t_\ell)$ for all $\ell$ makes $x_\delta=(1-\delta)y+\delta\bar x$ feasible for (CQP).
Under semiboundedness, the same $\delta$ satisfies $(1-\delta)t_\ell\le R$ for all $\ell$ .
If $\delta=\varepsilon t/(r+\varepsilon t)$ with $t\ge0$ , $(1-\delta)t\le R$ and $\gamma(\varepsilon)<1$ , then $t\le R/(1-\gamma(\varepsilon))$ and $\delta\le\gamma(\varepsilon)$ .

Significance

The result. Proposition 4.1 turns the qualitative sandwich "exact ⊆ polyhedral ⊆ relaxed" into a quantitative statement. When a problem is strictly feasible with margin $r$ and its conic right-hand sides are bounded by $R$ on the feasible set, the relaxed feasible set, shrunk towards $\bar x$ by $1-\gamma(\varepsilon)$ , lies inside the exact one. The error of the relaxation is thus controlled by $\gamma(\varepsilon)=R\varepsilon/r$ , which is linear in $\varepsilon$ . Together with the paper's main theorem, that a polyhedral $\varepsilon$ -approximation of the Lorentz cone with $O(k\ln(1/\varepsilon))$ variables and inequalities exists, this measures how well a linear program of moderate size approximates the conic problem. The paper uses it this way for the examples in its introduction.

The formalization. The proposition is proved in the paper; no machine-checked version is known. This mission produces a Lean formalization of conic quadratic problems and their relaxations with the Euclidean norm, together with the strict feasibility and semiboundedness conditions and the proof. The Lorentz-cone approximation results of the same paper are the subject of the companion missions I and II of this series.

Difficulty

The right inclusion is immediate. The left inclusion does not follow from convexity alone. A relaxed-feasible point $y$ may violate every conic constraint of (CQP), and nothing about $y$ bounds how far it is from $\mathrm{Feas}(\mathrm{CQP})$ . The needed information comes from semiboundedness, which constrains only feasible points of (CQP). That hypothesis therefore cannot be applied to $y$ itself, and the shrink factor $\gamma(\varepsilon)$ must be obtained without any bound on $c_\ell^Ty-d_\ell$ given in advance. The obvious attempt, bounding the violation at $y$ by $\varepsilon R$ , fails for exactly this reason.

Formalization scope

Vectors of $\mathbb R^n$ are Fin n → ℝ; the $m$ conic constraints are indexed by Fin m (0-based) with a dependent family of matrices (ℓ : Fin m) → Matrix (Fin (k ℓ)) (Fin n) ℝ, so the row sizes $k_\ell$ may differ. The norm is written out as eucNorm y = √(∑ i, y i ^ 2); Mathlib's norm on Fin k → ℝ is the sup norm and is not used.
Only feasible sets are compared; the objective $e$ is carried as data but plays no role.
Correction 1. In hypothesis (i) the page prints $[c_\ell^Tx-d_\ell]-r$ without the bar over $x$ . The proof uses $c_\ell^T\bar x-d_\ell-r$ , which is what IsStrictlyFeasible states.
Correction 2. The goal assumes $m\ge1$ , which the paper leaves implicit. With $m=0$ , semiboundedness is vacuous and $R$ may be negative, so $\gamma(\varepsilon)<0$ . Then the map $y\mapsto\gamma\bar x+(1-\gamma)y$ extrapolates beyond $y$ and can leave $\{Ax\ge b\}$ . An example is $n=1$ , $A=[1]$ , $b=0$ , $\bar x=1$ , $y=0$ , $R=-1$ , $r=\varepsilon=1$ . For $m\ge1$ the hypotheses force $R\ge r>0$ .
$\varepsilon$ ranges over all $\varepsilon>0$ with $\gamma(\varepsilon)<1$ , as in the paper; it is not restricted to $(0,1]$ .
The second milestone is stated for every $\delta\in[0,1]$ that dominates all ratios $\varepsilon t_\ell/(r+\varepsilon t_\ell)$ , rather than only for the paper's $\delta=\max_\ell$ . This includes the paper's case.
The goal cannot be satisfied trivially. The strict feasibility and semiboundedness hypotheses are jointly satisfiable (for example $n=m=1$ , the constraint $|x|\le 1$ written as $\|x\|_2\le 1$ , $\bar x=0$ , $r=1$ , $R=1$ ), and the conclusion is the full two-sided inclusion with the paper's $\gamma(\varepsilon)$ , not the existence of some contraction factor.
Needed infrastructure: Euclidean-norm convexity (the triangle inequality and homogeneity for eucNorm, or a transfer to EuclideanSpace ℝ (Fin k)) and linearity of Matrix.mulVec and dotProduct. A convexity lemma for feas P would be reusable beyond this mission, and contributions of it are welcome.

Selected references

A. Ben-Tal and A. Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Mathematics of Operations Research 26(2):193–205, 2001. https://doi.org/10.1287/moor.26.2.193.10561
M. S. Lobo, L. Vandenberghe, S. Boyd and H. Lebret, Applications of Second-Order Cone Programming, Linear Algebra and its Applications 284:193–228, 1998. https://doi.org/10.1016/S0024-3795(98)10032-0
Yu. Nesterov and A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

7 thms3 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

On Minimizing a Convex Function Subject to Linear Inequalities III: The Expected Cost of a Linear Program with Random Coefficients Is ConvexResearch Paper

Motivation

A linear program is solved with known data, but in planning problems the data are often only known in distribution when the main decision is taken: demands, yields and requirements are revealed later, and a corrective action is taken after they are. E. M. L. Beale's 1955 paper On Minimizing a Convex Function Subject to Linear Inequalities formulates this situation in its §5, "Linear Programming with Random Coefficients", as what is now called a two-stage stochastic linear program with recourse. Beale's motivating example is the transportation problem of Hitchcock (1941) with random requirements at the destinations, where every unit of shortage or excess incurs a loss. The same model was put forward in the same year by Dantzig, Linear Programming under Uncertainty (Management Science, 1955), as the paper's note added in proof acknowledges.

Timeline:

1955. Beale (§5, Theorems 2 and 3) and Dantzig independently introduce two-stage linear programs with random data; Beale proves that the expected cost is convex in the first-stage decision, and that the cost is convex in the random data for fixed decision.
1967. Walkup and Wets, Stochastic Programs with Recourse, study the domain of the expected recourse function and its properties under fixed recourse.
1974. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, gives the systematic treatment of convexity, finiteness and polyhedrality of the expected recourse function, now textbook material (Birge and Louveaux, Introduction to Stochastic Programming, Ch. 3).

Setting

Constants $c\in\mathbb R^n$ , $f\in\mathbb R^p$ and an $m\times p$ matrix $D=(d_{ik})$ are given. The data $A=(\alpha_{ij})$ , an $m\times n$ matrix, and $\beta\in\mathbb R^m$ are random variables on a probability space $(\Omega,P)$ : their distribution is known when the first-stage decision $x\in\mathbb R^n$ , $x\ge0$ , is chosen, and their values are known when the second-stage decision $y\in\mathbb R^p$ , $y\ge0$ , is chosen. The cost is

C=c'x+f'y,\qquad Ax+Dy=\beta. \qquad(5.3),(5.4)

For a right-hand side $b\in\mathbb R^m$ the second-stage value is

Q(b)=\min\{f'y : y\ge0,\ Dy=b\},

and for fixed data the cost of a first-stage decision is $C(x)=c'x+Q(\beta-Ax)$ . The expected cost is

E(C)(x)=\int_\Omega \bigl(c'x+Q(\beta(\omega)-A(\omega)x)\bigr)\,dP(\omega).

The problem is to choose $x\ge0$ minimising $E(C)$ . In Lean the value is secondStageValue D f b, the cost is cost c f D A β x, and the expected cost is expectedCost P c f D A β x, all in the namespace BealeConvexMin.RandomLP.

Formalization targets

Goal: Theorem 2 (p. 182)

Assume that for every $x\ge0$ the second-stage minimum is attained for almost every outcome and that $\omega\mapsto C(x,\omega)$ is integrable. Then

E(C)(\lambda_1x_1+\lambda_2x_2)\le\lambda_1E(C)(x_1)+\lambda_2E(C)(x_2)\qquad(x_1,x_2\ge0,\ \lambda_1,\lambda_2\ge0,\ \lambda_1+\lambda_2=1),

that is, $E(C)$ is convex on the non-negative orthant. The statement fixes no distribution class: it is claimed for any known distribution of $(A,\beta)$ .

Milestones

Pointwise convexity (last display of the proof of Theorem 2, p. 182): for fixed data $(A,\beta)$ , with the minimum attained at every $x\ge0$ ,

C(\lambda_1x_1+\lambda_2x_2)\le\lambda_1C(x_1)+\lambda_2C(x_2).

Theorem 3 (p. 182): for fixed $x$ , the cost $(A,\beta)\mapsto c'x+Q(\beta-Ax)$ is jointly convex on every convex set of data on which the second-stage minimum is attained.
Eqs. (5.5)–(5.6) (p. 182): for a finitely supported distribution, $A=A_r$ and $\beta=\beta_r$ with probability $p_r$ , the value $E(C)(x)$ is the minimum of $c'x+\sum_r p_r f'y_r$ over non-negative $y_r$ with $A_rx+Dy_r=\beta_r$ for all $r$ ; minimising $E(C)$ is then a linear program.

Significance

The result. Theorem 2 is the basic structural fact of two-stage stochastic linear programming: the first-stage problem is a convex program in $x$ , whatever the distribution of the data. It is what makes local optimality global for the first-stage problem, what justifies cutting-plane and decomposition methods that approximate $E(C)$ from below by supporting hyperplanes, and what makes sample-average approximations convex programs. Theorem 3, joint convexity in the data, gives through Jensen's inequality the comparison between the stochastic problem and its mean-value problem that Beale draws on p. 182. The discrete reformulation (5.5)–(5.6) is the deterministic-equivalent linear program used for finitely many scenarios.

Formalizing it. The theorems are proved in the paper, and their content is classical. The mission produces machine-checked statements of the model with its implicit hypotheses made explicit (attainment of the second stage, integrability of the cost), and proofs of the three results in Lean. The platform already has related statements in other models (finite scenario sets with extended-real recourse, and a complete-recourse, finite-second-moment version); none has Beale's hypotheses, and none states convexity of $c'x+E\,Q$ for an arbitrary distribution.

Difficulty

The mathematics is short; the difficulty is in the encoding. The second-stage value is a minimum that may fail to exist: the second stage may be infeasible for some $x$ and some outcomes, or unbounded below. A real-valued infimum then takes an arbitrary default value, and convexity would become a statement about that default. Similarly, the mean value only exists when the cost is integrable. A faithful statement has to carry attainment and integrability exactly where the paper tacitly assumes them, on the domain $x\ge0$ the paper uses, and no stronger condition (such as complete recourse or moment bounds) that the paper does not make. In the discrete reformulation, the minimum over the whole family $(y_r)_r$ has to be matched with the probability-weighted sum of per-scenario minima.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, inner products dotProduct, and $y\ge0$ is the componentwise order. The random data are functions A : Ω → Matrix (Fin m) (Fin n) ℝ and β : Ω → Fin m → ℝ on a measurable space with a probability measure P; no measurability of the data is assumed beyond integrability of the cost.
The second-stage value is the real infimum of $f'y$ over the feasible set. It equals $0$ on an infeasible or unbounded-below second stage, so each theorem assumes attainment of the minimum where it is evaluated (the paper's "value of $y$ that minimizes $C$ "). The goal assumes attainment for almost every outcome at every $x\ge0$ .
$E(C)$ is the Bochner integral, which is $0$ for a non-integrable integrand, so the goal assumes integrability of $C(x,\cdot)$ at every $x\ge0$ (the paper's "mean value $E(C)$ ").
Convexity is claimed on $\{x : x\ge0\}$ , the paper's domain, not on all of $\mathbb R^n$ . Theorem 3 is stated for fixed non-negative $x$ (the model's first-stage domain) and on every convex set of data on which the minimum is attained, since the paper names no domain.
A formalization in which the value is an unconstrained infimum without attainment, or the expectation is taken without integrability, is trivially convex on the region where the default values apply and does not state Beale's theorem; such variants are ruled out.
Reusable beyond this mission: basic facts on the optimal value of a parametric linear program in its right-hand side and cost data, and convexity of integrals of pointwise-convex integrands. Proofs of the milestones and of the goal, and alternative formulations in extended reals, are welcome.

Selected references

E. M. L. Beale, On Minimizing a Convex Function Subject to Linear Inequalities, Journal of the Royal Statistical Society, Series B 17(2):173–184, 1955. https://doi.org/10.1111/j.2517-6161.1955.tb00191.x
G. B. Dantzig, Linear Programming under Uncertainty, Management Science 1(3–4):197–206, 1955. https://doi.org/10.1287/mnsc.1.3-4.197
F. L. Hitchcock, The Distribution of a Product from Several Sources to Numerous Localities, Journal of Mathematics and Physics 20:224–230, 1941. https://doi.org/10.1002/sapm1941201224
D. W. Walkup and R. J.-B. Wets, Stochastic Programs with Recourse, SIAM Journal on Applied Mathematics 15(5):1299–1314, 1967. https://doi.org/10.1137/0115113
R. J.-B. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3):309–339, 1974. https://doi.org/10.1137/1016053
J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

6 thms3 active usersReviewed

Completed

Linear algebra Numerical Analysis Probability+1·Captain: mikedeng1

Randomized Algorithms for Estimating the Trace of an Implicit Symmetric Positive Semi-Definite Matrix I: Sample Bound for the Gaussian Trace EstimatorResearch Paper

Motivation

Many computations in scientific computing, statistics and machine learning need the trace of a matrix $A$ that is never formed explicitly: $A$ may be $f(B)$ for a large sparse $B$ , an inverse $B^{-1}$ , or a product of operators, and the only access to it is the ability to compute products $Az$ for chosen vectors $z$ . Examples are log-determinant estimation in Gaussian process regression, counting triangles in graphs through $\mathrm{trace}(B^3)$ , computing charge densities in electronic structure calculations, and generalized cross-validation in regularized regression. For such matrices the $n$ diagonal entries are not available, and computing them one at a time costs $n$ matrix–vector products.

Randomized trace estimators replace this by a small number $M$ of products: draw random vectors $z_1,\ldots,z_M$ from a fixed distribution with $\mathrm{E}(z_i^T A z_i) = \mathrm{trace}(A)$ and average the quadratic forms. Hutchinson (1989) introduced the estimator with Rademacher vectors and computed its variance; Silver and Röder (1997) used Gaussian vectors. Before Avron and Toledo (2011), the analyses of these estimators were variance computations, which do not say how many samples guarantee a given relative accuracy with a given probability. Avron and Toledo gave the first such sample bounds for several estimators, stated in terms of an $(\epsilon,\delta)$ guarantee; this mission formalizes their bound for the Gaussian estimator. Later work (Roosta-Khorasani and Ascher 2015; Cortinovis and Kressner 2022) sharpened these bounds and extended them to indefinite matrices.

Setting

Let $A \in \mathbb{R}^{n\times n}$ be symmetric positive semi-definite, and write $\tau = \mathrm{trace}(A)$ . Fix a number of samples $M \ge 1$ . Let $z_1, \ldots, z_M \in \mathbb{R}^n$ be random vectors whose $Mn$ entries are independent standard normal random variables. The Gaussian trace estimator (Definition 3.1) is

G_M = \frac{1}{M}\sum_{i=1}^{M} z_i^T A z_i .

Each term $z_i^TAz_i$ has expectation $\mathrm{trace}(A)$ , so $G_M$ is unbiased. A randomized trace estimator $T$ is an $(\epsilon,\delta)$ -approximator of $\mathrm{trace}(A)$ (Definition 4.1) if

\Pr\bigl(|T - \mathrm{trace}(A)| \le \epsilon\,\mathrm{trace}(A)\bigr) \ge 1-\delta ,

that is, if its relative error is at most $\epsilon$ except on an event of probability at most $\delta$ .

The analysis uses the eigenvalues $\lambda_1,\ldots,\lambda_n \ge 0$ of $A$ , listed with multiplicity, and the polynomial $h(t) = \sum_{s=2}^{n}(-2)^s t^s \sum_{|S| = s}\prod_{i\in S}\lambda_i$ , where $S$ ranges over subsets of $\{1,\ldots,n\}$ ; it satisfies $\prod_i(1-2\lambda_i t) = 1 - 2\tau t + h(t)$ .

Formalization targets

Goal: Theorem 5.2 (corrected)

For every symmetric positive semi-definite $A$ , every $0 < \epsilon \le 1/10$ , every $0<\delta<1$ and every natural number $M$ with

M \ge 20\,\epsilon^{-2}\ln(2/\delta),

the estimator $G_M$ is an $(\epsilon,\delta)$ -approximator of $\mathrm{trace}(A)$ . The sample count depends on neither $n$ nor $A$ .

Milestones

Lemma 5.1. For symmetric $A$ , $\mathrm{E}(G_1) = \mathrm{trace}(A)$ and $\mathrm{Var}(G_1) = 2\|A\|_F^2$ .
Eq. (1). For symmetric $A$ and every $t$ with $2\lambda_i t < 1$ for all $i$ , the moment generating function of $Z = MG_M$ is

m_Z(t) = \prod_{i=1}^{n}(1-2\lambda_i t)^{-M/2} = (1 - 2\tau t + h(t))^{-M/2}.

Elementary symmetric sums (p. 8:8). For non-negative $x_1,\ldots,x_n$ and $1\le i\le n$ , $\sum_{|S|=i}\prod_{j\in S}x_j \le (\sum_j x_j)^i$ ; hence $|h(t)| \le \sum_{j=2}^{n}(2\tau t)^j$ for $t\ge0$ when all $\lambda_i\ge0$ .
Upper tail (pp. 8:8–8:9). If $\tau > 0$ , $M\ge1$ and $0<\epsilon\le 0.1$ , then

\Pr\bigl(G_M \ge \tau(1+\epsilon)\bigr) \le \exp(-M\epsilon^2/20).

Both tails (p. 8:9). If $\tau>0$ , $0<\epsilon\le0.1$ and $M \ge 20\epsilon^{-2}\ln(2/\delta)$ , then $\Pr(G_M \ge \tau(1+\epsilon)) \le \delta/2$ and $\Pr(G_M \le \tau(1-\epsilon)) \le \delta/2$ .

Significance

The theorem gives a number of matrix–vector products, $O(\epsilon^{-2}\ln(1/\delta))$ , that suffices for a relative-error guarantee on the trace of any positive semi-definite matrix, independent of its dimension and spectrum. It is the reference row of the paper's Table I, against which the Hutchinson, normalized Rayleigh-quotient and unit-vector estimators are compared, and it is the form in which trace estimation enters the analysis of randomized algorithms for log-determinants, spectral densities and matrix functions.

The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The mission produces a machine-checked version with the constant $20$ and the range of $\epsilon$ made explicit, and with the misprints of the printed argument resolved (see Formalization scope). It also produces reusable pieces: the moment generating function of a Gaussian quadratic form, and the bound on elementary symmetric sums by powers of the power sum. Sharper constants, the removal of the restriction $\epsilon\le 0.1$ , or a direct formalization of the lower tail through a $\chi^2$ tail bound are welcome as further theorems.

Difficulty

Unbiasedness and the variance formula do not give the result: Chebyshev's inequality with $\mathrm{Var}(G_M) = 2\|A\|_F^2/M \le 2\tau^2/M$ yields $M \ge 2\epsilon^{-2}\delta^{-1}$ , with a polynomial rather than logarithmic dependence on $1/\delta$ . A logarithmic bound needs exponential moments of $G_M$ , and the exponential moment of $z^TAz$ is finite only for $t$ below $1/(2\lambda_{\max})$ ; the argument has to choose $t$ inside that range uniformly in the spectrum, using only $\lambda_{\max}\le\tau$ . The second obstacle is distributional: $z^TAz$ is not a sum of independent terms in the coordinates of $z$ , and reducing it to a weighted sum of independent $\chi^2$ variables requires the rotation invariance of the standard Gaussian vector. The paper proves only the upper tail with an explicit constant and states that the lower tail follows "using the same technique"; that step has to be supplied.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ; "symmetric positive semi-definite" is A.PosSemidef, "symmetric" is A.IsHermitian, and eigenvalues are Matrix.IsHermitian.eigenvalues. The sample space is Fin M → Fin n → ℝ with the product measure of $Mn$ copies of gaussianReal 0 1, so the law of the samples is constructed, not assumed; $G_M(\omega) = (M:\mathbb{R})^{-1}\sum_i \omega_i\cdot(A\omega_i)$ . Probabilities are Measure.real; the moment generating function is Mathlib's mgf; the variance is Mathlib's variance, and Lemma 5.1 asserts square integrability so that neither the integral nor the variance takes its default value. The sample count is a natural number $M\ge1$ ; $\epsilon$ and $\delta$ are real.

Corrections of the printed text, each recorded in the item's Formalization Note:

Theorem 5.2 is printed without a range for $\epsilon$ and is false without one (for rank-one $A$ , $\epsilon=100$ , $\delta=e^{-400}$ the threshold allows $M=1$ , while $\Pr(\chi^2_1>101)\approx e^{-50}>\delta$ ). The proof gives its key bound "for $\epsilon\le0.1$ "; the goal is stated for $0<\epsilon\le 1/10$ .
Eq. (1) is printed for $|\lambda_i t|\le\frac12$ , which admits $1-2\lambda_it = 0$ , where the moment generating function is infinite. It is stated for $2\lambda_i t<1$ . The page's sum over subsets of "the set $\Lambda$ of eigenvalues" is taken over index sets, so repeated eigenvalues count with multiplicity.
The last paragraph of the proof prints $\Pr(G_M\le\tau(1+\epsilon))\le\delta/2$ for the upper tail and $\Pr(|G_M-\tau|\le\tau(1+\epsilon))\le\delta$ for the conclusion; the intended statements are $\Pr(G_M\ge\tau(1+\epsilon))\le\delta/2$ and $\Pr(|G_M-\tau|>\epsilon\tau)\le\delta$ . Milestone 5 states the upper and lower tail bounds.
Lemma 5.1 is followed by the remark that it "also applies when $A$ is non-symmetric"; this is false for the variance and is not formalized. Definition 3.1 says "positive-definite"; the estimator is defined for every matrix and each theorem carries its own hypothesis.
The one-sided tail milestones assume $\mathrm{trace}(A)>0$ ; for $A=0$ their events are certain, while the goal holds trivially.

A formalization that makes the goal trivial is ruled out: the estimator's law is the explicit product Gaussian measure rather than a hypothesis, $M$ ranges over all natural numbers above the threshold, and the approximator predicate is evaluated on the genuine event $|G_M - \mathrm{trace}(A)|\le\epsilon\,\mathrm{trace}(A)$ .

A complete development needs rotation invariance of the standard Gaussian on $\mathbb{R}^n$ (Mathlib's stdGaussian_map), the moment generating function of a squared standard normal, independence of products of Gaussian vectors, and a Chernoff bound from the moment generating function. The Gaussian quadratic-form results (milestones 1 and 2) are reusable for the other Gaussian estimators of the paper, such as the rank estimator of Lemma 5.3. Proofs of any milestone, alternative proofs of the lower tail, and helper lemmas on $\chi^2$ moment generating functions are welcome.

Selected references

H. Avron and S. Toledo, Randomized algorithms for estimating the trace of an implicit symmetric positive semi-definite matrix, Journal of the ACM 58(2), Article 8, 2011. https://doi.org/10.1145/1944345.1944349
M. F. Hutchinson, A stochastic estimator of the trace of the influence matrix for Laplacian smoothing splines, Communications in Statistics – Simulation and Computation 18(3), 1059–1076, 1989. https://doi.org/10.1080/03610918908812806
R. N. Silver and H. Röder, Calculation of densities of states and spectral functions by Chebyshev recursion and maximum entropy, Physical Review E 56(4), 4822–4829, 1997. https://doi.org/10.1103/PhysRevE.56.4822
F. Roosta-Khorasani and U. Ascher, Improved bounds on sample size for implicit matrix trace estimators, Foundations of Computational Mathematics 15, 1187–1212, 2015. https://doi.org/10.1007/s10208-014-9220-1
A. Cortinovis and D. Kressner, On randomized trace estimates for indefinite matrices with an application to determinants, Foundations of Computational Mathematics 22, 875–903, 2022. https://doi.org/10.1007/s10208-021-09525-9

9 thms3 active usersReviewed

Completed

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

Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers 2: A Threshold Nash Equilibrium under Announced Fixed-Discount PricingResearch Paper

Motivation

Retailers of fashion and seasonal goods sell at a premium price early in the season and mark down later. When customers anticipate the markdown, some of them wait, and the seller's pricing problem becomes a game between the seller and a population of forward-looking (strategic) customers. Aviv and Pazgal (MSOM 10(3), 2008) study this game in a model with limited inventory, stochastic arrivals and valuations that decline over the season, under two classes of seller policies: contingent pricing, where the discount depends on the inventory left, and announced fixed-discount pricing, where the seller commits to both prices upfront. Their numerical study (§7.3) compares the two classes and finds that precommitment can raise expected revenue by up to about 8%.

That comparison needs, for every announced price path, the customers' equilibrium response. Theorem 2 of the paper (p. 348) supplies it: a threshold purchasing policy, pinned down by a scalar fixed-point equation for the probability that a waiting customer is served. This mission formalizes Theorem 2. A companion mission of the same series formalizes Theorem 1, the contingent-pricing counterpart.

Setting

A seller has $Q \ge 1$ units to sell over a season $[0, H]$ , split at a fixed time $T$ with $0 < T \le H$ . Customers arrive by a Poisson process with rate $\lambda > 0$ . Customer $j$ has a base valuation $V_j$ drawn from a continuous distribution $F$ (tail $\bar F = 1 - F$ ), and at time $t$ values the product at $V_j(t) = V_j e^{-\alpha t}$ , where the decline factor $\alpha \ge 0$ is common to all customers.

Under an announced price path the seller commits to a premium price $p_1$ on $[0, T)$ and a discount price $p_2 \le p_1$ from $T$ on; $p_2$ does not depend on the remaining inventory. Customers know the initial inventory but not the current one.

A customer arriving at $t < T$ buys immediately if and only if (i) the current surplus $V(t) - p_1$ is nonnegative and (ii) it is at least the expected surplus of waiting,

\omega\cdot\max\{V(T) - p_2, 0\},

where $\omega$ is the probability that a unit will be allocated to the customer at time $T$ . Units left at $T$ are rationed at random among the customers who request one.

For a threshold function $\psi$ on $[0, T)$ the paper defines three segment rates: $\Lambda_I(\psi)$ , the expected number of customers who buy at $p_1$ ; $\Lambda_S(\psi, p_1, p_2)$ , those who could buy at $p_1$ but wait and want to buy at $p_2$ ; and $\Lambda_W(p_1, p_2)$ , those whose valuation was below $p_1$ and who want to buy at $p_2$ . Each is $\lambda$ times an integral over $[0, T]$ of $\bar F$ at scaled prices (p. 345). With $P(x \mid \Lambda)$ the Poisson probabilities, the allocation probability of $q$ units is

A(q \mid \Lambda) = \sum_{y=0}^{\infty} \frac{q}{\max\{1+y, q\}}\,P(y \mid \Lambda).

Formalization targets

Goal: Theorem 2 (p. 348)

For $w \in [0,1]$ let

\psi_A(t) = \max\left\{p_1, \frac{p_1 - wp_2}{1 - we^{-\alpha(T-t)}}\right\},\qquad 0 \le t < T, \tag{7}

and suppose $w$ solves

w = \sum_{x=0}^{Q-1} P\big(x \mid \Lambda_I(\psi_A)\big)\cdot A\big(Q-x \mid \Lambda_S(\psi_A, p_1, p_2) + \Lambda_W(p_1, p_2)\big). \tag{8}

Then, when all other customers use $\psi_A$ (so that a waiting customer is served with the probability on the right of (8)), every customer arriving at $t \in [0, T)$ buys immediately if and only if $V(t) \ge \psi_A(t)$ : the symmetric threshold profile is a Nash equilibrium.

Milestones: the two cases of the proof (p. 358)

If $e^{-\alpha(T-t)} \le p_2/p_1$ , the threshold is $p_1$ .
If $e^{-\alpha(T-t)} > p_2/p_1$ , the threshold is $(p_1 - wp_2)/(1 - we^{-\alpha(T-t)}) \ge p_1$ .

Significance

Theorem 2 reduces the customers' equilibrium under an announced path to a single scalar $w$ . Everything downstream in §5 and §7 rests on it: the seller's expected revenue $\pi_{A/S}(p_1, p_2)$ (p. 348) is written in terms of $\psi_A$ , the seller's optimal announced path maximizes it, and the comparison between announced and contingent pricing uses the resulting value $\pi^*_{A/S}$ . The theorem also explains the qualitative prediction of the model: the threshold exceeds $p_1$ exactly when the announced discount is deep relative to the decline of valuations, and it rises with the perceived availability $w$ .

The result is proved in the paper; to the best of our search it has no machine-checked proof. A formal development contributes the model objects (segment rates for threshold policies, the allocation probability for random rationing among Poisson requesters) in a form reusable by the rest of the series and by other strategic-customer pricing models, and a checked proof of the equilibrium property. The existence of a solution to (8) is not proved in the paper and is a natural further target.

Difficulty

The best-response part of the argument is elementary once the availability is known. The substance of the statement lies in the availability itself: the probability that a waiting customer is served is not a free parameter but the one generated, through (8), by the other customers' use of the same threshold. A formalization must connect the segment rates, the Poisson counts and random rationing into one expression and keep the fixed-point coupling between $w$ and $\psi_A$ intact; dropping it turns the theorem into a one-line inequality about an arbitrary $w$ . The division by $1 - we^{-\alpha(T-t)}$ also degenerates when $w = 1$ and $\alpha = 0$ , and has to be excluded explicitly.

Formalization scope

The Lean development lives in namespace SeasonalPricing.Announced. Conventions:

Time is real; base valuations have law μ : Measure ℝ with IsProbabilityMeasure μ, $F$ = ProbabilityTheory.cdf μ, and continuity of $F$ (the paper's "continuous distribution") is a hypothesis of the goal. No support condition on $[0,\infty)$ is imposed; the statement quantifies over every real base valuation $V$ .
$\Lambda_I, \Lambda_S, \Lambda_W$ are interval integrals over $[0, T]$ exactly as printed. $P(x \mid \Lambda) = e^{-\Lambda}\Lambda^x/x!$ is written out; $A(q\mid\Lambda)$ is the infinite series (tsum) as printed, not its closed form.
availability is the right-hand side of (8), with $\psi_A$ built from $w$ by (7).

Readings of the paper's informal words:

"Nash equilibrium" is read as the best-response property the paper's proof checks: against the availability generated by (8), the immediate-purchase rule of p. 344 coincides with the threshold $\psi_A$ at every $t \in [0, T)$ and every valuation. The paper defines no strategy space beyond threshold rules.
" $w$ is a solution to (8)": the theorem is conditional on a solution; its existence is neither assumed elsewhere nor claimed. The conditional statement has content only when (8) has a solution, which the paper does not prove.
$w$ as a likelihood: $0 \le w \le 1$ is a hypothesis (it also follows from (8)).
Added hypothesis: $\alpha > 0$ or $w < 1$ , which keeps $1 - we^{-\alpha(T-t)} > 0$ for $t < T$ ; the paper's formula is undefined when it fails. In the milestones the same condition appears as $we^{-\alpha(T-t)} < 1$ , and $0 < p_1$ is added so that $p_2/p_1$ is meaningful.
The rule on $[T, H]$ (buy at $T$ iff $V(T) > p_2$ ) is part of the model and is not restated; $H$ does not enter the statements.

A formalization in which $w$ is an arbitrary number in $[0,1]$ , not tied to (8), is ruled out: it is the best-response lemma alone, not Theorem 2. Contributions welcome: proofs of the two milestones and the goal; lemmas such as $0 \le A(q\mid\Lambda) \le 1$ and summability of its series; the closed form of $A(q \mid \Lambda)$ printed on p. 346; and an existence result for (8).

Selected references

Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
X. Su, Intertemporal Pricing with Strategic Customer Behavior, Management Science 53(5):726–741, 2007. https://doi.org/10.1287/mnsc.1060.0667

5 thms3 active usersReviewed

Completed

Machine Learning Optimization Probability+1·Captain: mikedeng1

Simultaneous Analysis of Lasso and Dantzig Selector III: A Sparsity Oracle Inequality for the LassoResearch Paper

Motivation

In high-dimensional regression the number of candidate predictors $M$ can far exceed the number of observations $n$ . A regression function can then be estimated only if it is well approximated by a combination of a few elements of a large dictionary. The Lasso is the most widely used estimator in this regime. The question this mission formalizes is how well the Lasso predicts when the truth is not assumed to be sparse, or even to lie in the span of the dictionary.

A sparsity oracle inequality answers it. It bounds the prediction error of the estimator by the error of the best sparse approximation of the truth, which only an oracle knowing the truth could compute, plus a remainder proportional to the sparsity of that approximation times $\log M/n$ . Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 37(4), 2009) proved such an inequality for the Lasso under their restricted eigenvalue (RE) condition. Earlier oracle inequalities for Lasso-type estimators in fixed design (Bunea, Tsybakov and Wegkamp, 2006–2007) required the Gram matrix to be positive definite or to satisfy a mutual-coherence condition. The RE condition is weaker and allows $M\gg n$ , and it is now the standard hypothesis in this literature.

Setting

A dictionary $f_1,\dots,f_M$ is evaluated at fixed points $Z_1,\dots,Z_n$ . This gives the design matrix $X=(f_j(Z_i))\in\mathbb R^{n\times M}$ and, for an unknown regression function $f$ , the vector $f=(f(Z_1),\dots,f(Z_n))^\top$ . The observations are

y=f+W,\qquad W_1,\dots,W_n\ \text{independent}\ \mathcal N(0,\sigma^2),\ \sigma>0 .

Nothing is assumed about $f$ . For $v\in\mathbb R^n$ the empirical norm is $\|v\|_n=(\frac1n\sum_iv_i^2)^{1/2}$ , and for $\beta\in\mathbb R^M$ we write $f_\beta=X\beta$ . The column norms $\|f_j\|_n$ are assumed nonzero, with $f_{\max}=\max_j\|f_j\|_n$ and $f_{\min}=\min_j\|f_j\|_n$ . The support of $\beta$ is $J(\beta)=\{j:\beta_j\neq0\}$ and its sparsity is $\mathcal M(\beta)=|J(\beta)|$ .

The Lasso $\hat\beta_L$ is any minimiser of

\frac1n\sum_{i=1}^n\big(y_i-(X\beta)_i\big)^2+2r\sum_{j=1}^M\|f_j\|_n|\beta_j|,\qquad r=A\sigma\sqrt{\frac{\log M}{n}},\ A>2\sqrt2,

and $\hat f_L=X\hat\beta_L$ .

Assumption RE $(s,c_0)$ holds with constant $\kappa>0$ if, for every $J_0\subseteq\{1,\dots,M\}$ with $|J_0|\le s$ and every $\delta\neq0$ with $|\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1$ ,

\kappa\sqrt n\,|\delta_{J_0}|_2\le|X\delta|_2 .

The paper's $\kappa(s,c_0)$ is the largest such constant.

Formalization targets

Goal: Theorem 6.1

Fix $\varepsilon>0$ , $n\ge1$ , $M\ge2$ , $1\le s\le M$ , and let RE $(s,(3+4/\varepsilon)f_{\max}/f_{\min})$ hold with constant $\kappa$ . With probability at least $1-M^{1-A^2/8}$ , every Lasso solution satisfies, simultaneously for all $\beta$ with $\mathcal M(\beta)\le s$ ,

\|\hat f_L-f\|_n^2\le(1+\varepsilon)\Big\{\|f_\beta-f\|_n^2+C(\varepsilon)\frac{f_{\max}^2A^2\sigma^2}{\kappa^2}\,\frac{\mathcal M(\beta)\log M}{n}\Big\},\qquad C(\varepsilon)=\frac{4(2+\varepsilon)^2}{\varepsilon(1+\varepsilon)} .

Milestones

(B.4): the noise event $\mathcal A=\bigcap_j\{2|V_j|\le r\|f_j\|_n\}$ , with $V_j=n^{-1}\sum_iX_{ij}W_i$ , satisfies $P(\mathcal A^c)\le M^{1-A^2/8}$ .
(B.1) on $\mathcal A$ : for every Lasso solution and every $\beta$ ,

\|\hat f_L-f\|_n^2+r\sum_j\|f_j\|_n|\hat\beta_j-\beta_j|\le\|f_\beta-f\|_n^2+4r\sum_{j\in J(\beta)}\|f_j\|_n|\hat\beta_j-\beta_j| .

Lemma B.1: the same inequality with probability at least $1-M^{1-A^2/8}$ .
Cone step: in the case $\varepsilon\|f_\beta-f\|_n^2<4r\sum_{J(\beta)}\|f_j\|_n|\hat\beta_j-\beta_j|$ , the difference $\hat\beta_L-\beta$ lies in the cone with constant $(3+4/\varepsilon)f_{\max}/f_{\min}$ at $J(\beta)$ .
Inequality before decoupling: $\|\hat f_L-f\|_n^2\le\|f_\beta-f\|_n^2+4rf_{\max}\kappa^{-1}\sqrt{\mathcal M(\beta)}\,(\|\hat f_L-f\|_n+\|f_\beta-f\|_n)$ .
Decoupled bound: $\|\hat f_L-f\|_n^2\le\frac{b+1}{b-1}\|f_\beta-f\|_n^2+\frac{8b^2f_{\max}^2}{(b-1)\kappa^2}r^2\mathcal M(\beta)$ for all $b>1$ .
Corollary 6.2: the same oracle inequality with $\gamma$ in place of $\kappa$ and no global RE assumption. The infimum runs over those $\beta$ with $\mathcal M(\beta)\le s$ whose support alone satisfies the restricted eigenvalue inequality with constant $\gamma$ .

Significance

The theorem says that, up to the factor $1+\varepsilon$ and a remainder of order $\mathcal M(\beta)\log M/n$ , the Lasso predicts as well as the best $s$ -sparse linear combination of the dictionary. This is the case even when $f$ is not sparse and not in the span of the dictionary. The remainder is the parametric rate for $\mathcal M(\beta)$ parameters, inflated by $\log M$ and by the ill-posedness factor $f_{\max}^2/\kappa^2$ . Together with Theorem 5.1 of the same paper (mission II of this series), it shows that the Lasso and the Dantzig selector are within the same distance of the sparse oracle. The oracle inequality is used in aggregation, in model selection, and as a black box in later sparse-estimation papers.

The result is proved in the paper. It has not been formalized: at the time of writing, no Lasso oracle inequality and no probabilistic Lasso bound exist on Prove2Me or in Mathlib. What this mission contributes is a machine-checked proof of the paper's Theorem 6.1 with an explicit constant $C(\varepsilon)$ . The paper leaves $C(\varepsilon)$ unspecified, and its proof fixes the value used here. The mission also formalizes the Gaussian-tail step (B.4) and the deterministic basic inequality (B.1), both of which are shared with the paper's other Lasso results.

Difficulty

There is no sparse truth, so the usual argument does not apply. That argument places the error $\hat\beta_L-\beta^*$ in the RE cone and reads off a rate. Here the competitor $\beta$ is arbitrary, and the approximation error $\|f_\beta-f\|_n$ can dominate the penalty terms, in which case the error is not in the cone. The RE assumption can be used only where the error does lie in a cone, and the cone constant available there depends on $\varepsilon$ and on the column-norm ratio $f_{\max}/f_{\min}$ , because the penalty is weighted while RE is stated for unweighted vectors. What RE then yields is an inequality quadratic in $\|\hat f_L-f\|_n$ with a cross term, not the $(1+\varepsilon)$ form directly, and the constant $C(\varepsilon)$ is determined by how that cross term is absorbed. On the probabilistic side, the whole argument must run on one event of probability at least $1-M^{1-A^2/8}$ . That event may depend neither on $\beta$ nor on the choice of minimiser. The Lasso need not have a unique solution.

Formalization scope

The dictionary enters only through $X\in\mathbb R^{n\times M}$ (Matrix (Fin n) (Fin M) ℝ) and the target only through $f\in\mathbb R^n$ , which is arbitrary. The noise is a family W : Fin n → Ω → ℝ of measurable, independent random variables, each with law gaussianReal 0 σ², and $\sigma>0$ .
The Lasso is an argmin predicate, and every statement is made for every minimiser. "With probability at least $p$ " means a measurable event $E$ with $P(E)\ge p$ , chosen before the competitor $\beta$ and the minimiser.
RE is stated through a witness $\kappa>0$ . Since $\kappa(s,c_0)$ is attained and every bound decreases in $\kappa$ , this is equivalent to the paper's form, and it avoids a real infimum over an empty set.
The infimum over $\{\beta:\mathcal M(\beta)\le s\}$ is written as "for every such $\beta$ ". This is equivalent, because the set contains $\beta=0$ and the bracket is nonnegative.
Correction/strengthening. The printed theorem has an unspecified $C(\varepsilon)>0$ . The goal instead uses the value $C(\varepsilon)=4(2+\varepsilon)^2/(\varepsilon(1+\varepsilon))$ that the proof yields with $b=1+2/\varepsilon$ , and this implies the printed statement. Corollary 6.2 uses the same explicit constant.
The standing assumptions of Section 2 ( $M\ge2$ and every $\|f_j\|_n\neq0$ ) are hypotheses of every theorem.
Some formalizations would make the result trivial, and they are excluded here. The noise must be exactly i.i.d. $\mathcal N(0,\sigma^2)$ with $\sigma>0$ and must enter only through $y=f+W$ . The target $f$ must not be restricted to $X\beta^*$ . The event must be measurable. The constant must depend on $\varepsilon$ alone.
A single definition file provides the empirical norms, $f_{\max}$ , $f_{\min}$ , support and sparsity, the weighted Lasso, RE and its single-set version (the family $\Lambda_{s,\gamma,c_0}$ of Corollary 6.2), the Gaussian noise model and the event $\mathcal A$ . The same objects appear in the other missions of this series. Gaussian-tail and union-bound lemmas proved along the way are reusable, and contributions of such lemmas are welcome.

Selected references

P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. Cited version: arXiv:0801.1095v3; DOI 10.1214/08-AOS620.
F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Statist. 1, 169–194, 2007. DOI 10.1214/07-EJS008.
F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Aggregation for Gaussian regression, Ann. Statist. 35(4), 1674–1697, 2007. DOI 10.1214/009053606000001587.
R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Stat. Soc. B 58(1), 267–288, 1996. DOI 10.1111/j.2517-6161.1996.tb02080.x.

9 thms3 active usersReviewed