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.

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.

≤ 19.8899945Formalized record≤ 14.797074Open frontier

6 provers on it3 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.

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.

≤ 19.8899945Formalized record≤ 14.797074Open frontier

6 provers on it3 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 Linear Optimization Operations Research+1·Captain: mikedeng1

Cones of Matrices and Set-Functions and 0–1 Optimization I: n Rounds of the Lovász–Schrijver N Operator Give the 0–1 HullResearch Paper

Motivation

A 0–1 integer program asks for the best 0–1 vector satisfying a system of linear inequalities. Its linear relaxation is easy to optimize over, but the relaxation is usually much larger than the convex hull of the 0–1 solutions. Lift-and-project methods close this gap systematically: they lift the relaxation to a higher-dimensional space, add constraints that every 0–1 point satisfies there, and project back, obtaining a tighter relaxation that still contains every 0–1 solution.

L. Lovász and A. Schrijver introduced one of the two standard lift-and-project hierarchies in Cones of matrices and set-functions and 0–1 optimization (SIAM J. Optim., 1991). Their operators $N$ and $N_+$ represent a 0–1 point $x$ by the matrix $xx^{\mathsf T}$ , impose linear (and for $N_+$ semidefinite) constraints on such matrices, and project back to $\mathbb R^{n+1}$ . The same paper applies the operators to the stable set polytope, where one round already produces the odd hole, odd wheel, clique and odd antihole constraints. The Lovász–Schrijver hierarchy, the Sherali–Adams hierarchy (1990) and Lasserre's semidefinite hierarchy (2001) are the three reference lift-and-project methods; their rank lower bounds are a standard tool for proving that a relaxation cannot solve a combinatorial problem in few rounds.

This mission formalizes the first structural fact about the operator $N$ : iterating it $n$ times on any relaxation in $n$ variables yields exactly the 0–1 hull (Theorem 1.4 of the paper).

Setting

Vectors live in $\mathbb R^{n+1}$ with coordinates $x_0, x_1, \dots, x_n$ ; the space $\mathbb R^n$ of the original problem is the hyperplane $x_0 = 1$ , and polytopes are replaced by the convex cones they generate.

A convex cone is a nonempty set closed under addition and nonnegative scaling. For a set $S$ , $\operatorname{cone}(S)$ is the set of nonnegative combinations of finitely many vectors of $S$ .
The polar cone of $K$ is $K^* = \{u : u^{\mathsf T}x \ge 0 \text{ for all } x \in K\}$ .
A 0–1 vector has every coordinate, $x_0$ included, equal to $0$ or $1$ . The cube cone $Q$ is the cone spanned by the 0–1 vectors with $x_0 = 1$ ; it is the cone over the unit cube.
For a convex cone $K$ , $K^\circ$ is the cone spanned by the 0–1 vectors in $K$ . For $K \subseteq Q$ this is the cone over the convex hull of the 0–1 points of the relaxation.

For convex cones $K_1, K_2 \subseteq Q$ , the matrix cone $M(K_1, K_2)$ consists of the $(n+1)\times(n+1)$ real matrices $Y = (y_{ij})$ such that

$Y$ is symmetric;
$y_{ii} = y_{0i}$ for $1 \le i \le n$ (the diagonal equals the 0th column);
$u^{\mathsf T} Y v \ge 0$ for every $u \in K_1^*$ and $v \in K_2^*$ .

$M_+(K_1, K_2)$ adds the condition that $Y$ is positive semidefinite. The projections are $N(K_1, K_2) = \{Ye_0 : Y \in M(K_1, K_2)\}$ and $N_+(K_1, K_2) = \{Ye_0 : Y \in M_+(K_1, K_2)\}$ , where $e_0$ is the 0th unit vector. The cut operator is $N(K) = N(K, Q)$ , and its iterates are $N^0(K) = K$ , $N^t(K) = N(N^{t-1}(K))$ .

Two families of hyperplanes appear in the proofs: $H_i = \{x : x_i = 0\}$ and $G_i = \{x : x_i = x_0\}$ , the hyperplanes through the two opposite facets of $Q$ in direction $i$ .

Formalization targets

Goal: Theorem 1.4

For every closed convex cone $K \subseteq Q$ ,

N^n(K) = K^\circ .

The statement is uniform in $n$ and in $K$ : no polyhedrality, no bound on the number of constraints, and no assumption that $K$ contains a 0–1 point.

Milestones

Condition (iii″). For a closed convex cone $K \subseteq Q$ and a symmetric $Y$ with $y_{ii} = y_{0i}$ : $Y \in M(K, Q)$ if and only if every column of $Y$ is in $K$ and the difference of the first column and any other column is in $K$ .
Lemma 1.1. For closed convex cones $K_1, K_2 \subseteq Q$ ,

(K_1 \cap K_2)^\circ \subseteq N_+(K_1, K_2) \subseteq N(K_1, K_2) \subseteq K_1 \cap K_2 .

Lemma 1.3. For a closed convex cone $K \subseteq Q$ and every $1 \le i \le n$ ,

N(K) \subseteq (K \cap H_i) + (K \cap G_i).

Claim (4) in the proof of Theorem 1.4. For every set $T$ of $t \ge 1$ coordinates, with $\bar F$ the union of the faces of the unit cube that fix the coordinates in $T$ to $0$ or $1$ ,

N^t(K) \subseteq \operatorname{cone}(K \cap \bar F).

The remark after Lemma 1.1. $N(K_1 \cap K_2, K_1 \cap K_2) \subseteq N(K_1, K_2) \subseteq N(K_1 \cap K_2, Q)$ .

Significance

Theorem 1.4 is what makes $N$ a hierarchy rather than a single cut: the relaxations $K \supseteq N(K) \supseteq N^2(K) \supseteq \dots$ reach the 0–1 hull after at most $n$ rounds, so the $N$ -rank of a valid inequality (the least $t$ with the inequality valid for $N^t(K)$ ) is a well-defined number between $0$ and $n$ . The rest of the paper measures combinatorial constraints by this rank: odd hole constraints have rank one on the stable set polytope, and the rank of a stable set inequality is bounded by its defect. Rank lower bounds for lift-and-project hierarchies, in the literature that followed, all presuppose this finite convergence.

The theorem is proved in the paper; to the best of available knowledge none of the Lovász–Schrijver operators has been formalized in a proof assistant. A formalization provides machine-checked definitions of the matrix cones and the cut operators that later missions in this series (odd holes, the defect bound, the $N_+$ constraints) state their results against, and a checked proof of the column characterization (iii″) that all of those proofs use.

Difficulty

The inclusion $K^\circ \subseteq N^n(K)$ follows from Lemma 1.1 once each $N^t(K)$ is known to be a convex cone. The reverse inclusion is the content. A first attempt shows that one round of $N$ forces one coordinate to be integral, and then iterates; but $N(K)$ is not contained in the union of $K \cap H_i$ and $K \cap G_i$ , only in their Minkowski sum (Lemma 1.3), so a point of $N(K)$ is not itself integral in any coordinate. The induction must carry a statement about cones spanned by intersections with unions of cube faces, and it needs each iterate $N^t(K)$ to again be a closed convex cone inside $Q$ so that Lemma 1.3 can be reapplied. Closedness of the projection $N(K)$ is not automatic: a linear image of a closed cone need not be closed.

Formalization scope

Coordinates of $\mathbb R^{n+1}$ are indexed by Option ι for a finite type ι; none is $x_0$ and some i is $x_i$ , and $n$ is the cardinality of ι, which may be $0$ .
$\operatorname{cone}(S)$ is Mathlib's PointedCone.hull ℝ S; $Q$ and $K^\circ$ are defined as spans of 0–1 vectors, as on the page, not by the inequality description $0 \le x_i \le x_0$ .
$M(K_1, K_2)$ is defined by condition (iii) through the polar cones; the column form (iii″) is a milestone, not the definition.
The operators $N$ , $N_+$ and the iterates are defined on arbitrary sets; the hypotheses (convex cone, contained in $Q$ , closed) are carried by the theorems.
Closedness. The paper tacitly takes its cones closed (they are polyhedral in all its applications), and the rewriting (iii′) on p. 169 needs it. Every statement here assumes the cones closed. Without this the goal is false: for $K = \{x : 0 < x_1 < x_0\} \cup \{0\}$ in $\mathbb R^2$ , $K^\circ = \{0\}$ while $N(K) = Q$ .
In the proof of Theorem 1.4 the page places the cube $Q'$ in the hyperplane " $x_0 = 0$ "; this is a misprint for $x_0 = 1$ , and claim (4) is formalized with $x_0 = 1$ .
Not formalized in this mission: Lemma 1.2 (the dual description of $N(K)^*$ ), Lemma 1.5 (the $N_+$ analogue of Lemma 1.3, part of a later mission), and the algorithmic results of Section 1.c.

Contributions welcome: proofs that $N(K)$ is a closed convex cone contained in $Q$ whenever $K$ is, a proof of $Q^* = \operatorname{cone}\{e_i, e_0 - e_i\}$ , and lemmas on cones spanned by the intersection of a generating set with a supporting hyperplane; these are reusable by the other missions of the series.

Selected references

L. Lovász and A. Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM Journal on Optimization 1(2) (1991) 166–190. https://doi.org/10.1137/0801013
H. D. Sherali and W. P. Adams, A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems, SIAM Journal on Discrete Mathematics 3(3) (1990) 411–430. https://doi.org/10.1137/0403036
J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM Journal on Optimization 11(3) (2001) 796–817. https://doi.org/10.1137/S1052623400366802
M. Laurent, A comparison of the Sherali–Adams, Lovász–Schrijver, and Lasserre relaxations for 0–1 programming, Mathematics of Operations Research 28(3) (2003) 470–496. https://doi.org/10.1287/moor.28.3.470.16391

8 thms3 active usersReviewed

Completed

Control Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Supervisory Control of a Class of Discrete Event Processes I: Minimally Restrictive Supervisors Exist iff the Supremal Controllable Legal Sublanguage Contains the Minimal Acceptable LanguageResearch Paper

Motivation

Manufacturing cells, communication protocols, traffic systems and database transaction managers are naturally described not by differential equations but by sequences of discrete events: a machine starts, a part arrives, a message is lost. Ramadge and Wonham's 1987 paper (SIAM J. Control Optim. 25(1)) set up a control theory for such systems in which the plant is an automaton, the controller is another automaton that may disable some events, and specifications are formal languages. The framework, now called supervisory control theory or the Ramadge–Wonham framework, is the standard model for the logical control of discrete event systems and underlies the textbook treatment in Cassandras and Lafortune (Introduction to Discrete Event Systems, 2008) and Wonham and Cai (Supervisory Control of Discrete-Event Systems, 2019).

The question the paper answers is the basic synthesis question of the theory: given a plant, a set of legal behaviours and a set of minimally acceptable behaviours, when does a controller exist that keeps the plant legal, achieves at least the acceptable behaviour, and never deadlocks, and what is the least restrictive such controller?

Setting

A generator is $\mathcal G = (Q, \Sigma, \delta, q_0, Q_m)$ with a state set $Q$ , a finite alphabet $\Sigma$ of events, a partial transition function $\delta : \Sigma \times Q \to Q$ , an initial state $q_0$ and marker states $Q_m \subseteq Q$ . Extending $\delta$ to strings, the generated language $L(\mathcal G)$ is the set of strings $w$ for which $\delta(w, q_0)$ is defined, and the marked language $L_m(\mathcal G)$ is the subset of those that end in $Q_m$ . The closure $\bar K$ of a language $K$ is its set of prefixes; $K$ is closed if $K = \bar K$ . Throughout, $\mathcal G$ is assumed trim in the sense $L(\mathcal G) = \bar L_m(\mathcal G)$ : every generated string can be completed to a marked one.

The alphabet is split into controllable events $\Sigma_c$ and uncontrollable events $\Sigma_u = \Sigma - \Sigma_c$ . A supervisor $\mathcal S = (S, \phi)$ consists of a deterministic, accessible automaton $S = (X, \Sigma, \xi, x_0, X_m)$ , whose state set $X$ may be infinite, and a map $\phi$ assigning to each state $x$ the set of controllable events it enables; uncontrollable events are always enabled. The closed loop $\mathcal S/\mathcal G$ runs $S$ and $\mathcal G$ in lockstep: an event occurs when the plant can execute it, the supervisor enables it, and the supervisor's automaton can follow it. This defines the languages $L(\mathcal S/\mathcal G)$ , $L_m(\mathcal S/\mathcal G)$ and the controlled language $L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G) \cap L_m(\mathcal G)$ .

$\mathcal S$ is complete if its automaton never refuses an event that the plant can execute and $\phi$ enables; it is proper if it is complete and

\bar L_m(\mathcal S/\mathcal G) = \bar L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G),

that is, every closed-loop string can be completed to a marked task. A language $K$ is controllable if $K \subseteq L(\mathcal G)$ and $\bar K \Sigma_u \cap L(\mathcal G) \subseteq \bar K$ . For $L \subseteq L(\mathcal G)$ , $\mathbf C_{\mathcal G}(L)$ is the class of controllable sublanguages of $L$ and $\mathbf F_{\mathcal G}(L)$ the class of sublanguages $K$ of $L$ with $K = \bar K \cap L_m(\mathcal G)$ .

Given $\emptyset \neq L_a \subseteq L_g \subseteq L_m(\mathcal G)$ , the Supervisory Marking Problem (SMP) asks for a proper $\mathcal S$ with $L_a \subseteq L_m(\mathcal S/\mathcal G) \subseteq L_g$ , and the Supervisory Control Problem (SCP) for a proper $\mathcal S$ with $L_a \subseteq L_c(\mathcal S/\mathcal G) \subseteq L_g$ .

Formalization targets

Goal: Theorem 7.1 (pp. 218–219)

\text{SMP solvable} \iff \sup \mathbf C_{\mathcal G}(L_g) \supseteq L_a, \qquad \text{SCP solvable} \iff \sup\{\mathbf C_{\mathcal G}(L_g) \cap \mathbf F_{\mathcal G}(L_g)\} \supseteq L_a,

