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.

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999112Formalized record≤ 1.999074Open frontier

2 provers on it3 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

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

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

≤ 2.9983Formalized record≤ 2.99791Open frontier

3 provers on it2 of 3 missions formalized

The irrationality measure of π

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

≤ 7.606309Formalized record

6 provers on it7 of 7 missions formalized

Sharp diagonal Hlawka constant

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

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

References:

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

≤ 80Formalized record

3 provers on it7 of 7 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.

≤ 41Formalized record≤ 5Open frontier

35 provers on it11 of 13 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.

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999112Formalized record≤ 1.999074Open frontier

2 provers on it3 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

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

≤ 2.9983Formalized record≤ 2.99791Open frontier

3 provers on it2 of 3 missions formalized

The irrationality measure of π

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

≤ 7.606309Formalized record

6 provers on it7 of 7 missions formalized

Sharp diagonal Hlawka constant

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

References:

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

≤ 80Formalized record

3 provers on it7 of 7 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.

≤ 41Formalized record≤ 5Open frontier

35 provers on it11 of 13 missions formalized

Matrix multiplication exponent

≤ 2.37134Formalized record≤ 2.371177Open frontier

16 provers on it7 of 8 missions formalized

All missions

Completed

Discrete Geometry Linear Optimization Operations Research+1·Captain: mikedeng1

Elementare Theorie der konvexen Polyeder I: A Point on All Extreme Supports of a Finite Cone Is a Nonnegative Combination of at Most n GeneratorsResearch Paper

Motivation

A polyhedral cone can be described in two ways: as the set of nonnegative combinations of finitely many vectors (a finitely generated cone), or as the intersection of finitely many closed half-spaces through the origin. That the two descriptions give the same class of sets is the Minkowski–Weyl theorem. It is the structural basis of linear programming: the simplex method, LP duality, Farkas' lemma, and the vertex/facet description of polytopes used throughout combinatorial optimization all rest on it.

Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv. 7, 290–306) gives an elementary, self-contained proof of both directions. Its first result, which Weyl calls the Hauptsatz (main theorem, Satz 1), is the direction "finitely generated ⇒ finite intersection of half-spaces", in a sharp form: the half-spaces needed are exactly the extreme supports of the generating set, i.e. its facets. Its sharpening, Satz 2, bounds the number of generators needed to represent a point by the dimension $n$ . This mission formalizes §§1–2 of the paper (pp. 290–295): the Hauptsatz, its sharpening, and the steps of Weyl's inductive proof.

Timeline:

1896, H. Minkowski, Geometrie der Zahlen: polytopes as bounded intersections of half-spaces and as convex hulls of finitely many points.
1911, C. Carathéodory: a point in the convex hull of a set in $\mathbb{R}^d$ is a convex combination of at most $d+1$ of its points (Rend. Circ. Mat. Palermo 32).
1935, H. Weyl: the present paper; Satz 1 and Satz 2 for cones, with the dual statements in §3 and the polytope theorem in §4.

Setting

Points of $\mathbb{R}^n$ are $n$ -tuples $x = (x_1, \ldots, x_n)$ , and $\langle \alpha, x \rangle = \alpha_1 x_1 + \cdots + \alpha_n x_n$ . A vector $\alpha \ne 0$ determines the half-space $\{x : \langle\alpha,x\rangle \ge 0\}$ ; positive multiples of $\alpha$ give the same half-space.

A point system $S$ is a finite set of points of $\mathbb{R}^n$ . It is non-degenerate if its points do not all satisfy one equation $\langle\alpha,x\rangle = 0$ with $\alpha \neq 0$ , i.e. the only $\alpha$ orthogonal to every point of $S$ is $0$ .

A half-space $\langle\alpha,x\rangle\ge 0$ ( $\alpha\ne 0$ ) is a support of $S$ if every point of $S$ lies in it. It is an extreme support if, in addition, equality $\langle\alpha,x\rangle = 0$ holds at $n-1$ linearly independent points $x$ of $S$ .

A point $x$ is representable by $S$ if it is a nonnegative combination of the points of $S$ :

x = \sum_{s\in S} c_s\, s, \qquad c_s \ge 0 .

The set of points lying in all extreme supports of $S$ is Weyl's konvexe Pyramide. In the Lean development these objects are Representable, NonDegenerate, IsSupport and IsExtremeSupport in the namespace WeylPolyhedra.Pyramid, with points of type Fin n → ℝ and $\langle\alpha,x\rangle$ written α ⬝ᵥ x.

Formalization targets

Goal: Satz 2 (Verschärfung des Hauptsatzes), p. 295

For a finite non-degenerate $S \subset \mathbb{R}^n$ and a point $x$ with $\langle\alpha,x\rangle\ge 0$ for every extreme support $\alpha$ of $S$ ,

\exists\, T \subseteq S,\quad |T| \le n,\quad x = \sum_{t\in T} c_t\, t,\ \ c_t \ge 0 .

Satz 1 (Hauptsatz), p. 291

Under the same hypotheses, $x$ is representable by $S$ . Satz 2 contains Satz 1.

Steps of the proof (§1–§2)

A finite non-degenerate $S$ has only finitely many extreme supports, up to positive scaling (p. 291).
The reduction step of case a) (p. 292): if $S$ has an extreme support $\beta$ and $p$ satisfies all extreme supports, there are $e \in S$ with $\langle\beta,e\rangle>0$ and $\lambda\ge 0$ such that $q = p-\lambda e$ still satisfies all extreme supports and lies on the plane of one of them.
The lifting step (p. 293): with $x_n \ge 0$ an extreme support of $S$ and $S_0$ the points on $x_n = 0$ , every extreme support $\beta$ of $S_0$ in $\mathbb{R}^{n-1}$ lifts to the extreme support $\beta_1x_1+\cdots+\beta_{n-1}x_{n-1} - \mu x_n \ge 0$ of $S$ (inequality (6)).
Case b) (p. 291, proved pp. 293–294): if $S$ has no extreme support, every point of $\mathbb{R}^n$ is representable by $S$ .

Significance

Satz 1 together with its trivial converse identifies the cone generated by $S$ with the intersection of its extreme-support half-spaces. This is one half of the Minkowski–Weyl theorem for cones, and it names the half-spaces: they are the facets of the cone. Satz 2 adds the conic form of Carathéodory's theorem: every point of a cone generated by a finite spanning set in $\mathbb{R}^n$ is a nonnegative combination of at most $n$ generators. In linear programming this is the statement that a feasible system has a basic feasible solution. The second mission in this series, on §§3–4 of the paper, uses Satz 1 to prove that a bounded region cut out by finitely many inequalities is the convex hull of finitely many points, and conversely.

On formalization status: Mathlib defines finitely generated and dually finitely generated pointed cones (PointedCone, PointedCone.DualFG) and proves Carathéodory's theorem for convex hulls (convexHull_eq_union), but, at the pinned revision, it does not prove the Minkowski–Weyl theorem or the facet description of a finitely generated cone. The results are classical and proved in the paper; this mission produces machine-checked proofs of them, in Weyl's formulation with extreme supports, together with the intermediate steps of his induction.

Difficulty

The hypothesis only controls $x$ against the extreme supports, not against every support. Showing that $x$ lies in the cone generated by $S$ whenever $\langle\alpha,x\rangle\ge 0$ holds for every support is the conic Farkas lemma, which follows from a separating hyperplane argument. Here that argument is not enough: a separating hyperplane is a support, but in general not an extreme one, and the statement is about the finitely many extreme ones. The proof has to produce, for a point outside the cone, a violated extreme support, which requires control over the facet structure of the cone.

The dimension count of Satz 2 is a second difficulty. An induction on the dimension naturally gives $n$ generators in one case and $n+1$ in another (a point of a half-space needs one generator on each side), and Weyl notes that he could not avoid a detour to recover the bound $n$ . The case where $S$ has no extreme support at all must also be handled separately; it is not vacuous, since $S$ can then generate all of $\mathbb{R}^n$ .

Formalization scope

Conventions committed to in Lean:

$\mathbb{R}^n$ is Fin n → ℝ; points and normals share this type (the dual space is identified with $\mathbb{R}^n$ , as in the paper). The pairing is dotProduct, written α ⬝ᵥ x.
A point system is a Finset (Fin n → ℝ). The zero vector is not excluded.
A support normal satisfies α ≠ 0. Extreme supports require a subset T ⊆ S with T.card = n - 1 whose elements are linearly independent in the vector space $\mathbb{R}^n$ .
"All extreme support equations are satisfied" in Satz 1 is read as the inequalities $\langle\alpha,x\rangle\ge0$ for every extreme normal $\alpha$ , as the proof and Satz 2 make explicit. The hypothesis quantifies over all extreme normals, so no representatives are chosen.
"Positive-linear" combinations have nonnegative coefficients (display (3)). In Satz 2 the subset $T$ is not required to be linearly independent.
Finiteness of extreme supports is stated up to positive scaling.
The lifting step is stated in the coordinates Weyl fixes on p. 293: $\mathbb{R}^n$ is Fin (m+1) → ℝ, the extreme support is $x_n \ge 0$ (Fin.last m), $S_0$ is projected by Fin.init, and $\mu$ is given together with hypotheses that it is the attained minimum. The hypothesis $n \ge 2$ is made explicit.

Replacing extreme supports by all supports in the hypothesis of Satz 1 or Satz 2 would turn the goal into a much weaker theorem (the conic Farkas lemma plus Carathéodory) and is not an admissible formalization. Dropping non-degeneracy makes Satz 1 false: for $S = \{e_1\} \subset \mathbb{R}^2$ the extreme supports are $\pm x_2 \ge 0$ , and $x = (-1, 0)$ satisfies both without being a nonnegative multiple of $e_1$ .

A complete development needs basic linear algebra over Fin n → ℝ (hyperplanes through $n-1$ independent points, projection to a coordinate hyperplane) and finite minimisation. The facet description of finitely generated cones, conic Carathéodory and the finiteness of facets are reusable beyond this mission, including for the second mission of the series. Contributions of lemmas on PointedCone that connect Representable with PointedCone.span are welcome.

Selected references

H. Weyl, Elementare Theorie der konvexen Polyeder, Commentarii Mathematici Helvetici 7 (1935), 290–306. https://doi.org/10.1007/BF01292722
C. Carathéodory, Über den Variabilitätsbereich der Fourier'schen Konstanten von positiven harmonischen Funktionen, Rendiconti del Circolo Matematico di Palermo 32 (1911), 193–217. https://doi.org/10.1007/BF03014795
A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, §7.2 (the Farkas–Minkowski–Weyl theorem). ISBN 978-0-471-98232-6
G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995, Lecture 1. https://doi.org/10.1007/978-1-4613-8431-1

9 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research+2·Captain: mikedeng1

An Analysis of Several Heuristics for the Traveling Salesman Problem II: Every Insertion Method Is Within ⌈lg n⌉ + 1 of the Optimal TourResearch Paper

Motivation

The traveling salesman problem asks for a shortest closed route visiting every node of a weighted complete graph exactly once. It is NP-hard, so practitioners use fast heuristics, and the basic question about a heuristic is how far from optimal its tour can be. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the simple constructive heuristics under the triangle inequality: nearest neighbor, the family of insertion methods, and several variants.

Insertion methods build a tour by growing it one node at a time. They are among the most widely used construction heuristics in practice and in textbooks, and they differ only in the rule that chooses which node to insert next: the nearest one, the cheapest one, the farthest one, a random one, or any other. This mission formalizes the paper's result that holds for the whole family at once, regardless of that rule: every insertion method produces a tour at most $\lceil \lg n\rceil + 1$ times longer than an optimal one (Theorem 3, p. 571).

Timeline. 1977: Rosenkrantz, Stearns and Lewis prove $\lceil\lg n\rceil+1$ for every insertion method (Theorem 3), $\tfrac12(\lceil\lg n\rceil+1)$ for nearest neighbor (Theorem 1), both from a shared counting lemma (Lemma 1), and the constant $2$ for nearest and cheapest insertion (Theorem 4). 1994: Bafna, Kalyanasundaram and Pruhs (Theoretical Computer Science 125, 1994) give instances on which some insertion methods reach ratio $\Omega(\log n/\log\log n)$ , so the logarithmic growth cannot be replaced by a constant for the family as a whole.

Setting

A traveling salesman graph with $n$ nodes consists of a finite node set $N$ with $|N|=n$ and a distance $d:N\times N\to\mathbb R$ with $d(i,j)=d(j,i)$ , $d(i,j)\ge 0$ and $d(i,j)+d(j,k)\ge d(i,k)$ for all nodes (the triangle inequality). A tour visits every node once and returns to its start; its length is the sum of its edge lengths, and OPTIMAL is the least length of a tour.

A subtour is a tour on a subset of the nodes; a single node is a tour without edges. Given a subtour $T$ and a node $k\notin T$ , TOUR $(T,k)$ is obtained by choosing an edge $(x,y)$ of $T$ minimizing

d(x,k)+d(k,y)-d(x,y)

and replacing it by the edges $(x,k)$ and $(k,y)$ ; if $T$ is a single node $i$ , TOUR $(T,k)$ is the two-node tour $(i,k),(k,i)$ . COST $(T,k)$ is the length of TOUR $(T,k)$ minus the length of $T$ .

An insertion method constructs subtours $T_1,\dots,T_n$ with $T_1=\{a_0\}$ a single node and $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$ for some node $a_i\notin T_i$ , $1\le i<n$ . The final tour $T_n$ is the approximation, and INSERT denotes its length. No rule for choosing the $a_i$ is fixed, and ties between minimizing edges are broken arbitrarily.

Write $\lg$ for the logarithm to base 2 and $\lceil x\rceil$ for the least integer $\ge x$ .

Formalization targets

Goal: Theorem 3

For every traveling salesman graph with $n\ge 1$ nodes and every run of every insertion method,

\mathrm{INSERT}\ \le\ \bigl(\lceil\lg n\rceil+1\bigr)\cdot\mathrm{OPTIMAL}.

Milestones

(2.2), shortcutting: visiting a subset of the nodes in the order of a tour gives a tour of the subset that is no longer.
(2.1): if the numbers $l_1\ge\dots\ge l_n$ satisfy $d(p,q)\ge\min(l_p,l_q)$ for distinct $p,q$ , then $\mathrm{OPTIMAL}\ge 2\sum_{i=k+1}^{\min(2k,n)} l_i$ for $1\le k\le n$ .
Lemma 1: if $d(p,q)\ge\min(l_p,l_q)$ for distinct nodes and $l_p\le\frac12\mathrm{OPTIMAL}$ for all $p$ , then

\sum_p l_p\le\tfrac12\bigl(\lceil\lg n\rceil+1\bigr)\mathrm{OPTIMAL}.

Lemma 2: $\mathrm{COST}(T,k)\le 2\,d(k,j)$ for every node $j$ of $T$ .
(3.7): $\mathrm{INSERT}=\sum_{i=1}^{n-1}\mathrm{COST}(T_i,a_i)$ .
(3.10): $\mathrm{COST}(T_i,a_i)\le 2\,d(a_i,a_j)$ whenever $j<i$ .
(3.12): $\mathrm{COST}(T_i,a_i)\le\mathrm{OPTIMAL}$ for $1\le i<n$ .

Significance

The result. Theorem 3 is a guarantee for an entire class of algorithms rather than for one. Any rule for choosing the next node, including rules designed for speed or for empirical quality, inherits a worst-case ratio of $\lceil\lg n\rceil+1$ from the insertion step alone. The rule matters only for improving on that: nearest and cheapest insertion achieve the constant $2(1-1/n)$ (Theorem 4 and its corollary, the subject of the third mission of this series), while the logarithmic bound remains the best general statement for other rules, such as farthest or arbitrary insertion. Lemma 1 is reusable on its own: it converts "every node carries a charge bounded by half the optimum and by its distance to other nodes" into a logarithmic bound, and the same lemma yields the nearest neighbor bound of Theorem 1.

Formalizing it. The theorem has been proved since 1977; the work here is a machine-checked proof of the known argument together with a reusable library for subtours, insertion and insertion costs. The companion nearest neighbor bound (Theorem 1) is already on the platform as SupplyChainTheory.nearest_neighbor_bound (proved), and nearest insertion with constant 2 as SupplyChainTheory.nearest_insertion_bound; neither covers arbitrary insertion methods or states Lemma 1 separately.

Difficulty

The per-step facts are local: each insertion is cheap relative to a node already present (Lemma 2) and relative to OPTIMAL (3.12). The obvious way to combine them, adding up $n-1$ costs each at most OPTIMAL, gives only the ratio $n-1$ . The logarithm comes from a global counting argument over all nodes simultaneously (Lemma 1), in which OPTIMAL is compared with tours on nested subsets of nodes of doubling size, and the per-node charges must be matched against the edges of those tours. Formally, the delicate parts are the bookkeeping of subtours as they grow (that every earlier node lies on the current subtour, and that the insertion cost equals the length increase), the shortcutting of a tour to an arbitrary subset, and the ceiling-of-logarithm arithmetic.

Formalization scope

Nodes are Fin n; a tour of all nodes is a permutation τ : Equiv.Perm (Fin n), and OPTIMAL is the minimum of the tour length over the finite, nonempty set of permutations. Subtours are duplicate-free lists of nodes, with closed length $d(x_0,x_1)+\dots+d(x_{m-1},x_0)$ . TOUR $(T,k)$ is encoded as inserting $k$ at a list position whose resulting length is minimal among all positions; inserting at a position removes exactly one edge of $T$ and raises the length by exactly $d(x,k)+d(k,y)-d(x,y)$ , so this is the paper's rule, with every tie-breaking allowed. COST is the minimum length increase over positions. The paper's 1-based subtour index is kept ( $T_1=[a_0]$ , $T_n$ final). $\lceil\lg n\rceil$ is Nat.clog 2 n. All quantities are real.

Conventions and deviations, each disclosed in the item statements:

The distance satisfies $d(i,i)=0$ , a normalization not in the paper; a loop never enters any length.
Ratios are multiplied out ( $\mathrm{INSERT}\le c\cdot\mathrm{OPTIMAL}$ ), so the paper's exclusion of the identically zero distance (1.1) is not needed.
Condition a) of Lemma 1 is required for distinct nodes only. The page says "for all nodes $p$ and $q$ ", which for $p=q$ would force every $l_p\le 0$ and make the lemma inapplicable in the proof of Theorem 3; the proof uses the condition only on edges of a tour.
(2.2) is stated for every subset of the nodes and every tour, which is what the shortcut argument shows; the paper applies it to one specific subset and an optimal tour.
(2.1) uses 0-based node labels, so its range $k+1,\dots,\min(2k,n)$ becomes $k,\dots,\min(2k,n)-1$ .

The goal quantifies over every run: any choice of the inserted nodes $a_i$ and any minimizing insertion position. Adding a selection rule (nearest, cheapest) or fixing a tie-breaking would state a weaker, different theorem; restricting to instances with OPTIMAL $=0$ or to a fixed small $n$ would trivialize it.

Reusable beyond this mission: the subtour and insertion library (closed length of a list, TOUR, COST, insertion runs) and Lemma 1, which also yields Theorem 1. Contributions welcome: proofs of the milestones, general lemmas about the closed length of List.insertIdx and of filtered lists, and a proof of Theorem 1 from this mission's Lemma 1.

Selected references

D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM Journal on Computing 6(3):563–581, 1977. https://doi.org/10.1137/0206041
V. Bafna, B. Kalyanasundaram, K. Pruhs, Not all insertion methods yield constant approximate tours in the Euclidean plane, Theoretical Computer Science 125(2):345–353, 1994.

10 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Robust Mean-Covariance Solutions for Stochastic Optimization I: The General Projection Property of Mean-Covariance Distribution ClassesResearch Paper

Motivation

In robust stochastic optimization a decision maker chooses a decision $x$ whose outcome depends on a random vector $\mathbf R$ , but knows only the first two moments of $\mathbf R$ : its mean vector $\mu$ and its covariance matrix $\Sigma$ . The decision is evaluated by its worst-case expected utility over every distribution consistent with those moments. This model is standard in portfolio selection, where estimated means and covariances are the usual inputs, and in pricing and inventory problems with mean-variance information. It goes back to Scarf's min-max newsvendor (1958) and the Chebyshev-type moment bounds of Bertsimas and Popescu (2005).

For a linear outcome $x'\mathbf R$ , such as the return of a portfolio with weights $x$ , the robust objective is

