All missions

Motivation

A cycle cover of a graph is a collection of cycles that together use every edge at least once. Covering the edges of a network by closed tours appears in routing and inspection problems (the Chinese postman problem is the closed-walk version), and the minimum total length of a cycle cover is a classical extremal parameter of bridgeless graphs. Alon and Tarsi (Covering multigraphs by simple circuits, SIAM J. Algebraic Discrete Methods 6, 1985, pp. 345–350; reference [2] of the paper) conjectured that every bridgeless graph with $m$ edges has a cycle cover of length at most $7m/5$ (Conjecture 7.1 of the paper).

The question is closely tied to cycle double covers (CDCs): families of cycles covering every edge exactly twice. The Cycle Double Cover Conjecture of Szekeres and Seymour asserts that every bridgeless graph has one, and it suffices to prove it for cubic graphs. Brinkmann, Goedgebeur, Hägglund and Markström (Generation and properties of snarks, arXiv:1206.6690v3, 2013; J. Combin. Theory Ser. B 103, 2013) generated all snarks on up to 36 vertices and tested these conjectures on them. Section 7 of their paper derives cycle-cover bounds from double covers. For colourable cubic graphs (those with a proper 3-edge-colouring) the argument gives the bound $4m/3$, and the authors conjecture (Conjecture 7.4) that $4m/3 + o(m)$ holds for all snarks. This mission formalizes the colourable bound and the chain of statements behind it.

Setting

All graphs are finite and simple. A graph is cubic if every vertex has degree 3. It is colourable if its edges can be coloured with three colours so that edges sharing a vertex receive different colours.

A cycle is a 2-regular connected graph. Inside a graph $G$ a cycle is recorded by its edge set $C = \{v_1v_2, \dots, v_{\ell-1}v_\ell, v_\ell v_1\}$, with $v_1, \dots, v_\ell$ distinct and $\ell \ge 3$; its length is $|C| = \ell$. A 2-regular subgraph of $G$ is an edge set $D$ such that every vertex lies on none or exactly two edges of $D$: a union of vertex-disjoint cycles, possibly empty and not necessarily spanning. A 2-factor is a spanning 2-regular subgraph. An even subgraph is an edge set $S$ such that every vertex lies on an even number of edges of $S$.

A cycle double cover of $G$ is a multiset of cycles such that every edge lies in exactly two of them. It is a $k$-CDC if the cycles can be coloured with $k$ colours so that cycles sharing an edge get different colours. Each colour class is then an even subgraph, and following the paper the $k$-CDC is written as a family $D_0, \dots, D_{k-1}$ of even subgraphs with every edge in exactly two of them, counted with multiplicity.

A cycle cover of $G$ is a set $\mathcal F$ of cycles of $G$ such that every edge lies in at least one of them, and its length is $\ell(\mathcal F) = \sum_{C \in \mathcal F} |C|$. Throughout, $m$ denotes the number of edges of $G$.

Formalization targets

Goal: the $4m/3$ bound (§7, p. 24)

For every colourable cubic graph $G$ with $m$ edges there is a cycle cover $\mathcal F$ with

Equivalently, the shortest cycle cover of $G$ has length at most $4m/3$.

Milestones

1. Cycle decompositions (§5, p. 15). An edge set $S$ is an even subgraph of $G$ if and only if it is the union of pairwise edge-disjoint cycles of $G$.
2. Proposition 5.3 (p. 15). If $G$ is a colourable cubic graph and $D$ is any 2-regular subgraph of $G$, then $G$ has a 4-CDC $(D_0, D_1, D_2, D_3)$ with $D_0 = D$.
3. Lemma 7.2 (p. 24). If a cubic graph $G$ has a 2-regular subgraph $C$ and a CDC $\mathcal D$ with $C \in \mathcal D$, then $G$ has a cycle cover $\mathcal F$ with

Significance

The bound $4m/3$ is far below the Alon–Tarsi bound $7m/5$ and is attained up to lower-order terms on the snarks the paper enumerates (Corollary 7.3, which rests on a computer search and is not part of this mission). It isolates the colourable case of Conjecture 7.4, so any proof of that conjecture must at least reproduce it. Proposition 5.3 is a strong form of the Strong Cycle Double Cover Conjecture for colourable cubic graphs: every 2-regular subgraph, not only every cycle, is a colour class of a 4-CDC. Lemma 7.2 is the general device that turns a double cover containing a long 2-regular subgraph into a short cycle cover; the paper applies it again with long cycles of snarks.