and in each case the solving supervisor can be taken minimally restrictive: its marked (respectively controlled) language equals the supremal element and contains that of every proper supervisor whose language lies in $L_g$ .

Milestones

Proposition 4.1 (i), (ii): marking is independent of control; every $K \subseteq L_m(\mathcal G)$ , or $K \subseteq L \cap L_m(\mathcal G)$ for an achievable closed $L$ , is the marked language of a complete supervisor.
Proposition 5.1: a complete supervisor realizes $(L_m, L_c, L) = (K_1, K_2, K_3)$ iff $K_1 \subseteq K_2$ , $K_2 = K_3 \cap L_m(\mathcal G)$ and $K_3$ is closed and controllable.
Theorem 6.1 (i), (ii): a proper supervisor with $L_m(\mathcal S/\mathcal G) = K$ exists iff $K$ is controllable; one with $L_c(\mathcal S/\mathcal G) = K$ exists iff $K$ is controllable and $L_m(\mathcal G)$ -closed.
Proposition 7.1: $\mathbf C_{\mathcal G}(L)$ and $\mathbf F_{\mathcal G}(L)$ contain $\emptyset$ and are closed under arbitrary unions.
The supremal elements (p. 218): $\sup \mathbf C_{\mathcal G}(L)$ , $\sup \mathbf F_{\mathcal G}(L)$ and $\sup\{\mathbf C_{\mathcal G}(L) \cap \mathbf F_{\mathcal G}(L)\}$ belong to their classes.

Significance

Theorem 7.1 reduces the existence of a correct, non-blocking controller to a single language inclusion, and identifies the supremal controllable sublanguage as the behaviour of the least restrictive solution. That object is the backbone of the later theory: modular and decentralized control, control under partial observation, and the computational results that $\sup \mathbf C_{\mathcal G}(L)$ is regular and computable when $\mathcal G$ is finite and $L$ regular all start from it.

The result is proved in the paper and has been taught for decades; it is not open. Mathlib has no model of generators with partial transitions, supervisors or controllability (its DFA has a total transition function and a single accepted language), and no formalization of this theory exists on the platform. This mission provides one: a reusable Lean model of generators with partial transitions, supervisors with possibly infinite state, closed loops and controllability, together with the paper's existence theorems stated against it. A second mission on the same paper (quotients of supervisors, Theorem 10.1) builds on the same objects.

Difficulty

The combinatorial core of Proposition 7.1 is a short prefix-closure computation. The work lies in the constructions: to show existence, a supervisor must be built for an arbitrary controllable language, which in general is not regular, so the supervisor needs an infinite state set (for example strings of the target language) together with a proof that the closed loop generates exactly the intended language, is complete, and is proper. The converse directions require relating the closed-loop run to separate runs of the plant and of the supervisor's automaton. The naive shortcut of reading the "sup" as an arbitrary member of $\mathbf C_{\mathcal G}(L_g)$ containing $L_a$ skips the content of the supremal-element milestone; the goal is stated with the actual union.

Formalization scope

The alphabet is a type α with [Fintype α]; strings are List α, the empty string is [], and $s\sigma$ is s ++ [σ]. Languages are Set (List α); the closure is pre K = {s | ∃ t, s ++ t ∈ K}.
A generator is a structure with a state type Q : Type, a partial transition δ : α → Q → Option Q, an initial state and a marker set. No finiteness is assumed on states, of the plant or of the supervisor. Supervisors and generators live in Type 1.
$\phi$ maps states to Ec → Bool; an event outside $\Sigma_c$ is enabled by definition, so uncontrollable events cannot be disabled.
The closed loop is the product run from $(x_0, q_0)$ ; the accessible part in the paper's display (2.1) changes no language and is not built.
Standing assumptions carried by every theorem: $\Sigma$ finite, $L(\mathcal G) = \bar L_m(\mathcal G)$ , supervisor automata accessible (as a hypothesis on every input supervisor and a conjunct of every "there exists a supervisor").
$\sup$ is sSup in the complete lattice Set (List α).
A formalization in which the closed loop ignores $\phi$ or the plant, in which completeness is dropped from properness, or in which the supervisor is restricted to finitely many states, is not the paper's theorem and is ruled out by the definitions above.

Welcome contributions: the basic run lemmas (closed-loop runs project to plant and supervisor runs), the string-state supervisor construction, and proofs of the milestones in the given order.

Selected references

P. J. Ramadge and W. M. Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM J. Control Optim. 25(1):206–230, 1987. https://doi.org/10.1137/0325013
W. M. Wonham and P. J. Ramadge, On the Supremal Controllable Sublanguage of a Given Language, SIAM J. Control Optim. 25(3):637–659, 1987. https://doi.org/10.1137/0325036
C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems, 2nd ed., Springer, 2008. https://doi.org/10.1007/978-0-387-68612-7
W. M. Wonham and K. Cai, Supervisory Control of Discrete-Event Systems, Springer, 2019. https://doi.org/10.1007/978-3-319-77452-7

12 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Approximation Algorithms for Combinatorial Problems V: The Overlap-Ratio Greedy C2 Is Within 1 + ln k of the Least-Overlap Cover on EC(k)Research Paper

Motivation

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9 (1974) 256–278) was one of the first systematic worst-case analyses of polynomial-time heuristics for NP-complete optimization problems. Its Section 5 proves the harmonic bound $\sum_{j=1}^k 1/j$ for the greedy algorithm on minimum-cardinality set cover, a result that still underlies the standard $\ln n$ approximation guarantee.

Section 6, the subject of this mission, asks what happens when the cost of a cover is its total size rather than its number of sets. This problem, SET COVERING II (EC), is the optimization version of the EXACT COVER recognition problem of Karp's list (Karp 1972): a family has a disjoint subcover exactly when the optimum equals the number of covered points. Johnson shows that the change of measure breaks the cardinality greedy but that a greedy rule based on an overlap ratio recovers essentially the same guarantee. The same accounting (paying for each newly covered point) later became the standard analysis of greedy weighted set cover (Chvátal 1979).

Setting

An input is a finite family $F = \{S_1, \dots, S_p\}$ of finite sets. Its covered set is $T = \bigcup_{S \in F} S$ . A subcover is a subfamily $F' \subseteq F$ with $\bigcup_{S\in F'} S = T$ , and its measure is

m_{EC}(F') = \sum_{S \in F'} |S|.

The optimum $F^*$ is the least measure of a subcover; since every subcover has measure at least $|T|$ , an optimal subcover is one with the least possible overlapping. The subproblem EC $(k)$ admits only families in which every set has at most $k$ points.

Algorithm C2 keeps a subfamily SUB (initially empty), the unused sets LEFT (initially $F$ ) and the uncovered points UNCOV (initially $T$ ). While UNCOV is nonempty it chooses $S' \in$ LEFT minimizing

\mathrm{Ratio}(S) = \frac{|S - \mathrm{UNCOV}|}{|S \cap \mathrm{UNCOV}|},

the number of already-covered points of $S$ per newly covered point, and moves $S'$ from LEFT to SUB, removing its points from UNCOV. When several sets tie, any of them may be chosen; a subcover is choosable by C2 if some sequence of admissible choices returns it.

The overlap of a chosen set is $|S' - \mathrm{UNCOV}|$ at the moment it is chosen, and the cumulative overlap $\mathrm{OV}(F_1)$ of a run returning $F_1$ is the sum of these overlaps.

Formalization targets

Goal: Theorem 6 (p. 271)

For all $k \ge 1$ and $n > 0$ ,

R[C2, EC(k)](n) \le 1 + \ln(k) \le \sum_{j=1}^k \frac1j + \frac12,

and for all sufficiently large $n$ , $R[C2, EC(k)](n) \ge \sum_{j=1}^k (1/j)$ . In the size-free form used here, for every $k \ge 1$ :

every subcover $M$ choosable by C2 on an input of EC $(k)$ satisfies $m_{EC}(M) \le (1 + \ln k)\,F^*$ ;
$1 + \ln k \le \sum_{j=1}^k 1/j + 1/2$ ;
some input of EC $(k)$ with $F^* > 0$ has a choosable subcover with $m_{EC}(M) \ge \big(\sum_{j=1}^k 1/j\big) F^*$ .

Milestones (proof of Theorem 6, pp. 271–272)