U(x) = \min_{\mathbf R \sim (\mu,\Sigma)} E[u(x'\mathbf R)],

an optimization over an infinite-dimensional set of $n$ -variate distributions. Popescu (2007) showed that this problem depends on $\mu$ and $\Sigma$ only through the scalar mean $\mu_x = x'\mu$ and variance $\sigma_x^2 = x'\Sigma x$ . The multivariate robust problem then reduces to a univariate moment problem, and for many utilities to a parametric quadratic program. The reduction rests on one structural fact, the general projection property, which this mission formalizes.

Setting

Fix a dimension $n$ . A law on $\mathbb R^n$ is a Borel probability measure on $\mathbb R^n$ . For a vector $\mu \in \mathbb R^n$ and a real $n\times n$ matrix $\Sigma$ , the mean-covariance class $\mathbb M^n_{(\mu,\Sigma)}$ is the set of laws $P$ under which every coordinate $R_i$ has a finite second moment and

\int R_i\,dP(R) = \mu_i, \qquad \int (R_i-\mu_i)(R_j-\mu_j)\,dP(R) = \Sigma_{ij} \qquad (1\le i,j\le n).

Writing $\mathbf R \sim (\mu,\Sigma)$ means that the law of $\mathbf R$ lies in $\mathbb M^n_{(\mu,\Sigma)}$ . For $n=1$ the superscript is dropped: for real $m$ and $v$ , $\mathbb M_{(m,v)}$ is the set of laws on $\mathbb R$ with finite second moment, mean $m$ and variance $v$ .

For a vector $x \in \mathbb R^n$ , the $x$ -projection sends the law $P$ of $\mathbf R$ to the law of the scalar $\mathbf r = x'\mathbf R$ , that is, to the pushforward of $P$ under $R \mapsto x'R$ . Write $\mu_x = x'\mu$ and $\sigma_x^2 = x'\Sigma x$ . The matrix $\Sigma$ is positive semidefinite, $\Sigma \succeq 0$ , when $x'\Sigma x \ge 0$ for all $x$ (and $\Sigma$ is symmetric); $\Sigma^{1/2}$ denotes its positive semidefinite square root.

Formalization targets

Goal: Theorem 1 (General Projection Property)

For every $\mu \in \mathbb R^n$ , every $\Sigma \succeq 0$ and every nonzero $x \in \mathbb R^n$ , the $x$ -projection maps $\mathbb M^n_{(\mu,\Sigma)}$ into and onto $\mathbb M_{(\mu_x,\sigma_x^2)}$ :

\bigl\{\, \text{law of } x'\mathbf R \;:\; \mathbf R \sim (\mu,\Sigma) \bigr\} \;=\; \mathbb M_{(x'\mu,\; x'\Sigma x)}.

The "into" half says every projected law has the right mean and variance. The "onto" half says that every univariate law with mean $\mu_x$ and variance $\sigma_x^2$ , however heavy-tailed or irregular, is the law of $x'\mathbf R$ for some $\mathbf R \sim (\mu,\Sigma)$ . The degenerate case $x'\Sigma x = 0$ is included.

Milestones

The into half (§2.1, justification of (4)): $x'\mathbf R$ has mean $x'\mu$ and variance $x'\Sigma x$ .
The degenerate case: if $x'\Sigma x = 0$ then $x'\mathbf R = x'\mu$ almost surely.
Standardization: if $\mathbf r \sim (m, v)$ with $v > 0$ , then $v^{-1/2}(\mathbf r - m) \sim (0,1)$ .
Normalization: for $x'\Sigma x > 0$ , the vector $y = (x'\Sigma x)^{-1/2}\Sigma^{1/2}x$ satisfies $y'y = 1$ .
Isotropic lift: if $y'y = 1$ and $\mathbf z \sim (0,1)$ , there is $\mathbf Z \sim (0, I_n)$ with $y'\mathbf Z$ distributed as $\mathbf z$ .
Affine image: if $\mathbf Z \sim (0,I_n)$ then $\mu + \Sigma^{1/2}\mathbf Z \sim (\mu,\Sigma)$ , and $x'(\mu + \Sigma^{1/2}Z) = x'\mu + (x'\Sigma x)^{1/2}\,y'Z$ for every $Z$ .

Significance

The result. Theorem 1 immediately yields Proposition 1 of the paper: for every objective $u$ ,

\min_{\mathbf R\sim(\mu,\Sigma)} E[u(x'\mathbf R)] = \min_{\mathbf r\sim(\mu_x,\sigma_x^2)} E[u(\mathbf r)],

with minima in the wide sense of infima. The robust objective is therefore a function of $(\mu_x, \sigma_x)$ alone, which makes every robust mean-covariance problem with a linear outcome a bicriteria mean-variance problem. The paper's later results use this: the two-point and one-point support properties, the parametric quadratic programming solution, and the portfolio applications (bonus schemes, value at risk). The projection property holds with no assumption on $u$ , so it serves non-concave, discontinuous and quantile-based objectives alike.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. The mission produces a formal definition of mean-covariance classes that treats integrability honestly, a proof of the projection property, and through it a formally verified reduction of multivariate moment-robust problems to univariate ones. The paper's own construction of the lifted vector has a gap (see Difficulty), so a formal proof also records a corrected argument.

Difficulty

The into half is a computation with linearity of expectation. The difficulty is entirely in the onto half. Given an arbitrary univariate law with prescribed mean and variance, one must build an $n$ -variate law with a prescribed full covariance matrix whose one-dimensional marginal in direction $x$ is exactly the given law. This is a coupling problem: the obvious approach, taking independent coordinates, fixes the marginal in direction $x$ as a convolution and cannot reproduce an arbitrary target. Taking $\mathbf R$ supported on the line through $\mu$ in a single direction reproduces the target law but has a rank-one covariance and fails whenever $\Sigma$ has rank above one.

The paper's appendix constructs the lift through conditional distributions of the remaining coordinates given the projected one. As printed, the conditional second-moment requirement it imposes cannot hold for unbounded targets, so that argument does not go through verbatim. The milestone for the lift states only the claim, not the printed construction.

The integrability bookkeeping is real work: every intermediate law must be shown to have finite second moments before its moments can be computed.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with its Borel σ-algebra; $x'R$ is the inner product $\langle x, R\rangle$ ; $x'\Sigma x$ is x.ofLp ⬝ᵥ S *ᵥ x.ofLp, where the matrix $\Sigma$ is named S (the symbol Σ is reserved in Lean).
Laws are probability measures. Both classes require finite second moments (MemLp … 2), so that means and covariances are genuine integrals, not the default value $0$ that Lean assigns to non-integrable functions. The univariate class is parametrized by the variance $v = \sigma^2$ , not by $\sigma$ .
The projection is the pushforward P.map (fun R => ⟪x, R⟫) under a continuous map. "Pathwise" identities in the paper become equalities of pushforward laws, or pointwise algebraic identities.
$\Sigma^{1/2}$ is CFC.sqrt S, acting through Matrix.toEuclideanCLM, as in Mathlib's multivariateGaussian.
The goal is stated as Set.MapsTo ∧ Set.SurjOn with both classes explicit. Its only hypotheses are $\Sigma \succeq 0$ and $x \ne 0$ , as in the paper. No bound on $n$ , no invertibility of $\Sigma$ and no positivity of $x'\Sigma x$ is assumed. Restricting the target to Gaussian, bounded or finitely supported laws, or dropping the finite-second-moment clause (which would admit Cauchy laws as "mean 0, variance 0"), would trivialize or change the theorem and is ruled out.
Milestones 3, 4 and 6 assume $x'\Sigma x > 0$ (or $v > 0$ ), the case the proof treats after its first sentence; milestone 2 covers the complementary case.

Needed infrastructure: moments of pushforwards under linear and affine maps, a covariance calculus for coordinates of random vectors, and a coupling that realizes the isotropic lift. Mathlib's multivariateGaussian, stdGaussian and CFC.sqrt are available. A reusable lemma "the covariance of $A\mathbf Z + b$ is $A\,\mathrm{Cov}(\mathbf Z)A'$ " would serve beyond this mission. Related platform work on moment-based ambiguity sets: Wasserstein Distributionally Robust Optimization II. Contributions of any milestone, and alternative proofs of the lift, are welcome.

Selected references

I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
D. Bertsimas, I. Popescu, Optimal Inequalities in Probability Theory: A Convex Optimization Approach, SIAM Journal on Optimization 15(3):780–804, 2005. https://doi.org/10.1137/S1052623401399903
H. Scarf, A Min-Max Solution of an Inventory Problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
W. W. Rogosinski, Moments of Non-Negative Mass, Proceedings of the Royal Society A 245:1–27, 1958. https://doi.org/10.1098/rspa.1958.0062

10 thms2 active usersReviewed

Completed

Combinatorics Dynamic Programming Theoretical Computer Science·Captain: mikedeng1

A Faster Algorithm Computing String Edit Distances 1: for a finite alphabet and discrete costs, the block algorithm (Algorithms Y and Z) computes the edit distance from a finite tableResearch Paper

Motivation

The edit distance between two strings is the least total cost of a sequence of single-character insertions, deletions and replacements turning one string into the other. It is the basic similarity measure of spelling correction, file comparison and biological sequence alignment. Wagner and Fischer (JACM 1974) showed that it can be computed by filling a $(|A|+1) \times (|B|+1)$ matrix in $O(|A|\cdot|B|)$ time. Masek and Paterson (J. Comput. System Sci. 1980) gave the first asymptotic improvement: for a finite alphabet and edit costs that are integral multiples of a common constant, the edit distance can be computed in time $O(|A|\cdot|B|/\max(1, |B|/\log|A|))$ , that is $O(n^2/\log n)$ for two strings of length $n$ .

Timeline:

1970: Arlazarov, Dinic, Kronrod and Faradzev compute transitive closures by precomputing all small submatrices, the "four Russians" technique that Masek and Paterson adapt.
1974: Wagner and Fischer give the matrix-filling algorithm, with the first row and column of the matrix and the three-term recurrence for its interior (Theorems 1 and 2 of Masek–Paterson, cited from them).
1980: Masek and Paterson apply the four-Russians technique to the edit matrix, working with differences of adjacent entries, and show that the restriction to discrete costs cannot simply be dropped (their Section 4, the subject of the second mission of this series).
2015: Backurs and Indyk (arXiv:1412.0348) show that a strongly subquadratic algorithm would refute the Strong Exponential Time Hypothesis, so a logarithmic-factor speed-up of this kind is close to the best one can expect.

Setting

Let $\Sigma$ be an alphabet and $\lambda$ the null string. For a string $A$ , $|A|$ is its length, $A_n$ its $n$ -th character, $A^{i,j} = A_i \cdots A_j$ and $A^i = A^{1,i}$ , with $A^0 = \lambda$ .

An edit operation $a \to b$ is a pair $(a, b) \ne (\lambda, \lambda)$ of strings of length at most one: a replacement ( $a, b \ne \lambda$ , possibly $a = b$ ), a deletion ( $b = \lambda$ ) or an insertion ( $a = \lambda$ ). $B$ results from $A$ via $a \to b$ if $A = \sigma a \tau$ and $B = \sigma b \tau$ . An edit sequence $S = s_1, \dots, s_m$ takes $A$ to $B$ if there are strings $A = C_0, C_1, \dots, C_m = B$ with $C_{i-1} \to C_i$ via $s_i$ . A cost function $\gamma$ assigns a nonnegative real to every edit operation, $\gamma(S) = \sum_i \gamma(s_i)$ , and

\delta(\gamma, A, B) = \min\{\gamma(S) \mid S \text{ takes } A \text{ to } B\}.

Write $R_{a,b} = \gamma(a \to b)$ , $D_a = \gamma(a \to \lambda)$ , $I_a = \gamma(\lambda \to a)$ , and $\delta_{i,j} = \delta(\gamma, A^i, B^j)$ for the entries of the edit matrix. The cost function is normalized if $\gamma(a \to b) = \delta(\gamma, a, b)$ for every edit operation.

A step is a difference of two adjacent matrix entries, $\delta_{i,j} - \delta_{i-1,j}$ (vertical) or $\delta_{i,j} - \delta_{i,j-1}$ (horizontal). The cost set is $\Omega = \{D_a\} \cup \{I_a\} \cup \{R_{a,b}\}$ , and $\Omega$ is discrete if every element of $\Omega$ is an integral multiple of one constant $r > 0$ .

Algorithm Y takes two strings $C, D$ of length $m$ and two step vectors $R, S$ of length $m$ (the left column and top row of an $m \times m$ block) and fills a matrix $T$ of vertical steps and $U$ of horizontal steps by the recurrence of Corollary 1, returning the right column $R'$ and bottom row $S'$ . Algorithm Z cuts $A$ and $B$ into blocks of length $m$ , starts from the deletion costs of $A$ and the insertion costs of $B$ , obtains the steps of each block from Algorithm Y's output ("Fetch"), and returns the sum of the steps along the left column and the bottom row.

Formalization targets

Goal: correctness from a string-independent finite table

For a finite alphabet and a nonnegative, normalized cost function with discrete $\Omega$ , there is a finite set $T \subset \mathbb{R}$ such that for all $m \ge 1$ and all $A, B$ with $m \mid |A|$ , $m \mid |B|$ ,

\mathrm{cost}_{Z}(\gamma, m, A, B) = \delta(\gamma, A, B), \qquad \text{every entry of every } P(i,j), Q(i,j) \text{ lies in } T.

$T$ is fixed before $m$ , $A$ and $B$ . The second clause says that Algorithm Y's table need only range over $\Sigma^m \times \Sigma^m \times T^m \times T^m$ , whose size does not depend on the strings; this is what the running-time bound rests on.

Milestones

Theorem 1 [Wagner–Fischer]: $\delta_{0,0} = 0$ , $\delta_{i,0} = \sum_{r \le i} D_{A_r}$ , $\delta_{0,j} = \sum_{r \le j} I_{B_r}$ .
Theorem 2 [Wagner–Fischer]: $\delta_{i,j} = \min(\delta_{i-1,j-1} + R_{A_i,B_j}, \delta_{i-1,j} + D_{A_i}, \delta_{i,j-1} + I_{B_j})$ .
Corollary 1: the same recurrence written in terms of steps.
Algorithm Y returns the final step vectors of every $m \times m$ submatrix from its initial step vectors and strings (Section 2.1).
Lemma 3: $-I \le \delta_{i,j} - \delta_{i-1,j} \le D$ and $-D \le \delta_{i,j} - \delta_{i,j-1} \le I$ .
Lemma 4: if $\Omega$ is discrete, the set of possible steps is finite.

Significance

The result was the first algorithm for edit distance faster than quadratic, and its method (tabulate every possible small block of a dynamic program, described by differences rather than values) became the standard way of shaving a logarithmic factor from string dynamic programs. The discreteness hypothesis is where the method's power ends: Section 4 of the paper shows that with costs $1$ and $\pi$ the number of distinct steps grows without bound.

The results are proved in the paper; none of them is formalized. The Mathlib revision of this mission contains no edit-distance module. A formalization produces a definition of edit distance as a minimum over edit sequences, a machine-checked proof of the Wagner–Fischer recurrence for that definition under the normalization the paper assumes, and a checked proof that the four-Russians block assembly is correct and draws on a finite, string-independent table.

Difficulty

The hardest step is Theorem 2 for $\delta$ defined as a minimum over arbitrary edit sequences. An edit sequence may insert a character and later replace or delete it, or edit the same position many times, so the edit matrix's three-term recurrence does not follow by looking at the last operation. The upper bound is direct; the lower bound needs a normal form for edit sequences, and it fails without normalization: with $R_{a,c} = 10$ , $R_{a,b} = R_{b,c} = 1$ and all insertions and deletions costing $100$ , $\delta(\gamma, a, c) = 2$ while the recurrence gives $10$ .

The goal is then an induction over blocks that must keep track of which matrix entries each block's input and output vectors represent, with block boundaries at multiples of $m$ and the first row and column handled by Theorem 1.

Formalization scope

Strings are List α; characters are 1-based in all statements, as in the paper ( $A_i$ is A[i-1]). An edit operation is a structure with two Option α fields, not both none. $\delta$ is sInf of the set of costs of edit sequences taking $A$ to $B$ (nonempty, and bounded below for $\gamma \ge 0$ ). Costs are real-valued with an explicit nonnegativity hypothesis. Normalization is a hypothesis on Theorems 1, 2, Corollary 1, the Algorithm Y lemma and the goal; Lemmas 3 and 4 hold without it. The finite alphabet is [Fintype α] on Lemma 4 and the goal; Lemma 3 is stated for arbitrary upper bounds $I \ge I_a$ , $D \ge D_a$ , which implies the paper's version with maxima. The paper's standing assumption $|A| \ge |B|$ serves only the running time and is dropped. Step vectors are functions on Fin m.

Pinned statements. The paper states a running time $O(|A|\cdot|B|/\max(1,|B|/\log|A|))$ on a logarithmic-cost RAM; the goal formalizes the two facts that bound rests on, correctness and a finite table domain fixed before the strings. The RAM model, operation counts, the choice $m = \lfloor \log_k |A| \rfloor$ , the padding reduction for $m \nmid |A|$ , and the edit-path recovery of Section 2.3 are not formalized. Algorithm Y's result is a function (blockY); the Store/Fetch memory is not modelled.

The edit distance must stay the minimum over edit sequences: defining it by the Wagner–Fischer recurrence would make Theorems 1 and 2 true by definition and reduce the goal to a comparison of two recurrences. Algorithms Y and Z are transcribed from the pseudo-code and never refer to $\delta$ .

Useful beyond this mission: the §1.1 definitions and Theorems 1–2 are a general edit-distance library (the second mission of this series defines the same objects). Contributions of lemmas about normal forms of edit sequences, the triangle inequality for $\delta$ , and attainment of the minimum are welcome.

Selected references

W. J. Masek, M. S. Paterson, A Faster Algorithm Computing String Edit Distances, J. Comput. System Sci. 20 (1980), 18–31. https://doi.org/10.1016/0022-0000(80)90002-1
R. A. Wagner, M. J. Fischer, The String-to-String Correction Problem, J. ACM 21 (1974), 168–173. https://doi.org/10.1145/321796.321811
V. L. Arlazarov, E. A. Dinic, M. A. Kronrod, I. A. Faradzev, On Economical Construction of the Transitive Closure of an Oriented Graph, Soviet Math. Dokl. 11 (1970), 1209–1210.
A. Backurs, P. Indyk, Edit Distance Cannot Be Computed in Strongly Subquadratic Time (unless SETH is false), STOC 2015. https://arxiv.org/abs/1412.0348

10 thms2 active usersReviewed

Completed

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

Path-Finding Methods for Linear Programming I: Centering with Weights on the Weighted Central PathResearch Paper

Motivation

Interior point methods solve a linear program by following a central path: a curve of minimizers of a penalized objective that trades off cost against distance from the boundary of the feasible region. The classical analysis of path following with the logarithmic barrier needs $O(\sqrt{m}\,L)$ iterations for a program with $m$ constraints, where $L$ is the bit complexity of the input (Renegar 1988). For programs with many more constraints than variables, $m$ can be far larger than the dimension $n$ or the rank of the constraint matrix, and the $\sqrt m$ factor is then the bottleneck.

Lee and Sidford (FOCS 2014) reduce the iteration count to $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ by following a weighted central path in which each constraint carries its own positive weight, and the weights are re-computed as the algorithm moves. Their improved maximum-flow algorithm is an application of the same method.

Timeline. Karmarkar (1984) gave the first polynomial-time interior point method for linear programming. Renegar (1988) showed that path following with the logarithmic barrier needs $O(\sqrt m L)$ iterations. Nesterov and Nemirovskii (1994) showed that a universal self-concordant barrier yields $O(\sqrt n L)$ iterations, but that barrier is not known to be efficiently computable. Lee and Sidford (2014) achieved $\tilde O(\sqrt{\mathrm{rank}(A)}L)$ iterations, each reducible to $\tilde O(1)$ linear-system solves.

This mission covers the first half of that framework (§IV of the paper): the weighted central path, the weighted Newton step, and the centering theorem that shows a single step followed by re-weighting makes constant-factor progress.

Setting

Let $A\in\mathbb R^{m\times n}$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ , and consider the linear program

\min_{x\in\mathbb R^n:\ Ax\ge b} c^Tx .

The slack of a point $x$ is $s(x)=Ax-b$ , and the interior is $S^0=\{x : Ax>b\}$ , the points with all slacks strictly positive. For a path parameter $t$ and a vector of positive weights $w\in\mathbb R^m_{>0}$ , the weighted penalized objective is

f_t(x,w)=t\,c^Tx-\sum_{i=1}^m w_i\log s(x)_i .

A pair $(x,w)$ is feasible if $x\in S^0$ and $w>0$ .

Write $S_x=\mathrm{diag}(s(x))$ , $W=\mathrm{diag}(w)$ and $\|v\|_M=\sqrt{v^TMv}$ . The Newton step and the centrality are

\vec h_t(x,w)=\big(A^TS_x^{-1}WS_x^{-1}A\big)^{-1}\big(tc-A^TS_x^{-1}w\big),\qquad \delta_t(x,w)=\big\|\vec h_t(x,w)\big\|_{A^TS_x^{-1}WS_x^{-1}A}.

The matrix $A^TS_x^{-1}WS_x^{-1}A$ is the Hessian of $f_t$ in $x$ , and $tc-A^TS_x^{-1}w$ is its gradient; $\delta_t(x,w)=0$ exactly when $x$ minimizes $f_t(\cdot,w)$ .

For slacks $s$ and weights $w$ the projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A(A^TS^{-1}WS^{-1}A)^{-1}A^TS^{-1}W^{1/2}$ and the slack sensitivity is

\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\vec 1_i\big\|_{P_{S^{-1}A}(w)} .

A weight function (Definition 4) is a differentiable map $\vec g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ from slacks to weights with constants $c_1$ (size, a bound on $\|\vec g(s)\|_1$ ), $c_\gamma\ge1$ (slack sensitivity, $\gamma(s,\vec g(s))\le c_\gamma$ ), $c_r\ge1$ (step consistency, two inequalities on the Jacobian $G'(s)$ of $\vec g$ that hold for every $r\ge c_r$ ), and uniformity $\|\vec g(s)\|_\infty\le2$ .

Formalization targets

Goal: Theorem 5 (Centering with Weights), §IV.C

Let $\vec g$ be a weight function for $A$ with constants $c_1,c_\gamma,c_r$ , let $x^{(old)}\in S^0$ , $s^{(old)}=s(x^{(old)})$ , and

x^{(new)}=x^{(old)}-\frac{1}{1+c_r}\,\vec h_t\big(x^{(old)},\vec g(s^{(old)})\big).

If $\delta_t(x^{(old)},\vec g(s^{(old)}))\le\frac{1}{100c_\gamma c_r^2}$ , then $x^{(new)}\in S^0$ and

\delta_t\big(x^{(new)},\vec g(s^{(new)})\big)\le\Big(1-\frac{1}{4c_r}\Big)\delta_t\big(x^{(old)},\vec g(s^{(old)})\big).

The theorem is stated for every weight function, not for the specific one constructed in §V of the paper; that construction is the subject of a separate mission.

Milestone: Lemma 3 (Split Newton Step), §IV.B

For feasible $(x^{(old)},w^{(old)})$ and $r\ge0$ , the split step $x^{(new)}=x^{(old)}-\frac1{1+r}\vec h_t$ , $w^{(new)}=w^{(old)}+\frac r{1+r}W_{(old)}S_{(old)}^{-1}A\vec h_t$ satisfies, whenever $\delta_t\le\frac1{8\gamma}$ ,

\delta_t\big(x^{(new)},w^{(new)}\big)\le\frac{2}{1+r}\,\gamma\,\delta_t^2,

with $\gamma=\gamma(s(x^{(old)}),w^{(old)})$ , and the new pair is feasible.

Milestone: Lemma 1, §IV.B

For feasible $(x,w)$ and $\alpha,t\ge0$ :

\delta_{(1+\alpha)t}(x,w)\le(1+\alpha)\delta_t(x,w)+\alpha\sqrt{\|w\|_1}.

Significance

Theorem 5 is the centering half of the weighted path-following method. Combined with Lemma 1, it shows that the path parameter can be doubled, while staying close to the weighted central path, in a number of steps of the form (5) controlled by $c_\gamma$ , $c_r$ and $\sqrt{c_1}$ . The paper then constructs (§V, Theorem 1) a weight function with $c_1=2\,\mathrm{rank}(A)$ , $c_\gamma=2$ and $c_r$ logarithmic in $m/\mathrm{rank}(A)$ , which yields the $\tilde O(\sqrt{\mathrm{rank}(A)})$ iteration bound. The theorem isolates exactly which properties of a weighting scheme are needed, so it applies to any weight function satisfying Definition 4.

The FOCS extended abstract states these results without proofs; the proofs are in the arXiv full version (arXiv:1312.6677). The results are proved on paper. No machine-checked formalization of weighted path following, or of the Lee–Sidford framework, is known. A formal proof would check the constants $\frac1{100}$ , $\frac1{4}$ , $\frac18$ and $\frac2{1+r}$ as stated in the extended abstract, and would produce reusable Lean infrastructure for Newton steps of barrier functions with explicit matrix formulas.

Difficulty

The standard analysis of Newton's method on a self-concordant barrier gives quadratic convergence of centrality for a fixed barrier. Here the barrier changes during the step: the weights are reset to $\vec g(s(x^{(new)}))$ , so the new centrality is measured with respect to a different Hessian and a different gradient. The obvious argument, analysing the step at fixed weights and then treating the re-weighting as a small perturbation, does not give a contraction factor independent of $m$ : without control of how $\vec g$ reacts to changes in the slacks, the re-weighting can undo the progress of the step. The step-consistency conditions of Definition 4 are the only hypotheses that control this reaction, and they are pointwise bounds on the Jacobian of $\vec g$ , while the step moves the slacks by a finite amount.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and products are Matrix.mulVec and dotProduct. $S^{-1}$ is the diagonal matrix of reciprocals, $W^{\pm1/2}$ the diagonal matrices of $\sqrt{w_i}^{\pm1}$ , and $\|v\|_M=\sqrt{v^TMv}$ . The Newton step and centrality are defined by the explicit formulas (3) and (4), not by derivatives of $f_t$ ; the centrality uses the Hessian-norm form of (4). The Jacobian $G'(s)$ is the Fréchet derivative fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm.

Conventions fixed where the paper is silent:

Full column rank. Every theorem assumes A.rank = n. The paper uses $(A^TS_x^{-1}WS_x^{-1}A)^{-1}$ without comment; the inverse exists for positive slacks and weights exactly when $A$ has full column rank. Lean's matrix inverse is $0$ on singular matrices, which would make $\vec h_t$ , $\delta_t$ and $\gamma$ vanish and every statement trivially true; the rank hypothesis rules this trivializing reading out.
Size as an upper bound. Definition 4's " $c_1(\vec g)=\|\vec g(s)\|_1$ " is read as $\|\vec g(s)\|_1\le c_1$ for all $s>0$ (the paper's own weight function reports a $c_1$ above its $\ell_1$ norm). $c_1$ does not enter Theorem 5.
Operator norm. Step consistency's first bullet is written as $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ for all $y$ .
Lemma 3's $r$ ranges over $r\ge0$ , and $\gamma(x,w)$ means $\gamma(s(x),w)$ .
Feasibility of the new point is part of the conclusion of Lemma 3 and Theorem 5, since the page's conclusion evaluates quantities defined only on the interior.
Maximum over $[m]$ is a supremum over Fin m (attained for $m\ge1$ , equal to $0$ for $m=0$ ).
The path parameter $t$ is unrestricted in Theorem 5 and Lemma 3, as on the page; Lemma 1 assumes $t\ge0$ as the page does.

A complete development needs basic facts about weighted norms and the projection matrix $P_{S^{-1}A}(w)$ , spectral comparison of the matrices $A^TS^{-1}WS^{-1}A$ for nearby slacks and weights, and calculus for vector-valued maps on the positive orthant. The weighted-norm and projection-matrix material is reusable for any interior point analysis. Proofs of the milestones, alternative arguments, and sharper constants are welcome.

Selected references

Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv:1312.6677, 2013. https://arxiv.org/abs/1312.6677
J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40, 1988, pp. 59–93. https://doi.org/10.1007/BF01580724
N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, pp. 373–395. https://doi.org/10.1007/BF02579150
Y. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

6 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Critical-Path Planning and Scheduling II: The Project Cost Curve Is Non-Increasing, Piecewise Linear and ConvexResearch Paper

Motivation

A large engineering or construction project is a set of jobs with precedence constraints, and most jobs can be finished faster at a higher cost (overtime, more crews, faster equipment). Planners want to know, for every possible project duration, the cheapest way to meet it. The resulting trade-off between duration and direct cost is what management compares with overhead, penalties and market losses when it picks a schedule.

J. E. Kelley, Jr. and M. R. Walker introduced the critical-path method (CPM) in 1959, from work at du Pont and Remington Rand (Kelley and Walker 1959). Alongside the critical-path computation, they modelled each job's cost as a linear function of its duration and posed the choice of durations as a parametric linear program. They stated that its optimal value, as a function of the project duration $\lambda$ , is a non-increasing, piecewise linear, convex function, which they called the project cost curve. The 1959 paper gives no proof and defers the detailed development to a separate paper (Kelley 1961). Fulkerson (1961) gave a network-flow algorithm that computes the curve. Time–cost trade-off analysis ("crashing") has been a standard part of project management since then.

Setting

A project network has events labelled $0, 1, \dots, n$ with $n \ge 1$ . Event $0$ is the origin and event $n$ the terminus. A finite set $P$ of jobs is given, each an ordered pair $(i,j)$ : an arrow from event $i$ to event $j$ . As in the paper, labels increase along arrows ( $i < j$ for every $(i,j) \in P$ ), the origin precedes every event, and the terminus follows every event.

For job durations $y = (y_{ij})$ , the earliest event times are given by recursion (1):

t_0^{(0)} = 0,\qquad t_j^{(0)} = \max\,[\,y_{ij} + t_i^{(0)} \mid i<j,\ (i,j)\in P\,],\quad 1\le j\le n,

and $t_n^{(0)}(y)$ is the earliest project completion time.

Each job has a crash duration $d_{ij}$ and a normal duration $D_{ij}$ with $0 \le d_{ij} \le D_{ij}$ , and a linear job cost $a_{ij}y_{ij} + b_{ij}$ with $a_{ij} \le 0$ , $b_{ij} \ge 0$ . The project (direct) cost is

\text{(7)}\qquad \sum_{(i,j)\in P} (a_{ij} y_{ij} + b_{ij}).

A schedule for $\lambda$ is a pair $(y,t)$ with

\text{(5)}\ d_{ij}\le y_{ij}\le D_{ij},\qquad \text{(8)}\ y_{ij}\le t_j-t_i\quad ((i,j)\in P),\qquad \text{(9)}\ t_0=0,\ t_n=\lambda.

Let $\Lambda$ be the set of $\lambda$ for which a schedule exists. For $\lambda \in \Lambda$ the project cost curve $C(\lambda)$ is the minimum of (7) over schedules for $\lambda$ . Write $\lambda_c = t_n^{(0)}(d)$ (all jobs crashed) and $\lambda_N = t_n^{(0)}(D)$ (all jobs normal).

Formalization targets

Goal: the shape of the project cost curve (p. 165)

C \text{ is non-increasing on } \Lambda,\qquad C \text{ is piecewise linear on } \Lambda,\qquad C \text{ is convex on } \Lambda .

Piecewise linear means finitely many breakpoints $\beta_0<\dots<\beta_m$ with $\Lambda\subseteq[\beta_0,\infty)$ , and affine pieces on $\Lambda\cap[\beta_k,\beta_{k+1}]$ and on $\Lambda\cap[\beta_m,\infty)$ . The goal fixes no breakpoints or slopes. It asserts only the shape the paper claims, on the whole of $\Lambda$ .

Milestones

Feasible range (p. 165, "until no further reduction in project completion time is possible"): $\Lambda = [\lambda_c, \infty)$ .
Existence of optimal schedules (p. 165, the linear program (8), (9)): for every $\lambda\in\Lambda$ the minimum of (7) is attained.
All-normal solution (p. 165): $(D, t^{(0)}(D))$ is a minimum cost schedule for $\lambda = \lambda_N$ .
$\lambda$ is the earliest completion time (p. 165, "within the limits of most interest"): for $\lambda_c\le\lambda\le\lambda_N$ some minimum cost schedule $(y,t)$ for $\lambda$ has $t_n^{(0)}(y)=\lambda$ .

Significance

The cost curve is the output of CPM's cost analysis. Its convexity is what makes the paper's parametric procedure valid: jobs are expedited in order of increasing marginal cost, and the curve is traced from $\lambda_N$ down to $\lambda_c$ one linear piece at a time. Monotonicity justifies reading the curve as a trade-off. Piecewise linearity with finitely many pieces means the whole curve is determined by finitely many characteristic schedules, the vertices plotted in the paper's Fig. 3. The milestones identify the domain of the curve, show that it is well defined, and fix its right end at the all-normal solution.

These facts are classical: they follow from parametric linear programming, and Kelley (1961) and Fulkerson (1961) develop them in detail. No machine-checked proof of them is known. Prove2Me has a related result, LinearOptimization.lp_optimal_cost_convex_in_rhs (Bertsimas–Tsitsiklis, Theorem 5.1): convexity of the optimal cost of a standard-form LP in its right-hand side. It covers convexity only, for a different LP form, and says nothing about monotonicity or finitely many pieces. This mission adds a formal model of CPM's time–cost program and the full three-part shape theorem.

Difficulty

Convexity alone follows from the usual argument: a convex combination of optimal schedules for two durations is a schedule for the combined duration. Monotonicity needs the structure of the network: when $\lambda$ increases, only the constraints (8) on jobs ending at the terminus loosen, because no job leaves the terminus. The hard part is piecewise linearity with finitely many pieces. Convexity does not imply it, and a general result on value functions of linear programs has to be tied to this specific program, whose right-hand side depends on $\lambda$ only through $t_n = \lambda$ . The domain is also unbounded, so the argument must show that the curve is eventually a single affine (in fact constant) piece. It cannot just produce finitely many pieces on a compact interval.

Formalization scope

Events are Fin (n + 1) with origin 0 and terminus Fin.last n, and 1 ≤ n. Jobs are a Finset of ordered pairs, with at most one job per ordered pair. The standing assumptions of pp. 161–162 are fields of ProjectNetwork: labels increase along jobs, and reachability via Relation.ReflTransGen from the origin and to the terminus. Times and durations are real. Job data are functions Fin (n+1) → Fin (n+1) → ℝ, constrained and read only on $P$ . The hypotheses $0\le d_{ij}\le D_{ij}$ , $a_{ij}\le 0$ and $b_{ij}\ge 0$ are fields of JobData. Recursion (1) is earliest, defined by well-founded recursion on the label. It uses a fallback value $0$ for an event without predecessors, which occurs only at the origin. The paper's $\lambda$ is written lam. Constraint (9) fixes $t_n = \lambda$ exactly, and the event times are otherwise unconstrained.

The goal takes $C : \mathbb{R}\to\mathbb{R}$ with the hypothesis that $C(\lambda)$ is the least element of the set of costs of schedules for $\lambda$ , for every $\lambda \in \Lambda$ . All three conclusions are stated on $\Lambda$ only. This rules out the trivializing formalizations:

a junk-valued infimum off $\Lambda$ plays no role;
$C$ is tied to the program, and the hypothesis on $C$ is satisfiable by milestone 2;
piecewise linearity requires finitely many pieces that cover all of $\Lambda$ ;
all three properties are claimed, not convexity alone.

The goal keeps $a_{ij}\le 0$ , as the page does throughout §3, although monotonicity and convexity would hold without it.

Disclosed readings:

Milestone 1 renders "until no further reduction in project completion time is possible" as $\Lambda=[\lambda_c,\infty)$ .
Milestone 4 reads "within the limits of most interest" as $\lambda_c\le\lambda\le\lambda_N$ . It asserts that some optimal schedule has $t_n^{(0)}(y)=\lambda$ . "Every" is false: when all $a_{ij}=0$ , the all-crash durations are optimal for every $\lambda$ .

A complete development needs:

the existence of LP optima under a bounded objective, or a direct compactness argument on the feasible polyhedron;
a parametric-LP or polyhedral argument for finitely many linear pieces;
basic facts on the recursion (1).

The one-variable notion IsPiecewiseLinearOn and the facts on earliest event times can be reused in scheduling missions. Proofs of the milestones, of any of the three goal conjuncts separately, and general lemmas on parametric LP value functions are all welcome.

Not formalized: general piecewise linear convex job costs (deferred by the paper to its references [7], [8]), and the primal–dual procedure itself (a method, not a claim).

Selected references

J. E. Kelley, Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Proc. Eastern Joint IRE-AIEE-ACM Computer Conference, 1959, pp. 160–173. https://doi.org/10.1145/1460299.1460318
J. E. Kelley, Jr., Critical-Path Planning and Scheduling: Mathematical Basis, Operations Research 9(3), 1961, pp. 296–320. https://doi.org/10.1287/opre.9.3.296
D. R. Fulkerson, A Network Flow Computation for Project Cost Curves, Management Science 7(2), 1961, pp. 167–178. https://doi.org/10.1287/mnsc.7.2.167
D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §5.2 (the optimal cost as a function of the right-hand side).

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Incentives in Teams: The Own Profit Incentive Structure Is an Optimal Incentive Structure for a ConglomerateResearch Paper

Motivation

An organization whose members hold private information faces two problems at once. The first is the team problem of Marschak and Radner: choose the rules by which members observe, communicate and decide so as to maximize the expected payoff of the organization as a whole (Marschak–Radner 1972). The second is the incentive problem: a member who is paid by their own results has no reason to follow those rules, and in particular no reason to report truthfully what they have observed. Theodore Groves' Incentives in Teams (Econometrica 41(4), 1973) connected the two. For a decentralized firm in which subunits report to a head, it exhibits compensation rules that make the team-optimal behaviour, truthful messages included, each subunit manager's unique best reply.

The construction is the origin of what is now called the Groves scheme, and with Vickrey's second-price auction (Vickrey 1961) and Clarke's pivot rule (Clarke 1971) it forms the Vickrey–Clarke–Groves (VCG) family of mechanisms.

Timeline:

1961, Vickrey: second-price auctions make truthful bidding a dominant strategy for a single object.
1971, Clarke: pivot payments for public-good decisions with deterministic valuations.
1972, Marschak–Radner: the economic theory of teams, with information and decision structures but a common payoff.
1973, Groves: compensation $C_i^{II}$ based on the head's conditional expectation of the other units' payoffs; Theorem 1 proves optimality in a conglomerate with independent component states and one round of communication.
1977, Green–Laffont: in the complete-information setting, Groves-type payments are the only ones that make truth-telling dominant (Econometrica 45(2)).
1979, d'Aspremont–Gérard-Varet: Bayesian incentive-compatible mechanisms with expected externality payments (J. Public Econ. 11(1)).

The conglomerate model

The organization consists of a head (component $0$ ) and finitely many subunits $i = 1, \dots, n$ . Each component $k$ has its own random component state $s_k \in S_k$ , and the components are independent: the state of the environment $s = (s_0, s_1, \dots, s_n)$ is distributed according to the product law $P(s) = P_0(s_0) \prod_{i} P_i(s_i)$ (Condition S.2).

Every member plays a strategy $\beta_k = (\zeta_k, \gamma_k, \delta_k)$ made of an observation strategy $\zeta_k$ on its own state, a message strategy $\gamma_k$ and a decision strategy $\delta_k$ (Condition S.3). Communication runs only between the head and each subunit, in one exchange: the head observes $\zeta_0(s_0)$ and sends $\gamma_0^i(\zeta_0(s_0))$ to subunit $i$ ; the subunit, with information $y_i(s) = [\zeta_i(s_i), \gamma_0^i(\zeta_0(s_0))]$ , sends back $\gamma_i(y_i(s))$ ; the head's information is $y_0(s) = [\zeta_0(s_0), \{\gamma_i(y_i(s))\}_{i}]$ (3.1). Decisions are $\delta_i(y_i(s))$ and $\delta_0(y_0(s))$ .

The organization payoff is a sum of components (Condition S.4),

\omega_0(\beta, s) = \sum_{i=1}^n v_i[\delta_i(y_i(s)), \delta_0(y_0(s)); s_i] + v_0[\delta_0(y_0(s)), s_0],

and $\bar\omega_0(\beta) = E[\omega_0(\beta, s)]$ . Each $v_i$ accrues directly to subunit $i$ (Condition S.5). Strategy sets $B_0, B_1, \dots, B_n$ are given; $\beta/\beta_i$ denotes $\beta$ with subunit $i$ 's strategy replaced by $\beta_i$ . Two strategies $\beta_i', \beta_i''$ are equivalent if $\bar\omega_0(\beta/\beta_i') = \bar\omega_0(\beta/\beta_i'')$ for every $\beta \in B$ .

Assumption A requires a $\beta^* \in B$ maximizing $\bar\omega_0$ over $B$ such that, for each subunit, $\bar\omega_0(\beta^*) > \bar\omega_0(\beta^*/\beta_i)$ whenever $\beta_i \in B_i$ is not equivalent to $\beta_i^*$ .

An incentive structure $W = \{\omega_i\}$ pays subunit $i$ the amount $\omega_i(\beta, s)$ . The class $\mathscr{J}$ (3.2) consists of those of the form $\omega_i = v_i[\dots] + C_i(y_0(s))$ : own payoff plus a compensation computed from the head's information only. $W$ is optimal (2.6) if $\beta_i^*$ maximizes $\bar\omega_i(\beta^*/\beta_i)$ over $B_i$ , uniquely up to equivalence.

Formalization targets

Goal: Theorem 1 (p. 625)

With $C_i^{II}(y_0) = \sum_{j \ne i} E\big[v_j[\delta_j^*(y_j^*(s)), \delta_0^*(y_0^*(s)); s_j] \,\big|\, y_0^*(s) = y_0\big] - A_i$ , the sum running over all components $j \in \{0, \dots, n\}$ other than $i$ and the expectation taken under $\beta^*$ (3.3), the structure $\omega_i^{II} = v_i[\dots] + C_i^{II}(y_0(s))$ lies in $\mathscr{J}$ and satisfies, for every subunit $i$ and every $\beta_i \in B_i$ ,

\bar\omega_i^{II}(\beta^*/\beta_i) \le \bar\omega_i^{II}(\beta^*), \qquad \text{with strict inequality if } \beta_i \not\equiv \beta_i^*.

It holds for every $\beta^*$ satisfying Assumption A, all strategy sets and all constants $A_i$ .

Milestones

The Appendix Lemma: the sets of states consistent with the head's information under $\beta^*/\beta_i$ and under $\beta^*$ have the same projections onto every component other than $i$ .
The right-hand side of (A.2): the head's conditional expectation factorizes over the independent components.
(A.2) for a subunit $j \ne i$ , and 4. (A.2) for the head's component $j = 0$ : the expected payoff of component $j$ under $\beta^*/\beta_i$ equals the expected value of its conditional expectation.
(A.1): $\bar\omega_i^{II}(\beta^*/\beta_i) + A_i = \bar\omega_0(\beta^*/\beta_i)$ for all $\beta_i \in B_i$ .

Significance

Theorem 1 shows that a head who knows only the messages it receives can nonetheless align every subunit's interest with the organization's, without monitoring decisions or observations. It is an early statement that expected-externality payments make truthful communication an equilibrium of a decentralized organization, and the Bayesian, team-theoretic counterpart of the dominant-strategy results of Vickrey and Clarke. Its structure (own payoff plus a transfer depending only on the others' reported information) is the template later characterized by Green and Laffont and generalized by d'Aspremont and Gérard-Varet.

Theorem 1 is proved in the paper; nothing here is open mathematically. What the mission adds is a machine-checked version with every modelling choice explicit: how information is generated by the message protocol, what the conditional expectation in (3.3) means on events of probability zero, and which equivalence "uniquely" refers to. No machine-checked proof of Theorem 1 is known to the platform. The platform's AGT.vcg_incentive_compatible treats the complete-information, direct-revelation analogue (deterministic valuations, dominant strategies), a different model with a different conclusion.

Difficulty

The tempting argument conditions on the head's information $y_0^*(s) = y_0$ under $\beta^*$ and compares it with the head's information under a deviation. That comparison fails when a deviating subunit sends a message that $\gamma_i^*$ never sends: the conditioning event then has probability zero under $\beta^*$ , and the conditional expectation of (3.3) is not determined by the joint law. A second obstacle is that the head's information under a deviation differs from the information under $\beta^*$ in every coordinate the deviation touches, while the compensation is computed as if $\beta^*$ were played; the statement to be proved compares expectations taken under two different joint strategies, and the one-exchange protocol makes the head's messages, and hence every subunit's information, depend on the head's own state. Treating these dependencies loosely either produces a circular definition of the information functions (as (3.1) is printed) or a statement that fails on events of probability zero.

Formalization scope

Every component state space $S_k$ is a finite type with weights that are nonnegative and sum to one; the joint law is the product of these weights and expectations are finite sums. The paper allows general probability spaces; the finite case covers the whole argument and gives conditional expectations at a point an elementary meaning.
Subunits form a finite index type; the head is a separate component with its own observation, message and decision types. Observation, message and decision spaces are fixed types per component.
Information (3.1) follows the single exchange of messages the paper describes in §4.A (p. 627): the head's message to subunit $i$ is a function of the head's observation. As printed, (3.1) is circular; this protocol is the paper's own resolution.
$C_i^{II}$ is used in factorized form: the head's term conditions only the head's state on the head's observation, and subunit $j$ 's term conditions only $s_j$ on the message $j$ sent. A separate milestone states that this equals the literal conditional expectation of (3.3) whenever the conditioning event has positive probability. The literal elementary quotient takes the value $0$ on null events, and with it Theorem 1 is false (one subunit that can send an unused message suffices); the factorized form is what the Appendix computes. The sum in (3.3) includes the head's component $v_0$ .
Equivalence of strategies is footnote 5's, over all $\beta \in B$ ; optimality includes the strict inequality for non-equivalent deviations. A formalization that replaces equivalence by equality of strategies, fixes $B_i = \{\beta_i^*\}$ , drops the strict inequality, or assumes (A.1) as a hypothesis is not this theorem.
The Lemma carries the added hypothesis that the set $B(s)$ is nonempty; the paper's proof presumes it and the statement is false without it.

Contributions welcome: proofs of the milestones, and reusable finite-probability facts (conditioning on product events, iterated expectation over a coordinate) stated for product weights.

Selected references

T. Groves, Incentives in Teams, Econometrica 41(4):617–631, 1973. https://doi.org/10.2307/1914085
J. Marschak and R. Radner, Economic Theory of Teams, Yale University Press, 1972.
W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16(1):8–37, 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
E. H. Clarke, Multipart Pricing of Public Goods, Public Choice 11:17–33, 1971. https://doi.org/10.1007/BF01726210
J. Green and J.-J. Laffont, Characterization of Satisfactory Mechanisms for the Revelation of Preferences for Public Goods, Econometrica 45(2):427–438, 1977. https://doi.org/10.2307/1911219
C. d'Aspremont and L.-A. Gérard-Varet, Incentives and Incomplete Information, Journal of Public Economics 11(1):25–45, 1979. https://doi.org/10.1016/0047-2727(79)90043-4

7 thms2 active usersReviewed

Completed

Bandit Algorithms Machine Learning Operations Research+1·Captain: mikedeng1

Stochastic Linear Optimization under Bandit Feedback 2: A Regret Lower Bound on the CircleResearch Paper

Motivation

In stochastic linear optimization under bandit feedback a learner repeatedly chooses a point $x_t$ from a compact decision set $D\subset\mathbb R^n$ and observes only the random cost $\ell_t$ of that point, whose mean is $\mu\cdot x_t$ for an unknown vector $\mu$ . The problem models online routing, ad placement and other sequential decisions with linearly structured costs. The quality of a learner is measured by its regret against the best fixed decision.

For the $K$ -armed bandit the achievable regret for a fixed instance is logarithmic in the horizon $T$ (Lai and Robbins 1985; Auer, Cesa-Bianchi and Fischer 2002). Dani, Hayes and Kakade (COLT 2008) showed that for linear costs the picture depends on the geometry of $D$ . Their Theorem 1 gives polylogarithmic regret when the decision set has a positive gap between the best and second-best extreme point (a polytope, for instance), and their Theorem 2 gives $O^*(n\sqrt T)$ regret for every decision set. Their Theorem 3 shows that the second rate cannot be improved in general: on a decision set with zero gap, every algorithm pays $\Omega(\sqrt T)$ in expectation.

Timeline:

2002: Auer, Using confidence bounds for exploitation–exploration trade-offs (JMLR 3), introduces confidence-bound algorithms for linear bandits on finite decision sets.
2008: Dani, Hayes and Kakade prove the $O^*(n\sqrt T)$ upper bound for ConfidenceBall₂ and the $\Omega(\sqrt T)$ lower bound on a product of circles, the subject of this mission. A hypercube lower bound for the adversarial setting appears in their NIPS 2007 paper.
2010: Rusmevichientong and Tsitsiklis, Linearly parameterized bandits (Math. OR 35), give $\Omega(n\sqrt T)$ lower bounds on the unit sphere.
2020: Lattimore and Szepesvári, Bandit Algorithms, Theorems 24.1 and 24.2, give minimax lower bounds on the hypercube and the unit ball with Gaussian noise.

Setting

The decision set is the unit circle $D_2=S^1=\{x\in\mathbb R^2: x_1^2+x_2^2=1\}$ . An unknown mean vector $\mu\in\mathbb R^2$ is drawn once, uniformly from the circle $D_2/2$ of radius $1/2$ ; concretely $\mu=\mu(\theta)=\tfrac12(\cos\theta,\sin\theta)$ with $\theta$ uniform on $[0,2\pi)$ .

On each round $t=1,\dots,T$ the algorithm plays $x_t\in D_2$ and observes a cost $\ell_t\in\{-1,+1\}$ with $\Pr(\ell_t=+1)=(1+\mu\cdot x_t)/2$ , so that $\mathbb E[\ell_t]=\mu\cdot x_t$ . Given the decision, the cost is independent of the past.

An algorithm may be randomised. It draws a seed $s$ once from a probability measure $\rho$ on a measurable space $S$ , and chooses $x_t$ as a function of $s$ and the costs $\ell_1,\dots,\ell_{t-1}$ observed so far, measurably in $s$ .

The regret over $T$ rounds is

R=\sum_{t=1}^T(\mu\cdot x_t-\mu\cdot x^*),\qquad \mu\cdot x^*=\min_{x\in D_2}\mu\cdot x,

so each round costs $r_t=\mu\cdot x_t+\tfrac12\ge0$ when $\|\mu\|=1/2$ . The expected regret $\mathbb E R=\mathbb E_\mu\,\mathbb E(R\mid\mu)$ averages over the seed, the prior and the costs.

In the Lean development these objects are unitCircle, meanVec, optCost, RandomizedPolicy and expectedRegret in the namespace StochLinOpt.LowerBound.

Formalization targets

Goal: Theorem 3 for $n=2$

There is a universal constant $c>0$ such that for every randomised algorithm and every $T\ge1$ ,

\mathbb E R\ \ge\ c\sqrt T.

The constant is left existential, which is the form that survives any later improvement of the constant; it is chosen before the algorithm and before $T$ .

Milestones

Section 6.1, Eq. (3). For $\|\mu_1\|=\|\mu_2\|=1/2$ , $x\in S^1$ , a posterior probability $p\in[0,1]$ of $\mu=\mu_1$ and a cost $\ell\in\{\pm1\}$ , the Bayes-updated bias $b_{t+1}$ satisfies $|b_{t+1}-b_t|\le|(\mu_1-\mu_2)\cdot x|$ , where $b_t=2p-1$ .
Lemma 15. With $\varepsilon=\|\mu_1-\mu_2\|>0$ and the same data,

\mathbb E_\mu(r_t\mid\mathcal H_t)\ge\frac1{16}\Big(\varepsilon^2+\frac{|b_{t+1}-b_t|^2}{\varepsilon^2}\Big)\mathbf 1\{|b_t|\le1/2\}.

Theorem 4 (Freedman). For a martingale difference sequence $X_1,\dots,X_T$ bounded above by $b$ , with conditional variance sum $V$ , and all $a,v>0$ ,

\Pr\Big(\sum_i X_i\ge a,\ V\le v\Big)\le\exp\Big(\frac{-a^2}{2v+2ab/3}\Big).

Significance

The lower bound shows that the $\sqrt T$ dependence of the problem-independent upper bound (Theorem 2 of the same paper) is necessary. It also shows that the gap-dependent polylogarithmic rate of Theorem 1 cannot extend to decision sets without a gap, such as the sphere. Together with the upper bound it characterises the minimax regret of stochastic linear bandits in $T$ up to logarithmic factors, and in the paper's general- $n$ form it also underlies the claim that the price of bandit information is $\Theta^*(\sqrt n)$ .

The result is proved in the paper for $n=2$ and has not been machine-checked. The mission produces a checked Bayesian lower bound over all randomised algorithms, with an explicit probability model for the protocol. Two related platform results are different theorems: BanditAlgorithm.linear_bandit_unit_ball_minimax_lower_bound (Lattimore–Szepesvári Theorem 24.2: unit ball, Gaussian noise, a worst-case $\mu$ ) and BanditAlgorithm.linear_bandit_hypercube_minimax_lower_bound (Theorem 24.1: hypercube). The $\{-1,+1\}$ costs, the circle and the uniform prior used here are not covered by either.

Difficulty

The obvious attempt is a two-point change-of-measure argument with a fixed pair of means at distance $\varepsilon$ . It fails as stated because the decision set has no gap: an algorithm that plays close to the optimum of both candidates learns slowly but also pays little. The per-round trade-off between regret and information (Lemma 15) is exact only while the posterior is undecided, $|b_t|\le1/2$ . Turning it into a bound on the whole horizon requires controlling how long the posterior stays undecided, which is a statement about a martingale whose step sizes are chosen by the algorithm; a concentration bound that ignores the accumulated conditional variance (Azuma–Hoeffding with worst-case steps) is too weak for this. The averaging step from a two-point prior to the uniform prior on the circle is also part of the formal work.

Formalization scope

Vectors are Fin 2 → ℝ with the dot product ⬝ᵥ; Euclidean norms are written through dot products, never with Lean's sup norm. Rounds are 0-indexed internally: the Lean index $t$ is the paper's round $t+1$ . The expected regret is the exact finite expectation

\mathbb E R=\int_S\frac1{2\pi}\int_0^{2\pi}\sum_{\ell\in\{\pm1\}^T}\prod_{t=1}^T\frac{1+\ell_t\,\mu(\theta)\cdot x_t}{2}\;R\;d\theta\,d\rho(s),

so no infinite product of measures is needed. A randomised algorithm is a seeded policy, which covers every randomised algorithm. The optimal cost is the infimum of $\mu\cdot x$ over the compact circle and is attained. Every junk value in the model (a non-integrable integrand) could only make the lower bound harder to prove, never easier.

A statement over deterministic algorithms only, over a worst-case $\mu$ instead of the uniform prior, or with the constant allowed to depend on the algorithm or on $T$ would be a weaker theorem. The goal quantifies $\exists c>0$ before the algorithm and $T$ , and fixes the prior.

Corrections relative to the printed paper:

General $n$ is not stated. Theorem 3 as printed claims $\mathbb E R\ge\frac1{10}n\sqrt T$ for every even $n$ . It is false for $n>10$ : on $D_n$ with $\mu\in D_n/n$ each round has regret at most $1$ , so at $T=1$ the claim would need $\mathbb E R\ge n/10>1$ . The general case rests on Lemma 16, which has no proof. The goal is the $n=2$ case, which Section 6.1 proves.
The constant. For $n=2$ the paper prints $\frac15\sqrt T$ ; its proof gives $c=\frac1{16}\min(\frac12-\frac1e,\frac1{64})=\frac1{1024}$ . The proof's Freedman step prints $2\exp(-\frac{1/4}{1/8+\varepsilon/3})\le 2/e^2$ ; with $v=1/32$ the denominator is $1/16+\varepsilon/3$ , and the bound $2/e^2$ then needs $\varepsilon=T^{-1/4}\le3/16$ . Small $T$ is covered by the first round, whose expected regret is $1/2$ . The goal leaves $c$ existential.
Theorem 4. The printed variance sum runs to $n$ ; it runs to $T$ . The conditioning is on a general filtration, and square-integrability of the steps is assumed so that the conditional variance is defined.
Lemma 15. Its right side depends on the round- $t$ cost $\ell_t$ , which is not part of $\mathcal H_t$ ; the Lean statement holds for either value of $\ell_t$ .

Welcome contributions: a Lean proof of Freedman's inequality (reusable across the bandit and concentration missions on the platform); the averaging argument from two-point priors to the uniform prior; and the stopped-martingale bookkeeping for the bias sequence.

Selected references

Varsha Dani, Thomas P. Hayes, Sham M. Kakade, Stochastic Linear Optimization under Bandit Feedback, Proceedings of the 21st Annual Conference on Learning Theory (COLT), 2008.
David A. Freedman, On tail probabilities for martingales, The Annals of Probability 3(1):100–118, 1975. https://doi.org/10.1214/aop/1176996452
Colin McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer, 1998. https://doi.org/10.1007/978-3-662-12788-9_6
Peter Auer, Using confidence bounds for exploitation–exploration trade-offs, JMLR 3:397–422, 2002. https://www.jmlr.org/papers/v3/auer02a.html
Paat Rusmevichientong, John N. Tsitsiklis, Linearly parameterized bandits, Mathematics of Operations Research 35(2):395–411, 2010. https://doi.org/10.1287/moor.1100.0446
Tor Lattimore, Csaba Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 24. https://doi.org/10.1017/9781108571401

5 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization+1·Captain: mikedeng1

On Certain Polytopes Associated with Graphs IV: Adjacent Stable Sets on the Stable Set PolytopeResearch Paper

Motivation

Many combinatorial optimization problems are linear programs over a polytope whose vertices are the zero–one incidence vectors of the feasible objects: matchings, stable sets, spanning trees. The edges of such a polytope (pairs of vertices joined by a one-dimensional face) govern the behaviour of the simplex method and of local-search procedures, which move from vertex to vertex along edges: a pivot of the simplex method on a nondegenerate basis replaces a vertex by one of its neighbours.

In December 1971 M. L. Balinski asked when two matchings $M_1, M_2$ of a graph are neighbours on the matching polyhedron determined by Edmonds (Edmonds 1965). V. Chvátal answered a more general question in §6 of On certain polytopes associated with graphs (Chvátal 1975): he characterized the neighbours on the stable set polytope of an arbitrary graph. Since matchings of $G$ are the stable sets of the line graph $L(G)$ , Balinski's question is the special case of line graphs (Corollary 6.3 of the paper).

Setting

Let $G=(V,E)$ be a finite undirected loopless graph. A stable set is a set of vertices no two of which are adjacent. $S(G)$ denotes the set of all zero–one vectors $x=(x_u : u\in V)$ such that $\{u : x_u=1\}$ is stable, and the stable set polytope is

P(G)=\operatorname{conv} S(G)\subseteq \mathbb R^V .

For $y\in S(G)$ the corresponding stable set is $Y=\{u : y_u=1\}$ .

For an integer-valued vector $c=(c_u : u\in V)$ write $cx=\sum_{u\in V}c_ux_u$ . Two vectors $y, z$ are neighbours in $P(G)$ if there is an integer-valued $c$ such that $y$ and $z$ are the only two vectors which maximize $cx$ over $S(G)$ ; in particular $y\neq z$ . This is the definition the paper states at the start of the proof of Theorem 6.2.

A bicoloration of a graph $T$ is a partition $V=B\cup R$ , $B\cap R=\emptyset$ , such that every edge joins $B$ to $R$ . Every tree has one.

In the Lean development these objects are stableVectors G ( $S(G)$ ), stablePolytope G ( $P(G)$ ), onesSet y ( $Y$ ), AreNeighbors G y z and IsBicoloration T B R, all in the namespace ChvatalPolytopes.Neighbors.

Formalization targets

Goal: Theorem 6.2 (p. 149)

For $y,z\in S(G)$ with corresponding stable sets $Y,Z$ ,

y \text{ and } z \text{ are neighbours in } P(G) \iff \text{the subgraph } H \text{ of } G \text{ induced by } (Y-Z)\cup(Z-Y) \text{ is connected.}

Milestone: Lemma 6.1 (p. 149)

For a tree $T=(V,E)$ with a bicoloration $V=B\cup R$ there are nonnegative integers $c_u$ ( $u\in V$ ) and $m$ with

\sum_{u\in V}c_ux_u\le m\quad\text{for all } x\in S(T),

with equality exactly when $x$ is the incidence vector of $B$ or of $R$ .

Milestone: the certificate of the "if" part (p. 149, proof of Theorem 6.2, (i))

If $H$ is connected with spanning tree $T$ , and $c_u$ ( $u\in (Y-Z)\cup(Z-Y)$ ), $m$ are as in Lemma 6.1 for $T$ , extend $c$ by $c_u=1$ on $Y\cap Z$ and $c_u=-1$ outside $Y\cup Z$ . Then

\sum_{u\in V}c_ux_u\le m+|Y\cap Z|\quad\text{for all } x\in S(G),

with equality if and only if $x=y$ or $x=z$ .

Significance

Theorem 6.2 describes the 1-skeleton of the stable set polytope of every graph by a condition that can be checked in linear time, although optimizing over $P(G)$ is NP-hard in general and no complete linear description of $P(G)$ is known for general graphs. Through line graphs it gives the adjacency criterion for the matching polytope (two matchings are neighbours if and only if their symmetric difference is a single path or cycle), which settled Balinski's question. Characterizations of this type underlie the analysis of simplex-type and pivoting algorithms on combinatorial polytopes and the study of their diameters.

The result has been proved since 1975. The mission asks for a machine-checked proof of the theorem as stated in the paper; no formal proof of Theorem 6.2 or of the matching-polytope corollary is known to exist on Prove2Me or in Mathlib. The two milestones isolate the constructive half (Lemma 6.1 and the weighting built from it), which is reusable for any statement that needs an explicit objective singling out two stable sets.

Difficulty

The "only if" direction and the equality analysis are elementary; the substance lies in the "if" direction. An objective that makes both $y$ and $z$ optimal is easy to write down, for example $c=y+z$ ; the difficulty is to make them the only optimal vectors. Any stable set that agrees with $Y$ on some connected pieces of $H$ and with $Z$ on others ties with $y$ and $z$ under naive weightings, so the weights on $(Y-Z)\cup(Z-Y)$ must be chosen so that every mixed choice loses strictly. The integrality requirement on $c$ and the need to control all of $S(G)$ , not only the stable sets contained in $Y\cup Z$ , rule out a direct perturbation argument.

Formalization scope

Graphs. $V$ is a finite type with decidable equality and $G$ is a SimpleGraph V; loops and multiple edges are excluded, as in the paper.
$S(G)$ and $P(G)$ . $S(G)$ is the set of incidence vectors in V → ℝ of stable finsets; $P(G)$ is convexHull ℝ (S G).
Neighbours. Defined exactly as on p. 149: $y\ne z$ and, for some $c : V\to\mathbb Z$ , the set of maximizers of $cx$ over $S(G)$ equals $\{y,z\}$ . The face-lattice notion of an edge of $P(G)$ is not used; its equivalence with this definition is not part of the paper.
Induced subgraph and connectedness. $H$ is G.induce of the set $(Y\setminus Z)\cup(Z\setminus Y)$ , and "connected" is Mathlib's SimpleGraph.Connected, which requires at least one vertex. For $y=z$ both sides of the goal are therefore false.
Trees. SimpleGraph.IsTree, which includes connectedness; a spanning tree of $H$ is a graph $T$ on the vertex set of $H$ with $T\le H$ and T.IsTree. In Lemma 6.1 the integers $c_u$ and $m$ are natural numbers.

A trivializing formalization — defining neighbours through the symmetric-difference condition or through Lemma 6.1's certificate, or omitting $y\neq z$ from the definition — is excluded: neighbours are defined only through unique maximizers of integer objectives over $S(G)$ .

A complete development needs only finite graphs, induced subgraphs, spanning trees of connected graphs (available in Mathlib) and finite sums. Contributions welcome beyond the milestones: the equivalence of this notion of neighbours with the one-dimensional faces of $P(G)$ , and Corollary 6.3 for the matching polytope via line graphs.

Selected references

V. Chvátal, On certain polytopes associated with graphs, Journal of Combinatorial Theory, Series B 18 (1975), 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
M. W. Padberg, On the facial structure of set packing polyhedra, Mathematical Programming 5 (1973), 199–215. https://doi.org/10.1007/BF01580121

6 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization+1·Captain: mikedeng1

On Certain Polytopes Associated with Graphs II: No Clique Is a Cutset of a Connected α-Critical GraphResearch Paper

Motivation

The stability number $\alpha(G)$ of a graph, the largest number of pairwise non-adjacent vertices, is the optimum of an integer program over the stable set polytope $P(G)$ . Linear programming duality turns any explicit linear description of $P(G)$ into a certificate of optimality for $\alpha(G)$ , which is why the question "which inequalities are needed to describe $P(G)$ ?" has been central to polyhedral combinatorics since Edmonds' description of the matching polytope (Edmonds 1965). Chvátal's 1975 paper (doi:10.1016/0095-8956(75)90041-6) initiated the systematic study of $P(G)$ for arbitrary graphs: which graph operations preserve a known description, and which inequalities are facets, i.e. indispensable in every description.

Section 4 of the paper treats one such operation, gluing two graphs along a complete subgraph, and one family of facets, the "rank" inequality $\sum_u x_u\le\alpha(G)$ for graphs whose critical edges connect all vertices. Combining the two yields a purely graph-theoretic fact about $\alpha$ -critical graphs (graphs in which deleting any edge increases the stability number): no complete subgraph separates such a graph. The fact is due to Berge (Graphes et hypergraphes, 1970, Ch. 13, §3, Corollary 2); Chvátal's derivation obtains it from polyhedral arguments. $\alpha$ -critical graphs were studied by Erdős and Gallai, Hajnal, Andrásfai and Lovász, and their structure is closely tied to the facets of $P(G)$ .

Setting

Graphs are finite, undirected and loopless: $G=(V,E)$ . A stable set is a set of pairwise non-adjacent vertices; $\alpha(G)$ is the largest size of a stable set. The incidence vector of $s\subseteq V$ is $\chi^s\in\mathbb R^V$ with $\chi^s_u=1$ for $u\in s$ and $0$ otherwise. $S(G)$ is the set of incidence vectors of stable sets and

P(G)=\operatorname{conv}S(G)\subseteq\mathbb R^V .

A finite system $\sum_{u\in V}a_{iu}x_u\le b_i$ $(i\in J)$ is a defining linear system of $P$ if its solution set is exactly $P$ . An inequality $\sum_u a_ux_u\le b$ is a facet of $P$ if every defining linear system of $P$ contains, for some $t>0$ , the inequality $\sum_u ta_ux_u\le tb$ .

An edge $e$ of $G$ is critical if $\alpha(G-e)=\alpha(G)+1$ ; $E^*$ denotes the set of critical edges, $G^*=(V,E^*)$ , and $G$ is $\alpha$ -critical if every edge is critical. For graphs $G_1=(V_1,E_1)$ , $G_2=(V_2,E_2)$ put $G_1\cap G_2=(V_1\cap V_2,E_1\cap E_2)$ and $G_1\cup G_2=(V_1\cup V_2,E_1\cup E_2)$ . A vertex set $K$ is a cutset of $G$ if two vertices outside $K$ are joined by no path of $G-K$ , the subgraph induced on $V\setminus K$ .

In Lean, all objects live in the namespace ChvatalPolytopes.Separation: stablePolytope G, IsFacet P a b, IsCriticalEdge, criticalGraph G (for $G^*$ ), IsAlphaCritical G and IsCutset G K.

Formalization targets

Goal: Corollary 4.3 (p. 144)

For a finite connected $\alpha$ -critical graph $G$ and any $K\subseteq V$ inducing a complete subgraph,

K \text{ is not a cutset of } G .

The goal is pure graph theory; its proof in the paper consists of the two polyhedral theorems below.

Milestones

Proposition 2.1 (pp. 139–140). For a finite nonempty set $S$ of solutions of $-x_u\le0$ $(u\in V)$ , $\sum_u a_{iu}x_u\le b_i$ $(i\in J)$ : the solution set equals $\operatorname{conv}S$ if and only if for every $c\in\mathbb Z^V$

\max\{cx:x\in S\}=\min\Big\{\sum_i\lambda_ib_i:\lambda\ge0,\ \sum_i\lambda_ia_{iu}\ge c_u\ (u\in V)\Big\}.

Theorem 4.1 (p. 141). If $G_1\cap G_2$ is complete, the union of defining linear systems of $P(G_1)$ and $P(G_2)$ (each containing its nonnegativity rows) is a defining linear system of $P(G_1\cup G_2)$ .
Theorem 4.2 (p. 143). If $G^*$ is connected, then

\sum_{u\in V}x_u\le\alpha(G)

is a facet of $P(G)$ .

Significance

Theorem 4.1 says that clique-sums are harmless for linear descriptions of $P(G)$ : a description of a graph glued along a clique is the union of descriptions of the pieces. It underlies the later decomposition theory of stable set polytopes (clique cutsets appear throughout the study of perfect and $t$ -perfect graphs). Theorem 4.2 supplies a large class of facets with a combinatorial certificate, and was the starting point of the study of rank facets. Corollary 4.3 illustrates how polyhedral statements yield structural graph theory: the facet in Theorem 4.2 cannot coexist with a clique cutset.

All three results are proved in the paper, and Berge's corollary was known before it. None of them has, to the knowledge of this mission, a machine-checked proof; Mathlib has stable sets (IsIndepSet, indepNum), cliques and convex hulls, but no stable set polytope, no notion of facet via defining systems, and no $\alpha$ -critical graphs. The mission produces these definitions and the formal proofs of Proposition 2.1, Theorems 4.1, 4.2 and Corollary 4.3.

Difficulty

Proposition 2.1 requires LP duality in the form "min = max with both optima attained" together with a separation argument that reduces arbitrary objectives to integral ones; the "if" direction fails without the nonnegativity rows, so the statement is sensitive to the exact form of the system. In Theorem 4.1 the inclusion $P(G_1\cup G_2)\subseteq$ (solutions of the union) is routine; the difficulty is the converse: a point whose restrictions lie in $P(G_1)$ and in $P(G_2)$ is a convex combination of stable sets on each side, and the two combinations have to be matched on the clique $V_1\cap V_2$ to produce stable sets of $G_1\cup G_2$ . Theorem 4.2 concerns every defining linear system, so it cannot be proved by exhibiting one description; the natural route via "affinely independent tight points" is a different definition of facet and needs full-dimensionality of $P(G)$ to be equivalent. Finally, the goal requires translating a cutset into a decomposition $G=G_1\cup G_2$ with complete intersection, and then showing that a union of two systems on smaller vertex sets cannot contain a positive multiple of $\sum_{u\in V}x_u\le\alpha(G)$ .

Formalization scope

Graphs are SimpleGraph V on a Fintype V with DecidableEq V. $S(G)$ is a set of functions V → ℝ (incidence vectors of stable finsets), and $P(G)$ is convexHull ℝ (stableVectors G).
Linear systems are indexed by finite types with real coefficients. "Defining linear system" is equality of the solution set with the polytope. IsFacet quantifies over all finite index types J : Type and all real systems whose solution set equals the polytope; it is the paper's definition, not the affinely-independent-points characterization.
Proposition 2.1: "min = max" means an attained minimum equal to the maximum; the hypothesis $S\neq\emptyset$ is added (the paper's $\max$ over $S$ needs it), and the nonnegativity rows are kept.
Theorem 4.1: the glued graph $G$ lives on a type $V$ with finsets $V_1\cup V_2=V$ ; $G_1,G_2$ are the induced subgraphs on $V_1,V_2$ ; " $G_1\cap G_2$ complete" is encoded as " $V_1\cap V_2$ is a clique of $G$ and no edge joins $V_1-V_2$ to $V_2-V_1$ ", which is equivalent to the paper's hypotheses. The rows of each system are evaluated on the restriction of $x$ .
Theorem 4.2: " $G^*$ connected" is Mathlib's Connected, which requires $V\neq\emptyset$ — for $V=\emptyset$ the statement would be false. $\alpha(G)$ is indepNum, cast to $\mathbb R$ .
Corollary 4.3: "complete subgraph" is any clique set G.IsClique K, not only maximal cliques (the paper reserves "clique" for maximal complete subgraphs, but the corollary speaks of complete subgraphs), including $K=\emptyset$ . "Cutset" means two vertices outside $K$ joined by no path of $G-K$ . The formalization " $G-K$ is not connected" is ruled out: under Mathlib's convention it would make $K=V$ a cutset and the statement false for $K_1$ and $K_2$ .
Reusable infrastructure: the stable set polytope, facets via defining systems, Proposition 2.1 (shared with the other missions of this series), critical edges and $\alpha$ -critical graphs. Contributions of intermediate lemmas (LP duality in the attained form, full-dimensionality of $P(G)$ , the cutset–decomposition equivalence) are welcome.

Selected references

V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
C. Berge, Graphes et hypergraphes, Dunod, Paris, 1970 (English translation: Graphs and Hypergraphs, North-Holland, 1973), Chapter 13, §3.
J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965) 125–130. https://doi.org/10.6028/jres.069B.013
M. W. Padberg, On the facial structure of set packing polyhedra, Math. Programming 5 (1973) 199–215. https://doi.org/10.1007/BF01580121
L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4

8 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization+1·Captain: mikedeng1

On Certain Polytopes Associated with Graphs I: Clique Inequalities Define the Stable Set Polytope Exactly for Perfect GraphsResearch Paper

Motivation

Many combinatorial optimization problems ask for the best subset of a finite set subject to combinatorial side conditions. The polyhedral method replaces the finite family of feasible subsets by the convex hull of their incidence vectors and asks for an explicit system of linear inequalities describing that convex hull; once such a system is known, linear programming duality gives min–max theorems and certificates of optimality. The maximum weight stable set problem is the central test case: it is NP-hard in general, so no tractable complete description of its polytope is expected for all graphs, and the question becomes for which graphs a simple description suffices.

V. Chvátal's 1975 paper On certain polytopes associated with graphs answers this question for the two simplest families of valid inequalities, and its Section 3 connects the answer to Berge's perfect graphs. The result is a standard entry point to polyhedral combinatorics and is one of the ingredients behind the later polynomial-time algorithms for stable sets in perfect graphs by Grötschel, Lovász and Schrijver.

Timeline. Berge (1961) introduced perfect graphs and conjectured that a graph is perfect if and only if its complement is. Lovász (Normal hypergraphs and the perfect graph conjecture, Discrete Math. 1972; A characterization of perfect graphs, J. Combin. Theory Ser. B 1972) proved this, together with the characterization of perfection by $\alpha(G_A)\,\omega(G_A)\ge|A|$ and the invariance of perfection under vertex duplication. Fulkerson's theory of antiblocking polyhedra (1971–72) gave a polyhedral route to the same equivalence. Chvátal (received 1972, published 1975) gave the self-contained polyhedral statement formalized here, with a proof based on Lovász's two theorems.

Setting

A graph $G=(V,E)$ is finite, undirected and loopless. A stable set is a set of vertices no two of which are adjacent. A clique is a maximal complete subgraph, and $C(G)$ is the set of vertex sets $W\subseteq V$ of the cliques of $G$ .

$S(G)\subseteq\mathbb R^V$ is the set of zero–one vectors $x=(x_u:u\in V)$ such that $\{u:x_u=1\}$ is stable, and the stable set polytope is $P(G)=\operatorname{conv}S(G)$ . A finite system of linear inequalities is a defining linear system of $P(G)$ if its solution set is exactly $P(G)$ . For $c\in\mathbb R^V$ write $cx=\sum_{u\in V}c_ux_u$ .

$G$ is perfect (the paper's $\alpha$ -perfect) if for every zero–one vector $c$ ,

\max\{cx:x\in S(G)\}=\min\Big\{\sum_{W\in C(G)}\lambda_W:\ \lambda_W\in\{0,1\},\ \sum_{W\in C(G),\,u\in W}\lambda_W\ge c_u\ (u\in V)\Big\}.

For $A\subseteq V$ , $G_A$ is the induced subgraph, $\alpha(G_A)$ its stability number and $\omega(G_A)$ its clique number. To duplicate a vertex $u$ is to add a new vertex $u'$ adjacent to all neighbours of $u$ but not to $u$ .

In the Lean development these are stableVectors G, stablePolytope G, maximalCliques G, IsPerfect G and duplicate G u in the namespace ChvatalPolytopes.Perfect.

Formalization targets

Goal: Theorem 3.1 (p. 140)

For every graph $G$ , the system

-x_u\le0\quad(u\in V),\qquad\sum_{u\in W}x_u\le1\quad(W\in C(G))

is a defining linear system of $P(G)$ if and only if $G$ is perfect. Both directions are required.

Milestones

Proposition 2.1 (pp. 139–140). For a finite nonempty set $S$ of solutions of $-x_u\le0$ , $\sum_u a_{iu}x_u\le b_i$ $(i\in J)$ , the solution set equals $\operatorname{conv}S$ if and only if for every $c\in\mathbb Z^V$

\max\{cx:x\in S\}=\min\Big\{\sum_i\lambda_ib_i:\lambda\ge0,\ \sum_i\lambda_ia_{iu}\ge c_u\ (u\in V)\Big\}.

Lovász's first theorem (§3, p. 140). Every nonperfect $G$ has $A\subseteq V$ with $\alpha(G_A)\,\omega(G_A)<|A|$ .
Lovász's second theorem (§3, p. 140). Duplicating a vertex of a perfect graph gives a perfect graph.
Condition (iii) (p. 141). $G$ is perfect if and only if for every $c\in\mathbb Z^V$

\max\{cx:x\in S(G)\}=\min\Big\{\sum_{W\in C(G)}\lambda_W:\lambda_W\ge0,\ \sum_{W\ni u}\lambda_W\ge c_u\ (u\in V)\Big\}.

Significance

The result. The nonnegativity and clique inequalities are valid for $P(G)$ for every graph. Theorem 3.1 says they are complete exactly for perfect graphs, so on perfect graphs the maximum weight stable set problem is a linear program over an explicitly described polytope, and weighted min–max theorems (stable sets versus clique covers) follow from LP duality. Combined with the perfect graph theorem, it gives a polyhedral characterization of perfect graphs, and it is the model for later results that identify graph classes by the facets of their stable set polytopes (odd-cycle inequalities, $t$ -perfection, Section 7 of the same paper).

Formalizing it. The result is classical and proved. No machine-checked version of it is known, and Mathlib has neither perfect graphs nor stable set polytopes. The mission produces a formal statement of the polyhedral characterization with the paper's own notion of perfection, a formal version of the convex-hull/LP min–max principle (Proposition 2.1), which is reusable for any 0–1 polytope, and formal statements of the two theorems of Lovász that the proof relies on.

Difficulty

Proposition 2.1 reduces Theorem 3.1 to the equivalence of perfection with a fractional min–max for all integer weights. The obvious approach to that equivalence fails in both directions. From perfection one only gets the min–max for zero–one weights and zero–one multipliers; general integer weights do not reduce to zero–one weights by linearity, because the minimum over clique covers is not additive in $c$ . Conversely, a fractional clique cover of value $\alpha$ does not directly produce an integral one. The paper crosses this gap with two theorems of Lovász: a numerical certificate of nonperfection, and the invariance of perfection under vertex duplication. Both are substantial graph-theoretic results in their own right, and neither follows from the definitions by routine manipulation.

Proposition 2.1 itself needs separation of a point from a polytope by an integral objective and LP strong duality with the nonnegativity rows handled separately.

Formalization scope

Vertices form a finite type V with decidable equality; a graph is a SimpleGraph V. $S(G)$ is a set of functions V → ℝ, and $P(G)$ is Mathlib's convexHull ℝ of it. $C(G)$ is the finset of finsets that are maximal among cliques (Maximal), as on the page; with $V=\emptyset$ the only maximal clique is $\emptyset$ . "Defining linear system" is an equality of sets. Every "max = min" is written out in full: there is a value $m$ that is the maximum over $S$ (attained and an upper bound), some feasible multiplier vector attains $m$ , and every feasible multiplier vector has objective at least $m$ . Clique multipliers are functions Finset V → ℝ read only on $C(G)$ .

Explicit conventions and added hypotheses:

In Proposition 2.1 the index set $J$ is a finite type, coefficients are real, the nonnegativity rows are kept as a separate conjunct $x\ge0$ , and $S$ is assumed nonempty (the paper's $\max$ over $S$ needs it).
$\alpha$ and $\omega$ are Mathlib's indepNum and cliqueNum (natural numbers) of G.induce A.
The duplicated graph lives on Option V, with none the new vertex.

Perfection is the paper's zero–one min–max, not "the clique system defines $P(G)$ " (which would make the goal a tautology) and not Berge's $\chi(G_A)=\omega(G_A)$ (a different definition, equivalent only through the perfect graph theorem). $P(G)$ is the convex hull of $S(G)$ , never the solution set of an inequality system.

Needed infrastructure, all reusable: integral separation from a rational polytope and LP strong duality in the form $\max\{cx:Ax\le b,x\ge0\}=\min\{\lambda b:\lambda A\ge c,\lambda\ge0\}$ ; basic facts about stable sets and maximal cliques of induced subgraphs and of duplicated graphs; invariance of IsPerfect under graph isomorphism and under taking induced subgraphs. Proofs of the Lovász milestones, which have independent value for a Mathlib theory of perfect graphs, are welcome.

Selected references

V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4
L. Lovász, A characterization of perfect graphs, J. Combin. Theory Ser. B 13 (1972) 95–98. https://doi.org/10.1016/0095-8956(72)90045-7
D. R. Fulkerson, Anti-blocking polyhedra, J. Combin. Theory Ser. B 12 (1972) 50–71. https://doi.org/10.1016/0095-8956(72)90032-9
M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

8 thms2 active usersReviewed

Completed

Operations Research Optimization Theoretical Computer Science·Captain: mikedeng1

An Optimal On-Line Algorithm for Metrical Task System 1: Every n-State Metrical Task System Has Competitive Ratio 2n - 1Research Paper

Motivation

A system that processes a stream of tasks can often be configured in several ways, and the configuration affects both the cost of the current task and the cost of switching before the next one: paging schemes, replicated files, server placements. When the future is unknown, the natural worst-case yardstick is competitive analysis, introduced by Sleator and Tarjan for list update and paging (Sleator–Tarjan 1985): an on-line strategy is compared with the optimal strategy that knows the whole input in advance.

Borodin, Linial and Saks (J. ACM 1992; conference version STOC 1987) proposed metrical task systems as a single model containing all such problems, and determined the exact deterministic competitive ratio of every such system. Their theorem is the starting point of the on-line-algorithms literature on metrical task systems, the $k$ -server problem (Manasse–McGeoch–Sleator 1990) and their randomized variants.

Timeline. 1985: Sleator and Tarjan introduce competitive analysis for paging and list update. 1987: Borodin, Linial and Saks prove $w(S,d)=2n-1$ for every $n$ -state metrical task system (journal version 1992). 1990: Manasse, McGeoch and Sleator extend the task-system model to restricted task sets and pose the $k$ -server conjecture. The randomized ratio of the uniform task system, bounded in the same paper between $H(n)$ and $2H(n)$ , is the subject of the companion mission.

Setting

A task system $(S,d)$ has a finite set $S$ of $n$ states and a transition-cost matrix $d$ with $d(i,i)=0$ , $d(i,j)>0$ for $i\neq j$ , and the triangle inequality $d(i,j)+d(j,k)\ge d(i,k)$ . It is metrical if also $d(i,j)=d(j,i)$ .

A task $T$ is a vector of nonnegative processing costs $T(s)$ , $s\in S$ . Given a task sequence $\mathbf T=T^1\cdots T^m$ and an initial state $s_0$ , a schedule is a map $\sigma:\{0,\dots,m\}\to S$ with $\sigma(0)=s_0$ ; task $T^i$ is processed in state $\sigma(i)$ , and the cost is

c(\mathbf T;\sigma)=\sum_{i=1}^m d(\sigma(i-1),\sigma(i))+\sum_{i=1}^m T^i(\sigma(i)).

The off-line optimum $c_0(\mathbf T)$ is the minimum over all schedules. An on-line algorithm $A$ chooses $\sigma(i)$ knowing only $s_0$ and $T^1,\dots,T^i$ ; its cost is $c_A(\mathbf T)$ . For $w>0$ , $A$ is $w$ -competitive if there is a constant $K_w$ with $c_A(\mathbf T)\le w\,c_0(\mathbf T)+K_w$ for every finite task sequence. The competitive ratio of $A$ is $w(A)=\inf\{w: A\text{ is }w\text{-competitive}\}$ , and the competitive ratio of the task system is $w(S,d)=\inf_A w(A)$ .

For the upper bound the paper also uses continuous-time schedules, in which task $T^i$ occupies the interval $[i,i+1)$ and the scheduler may change state at any real time, paying $\int_i^{i+1}T^i(\sigma(t))\,dt$ for processing. For a general (possibly asymmetric) matrix $d$ , the cycle offset ratio $\psi(d)$ is the maximum over closed walks $s_0,\dots,s_k=s_0$ of $\sum_i d(s_{i-1},s_i)\big/\sum_i d(s_i,s_{i-1})$ ; it equals $1$ when $d$ is symmetric.

Formalization targets

Goal: Theorem 1.1

For every metrical task system $(S,d)$ with $n$ states,

w(S,d)=2n-1 .

The value depends on $n$ only, not on the distances.

Milestones

Lemma 2.1. If $c_0(T^1\cdots T^m)\to\infty$ along an infinite task sequence $\mathbf T$ , then $w(A)\ge w_{\mathbf T}(A)=\limsup_m c_A/c_0$ .
Theorem 2.2. Against the cruel taskmaster $M(\varepsilon)$ , which charges $\varepsilon$ in the state the algorithm currently occupies,

w_{\mathbf T(\varepsilon)}(A)\ge\frac{2n-1}{1+\varepsilon/\min_{i\neq j}d(i,j)} .

Lemma 3.1. Every on-line continuous-time algorithm is matched, on every task sequence, by an on-line discrete-time algorithm.
Lemmas 6.3, 6.4, 6.2. Properties of the functions $f_k$ that drive the algorithm $A^*_d$ : $f_k(s)-f_k(s')\le d(s',s)$ ; the identity $2\sum_{s\ne s_k}f_k(s)+f_k(s_k)=C_{k-1}+\sum_{i\le k}d(s_i,s_{i-1})$ ; and $f_k\le h_k$ , the off-line cost at the $k$ -th transition time.
Theorem 6.1 (= Theorem 1.2). For every task system, symmetric or not, $A^*_d$ has competitive ratio at most $(2n-1)\psi(d)$ .

Significance

The theorem settles the deterministic competitive ratio of the whole class of metrical task systems: the lower bound says that no deterministic on-line strategy can beat $2n-1$ on any metric, and the upper bound supplies one algorithm that achieves it on every metric. For asymmetric costs the same algorithm gives $(2n-1)\psi(d)$ . The $2n-1$ lower bound is also the benchmark against which restricted models, such as paging and the $k$ -server problem, measure their improvements, and the randomized question it leaves open drove much of the later work on metrical task systems.

The result was proved in 1987 and is standard; to the best of our knowledge no machine-checked proof exists. A formal development would provide a reusable model of deterministic on-line algorithms and competitiveness (on-line maps from task prefixes, additive competitiveness, infima over algorithms), an adversary construction by mutual recursion with an arbitrary algorithm, and an exact treatment of continuous-time schedules with piecewise-constant task costs. These pieces are reusable for other competitive-analysis results.

Difficulty

The lower bound is not a single bad input: the adversary is built from the algorithm it plays against, so the hard task sequence exists only as a recursion interleaved with the algorithm's choices, and the bound must hold for every deterministic on-line map, including ones that behave erratically. Obtaining the exact constant $2n-1$ , rather than some $\Omega(n)$ bound, requires a sharp estimate of the off-line cost of that sequence.

The upper bound needs an algorithm defined in continuous time, whose transition times are determined by accumulated processing costs; the budgets can be zero, so transitions can be instantaneous, and a formal cost must remain well defined before one knows that only finitely many transitions occur. Relating the off-line cost function at those times to the recursively defined $f_k$ (Lemma 6.2) requires reasoning about all continuous-time off-line schedules. Finally, the goal combines both directions through infima over all on-line algorithms, and the discretization of Lemma 3.1 must be composed with the continuous-time algorithm.

Formalization scope

States form a finite type S (Fintype, DecidableEq, Nonempty); the goal is stated for all $n\ge1$ , where $n=1$ gives $w(S,d)=1$ . Task costs are finite nonnegative reals; the paper also allows $+\infty$ entries, which are excluded (this affects neither bound). A task sequence is T : Fin m → S → ℝ, with T i the paper's $T^{i+1}$ , and a schedule is σ : Fin (m+1) → S. An on-line algorithm is a map sending $(s_0,[T^1,\dots,T^i])$ to $\sigma(i)$ , so on-line behaviour is built into the type. Competitiveness is written additively, $c_A\le w\,c_0+K$ , with $K$ independent of the task sequence and of $s_0$ .

The competitive ratio competitiveRatio d is the real infimum of the set of all $w$ for which some on-line algorithm is $w$ -competitive. It is not defined as an infimum of per-algorithm real infima: a non-competitive algorithm has $W_A=\emptyset$ , whose real infimum is $0$ , and that would drag $w(S,d)$ to $0$ for every system. Since the goal's value $2n-1$ is at least $1$ while the empty set's real infimum is $0$ , the goal cannot hold vacuously.

Continuous-time algorithms are given as lists of $(\text{state},\text{length})$ pieces per unit interval; processing integrals are exact finite sums. The algorithm $A^*_d$ minimizes over states different from the current one, as its proof requires (the printed rule ranges over all states, and would stall); ties are left arbitrary. Its budgets may be $0$ , its entry times are Option ℝ, and its cost is a sum in $[0,\infty]$ , so that Theorem 6.1 itself asserts that only finitely many transitions occur. The ratio $\psi(d)$ excludes closed walks that never move, and Theorems 2.2 and 6.1 require $n\ge2$ , where $\min_{i\ne j}d(i,j)$ and $\psi(d)$ are defined. Lemma 3.1 is stated comparing $A$ with $A'$ (the printed statement says "as well as $A$ ").

A complete development needs: the discrete model and off-line optimum (finite minimum over schedules), limsup arguments in EReal, continuous-time schedules with piecewise-constant costs, and the recursion defining $A^*_d$ . Proofs of any milestone, including the purely combinatorial Lemmas 6.3 and 6.4, are welcome, as is a formal composition of Lemma 3.1 with Theorem 6.1.

Selected references

A. Borodin, N. Linial, M. E. Saks, An optimal on-line algorithm for metrical task system, Journal of the ACM 39(4):745–763, 1992. https://doi.org/10.1145/146585.146588
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

12 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Nonmonotone Spectral Projected Gradient Methods on Convex Sets I: SPG2 Is Well Defined and Its Accumulation Points Are StationaryResearch Paper

Motivation

Minimizing a smooth function over a closed convex set $\Omega\subseteq\mathbb R^n$ on which projection is cheap (a box, a ball, a simplex) is a routine subproblem in large-scale optimization: box-constrained minimization is the inner solver of augmented Lagrangian methods, and bound-constrained least squares, image restoration and density estimation all have this form. The classical projected gradient method of Goldstein and of Levitin and Polyak is simple and needs only gradients and projections, but with constant or Armijo-type step lengths it is slow.

Spectral projected gradient (SPG) methods, introduced by Birgin, Martínez and Raydan (paper), combine three ingredients: the projected gradient direction; the Barzilai–Borwein (spectral) step length $\alpha_{k+1}=\langle s_k,s_k\rangle/\langle s_k,y_k\rangle$ , an inverse Rayleigh quotient of the average Hessian along the last step; and the nonmonotone line search of Grippo, Lampariello and Lucidi, which compares a trial value with the worst of the last $M$ objective values instead of the current one. The method is widely used in practice, and its analysis is the template for many later nonmonotone projected methods.

Timeline:

1964–1966: Goldstein; Levitin and Polyak introduce gradient projection.
1976: Bertsekas analyses the Armijo rule along the projection arc.
1986: Grippo, Lampariello and Lucidi introduce the nonmonotone line search for unconstrained problems.
1988: Barzilai and Borwein propose the two-point step size; Raydan (1993, 1997) proves convergence for quadratics and combines it with nonmonotone search in the unconstrained case.
2000: Birgin, Martínez and Raydan define SPG1 and SPG2 for convex constraints (SIAM J. Optim. 10(4)).
2003: the same authors publish the convergence proof that Theorem 2.1 refers to, in the inexact setting (IMA J. Numer. Anal. 23).

Setting

Let $\Omega\subseteq\mathbb R^n$ be nonempty, closed and convex, with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . Let $f$ have continuous partial derivatives on an open set $U\supseteq\Omega$ and write $g(x)=\nabla f(x)$ . The orthogonal projection $P(z)$ is the unique point of $\Omega$ nearest to $z$ . The scaled projected gradient is $g_t(x)=P(x-t\,g(x))-x$ for $x\in\Omega$ , $t>0$ . A point $\bar x$ is a constrained stationary point if $\langle g(\bar x),x-\bar x\rangle\ge0$ for all $x\in\Omega$ .

The parameters are an integer $M\ge1$ , reals $0<\alpha_{\min}<\alpha_{\max}$ , a sufficient-decrease constant $\gamma\in(0,1)$ and safeguards $0<\sigma_1<\sigma_2<1$ . Algorithm SPG2 starts from $x_0\in\Omega$ and $\alpha_0\in[\alpha_{\min},\alpha_{\max}]$ and at iteration $k=0,1,\dots$ :

Stop test. If $\|P(x_k-g(x_k))-x_k\|=0$ , stop: $x_k$ is stationary.
Backtracking. Set $d_k=P(x_k-\alpha_k g(x_k))-x_k$ and $\lambda=1$ . While

f(x_k+\lambda d_k)\le\max_{0\le j\le\min\{k,M-1\}}f(x_{k-j})+\gamma\lambda\langle d_k,g(x_k)\rangle\qquad(3)

fails, replace $\lambda$ by any $\lambda_{\rm new}\in[\sigma_1\lambda,\sigma_2\lambda]$ . When (3) holds, $\lambda_k=\lambda$ and $x_{k+1}=x_k+\lambda_kd_k$ . 3. Spectral step. With $s_k=x_{k+1}-x_k$ , $y_k=g(x_{k+1})-g(x_k)$ , $b_k=\langle s_k,y_k\rangle$ : $\alpha_{k+1}=\alpha_{\max}$ if $b_k\le0$ , else $\alpha_{k+1}=\min\{\alpha_{\max},\max\{\alpha_{\min},\langle s_k,s_k\rangle/b_k\}\}$ .

In Lean the projection is a function P with the predicate IsProjOnto Ω P, $g_t$ is scaledProjGrad P f t, stationarity is IsConstrainedStationary Ω f, the maximum in (3) is nonmonotoneRef f x M k, and an infinite run is IsSPG2Run Ω f P M αmin αmax γ σ₁ σ₂ x α.

Formalization targets

Goal: Theorem 2.1, accumulation points are stationary

For every infinite run $(x_k,\alpha_k)$ of SPG2 and every accumulation point $\bar x$ of $(x_k)$ ,

\langle g(\bar x),x-\bar x\rangle\ge0\qquad\text{for all }x\in\Omega.

The statement fixes no parameter values and assumes neither convexity of $f$ nor a bounded level set.

Milestones

Lemma 2.1 (ii). For $\bar x\in\Omega$ and $t\in(0,\alpha_{\max}]$ : $g_t(\bar x)=0$ iff $\bar x$ is a constrained stationary point.
Lemma 2.1 (i). For $x\in\Omega$ and $t\in(0,\alpha_{\max}]$ :

\langle g(x),g_t(x)\rangle\le-\tfrac1t\|g_t(x)\|_2^2\le-\tfrac1{\alpha_{\max}}\|g_t(x)\|_2^2.

Theorem 2.1, first clause (SPG2 is well defined). At a point where Step 1 does not stop, every admissible backtracking sequence reaches a step satisfying (3). The step is stated for an arbitrary reference value $R\ge f(x)$ , which covers the maximum in (3).
Section 2, p. 4. The iterates remain in $\Omega_0=\{x\in\Omega:f(x)\le f(x_0)\}$ .

Significance

Theorem 2.1 is the global convergence guarantee for SPG2. It holds without monotone decrease of $f$ and without any restriction on the spectral step beyond the safeguards. These are the two features that make the method fast in practice, and together they mean that no classical monotone projected-gradient argument applies directly. The same statement underlies the convergence claims of the SPG software (ACM TOMS Algorithm 813) and of the many methods that reuse the nonmonotone spectral framework: inexact SPG, augmented Lagrangian inner solvers, and projected BB methods for machine learning.

Status: the theorem is proved in the literature. This paper's proof reads "See [7]", a pointer to Birgin, Martínez and Raydan (2003). No Lean formalization of this theorem, of the nonmonotone Armijo analysis, or of the projected-gradient stationarity lemma is known. The mission produces a formal proof and a reusable Lean interface for projection-based first-order methods on convex sets.

Difficulty

The obvious argument for monotone descent methods is to show that $f(x_k)$ decreases, so that the total decrease is finite and the per-iteration decrease $\gamma\lambda_k|\langle d_k,g(x_k)\rangle|$ tends to zero. Here $f(x_k)$ need not decrease. Only the reference value $\max_{0\le j\le\min\{k,M-1\}}f(x_{k-j})$ is nonincreasing, and a small decrease of this maximum along the whole sequence does not by itself give a small decrease at the iterates that approach a given accumulation point $\bar x$ . A second difficulty is that the accepted step lengths $\lambda_k$ may tend to zero along the subsequence, while $f$ is $C^1$ only on a neighbourhood of $\Omega$ and no Lipschitz constant for $g$ is available, so no uniform sufficient-decrease estimate holds. The spectral steps $\alpha_k$ vary within $[\alpha_{\min},\alpha_{\max}]$ , so the directions $d_k$ are not a fixed function of $x_k$ .

Formalization scope

Space and data. The space is EuclideanSpace ℝ (Fin n) with inner ℝ and the 2-norm. $f$ is a total function EuclideanSpace ℝ (Fin n) → ℝ with ContDiffOn ℝ 1 f U on an open U ⊇ Ω, and $g$ is Mathlib's gradient f. The algorithm evaluates $f$ and $g$ only at points of $\Omega$ .
Iteration and trials. Iterations are indexed from $0$ . The backtracking choice (2) is universally quantified: a run carries, at each iteration, a finite trial list $\lambda^{(0)}=1$ , $\lambda^{(i+1)}\in[\sigma_1\lambda^{(i)},\sigma_2\lambda^{(i)}]$ , in which test (3) fails at every trial but the last and holds at the last.
Step size. $\alpha_{k+1}$ is given by Step 3 exactly.
Accumulation point. An accumulation point is MapClusterPt x̄ atTop x.
Excluded simplifications. A run predicate that accepts any positive step, or lets $\alpha_{k+1}$ range freely over $[\alpha_{\min},\alpha_{\max}]$ , is not SPG2. Nor is a goal stating $g_t(\bar x)=0$ instead of the variational inequality, or one that adds convexity of $f$ , a Lipschitz gradient or a bounded level set.
Non-vacuity. The hypotheses of the goal are satisfiable: for $f(x)=\|x\|^2$ , $\Omega=\mathbb R^n$ , $M=1$ , $\alpha_{\min}=1/8$ , $\alpha_{\max}=1/4$ , $\gamma=1/2$ and $v\ne0$ , the iterates $x_k=2^{-k}v$ with $\alpha_k=1/4$ form an infinite run with accumulation point $0$ .
Infrastructure. A complete development needs the variational characterization of the projection (Mathlib has it for the iInf form: norm_eq_iInf_iff_real_inner_le_zero), continuity properties of the projection, a mean-value estimate for $C^1$ functions on segments in $\Omega$ , and the nonmonotone reference-value bookkeeping. The projection lemmas and the nonmonotone bookkeeping are reusable beyond this mission, in particular for the companion mission on SPG1, and contributions of them as separate lemmas are welcome.

Selected references

E. G. Birgin, J. M. Martínez, M. Raydan, Nonmonotone spectral projected gradient methods on convex sets, SIAM J. Optim. 10(4) (2000) 1196–1211; authors' updated version, July 2004. https://doi.org/10.1137/S1052623497330963, https://www.ime.unicamp.br/~martinez/bmr.pdf
E. G. Birgin, J. M. Martínez, M. Raydan, Inexact spectral projected gradient methods on convex sets, IMA J. Numer. Anal. 23 (2003) 539–559. https://doi.org/10.1093/imanum/23.4.539
J. Barzilai, J. M. Borwein, Two-point step size gradient methods, IMA J. Numer. Anal. 8 (1988) 141–148. https://doi.org/10.1093/imanum/8.1.141
L. Grippo, F. Lampariello, S. Lucidi, A nonmonotone line search technique for Newton's method, SIAM J. Numer. Anal. 23 (1986) 707–716. https://doi.org/10.1137/0723046
M. Raydan, The Barzilai and Borwein gradient method for the large scale unconstrained minimization problem, SIAM J. Optim. 7 (1997) 26–33. https://doi.org/10.1137/S1052623494266365
D. P. Bertsekas, On the Goldstein–Levitin–Polyak gradient projection method, IEEE Trans. Automat. Control 21 (1976) 174–184. https://doi.org/10.1109/TAC.1976.1101194

10 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Robust Solutions of Optimization Problems Affected by Uncertain Probabilities II: A Self-Concordant Barrier for the Perspective ConstraintResearch Paper

Motivation

Robust optimization protects a decision against every scenario in an uncertainty set. When the uncertain data are probabilities, a natural uncertainty set is a ball around a nominal distribution measured by a φ-divergence (Kullback–Leibler, Burg entropy, χ², Hellinger and others). Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) show that the robust counterpart of a linear constraint over such a set is a finite convex system, and then ask whether that system is computationally tractable: can an interior-point method solve it in polynomial time?

For the Burg and Kullback–Leibler divergences the reformulated constraints (Eqs. (29) and (32) of the paper) have the shape $\lambda f(s_i/\lambda)\le\dots$ , a perspective constraint. Polynomial-time solvability by interior-point methods follows once the constraint set carries a self-concordant barrier in the sense of Nesterov and Nemirovski (Interior-Point Polynomial Algorithms in Convex Programming, SIAM 1994). Theorem 2 of the paper supplies such a barrier for every perspective constraint whose generating function satisfies a one-dimensional differential inequality. The same question arises for perspective and relative-entropy cones in conic optimization generally, so the criterion is of interest beyond φ-divergences.

Setting

A function $\varphi:F\to\mathbb R$ on an open convex set $F\subseteq\mathbb R^n$ is $\kappa$ -self-concordant ( $\kappa\ge0$ ) if it is three times continuously differentiable on $F$ and for every $y\in F$ and every direction $h\in\mathbb R^n$

\bigl|\nabla^3\varphi(y)[h,h,h]\bigr|\le 2\kappa\,\bigl(h^{\mathsf T}\nabla^2\varphi(y)h\bigr)^{3/2},

where $\nabla^k\varphi(y)[h,\dots,h]$ is the $k$ -th differential of $\varphi$ at $y$ in direction $h$ (Definition 1, p. 350). In Lean this is PhiDivRobust.Barrier.IsSelfConcordant κ F φ.

Let $f$ be a real function on $(0,\infty)$ . Its perspective is $g(s,y)=y\,f(s/y)$ for $s,y>0$ (perspective f). The constraint set (34) is

\{(s,y,z):\ y f(s/y)\le z,\ s\ge0,\ y\ge0\},

and its logarithmic barrier (35) is

\varphi_B(s,y,z)=-\ln\bigl(z-yf(s/y)\bigr)-\ln s-\ln y

(logBarrier f), finite on the open set $F_f=\{(s,y,z): s>0,\ y>0,\ yf(s/y)<z\}$ (barrierDomain f). Directions are $h=(h_1,h_2)$ for $g$ , with $h_1$ along $s$ and $h_2$ along $y$ , and $h\in\mathbb R^3$ for $\varphi_B$ .

Formalization targets

Goal: Theorem 2 (p. 350)

If $f$ is convex on $(0,\infty)$ and, for some $\kappa>0$ ,

|f'''(s)|\le\kappa\,\frac{f''(s)}{s}\qquad(s>0),\tag{33}

then $\varphi_B$ is $\bigl(2+\tfrac{\sqrt2}{3}\kappa\bigr)$ -self-concordant on $F_f$ .

Milestones (the displayed steps of the proof)

Eq. (37): $\nabla^2 g(s,y)[h,h]=f''(s/y)\bigl(h_1^2/y-2sh_1h_2/y^2+s^2h_2^2/y^3\bigr)$ .
The third differential of $g$ in terms of $f''(s/y)$ and $f'''(s/y)$ .
Under (33), inequality (36) with $\beta=3+\kappa\sqrt2$ :

\bigl|\nabla^3 g(s,y)[h,h,h]\bigr|\le\beta\,h^{\mathsf T}\nabla^2 g(s,y)h\,\sqrt{h_1^2/s^2+h_2^2/y^2}.

Lemma A.2 of den Hertog (1994), as quoted in the proof: if (36) holds with $\beta\ge0$ , then $\varphi_B$ is $(1+\beta/3)$ -self-concordant on $F_f$ .

Milestones 3 and 4 give the goal, since $1+\tfrac13(3+\kappa\sqrt2)=2+\tfrac{\sqrt2}{3}\kappa$ . A further item records the paper's application: $f(s)=-\log s$ (the Burg case) satisfies (33) with $\kappa=2$ .

Significance

The result. Theorem 2 turns a two-line calculus check on a scalar function into a certificate of polynomial-time solvability for a three-dimensional convex constraint. The paper uses it to conclude that the robust counterparts for the Burg entropy and Kullback–Leibler uncertainty sets are tractable, and the criterion applies to any other convex $f$ satisfying (33); for example $f(s)=s\log s$ satisfies it with $\kappa=1$ , which covers the relative-entropy cone. The constant $2+\tfrac{\sqrt2}{3}\kappa$ enters the complexity bound of any path-following method through the barrier parameter.

Formalizing it. The theorem is proved in the paper, but the decisive step is delegated to Lemma A.2 of den Hertog's monograph, which in turn belongs to the compatibility theory of Nesterov and Nemirovski. As far as is known none of these statements has a machine-checked proof. The mission produces a checked version of the compatibility lemma for perspective constraints, which is reusable for any barrier of the form $-\ln(z-g)-\ln s-\ln y$ , together with explicit second- and third-differential formulas for perspectives in Mathlib's iteratedFDeriv language. The printed third-differential display contains a typo (see below); the formal statements fix it.

Difficulty

The differential identities (milestones 1 and 2) are routine but heavy: they require computing iterated Fréchet derivatives of a composition with a quotient in two variables and matching them with one-variable iterated derivatives of $f$ . The inequality (milestone 3) is elementary real-variable algebra once the differentials are available.

The central difficulty is den Hertog's lemma. The obvious approach, bounding the three terms of $\nabla^3\varphi_B$ separately against $(\nabla^2\varphi_B)^{3/2}$ , fails: the cross term $-3\,(\nabla\omega\cdot h)\,\nabla^2 g[h,h]/\omega^2$ with $\omega=z-g$ couples the first and second differentials, and bounding it separately loses the constant $1+\beta/3$ . A further practical difficulty is that $F_f$ is open and convex only because the perspective of a convex function is jointly convex and continuous, which must itself be established.

Formalization scope

Points are $(s,y,z)\in\mathbb R\times\mathbb R\times\mathbb R$ and directions for $g$ are in $\mathbb R\times\mathbb R$ . Differentials are iteratedFDeriv ℝ k applied to the constant tuple $(h,\dots,h)$ ; $f''$ and $f'''$ are iteratedDeriv 2 f and iteratedDeriv 3 f. The power $x^{3/2}$ is Real.rpow, which is $0$ for $x<0$ ; this makes the Lean definition of self-concordance no weaker than the paper's. Real.log and division have junk values outside $F_f$ , but $F_f$ is open, so no differential at a point of $F_f$ sees them.

Committed conventions and disclosed deviations:

" $f:\mathbb R^+\to\mathbb R$ " is read as $f$ convex on the open half-line $(0,\infty)$ ; the Burg case $f=-\log$ is undefined at $0$ , and $f$ is only evaluated at $s/y$ with $s,y>0$ .
$f$ is assumed $C^3$ on $(0,\infty)$ . The page does not say so, but (33) uses $f'''$ and Definition 1 requires the barrier to be $C^3$ .
The printed third-differential display ends in $s^3h_x^3/y^5$ ; the correct term is $s^3h_2^3/y^5$ , and the Lean statement uses it. The milestone text keeps the printed version.
Lemma A.2 is stated with $\beta\ge0$ added. The quoted text says "if there exists a $\beta$ ", which is false for $\beta<0$ : with $f\equiv0$ , (36) holds for every $\beta$ and $\beta=-3$ would give a $0$ -self-concordant $-\ln z-\ln s-\ln y$ . The goal uses $\beta=3+\kappa\sqrt2>0$ and is unaffected.

A trivializing formalization is excluded. The self-concordance predicate requires $C^3$ regularity and quantifies over all directions $h\in\mathbb R^3$ , the domain is exactly $F_f$ (not a subset such as $\emptyset$ ), and $\kappa>0$ is as printed. The constant of the conclusion is tied to the same $\kappa$ as in (33).

Useful infrastructure, reusable beyond this mission: iterated derivatives of perspectives, joint convexity of perspectives, and the calculus of self-concordance (sums, $-\ln$ of a concave function composed with an affine map). Proofs of the milestones independently of the goal are welcome, as are proofs of the Burg item's consequence and of the analogous statement for $f(s)=s\log s$ .

Selected references

A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
D. den Hertog, Interior Point Approach to Linear, Quadratic and Convex Programming: Algorithms and Complexity, Kluwer Academic Publishers, 1994. https://doi.org/10.1007/978-94-011-1134-8
Yu. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. https://doi.org/10.1137/1.9781611970791

8 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Robust Solutions of Optimization Problems Affected by Uncertain Probabilities I: The Robust Counterpart of a Linear Constraint under φ-Divergence UncertaintyResearch Paper

Motivation

Many decision problems contain a constraint whose coefficients are an expectation under a probability vector that is not known exactly: an expected cost under uncertain scenario probabilities, an expected payoff of an asset under an estimated distribution, the expected demand in a newsvendor model. The probabilities are usually estimated from data, and a solution that is feasible for the estimate can be infeasible for the true distribution. Robust optimization protects against this by requiring the constraint to hold for every probability vector in an uncertainty region around the estimate.

A natural region is a ball in a φ-divergence, a family of statistical distances between probability vectors that contains the Kullback–Leibler divergence, the Burg entropy, the χ² distances, the Hellinger distance and the variation distance. Such balls arise as asymptotic confidence sets for the true distribution given observed frequencies (Pardo 2006), so the radius has a statistical meaning. Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) showed that the robust version of a linear constraint over such a ball is equivalent to a finite convex system involving the convex conjugate of φ. This reformulation is a standard tool in the later literature on distributionally robust optimization.

Setting

A φ-divergence function is a function $\phi:\mathbb R\to\mathbb R\cup\{+\infty\}$ that is convex on $[0,\infty)$ , finite on $(0,\infty)$ , and satisfies $\phi(1)=0$ ; the value $\phi(0)$ may be $+\infty$ . Examples are $\phi(t)=t\log t-t+1$ (Kullback–Leibler), $\phi(t)=-\log t+t-1$ (Burg), $\phi(t)=(t-1)^2$ (modified χ²) and $\phi(t)=|t-1|$ (variation). For $p,q\in\mathbb R^m$ with $q>0$ the φ-divergence is

I_\phi(p,q)=\sum_{i=1}^m q_i\,\phi\!\left(\frac{p_i}{q_i}\right),

and the conjugate of $\phi$ is $\phi^*(s)=\sup_{t\ge0}\{st-\phi(t)\}$ , a function with values in $\mathbb R\cup\{+\infty\}$ .

Fix $a\in\mathbb R^n$ , $B\in\mathbb R^{n\times m}$ with columns $b_i$ , $\beta\in\mathbb R$ , $C\in\mathbb R^{k\times m}$ with columns $c_i$ , $d\in\mathbb R^k$ , a nominal vector $q\in\mathbb R^m$ and a radius $\rho>0$ . The uncertainty region is

U=\{p\in\mathbb R^m\mid p\ge0,\ Cp\le d,\ I_\phi(p,q)\le\rho\},

where the linear constraints $Cp\le d$ can encode $e^\top p=1$ and any further information on $p$ . A decision $x\in\mathbb R^n$ satisfies the robust linear constraint if

(a+Bp)^\top x\le\beta\qquad\text{for all }p\in U. \tag{11}

Inequalities between vectors are componentwise throughout.

Formalization targets

Goal: Theorem 1

Assume $q>0$ and $q\in U$ . Then $x$ satisfies (11) if and only if there are $\eta\in\mathbb R^k$ and $\lambda\in\mathbb R$ with

a^\top x+d^\top\eta+\rho\lambda+\lambda\sum_{i}q_i\,\phi^*\!\left(\frac{b_i^\top x-c_i^\top\eta}{\lambda}\right)\le\beta,\qquad\eta\ge0,\ \lambda\ge0, \tag{13}

where $0\phi^*(s/0):=0$ for $s\le0$ and $0\phi^*(s/0):=+\infty$ for $s>0$ . The statement fixes no constants and no particular φ; it holds for the whole class.

Milestones

The proof in the paper has three displayed steps, which are the milestones. With the Lagrange function $L(p,\lambda,\eta)=(a+Bp)^\top x+\rho\lambda-\lambda I_\phi(p,q)+\eta^\top(d-Cp)$ and the dual objective $g(\lambda,\eta)=\sup_{p\ge0}L(p,\lambda,\eta)$ :

Closing identity. For $\lambda\ge0$ , $(\lambda\phi)^*(s)=\sup_{t\ge0}\{st-\lambda\phi(t)\}$ equals $\lambda\phi^*(s/\lambda)$ , with the convention above at $\lambda=0$ .
Eq. (15). For $q>0$ and $\lambda\ge0$ ,

g(\lambda,\eta)=a^\top x+d^\top\eta+\rho\lambda+\sum_{i=1}^m q_i(\lambda\phi)^*(b_i^\top x-c_i^\top\eta).

Duality. Under the hypotheses of Theorem 1, $x$ satisfies (11) if and only if $g(\lambda,\eta)\le\beta$ for some $\lambda\ge0$ , $\eta\ge0$ . This is split into the weak-duality direction and the strong-duality direction with attainment.

An additional item states Corollary 1, the specialization to $U=\{p\ge0,\ e^\top p=1,\ I_\phi(p,q)\le\rho\}$ , where the multiplier $\eta\in\mathbb R$ of the normalization is free in sign.

Significance

Theorem 1 turns a semi-infinite constraint, one inequality for each $p$ in a convex set, into a single convex inequality in $(x,\lambda,\eta)$ . The left side of (13) is jointly convex because $\lambda\phi^*(s/\lambda)$ is the perspective of a convex function. For the divergences of Table 4 of the paper the conjugate has a closed form, and the robust constraint becomes a linear, conic quadratic or self-concordant-barrier-representable constraint. The paper's applications (robust asset pricing, a robust newsvendor, and the tractability results of its §5) all start from this theorem, as do its Corollaries 2–5.

The theorem is proved in the paper; no machine-checked proof of it is known. Formalizing it adds a checked robust-counterpart theorem for φ-divergence regions, a reusable encoding of φ-divergences with extended values, and a strong-duality statement with attainment for convex programs whose constraint function takes the value $+\infty$ on the boundary of the orthant. It also records a correction: the paper states the theorem for $q\ge0$ , and that version is false (see Formalization scope).

Difficulty

The separation step (15) and the conjugate identity are elementary manipulations of suprema, but in extended arithmetic: $\phi$ may be $+\infty$ at $0$ , the conjugate may be $+\infty$ , and the case $\lambda=0$ follows its own convention. The central difficulty is the duality step. The worst-case problem is a convex program whose constraint $I_\phi(p,q)\le\rho$ is not a finite convex function on a closed set: for the Burg or χ² divergence it is $+\infty$ on the boundary of the orthant, and $U$ itself need not be closed. Textbook statements of Slater-type strong duality usually assume finite-valued convex functions on a closed domain, so they do not apply as stated. The statement also requires attainment of the dual minimum, not only the absence of a duality gap, and this is the part a naive limiting argument does not give.

Formalization scope

Conventions:

Vectors are Fin n → ℝ with the componentwise order; $B$ and $C$ are Matrix (Fin n) (Fin m) ℝ and Matrix (Fin k) (Fin m) ℝ; $b_i$ and $c_i$ are the columns fun j => B j i and fun j => C j i.
$\phi$ is ℝ → EReal, never $-\infty$ , finite on $(0,\infty)$ , with $\phi(1)=0$ and convexity on $[0,\infty)$ written out in EReal. $\phi(0)=+\infty$ is allowed, so the Burg, χ² and J divergences are covered.
$I_\phi(p,q)$ , $\phi^*$ , $(\lambda\phi)^*$ , $L$ , $g$ and the left side of (13) are EReal-valued. $\lambda\phi(t)$ is the EReal product, in which $0\cdot(+\infty)=0$ . The term $\lambda\phi^*(s/\lambda)$ is defined by an explicit case split at $\lambda=0$ , and $\lambda\sum_i q_i\phi^*(\cdot/\lambda)$ in (13) is read as $\sum_i q_i\,(\lambda\phi^*(\cdot/\lambda))$ with the convention applied term by term.
The paper's $\max_{p\ge0}$ in $g$ is a supremum; $\min_{\lambda,\eta\ge0}g\le\beta$ is stated in its attained form, $\exists\,\lambda\ge0,\eta\ge0$ with $g(\lambda,\eta)\le\beta$ .
$m$ and $k$ may be $0$ .

Corrected slip. The paper's standing assumption is $q\ge0$ . The third equality of (15) substitutes $p_i=q_it$ , which needs $q_i>0$ , and Theorem 1 is false for $q\ge0$ : with $m=k=2$ , $n=1$ , $\phi(t)=|t-1|$ , $q=(1,0)$ , both columns of $C$ equal to $(1,-1)^\top$ , $d=(1,-1)$ , $a=0$ , $B=(0\ \ 1)$ , $x=1$ , $\rho=1$ , $\beta=0$ , the vector $p=(1/2,1/2)$ lies in $U$ and violates (11), while $\eta=0$ , $\lambda=0$ satisfy (13). Every statement of the mission therefore assumes $q_i>0$ for all $i$ . The hypothesis $q\in U$ (the paper's "such that $q\in U$ ") and $\rho>0$ are kept.

Ruled-out trivializations: a conjugate taken as a supremum over all $t\in\mathbb R$ of a real-valued φ with junk values at $t<0$ is a different function; computing the $\lambda=0$ term as $0\cdot\phi^*(s/0)$ with Lean's $s/0=0$ makes it identically $0$ ; a real-valued, everywhere finite φ silently excludes the Burg, χ² and J divergences; dropping $q\in U$ or $\rho>0$ removes the Slater point and changes the theorem. The mission's definitions avoid all four.

Needed infrastructure: suprema of EReal-valued families over half-lines and orthants, the interchange of a supremum over a product with a finite sum, and a Lagrangian strong-duality theorem with attainment for a convex program with finitely many affine inequality constraints and one convex, possibly infinite-valued, inequality constraint with a Slater point in the interior of its domain. That duality theorem, and the φ-divergence definitions, are reusable beyond this mission, in particular for the paper's Corollaries 2–5 and for other distributionally robust formulations. Contributions of any of these pieces as separate theorems are welcome.

Selected references

A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
L. Pardo, Statistical Inference Based on Divergence Measures, Chapman & Hall/CRC, 2006. https://doi.org/10.1201/9781420034813
A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

12 thms2 active usersReviewed

Completed

Group Theory·Captain: dbenbenn

Cannon–Floyd–Parry: Thompson's group V is simpleTextbook

This mission formalizes §6 of J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, doi:10.5169/seals-87877: the definition of Thompson's group $V$ and Thompson's proof that $V$ is simple.

Motivation

Thompson's groups $T$ and $V$ , introduced in unpublished notes of Richard Thompson in 1965, were the first known examples of infinite, finitely presented, simple groups. The notes of Cannon, Floyd and Parry were written in part "to make available Thompson's unpublished proofs … of the simplicity of $T$ and $V$ " (p. 216); §6 is the proof for $V$ .

$V$ contains $T$ , which contains $F$ . Earlier missions on this platform formalize $F$ and its commutator subgroup (§1 and §4), its tree-diagram normal form (§2), its presentations (§3), and the simplicity of $T$ (§5). Unlike $T$ , the elements of $V$ need not be continuous: they cut the circle into pieces and rearrange them in any order, so $V$ contains every finite symmetric group.

Setting

The circle $S^1$ is $[0,1]$ with its endpoints identified, in Lean UnitAddCircle ( $\mathbb{R}/\mathbb{Z}$ ); $[x]$ denotes the image of $x \in \mathbb{R}$ . Maps compose right to left, $(fg)(t) = f(g(t))$ , and $[x, y] = xyx^{-1}y^{-1}$ .

The group $V$ (p. 240) consists of the right-continuous bijections of $S^1$ that map images of dyadic rationals to images of dyadic rationals, are differentiable except at finitely many images of dyadic rationals, and are linear with slope a power of $2$ on each maximal interval of differentiability. In Lean a permutation $f$ of the circle satisfies IsThompsonV f when it maps dyadic points to dyadic points and, for a finite set of dyadic breakpoints, is $[z] \mapsto [2^n z + c]$ on each half-open piece between consecutive breakpoints modulo $1$ . V is the subgroup generated by these maps; that they already form a group is the first milestone.

The elements. $A$ , $B$ , $C$ are $T$ 's generators, and $\pi_0$ (mapPi0) exchanges $[0, \tfrac12)$ and $[\tfrac12, \tfrac34)$ by $x \mapsto x/2 + \tfrac12$ and $x \mapsto 2x - 1$ . The words $X_0 = A$ , $X_n = A^{-(n-1)}BA^{n-1}$ , $C_n = A^{-(n-1)}CB^{n-1}$ , $\pi_1 = C_2^{-1}\pi_0C_2$ and $\pi_n = A^{-(n-1)}\pi_1A^{n-1}$ (p. 241) are defined once, as words in four symbols, and read both as maps of the circle and in $V_1$ .

The presented group $V_1$ (p. 242) is the free group on $A$ , $B$ , $C$ , $\pi_0$ modulo fourteen relators: the six relators of $T_1$ (§5), and eight more involving the $\pi_n$ , such as $\pi_1^2$ , $(\pi_2\pi_1)^3$ and $(\pi_1C_2)^3$ . In $V_1$ , $\Pi(n)$ is the subgroup generated by $\pi_0, \dots, \pi_{n-1}$ , $\Pi = \bigcup_n \Pi(n)$ , and an element is positive when it is a product of nonnegative powers of the $X_i$ .

Target

The goal is the sentence in which the notes state what §6 does, "In §6 we define $V$ and give Thompson's proof that $V$ is simple" (p. 216):

V \text{ is simple.}

The route is the section's own. Lemma 6.1 shows that $A$ , $B$ , $C$ , $\pi_0$ generate $V$ and satisfy the fourteen relations, so $V_1$ maps onto $V$ . Lemmas 6.2–6.8 establish how the $\pi_i$ move past the $X_j$ and $C_n$ , leading to Theorem 6.9, $V_1$ is simple, and hence $V_1 \cong V$ . The goal follows.

Significance

The result. $V$ is the third of Thompson's groups and the one whose elements rearrange pieces of the circle: it is infinite, finitely presented and simple, and it contains every finite group (through the finite symmetric groups). Together with $T$ it gave the first examples of infinite finitely presented simple groups.

Formalizing it. No machine-checked proof that $V$ is simple exists on this platform, and Mathlib has nothing on Thompson's groups. This mission reuses the formalization of $F$ and $T$ : $V_1$ 's first six relators are $T_1$ 's, and the proof of Theorem 6.9 applies Theorem 5.7 and Theorem 5.8 inside $V_1$ .

Difficulty

The central difficulty is the generation half of Lemma 6.1. The notes' proof uses tree diagrams with labelled leaves: every element of $V$ permutes the intervals of one standard dyadic partition onto those of another, $F$ moves any partition to a standard comb, and the subgroup generated by $\pi_0$ and $C_{n-2}$ acts as the full symmetric group on the comb's intervals. Each step is stated in one sentence; the milestones make each a separate statement.

The algebra of $V_1$ (Lemmas 6.2–6.6) is a chain of inductions. The proofs lean on two facts the notes use without isolating them: that $T_1$ maps to $V_1$ (so §5's lemmas hold in $V_1$ ), and the normal form $g = p\pi C_n^m q^{-1}$ in $V_1$ , stated inside the proof of Theorem 6.9. Both are milestones here. The notes also cite two facts about the finitary symmetric group $\Sigma$ without proof, its presentation and the behaviour of its proper quotients, and deduce $\Pi \cong \Sigma$ ; the proof of Theorem 6.9 uses all three, and each is a milestone.

What is left out

Figures 16–19, tree-diagram computations for relations 11) and 12); the relations are stated directly in Lemma 6.1.

Formalization scope

$V$ is a Subgroup (Equiv.Perm UnitAddCircle) generated by IsThompsonV. Half-open pieces make every element right-continuous; "linear" is read modulo $1$ , so a piece may wrap past $[0]$ , as a rotation does. Unlike $T$ , no lift to the line is available, since elements of $V$ need not be monotone.
$V_1$ is Mathlib's PresentedGroup on the four-element type FormalV. Relators are written out as $xyx^{-1}y^{-1}$ .
$\Sigma$ is SigmaPerm, the subgroup of Equiv.Perm ℕ of permutations moving finitely many points, and $s_i$ is the transposition of $i$ and $i + 1$ ; its presentation is a PresentedGroup on ℕ. $\Pi$ is taken as the subgroup of $V_1$ generated by all the $\pi_i$ , which is the union of the $\Pi(n)$ .
Lemma 6.1's surjection and the isomorphism $V_1 \cong V$ pin the images of the four symbols, so no isomorphism ignoring the generators satisfies them.
Reused platform theorems, which solutions may import: Theorem 3.4, Corollary 2.6, Lemma 4.2, Theorem 4.11, and from §5 Lemma 5.2, Lemmas 5.5 and 5.6, Theorem 5.7 and Theorem 5.8. The standard dyadic partitions of the tree-diagram milestone are the §2 bundle's IsStandardDyadicPartition.

Selected references

J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, §6 pp. 240–248. doi:10.5169/seals-87877

38 thms2 active usersReviewed

Completed

Mathematical Physics·Captain: Lucas

Microstate counting in dS₃: eigenvalue count vs. sphere partition functionResearch Paper

Motivation

Gibbons and Hawking conjectured that the cosmological horizon of a de Sitter static patch carries an entropy, computed semiclassically by the Euclidean gravitational path integral on the sphere. For three-dimensional de Sitter gravity the relevant quantity is $\log|Z^{S^3}_{\mathrm{grav}}|$ , whose leading term is the Gibbons–Hawking entropy $S_{\mathrm{GH}} = \pi\ell_{\mathrm{dS}}/(2G_N)$ . A microscopic account of this entropy — a count of states in some ordinary quantum or statistical system — is one of the long-standing goals of de Sitter holography.

Collier, Eberhardt and Mühlmann (arXiv:2501.01486) propose that pure dS $_3$ quantum gravity is dual to the double-scaled two-matrix integral of the complex Liouville string (arXiv:2409.17246). In §4.4 they test this by counting the "effective number of eigenvalues" of the matrix model and comparing $2\log N_{\mathrm{eff}}$ with $\log|Z^{S^3}_{\mathrm{grav}}|$ . The comparison reduces to explicit identities between elementary functions of the Liouville parameter $b$ ; this mission formalizes exactly those identities.

Setting

Fix a complex number $b$ with $-ib^2 \in \mathbb{R}_{>0}$ , i.e. $b^2 = i\beta$ with $\beta>0$ (the paper's footnote 2; then the central charge $c = 1+6(b+b^{-1})^2$ lies in $13+i\mathbb{R}$ ). Write $b^{-2} = (b^2)^{-1}$ and let $S_0\in\mathbb{R}$ be the genus-counting parameter of the matrix model.

Eigenvalue density (eq. (C.4)): for real $E$ ,

\rho_0(E) = \frac{2}{\pi}\,\sinh(-i\pi b^2)\,\sin\!\Big(-ib^2\,\operatorname{arccosh}\frac{E}{2}\Big).

First zero (§4.4): $E_0 = 2\cos(\pi b^{-2})$ .
Effective number of eigenvalues (eq. (4.32)): $N_{\mathrm{eff}} = \int_2^{E_0} e^{S_0}\rho_0(E)\,dE$ .
Microscopic entropy (eq. (4.33)): $S^{\mathrm{micro}}_{\mathrm{dS}} = 2\log N_{\mathrm{eff}}$ .
ZZ-instanton tension (eq. (4.34)): $\widehat T^{(b)}_{1,1} = \dfrac{8b^2\sin(\pi b^2)\sin(\pi b^{-2})}{1-b^4}$ and $T^{(b)}_{1,1} = e^{S_0}\,\widehat T^{(b)}_{1,1}$ .
Sphere normalization (eq. (4.4)): $C^{(b)}_{S^2} = 32\pi^4\Big(\dfrac{\sin(\pi b^2)\sin(\pi b^{-2})}{b^2-b^{-2}}\Big)^2$ .
Sphere partition function (eq. (4.5)): $Z^{S^3}_{\mathrm{grav}} \sim e^{2S_0}\,\dfrac{\sin(\pi b^2)^2\sin(\pi b^{-2})^2}{(b^{-2}-b^2)^2}$ , where $\sim$ is equality up to a $b$ -independent constant.

Formalization targets

Goal (eq. (4.35))

For any function $Z(b,S_0)$ whose modulus equals $K\cdot\big|e^{2S_0}\sin(\pi b^2)^2\sin(\pi b^{-2})^2/(b^{-2}-b^2)^2\big|$ for a fixed constant $K>0$ (the content of (4.5)), there is a real constant $c$ , independent of $b$ and $S_0$ , such that

S^{\mathrm{micro}}_{\mathrm{dS}}(b,S_0) = \log|Z(b,S_0)| + c \qquad\text{for all admissible } b \text{ and all } S_0.

This is the paper's statement that the matrix-model count reproduces the de Sitter entropy "regardless of the specific value of $Z^{S^3}_{\mathrm{grav}}$ ", up to the order-one constants that (4.37) later fixes.

Milestones

$E_0$ is real, $E_0>2$ , $\rho_0(E_0)=0$ , and $\rho_0$ is real and positive on $(2,E_0)$ (§4.4, App. C).
Closed form of $N_{\mathrm{eff}}$ (eqs. (4.32)–(4.33)).
The two expressions for $S^{\mathrm{micro}}_{\mathrm{dS}}$ in eq. (4.33).
$(\widehat T^{(b)}_{1,1})^2 \sim C^{(b)}_{S^2}$ (eq. (4.36)).

Significance

The identity (4.36) is the step the authors single out as "a genuinely nontrivial check": it holds for the complex Liouville string but, as they note, not for the Virasoro minimal string. The goal packages the argument of §4.4 into one exact statement, valid for every admissible $b$ (i.e. exactly in $G_N$ ), under the single physical input (4.5). The physical assumptions — the choice of cutoff at the first zero, the interpretation of $\log N^2$ as an entropy, and (4.5) itself — are not formalized; they enter as definitions and as the hypothesis on $Z$ . The mathematical content is a definite-integral evaluation plus trigonometric/hyperbolic identities for complex arguments.

Difficulty

The integral in (4.32) has a complex-looking integrand, a branch of $\operatorname{arccosh}$ , and an upper limit given by a complex cosine; one must first show that everything is real in the admissible regime and then evaluate the integral exactly, including the endpoint behaviour at $E=2$ where $\operatorname{arccosh}$ is not differentiable. The entropy statements additionally involve the complex principal logarithm, so one must control the argument (positivity) of $N_{\mathrm{eff}}$ and of the tension ratio; identities such as $\log(e^{S_0}x) = S_0+\log x$ fail for general complex $x$ .

Formalization scope

$b\in\mathbb{C}$ with the hypothesis $\exists\beta>0,\ b^2 = i\beta$ ; all objects depend on $b$ only through $b^2$ .
$\rho_0 : \mathbb{R}\to\mathbb{C}$ uses Mathlib's Real.arcosh (defined as $\log(x+\sqrt{x^2-1})$ ); its values for $E<2$ never enter.
$N_{\mathrm{eff}}$ is the oriented interval integral from $2$ to $\operatorname{Re}E_0$ ; milestone 1 shows $E_0$ is real, so taking the real part loses nothing.
$\log$ is the complex principal logarithm (Complex.log), and $S^{\mathrm{micro}}_{\mathrm{dS}}$ is complex-valued; the goal forces it to equal a real number.
The " $\sim$ " of (4.5) is encoded as a constant factor $K>0$ in the modulus; the " $\sim$ " of (4.36) as a nonzero $b$ -independent complex constant.
A trivialization is ruled out: the goal quantifies $c$ before $b$ and $S_0$ , and $K>0$ is required.

Selected references

S. Collier, L. Eberhardt, B. Mühlmann, A microscopic realization of dS $_3$ , arXiv:2501.01486 (2025). https://arxiv.org/abs/2501.01486
S. Collier, L. Eberhardt, B. Mühlmann, V. A. Rodriguez, The complex Liouville string, arXiv:2409.17246 (2024). https://arxiv.org/abs/2409.17246
G. W. Gibbons, S. W. Hawking, Cosmological event horizons, thermodynamics, and particle creation, Phys. Rev. D 15 (1977) 2738. https://doi.org/10.1103/PhysRevD.15.2738

6 thms2 active usersReviewed

Completed

Functional Analysis Mathematical Physics·Captain: Lucas

Uma Breve Introdução à Matemática da Mecânica Quântica I: Princípio da Incerteza de HeisenbergTextbook

Motivation

Heisenberg's uncertainty principle is the first quantitative statement a student meets about the incompatibility of position and momentum measurements in quantum mechanics. In A. O. Lopes' textbook Uma Breve Introdução à Matemática da Mecânica Quântica (31º Colóquio Brasileiro de Matemática, IMPA, 2017), written for mathematics students with no physics background, it is the capstone of Chapter 8 (Princípio da Incerteza e o Pacote de Onda Gaussiano), Teorema 8.2, p. 131. It collects the operator formalism built in Chapters 1, 3 and 4 — position and momentum operators, commutators, expected values — into one inequality. This mission is the first of a series formalizing the capstone results of the book.

Setting

A wave function is a map $\psi:\mathbb R^n\to\mathbb C$ . The book uses the $L^2$ inner product $\langle \varphi,\psi\rangle=\int_{\mathbb R^n}\varphi(x)\,\overline{\psi(x)}\,dx$ (linear in the first slot) and the norm $|\psi|=\langle\psi,\psi\rangle^{1/2}$ . A state is a wave function with $|\psi|=1$ . Fix $n\ge 1$ , an index $j\in\{1,\dots,n\}$ and the (reduced) Planck constant $\hbar>0$ .

The position operator is $(X_j\psi)(x)=x_j\,\psi(x)$ , with domain $D(X_j)=\{\psi\in L^2 : x_j\psi\in L^2\}$ .
The momentum operator is $(P_j\psi)(x)=-i\hbar\,\dfrac{\partial\psi}{\partial x_j}(x)$ (Definição 1.20), with domain $D(P_j)$ the $C^1$ functions of compact support.
The commutator of two operators is $[A,B]=AB-BA$ (Definição 3.1).
The expected value of $A$ in $\psi$ is $E_\psi(A)=\dfrac{\langle A\psi,\psi\rangle}{\langle\psi,\psi\rangle}$ (Definição 8.1, p. 125, and p. 128).
The dispersion of $A$ in $\psi$ is $\Delta_\psi(A)=\big|\,(A-E_\psi(A)\,I)\psi\,\big|$ (Definição 8.2).
The Gaussian wave packet with parameters $a>0$ , $x_0,p_0\in\mathbb R^n$ is $\psi(x)=(2\pi a^2)^{-n/4}\,e^{-|x-x_0|^2/(4a^2)}\,e^{\,i\langle p_0,x\rangle/\hbar}$ (Definição 8.3).

Formalization targets

Goal — Teorema 8.2 (Heisenberg)

For every state $\psi\in D(X_j)\cap D(P_j)$ ,

\Delta_\psi(X_j)\,\Delta_\psi(P_j)\;\ge\;\frac{\hbar}{2}.

Milestones

Lema 3.2 (canonical commutation relations): $[X_k,X_j]=[P_k,P_j]=0$ , $\tfrac{i}{\hbar}[P_j,X_j]=\mathrm{Id}$ , and $\tfrac{i}{\hbar}[P_j,X_k]=0$ for $j\ne k$ .
p. 23 — $X_j$ is symmetric: $\langle X_j\psi,\varphi\rangle=\langle\psi,X_j\varphi\rangle$ on $D(X_j)$ .
pp. 26–27 — $P_j$ is symmetric: $\langle P_j\psi,\varphi\rangle=\langle\psi,P_j\varphi\rangle$ on $D(P_j)$ .
Proposição 8.1 — $\Delta_\psi(A)=0$ if and only if $\psi$ is an eigenfunction of $A$ .
Definição 8.3 / p. 133 — the Gaussian packet is a state with $E(X_j)=(x_0)_j$ , $E(P_j)=(p_0)_j$ , $\Delta(X_j)=a$ , and it attains equality $\Delta(X_j)\,\Delta(P_j)=\hbar/2$ .

Significance

The inequality is the prototype of all Robertson-type uncertainty relations and is the point where the commutator formalism of the book produces a numerical, physically testable consequence. Milestone 5 shows the constant $\hbar/2$ cannot be improved. The mathematics is classical and fully proved in the source; what this mission adds is a machine-checked version of the textbook's operator calculus on $L^2(\mathbb R^n)$ — integration by parts for compactly supported $C^1$ functions, symmetry of $X_j$ and $P_j$ , commutation relations, and explicit Gaussian integrals — reusable by later missions of the series (Ehrenfest's theorem, density operators, quantum statistical mechanics).

Difficulty

The algebraic core is a short Cauchy–Schwarz argument, but it silently uses facts about unbounded operators: that $\langle\psi,[P_j,X_j]\psi\rangle$ may be rewritten as $\langle P_j\psi,X_j\psi\rangle-\langle X_j\psi,P_j\psi\rangle$ requires integration by parts with vanishing boundary terms, and the reduction to mean-zero observables requires the expected values to be real. Each of these needs integrability bookkeeping that the book leaves implicit. The Gaussian milestone requires evaluating first and second moments of Gaussian integrals in $n$ dimensions.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure; wave functions are plain functions ℝⁿ → ℂ (not $L^2$ classes), operators are maps on such functions, and domains are imposed as explicit hypotheses (InPositionDomain, InMomentumDomain).
The partial derivative $\partial/\partial x_j$ is the Fréchet derivative applied to the $j$ -th basis vector.
Integrals are Bochner integrals, which return $0$ for non-integrable integrands; every statement carries domain hypotheses guaranteeing integrability, so this junk value never enters a meaningful claim.
Expected values are complex numbers by definition; for symmetric operators they are real, which is part of what solvers must prove.
The goal is not vacuous: $D(P_j)$ contains nonzero compactly supported $C^1$ functions, which can be normalized.

Contributions welcome: integration-by-parts lemmas on $\mathbb R^n$ for compactly supported $C^1$ functions, Gaussian moment computations, and an abstract Robertson inequality.

Selected references

A. O. Lopes, Uma Breve Introdução à Matemática da Mecânica Quântica, 31º Colóquio Brasileiro de Matemática, IMPA, 2017. Extended version: http://mat.ufrgs.br/~alopes/hom/livroquantum.pdf
S. Gustafson, I. M. Sigal, Mathematical Concepts of Quantum Mechanics, Springer. https://doi.org/10.1007/978-3-030-59562-3

7 thms2 active usersReviewed

Completed

Group Theory·Captain: dbenbenn

Cannon–Floyd–Parry: Thompson's group T is simpleTextbook

This mission formalizes §5 of J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, doi:10.5169/seals-87877: the definition of Thompson's group $T$ and Thompson's proof that $T$ is simple.

Motivation

Thompson's groups $T$ and $V$ , introduced in unpublished notes of Richard Thompson in 1965, were the first known examples of infinite, finitely presented, simple groups. Every finitely presented simple group known before them was finite. The notes of Cannon, Floyd and Parry were written in part "to make available Thompson's unpublished proofs … of the simplicity of $T$ and $V$ " (p. 216), and §5 is that proof for $T$ .

$T$ is the circle's counterpart of Thompson's group $F$ . Earlier missions on this platform formalize $F$ and its commutator subgroup (§1 and §4 of the same notes), its tree-diagram normal form (§2), and its two presentations (§3). $F$ is not simple: its abelianization is $\mathbb{Z}^2$ . $T$ is simple, it has elements of finite order (the generator $C$ below has order $3$ ), and it contains $F$ as the stabilizer of a point.

Setting

The group $T$ (pp. 233–234) consists of the piecewise linear homeomorphisms of $S^1$ that map images of dyadic rationals to images of dyadic rationals, are differentiable except at finitely many images of dyadic rationals, and have slopes that are powers of $2$ . In Lean a permutation $f$ of the circle satisfies IsThompsonCircle f when it has a lift to the line: an order isomorphism $L$ of $\mathbb{R}$ with $L(x+1) = L(x) + 1$ and $f[x] = [L(x)]$ , mapping dyadic rationals to dyadic rationals, and affine with slope a power of $2$ between consecutive integer translates of finitely many dyadic breakpoints. T is the subgroup generated by these maps. That they already form a group is the first milestone.

The elements $A$ , $B$ , $C$ (Example 5.1). $A$ and $B$ are the generators of $F$ from the §1 mission (mapA, mapB), carried to the circle by toCircle, which sends an order isomorphism $g$ of $[0,1]$ to $[x] \mapsto [g(x)]$ . $C$ (mapC) is given on $[0,1]$ by $x/2 + 3/4$ , $2x - 1$ and $x - 1/4$ on $[0, \tfrac12]$ , $[\tfrac12, \tfrac34]$ and $[\tfrac34, 1]$ . symT sends the formal symbols $A$ , $B$ , $C$ to these three maps.

The presented group $T_1$ (p. 236) is the free group on formal symbols $A$ , $B$ , $C$ modulo six relators:

[AB^{-1}, A^{-1}BA],\quad [AB^{-1}, A^{-2}BA^2],\quad C^{-1}B(A^{-1}CB),

((A^{-1}CB)(A^{-1}BA))^{-1}B(A^{-2}CB^2),\quad (CA)^{-1}(A^{-1}CB)^2,\quad C^3.

In $T_1$ , $X_0 = A$ and $X_n = A^{-(n-1)}BA^{n-1}$ (XT1); $C_0 = 1$ and $C_n = A^{-(n-1)}CB^{n-1}$ (CT1) for $n \ge 1$ . An element is positive (IsPositiveT1) when it is a product of nonnegative powers of the $X_i$ .

Target

The goal is the sentence in which the notes state what §5 does, "In §5 we define $T$ and give Thompson's proof that $T$ is simple" (p. 216):

T \text{ is simple.}

The route is the section's own. Lemma 5.2 shows that $A$ , $B$ , $C$ generate $T$ and satisfy the six relations, so $T_1$ maps onto $T$ (Lemma 5.3). Lemmas 5.4–5.6 and a normal form (Theorem 5.7, every $g \in T_1$ is $p\,C_n^m q^{-1}$ with $p$ , $q$ positive and $m < n + 2$ ) lead to Theorem 5.8, $T_1$ is simple, and hence to Corollary 5.9, $T_1 \cong T$ . The goal follows.

Significance

The result. The simplicity of $T$ is one of the two facts that made Thompson's groups famous: $T$ is an infinite, finitely presented, simple group. Corollary 5.9 gives more, an explicit presentation of $T$ on three generators and six relators.

Formalizing it. No machine-checked proof that $T$ is simple exists on this platform, and Mathlib has nothing on Thompson's groups. The proof in the notes is short and complete. This mission connects the analytic definition of $T$ with the combinatorial group $T_1$ , reusing the platform's formalization of $F$ : the presentation of $F$ (Theorem 3.4), its normal form (Corollary 2.7), and the fact that its proper quotients are Abelian (Theorem 4.3).

Difficulty

The algebra of $T_1$ (Lemmas 5.5 and 5.6) is a chain of explicit inductions. The substance lies at two points.

The first is Theorem 5.7. The notes' proof that the set of elements $p\,C_n^m q^{-1}$ is closed under multiplication moves $q_1^{-1}p_2$ past $C_j^i$ and $C_l^k$ using the normal form of $F$ , transported into $T_1$ through Lemma 5.4, and then re-indexes, all inside the abstract group $T_1$ with no geometry to lean on.

The second is the analytic side of Lemma 5.2. Generation reduces an arbitrary $f \in T$ to an element of $F$ by composing with $C$ and with an element of $F$ that moves $f([0])$ to $[\tfrac34]$ . That needs the fact that an element of $T$ fixing $[0]$ comes from $F$ , which the notes state in one line. The relations are identities between explicit piecewise linear maps of the circle.

What is left out

The remark that $T$ is conjugate to a group of $C^\infty$ diffeomorphisms (Ghys–Sergiescu, p. 234). It is not used.
Tree diagrams for $T$ and Figures 11–15. The notes use them only to verify relations 3)–6), and those relations are stated directly in Lemma 5.2.
The observation on p. 237 that $C_n$ permutes $n + 2$ intervals cyclically, given "to gain some insight" and not used afterwards.

Formalization scope

$T$ is a Subgroup (Equiv.Perm UnitAddCircle) generated by IsThompsonCircle. The lift makes every element an orientation-preserving homeomorphism, so continuity is not stated separately. Unlike for $F$ , the condition that dyadics map to dyadics cannot be dropped: an irrational rotation satisfies every other clause.
$T_1$ is Mathlib's PresentedGroup on the three-element type FormalABC. Relators are written out as $xyx^{-1}y^{-1}$ , not with commutator notation.
Lemma 5.3 and Corollary 5.9 pin the images of the three symbols, so no isomorphism that ignores the generators can satisfy them. Lemma 5.4 pins the images of $A$ and $B$ .
Reused platform theorems, which solutions may import: Theorem 3.4 ( $F_1 \cong F$ ), Corollary 2.6 ( $A$ , $B$ generate $F$ ), Lemma 4.2, Corollary 2.7, Lemma 2.8, Theorem 4.3, line (3.2), and Theorem 4.11 ( $F$ is totally ordered, hence torsion-free).
Welcome beyond the milestones: §6's group $V$ , whose presentation extends $T_1$ .

Selected references

J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, §5 pp. 233–240. doi:10.5169/seals-87877
É. Ghys, V. Sergiescu, Sur un groupe remarquable de difféomorphismes du cercle, Comment. Math. Helv. 62 (1987) 185–239. doi:10.1007/BF02564445

26 thms2 active usersReviewed

Completed

Machine Learning Optimization·Captain: ajax

Vathek I: Tiled graft training preserves the mathematical updateResearch Paper

Motivation

Modern machine-learning systems are routinely assembled by grafting: pretrained components (an encoder, a decoder) are re-used inside a new architecture, parts of them are frozen, and only selected coordinates are trained. When the full computation does not fit in memory, practitioners cut the loss into tiles (microbatches, row blocks, vocabulary shards), accumulate gradient contributions, and apply the optimizer once. Every memory-constrained trainer assumes this tiled schedule computes the same update as the monolithic one — but the folklore proof hides real failure modes: updating parameters after each tile, averaging tile means, clipping per tile, detaching a frozen component's input, or saving a weights-only checkpoint all silently change the learner.

This mission turns that folklore into a theorem with explicit hypotheses. The design source is the Vathek Graft white paper (Davis, 2026), which proposes an open-predicate extractor trained as a graft and makes the schedule-preservation claim its first proof obligation (Theorem T0). The architectural precedents are established: parallel set-based extraction (DetIE), set-prediction objectives, pointer-generator copying, and low-rank adaptation of frozen bases. What none of them supplies is the exact-arithmetic statement that the memory-saving row schedule preserves the mathematical update — that is the target here.

Setting

Fix finite-dimensional spaces: logical parameters $w \in W = \mathbb{R}^d$ , of which only coordinates $j \in T$ are trainable ( $P_T$ zeroes frozen coordinates), and a shared-state space $V = \mathbb{R}^m$ . One training frame $\xi$ carries a differentiable shared computation $h_\xi : W \to V$ (the donor encoder plus shared projections), finitely many occurrence losses $f_i : W \times V \to \mathbb{R}$ with fixed coefficients $\alpha_i$ over a finite occurrence set $I$ , and all discrete choices, fixed during one logical update. The monolithic objective is

L_\xi(w) = \sum_{i \in I} \alpha_i\, f_i\big(w, h_\xi(w)\big).

A tile partition $\mathcal{B} = (B_1, \dots, B_q)$ splits $I$ into pairwise-disjoint tiles. The tiled evaluator streams the tiles through an accumulator of three slots — running loss, direct parameter-gradient contribution $A$ , shared cotangent $C$ — everything read at the same pre-update point $w_0$ , and finishes with one reverse pass:

g_{\mathrm{tile}} = A + Dh_\xi(w_0)^{\top} C.

Then the gradient is projected to trainable coordinates, globally clipped at radius $c$ , and a deterministic optimizer $U$ is applied exactly once: $\operatorname{Step}(S, \xi) = U\big(S, C_c(P_T\, g)\big)$ , where $S$ is the complete transition-relevant state (parameters, optimizer moments, step counter). One concrete masked-optimizer instance (masked AdamW) is included so "no decay on frozen coordinates" is a theorem, not a hope.

Formalization targets

The goal theorem packages exact one-step, trajectory, and restart preservation:

L_{\mathrm{tile}}(w_0) = L_\xi(w_0), \qquad g_{\mathrm{tile}} = \nabla L_\xi(w_0), \qquad \operatorname{Step}_{\mathrm{tile}}(S,\xi) = \operatorname{Step}_{\mathrm{mono}}(S,\xi),

and, by induction over a deterministic frame sequence, equality of the tiled and monolithic state trajectories, plus restart equality: saving at any completed update boundary $a \le n$ and reloading the round-tripped structural snapshot preserves the remaining trajectory,

\operatorname{Run}_{\mathrm{tile}}\big(\operatorname{reload}(S_a),\, a{:}n\big) = \operatorname{Run}_{\mathrm{mono}}(S_0,\, 0{:}n).

Twelve milestones build the result: partition flattening; weighted partition sums; the shared-path chain rule $\nabla[f \circ (\mathrm{id}, h)] = \nabla_1 f + Dh^{\top} \nabla_2 f$ ; linearity of the reverse pass over summed cotangents; the streaming-accumulator invariant and order independence; frozen-input differentiation with a concrete nonzero witness ( $\theta \mapsto 6\theta$ through a frozen donor gives gradient $66$ at $\theta = 2$ ); projection–clipping–optimizer congruence; one-step equivalence; trajectory equivalence; checkpoint round trip; restart equivalence; and the full two-tile non-vacuity witness, whose tiled gradient is the nonzero $105/2$ while its detached (input-frozen) variant falsely gives $0$ .

Significance

The result itself. Each clause rules out a real implementation bug: per-tile means change the objective on uneven tiles; updating after each tile reads moved parameters; clipping per tile differs from global clipping (gradients $10$ and $-9$ sum to $1$ , but clipped-then-summed give $0$ ); a weights-only checkpoint loses optimizer state and changes the resumed trajectory. A verified tiled trainer — or a verified compiler schedule for one — can cite this mission's lemmas as its exactness certificate.

What formalizing it adds. The paper states Theorem T0 informally with a proof sketch; no machine-checked version exists. The load-bearing content is precisely the discipline of hypotheses: the certificates that per-occurrence gradients are genuine derivatives (partial derivatives alone do not give the chain rule), the single pre-update point for all tiles, and the complete transition state. Follow-on missions in the same vocabulary (source-byte integrity, masked normalization, matching invariance, numerical refinement, resource bounds) can import these definitions.

Difficulty

The analysis is elementary; the danger is vacuity and silent strengthening. A statement that hypothesizes "the tiled gradient is correct" proves nothing; one that hypothesizes differentiability of every branch at every point in a way no real frame satisfies proves nothing either. The encoding must let tiles be empty and uneven, let the occurrence set be empty (zero objective, not division by zero), quantify certificates only at the points used, and keep the optimizer deterministic-but-arbitrary. The counterexamples above are disproof fixtures: a correct statement survives all of them without ad-hoc exclusions.

Formalization scope

Parameters are EuclideanSpace ℝ (Fin d); gradients use HasGradientAt with genuine Fréchet derivatives paired by inner-product duality, and the reverse pass is ContinuousLinearMap.adjoint — no uninterpreted gradient oracle appears anywhere. Partitions are lists of Finsets; the accumulator is an executable fold. The checkpoint is a real-valued structural snapshot (coordinate lists); finite-byte codecs and floating-point associativity are explicitly out of scope — the theorem is exact-arithmetic. A trivializing formalization (defining the tiled gradient as the monolithic one, or hypothesizing the conclusion) is ruled out: milestone M12 exhibits a concrete instance with nonzero gradient that satisfies every hypothesis, and the detachment mutant shows the hypotheses have teeth.

Definitions are shared across the whole mission series under the VathekProof namespace: the frame, derivative-certificate, state, and optimizer files are reusable beyond this mission. Contributions welcome on any milestone; the witness computations (M06, M12) are self-contained entry points.

Selected references

Davis, Vathek Graft: A Proof and Evidence Programme, mission-source white paper v1.0, 2026 (§4–6, Appendix A) — the theorem source; private document, cited by section.
Vasilkovsky et al., DetIE: Multilingual Open Information Extraction Inspired by Object Detection, 2022. https://arxiv.org/abs/2206.12514
See, Liu, Manning, Get To The Point: Summarization with Pointer-Generator Networks, ACL 2017. https://aclanthology.org/P17-1099/
Hu et al., LoRA: Low-Rank Adaptation of Large Language Models, 2021. https://arxiv.org/abs/2106.09685
Loshchilov, Hutter, Decoupled Weight Decay Regularization, ICLR 2019. https://arxiv.org/abs/1711.05101

17 thms2 active usersReviewed

Completed

Combinatorics Mathematical Physics·Captain: ShapeZero

The role postulates force exactly seven pointsTextbook

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) reaches the Fano plane — the seven-point, seven-line configuration behind the seven imaginary units of the octonions — by a combinatorial route (C1 Formal Proofs, §3). Points are arranged in Steiner triple systems, and each point of each line is given one of three roles. The model's claim is that the role postulates alone force the number of points to be exactly seven. This mission proves that claim.

What this mission does NOT prove.

Not that the system is the Fano plane. It proves the point count is $7$ . That every Steiner triple system on $7$ points is the Fano plane up to relabelling is a classical result, but it is not formalized here.
Not the modelling premise. Why lines have three points, and why there are three roles, is an input of the model, not derived here.
Not the later steps from the Fano plane to the octonions, and from there to the node size $n = 3$ and $\mathfrak{u}(3)$ .

Two corrections to C1 §3 built into this mission.

At least one point is required. The empty system — no points, no lines — satisfies every condition vacuously and has $0$ points, so C1 Theorem 3.6 as stated is false for it. The goal carries the hypothesis $0 < n$ . This is proved (in Lean, locally): the empty system is a Steiner triple system with a role colouring, so the statement without $0 < n$ is false.
C1 Theorem 3.3(a) is not used. Its condition "any two lines meet" does not force $7$ points: it also holds for a single triple ( $3$ points) and a single point, where there is no pair of lines to fail. This mission uses the role postulates instead.

Setting

Fix a natural number $n$ and take the points $\{0, \dots, n-1\}$ . A Steiner triple system is a family of subsets, called lines, such that

every line has exactly $3$ points, and
every pair of distinct points lies on exactly one line.

A role colouring assigns to each point $x$ and line $\ell$ a role $\rho(x, \ell) \in \{0, 1, 2\}$ such that

the three points of a line get three different roles;
completeness: every point takes every role at least once, on some line through it;
minimality: every point takes every role at most once — two different lines through $x$ give $x$ different roles.

In Lean these are RolesForceSeven.STS n and RolesForceSeven.RoleColouring S role, with points Fin n and lines Finset (Fin n).

Formalization targets

Goal: the role postulates force exactly seven points

n \ge 1,\ \text{a Steiner triple system on } n \text{ points with a role colouring} \;\Longrightarrow\; n = 7 .

This is RolesForceSeven.roles_force_seven. It asserts the point count only.

Milestones

M1 (replication count). In any Steiner triple system, every point lies on exactly $r$ lines with $2r + 1 = n$ .
M2 (three lines per point). Under a role colouring, every point lies on exactly $3$ lines.

Corollaries

A — the Fano plane has a role colouring. The Fano plane on $\{0, \dots, 6\}$ , with lines $\{i, i+1, i+3\}$ modulo $7$ , admits a role colouring. Without this the goal could be vacuously true.
B — AG(2, 3) is excluded (C1 Corollary 3.7): no Steiner triple system on $9$ points has a role colouring.

Significance

The result itself. It turns the model's role postulates into a precise count: whatever the Steiner triple system, if it carries a role colouring and has a point, it has exactly seven points. Corollary A shows the conditions are satisfiable, and Corollary B rules out the next Steiner triple system, AG(2, 3), explicitly.

Formalizing it. The C1 statement omits the non-emptiness hypothesis and is false for the empty system; the formal statement makes the hypothesis explicit and shows it is needed. The numerical check (Fano plane: $48$ role colourings; AG(2, 3): $0$ ; single triple: $0$ ) is replaced by a proof for every $n$ .

Numerical cross-check

system	points	lines through each point	role colourings
Fano plane	7	3	48
AG(2, 3)	9	4	0
single triple	3	1	0
empty system	0	—	vacuous (all conditions hold)

Difficulty

Moderate. The central step is the replication count: the lines through a point $x$ must be shown to cover every other point exactly once, two at a time, which is a double-counting argument over the pairs through $x$ . The role postulates then fix the replication number at three. The Fano plane corollary is a finite check.

Formalization scope

Points are Fin n; lines are finite sets of points, with no ambient geometry assumed.
The role function is total, Fin n → Finset (Fin n) → Fin 3; only its values on pairs $x \in \ell$ with $\ell$ a line matter.
Completeness and minimality are both hypotheses; the goal uses both.
$0 < n$ is necessary: without it the empty system is a counterexample (proved).
The conclusion is the number $7$ , not an isomorphism with the Fano plane.

Selected references

Wikipedia, Steiner system (Steiner triple systems, replication number). https://en.wikipedia.org/wiki/Steiner_system
Wikipedia, Fano plane. https://en.wikipedia.org/wiki/Fano_plane
Wikipedia, Octonion (Fano plane mnemonic for the multiplication of imaginary units). https://en.wikipedia.org/wiki/Octonion

7 thms2 active usersReviewed

Completed

Combinatorics Machine Learning Probability·Captain: naimengye

Understanding Machine Learning XXIV: Compression BoundsTextbook

Motivation

The book has characterized learnability through uniform convergence and through stability; Chapter 30 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), gives a third sufficient condition, compression: if a learning algorithm's output can be reconstructed from a small subsequence of $k$ training examples, then the error on the remaining examples estimates the true error, and the algorithm generalizes with a bound of order $k\log(m/\delta)/m$ (Theorem 30.2, Littlestone and Warmuth). The bound is a union bound over the $m^k$ possible index sequences of a held-out estimate that follows from Bernstein's inequality (Lemma 30.1), and in the consistent case it gives $L_D \le 8k\log(m/\delta)/m$ (Corollary 30.3). Classes admitting such compression schemes include axis-aligned rectangles ( $k = 2d$ ), homogeneous halfspaces ( $k = d$ , through the minimal-norm point of the convex hull and Carathéodory's theorem), separating polynomials by reduction, and any margin-separable data ( $k \le 1/\gamma^2$ , through the Perceptron). Whether every class of finite VC dimension has a compression scheme of size $O(d)$ is Warmuth's problem, open when the book was written.

Setting

A sample $S = (z_1, \dots, z_m)$ is drawn i.i.d. from $D$ ; a selection rule picks $(i_1, \dots, i_k) \in [m]^k$ (repetitions allowed), a reconstruction map $B : Z^k \to H$ produces $A(S) = B(z_{i_1}, \dots, z_{i_k})$ , and $V$ is the set of positions not selected, with $L_V$ the average loss over them. The loss takes values in $[0,1]$ . A class $H$ has a compression scheme of size $k$ (Definition 30.4) if for every $m \ge 1$ there are such $A$ and $B$ with $B(S_{A(S)})$ correct on every sample labeled by a member of $H$ ; the unrealizable version (Definition 30.5) asks $B(S_{A(S)})$ to be an empirical risk minimizer on every sample.

Formalization targets

Goal: Theorem 30.2

For a $[0,1]$ -valued loss, $k \ge 1$ , $m \ge 2k$ , any reconstruction map $B$ and any selection rule, with probability at least $1 - \delta$ over $S \sim D^m$ ,

L_D(A(S)) \le L_V(A(S)) + \sqrt{L_V(A(S))\,\frac{4k\log(m/\delta)}{m}} + \frac{8k\log(m/\delta)}{m}.

Milestones

Lemma 30.1 (the held-out Bernstein bound); Corollary 30.3 (the consistent case); Lemma 30.6 (realizable schemes give unrealizable schemes); the compression scheme of size $2d$ for axis-aligned rectangles (§30.2.1); the separation property of the minimal-norm point of the convex hull (§30.2.2). Further items: the size- $d$ scheme for homogeneous halfspaces and the margin scheme of §30.2.4.

Significance

Compression bounds are the cleanest generalization argument in the book: no complexity measure of the class enters, only the number of examples needed to encode the output, and the resulting bound is data-dependent through $L_V$ . They explain why support vector machines and the Perceptron generalize in terms of the number of support vectors or updates, and they underlie the sample-compression view of learning that connects to Chapters 9 and 15. Lemma 30.6 shows that compression is robust to label noise in the binary case. The halfspace scheme is a small piece of convex geometry of independent interest, and Warmuth's question about VC classes, settled in the affirmative for finite size by Moran and Yehudayoff after the book appeared, remains open in the form $O(d)$ .

Difficulty

Lemma 30.1 is Bernstein's inequality for the $n$ held-out losses with variance at most $L_D(h_T)$ , followed by solving the resulting quadratic in $\sqrt{L_D}$ to move the risk from the right-hand side to $L_V$ ; the constant $4$ comes out of that step (the exact value is about $3.19$ ). Theorem 30.2 is a union bound over the $m^k$ index sequences with $\delta' = m^k\delta$ , using $|V| \ge m - k \ge m/2$ and $\log(m^k/\delta') \le k\log(m/\delta')$ , which needs $k \ge 1$ ; formally the event for the learner is contained in the union of the events of Lemma 30.1 for each fixed index sequence, so no measurability of the selection rule is needed. Corollary 30.3 is immediate. Lemma 30.6 applies the realizable scheme to the subsample on which an ERM hypothesis is correct. The rectangle scheme is bookkeeping about extremal coordinates. The halfspace scheme needs three facts: the minimal-norm point of the hull separates (a one-line perturbation argument), it lies on a face and hence is a convex combination of $d$ sample points (Carathéodory's theorem, in Mathlib, applied to a face), and it is the minimal-norm point of the hull of those $d$ points (uniqueness of the projection onto a convex set); the existence of the minimizer uses compactness of the hull. The margin scheme is the Perceptron convergence theorem of Mission VI applied to the batch algorithm, whose output is the sum of the updated examples.

Formalization scope

Samples are Fin m-indexed under Mission I's iidLaw, and probability statements bound the outer measure of the failure event. Lemma 30.1 splits a sample of size $k + n$ into its first $k$ and last $n$ entries; Theorem 30.2 takes an arbitrary selection rule $\mathrm{sel} : Z^m \to [m]^k$ and reconstruction map $B$ , the held-out set being the positions not in the range of the selection, and requires $k \ge 1$ and $m \ge 1$ in addition to the book's $m \ge 2k$ : for $k = 0$ the bound reads $L_D \le L_V$ , which fails, and the book's derivation uses $k \ge 1$ in $\log(m^k/\delta') \le k\log(m/\delta')$ . Compression schemes are defined for every $m \ge 1$ , since for $m = 0$ there is no index to select, with indices allowed to repeat as in $[m]^k$ and with $B$ 's outputs in $H$ ; the unrealizable version uses Mission XXIII's multiclass 0–1 loss. The halfspace results are stated for strictly separable $\pm1$ -labeled samples, $y_i\langle w^\star, x_i\rangle > 0$ , the book's "w.l.o.g. all labels positive" normalization; this avoids the boundary negatives that a realizable sample may contain under the $\operatorname{sign}(0)$ convention of Mission VI, and it is the setting in which the minimal-norm argument works. The scheme is stated as the existence of $d$ indices whose signed examples have a minimal-norm hull point separating the whole sample, which is the content of $A$ and $B$ without fixing how ties among faces are broken. Rectangles are closed boxes. The margin scheme uses Theorem 9.1's normalization.

Not stated: §30.2.3 (polynomials, a reduction), the bibliographic remarks, and the intermediate Carathéodory step as a separate item.

Selected references

S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 30. doi:10.1017/CBO9781107298019
N. Littlestone, M. K. Warmuth, Relating data compression and learnability, technical report, University of California, Santa Cruz, 1986.
S. Floyd, M. K. Warmuth, Sample compression, learnability, and the Vapnik-Chervonenkis dimension, Machine Learning 21, 1995. doi:10.1007/BF00993593
S. Ben-David, A. Litman, Combinatorial variability of Vapnik-Chervonenkis classes with applications to sample compression schemes, Discrete Applied Mathematics 86, 1998. doi:10.1016/S0166-218X(98)00000-6
S. Moran, A. Yehudayoff, Sample compression schemes for VC classes, Journal of the ACM 63(3), 2016. doi:10.1145/2890490

10 thms2 active usersReviewed

Completed

Combinatorics Machine Learning Probability·Captain: naimengye

Understanding Machine Learning XXIII: Multiclass LearnabilityTextbook

Motivation

Chapter 17 introduced multiclass prediction; Chapter 29 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), asks the two questions the fundamental theorem answered for binary classes: which classes of multiclass predictors are PAC learnable with respect to the 0–1 loss, and with what sample complexity. Natarajan's dimension generalizes the VC dimension by shattering with two disagreeing label functions, and the multiclass fundamental theorem (Theorem 29.3) bounds the uniform-convergence, agnostic and realizable sample complexities in terms of it, up to logarithmic factors in the number of labels $k$ ; the only new ingredient in its proof is Natarajan's lemma, the multiclass substitute for Sauer's lemma. The chapter then computes or bounds the Natarajan dimension of the classes that matter, One-versus-All and general reductions to binary classifiers, and linear multiclass predictors (Theorem 29.7). Its last section is a warning: unlike the binary case, not all ERMs are equal, and with infinitely many labels a class can be learnable by one ERM and not by another, so learnability and uniform convergence come apart (Claim 29.9).

Setting

$H$ is a class of functions from $X$ to a finite label set $Y$ with $|Y| = k$ . $C \subseteq X$ is shattered by $H$ if there are $f_0, f_1 : C \to Y$ with $f_0(x) \ne f_1(x)$ everywhere on $C$ such that every $B \subseteq C$ is realized by some $h \in H$ agreeing with $f_0$ on $B$ and with $f_1$ on $C \setminus B$ (Definition 29.1); $\operatorname{Ndim}(H)$ is the largest size of a shattered set (Definition 29.2). One-versus-All builds $T(\bar h)(x) = \operatorname{argmax}_i h_i(x)$ from $k$ binary classifiers, the smaller label on ties; a general reduction applies a rule $r : \{0,1\}^l \to [k]$ to $l$ binary classifiers; the linear class $H_\Psi$ predicts $\operatorname{argmax}_i\langle w, \Psi(x, i)\rangle$ for a class-sensitive feature map $\Psi : X \times [k] \to \mathbb{R}^d$ (29.1). The class of §29.4 has labels $P_f(X) \cup \{\ast\}$ , the finite and cofinite subsets of $X$ plus a special label, and hypotheses $h_A(x) = A$ if $x \in A$ and $\ast$ otherwise; $A_{good}$ returns $h_\emptyset$ on an all- $\ast$ sample and $A_{bad}$ returns $h_{\{x_1, \dots, x_m\}^c}$ .

Formalization targets

Goal: Theorem 29.3

There are absolute constants $C_1, C_2 > 0$ such that every class $H \subseteq Y^X$ with $\operatorname{Ndim}(H) = d$ satisfies

C_1\frac{d + \log(1/\delta)}{\epsilon^2} \le m^{UC}_H(\epsilon,\delta),\ m_H(\epsilon,\delta) \le C_2\frac{d\log k + \log(1/\delta)}{\epsilon^2}, \qquad C_1\frac{d + \log(1/\delta)}{\epsilon} \le m^{\mathrm{real}}_H(\epsilon,\delta) \le C_2\frac{d\log(kd/\epsilon) + \log(1/\delta)}{\epsilon},

the upper bounds by every ERM learner and the lower bounds for small $\epsilon, \delta$ and $d \ge 2$ , in the format of Mission IV's Theorem 6.8.

Milestones

Lemma 29.4 (Natarajan: $|H| \le |X|^{\operatorname{Ndim}(H)}k^{2\operatorname{Ndim}(H)}$ ); Lemma 29.5 (the Natarajan dimension of One-versus-All is $O(kd\log(kd))$ ); Theorem 29.7 ( $\operatorname{Ndim}(H_\Psi) \le d$ ); Claim 29.9(1) ( $A_{good}$ needs $\frac1\epsilon\log\frac1\delta$ examples); Claim 29.9(2) ( $A_{bad}$ fails with constant probability on $(|X|-1)/(6\epsilon)$ examples). Further items: the equality $\operatorname{Ndim} = \operatorname{VCdim}$ for two classes, and Lemma 29.6 for general reductions.

Significance

Theorem 29.3 is the multiclass fundamental theorem of Natarajan (1989) and Ben-David, Cesa-Bianchi, Haussler and Long (1995): finite Natarajan dimension characterizes multiclass learnability, and the sample complexity is linear in it, with the dependence on $k$ confined to logarithms. Natarajan's lemma is the combinatorial core, and the dimension bounds of §29.3 are what make the theorem usable: a One-versus-All scheme over a class of VC dimension $d$ costs $\tilde O(kd)$ , and a linear multiclass predictor costs at most its number of parameters, so the multivector construction of Chapter 17 is learnable with $\tilde O(nk/\epsilon^2)$ examples. Claim 29.9 is a genuine phenomenon of Daniely, Sabato, Ben-David and Shalev-Shwartz (2011): in multiclass classification the choice of ERM matters, and the equivalence "learnable iff uniform convergence" of the binary theory is false, which is why Conjecture 29.10 about good ERMs is open in the form the chapter states it.

Difficulty

The equality with the VC dimension for two labels is a direct comparison of the two shattering definitions. Natarajan's lemma is a Sauer-type induction on $|X|$ , in which a shattered set must be produced from two hypotheses that differ at a point; the exercise-level proof of the book becomes a careful double induction formally. Theorem 29.3's upper bounds follow the binary proof of Chapter 28 with Natarajan's lemma in place of Sauer's, hence Massart's lemma and Theorem 26.5 for the agnostic case and the double-sample argument for the realizable case; the lower bounds reduce to the binary ones by embedding a binary class into a multiclass one on a shattered set. These are long formal developments, and the theorem is stated with unspecified constants for that reason. Lemmas 29.5 and 29.6 are counting: a shattered $C$ has $2^{|C|} \le |H_C| \le |(H_{bin})_C|^k$ , Sauer's lemma bounds the right side by $\big(\sum_{i \le d}\binom{|C|}{i}\big)^{k}$ , and the resulting inequality is solved. For Lemma 29.5's printed $3kd\log(kd)$ this fails only at $(k, d) = (2, 1), (3, 1)$ . There a shattered set splits by the label pair $\{f_0(x), f_1(x)\}$ into parts shattered by $\{B \setminus A : A, B \in H_{bin}\}$ (pairs $\{0, b\}$ ) or by $H_{bin}$ (other pairs). The first class has at most $31$ traces on $5$ points. Theorem 29.7 maps a shattered set into $\mathbb{R}^d$ by $\rho(x) = \Psi(x, f_0(x)) - \Psi(x, f_1(x))$ , up to sign, and shows the image is shattered by homogeneous halfspaces; the tie-breaking rule decides which sign and which halfspace convention to use. Claim 29.9(1) is the bound $(1-\epsilon)^m \le \delta$ ; Claim 29.9(2) needs only that at most $(d-1)/2$ of the $d-1$ light points appear in the sample, an event of probability at least $1/3$ by Markov's inequality when $m \le (d-1)/(6\epsilon)$ , which exceeds the claimed $e^{-1}/6$ .

Formalization scope

Labels are an arbitrary finite type, shattering and the Natarajan dimension are stated with witnesses $f_0, f_1$ defined on all of $X$ , and the dimension is a supremum in $\mathbb{N} \cup \{\infty\}$ . The multiclass 0–1 loss, the ERM property, agnostic PAC learnability and uniform convergence are Mission I's generic notions; the realizable multiclass PAC property is defined here in the shape of Definition 3.1 with $D(\{h \ne f\})$ as the error, since Mission I's binary version is $\{0,1\}$ -specific. Theorem 29.3 is stated exactly as Mission IV states Theorem 6.8, with existential constants, upper bounds for every ERM learner of a nonempty measurable class with the countable-approximation property (the measurability device of Remark 3.1), and lower bounds for $\epsilon < \epsilon_0$ , $\delta < \delta_0$ , $d \ge 2$ . Argmax predictors, both One-versus-All and $H_\Psi$ , break ties towards the smallest label; the book states this rule for One-versus-All, and some fixed rule is necessary for Theorem 29.7, since with arbitrary tie-breaking every function is an argmax predictor of the zero mapping. Lemmas 29.5 and 29.6 are stated per shattered set. Lemma 29.5 keeps the printed $3kd\log(kd)$ , which is true although the book's step $|(H_{bin})_C| \le |C|^d$ fails for small $|C|$ . Lemma 29.6 uses $2ld\log_2(2ld)$ , which the counting supports, because the printed $3ld\log(ld)$ is false at $l = d = 1$ . Theorem 29.3's uniform-convergence upper bound is stated for $d \ge 1$ . At $d = 0$ the confidence term $\log(1/\delta)$ vanishes as $\delta \to 1$ , the bound reaches $m = 1$ , and a single example is not representative. The class of §29.4 has labels Option of the subtype of finite-or-cofinite sets, with the discrete σ-algebra, and the two ERMs are predicates fixing the output on all- $\ast$ samples; Claim 29.9(1) is stated for countable $X$ with measurable singletons and Claim 29.9(2) for finite $X$ of size at least $2$ , with the proof's own distribution, $h_\emptyset$ as target, and every $\epsilon \in (0, 1/2)$ in place of the book's unspecified constant $a$ .

Not stated: Corollary 29.8 (its lower bound $(k-1)(n-1)$ is cited, not proved), Conjecture 29.10, the exercises.

Selected references

S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 29. doi:10.1017/CBO9781107298019
B. K. Natarajan, On learning sets and functions, Machine Learning 4, 1989. doi:10.1007/BF00114804
S. Ben-David, N. Cesa-Bianchi, D. Haussler, P. M. Long, Characterizations of learnability for classes of {0, …, n}-valued functions, Journal of Computer and System Sciences 50(1), 1995. doi:10.1006/jcss.1995.1008
D. Haussler, P. M. Long, A generalization of Sauer's lemma, Journal of Combinatorial Theory A 71(2), 1995. doi:10.1016/0097-3165(95)90001-2
A. Daniely, S. Sabato, S. Ben-David, S. Shalev-Shwartz, Multiclass learnability and the ERM principle, COLT 2011; Journal of Machine Learning Research 16, 2015.
A. Daniely, S. Sabato, S. Shalev-Shwartz, Multiclass learning approaches: a theoretical comparison with implications, NIPS 2012.

15 thms2 active usersReviewed

Completed

Combinatorics Machine Learning Probability·Captain: naimengye

Understanding Machine Learning XXII: Proof of the Fundamental TheoremTextbook

Motivation

Chapter 6 stated the fundamental theorem of statistical learning: a binary class is learnable if and only if its VC dimension is finite, with sample complexity $\Theta((d + \ln(1/\delta))/\epsilon^2)$ in the agnostic case and $\Theta((d\ln(1/\epsilon) + \ln(1/\delta))/\epsilon)$ in the realizable case. Chapter 28 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), proves it. The agnostic upper bound is obtained from the Rademacher machinery of Chapter 26 with Sauer's lemma and Massart's lemma, up to a $\log(d/\epsilon)$ factor that only chaining removes (28.1). The agnostic lower bound comes in two parts: a two-point construction giving $m \ge 0.5\log(1/(4\delta))/\epsilon^2$ , and a $d$ -point construction giving $m \ge d/(512\epsilon^2)$ at confidence $1/8$ , whose heart is Lemma 28.1, the optimality of the Maximum-Likelihood rule against the family of noisy distributions $D_b$ . The realizable upper bound is proved through $\epsilon$ -nets: with $m \ge \frac8\epsilon(2d\log(16e/\epsilon) + \log(2/\delta))$ examples a random sample hits every set of measure at least $\epsilon$ in the class (Theorem 28.3), so any hypothesis consistent with the sample has error below $\epsilon$ . Mission IV states these bounds with unnamed constants; this mission gives the chapter's explicit ones.

Setting

$H$ is a class of functions $X \to \{0,1\}$ with the 0–1 loss and $\operatorname{VCdim}(H) = d$ . For the upper bound, $A = \{(\mathbb{1}[h(x_i) \ne y_i])_i : h \in H\}$ is the loss set of a sample and $R(A)$ its Rademacher complexity. For the lower bounds, $C = \{c_1, \dots, c_d\}$ is a set shattered by $H$ and, for $b \in \{\pm1\}^d$ and $\rho \in (0,1)$ , $D_b$ draws $c_i$ uniformly and labels it $b_i$ with probability $(1+\rho)/2$ ; for $d = 1$ these are the distributions $D_\pm$ of §28.2.1. The Maximum-Likelihood rule $A_{ML}$ predicts at each $c_i$ the majority of the labels seen at $c_i$ . An $\epsilon$ -net for $H$ with respect to $D$ is a sample meeting every $h \in H$ with $D(h) \ge \epsilon$ (Definition 28.2).

Formalization targets

Goal: Theorem 28.3

Let $\operatorname{VCdim}(H) = d$ , $\epsilon \in (0,1)$ , $\delta \in (0, 1/4)$ and $m \ge \frac8\epsilon\big(2d\log\frac{16e}{\epsilon} + \log\frac2\delta\big)$ . Then with probability at least $1 - \delta$ over $S \sim D^m$ , $S$ is an $\epsilon$ -net for $H$ .

Milestones

The two-sided deviation bound of §28.1 ( $|L_D(h) - L_S(h)| \le 2\sqrt{(8d\log(em/d) + 2\log(4/\delta))/m}$ uniformly over $H$ ); the lower bound $m(\epsilon,\delta) \ge 0.5\log(1/(4\delta))/\epsilon^2$ of §28.2.1; Lemma 28.1; the lower bound $m(\epsilon, 1/8) \ge d/(512\epsilon^2)$ of §28.2.2; the realizable upper bound of §28.3 (ERM has error at most $\epsilon$ with probability $1 - \delta$ for the sample size of Theorem 28.3). Further items: the Rademacher bound $R(A) \le \sqrt{2d\log(em/d)/m}$ , the explicit uniform-convergence sample complexity of §28.1, and the expectation lower bound $\rho/4$ of §28.2.2.

Significance

These are the theorems that make the VC dimension the right measure of learnability, with constants. The upper bounds show what the abstract machinery of Missions II, IV, XX buys when instantiated: Sauer plus Massart plus Theorem 26.5 gives the agnostic rate, and the double-sample symmetrization plus Sauer gives the realizable rate, sharper by a factor $1/\epsilon$ because $\epsilon$ -nets need only one-sided control. The lower bounds are the No-Free-Lunch argument refined to quantify $\epsilon$ and $\delta$ : the two-point distribution shows that confidence costs $\log(1/\delta)/\epsilon^2$ , and the $d$ -point family with Lemma 28.1 shows that the dimension costs $d/\epsilon^2$ , through the exact optimality of majority voting and a binomial anti-concentration bound. Theorem 28.3 is also the basic $\epsilon$ -net theorem of Haussler and Welzl, a result of independent importance in computational geometry.

Difficulty

The Rademacher bound is Sauer's lemma (Mission IV) plus Massart's lemma (Mission XX) with $\|a - \bar a\| \le \sqrt m$ ; the deviation bound is Theorem 26.5 applied to $\ell$ and $-\ell$ with a union bound; the explicit sample complexity is Lemma A.2, $x \ge 4a\log(2a) + 2b \Rightarrow x \ge a\log x + b$ , which a formal proof must establish (the tangent inequality for $\log$ at $2a$ ). The two-point lower bound requires the binomial lower-tail estimate of Lemma B.11 and the algebra $\frac12(1 - \sqrt{1 - \sqrt{4\delta}}) \ge \delta$ , valid for $\delta < 1/4$ , the only nonvacuous range. Lemma 28.1 is a conditioning argument: fixing the instance indices and the labels off $c_i$ , the contribution of $c_i$ is minimized by predicting the more likely $b_i$ given the labels at $c_i$ , which is the majority; the formal proof must decompose the product measure $D_b^m$ over the positions $r$ with $x_r = c_i$ . The expectation bound $\rho/4$ then needs Lemma B.11 again, $1 - e^{-a} \le a$ , Jensen for $\sqrt{\cdot}$ and $\mathbb{E}[n_i] = m/d$ , and the probability bound $1/8$ follows by Mission III's reverse Markov inequality with $\rho = 8\epsilon$ . Theorem 28.3 is the double-sample argument: Claim 1 ( $P[S \in B] \le 2P[(S,T) \in B']$ , via a Chernoff bound that only needs $m\epsilon \ge 2\log 2$ ), Claim 2 (symmetrization by a random half, $P[(S,T) \in B'] \le e^{-\epsilon m/4}\tau_H(2m)$ ), Sauer's lemma, and Lemma A.2 once more. The realizable upper bound applies Theorem 28.3 to the error sets $\{x : h(x) \ne f(x)\}$ , a class of the same VC dimension.

Formalization scope

All objects are those of the earlier missions: risks, samples and learners from Mission I, vcDim and the countable-approximation property PointwiseSeparable from Mission IV (the measurability device for suprema over $H$ , used wherever a symmetrization or Rademacher argument is invoked), condLaw from Mission XIV for the distributions $D_b$ , and rademacher, evalSet, lossClass from Mission XX. Probability statements bound the outer measure of the failure event under iidLaw. The Rademacher and deviation items require $m > d + 1$ , the range in which Mission IV states Sauer's lemma in the form $(em/d)^d$ ; the explicit sample complexity of §28.1 implies this range, since its first term $432d\log(64d/\epsilon^2)/\epsilon^2$ dominates the possibly negative $8d\log(e/d)$ , and Lemma A.2 holds for any real $b$ , so the book's constants are used verbatim. The lower bounds take a shattered set as an injective $c : \mathrm{Fin}\ d \to X$ with the shattering property written out, use $D_b$ as condLaw of the uniform law on $C$ , and state the excess risk against $\min_{h \in H}L_{D_b}(h)$ as $\exists h \in H$ with $L(h) + \epsilon \le L(A(S))$ , or as a real infimum over $H$ in the expectation item; no measurability of the learner is needed because $D_b^m$ is atomic. Lemma 28.1 compares the sums over $b$ of the expected risks, the common term $\min_h L_{D_b}$ cancelling, for every majority rule with arbitrary tie-breaking. Theorem 28.3 and the realizable bound are stated for $\delta \in (0, 1/4)$ , the theorem's own range; the realizable bound is the inner clause of Mission I's IsPACWith on that range rather than a sample-complexity function, since the theorem does not cover $\delta \ge 1/4$ with its formula.

Not stated: the realizable lower bound (an exercise), the remark that chaining removes the logarithm in (28.1), and the intermediate claims of the proof of Theorem 28.3 as separate items.

Selected references

S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 28. doi:10.1017/CBO9781107298019
V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and its Applications 16(2), 1971. doi:10.1137/1116025
A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik-Chervonenkis dimension, Journal of the ACM 36(4), 1989. doi:10.1145/76359.76371
D. Haussler, E. Welzl, ε-nets and simplex range queries, Discrete and Computational Geometry 2, 1987. doi:10.1007/BF02187876
M. Anthony, P. L. Bartlett, Neural Network Learning: Theoretical Foundations, Cambridge University Press, 1999. doi:10.1017/CBO9780511624216

11 thms2 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: naimengye

Understanding Machine Learning XX: Rademacher ComplexitiesTextbook

Motivation

Chapter 4 showed that uniform convergence suffices for learnability; Chapter 26 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), measures its rate. The representativeness of a sample, $\sup_{h \in H}(L_D(h) - L_S(h))$ , is the quantity that controls the excess risk of ERM, and the Rademacher complexity $R(F \circ S) = \frac1m\mathbb{E}_\sigma\sup_{f \in F}\sum_i\sigma_i f(z_i)$ estimates it from the sample itself: the symmetrization argument gives $\mathbb{E}\operatorname{Rep} \le 2\,\mathbb{E}R$ (Lemma 26.2), and McDiarmid's bounded-differences inequality turns expectations into high-probability statements, yielding the generalization bounds of Theorem 26.5, including the data-dependent ones in which the complexity is computed on the training set. A small calculus of Rademacher complexities follows, affine images, convex hulls, Massart's lemma for finite sets and the contraction lemma for Lipschitz compositions, and it is applied to linear classes with $\ell_2$ and $\ell_1$ constraints. The chapter's payoff is dimension-free generalization bounds for linear predictors with Lipschitz losses (Theorem 26.12), for hard-SVM (Theorems 26.13–26.14), and for predictors with low $\ell_1$ norm (Theorem 26.15).

Setting

For a loss class $F = \ell \circ H$ and a sample $S = (z_1, \dots, z_m)$ , $\operatorname{Rep}_D(F, S) = \sup_{f \in F}(L_D(f) - L_S(f))$ (26.1), $F \circ S = \{(f(z_1), \dots, f(z_m)) : f \in F\}$ , and for $A \subseteq \mathbb{R}^m$ , $R(A) = \frac1m\mathbb{E}_\sigma[\sup_{a \in A}\sum_i\sigma_i a_i]$ with $\sigma$ uniform on $\{\pm1\}^m$ (26.5). The linear classes are $H_2 \circ S = \{(\langle w, x_i\rangle)_i : \|w\|_2 \le 1\}$ in a Hilbert space and $H_1 \circ S$ with $\|w\|_1 \le 1$ in $\mathbb{R}^n$ (26.14). Losses of the form $\ell(w, (x, y)) = \varphi(\langle w, x\rangle, y)$ with $a \mapsto \varphi(a, y)$ $\rho$ -Lipschitz (26.18) cover the hinge and absolute losses.

Formalization targets

Goal: Theorem 26.5

Assume $|\ell(h, z)| \le c$ for all $z$ and $h \in H$ . Then, each with probability at least $1 - \delta$ over $S \sim D^m$ :

for all $h \in H$ , $L_D(h) - L_S(h) \le 2\,\mathbb{E}_{S' \sim D^m}R(\ell \circ H \circ S') + c\sqrt{2\ln(2/\delta)/m}$ ;
for all $h \in H$ , $L_D(h) - L_S(h) \le 2R(\ell \circ H \circ S) + 4c\sqrt{2\ln(4/\delta)/m}$ ;
for any $h^\star \in H$ , $L_D(\mathrm{ERM}_H(S)) - L_D(h^\star) \le 2R(\ell \circ H \circ S) + 5c\sqrt{2\ln(8/\delta)/m}$ .

Milestones

Lemma 26.2 (symmetrization); Lemma 26.8 (Massart); Lemma 26.9 (contraction); Theorem 26.12 (linear predictors with $\ell_2$ constraints); Theorem 26.13 (hard-SVM). Further items: Theorem 26.3, Lemma 26.4 (McDiarmid), Lemmas 26.6, 26.7, 26.10, 26.11, Theorem 26.14 and Theorem 26.15.

Significance

Rademacher complexity is the modern language of uniform convergence: it is data-dependent, it is dimension-free for linear classes, and it composes with Lipschitz losses, which is why the SVM bounds of this chapter do not depend on the dimension of $w$ and apply verbatim to kernel methods (Remark 26.2). Theorem 26.5 is the template every such bound follows, symmetrization plus McDiarmid, and the two data-dependent parts are the first bounds in the book that use the training set both to learn and to certify. Massart's lemma and the contraction lemma are the two tools that make the calculus work, the first converting finiteness into a logarithmic dependence, the second removing the loss function from the picture. Theorem 26.13 finally justifies the margin-based sample complexity $R^2\|w^\star\|^2/\epsilon^2$ of hard-SVM, and Theorem 26.14 gives a bound computable from the output alone.

Difficulty

Lemma 26.2 is the symmetrization argument: a ghost sample, the exchange of $z_j$ and $z'_j$ (26.7), the introduction of one Rademacher sign at a time (26.8)–(26.9), and the split of the supremum. Formally it needs Fubini over the product of $2m$ copies of $D$ and the sign average, and the measurability of the suprema, which the statements assume. McDiarmid's inequality is a martingale argument with Hoeffding's lemma at each step; it is the substantial probabilistic input, and Theorem 26.5 combines it with Lemma 26.2, a union bound and Hoeffding's inequality along the decomposition (26.10). Lemma 26.6 is the symmetry $\sigma \mapsto -\sigma$ ; Lemma 26.7 is the fact that a linear functional on the simplex is maximized at a vertex; Massart's lemma is the exponential-moment bound $\mathbb{E}e^{\sigma a} \le e^{a^2/2}$ with Jensen and an optimized scaling; the contraction lemma is Kakade and Tewari's coordinate-by-coordinate argument (26.12)–(26.13), which in a formal proof must be run as an induction over the coordinates. Lemmas 26.10 and 26.11 are Cauchy–Schwarz and Hölder followed by Jensen, respectively Massart on the $2n$ coordinate vectors. Theorem 26.12 chains contraction, Lemma 26.10 and Theorem 26.5 on the almost-sure event $\|x\| \le R$ ; Theorem 26.13 specializes it to the ramp loss with $B = \|w^\star\|$ , where the hard-SVM output has zero empirical ramp loss; Theorem 26.14 is a union bound over the nested classes $\|w\| \le 2^i$ with $\delta_i = \delta/(2i^2)$ ; Theorem 26.15 repeats Theorem 26.12 with Lemma 26.11.

Formalization scope

The Rademacher complexity is a finite average over the $2^m$ sign vectors, so no measure on $\{\pm1\}^m$ is needed, and the supremum over $A$ is the real supremum over the subtype $A$ ; the theorems assume $A$ nonempty and bounded, which every evaluation set of a bounded loss class satisfies. Risks are Mission I's risk and empRisk, samples are Fin m-indexed under iidLaw, and probability statements bound the outer measure of the failure event. Expectations of suprema over uncountable classes are Bochner integrals, so Lemma 26.2, Theorem 26.3 and Theorem 26.5 carry explicit hypotheses that $S \mapsto \operatorname{Rep}_D(F, S)$ and $S \mapsto R(F \circ S)$ are measurable, the book's Remark 3.1 made visible; for the linear classes of §26.3–§26.4 these hold automatically when the Hilbert space is separable (the supremum over the ball is a supremum over a countable dense subset), which is why Theorems 26.12–26.14 assume SecondCountableTopology. McDiarmid's inequality is stated for a measurable function on a product of arbitrary probability measures. Theorem 26.13's error is $P[y\langle w_S, x\rangle \le 0]$ , which dominates $P[y \ne \operatorname{sign}\langle w_S, x\rangle]$ whatever $\operatorname{sign}(0)$ is, and the hard-SVM learner is any map returning a minimum-norm margin-1 separator on separable samples; measurability of the learner is not needed because the bound is uniform over the ball. Theorem 26.14 is given with the constants of its proof, $\sqrt{4(\ln(4\log_2\|w_S\|) + \ln(1/\delta))/m}$ rather than the printed $\sqrt{\ln(4\log_2\|w_S\|/\delta)/m}$ , and for $\|w_S\| \ge 2$ , where $i = \lceil\log_2\|w_S\|\rceil$ satisfies $1 \le i \le 2\log_2\|w_S\|$ as the proof requires; the item text records this. Norms on $\mathbb{R}^n$ as Fin n → ℝ are sup norms (Lemma 26.11, Theorem 26.15), Euclidean norms are written out (Massart), and inner product spaces carry the Euclidean norm.

Not stated: Definition 26.1 (already Mission II's IsRepresentative), the validation heuristic (26.2)–(26.3), Remark 26.1 (the improved rate under separability, no proof), Remark 26.2.

Selected references

S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 26. doi:10.1017/CBO9781107298019
P. L. Bartlett, S. Mendelson, Rademacher and Gaussian complexities: risk bounds and structural results, Journal of Machine Learning Research 3, 2002.
V. Koltchinskii, D. Panchenko, Rademacher processes and bounding the risk of function learning, in High Dimensional Probability II, Birkhäuser, 2000. doi:10.1007/978-1-4612-1358-1_29
C. McDiarmid, On the method of bounded differences, in Surveys in Combinatorics, Cambridge University Press, 1989. doi:10.1017/CBO9781107359949.008
S. M. Kakade, K. Sridharan, A. Tewari, On the complexity of linear prediction: risk bounds, margin bounds, and regularization, NIPS 2008.
S. Boucheron, O. Bousquet, G. Lugosi, Theory of classification: a survey of some recent advances, ESAIM: Probability and Statistics 9, 2005. doi:10.1051/ps:2005018

10 thms2 active usersReviewed