On the formal side, none of these objects exists in Mathlib or on the platform: there is no cycle double cover, no cycle cover, and no decomposition of even graphs into cycles (Veblen's theorem). Mathlib has walks, cycles as walks (Walk.IsCycle), Eulerian trails and the predicate IsCycles, but the step from an even edge set to a family of edge-disjoint cycles is missing. The results of this mission are all proved in the paper or classical; none has a machine-checked proof.

Difficulty

The arithmetic of the goal is immediate once the pieces exist: a 3-edge-colouring of a cubic graph on $n$ vertices consists of three perfect matchings, two of which form a 2-factor with $n = 2m/3$ edges, and $2m - 2m/3 = 4m/3$. The work lies elsewhere.

First, Veblen's theorem must be formalized: an even edge set is a union of edge-disjoint cycles. This requires extracting a cycle (a walk with no repeated vertex) from a nonempty even edge set and inducting on the number of edges; the bookkeeping between walks, their edge lists and finite edge sets is where formal proofs of this kind spend their effort. Lemma 7.2 needs it, because the colour classes of a CDC are even subgraphs, while a cycle cover consists of cycles.

Second, Proposition 5.3 needs the passage from a proper 3-edge-colouring (a colouring of the line graph) to three perfect matchings and to the three 2-factors formed by pairs of colours, and then a parity check that the symmetric differences with $D$ are even and cover every edge exactly twice. A tempting shortcut fails: the three pairwise unions of colour classes already form a 3-CDC, but a prescribed 2-regular subgraph $D$ need not be one of its classes.

Formalization scope

Graphs are SimpleGraph V on a finite type V with decidable equality and decidable adjacency. Cubic is G.IsRegularOfDegree 3. Colourable is G.lineGraph.Colorable 3, a proper vertex colouring of the line graph, never a vertex colouring of G. Edges are Sym2 V, and every subgraph is recorded by its finite edge set. A cycle is the edge set of a closed walk satisfying Walk.IsCycle, of length its number of edges. A $k$-CDC is a function Fin k → Finset (Sym2 V) of even edge sets with every edge of G in exactly two indices, so repeated and empty classes count correctly. A cycle cover is a Finset of cycles covering every edge, of length ∑ C ∈ F, C.card.

"The shortest cycle cover has length at most $X$" is stated as "some cycle cover has length at most $X$"; the two agree because a finite graph has finitely many cycle covers. Bounds are kept in $\mathbb N$ without subtraction or division: the goal is $3\,\ell(\mathcal F) \le 4m$, and Lemma 7.2 is $\ell(\mathcal F) + |C| \le 2m$. Lemma 7.2 is stated for a CDC given as a family of even subgraphs, the form in which the paper applies it (with $C$ a 2-factor that is a colour class of a 4-CDC); a CDC of single cycles is a special case. The cubic hypothesis of Lemma 7.2 is kept as printed although the argument does not use it.

The bound becomes trivial if a "cycle" is weakened to an even edge set or to the edge set of a closed walk, since then the single set $E(G)$ is a cover of length $m \le 4m/3$. The cycles here are genuine cycles of G.

Out of scope: Corollary 7.3 (the cycle-cover lengths of all snarks on at most 36 vertices) and every other statement resting on the exhaustive enumeration, Conjectures 7.1 and 7.4, and the Strong Cycle Double Cover material of §5.1 and §6.

Reusable infrastructure: cycles as edge sets, even subgraphs, $k$-CDCs, cycle covers and Veblen's theorem are general graph-theoretic objects, useful well beyond this paper (for flows, the Cycle Double Cover Conjecture, and Eulerian subgraph arguments). Proofs of Veblen's theorem and of the passage from a 3-edge-colouring to perfect matchings are particularly welcome.

Selected references

• G. Brinkmann, J. Goedgebeur, J. Hägglund, K. Markström, Generation and properties of snarks, arXiv:1206.6690v3, 2013; J. Combin. Theory Ser. B 103 (2013). https://arxiv.org/abs/1206.6690
• N. Alon, M. Tarsi, Covering multigraphs by simple circuits, SIAM J. Algebraic Discrete Methods 6 (1985), no. 3, 345–350; MR 791163. Cited as [2] in https://arxiv.org/abs/1206.6690

Motivation

Norms are the most common nonsmooth terms in convex optimization models. The $\ell_1$ norm promotes sparsity in the lasso and in compressed sensing, the Euclidean norm of blocks of variables promotes group sparsity in the group lasso, and the nuclear norm promotes low rank. First-order methods for such models, notably the proximal gradient method, ADMM and their accelerated and parallel variants, handle a norm term through a single operation: its proximal operator. Each iteration of these methods needs $\operatorname{prox}_{\lambda\|\cdot\|}(v)$ for some point $v$ and step $\lambda>0$, so a description of this operator for an arbitrary norm is needed in practice.

The monograph of N. Parikh and S. Boyd, Proximal Algorithms (Found. Trends Optim. 1(3), 2014), records this description twice. In §2.5 it derives it from Moreau decomposition, and in §6.5 it states the general scaled form: the proximal operator of a norm is the identity minus a scaled Euclidean projection onto the unit ball of the dual norm. The underlying decomposition is due to J.-J. Moreau (Proximité et dualité dans un espace hilbertien, Bull. SMF 93, 1965). The norm case is standard in convex analysis texts; Parikh and Boyd present it as the bridge between proximal operators of norms and projections onto norm balls.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $z^Tx$ and Euclidean norm $\|\cdot\|_2$.

A function $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ is closed proper convex if its epigraph $\{(x,t)\mid f(x)\le t\}$ is a nonempty closed convex set. For such $f$ and $\lambda>0$, the proximal operator is

which has a unique minimizer for every $v$. The convex conjugate is $f^*(y)=\sup_x\big(y^Tx-f(x)\big)$. For a set $C$, the indicator function $I_C$ is $0$ on $C$ and $+\infty$ off $C$, and the Euclidean projection onto a nonempty closed convex $C$ is $\Pi_C(v)=\operatorname{argmin}_{x\in C}\|x-v\|_2$.

Let $\|\cdot\|$ be a general norm on $\mathbb R^n$, possibly different from $\|\cdot\|_2$. Its dual norm and the dual unit ball are

In the Lean development the space is EuclideanSpace ℝ (Fin n), the general norm is a seminorm N with the definiteness hypothesis IsNorm N, $\|z\|_*$ is dualNorm N z, $\mathcal B$ is dualBall N, $I_C$ is indicator C, and $f=\|\cdot\|$ is normFun N.

Formalization targets

Goal: (6.8), §6.5, p. 187

For every general norm $f=\|\cdot\|$ on $\mathbb R^n$, every $\lambda>0$ and every $v\in\mathbb R^n$,

Stated as: $v-\lambda w=\operatorname{prox}_{\lambda f}(v)$ if and only if $w=\Pi_{\mathcal B}(v/\lambda)$, for all $v,w$.

Milestones, in attack order

1. Moreau decomposition (2.4), p. 133: $v=\operatorname{prox}_f(v)+\operatorname{prox}_{f^*}(v)$ for closed proper convex $f$. This is the published, proved theorem MoreauProx.Decomposition.moreau_decomposition.
2. §2.5, p. 134: for a norm, $f^*=I_{\mathcal B}$ as functions on all of $\mathbb R^n$.
3. §2.5, p. 134: the case $\lambda=1$, $v=\operatorname{prox}_f(v)+\Pi_{\mathcal B}(v)$.
4. (6.7), p. 187: $\operatorname{prox}_{\lambda f}(v)=v-\lambda\operatorname{prox}_{f^*/\lambda}(v/\lambda)$ for a general norm $f$ and $\lambda>0$, as printed.

Significance

The goal reduces evaluating the proximal operator of any norm to projecting onto one convex set, the unit ball of the dual norm. All the familiar closed forms are instances: soft thresholding for $\ell_1$ (whose dual ball is the $\ell_\infty$ box), block soft thresholding for $\|\cdot\|_2$ (whose dual ball is the Euclidean ball), and the $\ell_\infty$ prox via projection onto the $\ell_1$ ball. Conversely, it lets a projection onto a norm ball be computed from the norm's proximal operator. Milestone 4, the scaled Moreau decomposition, is here stated for norms; its general form is an identity used throughout splitting methods whenever a dual or conjugate prox is cheaper than the primal one.

The results are classical and proved in the literature; the work here is formalization. Moreau's decomposition is already formalized on the platform (Moreau 1965 series, proved). Several norm-specific corollaries are posed as open problems in other series: soft thresholding (BoydADMM.Prox.prox_l1_eq_softThreshold), block soft thresholding (BoydADMM.L1.group_lasso_z_update) and projection onto a Euclidean ball (Pegasos.Analysis.projBall_isProj). A proof of the goal here gives a uniform route to such statements for any norm. The general-norm statements, the conjugate of a norm and the scaled decomposition are not formalized elsewhere on the platform.

Difficulty

The derivation in the monograph is two lines, but each line hides a step. Computing $f^*$ for a norm requires the inequality $y^Tx\le\|x\|\,\|y\|_*$ and, for $\|y\|_*>1$, a direction along which $y^Tx-\|x\|$ grows without bound; the dual norm is a supremum, so finiteness and attainment have to be argued from finite dimensionality and definiteness of the norm. The scaling step requires knowing how the conjugate and the proximal operator transform under $f\mapsto\lambda f$ and $v\mapsto v/\lambda$, in extended-real arithmetic where $+\infty$ values must be tracked. The proximal operator of an indicator being the projection is an unfolding of definitions, but the minimizer predicates on both sides must be matched, including the factor $\tfrac12$ and squared versus unsquared distances.

A tempting shortcut is to work only with the Euclidean norm, where $\mathcal B$ is the Euclidean unit ball; that proves a special case, not the goal.

Formalization scope

• Space and norms. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) for arbitrary $n$, including $n=0$. The general norm is an arbitrary Seminorm ℝ (EuclideanSpace ℝ (Fin n)) with definiteness (IsNorm); the Euclidean norm of the space is used only in the proximal objective and the projection, as in (1.1) and (1.3).
• Extended values. Functions $\mathbb R^n\to\mathbb R\cup\{+\infty\}$ take values in EReal. The dual norm is computed in EReal as the supremum of the printed set, so it has no junk value. $\lambda f$ and $f^*/\lambda$ are products with the positive reals $\lambda$, $\lambda^{-1}$, and $\lambda>0$ is a hypothesis everywhere (p. 124).
• Proximal operator and projection as predicates. "$x=\operatorname{prox}_g(z)$" is IsProx g z x ($x$ minimizes $\tfrac12\|u-z\|_2^2+g(u)$) and "$x=\Pi_C(z)$" is IsProj C z x. With $g=\lambda f$, Moreau's objective $\tfrac12\|u-z\|_2^2+\lambda f(u)$ is $\lambda$ times the objective of (1.2), so it has the same minimizers. Both minimizers exist and are unique, so an equivalence over all candidate points states the printed equations exactly.
• Standing assumption. Every function whose proximal operator appears is closed proper convex (p. 124); a norm is, so no statement needs an extra hypothesis. Every statement, milestone 4 included, is about a general norm, as on the page.
• Ruling out trivializations. The dual unit ball is defined through the printed supremum $\sup\{z^Tx\mid\|x\|\le1\}$, never by a closed form or as "the set that makes (6.8) hold", and the projection is not pre-solved.
• Imported objects. The conjugate conj, IsProx and IsProj come from the published Moreau 1965 series definitions MoreauProx.Decomposition.ConvexDuality and MoreauProx.Decomposition.Cones.
• Source. The PDF used is the authors' copy of the published monograph in the journal's format (printed pages 123–231); page numbers are those of this copy.