the measure of the output is $|T| + \mathrm{OV}(F_1)$ ;
if C2 may choose a set with $\mathrm{Ratio}(S') \ge y$ , then $(y+1)\,|\mathrm{UNCOV}| \le F^*$ ;
with $a = F^*/|T|$ and $x = |T - \mathrm{UNCOV}|/|T|$ , the next chosen set has $\mathrm{Ratio}(S') \le a/(1-x) - 1$ ;
on EC $(k)$ , $\mathrm{OV}(F_1) \le |T|\,(a[\ln(k) + 1] - 1)$ ;
the analytic inequality $1 + \ln(k) \le \sum_{j=1}^k 1/j + 1/2$ ;
the lower-bound input (Fig. 1 of the paper with every set of $F_1$ filled out to exactly $k$ points) on which C2 may pay $\sum_{j=1}^k 1/j$ times the optimum.

Significance

The result. The measure $\sum|S|$ penalizes overlap, and the paper notes (without proof, p. 270) that an algorithm returning an optimal cover for the cardinality measure can be a factor $k$ from optimal for this one. Theorem 6 shows that the ratio rule C2 is within $1 + \ln k$ of the least-overlap cover, and the lower bound shows that no analysis of C2 can beat $\sum_{j=1}^k 1/j$ . The two bounds differ by less than $1/2$ for every $k$ . The theorem was an early instance of a logarithmic guarantee for a weighted covering problem, where each set's cost is its size.

Formalizing it. The theorem has been proved since 1974; no machine-checked proof is known to exist. The mission produces a formal model of the EC problem and of C2 as a nondeterministic process, the overlap identity, and the discrete form of the paper's area-under-a-curve estimate. The last is the part the paper argues informally, through a step function and an integral.

Difficulty

The cardinality argument for C1 counts the sets chosen; here the sets have different sizes, so it does not apply. The overlap C2 pays per newly covered point is not bounded by a constant: early choices can be free and late ones cost up to $k-1$ per point, and the bound on the cumulative overlap must hold against the whole run, for every sequence of tie-breaks.

In a formal proof the integral must be replaced by a sum. Covered points arrive in blocks (one block per chosen set), the charge is constant on a block but the bound depends on the covered fraction at the start of the block, and the sum has to be compared with a logarithm. The terms $a\ln a$ and $a/k$ that the paper drops using $1 \le a \le k$ must be controlled as well, and the relation $1 \le a \le k$ must itself be proved from optimality. The lower bound needs an explicit run of C2 through ties on an input with $k \cdot k!$ points, checking at every stage that the intended set is a ratio minimizer.

Formalization scope

Inputs. A family is p : ℕ with S : Fin p → Finset α (0-based, repetitions allowed; a repeated set counts twice in the measure if both copies are chosen, which C2 never does). Subcovers and SUB, LEFT are index sets. $F^*$ is a minimum over the finite, nonempty set of subcovers (Finset.inf'), never a junk value.
Algorithm. C2 is a step relation on states (SUB, LEFT, UNCOV). The choice at Step 3 is existential over all minimizers, so every result quantifies over every choosable output (the paper's WORST). $\mathrm{Ratio}(S)$ is $+\infty$ when $S \cap \mathrm{UNCOV} = \emptyset$ ; the formal rule requires the chosen set to meet UNCOV and compares ratios by cross-multiplication, with no division.
Overlap. The cumulative overlap depends on the run, not on the output alone, so it is carried by an inductive run relation RunOV.
No problem size. The paper's $R[A, P](n)$ maximizes over inputs of size at most $n$ in an unspecified encoding. Upper bounds are stated for every input and every choosable output; the lower bound exhibits one input and one choosable output. Given monotonicity of $R$ in $n$ , these are equivalent to the paper's claims. Ratios are stated multiplicatively, so $F^* = 0$ does not create a vacuous bound.
Numbers. Measures are natural numbers cast to $\mathbb R$ ; $\ln$ is Real.log; $\sum_{j=1}^k 1/j$ is Mathlib's harmonic k.
Ruled out. A deterministic tie-break would prove a weaker upper bound and could not realize the lower-bound run, and a ratio with $x/0 = 0$ would make disjoint-from-UNCOV sets the most attractive choice. The formalization uses neither.

The overlap identity and the discrete integral comparison are reusable for any greedy covering analysis that charges cost per newly covered point. Contributions welcome include proofs of the milestones, the invariants of the C2 run relation (SUB and LEFT partition the indices; UNCOV $= T - \bigcup$ SUB), and the explicit lower-bound run.

Selected references

D. S. Johnson, Approximation algorithms for combinatorial problems, J. Comput. System Sci. 9 (1974), 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
V. Chvátal, A greedy heuristic for the set-covering problem, Math. Oper. Res. 4 (1979), 233–235. https://doi.org/10.1287/moor.4.3.233

10 thms3 active usersReviewed

Completed

Combinatorics Linear algebra Theoretical Computer Science·Captain: mikedeng1

Sparse Approximate Solutions to Linear Systems 2: An Exact Cover by 3-Sets Exists iff Its Incidence System Has a 1/2-Approximate Solution with at Most m/3 NonzerosResearch Paper

Motivation

Many problems in signal processing, statistics and function interpolation ask for a solution of a linear system $Ax\approx b$ that uses as few columns of $A$ as possible: a sparse approximate solution. Natarajan's 1995 paper Sparse Approximate Solutions to Linear Systems (SIAM J. Comput. 24(2):227–234) was motivated by radial basis interpolation, where each column corresponds to a basis function and fewer columns mean a cheaper interpolant. The paper does two things. It proves that finding the sparsest approximate solution is computationally hard (§2, Theorem 1), and it analyses a greedy column-selection algorithm whose number of chosen columns is within a factor, depending on the conditioning of $A$ , of the optimum (§3, Theorem 2; a separate mission of this series).

The hardness theorem is the reason the second half of the paper exists: once exact minimization is ruled out, one settles for approximation guarantees. It is cited throughout the compressed-sensing literature as the canonical statement that $\ell_0$ -minimization under an $\ell_2$ error constraint is NP-hard, and is the starting point for the later theory of when convex relaxations recover sparse solutions.

The argument follows the classical reduction from Exact Cover by 3-sets (X3C) to minimum-weight solutions of linear systems in Garey and Johnson (1979), pp. 221 and 246, adapted to an approximate right-hand side.

Setting

Sparse approximate solution (SAS). Given a matrix $A\in\mathbb R^{m\times n}$ , a vector $b\in\mathbb R^m$ and a tolerance $\varepsilon>0$ , find a vector $x\in\mathbb R^n$ with $\|Ax-b\|_2\le\varepsilon$ whose number of nonzero entries, written $\|x\|_0=|\{j : x_j\neq0\}|$ , is as small as possible. Here $\|\cdot\|_2$ is the Euclidean norm.

Exact Cover by 3-sets (X3C). An instance is a ground set $S=\{s_1,\dots,s_m\}$ and a list $C=c_1,\dots,c_n$ of subsets of $S$ , each with exactly three elements. An exact cover is a sub-collection $\hat C=\{c_j : j\in J\}$ , $J\subseteq\{1,\dots,n\}$ , such that every element of $S$ occurs in exactly one set of $\hat C$ .

The transformation. From an X3C instance build the SAS instance with

the incidence matrix $A\in\mathbb R^{m\times n}$ : $A_{ij}=1$ if $s_i\in c_j$ and $A_{ij}=0$ otherwise, so column $j$ is the characteristic vector of $c_j$ ;
the all-ones vector $b=(1,1,\dots,1)\in\mathbb R^m$ ;
the tolerance $\varepsilon=\tfrac12$ .

In Lean, $S$ is Fin m, the collection is C : Fin n → Finset (Fin m) with hC : ∀ j, (C j).card = 3, an exact cover is an index set J with IsExactCover C J, the matrix is incidence C, the vector $b$ is onesVec m, $Ax$ is Matrix.toEuclideanLin (incidence C) x, and $\|x\|_0$ is nnz x.

Formalization targets

Goal: correctness of the reduction

For every X3C instance $(S,C)$ as above,

\bigl(\exists J,\ \{c_j\}_{j\in J}\text{ is an exact cover of }S\bigr)\iff\bigl(\exists x\in\mathbb R^n,\ \|Ax-b\|_2\le\tfrac12\ \text{and}\ 3\,\|x\|_0\le m\bigr).

This is the sentence the proof of Theorem 1 (p. 228) establishes: "the constructed instance of SAS has a solution with $m/3$ or fewer entries if and only if the given instance of X3C has a solution."

Milestones

Forward direction. If $\{c_j\}_{j\in J}$ is an exact cover, the indicator vector $x=\mathbf 1_J$ satisfies $Ax=b$ and $3\|x\|_0=m$ .
Entry bounds. For every $x$ with $\|Ax-b\|_2\le\frac12$ , each entry of $Ax$ lies in $[\frac12,\frac32]$ .
Lower bound on sparsity. For every such $x$ , $m\le3\|x\|_0$ .
Exact cover from a sparse solution. If moreover $3\|x\|_0\le m$ , the sets $c_j$ with $x_j\neq0$ form an exact cover.

Significance

The result. The equivalence shows that deciding whether a sparse approximate solution with a prescribed number of nonzeros exists is at least as hard as X3C, which is NP-complete. Consequently no polynomial-time algorithm computes the optimum of SAS unless P = NP, and approximation algorithms such as the greedy method of §3 are the natural object of study. The same instance shows hardness persists for 0/1 matrices, a right-hand side of all ones and a constant tolerance, so the difficulty does not come from ill-conditioned data or from vanishing precision.

Formalizing it. The reduction is proved in the paper; this mission produces a machine-checked proof of its correctness, the combinatorial core of every NP-hardness claim for $\ell_0$ -constrained least squares. No prior machine-checked version is known to exist, on the platform or elsewhere. The complexity-theoretic wrapper is out of scope (see below).

Difficulty

The forward direction is a direct computation. The converse contains the only real step, which the paper passes over with "it is clear". From $\|Ax-b\|_2\le\frac12$ one gets only that every entry of $Ax$ is in $[\frac12,\frac32]$ ; the entries of $x$ themselves are arbitrary reals, possibly negative or not equal to $1$ , so $x$ need not be an indicator vector and $Ax=b$ need not hold. The exact-cover property must therefore be extracted from support sizes alone: every element is covered by some column in the support, the support has at most $m/3$ columns of three elements each, and a counting argument forces the chosen sets to be pairwise disjoint. Reading off a cover from the values of $x$ (for instance, taking the $j$ with $x_j=1$ ) does not work.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin m) and EuclideanSpace ℝ (Fin n), so ‖·‖ is the paper's $\|\cdot\|_2$ . Using the sup norm of Fin m → ℝ would give a different statement.
The tolerance is exactly $\varepsilon=\frac12$ , as printed.
The collection is indexed, C : Fin n → Finset (Fin m): repeated sets are allowed and are distinct indices; an exact cover is a set of indices, and on the SAS side one nonzero entry is counted per index, so both sides treat duplicates consistently.
" $m/3$ or fewer" is written $3\|x\|_0\le m$ , never with natural-number division. With this form the equivalence holds for every $m$ (both sides are false when $3\nmid m$ ), which absorbs the paper's "without loss of generality $m$ is a multiple of 3"; no divisibility hypothesis is assumed. For $m=0$ both sides are true.
The hypothesis that every set has exactly three elements is essential for the converse (with $m=9$ , $O=\{s_3,\dots,s_9\}$ , $c_1=\{s_1\}\cup O$ , $c_2=\{s_2\}\cup O$ , $c_3=O$ , the vector $x=(1,1,-1)$ solves $Ax=b$ with $3\|x\|_0=m$ , yet $C$ has no exact cover since $c_1$ and $c_2$ must both be chosen) and is kept as hC.
Not formalized: the infinite-precision RAM machine model, polynomial-time many-one reductions, polynomial-time computability of the transformation (evident: an $m\times n$ 0/1 matrix), and the NP-completeness of X3C (cited by the paper from Garey–Johnson). The goal is therefore the correctness of the transformation, not a statement titled "SAS is NP-hard". A statement that only records the forward direction, or that fixes $x$ to be a 0/1 vector on the SAS side, would trivialize the converse and is not the target.
Tools a solver will need are in Mathlib: coordinate bounds for the Euclidean norm (PiLp.norm_apply_le), Finset.card_biUnion_le, and Finset.card_biUnion for disjoint unions. Contributions of a reusable exact-cover API, or of a polynomial-time reduction framework that could later wrap this equivalence into an NP-hardness theorem, are welcome.

Selected references

B. K. Natarajan, Sparse Approximate Solutions to Linear Systems, SIAM Journal on Computing 24(2):227–234, 1995. https://doi.org/10.1137/s0097539792240406
M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (X3C: problem [SP2], p. 221; minimum weight solution to linear equations: [MP5], p. 246).
F. P. Preparata and M. I. Shamos, Computational Geometry: An Introduction, Springer, 1985 (the real RAM model). https://doi.org/10.1007/978-1-4612-1098-6

6 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Scenario Reduction Algorithms in Stochastic Programming III: The Minimal Reduction Distance of a Regular Ternary Scenario TreeResearch Paper

Motivation

Multistage stochastic programs are solved on a finite scenario tree: a discrete probability distribution whose support points are paths of a random process. Realistic trees have far too many scenarios for the resulting optimization problem, so practitioners reduce the tree, keeping $n$ of its $N$ scenarios and redistributing the probability of the deleted ones. The reduction should keep the reduced distribution as close as possible to the original one in a probability metric that controls the optimal value of the stochastic program (Dupačová, Gröwe-Kuska, Römisch, Math. Program. 95 (2003)).

Choosing the best $n$ scenarios is a set-covering problem and NP-hard, and the algorithms used in practice (backward reduction, fast forward selection) are heuristics without error guarantees. Heitsch and Römisch (2003) therefore derived test instances with an exactly known optimum: regular binary and ternary scenario trees, for which the minimal reduction distance has a closed form once $n$ is not too small. This mission formalizes the ternary case, Proposition 3.2 of that paper. The binary case (Proposition 3.1) is a separate mission of the same series.

Setting

Fix a depth $K \in \mathbb{N}$ and branch widths $\delta^1, \dots, \delta^K \ge 0$ , with $\delta^0 = 0$ . A regular ternary scenario tree has $N = 3^K$ scenarios, one for each index tuple $(i_1, \dots, i_K) \in \{1, 2, 3\}^K$ , where $i_k$ is the successor chosen at level $k$ . Choosing successor $i_k$ adds the increment $\delta^k_{i_k} = (i_k - 2)\,\delta^k \in \{-\delta^k, 0, \delta^k\}$ , and scenario $i$ is the vector $\omega_i = (\omega_i^0, \dots, \omega_i^K) \in \mathbb{R}^{K+1}$ with

\omega_i^k = \sum_{j=0}^{k} \delta^j_{i_j}, \qquad k = 0, \dots, K \quad \text{(eq. (19))}.

All scenarios have probability $p_i = 1/N$ . The distance between scenarios is the maximum norm $c(\omega_i, \omega_j) = \|\omega_i - \omega_j\|_\infty = \max_{0 \le k \le K} |\omega_i^k - \omega_j^k|$ .

Deleting the scenarios of an index set $J$ and moving each deleted scenario's probability to a nearest kept scenario costs the reduction distance

D_J = \sum_{i \in J} p_i \min_{j \notin J} \|\omega_i - \omega_j\|_\infty \quad \text{(eq. (8))},

which by Theorem 2.1 of the paper is the optimal transport-type distance between the original distribution and the best distribution supported on the kept scenarios. The minimal reduction distance to $n$ scenarios is $D^{min}_n = \min\{D_J : \#J = N - n\}$ .

Formalization targets

Goal: Proposition 3.2 (7/9-solution)

Let $K \ge 3$ and let $k_0 \in \arg\min_{1 \le k \le K} \delta^k$ with $k_0 \le K - 2$ and $\max\{\delta^{k_0+1}, \delta^{k_0+2}\} \le 2\delta^{k_0}$ . Then any two distinct scenarios are at distance at least $\delta^{k_0}$ ; there is a set of $\tfrac79 N$ scenarios each paired with a scenario outside it at distance exactly $\delta^{k_0}$ ; and for each $n \in \mathbb{N}$ with $\tfrac29 N \le n < N$ ,

D^{min}_n = \min\{D_J : \#J = N - n\} = \frac{N - n}{N}\,\delta^{k_0} \quad \text{(eq. (21))},

with the minimum attained.

Milestones

Distinct scenarios satisfy $\|\omega_i - \omega_j\|_\infty \ge \delta^{k_0}$ .
Every $J$ with $\#J = N - n$ has $D_J \ge \frac{N-n}{N}\delta^{k_0}$ .
The index set $I_{**}$ of the proof has $\#I_{**} = \tfrac29 N$ , and its complement $J_{**}$ has $\tfrac79 N$ elements.
Every $j \in J_{**}$ has a partner $i \in I_{**}$ with $\|\omega_i - \omega_j\|_\infty = \delta^{k_0}$ .
Example 4.2: for $K = 6$ and $(\delta^1, \dots, \delta^6) = (0.7, 0.9, 1.2, 1.5, 2.6, 3.3)$ , $D^{min}_n = 0.7\,\frac{N-n}{N}$ for $162 \le n < 729$ .

Significance

The result gives an exact optimal value for an NP-hard reduction problem on an infinite family of instances. Heitsch and Römisch use it in their numerical section to measure how far the heuristics' reduced trees are from optimal (Examples 4.1 and 4.2 are the binary and ternary test trees of that study). A closed form of this kind is also the only way to certify that a heuristic is exactly optimal on some instances rather than only competitive with other heuristics.

The proposition is proved in the paper, but the published proof of its central step is one sentence: "Similarly as in Proposition 3.1 it can be shown that there exists an index $i \in I_{**}$ for each $j \in J_{**}$ …". A formal proof supplies that case analysis, which is absent from the literature. The formalization also settles two points the printed statement leaves loose (see Formalization scope): the count of pairs at distance $\delta^{k_0}$ , and the definition of $I_{**}$ when some widths vanish. No machine-checked version of this result or of the reduction distance $D_J$ is known to exist.

Difficulty

The lower bound is routine: two distinct scenarios first differ at some level $l$ , where their coordinates differ by $\delta^l$ or $2\delta^l$ . The substance is attainment: one must exhibit, for every $n \ge \tfrac29 N$ , a kept set of size $n$ whose every deleted scenario lies at distance exactly $\delta^{k_0}$ from some kept one. The obvious candidate, keeping the scenarios that take the middle branch at level $k_0$ , has every other scenario at distance exactly $\delta^{k_0}$ from a kept one, but it keeps $\tfrac13 N$ scenarios and so covers only $n \ge \tfrac13 N$ . Going down to $\tfrac29 N$ kept scenarios forces a deleted scenario and its partner to differ at more than one level, and since coordinates are running sums the differences at levels $k_0+1$ and $k_0+2$ accumulate on top of the one at level $k_0$ . The paper's proof of this step is not written out, and it depends on the widths of the two levels below $k_0$ : the hypothesis $\max\{\delta^{k_0+1}, \delta^{k_0+2}\} \le 2\delta^{k_0}$ is essential, and the result is false without it (for $K = 3$ and $(\delta^1, \delta^2, \delta^3) = (1, 3, 3)$ one has $D^{min}_6 = 31/27$ , not $7/9$ ).

Formalization scope

A scenario is an index tuple $\sigma : \mathrm{Fin}\,K \to \mathrm{Fin}\,3$ ; $\sigma(r)$ is the successor at paper level $r + 1$ , with $\mathrm{Fin}\,3$ values $0, 1, 2$ standing for the paper's $i = 1, 2, 3$ . The widths are $\delta : \mathbb{N} \to \mathbb{R}$ , of which only $\delta(1), \dots, \delta(K)$ are used; the standing assumption $\delta^k \in \mathbb{R}_+$ (p. 196) is the hypothesis $\delta(k) \ge 0$ for $1 \le k \le K$ . Scenarios live in $\mathrm{Fin}(K+1) \to \mathbb{R}$ , whose Mathlib norm is the maximum norm. Probabilities are uniform, $1/3^K$ .
$D_J$ is defined for a general finite index set, probabilities and cost, with the inner minimum a Finset.inf' over the complement of $J$ ; the complement must be nonempty, so no default value arises. $D^{min}_n$ is stated as IsLeast of the set of all values $D_J$ with $\#J = N - n$ : the goal asserts both the lower bound for every $J$ and attainment by some $J$ . A formalization that exhibits a single $J$ with $D_J = \frac{N-n}{N}\delta^{k_0}$ , or states an infimum without attainment, or drops any hypothesis on $k_0$ , is a different (and in the last case false) statement.
$\tfrac29 N \le n$ is written $2 \cdot 3^K \le 9n$ , and $\tfrac79 N$ as $7 \cdot 3^{K-2}$ .
Pairs. As printed, "there are $\tfrac79 N$ distinct pairs of scenarios such that the distance between the members of each pair is exactly $\delta^{k_0}$ " is false as an exact count (for $K = 3$ and $\delta = (1,1,1)$ there are 130 such pairs, not 21). The goal states what the proof constructs: a set $J_{**}$ of $\tfrac79 N$ scenarios, each paired with a scenario outside $J_{**}$ at distance exactly $\delta^{k_0}$ .
$I_{**}$ . The paper defines $I_{**}$ by testing whether the increments $\delta^k_{i_k}$ vanish. When one of $\delta^{k_0}, \delta^{k_0+1}, \delta^{k_0+2}$ is $0$ this no longer identifies the middle branch and the count $\tfrac29 N$ fails, although the proposition remains true. The formalization defines $I_{**}$ by branch indices (middle branch versus outer branches), which agrees with the paper whenever these three widths are positive. No positivity hypothesis is added to the goal.
Welcome contributions: a reusable library for regular scenario trees (first differing level, distance of paths), and the case analysis of milestone 4. The binary mission of this series needs the same lower-bound argument with the constant $2\delta^{k_0}$ .

Selected references

H. Heitsch, W. Römisch, Scenario Reduction Algorithms in Stochastic Programming, Computational Optimization and Applications 24 (2003), 187–206. https://doi.org/10.1023/A:1021805924152
J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: An approach using probability metrics, Mathematical Programming 95 (2003), 493–511. https://doi.org/10.1007/s10107-002-0331-0

9 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Scenario Reduction Algorithms in Stochastic Programming II: The Minimal Reduction Distance of a Regular Binary Scenario TreeResearch Paper

Why exact reduction distances matter

Multistage stochastic programs are solved on a finite scenario tree, a discrete probability measure whose atoms are paths of a stochastic process. The size of the deterministic equivalent grows with the number of scenarios, so practitioners replace the original measure $P=\sum_{i=1}^N p_i\delta_{\omega_i}$ by a measure supported on $n<N$ of its scenarios. Stability theory for stochastic programs (Dupačová, Gröwe-Kuska and Römisch, Math. Program. 95 (2003), doi:10.1007/s10107-002-0331-0) bounds the change of the optimal value by a probability metric between the two measures, which leads to the optimal scenario reduction problem: choose which $N-n$ scenarios to delete so that this distance is smallest.

That problem is a set-covering problem and is NP-hard, and the algorithms that Heitsch and Römisch study in the same paper (backward reduction, fast forward selection) are heuristics without error guarantees. To test them one needs original measures whose optimal reduction distance is known exactly. Section 3 of Heitsch and Römisch, Scenario Reduction Algorithms in Stochastic Programming, Comput. Optim. Appl. 24 (2003) (doi:10.1023/A:1021805924152) supplies such instances: regular binary and ternary scenario trees, for which the minimal distance to any reduced tree with at least a fixed fraction of the scenarios is an explicit formula. This mission formalizes the binary case, Proposition 3.1.

Setting

Fix a horizon $K\in\mathbb N$ and level parameters $\delta^1,\dots,\delta^K\ge0$ , with $\delta^0=0$ . A regular binary scenario tree has $N=2^K$ scenarios. A scenario is determined by a branch $i_k\in\{1,2\}$ at every level $k=1,\dots,K$ , and is the vector $\omega_i=(\omega_i^0,\dots,\omega_i^K)\in\mathbb R^{K+1}$ with

\omega_i^k=\sum_{j=0}^k\delta^j_{i_j},\qquad \delta^j_{i_j}=(2i_j-3)\,\delta^j\in\{-\delta^j,+\delta^j\}.\tag{19}

All scenarios start at the root $\omega_i^0=0$ and carry probability $p_i=1/N$ . Scenarios are compared in the maximum norm $\|\omega-\tilde\omega\|_\infty=\max_{k=0,\dots,K}|\omega^k-\tilde\omega^k|$ .

Deleting the scenarios with indices in $J\subset\{1,\dots,N\}$ and moving each deleted scenario's probability to a nearest kept scenario costs the reduction cost

D_J=\sum_{i\in J}p_i\min_{j\notin J}\|\omega_i-\omega_j\|_\infty,\tag{8}

which by Theorem 2.1 of the paper is the minimal Kantorovich-type distance between $P$ and a measure supported on the kept scenarios. The minimal reduction distance for $n$ kept scenarios is $D^{min}_n=\min\{D_J:\#J=N-n\}$ .

In the Lean development, scenarios are indexed by σ : Fin K → Fin 2 (Fin-index $r$ is tree level $r+1$ , value $0$ is the branch $-\delta$ , value $1$ is $+\delta$ ), lev σ k is the branch at level $k$ , scenario δ σ : Fin (K+1) → ℝ is $\omega_\sigma$ , and redCost δ J hJ is $D_J$ .

Formalization targets

Goal: Proposition 3.1 (3/4-solution)

Let $K\ge3$ , $k_0\in\arg\min_{1\le k\le K}\delta^k$ , $k_0\le K-2$ and $\max\{\delta^{k_0+1},\delta^{k_0+2}\}\le2\delta^{k_0}$ . Then any two distinct scenarios are at distance at least $2\delta^{k_0}$ ; there is a set $J_*$ of $\frac34N$ scenarios each of which has a partner outside $J_*$ at distance exactly $2\delta^{k_0}$ ; and for every $n\in\mathbb N$ with $\frac N4\le n<N$

D^{min}_n=\min\{D_J:\#J=N-n\}=\frac{N-n}{N}\,2\delta^{k_0}.\tag{20}

Milestones

Two scenarios that first differ at level $l$ are at distance $\ge2\delta^l\ge2\delta^{k_0}$ .
$D_J\ge\frac{N-n}{N}2\delta^{k_0}$ for every $J$ with $\#J=N-n$ .
The index set $I_*$ (branch at $k_0$ opposite to the common branch at $k_0+1,k_0+2$ ) has $\#I_*=N/4$ , so $\#J_*=\frac34N$ .
Every $j\in J_*$ has a partner $i\in I_*$ with $\|\omega_i-\omega_j\|_\infty=2\delta^{k_0}$ .
Example 4.1: for $K=10$ and the paper's parameters, Proposition 3.1 applies with $k_0=1$ and $D^{min}_n=\frac{N-n}{N}$ for $256\le n<1024$ .

Significance

The result. Proposition 3.1 gives the exact optimum of an NP-hard combinatorial problem on an explicit, parametrized family of instances of every size $N=2^K$ . Section 4 of the paper uses it (Example 4.1, $N=1024$ ) as ground truth for the relative accuracy of backward reduction and fast forward selection. Without it, the quality of a heuristic reduction on a large tree could only be compared with other heuristics or with lower bounds.

The formalization. The proposition is proved in the paper; to our knowledge no machine-checked version exists. A formal proof certifies the benchmark values, and the statement also corrects the printed text in two places. First, "there are $\frac34N$ distinct pairs … at distance exactly $2\delta^{k_0}$ " is false as an exact count (for $K=3$ , $\delta=(1,1,1)$ there are twenty such pairs, not six), so the goal states "at least", in the form the proof exhibits. Second, the paper's sign-based definition of $I_*$ degenerates when some $\delta^k=0$ , although the proposition still holds; the mission defines $I_*$ by branch indices.

Difficulty

The lower bound is a direct computation. The content is the matching upper bound: a set $J$ of the prescribed size for which every deleted scenario has a kept scenario at the minimal possible distance. A natural first attempt pairs scenarios that differ only at level $k_0$ . That handles only half of the scenarios with a single partner each, and it cannot reach $\frac34N$ deleted scenarios. Once scenarios differ at more than one level, their maximum-norm distance is a maximum of several partial sums, and keeping all of them at most $2\delta^{k_0}$ is exactly where the hypothesis $\max\{\delta^{k_0+1},\delta^{k_0+2}\}\le2\delta^{k_0}$ enters. Without it, eq. (20) fails: for $K=3$ , $\delta=(1,3,3)$ and $n=2$ the true minimum is $\frac52$ , not $\frac32$ . The passage from $n=N/4$ to general $n\ge N/4$ also needs care: the deleted set must shrink while each remaining deleted scenario keeps its partner among the kept ones.

Formalization scope

The index type is Fin K → Fin 2, which has exactly $2^K$ elements. The paper's $(K+1)$ -tuple has a level-0 entry with no choice, so it is dropped, and the vector $\omega$ keeps its $K+1$ coordinates with $\omega^0=0$ .
The parameters are δ : ℕ → ℝ, with $\delta^k\ge0$ and the arg min stated for $k=1,\dots,K$ only. $\delta^k>0$ is not assumed, because the paper allows $\delta^k\in\mathbb R_+$ and the proposition holds with zeros.
The cost is Mathlib's norm on Fin (K+1) → ℝ, which is the maximum norm, and $p_i=1/2^K$ is written out.
$D_J$ requires a nonempty set of kept scenarios, and its inner minimum is a finite Finset.inf'.
$D^{min}_n$ is stated with IsLeast over the set of attained values $D_J$ , $\#J=N-n$ , so both the lower bound and attainment are part of the goal. A proof of $D_{J}\le\frac{N-n}{N}2\delta^{k_0}$ for a single exhibited $J$ , or a real infimum without attainment, does not prove the goal.
" $\frac N4\le n$ " is written $2^K\le4n$ , and $\frac34N$ is $3\cdot2^{K-2}$ .
The pairs claim is "at least $\frac34N$ pairs", expressed as a set $J_*$ of that size with a partner outside $J_*$ for every member.
All hypotheses on $k_0$ appear in the goal; dropping any of them makes (20) false.

Useful infrastructure: sup-norm lemmas for Fin n → ℝ (pi_norm_le_iff_of_nonneg, norm_le_pi_norm), Finset.inf' lemmas, and counting functions Fin K → Fin 2 with prescribed values (Fintype.card_fun, Fintype.card_pi). The tree and reduction-cost definitions are shared in spirit with the ternary-tree mission of this series (Proposition 3.2), and a proof whose structure transfers to $d=3$ is welcome. Contributions of proofs of the milestones individually, in any order, are welcome.

Selected references

H. Heitsch, W. Römisch, Scenario Reduction Algorithms in Stochastic Programming, Computational Optimization and Applications 24 (2003), 187–206. doi:10.1023/A:1021805924152
J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: An approach using probability metrics, Mathematical Programming 95 (2003), 493–511. doi:10.1007/s10107-002-0331-0

9 thms3 active usersReviewed

Completed

Operations Research Optimal Transport Optimization·Captain: mikedeng1

Scenario Reduction Algorithms in Stochastic Programming I: Fast Forward Selection Realizes the Forward Selection PrincipleResearch Paper

Why reduce scenarios

Multistage and two-stage stochastic programs are solved numerically on a discrete probability distribution: a finite set of scenarios $\omega_1,\dots,\omega_N$ with probabilities $p_1,\dots,p_N$ . The size of the resulting optimization problem grows with $N$ , and scenario sets produced by sampling or by historical data are often far too large to be solved directly. Scenario reduction replaces the original distribution by one supported on a small subset of the scenarios, chosen so that the optimal value and solutions of the stochastic program change as little as possible.

Stability theory for stochastic programs (Rachev and Römisch, 2002) shows that this change is controlled by a probability distance of Fortet–Mourier type, which for discrete measures is bounded by the value of a transportation problem. Dupačová, Gröwe-Kuska and Römisch (2003) turned this into a combinatorial problem and proposed greedy backward and forward heuristics. Heitsch and Römisch (2003) gave faster versions of both heuristics; the forward version, fast forward selection, is the subject of this mission. Implementations of these reduction heuristics are distributed with the GAMS modelling system (SCENRED) and are used in energy and finance applications of stochastic programming.

Setting

Let $E$ be a finite-dimensional real vector space with a norm $\|\cdot\|$ , let $\omega_0\in E$ , and let $h:[0,\infty)\to[0,\infty)$ be continuous and nondecreasing with $h(0)=0$ . The cost between two points of $E$ is

c(\omega,\tilde\omega)=\max\bigl\{1,\,h(\|\omega-\omega_0\|),\,h(\|\tilde\omega-\omega_0\|)\bigr\}\,\|\omega-\tilde\omega\| .

It is nonnegative, symmetric, and zero on the diagonal.

The original distribution is $P=\sum_{i=1}^N p_i\delta_{\omega_i}$ with $p_i>0$ and $\sum_i p_i=1$ . Deleting the scenarios in a set $J\subset\{1,\dots,N\}$ and assigning new weights $q_j\ge 0$ , $\sum_{j\notin J}q_j=1$ , to the kept ones gives $Q=\sum_{j\notin J}q_j\delta_{\omega_j}$ . The distance $D(J;q)$ between $P$ and $Q$ is the optimal value of the transportation problem

D(J;q)=\min\Bigl\{\sum_{i=1}^N\sum_{j\notin J}c(\omega_i,\omega_j)\eta_{ij}:\ \eta_{ij}\ge 0,\ \sum_{i}\eta_{ij}=q_j,\ \sum_{j\notin J}\eta_{ij}=p_i\Bigr\}.

The reduction cost of deleting $J$ is

D_J=\sum_{i\in J}p_i\min_{j\notin J}c(\omega_i,\omega_j),

and the optimal reduction problem (8) minimizes $D_J$ over all $J$ with $\#J=N-n$ , where $n$ is the number of scenarios to keep.

Forward selection builds the kept set greedily. With $J^{[0]}=\{1,\dots,N\}$ and $J^{[i]}=\{1,\dots,N\}\setminus\{u_1,\dots,u_i\}$ , it chooses

u_i\in\arg\min_{u\in J^{[i-1]}}D_{J^{[i-1]}\setminus\{u\}},\qquad i=1,\dots,n. \tag{16}

Fast forward selection (Algorithm 2.4) computes the same choices through an updated cost matrix: $c^{[1]}_{ku}=c(\omega_k,\omega_u)$ , $c^{[i]}_{ku}=\min\{c^{[i-1]}_{ku},c^{[i-1]}_{ku_{i-1}}\}$ , $z^{[i]}_u=\sum_{k\in J^{[i-1]}\setminus\{u\}}p_kc^{[i]}_{ku}$ , and $u_i\in\arg\min_{u\in J^{[i-1]}}z^{[i]}_u$ .

Formalization targets

Goal: Theorem 2.5

For $1\le n\le N$ and every run $u_1,\dots,u_n$ of Algorithm 2.4, with any tie-breaking in the arg min,

u_i\ \text{satisfies (16)}\quad\text{and}\quad z^{[i]}_{u_i}=D_{J^{[i]}}\qquad(i=1,\dots,n).

Milestones

Theorem 2.1 (redistribution). For $J$ with at least one kept scenario, $D_J=\min_q D(J;q)$ , and the minimum is attained at $\bar q_j=p_j+\sum_{i\in J,\,j(i)=j}p_i$ for every choice of nearest kept scenarios $j(i)$ .
Eq. (10). $D_{\{1,\dots,N\}\setminus\{u\}}=\sum_{i=1}^Np_ic(\omega_i,\omega_u)$ , so (8) with $\#J=N-1$ is problem (10).
Eq. (12). The sum $lb$ of the $N-n$ smallest single-deletion costs $p_l\min_{j\neq l}c(\omega_l,\omega_j)$ , taken in the greedy order (11), is at most $D_J$ for every $J$ with $\#J=N-n$ .
Optimality condition (p. 191). If each $l_i$ has a nearest other scenario outside $\{l_1,\dots,l_{N-n}\}\setminus\{l_i\}$ , then $\{l_1,\dots,l_{N-n}\}$ solves (8).
Eq. (17), unrolled recursion. For any index sequence, $c^{[i]}_{ku}=\min_{j\notin J^{[i-1]}\setminus\{u\}}c(\omega_k,\omega_j)$ for $u\in J^{[i-1]}$ .
Eq. (17), conclusion. For any index sequence, $z^{[i]}_u=D_{J^{[i-1]}\setminus\{u\}}$ for $u\in J^{[i-1]}$ .

Significance

Theorem 2.5 certifies that the cheap update of Algorithm 2.4 (one pairwise minimum per matrix entry and step) produces exactly the greedy forward selection defined through the reduction costs, and that the running objective $z^{[i]}_{u_i}$ is the reduction cost of the scenarios deleted so far. Combined with Theorem 2.1, $z^{[i]}_{u_i}$ is the optimal transportation distance between $P$ and the best measure on the kept scenarios, which is the quantity practitioners monitor to decide how many scenarios to keep. The lower bound (12) and the optimality condition give a posteriori quality certificates for any reduced set.

All results of this mission are proved in the paper or in the works it cites (Dupačová et al., 2003); none is open. To the best of a platform search, none has been machine-checked. The mission provides a verified specification of a widely deployed algorithm, a formal link between a combinatorial set-covering objective and a finite transportation problem, and definitions (reduction cost, transportation plans with a partially free target marginal, greedy runs with arbitrary tie-breaking) reusable by the regular-tree missions of this series and by later scenario-tree construction papers.

Difficulty

The mathematics is elementary; the difficulty is bookkeeping. The recursion for $c^{[i]}$ refers to the previous step's column $u_{i-1}$ , which itself was updated, so unrolling it to a minimum over $\{u,u_1,\dots,u_{i-1}\}$ is an induction on $i$ in which the index sets $J^{[i]}$ , the 1-based step counter and the complement structure all move together. The natural first attempt, identifying $c^{[i]}_{ku}$ with the minimum over the complement of $J^{[i]}$ , is off by one step: the correct set is the complement of $J^{[i-1]}\setminus\{u\}$ , which contains $u$ itself. For Theorem 2.1 the lower bound requires using that $c(\omega_i,\omega_i)=0$ for kept scenarios and that every plan ships all of $p_i$ somewhere outside $J$ ; the attainment part requires constructing the plan explicitly from the choice $j(\cdot)$ , including scenarios for which several kept scenarios are equally near.

Formalization scope

Scenarios are ω : Fin N → E with E a finite-dimensional real normed space; the paper's closed set $\Omega\subset\mathbb R^s$ plays no role beyond containing the scenarios and is omitted. Scenarios need not be distinct.
$h$ is a function ℝ → ℝ with the paper's assumptions imposed on $[0,\infty)$ (IsGrowthFunction); every theorem carries them, together with $p_i>0$ and $\sum_ip_i=1$ .
The functions $f_0$ , $g$ and the stochastic program (1)–(2) that motivate $c$ appear in no statement.
$D(J;q)$ is the paper's finite transportation problem (p. 188), not the Kantorovich functional on measures. Weights $q$ and plans $\eta$ are indexed by all of $\{1,\dots,N\}$ with entries at deleted indices fixed to $0$ .
$D_J$ requires a proof that the complement of $J$ is nonempty; minima are Finset.inf', never a real infimum with a default value.
Algorithm 2.4 is a relation on sequences u : ℕ → Fin N with 1-based steps. $c^{[i]}$ is the printed recursion, extended to all indices; runs are any sequences satisfying the arg-min conditions, so every tie-breaking rule is covered.
The paper's standing restriction $n<N$ is relaxed to $n\le N$ in Theorem 2.5; the statement remains true at $n=N$ .
A trivializing formalization is ruled out: defining $c^{[i]}$ or $z^{[i]}$ directly as the minimum over the selected set or as $D_{J^{[i-1]}\setminus\{u\}}$ would make Theorem 2.5 hold by definition, and proving it for one fixed tie-breaking rule would prove less than the paper; neither is done.
Proofs of the milestones, alternative proofs of Theorem 2.1 via LP duality, and a verified executable implementation of Algorithm 2.4 are all welcome.

Selected references

H. Heitsch, W. Römisch, Scenario Reduction Algorithms in Stochastic Programming, Computational Optimization and Applications 24 (2003), 187–206. https://doi.org/10.1023/A:1021805924152
J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: an approach using probability metrics, Mathematical Programming 95 (2003), 493–511. https://doi.org/10.1007/s10107-002-0331-0
S. T. Rachev, W. Römisch, Quantitative stability in stochastic programming: the method of probability metrics, Mathematics of Operations Research 27 (2002), 792–818. https://doi.org/10.1287/moor.27.4.792.304

12 thms3 active usersReviewed

Completed

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

Golden Ratio Algorithms for Variational Inequalities I: The Golden Ratio Algorithm with a Fixed Step Converges to a Solution of a Monotone Variational InequalityResearch Paper

Motivation

A monotone variational inequality asks for a point at which a monotone operator and a convex function are in equilibrium. It unifies convex minimization (where $F$ is a gradient), convex–concave saddle-point problems (where $F$ is the skew gradient of a Lagrangian), Nash equilibria of monotone games, and complementarity problems in economics and traffic assignment. In operations research, first-order methods for such problems are the workhorse behind large-scale saddle-point formulations of linear and conic programs, where only one operator evaluation and one projection or proximal step per iteration are affordable.

The classical method for Lipschitz monotone operators is Korpelevich's extragradient method (1976) and its proximal variant, Tseng's forward–backward–forward method (2000); both need two evaluations of $F$ per iteration. The reflected projected gradient method of Malitsky (SIAM J. Optim., 2015) uses one evaluation of $F$ but evaluates it at $2z^k-z^{k-1}$ , a point that may lie outside the domain of $g$ . Malitsky's Golden Ratio Algorithm (GRAAL), introduced in Golden Ratio Algorithms for Variational Inequalities (preprint 2018; published in Mathematical Programming, doi:10.1007/s10107-019-01416-w), uses one evaluation of $F$ , always at a feasible point, and one proximal step per iteration. Its fixed-step version, Theorem 1 of that paper, is the subject of this mission; the explicit, adaptive-step version (Theorem 2) is a separate mission of this series.

Setting

Let $\mathcal E$ be a finite-dimensional real inner product space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\| = \sqrt{\langle\cdot,\cdot\rangle}$ . Let $g:\mathcal E\to(-\infty,+\infty]$ and write $\operatorname{dom} g = \{x : g(x)<+\infty\}$ . Let $F:\operatorname{dom} g\to\mathcal E$ . The variational inequality is

\text{find } z^*\in\mathcal E \quad\text{such that}\quad \langle F(z^*), z-z^*\rangle + g(z)-g(z^*)\ \ge\ 0\qquad \forall z\in\mathcal E. \tag{1}

The standing assumptions are:

(C1) the solution set $S$ of (1) is nonempty;
(C2) $g$ is proper (never $-\infty$ , finite somewhere), convex, and lower semicontinuous;
(C3) $F$ is monotone: $\langle F(u)-F(v),u-v\rangle\ge0$ for all $u,v\in\operatorname{dom} g$ .

The proximal operator of $g$ is $\operatorname{prox}_g(z) = \operatorname{argmin}_x\{g(x)+\tfrac12\|x-z\|^2\}$ . Let $\varphi = \frac{\sqrt5+1}{2}$ be the golden ratio, so that $\varphi^2 = 1+\varphi$ . For a step $\lambda>0$ and arbitrary starting points $z^1,\bar z^0\in\mathcal E$ , the Golden Ratio Algorithm generates, for $k\ge1$ ,

\bar z^k = \frac{(\varphi-1)z^k + \bar z^{k-1}}{\varphi},\qquad z^{k+1} = \operatorname{prox}_{\lambda g}\big(\bar z^k - \lambda F(z^k)\big). \tag{6}

The first line is a convex combination of the newest iterate and the previous average; the second is a forward–backward step taken from the average rather than from $z^k$ .

Formalization targets

Goal: Theorem 1

If $F$ is $L$ -Lipschitz on $\operatorname{dom} g$ ( $L>0$ ), (C1)–(C3) hold, and $\lambda\in\big(0,\frac{\varphi}{2L}\big]$ , then there is $z^*\in S$ with

z^k\to z^*\qquad\text{and}\qquad \bar z^k\to z^*\qquad(k\to\infty).

Both sequences converge, to one and the same solution. The goal is stated with the paper's exact step range; no rate is claimed, as the paper claims none.

Milestones

Eq. (4), the prox-inequality: for proper convex lsc $g$ ,

\bar x = \operatorname{prox}_g z \iff \langle\bar x - z, x-\bar x\rangle\ge g(\bar x)-g(x)\quad\forall x\in\mathcal E.

Eq. (12), an identity using only the averaging step of (6): for every point $z^*$ ,

\|z^{k+1}-z^*\|^2 = (1+\varphi)\|\bar z^{k+1}-z^*\|^2-\varphi\|\bar z^k-z^*\|^2+\tfrac1\varphi\|z^{k+1}-\bar z^k\|^2 .

Eq. (14), the energy inequality: for $z^*\in S$ and $k\ge2$ ,

(1+\varphi)\|\bar z^{k+1}-z^*\|^2+\tfrac\varphi2\|z^{k+1}-z^k\|^2\le(1+\varphi)\|\bar z^k-z^*\|^2+\tfrac\varphi2\|z^k-z^{k-1}\|^2-\varphi\|z^k-\bar z^k\|^2 .

Lemma 1 (Bauschke–Combettes, Theorem 5.5): a sequence that is Fejér monotone with respect to a nonempty set $C$ and whose cluster points all lie in $C$ converges to a point of $C$ .

Significance

The result. Theorem 1 shows that monotone variational inequalities with a Lipschitz operator can be solved with one operator evaluation and one proximal step per iteration, with $F$ evaluated only at points of $\operatorname{dom} g$ , where it is defined. This matters when $F$ is expensive (a large matrix–vector product, a simulation) or undefined outside the feasible set (for instance an operator involving $\log x$ on the positive orthant). The analysis also explains the constant: the averaging weight $\varphi$ is the largest $c$ with $1/c\ge c-1$ , and the step bound $\varphi/(2L)$ follows from it. The fixed-step analysis is the template for the explicit, adaptive-step EGRAAL of the same paper (Theorem 2), which needs only local Lipschitz continuity of $F$ .

The formalization. The theorem has a published proof, and no machine-checked version of it or of GRAAL is known. Mathlib contains the golden ratio, Lipschitz conditions, lower semicontinuity and cluster points, but no proximal operator of an extended-valued function, no prox-inequality and no Fejér-monotonicity convergence lemma. This mission produces those pieces and a complete convergence proof for a first-order VI method, which are reusable for projected gradient, forward–backward, extragradient and reflected-gradient analyses.

Difficulty

The naive approach, to show that $\|z^k-z^*\|$ decreases, fails: GRAAL is not Fejér monotone in $z^k$ , because the forward step is taken from the average $\bar z^k$ and uses $F(z^k)$ rather than $F$ at the new point. The quantity that decreases is an energy mixing $\|\bar z^k-z^*\|^2$ with the successive difference $\|z^k-z^{k-1}\|^2$ , and both the averaging identity and the Lipschitz estimate must produce matching coefficients for the cross terms to cancel. The energy inequality alone gives only boundedness and vanishing successive differences; convergence of the whole sequence, and the fact that the limit solves (1) when $g$ is merely lower semicontinuous and extended-valued, is a separate step. On the formal side, $g$ takes the value $+\infty$ , so the prox-inequality and the variational inequality must be handled in extended arithmetic without letting $\infty-\infty$ decide anything.

Formalization scope

$\mathcal E$ is a type E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E].
$g$ is E → EReal. (C2) is IsProperConvexLSC g: never $\bot$ , somewhere finite, convex epigraph $\{(x,t)\in E\times\mathbb R: g(x)\le t\}$ , and LowerSemicontinuous g on all of E. $\operatorname{dom} g$ is effDom g = {x | g x ≠ ⊤}.
$F$ is a total function E → E; monotonicity and the Lipschitz bound $\|F(u)-F(v)\|\le L\|u-v\|$ are required on effDom g only. The step range is 0 < λ, λ ≤ φ / (2 * L) with 0 < L and φ = Real.goldenRatio.
$S$ is solutionSet g F: points of effDom g satisfying (1) for every $z\in E$ , evaluated in EReal.
The proximal step is the argmin predicate IsProxPoint (fun x => λ * g x) w z⁺, not a choice function, so no junk value is involved. A run of (6) is IsGRAALRun g F λ z zbar on sequences ℕ → E indexed as in the paper: $z^1$ and $\bar z^0$ are free and the entry $z^0$ is unused.
The conclusion is ∃ zs ∈ solutionSet g F, Tendsto z atTop (𝓝 zs) ∧ Tendsto zbar atTop (𝓝 zs).

The hypotheses of the goal are jointly satisfiable, so the theorem is not vacuous: for $g\equiv0$ and $F\equiv0$ every point is a solution and constant sequences form a run of (6); a formalization under which IsGRAALRun has no instances, or in which $S$ may be empty, is ruled out. Two hypotheses are added to printed statements and flagged in their notes: $C\neq\emptyset$ in Lemma 1, which is false without it, and $z^1\in\operatorname{dom} g$ in Eq. (14), needed at $k=2$ because the paper's $F$ is only defined on $\operatorname{dom} g$ .

Welcome contributions: existence and uniqueness of the proximal point of a proper convex lsc function in finite dimensions; the prox-inequality; Fejér-monotonicity lemmas; the energy inequality; and the final convergence argument. The prox and Fejér infrastructure is independent of the golden ratio and is shared with the second mission of this series.

Selected references

Y. Malitsky, Golden Ratio Algorithms for Variational Inequalities, preprint, Optimization Online 6598, 2018. https://optimization-online.org/wp-content/uploads/2018/05/6598.pdf ; published in Mathematical Programming. https://doi.org/10.1007/s10107-019-01416-w
H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011 (2nd ed. 2017). https://doi.org/10.1007/978-3-319-48311-5
G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12 (1976) 747–756.
P. Tseng, A modified forward–backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38 (2000) 431–446. https://doi.org/10.1137/S0363012998338806
Y. Malitsky, Projected reflected gradient methods for monotone variational inequalities, SIAM J. Optim. 25 (2015) 502–520. https://doi.org/10.1137/14097238X

8 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Number Theory+1·Captain: mikedeng1

Fast Algorithms for Finding Nearest Common Ancestors II: Nearest Common Ancestors in a Complete Binary Tree by Symmetric-Order ArithmeticResearch Paper

Motivation

The nearest common ancestor (nca) problem asks, for a fixed rooted tree and a sequence of vertex pairs $(v, w)$ , for the deepest vertex that is an ancestor of both. It is a basic step in suffix-tree string algorithms and is equivalent to range-minimum queries (Bender, Farach-Colton, 2000). Harel and Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13 (1984) 338–355, gave the first algorithm answering each query on a static tree in constant time on a random-access machine after linear preprocessing.

Their construction reduces the general problem to the case of a complete binary tree, where §3 of the paper shows that nca queries can be answered "by direct calculation" on vertex numbers: multiplication, division, powers of two, the base-two logarithm and bitwise exclusive or. The later simplification of Schieber and Vishkin (1988) is built on the same in-order numbering of a complete binary tree. This mission formalizes that arithmetic core.

Timeline, as reviewed in the paper's §1 (pp. 338–340):

1976: Aho, Hopcroft and Ullman (SIAM J. Comput. 5) give an $O(n + m\alpha(m+n, n))$ -time off-line algorithm on a pointer machine, and for static trees a random-access algorithm with $O(n \log\log n)$ preprocessing and $O(\log\log n)$ time per query.
1976: van Leeuwen (unpublished report) gives an $O(n + m \log\log n)$ -time algorithm for linking roots and static trees that runs on a pointer machine in $O(n)$ space.
1980: Harel (Proc. 21st FOCS) gives a preliminary version of the paper's results.
1984: Harel and Tarjan prove that pointer machines need $\Omega(\log\log n)$ time per query on static trees (Theorem 1), and give the $O(n)$ -preprocessing, $O(1)$ -query random-access algorithm whose base case is the subject of this mission.

Setting

Fix $d \ge 0$ and let $T$ be the complete binary tree of depth $d$ . A vertex is identified with the path from the root to it, a word of at most $d$ left or right turns; the root is the empty word and $T$ has $n = 2^{d+1} - 1$ vertices. Following the paper's Appendix (pp. 354–355):

$w$ is an ancestor of $v$ ( $v$ a descendant of $w$ ) if the word $w$ is a prefix of the word $v$ ; every vertex is its own ancestor. $v$ and $w$ are unrelated if neither is an ancestor of the other.
The depth of $v$ is its distance to the root; its height $h(v)$ is the length of the longest path from a leaf to $v$ , which in $T$ is $d - \operatorname{depth}(v)$ .
$\operatorname{nca}(v, w)$ is the vertex of greatest depth that is an ancestor of both: the longest common prefix.

The vertices of $T$ are numbered from $1$ to $n$ in symmetric order (in-order): at every vertex, first the left subtree, then the vertex, then the right subtree. $\mathrm{sym}(v)$ is the number of $v$ and $\mathrm{sym}^{-1}(i)$ the vertex numbered $i$ . For $d = 4$ (Fig. 1 of the paper) the root is $16$ , its children $8$ and $24$ , and the leaves $1, 3, 5, \dots, 31$ . $i \oplus j$ denotes bitwise exclusive or and $\lg$ the base-two logarithm.

Two procedures of §3 use only numbers, heights and $d$ :

the nca depth algorithm: return $d - h(v)$ if $\mathrm{sym}(w) \in [\mathrm{sym}(v) - 2^{h(v)} + 1, \mathrm{sym}(v) + 2^{h(v)} - 1]$ ; else $d - h(w)$ if the same holds with $v, w$ exchanged; else $d - \lfloor \lg(\mathrm{sym}(v) \oplus \mathrm{sym}(w)) \rfloor$ ;
the depth algorithm: given $v$ and a depth $d_2 \le \operatorname{depth}(v)$ , with $h = d - d_2$ , return $\mathrm{sym}^{-1}\bigl(2^{h+1}\lfloor \mathrm{sym}(v)/2^{h+1}\rfloor + 2^h\bigr)$ .

Formalization targets

Goal: the nca algorithm is correct

The algorithm to compute $\operatorname{nca}(v,w)$ (p. 342) runs the nca depth algorithm to obtain $d_0$ and then the depth algorithm on $(v, d_0)$ . The goal states that it returns the nearest common ancestor: for all vertices $v, w$ of $T$ , with $d_0$ the output of the nca depth algorithm and $h = d - d_0$ ,

\mathrm{sym}(\operatorname{nca}(v,w)) = 2^{h+1}\left\lfloor \frac{\mathrm{sym}(v)}{2^{h+1}} \right\rfloor + 2^h .

Milestones

In the order the paper uses them:

Numbers at height $h$ (p. 341): the vertices of height $h$ are numbered $2^h, 3\cdot 2^h, 5\cdot 2^h, \dots$ from left to right.
Lemma 1: $h(v)$ is the largest $h$ with $2^h \mid \mathrm{sym}(v)$ .
Lemma 2: the descendants of $v$ are the vertices numbered in $[\mathrm{sym}(v) - 2^{h(v)} + 1, \mathrm{sym}(v) + 2^{h(v)} - 1]$ .
Lemma 3: for a height $h \ge h(v)$ , the height- $h$ ancestor of $v$ has number $2^{h+1}\lfloor \mathrm{sym}(v)/2^{h+1}\rfloor + 2^h$ .
Lemma 4: for unrelated $v, w$ ,

h(\operatorname{nca}(v,w)) = \lfloor \lg(\mathrm{sym}(v) \oplus \mathrm{sym}(w)) \rfloor .

The nca depth algorithm returns $\operatorname{depth}(\operatorname{nca}(v,w))$ .
The depth algorithm returns the number of the depth- $d_2$ ancestor of $v$ .

Two supporting statements pin the definitions to the paper: $\mathrm{sym}$ is a bijection onto $\{1, \dots, 2^{d+1} - 1\}$ , and the longest common prefix is the deepest common ancestor.

Significance

The constant-time nca computation on complete binary trees is the base case of the whole paper: §§4–5 embed an arbitrary tree into a moderately sized complete binary tree through a compressed tree and a balanced binary tree, and every query ends with the arithmetic of §3. The same idea, that in-order numbers encode ancestry in their low-order bits, underlies the Schieber–Vishkin algorithm. Lemma 1 identifies the height with the 2-adic valuation of the number, and Lemma 4 identifies the nca height with the position of the highest differing bit.

The results are proved in the paper, with the proofs left as "easy to verify". No machine-checked version of this numbering or of these four lemmas is known to exist in Mathlib or on this platform. A formal development supplies proofs of the four lemmas and the two algorithms, and a reusable library connecting in-order ranks of a complete binary tree to binary arithmetic (Nat.log, bitwise xor, 2-adic valuation).

Difficulty

The numbering is defined by a traversal order, while the lemmas speak about divisibility, floor division and exclusive or. The work lies in connecting the rank of a vertex in symmetric order to its closed form $(2j+1)\cdot 2^{h(v)}$ , where $j$ is its left-to-right position. That counting argument sums the sizes of the subtrees that precede $v$ and is where most of the effort goes. Lemma 4 then needs the observation that two unrelated numbers agree in all bits above the height of their nca and differ in the bit at that height. This is a statement about Nat.testBit of the exclusive or, and it fails for related vertices. The algorithm statements add a case analysis whose first two cases overlap when $v = w$ .

Formalization scope

A vertex of the tree of depth $d$ is a List Bool of length at most $d$ (false = left). Ancestry is the prefix relation, $\operatorname{nca}$ the longest common prefix, depth the length, and height $d - \text{length}$ . None of these structural notions uses the numbering.
$\mathrm{sym}(v)$ is the number of vertices whose in-order sort key is lexicographically at most that of $v$ . The key is the path with left $\mapsto 0$ , right $\mapsto 2$ , followed by $1$ . The numbering is not defined by the closed form or by a recursion on numbers: a definition of that kind would make the height- $h$ numbering and Lemma 1 immediate and move the content of the mission into an uncheckable definition.
$\lfloor \lg x \rfloor$ is Nat.log 2 x, which agrees for $x \ge 1$ . $\oplus$ is ^^^ on $\mathbb N$ , and floor division is / on $\mathbb N$ .
Interval tests $a \in [b - c + 1, b + c - 1]$ are written additively as $b + 1 \le a + c$ and $a + 1 \le b + c$ . The subtractions $d - h(v)$ and $d - d_2$ never truncate for heights and depths of vertices.
Lemma 3 states explicitly that $h \le d$ (" $h$ is a height") and that the ancestor exists. The depth algorithm assumes $d_2 \le \operatorname{depth}(v)$ , as printed.
$\mathrm{sym}^{-1}$ is not defined as a function. The goal and the depth algorithm state that a vertex has the computed number if and only if it is the nearest common ancestor (respectively the ancestor at depth $d_2$ ), which says that $\mathrm{sym}^{-1}$ of that number is that vertex.
The $O(1)$ time bounds are not formalized, since the random-access machine model is out of scope.

Proofs of any milestone are welcome.

Selected references

D. Harel and R. E. Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13(2) (1984), 338–355. https://doi.org/10.1137/0213024
A. V. Aho, J. E. Hopcroft and J. D. Ullman, On Finding Lowest Common Ancestors in Trees, SIAM J. Comput. 5(1) (1976), 115–132. https://doi.org/10.1137/0205011
B. Schieber and U. Vishkin, On Finding Lowest Common Ancestors: Simplification and Parallelization, SIAM J. Comput. 17(6) (1988), 1253–1262. https://doi.org/10.1137/0217079
M. A. Bender and M. Farach-Colton, The LCA Problem Revisited, LATIN 2000, LNCS 1776, 88–94. https://doi.org/10.1007/10719839_9

11 thms3 active usersReviewed

Completed

Combinatorics Complexity Theory Theoretical Computer Science·Captain: mikedeng1

Fast Algorithms for Finding Nearest Common Ancestors I: A Lower Bound for Pointer MachinesResearch Paper

Motivation

The nearest common ancestor problem asks, for a rooted tree and two of its vertices $x$ and $y$ , for the deepest vertex that is an ancestor of both, written $\operatorname{nca}(x,y)$ . It appears as a subroutine in string algorithms (suffix trees), in graph algorithms (path queries, dominators) and in the analysis of set-union structures. Aho, Hopcroft and Ullman (On finding lowest common ancestors in trees, SIAM J. Comput. 5, 1976) posed it in several versions, differing in how much the tree changes while the queries are answered.

Harel and Tarjan (Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13, 1984) study how the answer depends on the machine model. On a random-access machine, where addresses can be computed arithmetically, they preprocess a static tree in linear time and then answer each query in constant time. On a pointer machine, where memory can only be traversed by following pointers, their §2 shows that no representation of the tree allows constant-time queries: $\Omega(\log\log n)$ steps are needed in the worst case. This mission formalizes that lower bound.

Timeline.

1976: Aho, Hopcroft and Ullman give an $O(\log\log n)$ -per-query random-access algorithm for static trees.
1976: van Leeuwen (Finding lowest common ancestors in less than logarithmic time, unpublished report, reference [14] of Harel–Tarjan) gives an $O(n + m\log\log n)$ algorithm for static trees that runs on a pointer machine.
1984: Harel and Tarjan prove Theorem 1, the matching $\Omega(\log\log n)$ lower bound for pointer machines, and the $O(1)$ -per-query random-access algorithm.

Setting

A pointer machine stores its data as a collection of nodes. Each node has a fixed number of fields, and a pointer field holds either a node or nil. The machine can follow a pointer from a node it holds, but it cannot compute an address. Following Harel and Tarjan (p. 340), a static tree is represented by a list structure: each tree vertex $v$ is represented by a single node $\mathrm{rep}(v)$ , distinct vertices by distinct nodes, and the structure may contain further nodes that represent no vertex. Each node has two pointer fields; the paper reduces any fixed number of pointers to two "without loss of generality". To answer a query on $x$ and $y$ , the machine is given pointers to $\mathrm{rep}(x)$ and $\mathrm{rep}(y)$ and must return a pointer to $\mathrm{rep}(\operatorname{nca}(x,y))$ .

The node $b$ is accessible from $a$ in $j$ steps or less if it can be reached from $a$ by following at most $j$ pointers. Write $\mathrm{acc}_j(a)$ for the set of such nodes. A run of $t$ steps from input nodes $a$ and $b$ is a sequence $n_1,\dots,n_t$ in which each $n_s$ is the content of a pointer field of a node among $a, b, n_1, \dots, n_{s-1}$ . A query with answer $c$ is answered in $k$ steps if some run of at most $k$ steps holds $c$ .

The tree is the complete binary tree $T$ of height $h$ , with $n = 2^h$ leaves. Its vertices are the words $w \in \{0,1\}^{\le h}$ (the root-to-vertex path, $0$ = left), the ancestors of $v$ are its prefixes, the depth of $w$ is $|w|$ and its height is $h - |w|$ . Then $\operatorname{nca}(x,y)$ is the longest common prefix of $x$ and $y$ . Logarithms are binary: $\lg = \log_2$ .

Formalization targets

Goal: Theorem 1 in the explicit form of its proof

For every $h$ , every node type, every list structure with two pointers per node and every injective representation $\mathrm{rep}$ of the complete binary tree with $n = 2^h$ leaves: if every nca query on two leaves is answered in $k$ steps, then

k > \lg\lg n - 2 .

This is the last display of the proof (p. 341), which is what the paper's $\Omega(\log\log n)$ means. The representation is arbitrary and is quantified before the query bound, so the bound holds for every representation.

Milestones: the claims of the proof

A query answered in $k$ steps reaches only nodes in $\mathrm{acc}_k(\mathrm{rep}(x)) \cup \mathrm{acc}_k(\mathrm{rep}(y))$ .
$|\mathrm{acc}_j(a)| \le 2^{j+1} - 1$ for every node $a$ .
With $A_x$ the set of vertices whose nodes are accessible from $\mathrm{rep}(x)$ in $k$ steps or less: for a nonleaf $w$ with children $u, v$ , either $w \in A_x$ for every leaf $x$ below $u$ , or $w \in A_y$ for every leaf $y$ below $v$ .
A vertex of height $i \ge 1$ lies in $A_x$ for at least $2^{i-1}$ leaves $x$ .

\sum_{x \in L} |A_x| \ge \frac{n}{2}\lg n,

where $L$ is the set of leaves.

Significance

The result. Theorem 1 shows that van Leeuwen's pointer-machine algorithm for static trees is optimal up to a constant factor, and that the constant-time queries of the paper's §§3–5 depend on address arithmetic. It is an early nontrivial lower bound for pointer machines on a natural problem; the paper compares it with Tarjan's lower bound for disjoint-set union on a pointer machine (J. Comput. System Sci. 18, 1979).

Formalizing it. The theorem is proved in the paper; as far as could be determined no machine-checked version exists, and Mathlib has no pointer-machine model. The mission produces an explicit, reusable definition of pointer-machine runs and accessibility together with a complete proof of the explicit bound. A formal model of this kind is the precondition for stating any other pointer-machine lower bound.

Difficulty

The statement must hold for every representation, including structures with many auxiliary nodes and arbitrary pointers between tree nodes. Arguing about one natural representation, such as parent pointers, where a leaf is far from its ancestors, says nothing about other representations: a structure with shortcut pointers or auxiliary nodes may bring some ancestors close to some leaves, and the bound must survive every such choice. In the formal setting the counting also has to handle overlaps: nodes reachable from several leaves, nodes that represent no vertex, and pointer cycles.

Formalization scope

Model. Nodes form an arbitrary type N, not necessarily finite. ptr : N → Fin 2 → Option N gives the two pointer fields (none = nil), and rep : Vertex h → N is required to be injective. acc ptr j a is defined recursively. Run ptr a b t held is an inductive predicate for runs of $t$ steps, AnsweredIn asks for some run of at most $k$ steps holding the answer, and AnswersLeafQueriesIn ptr rep k requires this for every pair of leaves.
Conventions.
- Two pointer fields per node, as the paper's "without loss of generality" reduction allows; the reduction itself is not formalized.
- Only queries on two leaves are assumed answerable. This is weaker than all queries, so the theorem is at least as strong as the paper's.
- Time is counted as pointer-following steps. Mutation of the structure during a query and non-pointer fields are not modelled: neither lets the machine hold a node it has not reached by following pointers. The clause "the algorithm remembers nothing between queries" is built into the static structure.
- Vertex h is {s : List Bool // s.length ≤ h}, nca is the longest common prefix, and a separate theorem identifies it with the Appendix's deepest common ancestor. $n = 2^h$ counts leaves, not vertices.
- $\lg$ is Real.logb 2. For $h = 0$ Lean's $\log_2 0 = 0$ gives the true statement $k > -2$ ; for $h \ge 1$ , $\lg\lg n = \log_2 h$ .
- Cardinalities in the milestones are Set.encard in $\mathbb N \cup \{\infty\}$ , so finiteness is part of each claim. Divisions are cleared: $h\,2^h \le 2\sum_x |A_x|$ .
Ruling out trivial formalizations. The hypothesis AnswersLeafQueriesIn is satisfiable: the parent-pointer representation answers every leaf query in $h$ steps. If rep were not injective, a constant rep would answer every query in zero steps, so injectivity is kept in the goal. The milestones do not need it and do not assume it.
Infrastructure. The goal needs finite-set counting over the leaves of the complete binary tree and a double count over heights. The run and accessibility definitions are reusable for other pointer-machine arguments. Proofs of the milestones, and of the ℕ form $h < 2^{k+2}$ that the goal reduces to, are welcome.

Selected references

D. Harel, R. E. Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13(2):338–355, 1984. https://doi.org/10.1137/0213024
A. V. Aho, J. E. Hopcroft, J. D. Ullman, On finding lowest common ancestors in trees, SIAM J. Comput. 5(1):115–132, 1976. https://doi.org/10.1137/0205011
A. Schönhage, Storage modification machines, SIAM J. Comput. 9(3):490–508, 1980. https://doi.org/10.1137/0209036
R. E. Tarjan, A class of algorithms which require nonlinear time to maintain disjoint sets, J. Comput. System Sci. 18(2):110–127, 1979. https://doi.org/10.1016/0022-0000(79)90042-4

8 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Numerical Analysis+1·Captain: mikedeng1

Proximal Newton-Type Methods for Minimizing Composite Functions II: Local Linear and Superlinear Convergence of the Inexact Proximal Newton MethodResearch Paper

Motivation

Many estimation problems in statistics, signal processing and bioinformatics minimize a composite function $f = g + h$ : a smooth convex loss $g$ plus a convex but nonsmooth penalty or constraint $h$ , such as the lasso's $\ell_1$ norm or the indicator of a convex set. Proximal Newton-type methods handle such problems by minimizing, at each iterate $x_k$ , a model $\hat f_k = \hat g_k + h$ in which $g$ is replaced by its second-order Taylor expansion. Widely used solvers of this kind (glmnet, newGLMNET, QUIC) never solve these model subproblems exactly; they stop an inner iterative solver early by some heuristic. Lee, Sun and Saunders (arXiv:1206.1623v13, 2014) proposed an adaptive stopping rule for the inner solver and proved that it preserves fast local convergence. This mission formalizes that local convergence theory (§3.4 of the paper).

Timeline:

1982: Dembo, Eisenstat and Steihaug introduce inexact Newton methods for smooth equations and prove local linear and superlinear convergence under a relative-residual condition with forcing terms $\eta_k$ (doi:10.1137/0719025).
1996: Eisenstat and Walker propose self-adjusting forcing terms that avoid oversolving (doi:10.1137/0917003).
2012–2014: Lee, Sun and Saunders transfer the relative-residual condition to composite functions, replacing gradients by composite gradient steps, and prove Theorems 3.10 and 3.11.
2016: Byrd, Nocedal and Oztoprak analyze inexact proximal Newton methods for $\ell_1$ -regularized problems under an additional sufficient-descent condition on the subproblem (doi:10.1007/s10107-015-0941-y).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product. The smooth part $g:\mathbb R^n\to\mathbb R$ is twice continuously differentiable and strongly convex with constant $m>0$ : $g(y)\ge g(x)+\nabla g(x)^T(y-x)+\frac m2\|x-y\|^2$ for all $x,y$ . Its gradient $\nabla g$ is Lipschitz with constant $L_1$ , its Hessian $\nabla^2 g$ is Lipschitz with constant $L_2$ , and $\nabla^2 g(x)\preceq MI$ for a constant $M>0$ . The nonsmooth part $h$ is proper, closed and convex, and may take the value $+\infty$ ; it is given by its domain $D$ and its values on $D$ . The problem is $\min_x f(x)=g(x)+h(x)$ , and $x^\star$ denotes its (unique) optimal solution.

The proximal mapping of $h$ is $\operatorname{prox}_h(v)=\arg\min_y h(y)+\frac12\|y-v\|^2$ . The composite gradient step with step length $t>0$ is

G_{tf}(x)=\tfrac1t\big(x-\operatorname{prox}_{th}(x-t\nabla g(x))\big),

with $G_f=G_{1f}$ ; it vanishes exactly at minimizers of $f$ and plays the role of the gradient. The step $G_{f/M}$ is the unit step on $f/M=g/M+h/M$ . The model at $x_k$ is $\hat f_k=\hat g_k+h$ with $\hat g_k(y)=g(x_k)+\nabla g(x_k)^T(y-x_k)+\frac12(y-x_k)^T\nabla^2 g(x_k)(y-x_k)$ .

The inexact proximal Newton method with unit step lengths produces $x_{k+1}=x_k+\Delta x_k$ , where the direction $\Delta x_k$ is any point satisfying the adaptive stopping condition

\|G_{\hat f_k/M}(x_k+\Delta x_k)\|\le\eta_k\,\|G_{f/M}(x_k)\|\qquad(2.24)

for a forcing term $\eta_k\ge0$ . The Eisenstat–Walker choice is

\eta_k=\min\Big\{\frac m2,\ \frac{\|G_{\hat f_{k-1}/M}(x_k)-G_{f/M}(x_k)\|}{\|G_{f/M}(x_{k-1})\|}\Big\}.\qquad(2.25)

Formalization targets

Goal: Theorem 3.10 (p. 17)

There are $\bar\eta\in(0,m/2)$ , $\delta>0$ and $r\in[0,1)$ such that, whenever $0\le\eta_k\le\bar\eta$ for all $k$ and $\|x_0-x^\star\|<\delta$ ,

\|x_{k+1}-x^\star\|\le r\,\|x_k-x^\star\|\quad\text{for all }k.

For every forcing sequence with $\eta_k\ge0$ , $\eta_k\to0$ , there is $\delta>0$ such that every run with $\|x_0-x^\star\|<\delta$ converges to $x^\star$ q-superlinearly: for every $\varepsilon>0$ , eventually $\|x_{k+1}-x^\star\|\le\varepsilon\|x_k-x^\star\|$ .

Both parts are asserted together. The statement fixes no constant beyond the existence of $\bar\eta$ , $\delta$ and $r$ .

Milestones

§2.1, property 3: $G_f(x)=0$ if and only if $x$ minimizes $f$ .
Lemma 2.2: $\|G_f(x)\|\le(L_1+1)\|x-x^\star\|$ .
Lemma 3.8: $\|G_f(x)-G_{\hat f_k}(x)\|\le\frac{L_2}2\|x-x_k\|^2$ .
Lemma 3.9: $(x-y)^T(G_{tf}(x)-G_{tf}(y))\ge\frac m2\|x-y\|^2$ for $0<t\le1/L_1$ .
Theorem 3.11: with the forcing terms (2.25), the method converges q-superlinearly from every start sufficiently close to $x^\star$ .

Significance

Theorem 3.10 justifies stopping the inner solver of a proximal Newton method at a relative accuracy that is set by the current optimality measure $\|G_{f/M}(x_k)\|$ : a constant small forcing term keeps linear convergence, and forcing terms that decay to zero recover superlinear convergence, with no sufficient-descent condition on the subproblem and for a generic nonsmooth $h$ . Theorem 3.11 shows that the self-adjusting choice (2.25) achieves the superlinear regime automatically. Together they are the composite analogue of the inexact Newton theory used in most large-scale smooth solvers.

The results are proved in the paper. No machine-checked proof of any of them is known, and the platform contains no proximal mapping, composite gradient step or inexact Newton condition. A formalization adds a checked proximal-operator toolkit (existence and nonexpansiveness of $\operatorname{prox}$ , the optimality characterization of $G_f$ , strong monotonicity of $G_{tf}$ ) and a precise form of the theorem: the paper's proofs mix two scalings of the composite step and cite a lemma where another is meant, so the formal proof settles which constants are valid.

Difficulty

The obvious argument compares the inexact step with the exact proximal Newton step and treats the gap as a perturbation. For composite functions this fails: the exact step is defined by a nonsmooth inclusion, and the stopping condition bounds a residual of the model's composite gradient step, not the distance to the model's minimizer. The link between the two is strong monotonicity of the composite gradient step (Lemma 3.9), which requires controlling the proximal mapping of a general closed convex $h$ jointly with the curvature of $g$ ; for $h=0$ it is immediate, and for general $h$ it is the central step. A second difficulty is that the threshold on $\eta_k$ is not scale invariant: a threshold below $m/2$ chosen arbitrarily does not give convergence, so the admissible $\bar\eta$ has to come out of the analysis.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). The nonsmooth part is a pair $(D,h)$ : $D$ nonempty and convex, $h$ convex on $D$ , and the extended function ( $h$ on $D$ , $+\infty$ off $D$ ) lower semicontinuous; indicator functions of closed convex sets are included. The proximal mapping is a total function chosen among the minimizers over $D$ , which exist uniquely under these hypotheses. $G_{f/M}$ , $G_{\hat f_k/M}$ and $G_{tf}$ are functions of the split $(g,D,h)$ and a scalar, never of $f$ alone. The Hessian is the derivative of the gradient map, measured in operator norm. Sequences are indexed from $k=0$ ; a run requires $x_0\in D$ and $x_k+\Delta x_k\in D$ . Rates are stated without quotients.

" $x_0$ sufficiently close to $x^\star$ " is an existential radius chosen before the run; assuming $x_k\to x^\star$ , letting the radius depend on the run, or reading part 1 as "for every $\bar\eta<m/2$ " (which is false: $g(x)=2x^2$ , $h=0$ , $\eta_k\equiv\frac32$ diverges) are ruled out. The forcing sequence of Theorem 3.10 is fixed in advance; that of Theorem 3.11 depends on the iterates through (2.25), with a free first term $\eta_0\in[0,m/2]$ .

A complete development needs existence, uniqueness and firm nonexpansiveness of the proximal mapping of an extended-valued closed convex function, the subgradient characterization of $\operatorname{prox}$ , and a second-order Taylor bound for $C^2$ functions with Lipschitz Hessian. These are reusable well beyond this mission. Contributions of any of them, of the milestones, or of alternative proofs of Lemma 3.9 are welcome.

Selected references

J. D. Lee, Y. Sun, M. A. Saunders, Proximal Newton-type methods for minimizing composite functions, arXiv:1206.1623v13, 2014; SIAM J. Optim. 24(3), 2014. https://arxiv.org/abs/1206.1623
R. S. Dembo, S. C. Eisenstat, T. Steihaug, Inexact Newton methods, SIAM J. Numer. Anal. 19(2), 1982. https://doi.org/10.1137/0719025
S. C. Eisenstat, H. F. Walker, Choosing the forcing terms in an inexact Newton method, SIAM J. Sci. Comput. 17(1), 1996. https://doi.org/10.1137/0917003
R. H. Byrd, J. Nocedal, F. Oztoprak, An inexact successive quadratic approximation method for L-1 regularized optimization, Math. Program. 157, 2016. https://doi.org/10.1007/s10107-015-0941-y

9 thms3 active usersReviewed

Completed

Graph Theory Operations Research Optimization+1·Captain: mikedeng1

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

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

Formalization targets

Goal: Corollary 4.4 (p. 931)

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

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

The constant is the printed one.

Milestones

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

Significance

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

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

Difficulty

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

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

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

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

Formalization scope

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

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

All constants are explicit, exactly as printed:

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

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

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

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

Selected references

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

10 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Numerical Analysis+1·Captain: mikedeng1

Proximal Newton-Type Methods for Minimizing Composite Functions I: Proximal Quasi-Newton Methods Converge Q-Superlinearly under the Dennis–Moré CriterionResearch Paper

Motivation

Many estimation problems in statistics, machine learning and signal processing minimize a composite function, the sum of a smooth loss and a convex but nonsmooth regularizer or constraint: the lasso and $\ell_1$ -regularized logistic regression, the graphical lasso for sparse inverse covariance estimation, and constrained least squares, where the nonsmooth part is the indicator function of a convex set. First-order proximal gradient methods (ISTA, FISTA, SpaRSA) are the standard tools, and their convergence is at best linear. Practical solvers such as glmnet, newGLMNET and QUIC instead minimize a local quadratic model of the smooth part plus the nonsmooth part at every iteration, and in practice they need far fewer iterations.

Lee, Sun and Saunders (arXiv:1206.1623, SIAM J. Optim. 2014) put these methods into one framework, proximal Newton-type methods, and proved that they inherit the local convergence rates of Newton and quasi-Newton methods for smooth problems. This mission formalizes the exact-subproblem half of their analysis, ending with q-superlinear convergence of proximal quasi-Newton methods whose Hessian approximations satisfy the Dennis–Moré criterion.

Timeline. Dennis and Moré (1974) characterized superlinear convergence of quasi-Newton methods for smooth equations and minimization by what is now called the Dennis–Moré condition. Tseng and Yun (2009) analyzed coordinate gradient descent for composite problems with a scaled quadratic model. Byrd, Nocedal and Oztoprak (2013) studied inexact proximal Newton methods for $\ell_1$ -regularized problems. Lee, Sun and Saunders (2012–2014) proved quadratic and superlinear local convergence for a generic closed convex $h$ .

Setting

The problem is

\min_{x\in\mathbb R^n} f(x) := g(x) + h(x). \qquad (1.1)

The smooth part $g:\mathbb R^n\to\mathbb R$ is twice continuously differentiable and strongly convex with constant $m>0$ , meaning $g(y)\ge g(x)+\nabla g(x)^T(y-x)+\tfrac m2\|x-y\|^2$ for all $x,y$ (Definition 3.2). Its gradient $\nabla g$ and Hessian $\nabla^2 g$ are Lipschitz continuous with constants $L_1$ and $L_2$ . The nonsmooth part $h$ is a proper closed convex function that may take the value $+\infty$ . Its effective domain $D=\operatorname{dom} h$ is nonempty and convex, and $x^\star$ denotes the optimal solution of (1.1), which is unique by strong convexity.

At an iterate $x_k$ the method chooses a symmetric positive definite matrix $H_k$ and computes the search direction $\Delta x_k$ , the minimizer of the model subproblem

\Delta x_k=\arg\min_d\ \nabla g(x_k)^Td+\tfrac12 d^TH_kd+h(x_k+d). \qquad (2.9)

The predicted decrease is $\lambda_k=\nabla g(x_k)^T\Delta x_k+h(x_k+\Delta x_k)-h(x_k)$ . A step length $t$ satisfies the sufficient descent condition (2.19) if $f(x_k+t\Delta x_k)\le f(x_k)+\alpha t\lambda_k$ for a fixed $\alpha\in(0,\tfrac12)$ . A backtracking line search with factor $\beta\in(0,1)$ takes $t_k=\beta^{j}$ for the least $j\ge0$ that passes, so the unit step is tried first. The update is $x_{k+1}=x_k+t_k\Delta x_k$ (Algorithm 1). With $H_k=\nabla^2 g(x_k)$ this is the proximal Newton method. With any other choice of $H_k$ it is a proximal quasi-Newton method. The sequence $\{H_k\}$ satisfies the Dennis–Moré criterion if

\frac{\|(H_k-\nabla^2 g(x^\star))(x_{k+1}-x_k)\|}{\|x_{k+1}-x_k\|}\to0. \qquad (3.2)

Formalization targets

Goal: Theorem 3.7

If $mI\preceq H_k\preceq MI$ for all $k$ , with $0<m\le M$ , and $\{H_k\}$ satisfies (3.2), then every run of Algorithm 1 from any $x_0\in D$ satisfies

x_k\to x^\star,\qquad \|x_{k+1}-x^\star\|=o(\|x_k-x^\star\|).

The goal fixes no rate constant. It asserts only the shape of the convergence.

Milestones

In the order the proof uses them:

Proposition 2.4: $\lambda\le-\Delta x^TH\Delta x$ and $f(x+t\Delta x)\le f(x)+t\lambda+O(t^2)$ .
Proposition 2.5: $x$ is optimal if and only if $\Delta x=0$ at $x$ .
Lemma 2.6: every $t\le\min\{1,(2m/L_1)(1-\alpha)\}$ satisfies (2.19).
Theorem 3.1 (global convergence), restated under the assumptions of §3.3: $x_k\to x^\star$ .
Lemma 3.3: the proximal Newton method eventually accepts the unit step.
Theorem 3.4: the proximal Newton method converges q-quadratically, with eventually

\|x_{k+1}-x^\star\|\le\frac{L_2}{2m}\|x_k-x^\star\|^2 .

Lemma 3.5 / A.1: under (3.2) the unit step is eventually accepted.
Proposition 3.6: $\|\Delta x_1-\Delta x_2\|\le\sqrt{(1+\bar\theta)/m}\,\|(H_2-H_1)\Delta x_1\|^{1/2}\|\Delta x_1\|^{1/2}$ , with $\bar\theta$ depending only on the eigenvalue bounds.

Significance

The result. Theorem 3.7 is the composite counterpart of the Dennis–Moré theorem. It says that the rate of a proximal quasi-Newton method is governed by how well $H_k$ approximates the Hessian of the smooth part along the steps actually taken, whatever the nonsmooth part is. It covers proximal BFGS-type methods for $\ell_1$ -regularized and constrained problems, and it explains why solvers built on these methods reach high accuracy in few iterations. Theorem 3.4 gives the corresponding quadratic rate when the exact Hessian is used.

Formalizing it. The results are proved in the paper. None of them has a machine-checked proof: the platform currently has Newton's method only for smooth objectives (Boyd–Vandenberghe's quadratic phase in the mission Convex Optimization V: Newton's Method), and nothing on proximal or composite Newton-type methods. The formalization also settles two defects of the printed text. Theorem 3.1 is false as printed, since it lacks an upper bound on $H_k$ : with $g(x)=x^2/2$ , $h=0$ and $H_k=2^{k+1}$ the iterates stall at about $0.289\,x_0$ . It is therefore stated here under the assumptions of §3.3. Proposition 3.6 uses an undefined constant $m_1$ (read as $m$ ), and the first-order inequalities in its printed proof contain a typo. The explicit constant $L_2/(2m)$ in Theorem 3.4 is the one the paper's proof derives.

Difficulty

The difficulty is the nonsmooth part. For smooth $g$ the Newton step solves a linear system, and the classical analysis works with that closed form. Here $\Delta x_k$ is defined only as the minimizer of a nonsmooth subproblem, and every estimate on it has to come from the optimality of that minimizer, i.e. from the firm nonexpansiveness of scaled proximal maps in a norm that changes with $H_k$ . A natural first idea is to apply the smooth Dennis–Moré argument to $\nabla f$ . It fails because $f$ is not differentiable and may be $+\infty$ outside $D$ . The superlinear rate also depends on the line search eventually accepting the unit step. That acceptance comes only from a third-order Taylor bound combined with (2.15) and the Dennis–Moré residual, and a line search that may return any admissible step does not give it.

Formalization scope

Space. The space is EuclideanSpace ℝ (Fin n), and matrices are continuous linear operators. $\nabla g$ is Mathlib's gradient, and $\nabla^2 g$ is fderiv ℝ (gradient g). "Positive definite" includes symmetry, and $mI\preceq H\preceq MI$ is stated through quadratic forms of a symmetric $H$ .
The nonsmooth part. $h$ is encoded by its domain $D$ and its values on $D$ : $D$ is nonempty and convex, $h$ is convex on $D$ , and the $+\infty$ -extension of $h$ is lower semicontinuous. The objective $f$ is extended-valued. Only comparisons are made in EReal, never arithmetic. Replacing $h$ by a real-valued function on all of $\mathbb R^n$ would exclude indicator functions and is not the paper's setting.
Algorithm. The search direction is a predicate: it minimizes (2.9) over $\{d : x+d\in D\}$ . Backtracking is the least- $j$ rule with factor $\beta\in(0,1)$ , the convention of Boyd and Vandenberghe, whom the paper cites for its line search. Runs are infinite and indexed from $k=0$ , with no stopping test.
Rates. $o(\cdot)$ and (3.2) are stated without quotients: for every $\varepsilon>0$ the inequality holds eventually.
Ruling out trivial versions. A line search allowed to return any step satisfying (2.19) would make Theorems 3.4 and 3.7 false. Taking $x^\star$ to be an arbitrary point instead of the minimizer, or letting $\bar\theta$ in Proposition 3.6 depend on the data, would empty the statements. None of these readings is used.
Infrastructure. A complete development needs: existence and uniqueness of minimizers of strongly convex, lower semicontinuous extended functions; first-order optimality for the subproblem; firm nonexpansiveness of scaled proximal maps in the $H$ -norm; and second- and third-order Taylor bounds from Lipschitz derivatives. These pieces are reusable across proximal methods. Contributions of any milestone, of these supporting lemmas, or of the goal directly are welcome.

Selected references

J. D. Lee, Y. Sun, M. A. Saunders, Proximal Newton-type methods for minimizing composite functions, arXiv:1206.1623v13 (2014); SIAM J. Optim. 24(3), 2014. https://arxiv.org/abs/1206.1623
J. E. Dennis, J. J. Moré, A characterization of superlinear convergence and its application to quasi-Newton methods, Math. Comp. 28 (1974), 549–560. https://doi.org/10.1090/S0025-5718-1974-0343581-1
P. Tseng, S. Yun, A coordinate gradient descent method for nonsmooth separable minimization, Math. Program. 117 (2009), 387–423. https://doi.org/10.1007/s10107-007-0170-0
R. H. Byrd, J. Nocedal, F. Oztoprak, An inexact successive quadratic approximation method for convex L-1 regularized optimization, Math. Program. 157 (2016), 375–396; arXiv:1309.3529. https://arxiv.org/abs/1309.3529
S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://web.stanford.edu/~boyd/cvxbook/

10 thms3 active usersReviewed

Completed

Graph Theory Operations Research Optimization+1·Captain: mikedeng1

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

Motivation

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

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorems 3.11 and 3.4

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

17 thms3 active usersReviewed

Completed

Operations Research Probability Statistics·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: THEOREM 5, combining equally spaced subintervals

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

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

with, if $a > 0$ ,

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

and, if $a = 0$ ,

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

8 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: mikedeng1

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

Motivation

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

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

Setting

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

The data are:

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

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

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

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

Formalization targets

Goal: uniqueness of solutions with vanishing tail

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

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

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

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

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

Milestones

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

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

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

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

Selected references

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

6 thms3 active usersReviewed

Completed

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

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