Operations Research

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

1. Eq. (3.4): $w(\pi)=\min_A\{c_A+\sum_i\pi_i(v_A)_i\}$ over all $n^n$ assignments $A$.
2. §3, Eqs. (3.1)–(3.3): $w$ attains its maximum, and $\max w$ equals the cost of an optimal permutation.
3. 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)$.
4. 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

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:

1. (§2, p. 3) $C = \operatorname{conv}(\operatorname{ext} C)$ and $C^\circ = \operatorname{conv}(\operatorname{ext} C^\circ)$.
2. (proof, p. 4) For every $c\in\operatorname{ext}(C^\circ)$, $\max\{\langle c,x\rangle : x\in C\} = 1$, attained.
3. (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

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

1. 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$.
2. 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]$.
3. 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$.
4. 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.
5. §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

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

1. Eq. (16). Every perturbation with $\|[\Delta A\ \Delta b]\|_F \le 1$ has residual at most $\|Ax-b\| + \sqrt{\|x\|^2+1}$.
2. 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.
3. Spectral norm. The worst case over the larger ball $\|[\Delta A\ \Delta b]\| \le 1$ is the same value.
4. Strict convexity. $x \mapsto r(A,b,x)$ is strictly convex on $\mathbb{R}^m$.
5. 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

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).

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

1. Laziness (p. 4): every deterministic algorithm is dominated by a lazy one (a published theorem, reused).
2. 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'$.
3. Stale set before the terminating request (p. 6): it has $l+1$ elements, each covered with probability $1/(l+1)$.
4. Expected cost of a phase to EATR (p. 6): exactly $l+\frac{l}{l+1}$.
5. 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).

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

1. (Section 5, p. 12) $\rho_\gamma$ is a conditional convex risk measure.
2. (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}\}$.
3. (Proof of Proposition 5.4) $\rho_\gamma$ is continuous from above: $X_n\searrow X$ implies $\rho_\gamma(X_n)\nearrow\rho_\gamma(X)$.
4. (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)$.
5. (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)\}$.
6. (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