Useful contributions include lemmas on conjugates of positively homogeneous functions, on the behaviour of IsProx under scaling, and the identity $\operatorname{prox}_{I_C}=\Pi_C$ in the predicate form; all are reusable beyond this mission.

Selected references

• N. Parikh and S. Boyd, Proximal Algorithms, Foundations and Trends in Optimization 1(3), 2014. https://doi.org/10.1561/2400000003
• J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bulletin de la Société Mathématique de France 93:273–299, 1965. https://doi.org/10.24033/bsmf.1625
• H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5
• S. Boyd, N. Parikh, E. Chu, B. Peleato and J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 2011. https://doi.org/10.1561/2200000016

Motivation

A retailer that sells products in several categories has to decide which products to put on display. Under the nested logit model a customer first picks a category (a nest) and then a product inside it, so offering a product changes the purchase probabilities of every other product. Choosing the assortment that maximizes expected revenue is assortment optimization, a standard problem of revenue management. Gallego and Topaloglu (Management Science, 2014) study it when every nest carries its own constraint on the assortment. With a limit on the shelf space of each nest the problem is NP-hard even for a single nest, so the paper builds an assortment that is guaranteed to earn at least half of the optimum.

A worst-case factor of two says little about one concrete instance. For its computational study (§7.1) the paper therefore needs, instance by instance, a number that is provably at least the optimal expected revenue, and it obtains one from a linear program, (13), whose constraints come from the linear programming relaxations of knapsack problems. Proposition 7 (Online Supplement A, p. 33) proves that this linear program does give an upper bound. This mission formalizes that proposition.

