Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
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.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic 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 -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
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.
The sharp Hlawka inequality for Schatten -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 . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Best subset selection with ridge shrinkage asks for a sparse linear model: given a design matrix and responses , minimize
where counts nonzero coefficients. The problem is NP-hard, and exact methods solve it as a mixed integer program by branch-and-bound (Bertsimas, King, Mazumder 2016). The speed of branch-and-bound is governed by two things: how tight the continuous relaxation at each node is, and how cheaply that relaxation can be solved.
Hazimeh, Mazumder and Saab (arXiv:2004.06152v2; Mathematical Programming 2022) build a branch-and-bound solver whose node relaxations are solved by first-order methods rather than by a conic interior-point solver. Their starting point is the perspective formulation, a standard device for strengthening relaxations of mixed integer programs with indicator variables (Frangioni, Gentile 2006; Günlük, Linderoth 2010). Theorem 1 of the paper shows that the interval relaxation of this formulation is a box-constrained least squares problem with a separable penalty in alone. This mission formalizes Theorem 1.
Timeline. Owen (2007) introduced the reverse Huber penalty as a hybrid of lasso and ridge. Dong, Chen, Linderoth (2015) showed that the interval relaxation of the perspective formulation without a Big-M bound reduces to least squares with a reverse Huber penalty. Hazimeh, Mazumder and Saab (2020–2021) added the Big-M constraint and obtained Theorem 1, with a second regime in which the penalty becomes .
Fix , , , and , and write . The perspective formulation is problem (3) of the paper:
Here indicates whether may be nonzero, stands in for through the rotated second-order cone constraint , and bounds . The interval relaxation replaces with .
The reverse Huber penalty (4) is for and for . Put
and let if and if . The reduced relaxation (5) is
with optimal value . For one coordinate , is the minimum of over , , , .
The interval relaxation of (3) is equivalent to (5):
and both problems attain the common optimal value .
The result. Theorem 1 removes the auxiliary variables and all conic constraints from the node relaxation. What remains is a composite problem, a smooth least squares loss plus a separable, convex penalty under a box constraint, to which coordinate descent and proximal methods apply directly. The paper's solver, its active-set strategy, and the dual bounds of its Section 3 are all built on (5). The theorem also exposes a regime change: when , the ridge term of the perspective formulation disappears from the relaxation and the penalty is pure . Propositions 1 and 2 of the paper, which compare the strengths of the perspective, Big-M and relaxations, use this reduced form.
Formalizing it. The result is proved in the paper (Appendix A) by a coordinatewise argument. To our knowledge it has no machine-checked proof. Formalizing it gives a verified bridge from the conic mixed integer formulation to the penalized form that later results of the paper use, and a checked case analysis at the regime boundary , where the two formulas must agree with the stated tie-breaking.
The obvious approach, "minimize over and coordinate by coordinate", is correct in outline, but each step hides a boundary case. The rotated cone constraint degenerates at or , where is undefined, and the paper's convention for must be handled. The one-variable problem (36) is a minimum of a pointwise maximum of two functions of , one convex and decreasing then increasing, the other increasing. Its minimizer lies either in the interior of the region where the first term dominates or on the crossover , depending on the regime. The paper's proof describes the cases loosely: it optimizes the Case I term without imposing the side condition that Case I attains the maximum. A complete argument must prove the lower bound over all feasible , not just evaluate at a candidate. Finally, the minimum over must be shown to split into a sum of coordinate minima, each attained.
Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ, and reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M; the paper's is Fin p. The squared norm is the explicit sum , and is for all . The cone constraint is kept in product form . In and (36), Lean's coincides with the paper's convention for . Every "min" is stated with IsLeast (membership plus lower bound), so attainment is part of each statement. is defined as a real infimum over the box, and Theorem 1 asserts that this infimum is attained by both problems. No normalization of or is assumed; the paper's unit-norm assumption starts in Section 3. The paper writes no in these results, so there are no constants to instantiate.
A goal stating only one inequality (that is achieved by some , or that it bounds the relaxation from below), or a goal over , would not be Theorem 1. The IsLeast form rules out both. The goal uses with both regimes.
A complete development needs: a two-variable convexity argument for on ; a lemma that the infimum of a separable objective over a product of feasible sets is the sum of the coordinate infima; and continuity of with compactness of the box to obtain an optimal . The coordinate lemmas and the definition of the reverse Huber penalty are reusable in the companion missions on relaxation strength and Lagrangian duality. Contributions to any milestone, or an alternative proof of the goal, are welcome.
Thompson sampling (TS) selects each action by sampling a parameter from the current posterior and playing the action that is optimal for the sample. It is a stationary randomized strategy: the distribution of the action is a fixed function of the posterior, the same in every period, and the action is drawn at random from it. Its Bayesian regret bounds, surveyed in §8.1 of the tutorial by Russo, Van Roy, Kazerouni, Osband and Wen (Found. Trends Mach. Learn. 11(1), 2018), grow sublinearly in the horizon .
A natural question is whether the randomization is essential. A strategy that maps the posterior to an action deterministically, for example "play the action with the highest posterior mean", is equally stationary and conceptually simpler. §8.1.3 of the tutorial answers the question with Example 8.1 (A Known Standard), taken from Russo and Van Roy, Learning to optimize via information-directed sampling (Operations Research 66(1), 2018): in a two-action problem with a known baseline action, every stationary deterministic strategy suffers linearly growing expected regret under some prior. The example is the standard justification for why posterior sampling, and not a deterministic function of the posterior, is the right stationary rule.
There are two actions and a binary unknown parameter with prior
In each period the agent selects an action and observes a binary reward . Rewards are conditionally independent across periods given and the actions:
The mean reward of action is its success probability, and the optimal action is action if and action if , so or .
The history lists the actions and rewards of the first periods. The posterior is given by Bayes' rule (4.2) of the tutorial, applied period by period:
with the prior on the empty history.
A stationary deterministic strategy is one function from posterior probabilities to actions, used in every period: . The expected cumulative regret (Bayesian regret, p. 71) of running from the prior for periods is
the expectation taken over and the rewards. The Lean development names these objects succProb (), optMean (), post (), Strategy (), lawGiven (the probability of a history given ) and expRegret.
This is the sentence "for any deterministic stationary strategy, there exists a prior probability such that expected cumulative regret grows linearly with time" (p. 79). The prior is chosen after the strategy. No constant is fixed; only the linear shape is asserted.
The example separates two properties that regret analyses often conflate: being a function of the posterior alone (stationarity) and achieving sublinear Bayesian regret. It shows that a stationary strategy with sublinear regret on all priors must randomize, which is the structural reason TS samples rather than maximizes. It also explains why deterministic algorithms with good regret, such as upper confidence bound methods, are necessarily nonstationary: their confidence radii depend on the period and on counts, not only on the posterior.
The tutorial gives the argument in one paragraph. A formal version makes precise what is left implicit there: that the posterior is the actual conditional probability computed from the history, that "uninformative" means the posterior is invariant under action , and that under action the posterior never leaves . The result is a closed-form regret identity in each case, not only an asymptotic statement. As far as is known, neither the example nor its source in Russo and Van Roy (2018) has been machine-checked.
The mathematics is elementary; the work lies in the bookkeeping of a history-dependent strategy. The strategy's action in period depends on the whole history through , so the law of is a product of indicator factors, each evaluating at a posterior computed from a prefix of the same history. A direct computation of the regret must show that every history of positive probability follows a single action path, and that is a statement about the posterior along every prefix, not only at the first period. A first attempt that defines the posterior by a recursion in which "the posterior stays at " is built in proves nothing about the example; the posterior must be Bayes' rule applied to the history.
0 : Fin 2, action is 1 : Fin 2; is true; a reward of is true. Lean period s : Fin T is the paper's period .Fin t → Fin 2 × Bool; every probability and expectation is a finite sum, so no measure theory is needed.post is the closed form of iterated Bayes' rule (4.2). The probabilities with which the strategy picks its actions are or and do not depend on ; on histories of positive probability they cancel, so post is the true conditional probability there. For its denominator is positive, so Lean's convention is never used.ℝ → Fin 2; its values outside are never used. The same function acts in every period, which is what "stationary" means.The tutorial's argument for the example is on p. 79; the tutorial attributes the example to Russo and Van Roy (2018).
A chance-constrained program chooses a decision so that a random vector falls outside a decision-dependent safety set with probability at most . Chance constraints are a standard model for reliability requirements in power systems, supply chains and transportation, where a plan must survive random demand or supply with high probability. In practice the distribution of is known only through samples , and the sample average approximation (SAA) that replaces it by the empirical distribution is sensitive to the particular sample.
Distributionally robust chance constraints regularize SAA by requiring the probability bound for every distribution within Wasserstein distance of . Chen, Kuhn and Wiesemann (arXiv:1809.00210) and Xie (doi:10.1007/s10107-019-01445-5) showed that, for safety sets defined by linear inequalities, the resulting program (DR-CCP) is a mixed-integer linear program with a big-M constant. These big-M formulations are hard for solvers to close when is small. Ho-Nguyen, Kılınç-Karzan, Küçükyavuz and Lee (doi:10.1007/s10107-020-01605-y) connect the formulation to the mixing sets of SAA and to robust 0–1 programming, and derive a smaller and tighter formulation that is still exact.
The random vector lives in with an arbitrary norm ; in the formalization it is a finite-dimensional real normed space . The dual norm of a linear functional is . The decision ranges over a set .
The 1-Wasserstein distance between distributions is the infimum of over couplings of and . The ambiguity set is the set of distributions within distance of . The feasible region of (DR-CCP) is
Throughout, and are fixed.
The paper studies joint chance constraints with right-hand side uncertainty: for there are , and , and
Write and . Let be the -th largest value among , and let .
The big-M formulation (5) of Chen et al. uses binaries , slacks and a scalar with
The paper's improved formulation (20) keeps the first two families, adds the knapsack constraint , replaces in the third family by , imposes it only for , and adds for every .
The goal states equality of feasible sets of . Because the objective depends on alone, this is the paper's "exact reformulation".
Milestones 2 and 3 are results of Chen, Kuhn and Wiesemann that this paper cites and uses, not results it proves.
Theorem 3 says that the scenario-wise big-M rows of the Wasserstein chance constraint can be replaced by at most rows per , with coefficients computed from the data. Remark 2 of the paper counts at least fewer rows than (17). The reduced form exposes a robust 0–1 substructure, and the paper adapts Atamtürk's valid inequalities for it. Its computational study reports order-of-magnitude speed-ups on stochastic transportation problems.
The results are proved on paper; none is machine-checked. The formalization would give a verified chain from the Wasserstein worst-case probability to a finite mixed-integer system. Milestone (3), the dual reformulation, is reusable for any distributionally robust chance constraint over a 1-Wasserstein ball around an empirical distribution, and (4b) for any polyhedral safety set. A second formalization layer would verify the order-statistic arguments (Lemma 1, Proposition 1) used throughout the quantile-strengthening literature.
The deterministic parts — Theorems 1–3 given (3) and (4b) — are finite case analyses on , but each step relies on order statistics of the sample with ties. Lemma 1 rests on the paper's "without loss of generality, sort the distances", and a formal proof must handle ties and the floor exactly. The paper's proof of Theorem 2 argues "at optimality"; for a statement about feasible sets that argument has to be replaced by an explicit choice of .
The hard step is (3). It exchanges a supremum over all Borel probability measures in a Wasserstein ball for a scalar system. The naive attempt, which perturbs by moving mass from the samples to the nearest unsafe points, proves only one inclusion. The other needs strong duality for worst-case probabilities over transport balls, together with attainment of the dual infimum, which uses .
E with [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] and its Borel σ-algebra. The norm is arbitrary, not the sup norm of Fin K → ℝ.StrongDual ℝ E), so is its operator norm.Fin L → ℝ, with written a p ⬝ᵥ x. Indices are 0-based.ModelRiskOT.WorstProb.worstProb with cost , valued in , around the published WassersteinDRO.Duality.empiricalDistribution.Metric.infDist.Standing assumptions and pins in every statement:
In (17b), the printed "(5b)–(5d) and (5c)" is read as "(5b)–(5d) and (8c)", following the proof of Theorem 2 and (20b).
Several trivializing formalizations are ruled out:
infDist never sees the empty set;Welcome contributions:
Given a graph that is promised to be -colourable, how many colours are needed to find a proper colouring in polynomial time? The decision version asks to distinguish -colourable graphs from graphs that are not even -colourable. It has been studied since Garey and Johnson (1976) and is conjectured to be NP-hard for all fixed . This is the approximate graph colouring problem, and it is one of the motivating examples of promise constraint satisfaction problems (PCSPs).
Timeline of the NP-hardness results without extra assumptions, as surveyed in Example 2.9 and §6.2 of the paper:
The method also applies to the question of 5-cycle versus 3-colouring, which Brakensiek and Guruswami had raised as an open case.
A relational structure consists of a finite domain and relations , one for each symbol of a signature. A PCSP template is a pair of structures with the same signature and a homomorphism . Write .
An -ary polymorphism from to is a map that, applied coordinatewise to any tuples of , returns a tuple of . For and these are exactly the -colourings of the power . The set of polymorphisms of all arities is closed under minors: for . A minion is any nonempty set of functions of arities that is closed under minors. A minion homomorphism preserves arities and commutes with minors. Write .
An Olšák function is a 6-ary function with
The free structure has the -ary members of as its domain and relations defined by minor identities that follow the tuples of .
For every ,
is left unspecified, as in the paper. This is the statement from which the paper deduces that versus colouring is NP-hard.
One further item, not a milestone, shows the bound is sharp. Proposition 10.1 says that contains an Olšák function.
Theorem 6.2 is a criterion stated entirely inside the minion. Together with the reduction theory of the paper (a minion homomorphism gives a log-space reduction from to ) and the NP-hardness of approximate hypergraph colouring (Dinur, Regev and Smyth 2005), it shows that every finite template without an Olšák polymorphism has an NP-hard PCSP (Corollary 6.3). Lemma 6.4 then settles the 3 versus 5 colouring case and improves the bound to for every . Proposition 10.1 shows that this criterion cannot go beyond .
The results are proved in the paper. None of them has a machine-checked proof that this mission knows of. This mission produces a Lean statement of the minion side of the argument. That includes the free-structure correspondence (Lemma 4.4), which every later application of the theory uses, and Theorem 6.2 for arbitrary finite minions. A finished formalization would include the clique argument behind Lemma 6.4 and would check the key hardness inequality of the paper by machine.
Lemma 6.4 is a statement about every -colouring of that is constant on certain triples of vertices. The power graph has vertices, so exhaustive search is out of reach for general , and case checks for do not give the general claim. Showing that colours do not suffice requires an explicit obstruction, uniform in , in the graph obtained by identifying those triples; the identification creates edges that are not present in , and keeping track of them is the combinatorial core. The bound is tight (Proposition 10.1), so no argument that would also apply to colours can work.
In Theorem 6.2 the direction from "no Olšák function" to a minion homomorphism must build a minion homomorphism into out of nothing but the absence of a single identity. That direction depends on Lemma 4.4, which relates maps defined on functions of a single arity to minion homomorphisms defined on all arities; in Lean the bookkeeping of enumerations, minors and dependent arities is substantial.
The development reuses the published relational-structure layer PCSPBLPAff_Symmetric_Setting (RelStruct, IsHom, IsPolymorphism, IsPromiseTemplate). Domains are Fin k. and have one-symbol signatures of arity 2 and 3. Polymorphisms apply to the columns of an matrix whose rows lie in , which is the paper's matrix transposed. A minion is a family mem n of -ary functions (Fin n → A) → B with no nullary members, nonempty and closed under the minors fun x => g (x ∘ π). A minion homomorphism is a family of maps that preserves membership and minors on members, with unconstrained values outside the minion, so Lemma 4.4's "one-to-one" is stated up to agreement on the minion. Theorem 6.2 assumes the minion's sets are finite, which is the paper's standing convention (Definition 2.20). The free structure takes an enumeration of the generating domain and quantifies the enumeration of each relation existentially. In the goal, makes free of natural-number truncation.
The codomain of the goal is exactly with . A minion homomorphism into an arbitrary or existentially chosen minion, or into with , would be trivial and is ruled out by the statement.
Not formalized. The NP-hardness conclusions of Theorem 6.5 and Corollary 6.3 are left out, and so are the log-space reduction of Theorem 3.1 and the cited hardness of approximate hypergraph colouring (Theorem 5.23, [DRS05]). There is no complexity-theoretic substrate in Mathlib for them. Lemma 6.6 () is a natural follow-up item. Contributions are welcome on every milestone. Lemma 4.4 and the minion layer can be reused beyond this mission, for any minion-homomorphism argument in the PCSP literature.
Many algorithms in signal processing, statistics and machine learning share one template: replace a hard objective by a simpler function that lies above and touches it at the current point , minimise that surrogate, and repeat. The expectation–maximisation (EM) algorithm, difference-of-convex (DC) programming, proximal minimisation and many majorisation–minimisation schemes are of this form. Razaviyayn, Hong and Luo (arXiv:1209.2385; SIAM J. Optim. 23 (2013) 1126–1153) call the single-block version Successive Upper-bound Minimization (SUM) and give a short set of conditions on the surrogate under which every limit point of the iterates is a stationary point, without convexity or smoothness of .
Their single-block result, Theorem 1, is the base case of the paper. The block versions (BSUM, and block successive convex approximation with Armijo steps) are the subjects of the next two missions in this series. Earlier convergence results for related schemes were weaker: the inner approximation algorithm of Marks and Wright (1978), cited on p. 5–6 of the paper, guarantees stationarity only if the whole sequence converges, and only for smooth objectives.
Let be a closed convex set and an objective whose relevant values are those on (the paper assumes ). The problem is
The directional derivative of a function at in direction is the lower limit
an extended real number. A point is a stationary point of (2) if and for every with ; the set of stationary points is .
An approximation function satisfies Assumption 1 if
The SUM algorithm starts from and, for , sets to an arbitrary element of . A limit point of the iterates is the limit of some subsequence .
Under Assumption 1, every limit point of the iterates generated by the SUM algorithm is a stationary point of (2):
The theorem asserts nothing about existence of limit points or of minimisers of the subproblems; it holds for every run the algorithm can produce.
Theorem 1 reduces the convergence analysis of an entire family of algorithms to checking four properties of a surrogate. Proposition 1 makes (A3) checkable in the common composite case "smooth plus nonsmooth": majorise only the smooth part and keep the nonsmooth part unchanged. Corollary 1 turns the limit-point statement into convergence of the whole sequence to the stationary set when the level set is compact. The block-coordinate results of the same paper (Theorems 2–4) reuse the structure of this argument block by block.
The results are proved on paper; to our knowledge none of them has a machine-checked proof. A formal development would supply a reusable account of extended-real lower directional derivatives on convex sets, the first-order necessary condition for constrained minimisers in that generality, and the limit-point argument for descent methods with a continuous surrogate, all of which recur in the analysis of block coordinate and majorisation–minimisation methods.
The argument is short, and the difficulty lies in its precise use of the hypotheses. The surrogate inequality must be passed to the limit along a subsequence, and only joint continuity of (A4) on allows this: itself is not assumed continuous, so the natural first idea of passing to the limit is not available. The derivative is a liminf in the extended reals, so it may be , and the comparison between and is made only through (A3) at the single point and only in feasible directions. For Proposition 1, (4)–(5) give only a one-sided inequality between the derivatives of and at , because may lie on the boundary of ; equality needs an argument at interior points of a feasible segment and the continuity of the derivatives.
The space is EuclideanSpace ℝ (Fin m) (the 2-norm of p. 4). The directional derivative is the published TsengBCD.Stationary.dirDeriv (Tseng 2001), an EReal-valued liminf over , used as a reference item. The definitions module BSUMConv.SUM.Setting provides IsStationaryOn, stationarySet, AssumptionA1–AssumptionA4, Assumption1, the run predicate IsSUMRun and the level set levelSet0.
Conventions committed to:
MapClusterPt), not the limit of a convergent sequence.The statements cannot be trivialised: Assumption 1 is satisfiable (for instance by the proximal surrogate of §VIII-B for suitable ), stationarity is a genuine condition (it fails for at any on ), and Theorem 1 is about every cluster point, not about runs assumed convergent. Contributions welcome: proofs of the three milestones, of Theorem 1 from them, and of the two companion statements; general lemmas about dirDeriv (constants, sums with a function having a finite one-sided derivative, first-order conditions on convex sets) are reusable across this series.
The optimal assignment problem asks for a one-to-one matching of points to objects of least total cost. It is the discrete optimal transport problem between two uniform measures with the same number of atoms, and by the Birkhoff–von Neumann theorem it coincides with the Kantorovich linear program on that instance (Peyré and Cuturi, Computational Optimal Transport, Proposition 2.1). Assignment solvers are therefore the inner routine of exact discrete optimal transport, of matching-based estimators in statistics and of many combinatorial optimization pipelines.
The auction algorithm was introduced by Bertsekas in 1981 (Bertsekas 1981) and refined with ε-scaling by Bertsekas and Eckstein in 1988 (Bertsekas & Eckstein 1988). It is a dual coordinate method with an economic reading: unassigned points bid for objects, prices of contested objects move, and an object changes hands when outbid. Its practical appeal is that each iteration is local and cheap, and that it parallelizes well. Peyré and Cuturi present it in §3.7 of their monograph (pp. 417–422) as an alternative use of the machinery of C-transforms, and as a precursor to the Sinkhorn algorithm of Chapter 4.
Fix , write , and let be a cost matrix: is the cost of assigning point to object . A permutation of is an assignment, of cost .
A dual vector (price vector) is indexed by the objects. Its -transform is , the best adjusted cost available to point ; a pair is dual feasible if for all .
The algorithm maintains a triplet : a set of assigned points, a partial assignment vector (an injective map from to ) and a dual vector . The state satisfies ε-complementary slackness (ε-CS) if
One iteration picks a point , a lowest adjusted cost index and a second lowest , and performs
removes from the point with (if there is one), sets and adds to . The algorithm starts from , , and terminates when .
For every and every run of the algorithm that terminates, the final is a permutation and
The goal fixes no particular tie-breaking rule and no order in which unassigned points bid: it holds for all of them.
For , every run has at most iterations. This is the termination statement; the goal does not depend on it.
Proposition 3.9 is the accuracy guarantee of the auction algorithm. With integer costs and it yields an exactly optimal assignment, which is how the algorithm is used as an exact solver; combined with ε-scaling it gives the complexity bounds quoted in Remark 3.3. The argument is also the template for every ε-relaxed primal–dual method: an approximate optimality certificate maintained by local moves, turned into a global suboptimality bound by weak duality.
The results are classical and proved in the book and in Bertsekas's monographs; they are not open. What this mission adds is a machine-checked account of the algorithm with all of its nondeterminism (ties in the argmins, the order of bidders) quantified explicitly, together with the corrected iteration bound. To the best of the mission's prior-art search, no Lean formalization of the auction algorithm exists on the platform or in Mathlib, which has the assignment problem only implicitly (through permutations and doubly stochastic matrices).
The obvious argument for the goal sums the ε-CS inequality over and compares with an arbitrary permutation . The sum telescopes only if the final is a bijection, so the proof must carry, through every iteration, the invariant that is injective on , and this invariant interacts with the removal of the displaced point in step 2: the set update has to remove exactly the point holding , which needs injectivity at the previous step.
Preserving ε-CS for the points that are not bidding relies on prices only ever decreasing, which in turn needs and the specific form of (3.9); preserving it for the bidder needs the second-best index to realize the minimum over , including in the presence of ties. The printed termination bound is false (see below), so the companion requires reconstructing the counting argument: an object that is still unassigned has never been bid on and keeps price , which caps the number of bids on any other object.
Fin n; is a Matrix (Fin n) (Fin n) ℝ; prices are Fin n → ℝ; is the infimum over the finite nonempty index set.S : Finset (Fin n), ξ : Fin n → Fin n and g : Fin n → ℝ. Only the values of ξ on S are meaningful; injectivity on S is a property to be proved, not a field.AuctionStep), with the choice of bidder, of and of existential. A run of iterations is a sequence of states starting from , ; it is terminated when at step . The results hold for every run, whatever the tie-breaking.Contributions welcome: the injectivity invariant of ξ on S as a reusable lemma; the milestones in any order; a proof of termination (the companion) and of the existence of a terminated run for every .
A buyer can reduce production cost by using a supplier whose operations carry a risk of a responsibility violation. That choice can also bring a direct penalty and cause customers to leave. Guo, Lee, and Swinney study how the cost saving, consumer demand, and violation risk jointly determine the buyer’s sourcing decision in a transparent supply chain. Their model distinguishes customers who value responsible production from those who do not, making it possible to ask when the buyer uses a responsible supplier, a risky supplier, or both. The question concerns supplier selection when the buyer knows each supplier’s responsibility type and customers can react to a violation. Guo, Lee, and Swinney (2016) give the model and its four strategy regions.
A single buyer sells to a market whose total size is normalized to one. A responsible supplier has marginal cost and no responsibility violation in the model. A risky supplier has lower marginal cost and a violation occurs with probability . Write for the responsible supplier’s cost premium. A violation costs the buyer a fixed amount .
Every consumer has baseline willingness to pay . A fraction is socially conscious and has additional willingness to pay for a responsibly sourced product. Upon a violation, a fraction of this group exits the market. The remaining fraction has no responsible-sourcing premium and does not exit for that reason. These symbols and ranges follow the paper’s Section 3; the theorem adds no sign restriction to , , or .
The buyer chooses among four sourcing strategies. Low-cost sourcing (LC) uses the risky supplier for the whole market. Dual sourcing (DS) serves socially conscious consumers with responsible units and other consumers with risky units. Responsible niche sourcing (RN) serves only socially conscious consumers with responsible units. Responsible mass market sourcing (RM) serves everyone with responsible units. With denoting strategy ’s expected profit, Table 2 gives
A strategy is optimal when its profit is at least the profit of each of the four strategies. This definition allows ties. In the statements below, , as defined immediately before Proposition 1. Section 4 and Table 2 are the sources for these formulas.
The goal is all four clauses of Proposition 1, p. 2729, as printed. For LC, the sufficient conditions are
For DS, they are
For RN, the threshold is ; for RM it is . Each of these last two clauses also requires that neither LC nor DS be optimal. They are stated for , since their displayed quotient is undefined at zero. The six milestones record the pairwise strategy comparisons stated in the appendix proof, in its order: LC with DS, RM, and RN; RN with RM; and DS with RN and RM. Proposition 1 and its appendix proof supply these targets.
The proposition partitions the buyer’s decision into explicit sufficient regions. It identifies when the low cost of risky sourcing outweighs expected violation costs, when serving both segments separately pays, and when responsible sourcing should serve only the conscious segment or the full market. The four profits also provide the base for the paper’s later comparative statics on sourcing quantities, penalties, and transparency. Those later propositions are outside this mission; their exact treatment of strategy ties and sourcing quantities warrants a separate development. Guo, Lee, and Swinney (2016) establish these results in the published article.
The mathematical result is proved in that article. The formalization task is to give its parameter ranges, four profits, and optimality claims a machine-checkable statement, then prove the pairwise comparisons and the four-clause goal. The draft statements compile locally, but their proofs are open. The resulting model and comparisons can support later formalizations of the article’s other propositions.
The four choices must be compared under a single, consistent profit table. A comparison with one competitor does not establish optimality among all four, and the positive-part term in Proposition 1 compresses two distinct comparisons into one threshold. Boundary cases also matter: a strict “preferred to” comparison can disappear when its profit difference is zero, even though weak optimality remains meaningful. The printed sufficient condition in part (ii) uses inside the violation term, while the appendix’s DS comparisons use . Both statements must retain their respective printed forms; treating them as the same expression would change the source claim.
Lean represents the eight parameters by real fields of one record and the four strategies by a finite inductive type. The range assumptions are and . The cost premium is defined from the two costs. The theorem compares exactly the four Table 2 profits; the Section 3–4 derivation of prices and quantities from the underlying selling game is outside this mission. An optimal strategy is weakly best against all four strategies, including itself. A model with fewer competitors or profits that differ from Table 2 would not capture the proposition.
The clauses containing division by require . The appendix’s strict LC–DS equivalence additionally requires and ; otherwise equal profits can defeat its “if and only if” wording. Proposition 1 itself retains the full standing ranges. No positivity of , , or is assumed. Part (ii) retains the printed , which makes its hypothesis stronger than the corresponding appendix conditions with . Its conclusion remains valid under the standing ranges. These conventions are visible in the statements and can be checked independently of the paper’s informal derivation.
The development needs only real arithmetic, finite case analysis, the four profit definitions, and the maximum of a real number with zero. The parameter record and strategy comparison interface are reusable for later propositions in the same paper. Contributions that prove the exact milestone statements, establish the goal, or clarify behavior at ties are within scope.
Nesterov's accelerated gradient method minimizes a smooth convex function at the rate in the number of iterations , against for plain gradient descent. Su, Boyd and Candès (arXiv:1503.01243) observed that, as the step size tends to zero, Nesterov's scheme becomes the second-order differential equation
with , a heavy-ball system whose friction coefficient vanishes as (asymptotic vanishing damping). Studying (1) in continuous time gives Lyapunov arguments that are then discretized into new algorithms.
Attouch, Chbani, Peypouquet and Redont (Math. Program. 168 (2018), DOI 10.1007/s10107-016-0992-8) analyse (1) for general . This mission formalizes their result for strongly convex , where the rate of convergence of (1) depends on and improves without bound as grows.
Timeline.
Let be a real Hilbert space with inner product and norm , and let be continuously differentiable with gradient . Fix and . A solution of (1) is a twice differentiable trajectory with velocity satisfying (1) at every .
is strongly convex with constant if
Such a has exactly one minimizer , and .
For , the anchored energy is
a sum of nonnegative terms. The proof of the main theorem fixes
For strongly convex and , every solution of (1) converges strongly to the unique minimizer , and
as . The goal states the asymptotic form; the explicit constants are milestones.
The theorem shows that the rate of (1) on strongly convex functions is not capped at or : the exponent grows linearly in , and it already exceeds for every . It extends [44, Theorem 4.2], which needs and gives . The same parametrized energy is the template for the discrete analyses of Nesterov-type algorithms with parameter , so its derivative identity (10) is reusable beyond this mission.
The result is proved on paper. To the best of current knowledge none of it is formalized: Mathlib has no theory of inertial dynamics, and the platform's strongly convex rates concern discrete methods. A completed mission gives a machine-checked Lyapunov analysis of a non-autonomous second-order ODE in a Hilbert space, with the explicit constants of the paper.
The derivative identity (10) is a computation, but it must be carried out with one-sided derivatives at , real powers , and the chain rule for in an infinite-dimensional space. The obvious argument, that is nonincreasing, fails: even with the best choice of and the bound on its derivative keeps a term of no fixed sign, and only for is the quadratic term in nonpositive. Passing from the differential inequality to (26) therefore needs integration on for functions known only through one-sided derivatives. The velocity bound then combines (26), (27) and (28) through square roots, and the goal additionally requires the existence of the minimizer in an infinite-dimensional space, which is a compactness argument (weak lower semicontinuity) and not an algebraic one.
InnerProductSpace ℝ H, CompleteSpace H), not . is ContDiff ℝ 1 and is Mathlib's gradient.Asymptotics.IsBigO along atTop; strong convergence is norm convergence. The existence and uniqueness of are conclusions of the goal, not hypotheses, so the goal cannot be satisfied vacuously by an empty argmin; the strong-convexity hypothesis is satisfiable (e.g. with , and solves (1)).Useful infrastructure: the derivative of via gradient, integration of differential inequalities on , and existence of minimizers of strongly convex continuous functions on Hilbert spaces. Proofs of any milestone, and of the goal from the milestones, are welcome.
Proximal gradient methods are used to minimize an objective with one smooth part and one convex part whose proximal map can be evaluated. A small proximal gradient step is a practical stopping signal, but it indicates proximity to an optimizer only when the objective has an appropriate error bound. Section 4 of Drusvyatskiy and Lewis gives conditions for that bound in the structured problem : the conditions concern the dual problem and the growth of the two component functions, rather than requiring strong convexity of their sum. This matters for problems with a nontrivial solution set and for penalties that are not strongly convex. The paper places this result after its §3 comparison of quadratic growth and proximal gradient error bounds (pp. 9–11).
Let and , with their Euclidean inner products and norms. Let be linear, be continuously differentiable and convex, and be proper, lower semicontinuous, and convex. The primal objective and its minimizer set are
The mission assumes is nonempty and bounded. Its minimum is finite. For an extended-real function , its Fenchel conjugate is . The dual objective is , and denotes a dual minimizer. The effective domain is ; denotes relative interior. The paper assumes dual nondegeneracy, , and dual strict complementarity, (p. 10).
A closed convex function is firmly convex relative to when its tilt grows at least quadratically away from its minimizers on each compact set. The positive coefficient may depend on the compact set. Theorem 4.2 assumes this property for at and for at (Definition 4.1, p. 11).
For , a proximal gradient step is , and its residual is . The error bound asks whether the distance from to is controlled by whenever lies below a prescribed objective threshold (Definition 3.1, p. 5).
The milestone path records the Kuhn–Tucker description of , the relative-interior identity (4.3), the compact-set distance estimate (4.4), the two component inequalities (4.5), and the resulting quadratic growth of on every sublevel set. In particular, for each there is such that
These are the claims stated in §4 and in the proof of Theorem 4.2, pp. 10–11. The milestone for (4.5) retains the paper's printed in its quotation, while the Lean statement uses positive constants, as Definition 4.1 requires for nontrivial quadratic growth.
The goal is Theorem 4.2: under the conditions above, for every there exist such that
The formal statement makes explicit that has a Lipschitz constant. This is part of the §3 setting used by the paper's Corollary 3.6 to reach the displayed error bound. A companion statement, Theorem 4.5, pp. 12–13, says that the Moreau envelope of a firmly convex function retains firm convexity relative to the same vector.
The conclusion converts dual geometric information and component growth into an error bound expressed through a proximal gradient step. The residual is available when running the method, whereas the distance to is generally not. Combined with the paper's §3 results, the error bound yields local convergence guarantees for the proximal gradient method in structured convex problems (Corollary 3.6 and Theorem 4.2). The statement covers settings in which component functions have local quadratic growth after a tilt while the composite objective need not be strongly convex.
The research result is proved in the paper. The work of this mission is to formalize its exact assumptions and claims, including the convex dual and the relative-interior statements, then supply machine-checked proofs. The resulting Euclidean conjugate, firm-convexity, and structured-objective definitions can also support other convex optimization formalizations. The statements in this proposal are proof obligations; compiling the statements alone does not establish the theorems.
Component growth concerns distance to separate subdifferential inverse images. The desired error bound concerns distance to their intersection, which is the primal solution set. Two small component distances do not automatically control distance to an intersection: the sets can meet at a poor angle. The dual interior hypotheses supply the regularity needed in (4.4). The argument also changes the quantity being controlled from objective growth to a proximal gradient residual. Those two changes are the substantive steps a proof must justify; treating either as an unrestricted distance identity would change the theorem.
The Lean spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); dimensions zero are permitted. The linear map is continuous, and is its adjoint. Extended-real values use EReal; properness excludes values, and lower semicontinuity encodes closedness. Conjugates take suprema in EReal, and the dual objective follows (4.2). Relative interior is intrinsicInterior ℝ. The published convex subdifferential, proper-convex predicate, and proximal-point predicate are imported as reference items because their meanings match the paper's objects. The paper's Euclidean conjugate is defined locally because the available published conjugate has a strong-dual codomain.
The minimum value is real and is pinned to the nonempty primal minimizer set. The dual point is pinned as a minimizer of . Proximal steps are expressed as argmin predicates, so no default result is chosen for a failed minimization. The firm-convexity predicate requires a nonempty minimizer set of the tilted function: otherwise Lean's real distance to the empty set would be zero while the source uses an infinite distance. The growth constant of Definition 4.1 and the constants of (4.5) are strictly positive: the page leaves the sign implicit or prints , but with a zero constant every convex function would be firmly convex, contradicting the page's own example , and the growth statements would be empty. The error bound is restricted to the stated sublevel set, and all of its constants are positive. The goal includes a nonnegative Lipschitz constant for , disclosed because the source's §3 bridge to the error bound assumes one; the component-growth milestones do not assume it.
Contributions should establish the Euclidean convex-duality identities, the compact-set regularity estimate, the component and composite growth claims, and the proximal gradient conclusion. The Moreau-envelope preservation theorem is a separate companion target. None of the dual interior conditions or the firm-convexity assumptions may be replaced by a vacuous condition: the goal concerns their effect on the actual solution set of .
Fractional programs minimize a ratio over a constraint set. They arise whenever a quantity has to be normalized: the scale-invariant sparse recovery model minimizes (Rahimi, Wang, Dong, Lou 2019), robust Sharpe-ratio portfolio selection maximizes a mean-to-worst-case-risk ratio, and generalized eigenvalue problems minimize Rayleigh quotients. Classical methods such as Dinkelbach's algorithm assume convex and concave ; many modern instances have neither.
Boţ, Dao and Li (arXiv:2003.04124, Math. Oper. Res. 2022) study the nonconvex nonsmooth case in which the numerator is a smooth convex part plus a lower semicontinuous part and the denominator is weakly convex on the constraint set. Their basic method, the extrapolated proximal subgradient (e-PSG) algorithm, converges subsequentially to lifted stationary points. When the denominator is a maximum of finitely many smooth functions, a lifted stationary point may be spurious: it only requires one element of the subdifferential of to balance the numerator. Section 6 of the paper proposes an enhanced algorithm, in the spirit of the enhanced DC algorithm of Pang, Razaviyayn, Alvarado 2017, whose cluster points satisfy the stronger condition for all such elements. This mission formalizes that result.
is a finite-dimensional real Hilbert space, is nonempty, closed and convex, and the problem is
Algorithm 2 starts from . At step it sets , picks a step size and extrapolation weights , , and forms and . For every it computes a proximal candidate
(up to constants), and keeps as the candidate minimizing the merit value .
Assume the sublevel set is bounded and . Then every cluster point of satisfies , ,
and, if is weakly convex on , is a strong lifted stationary point of (P).
For max-type denominators the result separates the enhanced algorithm from the basic one. A lifted stationary point only needs . The paper's Example 3.3 () has the lifted stationary point , which is not a local minimizer; the strong lifted stationary points of that example are exactly its minimizers. Lemma 3.4 of the paper identifies strong lifted stationarity with d-stationarity of on when and are weakly convex. This is the sharpest first-order notion used for DC-type programs.
The theorem is proved in the paper (pp. 22–24). No machine-checked version of it, of the e-PSG analysis, or of lifted stationarity exists on the platform. Formalizing it checks the step-size bookkeeping that the printed algorithm gets wrong (see below). It also produces reusable statements about weakly convex functions and the limiting subdifferential of .
The descent part follows the template of the basic e-PSG analysis, but the merit criterion couples the candidate selection with the extrapolation: the coefficient has to stay positive, and the cross term has to be split with the specific weight for the constants of (27) to close.
The limit step is the main obstacle. The algorithm works with , but the conclusion concerns at a limit point. One must show that every index active at was a candidate along the subsequence. One must also show that although is only lower semicontinuous. The naive approach, passing to the limit in the optimality condition of a single subproblem, gives one element of only, which is lifted stationarity again. The final step needs the limiting subdifferential of a finite max of functions to be the convex hull of the active gradients. The paper uses this fact without proof, and Mathlib does not provide it for .
EuclideanSpace ℝ (Fin N). Functions into are EReal-valued. is the published NonconvexSplitting.Shared.LimitingSubdiff, and properness is IsProperFn.Fin p with , so they run . is defined as Finset.sup' of the , never as an independent function. The standing assumptions of (P) are kept: is lower semicontinuous and positive on .ConvexOn of on . For extended-real it is convexity of the epigraph of .Filter.liminf τ atTop, which is well defined because . The -range is multiplied out to avoid dividing by .toReal value of never enters.The ℓ1-regularized least squares problem (the Lasso, or basis pursuit denoising) is the model problem of compressed sensing and sparse inverse problems: given a matrix , data and a weight , one seeks a vector that fits while having few nonzero entries. The standard first-order method for it is the iterative shrinkage thresholding algorithm (ISTA), a forward-backward splitting scheme whose backward step is componentwise soft thresholding. Each iteration costs two matrix–vector products, which is why ISTA and its variants are used on problems far too large for interior-point methods.
The classical complexity guarantee for ISTA is , the rate of the proximal gradient method on any convex composite problem (Beck–Teboulle 2009). ISTA itself goes back to Daubechies–Defrise–De Mol 2004, and its link with forward-backward splitting to Combettes–Wajs 2005. An asymptotic linear rate was known, with an explanation through partial smoothness (Liang–Fadili–Peyré), but there was no global, explicit, non-asymptotic bound. Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234v3, Math. Program. 2017) derive such a bound from two ingredients: an error bound for the Lasso objective on balls, with a constant written through a Hoffman constant, and their general theory turning a Kurdyka–Łojasiewicz (KL) inequality into complexity bounds for descent methods.
Write with the Euclidean norm , and . For a matrix , is its spectral norm, the operator norm from to with Euclidean norms. The objective is
with and . Put and . Then is convex with gradient , Lipschitz with constant .
Given stepsizes with and any , ISTA is
where is the minimizer of . More generally, in a real Hilbert space with proper, lower semicontinuous and convex and convex with -Lipschitz gradient, the forward-backward method takes to be a minimizer of .
A sequence is a subgradient descent sequence for a convex with constants if and, for every ,
With , has the KL property on a set with desingularizing function if for every such and every .
A number is a Hoffman constant for a pair of matrices if, for every right-hand side with and intersecting, for all .
Put and , and . Let be such that whenever . Then ISTA converges to some and
The result. The theorem replaces the sublinear guarantee of ISTA by a global linear rate with explicit constants depending only on , , , the stepsizes, and a Hoffman constant. It also bounds the distance of the iterates to the limit, not only the objective gap, and needs no uniqueness of the minimizer. Through , it shows that conditioning of the objective near its minimizers, rather than strong convexity, governs the complexity of the method. The general machinery behind it (Theorem 16 of the paper, a separate mission of this series) applies to any method producing subgradient descent sequences.
Formalizing it. The result is proved on paper, and no machine-checked proof of it or of its ingredients is known. A formalization would give a verified linear-rate certificate for a widely deployed algorithm. It would also yield reusable lemmas: the descent and relative-error properties of the forward-backward method in a Hilbert space, and quadratic growth for the Lasso on balls. Lemma 10 rests on an external result (Beck–Shtern, Lemma 2.5) that a complete development must also formalize.
The Lasso objective is not strongly convex when has a nontrivial kernel, and its minimizer need not be unique. The textbook argument for linear convergence of proximal gradient methods, which uses strong convexity, therefore does not apply. Quadratic growth is the substitute, but it holds only on bounded sets, with a constant degrading in the radius. The analysis must therefore show that the iterates stay in a fixed ball and keep track of how the growth constant enters the rate. Deriving the explicit requires recasting the problem as a quadratic program over a polyhedron with facets and invoking a Hoffman-type error bound for it.
Citations refer to the arXiv preprint arXiv:1510.08234v3 (20 July 2016), with its numbering and pages; the journal version is not used. is EuclideanSpace ℝ (Fin n) and matrices act through Matrix.toEuclideanLin. Spectral norms are operator norms of the associated continuous linear maps, never Mathlib's default entrywise matrix norm. The data vector, called in §3.2.1 of the paper and in §5.3, is throughout; is the constant of (H2).
Functions with values in are EReal-valued. The convex subdifferential, Γ₀, , the prox predicate and the class of desingularizing functions are reused from published platform definitions. The stepsize condition is written , so that (where ) is covered. is the infimum of , and is a real power.
In the goal, is any positive constant satisfying the error bound on the ball of radius ; it is not fixed to the value (10) and not existentially quantified. The constants are fixed formulas, never existentials. A statement with an unspecified constant, with chosen after the sequence, or with the stepsize hypothesis written as (unsatisfiable or vacuous at ) would trivialize the goal and is ruled out.
The subgradient-descent and KL notions duplicate, in the sub-namespace ErrBoundCplx.ISTA, those of the series' first mission, because draft items cannot import each other. Proofs of any milestone are welcome, in particular Proposition 13 and the KL consequence of Lemma 10, which are self-contained. A formalization of Hoffman's error bound and of Beck–Shtern's Lemma 2.5 is the main infrastructure Lemma 10 needs.
Many problems in signal processing, statistics and machine learning are of the form : a smooth data-fitting term , plus a possibly nonsmooth and nonconvex regularizer applied to a linear image of the variable. Examples are total-variation-type penalties with nonconvex potentials, -type sparsity terms, and constraints with nonconvex. The alternating direction method of multipliers (ADMM) treats and separately, which makes it the method of choice for this class. For convex problems its convergence theory is classical. For nonconvex problems it was long used as a heuristic, and the Kurdyka–Łojasiewicz (KŁ) framework of Attouch, Bolte, Redont, Soubeyran and Svaiter, and of Bolte, Sabach and Teboulle, is now the standard tool for proving that such methods converge.
Timeline. Li and Pong (SIAM J. Optim. 2015) proved global convergence of a proximal ADMM with for twice differentiable under a KŁ hypothesis. Hong, Luo and Razaviyayn (SIAM J. Optim. 2016) studied related nonconvex ADMM schemes under other assumptions. Boţ and Nguyen (arXiv:1801.01994v2, Math. Oper. Res. 45(2), 2020) extended this in three directions. Their scheme uses variable metrics , . It allows a relaxation parameter in the dual step. It covers both a proximal and a proximal-linearized -update. Under these conditions they proved that bounded iterates have finite length and converge to a KKT point whenever a regularized augmented Lagrangian has the KŁ property. This mission formalizes that theorem.
Let be proper and lower semicontinuous, let be differentiable with -Lipschitz gradient, and let be linear. The augmented Lagrangian with parameter is
Let and be symmetric positive semidefinite matrices, and write . Fix . From an arbitrary starting point , Algorithm 1 generates
Algorithm 2 is the same, except that in the -update is replaced by its linearization . Assumption 1 asks for four things:
With the constants and of §2.2 of the paper, the regularized augmented Lagrangian is
A KKT point of the problem is a triple with , and , where is the limiting subdifferential. A proper lower semicontinuous is a KŁ function if, near every point of , a concave desingularizing function satisfies .
Under Assumption 1, let be a bounded sequence generated by Algorithm 1 or Algorithm 2. If is a KŁ function, then
and for some KKT point .
The milestones follow the order in which the paper's proof uses them:
Theorem 6, the boundedness of the iterates under coercivity, is included as a supporting item that discharges the boundedness hypothesis.
The theorem gives global convergence of the whole sequence, not just subsequences, for a broad family of nonconvex splitting methods. The family includes full-splitting variants, in which makes the -update explicit. The KŁ hypothesis on holds, for example, whenever and are semi-algebraic. The finite length conclusion is also the starting point for the rates of Section 3 of the paper, which are the subject of the companion mission.
The paper result is proved; this mission formalizes the known proof. As far as the platform records go, no machine-checked proof of convergence of a nonconvex ADMM exists. The Li–Pong ADMM theorems on the platform are open statements about a different algorithm. A completed development would supply the following reusable pieces:
The obvious Lyapunov candidate, itself, does not decrease along the iterates: the dual step increases it by . That increase has to be paid for by primal progress, and this is possible only because surjectivity of lets the dual increment be controlled by -increments over two consecutive steps. This is where the specific constants , , and the coupling condition (15) come from. The KŁ argument must therefore be run on the lifted function in five variables, whose subgradient bound (Corollary 10) involves three past increments and two telescoping terms. The textbook one-step KŁ argument therefore does not apply directly, and the recursion has to be closed with the three-step summability Lemma 3. For the dual update is relaxed, and the estimates must handle in both regimes and .
Spaces are EuclideanSpace ℝ (Fin n), and products such as and the 5-fold domain of are nested WithLp 2 products. Their norm is the Euclidean product norm the paper uses, not the sup norm. The function and the functions , take values in EReal. The data are bundled in a structure Data, and the algorithm is a parameter Variant (prox for Algorithm 1, linearized for Algorithm 2), so every statement covers both algorithms. A run is a relation: any minimizer may be selected at each step, and existence of minimizers is not claimed. and are replaced by parameters with the inequalities the proofs use ( with , and ). The paper's statements are the instance , . The subdifferential is the published limiting subdifferential, and "KŁ function" is the published IsKLFunction. In that definition, is read as a bound for every subgradient, so . Corrections read past: the paper indexes although exists only for , and it writes "defined in Assumption 1" for and , which are defined on p. 10.
There are three ways to formalize the statement trivially, and all are excluded:
Contributions are welcome at every milestone. Lemma 3 and the subdifferential calculus behind Lemmas 8–9 are independent of the algorithm, and are good entry points.
Best subset selection asks for the linear model that fits a response with as few predictors as possible. It is a basic problem of statistics and a standard test case for mixed-integer optimization. The penalized form
is NP-hard in general. Exact mixed-integer methods (Bertsimas, King, Mazumder 2016) certify global optimality but scale to moderate only. Hazimeh and Mazumder (arXiv:1803.01454, Operations Research 2020) proposed a hierarchy of local minima for the -penalized problem, together with algorithms that reach each class. These are coordinate descent for coordinate-wise minima, and coordinate descent combined with small combinatorial swap searches for the finer swap inescapable minima. The software built on these algorithms, L0Learn, runs on problems with in the millions.
The companion mission (part I) proves that the coordinate descent stage converges. This mission proves the guarantee of the second stage: the local combinatorial search stops after finitely many rounds, and it stops at a partial swap inescapable minimum.
Data and objective. Let have columns of unit Euclidean norm, let , and let , . Problem (2) is
where is the number of nonzero entries. The paper names three cases: (L0), with ; (L0L1), with ; and (L0L2), with . , and keeps the entries of in and zeroes the others.
Classes of minima. A stationary solution has nonnegative lower directional derivative in every direction . A CW minimum is a point where each coordinate minimizes with the other coordinates held fixed. For a positive integer , a PSI() minimum is a stationary with support such that, for all and with ,
In words, dropping at most active coordinates, adding at most new ones and optimizing only over the added ones never lowers the objective.
Algorithm 1 (CDSS) is cyclic coordinate descent. Each step sets one coordinate to the minimizer given by the thresholding operator of (12). Every time a support has been visited times, the algorithm also performs a spacer step: one pass of coordinate descent on restricted to that support.
Algorithm 2 (CD-PSI()) alternates two steps. It runs Algorithm 1 from to obtain . It then searches the swap problem (14),
with , for a feasible with . If it finds one, it sets and continues; otherwise it terminates.
Assume the (L0), (L0L1) or (L0L2) setting. For (L0) and (L0L1), assume also that every columns of are linearly independent (Assumption 1) and, when , that the start satisfies the objective bound of Assumption 2. Then every run of CD-PSI() satisfies
No bound on is part of the goal, and the paper states none.
The result. Theorem 4 makes CD-PSI() an algorithm with a guarantee. It always stops, and its output satisfies an optimality condition that is strictly stronger than coordinate-wise optimality: the hierarchy (4) of the paper places PSI() minima inside CW minima, and for large they coincide with global minimizers. The same termination argument underlies the full-optimization variant (FSI minima) and the swap heuristics of L0Learn, which the paper treats "by the same argument".
Formalizing it. The theorem is proved on paper, in a short argument in Appendix A.8 that rests on the convergence of Algorithm 1 (Theorem 2, the companion mission). No part of it has been machine-checked. This mission produces checked definitions of PSI minima, of the swap problem and of the two-level algorithm; a formal proof of the finite termination; and the bridge lemmas between CW minima, stationarity and the restricted least-squares problem, which any formal treatment of -penalized regression needs.
The obvious argument is that each round lowers the objective, there are finitely many supports, so the algorithm stops. A strict decrease of alone gives no finiteness: a real-valued sequence can decrease forever. What makes the argument work is that the value of at an output of Algorithm 1 depends only on its support. That needs every output to be a CW minimum, which is Theorem 2, a nontrivial convergence theorem for a discontinuous objective. It also needs every CW minimum to minimize the convex function over its support, which uses the characterization (8) and convexity.
A second difficulty is bookkeeping. Algorithm 1 never stops ("while not converged"), so its output is a limit. Each call of Algorithm 1 inside Algorithm 2 must satisfy the hypotheses of Theorem 2, in particular Assumption 2 for the new starting point, and that holds only because the objective has decreased since .
Vectors are Fin p → ℝ, so indices are -based. All norms are explicit sums, never Lean's sup norm. is Real.sign, with . The lower directional derivative is EReal-valued. The theorems are stated for the three named problems, via the hypothesis . Assumptions 1–2 are required only when .
Algorithm 1 is a deterministic state machine with a cyclic pointer, a table and a pending-spacer flag, following the box on p. 11. A run of Algorithm 2 is a pair of sequences: is the limit of the CDSS iterates from , and is any improving feasible point of (14), required only while the run has not terminated. The predicate is not vacuous: on the instance , , , , , , a run exists and terminates at . "" in Definition 3 is read as " every value".
A statement that assumes the outputs of Algorithm 1 are CW minima, or that the run terminates, or that only finitely many supports are visited, would trivialize the goal. All three are conclusions of the mission, not hypotheses.
The development needs the CDSS model shared with the companion mission, convexity of the restricted least-squares objective and a finiteness argument over Finset (Fin p). The definitions of Problem (2), Algorithm 1 and the stationarity notions are reusable for any later mission on -penalized regression. Proofs of the milestones independently of the goal are welcome; Theorem 2 can also be imported once the companion mission proves it. Theorem and page numbers are those of arXiv:1803.01454v3.
Many problems in statistics and signal processing ask for an orthonormal frame that is both a good fit to the data and sparse or otherwise structured. Sparse principal component analysis, compressed modes in physics, unsupervised feature selection and sparse blind deconvolution all take the form
with smooth and convex but nonsmooth, typically an penalty. Before the work of Chen, Ma, So and Zhang, algorithms for this class fell into three groups: subgradient-oriented methods, which solve a quadratic program over sampled subgradients in every step; proximal point algorithms, whose subproblems are as hard as the original problem; and operator-splitting methods such as SOC and MADMM. The manifold proximal gradient method (ManPG) carries the Euclidean proximal gradient method over to the Stiefel manifold. The paper shows that ManPG keeps the global convergence and the iteration complexity that Riemannian gradient descent has for smooth objectives (Boumal, Absil and Cartis, 2019).
The feasible set is the Stiefel manifold
The ambient space carries the Frobenius inner product and norm . The tangent space at is . The orthogonal projection onto it is .
The standing assumptions on are imposed on all of :
A point is stationary (Definition 3.3) if
where is the convex subdifferential.
A retraction maps tangent vectors at back to , with . On the compact manifold every retraction satisfies, for some and all , (Fact 3.6),
ManPG (Algorithm 1) takes , and . In iteration it solves the convex subproblem
It then backtracks until , and sets .
A point is -stationary (Definition 5.4) if the solution of (4.3) at with has . The proof of Lemma 5.2 uses a bound on over and the constants
For every run of ManPG:
has and is -stationary.
Here is the optimal value of (1.1). The constant is the paper's, kept exactly.
Theorem 5.5 is the paper's main result. It certifies ManPG as a first-order method for nonsmooth problems on the Stiefel manifold with the same complexity as Riemannian gradient descent in the smooth case. When the bound reduces to the Boumal–Absil–Cartis rate (Remark 5.6). Later proximal methods on matrix manifolds build on this analysis. Lemmas 5.1–5.3 are the reusable steps: descent of the subproblem, sufficient decrease after retraction, and the stopping test as a stationarity certificate.
The result is proved in the paper; it is not formalized anywhere. No proof assistant library contains the convergence theory of a proximal method on a matrix manifold. The mission produces a machine-checked version of the full chain from the subproblem to the iteration bound. Along the way it builds infrastructure that Mathlib lacks: the Frobenius geometry of as a trace formula, the tangent space and projection of the Stiefel manifold, and optimality conditions for convex problems restricted to a subspace.
The bookkeeping inequalities (Lemma 5.1, (5.5), the decrease estimate, the telescoping) are short computations once the right facts are available. The difficulty lies elsewhere.
A natural first idea is to restate everything for the Riemannian gradient and reuse smooth Riemannian results. That route does not work: is nonsmooth, and the argument runs in the ambient space through the Euclidean subdifferential.
Matrix (Fin n) (Fin r) ℝ.trace (Aᵀ * B) and the norm is its square root. No Mathlib matrix norm instance is used.ProjLikeRetr.Stiefel.stiefel.gradf, tied to it by derivatives along every line.Nat.ceil.Two encodings would trivialize the theorem, and the mission excludes both.
Lemma 5.2 as printed fixes and asserts the decrease for the accepted iterate. What its proof establishes is three separate facts: decrease at every trial stepsize , termination of the line search, and along a run. The mission states these three facts.
Contributions are welcome at every level: proofs of the milestones, and general lemmas such as the descent lemma for functions on , the optimality condition of a strongly convex problem on a subspace, and properties of the Stiefel tangent projection. Theorem numbers and pages refer to arXiv:1811.00980v2, the version read for this mission.
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 edges has a cycle cover of length at most (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 , and the authors conjecture (Conjecture 7.4) that holds for all snarks. This mission formalizes the colourable bound and the chain of statements behind it.
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 a cycle is recorded by its edge set , with distinct and ; its length is . A 2-regular subgraph of is an edge set such that every vertex lies on none or exactly two edges of : 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 such that every vertex lies on an even number of edges of .
A cycle double cover of is a multiset of cycles such that every edge lies in exactly two of them. It is a -CDC if the cycles can be coloured with colours so that cycles sharing an edge get different colours. Each colour class is then an even subgraph, and following the paper the -CDC is written as a family of even subgraphs with every edge in exactly two of them, counted with multiplicity.
A cycle cover of is a set of cycles of such that every edge lies in at least one of them, and its length is . Throughout, denotes the number of edges of .
For every colourable cubic graph with edges there is a cycle cover with
Equivalently, the shortest cycle cover of has length at most .
The bound is far below the Alon–Tarsi bound 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.
The arithmetic of the goal is immediate once the pieces exist: a 3-edge-colouring of a cubic graph on vertices consists of three perfect matchings, two of which form a 2-factor with edges, and . 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 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 need not be one of its classes.
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 -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 " is stated as "some cycle cover has length at most "; the two agree because a finite graph has finitely many cycle covers. Bounds are kept in without subtraction or division: the goal is , and Lemma 7.2 is . Lemma 7.2 is stated for a CDC given as a family of even subgraphs, the form in which the paper applies it (with 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 is a cover of length . 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, -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.
Norms are the most common nonsmooth terms in convex optimization models. The 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 for some point and step , 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.
Work in with the Euclidean inner product and Euclidean norm .
A function is closed proper convex if its epigraph is a nonempty closed convex set. For such and , the proximal operator is
which has a unique minimizer for every . The convex conjugate is . For a set , the indicator function is on and off , and the Euclidean projection onto a nonempty closed convex is .
Let be a general norm on , possibly different from . 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, is dualNorm N z, is dualBall N, is indicator C, and is normFun N.
For every general norm on , every and every ,
Stated as: if and only if , for all .
MoreauProx.Decomposition.moreau_decomposition.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 (whose dual ball is the box), block soft thresholding for (whose dual ball is the Euclidean ball), and the prox via projection onto the 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.
The derivation in the monograph is two lines, but each line hides a step. Computing for a norm requires the inequality and, for , a direction along which 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 and , in extended-real arithmetic where 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 and squared versus unsquared distances.
A tempting shortcut is to work only with the Euclidean norm, where is the Euclidean unit ball; that proves a special case, not the goal.
EuclideanSpace ℝ (Fin n) for arbitrary , including . 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).EReal. The dual norm is computed in EReal as the supremum of the printed set, so it has no junk value. and are products with the positive reals , , and is a hypothesis everywhere (p. 124).IsProx g z x ( minimizes ) and "" is IsProj C z x. With , Moreau's objective is 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.conj, IsProx and IsProj come from the published Moreau 1965 series definitions MoreauProx.Decomposition.ConvexDuality and MoreauProx.Decomposition.Cones.Useful contributions include lemmas on conjugates of positively homogeneous functions, on the behaviour of IsProx under scaling, and the identity in the predicate form; all are reusable beyond this mission.
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.
There are nests and products in each nest. Product of nest has a preference weight and a revenue (any real number); is the preference weight of buying nothing, and is the dissimilarity parameter of nest . For an assortment of nest put
with for the empty assortment . The expected revenue of is
Under space constraints product of nest uses units of space and nest has capacity , with for every product, so the feasible assortments are . Problem (1) is .
For a scalar , the knapsack problem (10) of nest maximizes over with . Its linear programming relaxation allows . The paper partitions into finitely many intervals , , on each of which one vector solves the relaxation. For a fractional vector it writes and .
The linear program (13) in the variables is
If is an optimal solution of (13), then
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 . The bound is a linear program with variables and one constraint per interval solution, so it can be solved for instances where 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 (only their feasibility and their optimality for every matter), the extension of and to fractional vectors, and the concavity of . 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.
The constraints of (13) are indexed by finitely many fractional vectors, while 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 directly. The link between the two has to be made nest by nest, through the knapsack relaxations at values of that depend on the unknown optimum, and the fractional vectors are compared with integral assortments through the nonlinear map .
The formalization references the published nested logit model NestedLogitVariants.General.Model (instance, , , , ) and NestedLogitVariants.General.Relaxation (the unit box and the term of the constraints of (13)). The conventions are:
Fin n, indexed from ; assortments are finite sets of products and is the empty set;Real.rpow, and , which gives as in the paper and makes the constraint term at equal to ;The statement is not to be trivialized: setting , taking to be the whole box (not a finite set and not LP (13)), assuming , or proving the bound for one particular feasible point are all excluded.
A complete development needs the concavity (tangent-line) inequality of at a positive point and elementary facts about fractional knapsack relaxations; both are reusable. Proofs of the milestones and of the goal are welcome.
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.
Let be a positive integer and let the unit simplex be
For a vector , let be the number of nonzero coordinates. The objective is the squared Euclidean norm . Its minimum on the full simplex is , reached at the uniform point. The paper compares that optimum with the best value permitted by a bound on . The dimension and sparsity budget are separate: the goal assumes , so at least one coordinate must be zero at every eligible point.
The duality gap at a feasible 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 . 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.
For , Lemma 3 asserts an attained minimum:
The associated primal-error statement says that a point with exactly nonzero coordinates has , where is an optimizer on the full simplex. The minimum and the primal-error reading are both included as draft theorems.
For every natural number , Lemma 4 states the mission goal:
The threshold is essential to this exact value. If all coordinates may be active, the uniform optimizer has zero gap. The case 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- 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 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.
The source's convergence analysis gives error guarantees that decrease with the number of iterations, while its simplex example shows that using only atoms leaves primal error at least and, for , gap at least . 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.
Bounding the quadratic objective alone does not establish the duality-gap statement. The gap also involves the best linear comparison point 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 as the objective: that norm is the supremum norm, whereas the paper uses the Euclidean squared norm.
The paper's displayed curvature value is included as a companion statement. It uses the Euclidean diameter of the simplex, which is for . The one-dimensional simplex is a single point, so extending that equality to would be false. The formalized companion makes the dimension condition explicit.
Vectors are functions . The domain is Mathlib's ; 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 , which implies 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 because the printed quotient has no value at zero. The companion assumes , 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.
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.
Let be a finite set of nests and a finite set of products available in each nest. An assortment is the set offered in nest . Product in nest has preference weight and revenue . The empty assortment is allowed. The main model has no within-nest no-purchase option, so its total offered weight is . The conditional revenue in nest is , with under the paper's convention.
The weight of no purchase outside the nests is . Each nest has a dissimilarity parameter . Its attraction weight is . The expected revenue of a combined assortment is
For each nest, is a finite nonempty collection of candidate assortments. The paper obtains these from a feasible set , which may impose a cardinality or space constraint; Theorem 2 compares only combinations drawn from the supplied candidates. Equation (2) defines a real scalar through the maximum, over separately, of . Problem (3) selects a maximizing candidate in each nest at that scalar. Linear program (4) has decision variables , minimizes , and imposes and for every and every .
The goal is the exact candidate-selection claim of Theorem 2. If minimizes among all feasible pairs of program (4), and every solves problem (3) at , 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.
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 variables and constraints when the candidates are indexed by .
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, , , , 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.
Optimizing a candidate independently in every nest at an arbitrary value of 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 convention.
Nests are represented by any finite type, and products by Fin n, indexed rather than the paper's . A Boolean offer vector is represented by Finset (Fin n); is the empty finset. Each is a finite set of such assortments. There is no single-nest or 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 to a set.
The source's main model is selected from the imported general instance by setting . In the paper's later extension, ; this is different from the imported unmodified when , so the extension is outside this mission. Positive and product weights are stated explicitly to keep the probability denominator positive and to match the model's preference interpretation. Revenues remain arbitrary real numbers: neither an order nor nonnegativity is assumed. The dissimilarities satisfy the paper's range. The paper states candidate feasibility ; this mission's claim holds for arbitrary candidate collections because no step compares against . The definitions of revenue and LP feasibility are imported, so useful contributions include proofs of the balance characterization, the root result, Lemma 1, and the final LP statement.
A retailer that sells through a choice model decides two things at once: which products to put on the shelf and at what price. Under the nested logit model of discrete choice, products are grouped into nests (brands, categories, store sections); a customer first picks a nest, or leaves without buying, and then picks a product inside the nest. The price of a product changes its attractiveness, and the attractiveness of every product changes the purchase probabilities of all the others, so assortment and price interact.
Gallego and Topaloglu (Management Science, 2014) study assortment optimization under the nested logit model with constraints on what may be offered in each nest. Their §6 treats joint assortment and pricing when each product can be sold at one of finitely many price levels. Earlier work on nested logit pricing, by Li and Huh (2011) and Gallego and Wang (2011), assumes that a product priced at has preference weight . With a finite menu of price levels, no parametric link between price and preference weight is required, and the prices can be restricted to a range or a grid (for example $49.99, $59.99, …), as retail practice often demands.
There are nests . In each nest there are products , and each product can be offered at one of price levels . Offering product at level in nest earns the price and gives the product the preference weight . The relation between and is arbitrary.
Each pair (product, price level) is a virtual product. Nest has virtual products ; is the set of the virtual products of product , and the sets are disjoint. Virtual product at level has revenue and preference weight . An assortment of nest is a set , and the feasible assortments are
so each product is offered at no more than one price, or not at all.
For an assortment write and , with . For a number , problem (7) of the paper is
Its objective equals with ; under this is problem (12) of the paper.
For every nest there is a collection , fixed independently of , with
such that for every some is an optimal solution of problem (7). The page states ; the explicit bound is the count of intervals left by the intersection points of the lines , , with .
The paper's Theorem 4 shows that a collection containing an optimal solution of (7) for every yields an optimal solution of the full nested logit problem, and its Theorem 2 that the best combination of candidates solves a linear program with variables and constraints. With the goal above, the joint assortment and pricing problem is solved exactly by a linear program of polynomial size, constraints, for arbitrary price–weight relations. This is one of the paper's three headline results.
The result is proved in the paper in prose, without a numbered statement. No machine-checked proof of it is known. The mission fixes the constant hidden in , states the feasible set exactly, and isolates the two steps of the argument as separate statements.
The naive candidate set is all of , which has members; the content of the goal is the polynomial bound with the collection fixed before . The argument must handle ties between coefficients, lines that coincide or never cross, intersection points at negative , and the boundary points between intervals, where several assortments are optimal at once. The count must be made per product: a count over all pairs of virtual products gives and misses the stated bound.
ι; virtual products are Fin n and products Fin p, both 0-based. is the fiber of a map prod : Fin n → Fin p; the hypothesis that every fiber has exactly elements is IsVirtualProductMap prod b. The price level of a virtual product is left implicit.NestedLogitVariants.LP.Instance fields r i j and v i j; there is no parametric price–weight relation and no ordering of prices.Finset (Fin n); the empty assortment is allowed and has objective .0 ≤ u).A complete development needs the reduction of (7) to the linear objective (identity (8)), the per-product optimality of problem (12), and a counting argument for the intersection points of finitely many lines on . The last one is reusable beyond this mission: the paper's cardinality-constrained result uses the same kind of argument. Proofs of the milestones, and lemmas such as (8) for the published V and R, are welcome.
The rank of a matrix does not depend on the field in which its entries are read: a rational matrix has the same rank over , and , because rank is computed by Gaussian elimination, which never leaves the field of the entries. For 3-tensors, arrays with three indices, this fails. Tensor rank governs the complexity of bilinear maps (the exponent of matrix multiplication is a statement about the rank of one tensor), the uniqueness of the CANDECOMP/PARAFAC decompositions used in psychometrics and signal processing, and the identifiability of latent-variable models. In each application the field matters: algorithms are run over or , while complexity results are often proved over or finite fields.
Håstad (1990) proved that deciding is NP-complete over finite fields and NP-hard over . De Silva and Lim (2008) gave real tensors whose rank over is strictly smaller than their rank over . Hillar and Lim (2013, Theorem 1.14) showed that the same phenomenon already occurs between and , for a tensor with integer entries, so that Håstad's result over does not by itself say anything about rank over .
Let be a field. The outer product of , , is the tensor with entries . The rank of over is
If has entries in a subfield , both and are defined, and .
The paper's example uses , and
A decomposition with , is equivalent to the eight cubic equations (30) in the twelve unknowns , one for each entry of .
In Lean, outer x y z and rankOver E A implement the two definitions, tensorA is , and System30 is (30).
The theorem shows that tensor rank, unlike matrix rank, is not invariant under field extension even between and , and even for the smallest nontrivial format . Its consequence for complexity is that a hardness result for rank over cannot be transferred to by reading the same instance in a larger field; the paper accordingly re-examines Håstad's construction to obtain hardness over and (Theorem 8.2), which is outside this mission.
The result is proved in the paper, with the decisive algebraic step delegated to a computer-algebra computation (Appendix). A machine-checked proof replaces that computation by a certificate verified in Lean, and it settles a printed error: one of the two consequences of (30) in the proof of Lemma 8.1 is printed with the wrong sign (see Formalization scope). No formalization of array tensor rank over a field, or of its field dependence, is known to exist in Mathlib or on this platform.
The upper bound is an identity among explicit arrays. The lower bound is the substance: one must show that the cubic system (30), which has real solutions, has no rational one. Since (30) is solvable over , no argument by signs, inequalities or real geometry can work; the obstruction is arithmetic, coming from the irrationality of . The step that fails in a naive attempt is the elimination: eliminating ten of the twelve unknowns from eight cubic equations by hand is impractical. A second, smaller difficulty is the reduction from "" to two terms of the special form (29), which requires absorbing the scalars and padding a decomposition with fewer than two terms.
Fin l → Fin m → Fin n → E, with 0-based indices: the paper's is A (i-1) (j-1) (k-1). Vectors are Fin n → E.rankOver E A is the sInf over of the lengths of decompositions . The set is nonempty (one term per entry), so this is the paper's minimum. Zero summands are allowed; this gives the same minimum as the paper's sum of nonzero rank-1 tensors.rankOver ℝ of its entrywise cast to ; is rankOver ℚ, whose witnesses are rational. A formalization in which both ranks range over real witnesses would make the theorem false.Needed infrastructure: finite sums of arrays, Real.sqrt and irrational_sqrt_two, and an ideal-membership certificate for milestone 3. The array rank rankOver is reusable for any statement about tensor rank over a field. The platform's mme_tensor_rank (restriction-based rank of a TensorObj over a single field, from the matrix-multiplication exponent series) is a different object and is not reused. Proofs of any milestone, and alternative certificates for Lemma 8.1, are welcome.
A snark is an uncolourable, cyclically 4-edge-connected cubic graph of girth at least 5: a cubic graph whose edges cannot be properly coloured with three colours, and which is not reducible to a smaller such graph by an elementary operation. Snarks are the critical cases for several of the central conjectures of graph theory, among them the cycle double cover conjecture, Tutte's 5-flow conjecture and the Berge–Fulkerson conjecture: a minimal counterexample to any of them, if one exists, is a snark. Lists of all small snarks are therefore used to test such conjectures by computer.
Brinkmann, Goedgebeur, Hägglund and Markström (arXiv:1206.6690v3, 2013) generated all snarks on up to 36 vertices. Testing 3-edge-colourability is NP-complete, and only a vanishing fraction of cubic graphs are snarks (0.00044% of the cubic graphs of girth at least 5 on 28 vertices, p. 4), so the generation algorithm needs cheap criteria that recognise, before a graph is built, that it will be colourable and can be skipped. Section 3.1 of the paper supplies such a criterion for the last construction step, and this mission formalizes it.
All graphs are finite and simple. A graph is cubic if every vertex has degree 3. A 3-colouring of a graph is a map that gives different colours to any two distinct edges sharing an end-vertex; is colourable if it has one, i.e. its chromatic index satisfies (p. 2, Isaacs' terminology).
A 2-factor of is a spanning 2-regular subgraph (p. 4); each connected component of is a cycle. is an even 2-factor if all its cycles have even length (p. 5). For a 3-colouring and colours , write for the spanning subgraph whose edges are those coloured or .
The edge insertion operation (Figure 1(d), p. 5) takes two distinct edges and of , which may share an end-vertex, subdivides by a new vertex and by a new vertex , and adds the edge . The resulting graph has vertex set and edge set
If is cubic, so is . In the generation algorithm every graph of girth at least 4 is produced from a graph with two fewer vertices by this operation.
Let be a cubic graph with a 3-colouring , let be colours, and let , be distinct edges of lying on the same cycle of . Then
Theorem 3.4 (p. 6, stated as folklore without proof). If is a colourable cubic graph and the inserted edge lies on a 4-cycle of , then is colourable.
The result. Theorem 3.3 is the look-ahead of the snark generator: one 3-colouring of a graph on vertices excludes, at once, every pair of edges lying on a common cycle of one of its three bicoloured 2-factors. For 28 vertices the first colouring alone discards on average 85% of the candidate edge pairs (p. 6), and the overall ratio of weak snarks among generated graphs on the last level improves by a factor of 85 (p. 4). The enumeration of all snarks up to 36 vertices, on which the paper's counterexamples and statistics rest, depends on this pruning being sound: a wrong pruning rule would silently delete snarks from the lists. Theorem 3.4 is a second pruning rule of the same kind.
Formalizing it. The results are proved (Lemma 3.1 is classical; the paper gives the argument for Lemma 3.2 in one sentence and for Theorem 3.3 by combination). None of them, and no statement about 3-edge-colourings of cubic graphs and their 2-factors, is formalized on the platform. The mission produces a machine-checked soundness proof of the pruning criterion and, along the way, a reusable development of the equivalence between 3-edge-colourings and even 2-factors in Lean's SimpleGraph library. Theorem 3.4 has no proof in the paper.
The combinatorial content is short; the difficulty lies in graph-theoretic infrastructure that Mathlib does not have. Lemma 3.1 relates a global object (a proper colouring of all edges) to the cycle structure of a spanning 2-regular subgraph, and either direction needs the description of a finite 2-regular graph as a disjoint union of cycles together with parity information along each cycle. Mathlib has walks, cycles and connected components, but no decomposition of a 2-regular graph into cycles and no notion of the length of a component as a cycle.
Lemma 3.2 and Theorem 3.3 change the vertex type: lives on , so 2-factors, connected components and cycle lengths must be transported from to , and the case where and share an end-vertex (allowed by Figure 1(d)) has to be handled alongside the generic one. A first idea, to extend a given 3-colouring of directly to , does not work in general: the colours forced on the edges at and by the old colours of and can conflict, and the hypothesis "same cycle" is what has to be used to avoid the conflict.
Vertices form a type V with [Fintype V] [DecidableEq V]; graphs are SimpleGraph V with decidable adjacency, and "cubic" is Mathlib's G.IsRegularOfDegree 3. Colourability is G.lineGraph.Colorable 3 (an edge colouring, not a vertex colouring), and a 3-colouring is G.lineGraph.Coloring (Fin 3). A 2-factor is a graph F on the same vertex type with F ≤ G and F.IsRegularOfDegree 2; it is even if every connected component has an even number of vertices (Nat.card). The edge insertion operation produces a graph on V ⊕ Fin 2, with Sum.inr 0 subdividing and Sum.inr 1 subdividing ; edges are unordered pairs Sym2 V. "On the same cycle" is encoded as membership of both edges in the 2-factor plus reachability of their end-vertices inside the 2-factor. Oddness is not defined as a number; Lemma 3.1 is stated in its second form.
Dropping "on the same cycle" would make Theorem 3.3 and Lemma 3.2 false (inserting edges between different cycles of a bicoloured 2-factor is exactly how snarks are produced), and both statements require the two edges to be distinct; a formalization without either hypothesis is ruled out. Every statement assumes cubicity, without which Lemma 3.1 fails.
Out of scope: the algorithmic content of §3 (isomorphism rejection, the look-ahead implementation, recolouring along non-hamiltonian cycles, the 85% / 11% / 3.4% statistics), the generation counts, and every exhaustive-search claim of the paper. The remaining results of the paper are covered by three sibling missions of this series.
Reusable beyond this mission: the 2-factor and even-2-factor definitions, the two-colour 2-factor of an edge colouring, and Lemma 3.1 itself. Contributions welcome: the cycle decomposition of finite 2-regular graphs, alternating colourings of even cycles, and a proof of Theorem 3.4.
Quasi-Newton methods replace the Hessian of an objective by a matrix that is updated from observed pairs of steps and gradient changes. The secant equation asks the new matrix to map the observed steps to the observed changes . The best-known update is BFGS, which for simultaneous pairs reads
Schnabel (Quasi-Newton methods using multiple secant equations, technical report, University of Colorado at Boulder, 1983, reference [25] of the paper) studied such multiple-secant updates; one of his results is that a positive definite with exists exactly when .
Dahl and Andersen (Math. Program. 194:341–370, 2022) use multiple-secant BFGS updates to build primal-dual scaling matrices for an interior-point algorithm on the nonsymmetric exponential cone, following Tunçel (Found. Comput. Math. 1:229–254, 2001) and Myklebust and Tunçel (arXiv:1411.2129). In their setting , and they need the update in factored, low-rank form. Their Theorem 2 supplies it: the term , and its counterpart for the inverse update, are computed by rank-one steps. These steps resemble single-secant quasi-Newton updates, and no inverse is formed. This mission formalizes Theorem 2 and the steps of its proof.
Let and . Write for the -th unit vector of and for the inner product of , so that . The hypothesis of the theorem is
meaning that the matrix is symmetric and positive definite.
For the recursions (25)–(26) are
Both updates of step use the previous pair . Collect the vectors into and .
The proof uses two more objects. The first is the matrix
The second is , the principal submatrix formed by the last rows and columns of . In Lean these are ExpConeIPM.Secant.Ys, Ss, d, V, U, L and Ψ, all in one definition item.
The first identity of the goal follows from milestones 4 and 5. The paper says the second "follows similarly". The analogous identity is not displayed in the paper, so it is not a milestone.
The result. Theorem 2 expresses the multiple-secant part of the BFGS update (23), and of its inverse, as a sum of rank-one terms and . Each term comes from a recursion that touches one column at a time. On pp. 359–360 Dahl and Andersen apply it twice with . This gives the BFGS scaling of their exponential-cone algorithm as an explicit rank-3 update of , which is how the algorithm implemented in MOSEK computes its scaling matrices (§6, p. 361 of the paper). The argument is a Cholesky factorization of carried out implicitly on the factors and .
Formalizing it. The theorem is proved in the paper, in under a page. Its proof leaves two steps implicit. The first is that the symmetry of every , which (27) and the step to use, propagates from . The second is the second identity, which the paper does not prove. A machine-checked proof records both. To our knowledge no proof assistant has a formal treatment of multiple-secant updates. The recursion also gives a reusable statement: a column-by-column Schur-complement process on a product produces its Cholesky factor.
The obvious route expands directly and compares it with . This leads nowhere, because depends on all earlier steps through and . The step that carries the proof is an invariant over the recursion. The trailing blocks of must stay symmetric positive definite, and the leading columns of and must stay zero. Both must be maintained together through a pair of coupled updates, in which is updated with the old . A second difficulty is bookkeeping: the paper's 1-based columns, the step count , and the trailing block of size shift relative to each other.
The hypothesis needs care. If is only assumed to satisfy for , without symmetry, the identities are false in general. A instance whose symmetric part is positive definite, with a small antisymmetric part, violates the first identity by in the largest entry.
Everything is real matrix algebra over Matrix (Fin n) (Fin p) ℝ, with arbitrary (including , where both sides are zero). The formalization commits to the following conventions.
Matrix.PosDef, which includes symmetry. The inverse is Matrix.inv. It is a genuine inverse under this hypothesis.j : Fin p is the paper's . Ys Y₀ S₀ k and Ss Y₀ S₀ k are and after steps, and they are left unchanged after step . d Y₀ S₀ j is .Real.sqrt. The division by it is multiplication by an inverse. Both return junk values on non-positive arguments, which never occur under the hypothesis; milestone 2 states this.No repair of the printed statements was needed. On p. 359 two misprints are not copied: for , and for . The definition of uses .
A complete development needs rank-one updates of products, Schur complements of a positive definite matrix in its leading entry, and inverses of for an invertible . Schnabel's existence theorem (Theorem 1 of the paper) and the applications on pp. 359–360 are outside the mission. A general lemma on Schur-complement recursions producing Cholesky factors would be reusable on its own. Contributions on the U-side identity are welcome.
Nonnegative matrix factorization (NMF) approximates a data matrix by a product of two nonnegative factors. Adding a cap on the number of nonzero entries of each factor gives sparse NMF, used in signal separation, text mining and image analysis because sparse nonnegative factors are easier to interpret. Bolte, Sabach and Teboulle (Math. Program. 146 (2014)) introduced the algorithm PALM (proximal alternating linearized minimization) for problems of the form with nonconvex, nonsmooth and , and proved that its bounded runs converge to critical points when the objective has the Kurdyka–Łojasiewicz property. Sparse NMF is the paper's main application (§4).
PALM is only implementable when the proximal map of each nonsmooth term can be computed. For sparse NMF the nonsmooth term is the indicator of the nonconvex set of nonnegative matrices with at most nonzero entries. Proposition 4.1 of the paper computes that proximal map in closed form. This mission formalizes Proposition 4.1 and the steps of its proof. The convergence theory of PALM is a separate mission of the same series.
Matrices are real arrays . The squared Frobenius norm is . The sparsity count is the number of nonzero entries of , and means for every .
For a set , the indicator is on and off . For a natural number , set
the function that is on nonnegative matrices with at most nonzero entries and elsewhere.
For and , the proximal map (2.2) of the paper is the set
Throughout, is the set of all points of where attains its smallest value on .
The hard-thresholding operator of Definition 4.1 is
which is multi-valued when the largest entries of in absolute value are not uniquely determined. The projection onto the nonnegative orthant is , componentwise.
In the proof, is fixed and , , with partial squared norms .
For every and every ,
Both equalities are equalities of sets, and both are part of the goal.
The result. Proposition 4.1 says that the proximal step for the nonnegative sparsity constraint is computed by clipping the negative entries of to zero and then hard-thresholding: keeping entries of largest magnitude and zeroing the rest. The paper remarks that this costs operations. It is what turns PALM into the explicit algorithm PALM-Sparse NMF, and the same formula applies to any method that needs a projection onto nonnegative sparse matrices (projected gradient methods, iterative hard thresholding with sign constraints).
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked proof exists. The platform has a projection-onto-sparse-vectors statement without nonnegativity and stated as a single inclusion, which is a different theorem. The mission produces a set-level statement that handles ties, the degenerate cases and , and the interaction of the sign and the sparsity constraints, all of which the informal proof passes over quickly.
The obvious argument is: "project onto the nonnegative orthant, then onto the sparse matrices". Composing two projections onto nonconvex sets is not in general the projection onto their intersection, so this argument is not valid as it stands; the equality holds here because of the specific coordinate structure, and the proof must show it. The second obstacle is that everything is set-valued: when several entries of tie for the -th largest magnitude, has several elements, and the equality must account for every one of them, in both directions. The step "(4.1) = (4.2)" and the removal of are dismissed in the paper as "a simple contradiction argument" and "arguing in a similar way"; each needs an explicit modification of a feasible point that preserves sparsity and does not increase the objective.
Matrices are Matrix (Fin m) (Fin n) ℝ, with 0-based indices (harmless relabelling of ). is the Frobenius inner product of the published definition CaiCandesShen.ProximalLimit.Basic. The indicators and take values in EReal, with ; membership in is the inequality in EReal for every . The proximal map carries the weight of (2.2), not . is defined by the componentwise formula. No restriction is placed on .
Every operator in the statement is a set of minimizers. A formalization that selects one element (for instance "keep the largest entries with a fixed tie-break") proves only one inclusion of a weaker statement and does not count.
The development needs only finite sums and the argmin-set definition shared by all items; no further library is required. Lemmas about hard thresholding on matrices (the description of by largest entries, nonnegativity of of a nonnegative matrix) are reusable well beyond this mission, and contributions of such lemmas are welcome.
Theorem numbers and page numbers refer to the author version of the paper (36 pages, printed page = PDF page), not to the Springer typesetting.
In two-echelon distribution goods travel from a central depot to intermediate facilities, called satellites, on large first-level vehicles, and from the satellites to customers on smaller second-level vehicles. City logistics schemes that keep heavy trucks out of urban centres are the standard example. The two-echelon capacitated vehicle routing problem (2E-CVRP) asks for the cheapest set of routes on both levels that serves every customer while respecting vehicle, fleet and satellite capacities.
Exact methods for problems of this kind are branch-and-bound or enumeration schemes whose speed depends on the quality of the lower bounds they use. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) built their exact algorithm on a Lagrangean-type relaxation of a set-partitioning formulation , rather than on the LP relaxation of that formulation. Their Theorem 2 is the justification for that design choice: the best bound can deliver is never weaker than , and can be strictly stronger. This mission formalizes that comparison.
An instance has a depot , satellites and customers , a symmetric travel cost (in which the fixed vehicle costs have already been folded into the depot–satellite and satellite–customer entries), positive integer demands , capacities for first- and second-level vehicles, a bound on first-level vehicles, second-level vehicles at satellite , a global bound on second-level vehicles, a capacity and a unit handling cost for each satellite.
A first-level route leaves the depot, visits a set of satellites and returns; its cost is the cost of that closed walk. A second-level route leaves satellite , visits a set of customers and returns; its load is , counts its visits to customer , and its cost is its closed-walk cost plus .
Formulation uses binaries (route of satellite is used), binaries , and nonnegative integers (quantity route delivers to satellite ). It minimizes subject to: each customer is covered exactly once (2); at most routes at satellite (3) and overall (4); the load delivered from satellite is at most (5); at most first-level routes (6); what first-level routes bring to satellite equals what its second-level routes carry (7); and (8).
The LP relaxation replaces the integrality of by , . Its value is , equal to when is infeasible.
The relaxation relaxes (2)–(4) with penalties , and , and replaces the second-level routes by marginal routing costs that must satisfy, for every route ,
Its variables are binaries (customer is supplied from satellite ), and ; it minimizes
subject to single assignment of each customer, flow balance , satellite capacity , and (6), (8). A choice with and (12) is admissible.
Formally: (1) for every instance and route families whose is feasible, some admissible satisfies ; (2) some instance, route families and admissible choice give .
Theorem 2 places the relaxation in the hierarchy of bounds for the 2E-CVRP. The remark on explains its weakness: in the LP relaxation each first-level route is paid for only in proportion to the load it carries, so degrades as first-level routing costs grow. keeps binary and therefore pays the full cost of every first-level route used, while the second-level routing is priced through . The theorem guarantees that optimizing over penalties never loses against the LP bound, which is what makes the bounds LD1 and the further relaxation of the paper worth computing.
The paper's proof is in its electronic companion and is not reproduced in the article. A formal proof makes the comparison checkable, and fixes the exact conditions under which it holds: the remark on needs positive first-level route costs, and the "max" in Theorem 2 is attained only when is feasible. Neither part is formalized elsewhere. Linear programming strong duality is available on the platform as LinearOptimization.lp_strong_duality (Bertsimas and Tsitsiklis, Theorem 4.4, Proved); a related but different statement is LinearOptimization.lagrangean_dual_eq_lp_over_hull (Theorem 11.4 there), which concerns the Lagrangean dual of a generic integer program rather than .
is not the Lagrangean dual of in the textbook sense: it changes the variables (customer-to-satellite assignments instead of routes ), keeps the assignment constraints, and couples the multipliers through the inequalities (12). So the general fact that a Lagrangean dual is at least the LP bound does not apply directly; one must construct, from the data of , an admissible that is compatible with the flow-balance and capacity constraints of . For the strict clause, the instance must satisfy every structural requirement of the model (positive demands, , route loads at most , ), and must be feasible, so that the gap is a genuine gap between finite bounds.
Satellites and customers are Fin ns and Fin nc (0-based). The travel cost is an arbitrary symmetric real matrix; the triangle inequality is not assumed. Demands are positive integers. Route families , are arbitrary finite families of nonempty elementary routes (repetitions allowed), with costs computed from along the closed walk, so the statements cover the paper's families of all routes as a special case. Binary variables are Bool, integer quantities ℕ, variables real. Optimal values are infima over the feasible set in EReal, for an infeasible problem; there is no junk value .
Part 1 of the goal assumes feasible: when is infeasible the printed relation would read "", which is not attained by any single choice of penalties. Part 2 requires , which rules out the trivial witness of an instance with infeasible; admissibility includes , without which the supremum is for trivial reasons.
The definitions (instance, route systems, , , (12), ) are shared in shape with the two companion missions of this series and are intended for consolidation. Proofs of the bound will need finite-dimensional LP duality; contributions that connect to the platform's general-form LP and its strong duality theorem are welcome.