Setting

There are nests $M = \{1, \dots, m\}$ and products $N = \{1, \dots, n\}$ in each nest. Product $j$ of nest $i$ has a preference weight $v_{ij} > 0$ and a revenue $r_{ij}$ (any real number); $v_0$ is the preference weight of buying nothing, and $\gamma_i \in (0, 1]$ is the dissimilarity parameter of nest $i$. For an assortment $S_i \subseteq N$ of nest $i$ put

with $R_i(\bar 0) = 0$ for the empty assortment $\bar 0$. The expected revenue of $(S_1, \dots, S_m)$ is

Under space constraints product $j$ of nest $i$ uses $w_{ij}$ units of space and nest $i$ has capacity $c_i$, with $w_{ij} \le c_i$ for every product, so the feasible assortments are $\mathcal C_i = \{S_i : \sum_{j \in S_i} w_{ij} \le c_i\}$. Problem (1) is $Z^* = \max\{\Pi(S_1, \dots, S_m) : S_i \in \mathcal C_i \ \forall i\}$.

For a scalar $u$, the knapsack problem (10) of nest $i$ maximizes $\sum_j v_{ij}(r_{ij} - u) x_j$ over $x \in \{0,1\}^n$ with $\sum_j w_{ij} x_j \le c_i$. Its linear programming relaxation allows $x \in [0,1]^n$. The paper partitions $u \ge 0$ into finitely many intervals $\mathcal I_i^g$, $g \in \mathcal G_i$, on each of which one vector $x_i^g$ solves the relaxation. For a fractional vector $x$ it writes $V_i(x) = \sum_j v_{ij} x_j$ and $R_i(x) = \sum_j v_{ij} r_{ij} x_j / V_i(x)$.

The linear program (13) in the variables $(z, y_1, \dots, y_m)$ is

Formalization targets

Goal: Proposition 7

If $(\hat z, \hat y)$ is an optimal solution of (13), then

Milestones

1. Every feasible $(z, y)$ of (13) has $y_i \ge 0$ for all $i$ (p. 33).
2. For a nonempty $S \in \mathcal C_i$ with $R_i(S) > z$, $\hat u = \gamma_i z + (1 - \gamma_i) R_i(S)$, and a nonzero optimal solution $x$ of the relaxation at $\hat u$:

3. Under the same hypotheses, the zero vector is not an optimal solution of the relaxation at $\hat u$ (p. 34).
4. The claim of the proof: every feasible $(z, y)$ of (13) satisfies $y_i \ge V_i(S_i)^{\gamma_i}(R_i(S_i) - z)$ for every nest $i$ and every feasible assortment (pp. 33–34).

Significance

The proposition makes the optimality gaps of §7 meaningful: the expected revenue of any assortment that respects the space constraints, divided by the optimal value of (13), is a certified lower bound on its fraction of $Z^*$. The bound is a linear program with $1 + m$ variables and one constraint per interval solution, so it can be solved for instances where $Z^*$ itself, an NP-hard quantity, cannot be computed.

The result is proved in the paper; no machine-checked proof of it is known. Formalizing it checks the interplay of three ingredients that the paper treats briefly: the role of the interval solutions $x_i^g$ (only their feasibility and their optimality for every $u \ge 0$ matter), the extension of $V_i$ and $R_i$ to fractional vectors, and the concavity of $V \mapsto V^{\gamma_i}$. A related but different program is Davis, Gallego and Topaloglu's LP (16) (NestedLogitVariants.LP.lp16_upper_bound), which bounds the unconstrained problem by another argument.

Difficulty

The constraints of (13) are indexed by finitely many fractional vectors, while $Z^*$ is attained at an integral assortment that need not be among them. The obvious argument, that (13) is a relaxation of an exact linear-programming formulation of problem (1), does not apply: no constraint of (13) involves $S_i^*$ directly. The link between the two has to be made nest by nest, through the knapsack relaxations at values of $u$ that depend on the unknown optimum, and the fractional vectors $x_i^g$ are compared with integral assortments through the nonlinear map $V \mapsto V^{\gamma_i}$.

Formalization scope

The formalization references the published nested logit model NestedLogitVariants.General.Model (instance, $V_i$, $R_i$, $V_i^{\gamma_i}$, $\Pi$) and NestedLogitVariants.General.Relaxation (the unit box and the term $F$ of the constraints of (13)). The conventions are:

• nests are any finite type; products are Fin n, indexed from $0$; assortments are finite sets of products and $\bar 0$ is the empty set;
• the within-nest no-purchase weights of the published model are set to $0$ in every statement, which makes $V_i$ the paper's $V_i(S_i) = \sum_{j \in S_i} v_{ij}$;
• $v_0 > 0$, $v_{ij} > 0$ and $w_{ij} > 0$ are added hypotheses, and the paper's $w_{ij} \le c_i$ (p. 8) is kept wherever the proof needs the zero vector to be feasible for the relaxation; revenues are arbitrary reals; $\gamma_i \in (0, 1]$ as on p. 8;
• real powers are Real.rpow, and $a/0 = 0$, which gives $R_i(\bar 0) = 0$ as in the paper and makes the constraint term at $x = 0$ equal to $0$;
• the vectors $\{x_i^g\}$ are replaced by any finite sets $X_i$ of vectors that are feasible for the relaxation and contain an optimal solution of it for every $u \ge 0$, the family fixed before $u$; this is what the proof uses, and the paper's interval solutions satisfy it;
• $Z^*$ is the revenue of a hypothesised optimal assortment of problem (1) under the space constraints; an optimal solution of (13) is a feasible pair with minimal $z$.

The statement is not to be trivialized: setting $\gamma_i = 1$, taking $X_i$ to be the whole box $[0,1]^n$ (not a finite set and not LP (13)), assuming $0 \in X_i$, or proving the bound for one particular feasible point are all excluded.

A complete development needs the concavity (tangent-line) inequality of $V \mapsto V^{\gamma}$ at a positive point and elementary facts about fractional knapsack relaxations; both are reusable. Proofs of the milestones and of the goal are welcome.

Selected references

• G. Gallego and H. Topaloglu, Constrained Assortment Optimization for the Nested Logit Model, Management Science, 2014 (authors' manuscript of September 11, 2013). https://doi.org/10.1287/mnsc.2014.1931
• J. M. Davis, G. Gallego and H. Topaloglu, Assortment Optimization Under Variants of the Nested Logit Model, Operations Research, 2014. https://doi.org/10.1287/opre.2014.1256
• P. Rusmevichientong, Z.-J. M. Shen and D. B. Shmoys, A PTAS for Capacitated Sum-of-Ratios Optimization, Operations Research Letters, 2009. https://doi.org/10.1016/j.orl.2009.03.002

Why sparsity limits accuracy

The Frank–Wolfe algorithm minimizes a smooth convex objective over a compact convex domain by choosing an atom through a linear optimization problem and moving toward it. On a domain that is the convex hull of atoms, each ordinary iteration introduces at most one new atom. That makes the method useful when a solution represented with few atoms is valuable, but it raises a basic question: how much accuracy can a solution with only a few atoms attain? Jaggi's 2013 analysis gives upper bounds on primal error and duality gap for four Frank–Wolfe variants. Its sparsity section supplies a matching obstruction on the unit simplex. This mission isolates that obstruction so the claimed dependence on sparsity can be checked independently of any particular implementation of the algorithm.

The paper calls the number of used atoms the sparsity of an iterate. It proves two lower bounds for one quadratic objective: a sparse point cannot have arbitrarily small objective value, and, with fewer active coordinates than the simplex dimension, it cannot have arbitrarily small duality gap. These are worst-case statements about feasible points themselves. Consequently, any method whose iterates retain the stated sparsity is subject to them, regardless of how it selects its next atom. The source statements and constants are Lemma 3 and Lemma 4, PDF p. 5.

The quadratic simplex problem

Let $n$ be a positive integer and let the unit simplex be

For a vector $x$, let $\operatorname{card}(x)$ be the number of nonzero coordinates. The objective is the squared Euclidean norm $f(x)=\|x\|_2^2=\sum_i x_i^2$. Its minimum on the full simplex is $1/n$, reached at the uniform point. The paper compares that optimum with the best value permitted by a bound on $\operatorname{card}(x)$. The dimension $n$ and sparsity budget $k$ are separate: the goal assumes $k<n$, so at least one coordinate must be zero at every eligible point.

The duality gap at a feasible $x$ is

For a convex objective, this gap bounds the difference between the current objective value and the optimum; the paper introduces that certificate in display (2), PDF p. 2. Here the maximum exists because the simplex is nonempty and compact and the expression is continuous in $s$. It is the same certificate computed by minimizing a linear function over the domain in a Frank–Wolfe step. The paper's Table 1, PDF p. 6 identifies the simplex linear subproblem with choosing a coordinate having the largest coefficient.

Formalization targets

Sparse objective minimum

For $1\le k\le n$, Lemma 3 asserts an attained minimum:

The associated primal-error statement says that a point with exactly $k$ nonzero coordinates has $f(x)-f(x^*)\ge1/k-1/n$, where $x^*$ is an optimizer on the full simplex. The minimum and the primal-error reading are both included as draft theorems.

Duality-gap lower bound

For every natural number $k<n$, Lemma 4 states the mission goal:

The threshold $k<n$ is essential to this exact value. If all coordinates may be active, the uniform optimizer has zero gap. The case $k=0$ is formally allowed by the paper's natural-number wording, but has no eligible simplex point. The formal statement keeps the paper's quantifier order and does not add a positive-$k$ hypothesis.

Three milestones accompany the goal. The first records that an atomic set and its convex hull have the same support function. The second records the simplex support value $\max_i y_i$ from Table 1. The third is Lemma 3's attained sparse minimum. They are stated as mathematical claims independent of any algorithmic running-time assertion.

What the bound establishes

The source's convergence analysis gives error guarantees that decrease with the number of iterations, while its simplex example shows that using only $k$ atoms leaves primal error at least $1/k-1/n$ and, for $k<n$, gap at least $2/k$. Together they delimit what the paper's sparsity guarantees can achieve. The duality-gap claim concerns a certificate of approximation quality, so it applies even when the optimal value is unavailable to an algorithm. The result is already proved in the 2013 paper; the open work here is its Lean formalization and the finite-dimensional facts needed to connect sparse coordinates, linear optimization, and the gap.

The formalization also produces reusable interfaces for sparse simplex optimization: a coordinate-count notion of sparsity, an attained minimum formulation, and a support-function statement that avoids making a real supremum silently return a default value on an empty or unbounded set. These can serve later work on atomic methods without tying that work to one choice of Frank–Wolfe steps.

Where the argument is delicate

Bounding the quadratic objective alone does not establish the duality-gap statement. The gap also involves the best linear comparison point $s$ in the simplex. The unrestricted simplex optimum, the optimum under a sparsity budget, and the best linear comparison are different objects and must retain their respective domains. An encoding that replaces the gap's domain with the sparse feasible set would change the theorem. Another easy mistake is to use the ambient norm of a function $\mathrm{Fin}(n)\to\mathbb R$ as the objective: that norm is the supremum norm, whereas the paper uses the Euclidean squared norm.

The paper's displayed curvature value $C_f=4$ is included as a companion statement. It uses the Euclidean diameter of the simplex, which is $\sqrt2$ for $n\ge2$. The one-dimensional simplex is a single point, so extending that equality to $n=1$ would be false. The formalized companion makes the dimension condition explicit.

Formalization scope

Vectors are functions $\mathrm{Fin}(n)\to\mathbb R$. The domain is Mathlib's $\mathrm{stdSimplex}\ \mathbb R\ (\mathrm{Fin}(n))$; the objective is an explicit sum of coordinate squares, and sparsity counts nonzero coordinates. The gradient pairing in the source is represented by the Fréchet derivative applied to a direction. For this quadratic, the two agree coordinate by coordinate. The duality gap is a real supremum of those derivative values over the simplex. Its use in the goal is guarded by $k<n$, which implies $n>0$ and makes the simplex nonempty; compactness makes the supremum a maximum. The support-function milestone states equality through all upper bounds, so it also has a meaningful reading for empty or unbounded atomic sets.

The curvature set follows display (3), PDF p. 3, with step size $0<\gamma\le1$ because the printed quotient has no value at zero. The $C_f=4$ companion assumes $n\ge2$, a necessary dimension pin beyond the paper's sentence. Other standing conditions of the general problem are discharged by the chosen quadratic and simplex, rather than added as free hypotheses. No theorem assumes the quadratic minimum, a gap maximizer, or a zero coordinate as a premise; those are consequences to be established from feasibility and sparsity. The source PDF contains the statements but not its cited appendix proofs, so formal proof contributions may use other valid arguments. The simplex support, sparse minimum, and curvature interfaces are reusable beyond this mission.

Selected references

• Martin Jaggi, Revisiting Frank-Wolfe: Projection-Free Sparse Convex Optimization, Proceedings of the 30th International Conference on Machine Learning, JMLR Workshop and Conference Proceedings 28, 2013. Proceedings page.

Motivation

An assortment planner chooses which products to offer to arriving customers. When products are grouped into nests, a customer's choice of nest depends on all the assortments offered at once. A planner may nevertheless be able to generate only a short list of promising assortments for each nest. The remaining task is to choose one assortment from each list so that their combined expected revenue is as large as possible. Testing every combination requires a number of evaluations equal to the product of the list sizes. Gallego and Topaloglu show that the choice can instead be described through a linear program whose number of constraints grows with the sum of those sizes; this is Theorem 2 of their 2014 paper, in the authors' September 11, 2013 manuscript, pp. 10–12.

This mission isolates that selection result. Later parts of the paper address how to construct useful candidate lists under cardinality, space, and pricing constraints. Here the candidates are already given, and the question is which combination earns the most. The result matters whenever the candidate lists are much smaller than the space of all assortments: it makes the last step of those algorithms an exact optimization over the candidates, without enumerating their Cartesian product.

Setting

Let $M$ be a finite set of nests and $N$ a finite set of products available in each nest. An assortment $S_i\subseteq N$ is the set offered in nest $i$. Product $j$ in nest $i$ has preference weight $v_{ij}>0$ and revenue $r_{ij}\in\mathbb R$. The empty assortment is allowed. The main model has no within-nest no-purchase option, so its total offered weight is $V_i(S_i)=\sum_{j\in S_i}v_{ij}$. The conditional revenue in nest $i$ is $R_i(S_i)=\sum_{j\in S_i}v_{ij}r_{ij}/V_i(S_i)$, with $R_i(\varnothing)=0$ under the paper's $0/0=0$ convention.

The weight of no purchase outside the nests is $v_0>0$. Each nest has a dissimilarity parameter $\gamma_i\in(0,1]$. Its attraction weight is $V_i(S_i)^{\gamma_i}$. The expected revenue of a combined assortment $S=(S_i)_{i\in M}$ is

For each nest, $A_i$ is a finite nonempty collection of candidate assortments. The paper obtains these from a feasible set $C_i$, which may impose a cardinality or space constraint; Theorem 2 compares only combinations drawn from the supplied candidates. Equation (2) defines a real scalar $\widehat z$ through the maximum, over $A_i$ separately, of $V_i(S_i)^{\gamma_i}(R_i(S_i)-z)$. Problem (3) selects a maximizing candidate $\widehat S_i$ in each nest at that scalar. Linear program (4) has decision variables $(z,y_i)_{i\in M}$, minimizes $z$, and imposes $v_0z\ge\sum_i y_i$ and $y_i\ge V_i(S_i)^{\gamma_i}(R_i(S_i)-z)$ for every $i$ and every $S_i\in A_i$.

Formalization targets

The goal is the exact candidate-selection claim of Theorem 2. If $(\widehat z,\widehat y)$ minimizes $z$ among all feasible pairs of program (4), and every $\widehat S_i$ solves problem (3) at $\widehat z$, then

The milestones record three statements from pp. 11–12: equation (2) has a unique real root; the balance equation and its inequality form characterize the expected revenue of a fixed assortment; and Lemma 1 identifies the root as the best revenue attainable from candidate combinations while showing that local maximizers attain it. They separate the paper's numerical characterization of the best candidate revenue from its LP formulation. The target does not prescribe how the candidate lists were generated or claim that the selected combination is best among assortments outside those lists.

Significance

The theorem gives an exact, compact choice rule for assembling nestwise candidates. If the lists contain useful assortments under the original constraints, their best combination can be selected through program (4). The rest of the paper establishes candidate-generation and approximation results under particular constraint families; the stitching theorem supplies the common final selection step for those results. A larger candidate list may improve the obtainable revenue, but its Cartesian product need not be searched explicitly. The authors' manuscript, p. 12, states that program (4) has $1+m$ variables and $1+\sum_i|T_i|$ constraints when the candidates are indexed by $T_i$.

Formalizing the theorem yields a reusable statement about the interaction of a fractional revenue objective, independent nestwise candidate families, and a shared scalar LP. The published Prove2Me definition NestedLogitVariants.LP.Model already supplies the instance, $V_i$, $R_i$, $\Pi$, and the feasibility and optimality predicates for program (4). Its previously proved lp4_opt_binding concerns an equality at an LP optimum under ordered, nonnegative revenues; it does not contain Theorem 2's maximality claim under this paper's revenue assumptions. The four statements in this mission are draft targets awaiting machine-checked proofs.

Difficulty

Optimizing a candidate independently in every nest at an arbitrary value of $z$ does not generally optimize the combined revenue: the revenue denominator couples all nests. Likewise, an LP-feasible value need not be its minimum, and using such a value in problem (3) does not establish the theorem. The substantive assertion is that choosing the local maximizers at the optimal LP value solves the combined selection problem. The unique-root statement also needs care at empty assortments, where a nest contributes zero attraction and the conditional revenue uses the paper's $0/0$ convention.

Formalization scope

Nests are represented by any finite type, and products by Fin n, indexed $0,\ldots,n-1$ rather than the paper's $1,\ldots,n$. A Boolean offer vector is represented by Finset (Fin n); $\overline 0$ is the empty finset. Each $A_i$ is a finite set of such assortments. There is no single-nest or $\gamma_i=1$ specialization, and no substitution of all possible assortments for the supplied candidates. The LP assumption is its full minimum objective property, not merely feasibility. The imported LP4Optimal predicate uses a set of candidates, supplied by coercing each finite $A_i$ to a set.