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?
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.Distributionally robust optimization (DRO) replaces the expected loss of a linear decision rule by its worst case over all data laws within transport distance of the baseline . When is an empirical distribution this covers regularized regression and classification (Blanchet, Kang, Murthy 2019; Esfahani, Kuhn 2018). The optimal value is one number; a practitioner also wants to know which distribution realizes it, the adversary's best response. It shows which data points the robust model guards against, it gives stress-test scenarios, and its structure is what the paper's comparative statics (Theorem 7) and iterative schemes build on.
J. Blanchet, K. Murthy and F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes (arXiv:1810.02403v3; Math. Oper. Res. 47(2), 2022), answer this for a state-dependent Mahalanobis cost. Theorem 6 of that paper describes the worst-case distribution through the solution of the one-dimensional dual problem. This mission formalizes Theorem 6.
The data take values in with law , a Borel probability measure. The decision ranges over a convex set (a standing assumption of the paper). Moving mass from to costs
where is positive definite. Assumption 1 asks that be lower semicontinuous and that for -almost every , with . The optimal transport cost is the least value of over couplings of and . For the worst-case objective is
Assumption 2 asks that the loss be convex, that the growth exponent be finite, and that .
The dual side is built from
the robust loss , the dual objective and the maximizer set . By the paper's Theorem 1, (6) equals , and a minimizer , the dual optimizer, exists. The threshold is ; below it .
Let and . Let be measurable selections with the largest and smallest square, , , and let be independent of with . Then
and the law of attains the supremum in (6).
Theorem 6(a): unless is constant. Theorem 6(b): . Theorem 6(d), as the paper's example: for , , and , and no distribution attains the value . Theorem 6(e), with Lemma 8: if and , then is a singleton almost surely and the law of is the unique worst case.
The result reduces a search over all probability measures to a scalar problem per data point. Each point is pushed along the single direction , by an amount read off the maximizers of , and the budget is always spent completely. When the maximizer is not unique, randomization between two extreme maximizers is needed and suffices. Part (d) shows that the threshold condition cannot be removed, and part (e) gives a deterministic transport map (a Monge solution) under smoothness. Theorem 7 of the paper, the monotone growth of worst-case displacements in , is a statement about the random variable produced here.
None of these statements has been machine-checked before. The general strong duality with complementary slackness of Blanchet–Murthy (arXiv:1604.01446) is proved on the platform, so this mission connects that abstract theorem to an explicit worst-case law. A formal proof also has to settle one point the printed text leaves loose: which extreme maximizers enter the mixture (see Formalization scope).
The first idea is to take the pointwise maximizers of at and push forward. That works only when the maximizer is unique and the budget constraint happens to be tight. In general the maximizer set is not a singleton, and the derivative of at only lies between a left and a right derivative. Turning the first-order condition into an exact cost needs three things. The one-sided derivatives must be identified as expectations over , an envelope theorem under an integral with a non-compact parameter set. The extreme maximizers must be compact and measurably selectable. Finally the resulting coupling must be certified optimal through complementary slackness. Each step needs a hypothesis that is easy to lose: the growth control of Lemma 3, the essential supremum in , measurability of selections.
Points of are EuclideanSpace ℝ (Fin d), is the inner product, and is quadInv A β x. and are extended-real valued; uses the published extended integral ModelRiskOT.Duality.extIntegral. The worst-case objective (6) is the published primal problem primalValue: a supremum over couplings with first marginal and (primalFeasible). A distribution attains (6) when a coupling with that second marginal has value primalValue. The random worst case is encoded by the joint law of , a mixture of two graph couplings, because depends on the pair. A dual optimizer is a real minimizing on .
Standing hypotheses on every statement: a probability measure, Assumptions 1 and 2, , convex. The following departures from the printed text are disclosed in each item:
Every expectation used in the goal (, ) carries an integrability conjunct. The cost identity and optimality are asserted for the measure itself, so no junk value of a non-integrable integral can make the goal hold vacuously. A statement asserting only first-order conditions for would not be Theorem 6. The goal asserts primal attainment and the exact cost.
Needed infrastructure, reusable beyond this mission: envelope (Danskin) theorems for one-sided derivatives of suprema, differentiation of convex integral functionals, measurable selection of argmax sets, and complementary slackness through the published Blanchet–Murthy theorem. Contributions of any of these as standalone lemmas are welcome.
The alternating direction method of multipliers (ADMM) solves linearly constrained problems whose objective splits into separately treatable blocks. For two blocks, , it alternates one minimisation of the augmented Lagrangian in each block with a multiplier update. Its convergence for closed convex has been known since the work of Glowinski–Marrocco (1975) and Gabay–Mercier (1976), and the survey of Boyd, Parikh, Chu, Peleato and Eckstein (2011) made it a standard tool in statistics, imaging and machine learning.
Many applications have three or more blocks: robust principal component analysis with noisy and incomplete data, latent-variable graphical model selection, image alignment. Practitioners therefore apply the direct extension of ADMM, which simply cycles through all blocks in Gauss–Seidel order before updating the multiplier. Whether this extension converges for convex problems remained open for years: convergence was known under extra assumptions (strong convexity with a restricted penalty, Han–Yuan 2012; orthogonality of coefficient matrices, Section 2 of the source paper), and modified schemes with correction steps were proposed precisely because no proof was available.
Chen, He, Ye and Yuan (Math. Program., 2014) settled the question negatively by an explicit three-block example. This mission formalizes that example and the paper's main theorem.
Problem (1.1). Given , , closed convex sets and convex functions , with a nonempty solution set,
Augmented Lagrangian (1.6). For a penalty and multiplier ,
Direct extension of ADMM (1.5). From : minimises over ; minimises over ; minimises over ; and . A sequence satisfying these four conditions for every is a run (IsRun15).
The example. System (3.1) is with columns , scalar unknowns, zero objective, and ; its unique solution is when is nonsingular. The paper takes
the instance example310. With the scaled multiplier , the state is (stateVec). The matrices (3.6) and (3.7) are built from the inner products and the columns, and (3.9).
For the instance (3.10), which satisfies the standing assumptions of (1.1), there are a three-dimensional subspace and a nonzero linear functional on such that for every and every starting point with
a run of (1.5) from exists and no such run converges.
The theorem shows that convexity alone does not make the cyclic three-block ADMM convergent, and the failure is robust: it holds for every penalty parameter and for an open half of a three-dimensional subspace of starting points, on a problem as simple as a nonsingular homogeneous linear system with zero objective. It explains why later convergent variants add assumptions (strong convexity, orthogonality, small step sizes, randomised block order) or modify the scheme, and it is the standard reference for that fact in the operator-splitting literature.
The result is proved in the paper; no machine-checked version is known. A formal version produces a certified negative example for the most widely used multi-block splitting heuristic, a reusable formal model of the extended ADMM (Problem, augLag, IsRun15) on which convergent variants can later be stated, and a worked instance of turning a numerically presented spectral argument (the paper prints its eigen-decomposition to four digits) into exact statements.
The first step, that the iteration on (3.1) is linear in and independent of , is elementary but requires extracting minimisers of convex quadratics from the minimiser conditions of the run. The main difficulty is exact spectral information about a specific rational matrix whose characteristic polynomial is times an irreducible quartic over with two pairs of complex roots of moduli about and . The paper's evidence is a floating-point eigen-decomposition; a proof must instead locate the roots exactly, for example by certified bounds, and must show that the divergent component is present for a whole real subspace of starting points rather than for one numerically chosen vector. Finally, unboundedness of the scaled state has to be transferred back to the original sequence for every .
Vectors are Fin n → ℝ, matrices Matrix (Fin p) (Fin n) ℝ, and in (1.6) is the dot product . Each is real-valued and convex on all of ; "closed" is automatic for such functions and is not stated separately. "Argmin" is read as "a minimiser": the run predicate does not select a minimiser, and the goal asserts that a run exists, so the non-convergence claim is not vacuous. The paper's blocks and multiplier components are 1-based, the Lean components 0-based. Convergence of the sequence is convergence of in the product topology; is never read by (1.5). "Divergent" means "not convergent". The "continuously dense half space of dimension 3" is for a three-dimensional subspace and nonzero linear , expressed in the coordinates ; and are chosen before , as in the paper. Requiring and rules out the trivial choices or . Eigenvalues are complex roots of the characteristic polynomial; a statement using only real eigenvalues would be wrong, since the only real eigenvalue of is . Norms enter only through "", where the choice of norm on is irrelevant. The rounded numbers of (3.11) are not used anywhere.
Every object is defined in ExtADMM.Diverge.Setting. The general definitions (problem, augmented Lagrangian, run) are written for arbitrary dimensions and are intended for reuse by later missions on multi-block splitting. Contributions welcome: proofs of the milestones, exact root localisation for the quartic factor of the characteristic polynomial, and general lemmas such as "a real matrix with an eigenvalue of modulus above one has unbounded orbits on a real subspace".
Deciding whether a planar graph is 3-colorable is NP-complete, so a large part of the theory of planar graph coloring looks for simple local conditions that guarantee 3-colorability. Grötzsch's theorem (1959) is the model result: every triangle-free planar graph is 3-colorable. Forbidding triangles is not the only possibility, and in 1976 Richard Steinberg asked whether forbidding cycles of two other lengths suffices.
Steinberg's Conjecture (1976). Every planar graph with no cycles of length four or five is 3-colorable.
The conjecture drove four decades of work on planar coloring. It was surveyed by Borodin as one of the central problems of the area (Borodin 2013, §7), and it was one of the six graph theory problems ranked with the highest importance in the Open Problem Garden.
Timeline:
All graphs are finite and simple. A cycle of length in a graph is a sequence of pairwise distinct vertices with an edge for each (indices mod ). has no cycles of length four or five if no cycle of has length or ; triangles and cycles of length at least six are allowed. A 3-coloring of assigns one of three colors to each vertex so that adjacent vertices get different colors, and is 3-colorable if it has one. The distance is the number of edges of a shortest – path. is planar if it can be drawn in the plane without crossing edges.
The paper builds its counterexample in three steps, from three concrete graphs given as drawings.
In the Lean development these are the definitions G1, G2 and G. The hypothesis "no cycles of length four or five" is the definition NoFourFiveCycle.
This is the paper's main theorem and exactly the negation of Steinberg's Conjecture. It leaves the witness free, so any counterexample proves it.
Milestones 3–5 together give the goal, with as the witness.
The result. Theorem 3 settles a 40-year-old problem negatively. It shows that forbidding 4- and 5-cycles is not a local condition that forces 3-colorability, which redirects the Erdős relaxation: the threshold for "no cycles of lengths " lies in , since is known and is now excluded. The paper notes that the same graph also disproves the Strong Bordeaux Conjecture and the Novosibirsk 3-Color Conjecture.
Formalizing it. The theorem is proved, and the proof is short. As far as is known it has no machine-checked version. Every claim in the proof is a finite statement about explicit graphs, so the work here is to verify the three gadgets and the gluing arguments in Lean, including planarity of an explicit 166-vertex graph, which is asserted in the paper only through its figures. Planarity, cycle structure and coloring of a concrete graph of this size are a useful benchmark for computational verification in Lean.
The obvious approach is brute force: is a fixed finite graph, so in principle each claim can be decided. In practice decide is not workable at this size. Excluding 4- and 5-cycles means quantifying over walks of a 166-vertex graph. Non-3-colorability is a search over assignments unless it is reduced, as the paper does, through the gadget lemmas. The planarity witness needs explicit coordinates for 166 points and a check of all pairs of segments, in exact arithmetic. The gluing arguments ("a cycle through two copies has length at least six") are where the paper's distance claims are used. Turning those claims into statements about Mathlib walks on unions of embedded copies is the conceptual work.
Lean representation and conventions:
SimpleGraphs. G1 lives on Fin 15, with . G2 lives on Fin 42, with , and G lives on Fin 166, with .G2 is literally (⨆ k, G1.map (copy2 k)) ⊔ the triangle , with explicit embeddings copy2 k : Fin 15 ↪ Fin 42. G is (⨆ k, G2.map (copyG k)) ⊔ the twelve extra edges, with copyG k : Fin 42 ↪ Fin 166. The contact tables are in each definition's statement. A local check confirms the edge counts 23, 72 and 300, and that G agrees edge for edge with an independent transcription of Figure 3.p : H.Walk v v with p.IsCycle, and their length is p.length.H.Coloring (Fin 3), and 3-colorability is H.Colorable 3. "No 3-coloring gives one color" is ∀ C, ¬ (C a = C b ∧ C b = C c). Colorings in which two of the three share a color are still allowed, as in the paper.SimpleGraph.dist. Its junk value for unreachable pairs is never hit, because every asserted distance is positive.OPG37357.IsPlanar: an injective placement of the vertices in in which no vertex lies inside an edge segment and edges with four distinct endpoints have disjoint segments. For finite simple graphs it is equivalent to planarity by Fáry's theorem, and it implies topological planarity.Fin n. This loses no generality for finite graphs, and the empty graph cannot serve as a trivial witness because it is 3-colorable.The following trivializing formalizations are ruled out. Closed walks, instead of cycles, would exclude every graph with an edge. Girth is not used: contains triangles. Lemmas 1 and 2 do not assert that and get different colors, which would be false for . An infinite or unspecified vertex type is not allowed for the witness.
Welcome contributions: decision procedures or certificates for short cycles and colorings of explicit finite graphs; a straight-line embedding of with rational coordinates; lemmas on cycles and distances in graphs glued from embedded copies, which are reusable for other gadget constructions; and proofs of Lemmas 1–2 by computation or by the paper's arguments.
The alternating direction method of multipliers (ADMM) is one of the standard splitting methods for problems of the form , in which a nonsmooth term acts on a linear image of the variable. It is used in signal and image processing, statistical learning and matrix completion, and in many of these applications or is nonconvex: sparsity penalties such as or with , rank constraints, or indicator functions of nonconvex sets. For convex problems the convergence theory of ADMM is classical; for nonconvex problems the questions of whether, and how fast, the iterates converge were open until the last decade.
R. I. Boţ and D.-K. Nguyen (arXiv:1801.01994v2, Math. Oper. Res. 45(2), 2020, DOI) analyse a proximal ADMM with variable metrics and its linearized variant in the nonconvex setting. Their first main result (Theorem 14, the subject of the companion mission of this series) shows that bounded iterates converge to a KKT point when a regularization of the augmented Lagrangian has the Kurdyka–Łojasiewicz property. This mission formalizes their second main result, Theorem 20: when that function has the Łojasiewicz property with exponent , the iterates converge in finitely many steps, linearly, or sublinearly, according to the value of .
Timeline. Łojasiewicz (1963) proved his gradient inequality for real-analytic functions; Attouch and Bolte (Math. Program. 2009) derived from its nonsmooth version the rates / / for the proximal point algorithm; Bolte, Sabach and Teboulle (Math. Program. 2014) gave a general KL-based convergence scheme (PALM); Li and Pong (SIAM J. Optim. 2015) proved convergence of a proximal ADMM under KL assumptions; Boţ and Nguyen (2018/2020) treated variable metrics, relaxation parameters , and the linearized variant, with explicit rates.
Let be proper and lower semicontinuous, differentiable with -Lipschitz gradient, and linear. The augmented Lagrangian with parameter is
Given positive semidefinite matrices , and , Algorithm 1 produces from any starting point by: minimizes ; minimizes ; and . Algorithm 2 replaces in the -step by .
Assumption 2 requires and to be bounded below, to be surjective with (), , , , and for all , where and are explicit functions of .
The analysis runs on the regularized augmented Lagrangian of Section 3
with explicit constants , . Along a run, . If the run converges to , put , and . has the Łojasiewicz property at with constant and exponent if
for all near , where is the limiting subdifferential.
Under Assumption 2, for a bounded run converging to at which has the Łojasiewicz property with exponent :
All constants are existential and independent of ; the goal fixes only the shape of each rate.
Theorem 20 is the quantitative half of the paper: it converts a local growth condition on one explicit function into convergence rates for the iterates of two practical nonconvex splitting methods. Since semi-algebraic functions satisfy the Łojasiewicz property with some exponent, the theorem applies to most of the sparsity- and rank-type models for which ADMM is used, and it explains when finite termination or linear convergence is to be expected. The intermediate results (Lemma 15 in particular) are the standard route from a Łojasiewicz inequality to rates and recur in the analysis of many first-order methods.
The result is proved in the paper; to our knowledge no part of it has a machine-checked proof. The mission produces a formal statement and proof of the rates, with every constant of the paper defined explicitly, and records where the paper's constants need recomputing: the constants and of Lemma 9 are reused on p. 26 for a regularization whose gradient is twice as large.
Lemma 15 is elementary but delicate: the recurrence has a lag and, for , a nonlinearity that a direct induction does not control, and the index bookkeeping determines the exponent. The rates for require a bound on an explicit subgradient of , whose limiting subdifferential involves the nonsmooth , so the calculus of limiting subgradients for a sum of a lower semicontinuous and a smooth function on a product space is needed. Transferring rates from to the iterates needs a finite-length estimate with explicit constants, uniform in the tail. A tempting shortcut, applying the Łojasiewicz inequality directly to , fails: does not decrease along the iterates; only the regularized does.
Vectors live in EuclideanSpace ℝ (Fin n); takes values in EReal and is proper and lower semicontinuous; and take values in EReal. Points of form a nested WithLp 2 product, so the norm and the inner product are the Euclidean ones of the paper. The limiting subdifferential is the published NonconvexSplitting.Shared.LimitingSubdiff. The two algorithms are the constructors of an inductive type; a run is a relation (any minimizer may be taken), and every statement holds for both. and are replaced by arbitrary valid bounds. is , which the paper shows equals .
The Łojasiewicz hypothesis requires the inequality for every subgradient, so that , and only at points with , the convention ; with Lean's the hypothesis would be unsatisfiable at , and a Łojasiewicz hypothesis that no function satisfies, an Assumption 2 that no data satisfy, or a rate whose constant depends on would each make the targets trivial. Assumption 2 together with the run predicate is satisfiable (checked on a one-dimensional instance), and all constants are quantified before .
Labelled corrections: uses as displayed on p. 25 (not ); and are recomputed for the Section 3 ; Lemma 17 asks for ; Lemma 19 assumes , since for the paper's is .
Needed infrastructure: calculus of the limiting subdifferential for the sum of a lower semicontinuous function and a function on a product space, the descent lemma, and real-power estimates for sequences. Lemma 15 is independent of ADMM and reusable. Proofs of individual milestones are welcome in any order.
The alternating direction method of multipliers (ADMM) solves a constrained optimization problem by minimizing an augmented Lagrangian over one block of variables at a time and then updating a multiplier. Its two-block version had established convergence results. Applying the same cycle to three or more blocks was natural in models whose objective separates into several terms, but its convergence was unresolved when Chen, He, Ye and Yuan wrote this paper. Their analysis gives both a sufficient condition for convergence and, elsewhere in the paper, a counterexample to unrestricted convergence. This mission concerns the sufficient condition: the first and third constraint matrices are orthogonal in the sense . Chen, He, Ye and Yuan (2014)
The condition matters because the third block is separated from the first in the quadratic part of the augmented Lagrangian, while the middle block still participates in both updates. The result therefore covers a genuine three-block algorithm. It identifies what the direct cyclic extension can guarantee under this structure. The companion result gives an ergodic rate for averages of auxiliary iterates, from any starting point.
The three-block problem has variables , matrices , and a vector :
Each is closed and convex, each is convex, and the primal solution set is nonempty. For , write . The augmented Lagrangian is . The minus sign in front of fixes the sign of the multiplier step of (2.4c).
The paper analyzes a reordered cycle, numbered (2.4): minimize in , minimize in , update , then minimize in . The input state is ; is an intermediate variable. Each minimization may choose any minimizer. The reordered cycle is the cyclic direct extension with shifted by one index. A run is any sequence satisfying all four update conditions. Chen et al., pp. 4–5
Let , , and . The affine map has blocks . The variational inequality solution set consists of for which for every . Such points are the KKT points used in this mission. The paper employs and without defining them; these definitions fix their intended meaning.
Let , and let be the corresponding projection of . With the positive semidefinite block matrix in equation (2.11), the main target is Theorem 2.4:
If and have full column rank and , the entire sequence converges to a point of . The milestone list follows the paper's affine monotonicity statement, Lemmas 2.1–2.3, the displayed contraction, the summability and vanishing correction terms, and the cluster-point variational inequality. Chen et al., pp. 5–9
Theorem 2.5 bounds a gap at the average , where is the auxiliary point of (2.13). For every , the target is
This companion is stated, as on the page, for an arbitrary starting point. Chen et al., p. 9
The contraction gives a quantitative decrease relative to any variational inequality solution, even though is only semidefinite. Combined with the rank assumptions, it yields convergence of all primal blocks and the multiplier to a KKT point. The auxiliary average gives a finite-iteration gap bound with an explicit coefficient. These statements locate a useful structural regime inside a method that the same paper shows can diverge without additional conditions.
The formal development records the whole update cycle, the variational inequality, and the two block operators and . It leaves the named theorems as proof targets; compiling their statements does not claim a machine-checked proof. The definitions and intermediate inequalities can be reused when formalizing other cyclic splitting schemes or comparing this one with two-block ADMM.
The familiar two-block ADMM convergence argument cannot simply be applied to a three-block cycle: the middle iterate is updated between the first and third blocks, and the multiplier update sits before the next first-block minimization. The resulting one-step inequality contains a correction involving the previous and next essential states. Even after that correction is controlled, is semidefinite, so contraction in its quadratic form alone does not imply convergence of every coordinate. The full column rank conditions provide the additional control demanded by the paper's conclusion.
Vectors are functions on Fin n; matrices are Mathlib matrices. Every occurrence of a squared Euclidean norm in the paper is represented by a dot product or the expanded quadratic form. Mathlib's default norm on a function vector is a sup norm, so it is not used for those squares. The topology in the final convergence statement is the product topology on the four vector blocks. The block labels in the paper correspond to separate fields in Lean. The initial is unused by the run predicate. A zero-dimensional block is allowed when the stated conditions still make sense.
There are disclosed repairs to the printed text. Lemma 2.3 and the contraction are restricted to : their derivation uses the preceding optimality condition, which an arbitrary initial point need not satisfy. The convergence part additionally assumes , since the paper assumes a primal optimizer but supplies no constraint qualification guaranteeing a KKT point. Lemma 2.2's displayed uses , while its inequality and the run use ; Lean uses the latter. Theorem 2.5's verbal assertion that is represented as the indexed average .
The convex objectives are real valued on all of , as on p. 1. Such a convex function is continuous, so the paper's word “closed” adds no extra condition here. Runs quantify over actual minimizers and are not constructed by a default-valued argmin; this prevents an empty subproblem from creating a fictitious iterate. A complete proof can contribute the convex first-order conditions, matrix identities, summability argument and finite-dimensional convergence steps. The reusable interfaces are the three-block problem, run, variational inequality and block quadratic forms.
Many first-order methods for nonconvex and nonsmooth optimization are analysed with the same template: a merit function decreases by a definite amount at every step, a subgradient of the merit function at the current point is bounded by the step length, and the Kurdyka–Łojasiewicz (KL) property of the merit function turns these two facts into a proof that the whole sequence of iterates has finite length and converges. Attouch and Bolte (Math. Program. 2009), Attouch, Bolte and Svaiter (Math. Program. 2013) and Bolte, Sabach and Teboulle (Math. Program. 2014) isolated this template as a set of abstract conditions. Later frameworks for methods with inertia or extrapolation, such as iPiano (Ochs, Chen, Brox and Pock, SIAM J. Imaging Sci. 2014), needed the relative error bound to involve more than one past step.
Boţ, Dao and Li (arXiv:2003.04124, Math. Oper. Res. 2022) state a framework (H1)–(H5) in which the relative error bound is a convex combination of several step lengths, past or future, plus a summable error, and the iterates of the algorithm may live in a different space from the merit function. They prove finite length, convergence, stationarity and, for KL exponent at most , linear rates; they then apply it to an extrapolated proximal subgradient method for fractional programs. This mission formalizes that abstract result, Theorem 5.2 of the paper.
Let and be finite-dimensional real Hilbert spaces and a proper (never , finite somewhere) lower semicontinuous function. denotes the limiting subdifferential of at , empty where , and .
Data: sequences in and in ; ; , with the convention for ; integers (not necessarily positive), , and weights with . The conditions, for all , are:
is the set of cluster points of , , and for . A desingularizing function is continuous and concave on , vanishes at , and is with on . has the KL property at if for some neighbourhood of , and , whenever and ; it has the KL property with exponent if can be taken as .
Assume (H1)–(H4), bounded, constant on with the KL property at every point of . Then
(iv) if has KL exponent on , , and , then for some , ,
and under (H5) and , for the same .
Lemma 2.3 (uniformized KL along a bounded sequence, and its power form under an exponent); Lemma 5.1(i)–(iii) (nonemptiness of and monotone convergence of values; ; the subgradient bound and stationarity); the tail bound (24) from the proof of (i); Theorem 5.2(i); and the first claim of Theorem 5.2(iv).
The theorem separates what is specific to an algorithm (checking (H1)–(H5) for its iterates) from what is common to all KL-based analyses (finite length, convergence, rates). In the paper it yields global convergence of the extrapolated proximal subgradient method (Theorem 5.5) with and , and Remark 5.4 shows that the frameworks of Attouch–Bolte–Svaiter, Bolte–Sabach–Teboulle, Frankel–Garrigos–Peypouquet and iPiano are special cases, while the linear rate for the iterates in the multi-step setting is new relative to those frameworks.
The result is proved on paper. To our knowledge no machine-checked version of this abstract framework exists. A formal proof yields a reusable theorem: any later mission that verifies (H1)–(H5) for a specific method gets convergence and rates by citation. Related single-algorithm KL convergence results on the platform (proximal alternating minimization, PALM, proximal ADMM) each repeat the same argument; this framework is the common abstraction.
The naive argument—sum (H1) to get —gives only square-summability, which does not imply convergence of the iterates. Finite length needs the KL inequality along the whole tail of the sequence with one function , but the KL property is only pointwise; this requires a uniformization over the (compact) cluster set and the restriction to , where values converge. The multi-step error with possibly negative indices in means the right-hand side of (H2) can involve future steps, so the telescoping estimate must absorb sums with shifted index ranges. For the rates, the KL exponent turns the inequality into a recursion between and separated by several steps, whose contraction must be shown to give a geometric rate.
is EuclideanSpace ℝ (Fin N) and is EuclideanSpace ℝ (Fin P); takes values in EReal, with properness and limiting subdifferential from the published NonconvexSplitting.Shared definitions and the KL property (HasKLProperty, IsDesingularizer, KLIneq) from the published NonconvexSplitting.ADMMKL definitions. is a positive real. is indexed by and vanishes on negative integers. is encoded as "some has ", and the KL inequality as "every satisfies "; Metric.infDist is never used, because it returns on the empty set where the paper's distance is , which would make (H2) trivially satisfiable. Infima are encoded by positive lower bounds; hypotheses as eventual bounds with a constant; by quantifying over . Lemma 5.1(ii) assumes explicitly, which the page presupposes.
The definitions file FracPSG.Abstract.Basic (the setting, (H1)–(H5), , , the KL exponent) is reusable by any mission that instantiates the framework. Contributions welcome: proofs of the milestones, the uniformized KL lemma in general form, and summation lemmas for sequences indexed by .
Data-driven decision making estimates the cost of a decision from training data and then optimizes that estimate. The optimized estimate is biased downwards: the decision that looks best on the training data tends to disappoint on fresh data. Distributionally robust optimization counters this by optimizing the worst case of the estimate over all distributions within a radius of the empirical distribution, measured by a chosen distance function . Many distance functions are in use (φ-divergences, Wasserstein distances, moment sets), and the choice is usually justified by tractability.
Bertsimas and Van Parys, Bootstrap robust prescriptive analytics (arXiv:1711.09974v2), measure disappointment on bootstrap data: resamples drawn with replacement from the training data. Their Theorem 6 shows that with the entropic bootstrap distance the bootstrap disappointment decays exponentially in the sample size at rate at least . Proposition 1, the subject of this mission, is the converse: is the smallest distance function with this guarantee. Any distance that is strictly larger than near some distribution admits a nominal formulation whose disappointment decays strictly slower than . The result is in the spirit of Van Parys, Esfahani and Kuhn (arXiv:1704.04118), where the relative entropy is shown to be the optimal ambiguity set for i.i.d. data.
The distinct training points form a finite set , written in Lean. A distribution on it is a vector with nonnegative entries summing to one; the simplex of all such vectors is . The training data have the empirical distribution , which gives positive weight to every point of .
The bootstrap distance (Definition 6, Eq. (27)) is the relative entropy
with and if some .
A distribution distance function (Definition 4) is a map that is nonnegative, vanishes exactly on the diagonal ( iff ), and is convex in its first argument. is one.
A bootstrap sample of size is independent draws from (Eq. (14)); its law is the product , and its empirical distribution is , the frequency of each point of among the draws.
A nominal formulation here is a loss with cost estimator . Its robust counterpart (Eq. (24)) replaces the estimate by , and its disappointment set is
the bootstrap distributions on which the realized cost exceeds the robust budget.
Let be a distribution distance function, with , and a neighbourhood of , open in , on which . Then there is a loss whose disappointment set satisfies
stated in Lean in the equivalent form: for some , eventually .
Proposition 1 turns Theorem 6 from a sufficient condition into a characterization. Theorem 6 says the bootstrap distance guarantees disappointment rate ; Proposition 1 says no distance function that is larger than on an open set does, for some nominal formulation. A practitioner who wants the bootstrap guarantee with the least conservative ambiguity set therefore has no better choice than in this sense. The result is one instance of a pattern in data-driven optimization, where large-deviation rate functions appear as the optimal ambiguity sets.
The paper's proof is a short combination of three standard facts: strict separation of convex sets, Sanov's theorem, and convexity of relative entropy. None of the three is available on the platform in the form needed. Sanov's theorem for empirical distributions on a finite alphabet has no machine-checked proof in Mathlib or on the platform; the lower bound (31) is a self-contained, reusable result of independent interest. The separation step needs strict separation inside the affine hull of the simplex, which Mathlib provides only in the ambient vector space. The result is proved on paper; none of it is formalized.
The separation and convexity steps are routine once the relative topology of the simplex is handled. The central difficulty is the lower bound (31), a large-deviation lower bound for the empirical distribution of i.i.d. draws. The bootstrap probability of an event is a sum of multinomial probabilities over the empirical distributions with denominator that fall in the event, and the bound must hold for every point of the relative interior, including points on the boundary of the simplex, where some coordinates vanish and the distance is not differentiable. An argument that only treats distributions of full support, or only open sets of , does not cover these points.
A second difficulty is bookkeeping between the three topologies in play: the ambient space , the simplex , and the affine hull in which separation takes place.
stdSimplex ℝ ι. Covariates, responses, neighbourhood weights and the decision are abstracted away: the nominal formulation is the estimator (the estimator (18) with and unit weights), so the robust prescription plays no role.EReal-valued; convexity of is written out in EReal. The supremum defining is an EReal supremum. It is never empty, because lies in the -ball, so cannot collapse to all of .Measure.pi of , with fixed while .A complete development needs the method of types on a finite alphabet, strict separation in an affine subspace, and the convexity of relative entropy. The method-of-types lower bound is reusable well beyond this mission (hypothesis testing, large deviations of empirical measures). Proofs of any milestone, and alternative proofs of (31), are welcome.
A two-stage stochastic program chooses a decision before uncertainty is observed and a recourse decision afterward. Its objective can involve the expected optimal value of the recourse problem. Even with linear constraints, evaluating that expectation can be difficult when the random input has many coordinates. Dyer and Stougie's 2006 complexity paper studied this question for stochastic programming. Hanasusanto, Kuhn and Wiesemann identified a false volume identity in one fixed-recourse argument, then supplied a quantitative replacement in their 2015 preprint. The replacement shows that sufficiently accurate expected-recourse values determine an exact counting answer.
The distinction matters to researchers designing numerical methods for stochastic programs. A hardness statement at a specified absolute accuracy identifies the scale at which a general exact-information guarantee would have strong complexity consequences. It does not say that useful approximations at coarser accuracy are unavailable. The present mission records the mathematical reduction behind the paper's Theorem 1 and its quantitative tolerance.
Let . A realization lies in the unit cube , equipped with Lebesgue measure. This cube has volume one, so integration over it is expectation under the uniform law. Let be nonnegative weights and a budget. The second-stage value is the maximum of
over and for each . Its expected recourse value is . There is no first-stage decision in this instance of the model.
The knapsack polytope is , and denotes its volume. For integer weights and budget, its binary points correspond to subsets with . The #Parity count is the number of such subsets of even size minus the number of odd size. The paper invokes the counting complexity of this problem from Dyer and Frieze's 1988 volume paper.
For , define and a square matrix by for . The first column has power and the last has power zero. This order matters: the first coordinate of the coefficient vector is the parity count. The matrix inverse is controlled by a column-sum bound of the kind studied by Gautschi in 1962.
Write and , exactly the right sides of (3) and (7). For positive integer weights, , and , take any oracle with at every nonnegative . Set and
The target is that every solution of
satisfies . Nearest-integer rounding therefore recovers .
The milestones establish the value formula for the second-stage program, the inclusion–exclusion volume formula (8), the integer coefficient identity for the exact volume system, the inverse bound (4), the perturbation bound (6), the derivative identity in Lemma 2, a global volume-growth bound, and the finite-difference estimate in Theorem 1. Together they retain the paper's constants and its sequence from expected values to volume approximations to an exact count. Proposition 1 separately records why the earlier proposed identity fails.
The result certifies a concrete information transfer. A function returning expected-recourse values to the stated absolute tolerance also contains enough information to distinguish the exact even-minus-odd count of feasible binary points. The bound states how accurate those values must be as dimension and weights change; a qualitative assertion of hardness alone would hide that dependence. The paper concludes #P-hardness after accounting for the polynomial-time operations of the reduction. That complexity-class conclusion is part of the paper, while the Lean goal isolates the reduction's numerical correctness.
A complete formalization would give separately reusable results about cube integrals, knapsack volumes, perturbations of Vandermonde systems, and finite differences of expected hinge functions. The source paper proves the mathematical assertions; this proposal stages their Lean statements as open proof obligations. No machine-checked proof is claimed here. The companion counterexample also keeps the corrected argument anchored to the precise error it repairs.
The tempting identity fails: the expectation of the second-stage optimum is a positive-part expectation, while volume is a distribution function. The paper's Proposition 1 makes the discrepancy explicit for all-ones weights. Recovering volume requires differentiation with respect to the budget, and an approximate function value does not directly provide an accurate derivative. The difficulty is controlling both oracle error and the change of volume over a finite budget interval tightly enough that the final coefficient error is strictly below one half.
There are further exactness points. The column order of fixes which coefficient equals . The -norm in (4) is the maximum column sum of the inverse, not a generic matrix norm. The perturbation threshold contains , every weight, and the power ; losing one factor can invalidate the rounding guarantee.
Lean uses vectors , with zero-based indices; the paper's is the final coordinate. Lebesgue measure is restricted to , whose volume is one. The LP value is a real supremum of its feasible objective values. For the nonnegative weights used in the theorems, the feasible set is nonempty and bounded, so this represents the actual maximum. The expected value is a real integral over the cube. The matrix has descending powers, and its -norm estimate is written as a bound on each inverse column sum. Binary vectors are represented by subsets; keeps the paper's even-minus-odd convention.
Positive weights are required where (3) and (7) divide by their product, and where divides a finite difference. The case is excluded from the main target because the paper first answers it directly with . Lemma 2 excludes , where the claimed derivative fails to exist. The volume-growth milestone gives the content of the paper's argument without requiring a second derivative at a kink; it applies across the actual interval starting at . The printed determinant sign is also adjusted to the descending columns by asserting nonsingularity, which is what the proof uses. The second-stage value milestone retains only the optimal value, because the optimal decisions the page calls unique need not be unique at ties. The mission must use the LP and counting definitions above; replacing them with an arbitrary function assumed to have the desired derivative would empty the reduction.
The formal work requires measure and integration theory, finite polytope volume, finite sums over subsets, matrix inverses, and real inequalities. Contributions proving the eight milestones and any honest supporting lemmas are welcome. The setup does not encode polynomial-time computability, bit lengths, or a #P complexity class, so closure of the Lean goal alone is not a formal proof of the full complexity statement.
Prescriptive analytics chooses a decision from data after observing a context : a retailer sets an order quantity after seeing the weather forecast, a hospital schedules staff after seeing the day of the week. A common recipe estimates the expected cost of each decision from the training observations closest to (nearest neighbours, or a kernel-weighted Nadaraya–Watson average) and then minimizes that estimate (Bertsimas and Kallus, 2020). The decision that minimizes an estimate tends to look better on the training data than it is: its estimated cost is optimistically biased. Bertsimas and Van Parys (arXiv:1711.09974v2) measure that optimism on resampled data. Bootstrap data are independent draws from the training distribution, in the sense of Efron (1979). A cost budget computed on the training data disappoints when the estimate on a bootstrap sample exceeds it. The paper replaces the nominal estimate by a robust budget, a worst case over all distributions within relative-entropy distance of the training distribution. Its Theorem 6 bounds the probability of disappointment by an explicit sum of exponentials in .
This mission formalizes that theorem, together with the structural results its proof rests on and the Nadaraya–Watson special case, Corollary 2. The same paper's dual reformulation of the budget (Lemma 2) and its optimality statement for the relative entropy (Proposition 1) are the subject of two sibling missions.
The training points have a finite set of distinct values. A distribution on is a vector in the standard simplex; these form . The training distribution gives every point of positive mass. The bootstrap distributions are
These are the possible empirical distributions of independent draws from .
Around the context the points of are grouped into nested neighbourhoods . Each point carries a positive weight and, for a decision , a loss . Fix . The estimator (18) of a distribution averages the loss with weights over the smallest neighbourhood with -mass at least . For , the partial estimator is the value of the linear program (22). Its domain is contained in
and off that domain .
The bootstrap distance is the relative entropy
The partial robust budgets are , the robust budget is (26), and the minimum radii are (29).
For every decision ,
The bound holds for every , , neighbourhood chain, weight vector and radius, with no asymptotics.
Theorem 6 makes the radius an explicit statistical dial. The sum can be computed from the training data, because each is a convex program. So a practitioner can choose for a target disappointment , and the bound decays exponentially in at rate at least . Corollary 2 gives a single exponential bound for Nadaraya–Watson: gives disappointment at most . Together with the paper's Proposition 1, which shows that no smaller distance keeps the rate , the result explains why the relative entropy is the natural ambiguity measure for bootstrap guarantees.
On the formal side, the results are proved in the paper. Theorem 5 is cited there from Csiszár (1984), not reproved. The local platform search found no matching machine-checked statement of Theorem 6, Theorem 1 or Csiszár's convex-set inequality. A formal proof of Theorem 5 on a finite alphabet would be a reusable large-deviation tool: a finite-sample Sanov upper bound without polynomial prefactor, for empirical distributions of i.i.d. samples in any convex set. Theorem 1 and the partition lemma are the combinatorial facts behind the nearest-neighbours robust formulation of this paper.
Two steps carry the weight. The first is Theorem 5. The method of types alone gives , and its polynomial factor is fatal here: the goal has none. Removing it needs convexity of in an essential way; the bound is false for general sets. The set need not be closed and its infimum need not be attained. The second is Theorem 1. The estimator selects its neighbourhood depending on , so it is neither linear nor concave in . The disappointment event is therefore not convex, and Theorem 5 cannot be applied to it directly. Splitting it over the sets needs the partition of . That partition fails off the grid : a mass strictly below is at most only for multiples of .
The support is a finite type , and a distribution is a vector ι → ℝ in stdSimplex ℝ ι. Covariates, responses, the context and the distance function of Definition 2 do not appear. The neighbourhoods are a chain N : ℕ → Finset ι with Monotone N, N 0 = ∅ and N n = univ, which abstracts Definition 2 and its tie-breaking. Weights are positive, losses are real-valued (Assumption 1 allows ; no planned statement needs it), and nonnegativity and convexity of the loss are not assumed. The relative entropy is EReal-valued, with and when . Every supremum and infimum that may be empty or unbounded is in EReal: an infeasible program (22) is , an empty has , and . The bootstrap law is the product measure Measure.pi of copies of . The robust budget is the formulation (26), , which the paper computes and which never exceeds (24). The theorem is stated for every decision , not only for the robust prescriptor. The printed strict inequalities for the infima over are stated as .
Trivializing encodings are ruled out explicitly. Real sSup/sInf would turn infeasible programs and empty sets into a finite . A real logarithm with a vanishing reference would give a finite junk value. A single draw or a non-product law would make Theorem 5 false. A chain without and would break the partition. expNeg treats explicitly so that an empty contributes , not .
A complete development needs the method of types on a finite alphabet, I-projections onto convex sets of the simplex, and the Pythagorean inequality. The latter two are reusable well beyond this mission. Contributions to any milestone, or to a standalone finite-alphabet Csiszár inequality, are welcome.
A promise constraint satisfaction problem asks to distinguish instances that are satisfiable in a structure from instances that are not even satisfiable in a weaker structure . Approximate graph colouring (tell 3-colourable graphs from graphs that are not 5-colourable) and are standard examples. The algebraic approach to CSPs explains the complexity of such problems through polymorphisms, the multi-argument maps that preserve every relation.
Two polynomial-time relaxations dominate the algorithmic side: the Basic LP relaxation, solved over , and the affine relaxation, the same linear system solved over . Barto, Bulín, Krokhin and Opršal (BBKO19) characterized each one separately: BLP solves exactly when has symmetric polymorphisms of all arities, and the affine relaxation exactly when it has alternating polymorphisms of all odd arities. Brakensiek and Guruswami (BG19) used ad hoc combinations of the two. Brakensiek, Guruswami, Wrochna and Živný (arXiv:1907.04383) combine them into a single algorithm, BLP+Affine, and characterize its power exactly. This mission formalizes that characterization, Theorem 4 of the paper.
A signature assigns to each symbol an arity . A relational structure on a finite domain fixes relations . A homomorphism is a map sending every tuple of into , and is a promise template if one exists. An instance has variables and constraints ; it is satisfiable in (written ) if some assignment sends each into .
A map is a polymorphism if applying column-wise to any matrix whose rows are in gives a tuple of . It is block-symmetric for a partition if it is invariant under permutations of its arguments that preserve every block, and its width is the largest minimum block size over such partitions.
The Basic LP has a probability distribution on for each variable and on for each constraint, with the marginal of at each position of equal to the distribution of the variable in that position. The affine relaxation is the same system over with unknowns , and no sign constraints. BLP+Affine (Figure 1) takes a relative interior point of the LP, keeps only the integer solutions that vanish wherever does, and accepts iff one remains. It correctly solves if it accepts every and rejects every .
The minor of along is . The minion has as -ary objects the pairs with , , both summing to , and ; the minor along sums both over fibres of . A minion homomorphism sends -ary objects to -ary polymorphisms and commutes with minors. The free structure has the -ary objects as its domain, and a tuple is in iff it is the family of coordinate minors of one -ary object.
For a promise template on finite domains, the following are equivalent:
The paper proves Theorem 4 through Lemmas 7, 8 and 9. The milestones follow that proof:
A companion item, Example 10, records that the disjoint union of a directed 2-cycle and a directed 3-cycle has no block-symmetric polymorphism of width at least .
Theorem 4 is an exact criterion: the power of an algorithm is read off from the polymorphisms of the template. Its sufficiency direction (Theorem 3, the subject of the companion mission) says that one fixed algorithm decides every PCSP with block-symmetric polymorphisms of unbounded width, which covers nearly all tractable Boolean PCSPs known at the time, including those with threshold and alternating-threshold polymorphisms. The necessity direction, new in Theorem 4, gives a method for proving that BLP+Affine fails on a template: exhibit, for some , the absence of a -ary polymorphism with blocks of sizes and . Example 10 is an instance: a tractable template that the algorithm does not solve. The minion and its free structure are the template for later characterizations of relaxation hierarchies.
The result is proved in the paper. As far as is known it has not been machine-checked. A formalization adds a checked development of minions, minion homomorphisms and free structures for PCSPs, a compactness theorem for relational structures, and a checked version of the one-block argument whose many-block extension the paper only asserts.
The equivalence passes through three different kinds of object: an algorithm, an infinite algebraic object (a homomorphism defined on all of ), and finite families of polymorphisms. From polymorphisms one obtains homomorphisms only on finite pieces , each from a different polymorphism, and these do not agree with one another; a single homomorphism on the whole minion needs a compactness argument over the finitely many restrictions, which uses the finiteness of and . The passage from "every instance satisfiable in the free structure is satisfiable in " to a homomorphism from the infinite free structure is a second compactness step. The relative interior point of Figure 1 must be kept: accepting whenever both relaxations are merely feasible is a different, weaker algorithm.
All objects are in the definitions file PCSPBLPAff.Characterization.Setting, built on Mathlib only.
(τ : Type) (ar : τ → ℕ), with no finiteness of ; the paper's requirement that arities be positive is dropped, and no statement needs it. Domains are finite types; instance variables are Fin n and arities Fin L.Two trivializing formalizations are ruled out: the acceptance condition keeps the maximal-support requirement, and the free structure's relation requires the witnessing pair to be an object of supported in .
A complete development needs finite sums over fibres, transport of objects along Fintype.equivFin, Tychonoff or König's lemma (Mathlib.Order.KonigLemma, Mathlib.Combinatorics.Compactness), and the existence of a maximal-support point of a rational polytope. The compactness theorem for relational structures and the free-structure lemma are reusable beyond this mission. Proofs of any milestone, and of the general Lemma 17 for an abstract minion, are welcome.
Distributionally robust optimization chooses a decision against a range of plausible probability laws instead of a single fitted law. Here the decision is a linear rule evaluated through a loss function. The range of laws is specified by how much probability mass may be transported away from a baseline law. A conventional transport cost depends only on the displacement. Blanchet, Murthy and Zhang allow the cost of moving a point to depend on its starting location, so the uncertainty model can reflect local information. Their introduction gives a portfolio example: uncertainty about returns may differ across market conditions, and a state dependent cost can encode that difference. The paper develops a dual reformulation as the basis for its later convexity, optimizer, and algorithmic results.
The theorem in this mission is the first structural result of that development. It says that evaluating the worst-case loss does not require optimizing directly over all probability distributions. A dual objective built from the baseline law gives the same value, and its nonnegative scalar multiplier attains the best value. The earlier general transport duality theorem of Blanchet and Murthy is already formalized and proved on Prove2Me; the remaining target here is the state dependent Mahalanobis specialization and its explicit scalar form.
Let have a baseline law , and let be a convex set of decisions. A decision incurs loss , where . The transport cost of moving to is
where is positive definite at every . Under Assumption 1, is lower semicontinuous, and the eigenvalues of lie between fixed positive bounds and for -almost every . Since depends on the starting point, need not be symmetric. For two laws and , is the least expected cost among couplings whose first and second marginals are and . The ambiguity set at radius consists of laws satisfying . The paper writes the worst-case loss as an equivalent supremum over couplings with first marginal and cost at most (§2.1, p. 9).
For , write . The paper introduces a pointwise robust loss from
by setting and . This expectation may be extended real. These are the objects of display (7) and Theorem 1 on p. 10.
The goal is Theorem 1 of the paper. If is upper semicontinuous and the baseline loss is integrable, then for each ,
and a multiplier attains the infimum. The target retains the state dependence of , the full range of in , and the possible extended value of the worst-case loss. It asserts both the value identity and attainment; the latter is part of the printed theorem.
The milestone list follows the paper's proof on p. 32: the previously proved general strong duality theorem, the quadratic minimum under a linear constraint, and pointwise equality (25) between the transport envelope and . The quadratic minimum is stated with attainment. The pointwise equality includes and records the change from the original transport multiplier to the scaled multiplier used in .
The formula replaces a search over probability laws with a scalar outer optimization and an expectation under . That representation is the paper's starting point for examining the shape of , locating dual optimizers, describing worst-case laws, and designing iterative schemes. Without a faithful dual identity, those later claims would concern a function whose connection to the original distributional problem had not been established (Theorems 2–7).
The general Blanchet–Murthy strong duality theorem has a machine-checked proof on Prove2Me. This mission supplies the specialized model, the quadratic reduction, and the equality with the paper's . Those declarations can then serve as a stable interface for the remaining missions in this series. The current goal and its new milestones are open Lean statements; the paper result itself is proved in the cited work.
The general duality theorem returns a dual problem whose envelope is a supremum over destination points in . The paper's formula instead uses one scalar , and its multiplier is scaled by . Showing that these describe the same value requires controlling a positive definite quadratic cost with a state dependent matrix at every starting point. At , the hyperplane formula used in the nonzero case has a zero denominator, while equation (25) remains meaningful. Extended values also matter: the pointwise supremum can be infinite, and replacing it with a real-valued approximation could alter the theorem.
Vectors are EuclideanSpace ℝ (Fin d), laws are Borel probability measures, and matrices are real positive definite matrices. The local Setting definition fixes , , , , and using the paper's notation. The worst-case objective reuses the published coupling form ModelRiskOT.Duality.primalValue; its feasible plans already enforce the first marginal and cost budget. EReal carries the primal value, pointwise supremum, integral, and outer infimum. The extended integral is the published ModelRiskOT.Duality.extIntegral, with its documented convention for a difference of two infinite parts. The multiplier ranges over , and is explicit so its square root can be used in the rescaling.
The goal retains the paper's standing convexity of , Assumption 1, and . It adds integrability of , required by the cited general duality theorem but omitted from the printed Theorem 1. This addition is disclosed so the statement's scope is clear. The goal equates the primal worst-case loss with the explicit infimum of and asserts attainment; an identity between two dual notations would leave the main claim unaddressed. Contributions to the positive definite quadratic minimization, the pointwise envelope equality, and their connection to the general duality theorem are in scope. The shared Setting layer is intended for reuse in the later convexity and worst-case-law missions.
Regularized loss minimization covers support vector machines, logistic and ridge regression, and the absolute-deviation regression of robust statistics. Stochastic dual coordinate ascent (SDCA) solves these problems by maximizing the Fenchel dual one randomly chosen coordinate at a time. Shalev-Shwartz and Zhang (arXiv:1209.1873, JMLR 2013) gave the first analysis of SDCA in terms of the duality gap. For smooth losses their rate is linear; for Lipschitz but non-smooth losses such as the hinge loss it is of order , which is no better than stochastic gradient descent, although SDCA is observed to converge much faster than SGD on SVM problems asymptotically.
Section 5 of the paper explains that observation. Many non-smooth losses are smooth at most points: the hinge loss fails to be smooth only at . If, at the optimum, most margins stay away from the kink, the dual is strongly concave in most coordinates, and SDCA converges linearly in the dual objective. Earlier linear-rate results for dual coordinate ascent on SVMs (Luo and Tseng, 1992) depend on the smallest nonzero eigenvalue of the data Gram matrix, which can be arbitrarily small when two data points are close; the condition of Section 5 avoids the Gram matrix.
Data (Euclidean norm), scalar convex losses and define the primal problem
The convex conjugate of is . The dual problem is with
A dual variable is feasible when every is finite. A function is -Lipschitz if . The standing assumptions are , and .
Procedure SDCA starts from . At iteration it picks uniformly at random, independently of the past, chooses maximizing , and sets . Let be a dual optimum and .
The refined dual strong convexity condition (Definition 2, (4)) asks for functions with
For the hinge loss one may take . With constants , the dual strong convexity inequality (5) is
and counts the coordinates with small modulus.
Assume convex -Lipschitz losses, the standing assumptions, and (5) with constants . For every and with ,
The constants and are the paper's.
Theorem 5 gives a linear rate for the dual sub-optimality of SDCA on non-smooth losses whenever few constants are small. If for some (for the SVM, for all ), the iteration count is , compared with order from the Lipschitz analysis of Theorem 1 of the same paper. The paper uses Theorem 5 to explain the observed asymptotic advantage of SDCA over SGD, and its Theorem 6 converts it into a duality-gap bound.
The result is proved in the paper. It has not been formalized: no SDCA convergence result is on Prove2Me, and Mathlib has no conjugate-duality theory for this problem class. The mission produces a formal account of the dual objective in extended reals, of the exact coordinate maximization step, and of the averaging over uniformly random coordinate sequences, together with a checked proof of the rate. The companion missions of this series cover Theorem 1 (Lipschitz losses) and Theorem 2 (smooth losses).
Condition (5) gives a modulus per coordinate, and some may be zero, so the dual is not strongly concave and the standard linear-rate argument for strongly concave coordinate ascent does not apply. The per-step progress has a variance term with the sign of , which is positive exactly on the coordinates with small modulus; that term must be controlled by bounding the dual variables themselves, which requires the Lipschitz structure through the conjugate. The extended-real-valued conjugate is a second source of work: every quantity must be shown finite along the run before it can be manipulated as a real number.
Lean works in EuclideanSpace ℝ (Fin d), with data points indexed by Fin n, . The conjugate is an EReal supremum and is EReal-valued, exactly at infeasible points. Real-valued expectations of dual values appear only together with a conjunct stating their finiteness. The SDCA step is a map with the hypothesis that is an exact maximizer of the coordinate objective. The run is a fold over the sequence of chosen coordinates, and the expectation is the uniform average over all sequences of length (SAGA.Convex.expectIdx, a published definition). The optimum is a hypothesis for all ; in (5), is . Inequality (5) quantifies over feasible only. Lemmas 5 and 6 are stated for an arbitrary feasible current state, which is stronger than the history-averaged form printed. The paper's range becomes , because at the iteration bound is undefined. A formalization that admits would evaluate it to and claim the bound at , which is false.
The development needs elementary facts about conjugates of scalar functions in EReal (convexity, the Fenchel–Young inequality, the Lipschitz domain bound), the weak duality inequality , and finite averages over coordinate sequences. The conjugate facts and the expectation calculus are reusable by the other two missions of the series. Proofs of individual milestones are welcome independently.
A classifier trained from finitely many examples can perform well on those examples while responding poorly to changes in the feature distribution or to mislabeled observations. Distributionally robust learning addresses this by choosing a classifier against every probability distribution within a specified distance of the empirical distribution. The resulting optimization appears to range over an infinite-dimensional family of distributions. Shafieezadeh-Abadeh, Kuhn, and Mohajerin Esfahani show that, for linear classification with a convex Lipschitz loss, this problem has an exact finite convex reformulation. That result is Theorem 3.11(ii) of the 2019 arXiv preprint, which is the source used here.
The authors' transport metric allows a data point's features to move and its binary label to flip, with separate prices for those two changes. This matters when robustness to inaccurate labels is part of the model. A label-preserving metric cannot express that choice. The paper builds on its Section 2 learning model and the transport duality developed in Appendix A.1; the present mission isolates the classification result and the intermediate statements used for it. The preprint's Corollary 3.14 specializes the result to logloss, while its Corollary 3.12 treats hinge loss. A logloss-specific reformulation and a label-preserving classification result already have proved statements on Prove2Me; the general convex-Lipschitz, finite label-cost theorem remains the target of this mission.
Let be a finite-dimensional real vector space with a chosen norm . Features are and labels are . A linear classifier is a continuous linear functional , with score . Its dual norm is the operator norm induced by . Given training pairs , their empirical distribution is .
For , the transport cost between pairs is
The Wasserstein distance is the least expected transport cost among joint distributions whose two marginals are and . For a radius , the Wasserstein ball contains probability distributions satisfying . The loss is , where is convex and Lipschitz continuous. The Lipschitz modulus is the smallest Lipschitz bound for , defined as the supremum of its difference quotients. These are the objects and standing conventions of Sections 1.1, 2, and 3.2 of the preprint.
The goal is Theorem 3.11(ii): for every fixed , the worst-case expected loss equals the value of program (18),
Taking the infimum of both sides over gives equality between problem (4) and the full program (18). The fixed- identity is stated explicitly because it is the stronger assertion established in the proof. The milestone list follows the paper's appendix: Lemma A.1 converts the robust expectation into a scalar transport-price infimum; the label split isolates the two possible labels; Lemma A.3 evaluates the feature supremum; the ensuing display gives the program in terms of conjugate slopes; and the final identity identifies those slopes with . Each milestone is tied to its printed page in the preprint.
The theorem replaces a search over probability distributions by a finite convex program with one scalar and one slack variable per sample, in addition to the classifier . It makes the price of label changes explicit through and the price of feature changes through . Consequently, different convex Lipschitz classification losses can be treated within the same transport model rather than by deriving a new distributional optimization problem for each loss. The preprint applies the result to hinge, smoothed hinge, and logloss examples in the paragraphs following Theorem 3.11.
The result is proved in the cited paper. Its general statement and the paper's appendix milestones are not yet machine-checked in this mission. A verified development would connect the published definitions of the Wasserstein ball and Lipschitz modulus to an exact program-value theorem that later work can import. The loss-specific proved statements already available on Prove2Me provide useful comparisons, but their narrower losses or label-preserving transport costs do not replace this theorem.
The visible finite constraints contain no probability distributions, while the left-hand side optimizes over all probability measures in a Wasserstein ball. Establishing that the two values coincide requires control of the transport budget and the inner worst-case loss at the same time. The straightforward comparison of feasible values gives only one inequality. It does not show that every improvement allowed by a distribution can be represented by the scalar transport price and the samplewise constraints. The case also needs care: Lemma A.1's strong-duality proof cites a result for strictly positive radius, whereas the theorem itself allows zero radius and states an infimum rather than an attained minimum.
Lean represents by an abstract finite-dimensional real normed space with its Borel measurable structure. This retains the arbitrary norm of in the paper. Labels are Bool, interpreted as and ; the published DRLogReg_Reformulation_Core definition supplies their sign map, the metric, Wasserstein distance, ball, and empirical distribution. The published WassersteinDRO_Duality_lipschitzModulus definition supplies the exact Lipschitz modulus. The mission's own definitions add the general loss, the feasible set of (18), the fixed-classifier program value, and the effective domain of the convex conjugate. The same objects and conventions are used across all milestones.
All potentially infinite robust values are represented in ; the unbounded feature suprema in Lemma A.3 and the label split use extended reals. The standing loss condition comes from the paper's Section 2.1 loss codomain. It also makes the lower Lebesgue integral and the finite program's extended-nonnegative objective faithful. The sample size is positive, , and the goal allows . Lemma A.1 separately assumes , matching the strong-duality condition used on page 29. The printed extra index in the page-35 classification display is carried in its verbatim milestone provenance but not in the Lean statement, because no exists in part (ii). The formalization does not obtain the theorem by restricting to a constant loss, by taking a singleton feature space, or by substituting an arbitrary Lipschitz bound for its modulus. Contributions that establish transport duality, the conjugate-domain slope identity, or the zero-radius case are directly reusable.
A cubic graph has chromatic index 3 or 4 (Vizing). Cubic graphs of chromatic index 4 — the uncolourable ones — are where most of the open problems on cubic graphs live: a minimal counterexample to the cycle double cover conjecture or to Tutte's 5-flow conjecture would be among them. Uncolourable graphs with small edge cuts or short cycles reduce to smaller ones, so attention concentrates on snarks, the uncolourable cubic graphs that are cyclically 4-edge connected and have girth at least 5.
Brinkmann, Goedgebeur, Hägglund and Markström (arXiv:1206.6690v3, J. Combin. Theory Ser. B 103, 2013) generated all snarks on up to 36 vertices and tested a series of published conjectures against them. One of these concerns the 2-factors of a snark, its spanning subgraphs in which every vertex has degree 2. A 3-edge-colouring of a cubic graph gives 2-factors made of even cycles, so a snark is a graph in which some 2-factors are forced to contain odd cycles. At the far end are the snarks in which every 2-factor consists of odd cycles only. Abreu, Labbate and Sheehan (European J. Combin. 33, 2012), studying pseudo and strongly pseudo 2-factor isomorphic graphs, conjectured that this happens only for the Petersen graph, the Blanuša-2 snark and the Flower snarks (paper, p. 11, Conjecture 4.11).
Timeline:
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 an endpoint get different colours, and uncolourable otherwise. The girth is the number of vertices of a shortest cycle. is cyclically -edge connected if deleting fewer than edges never leaves two components that both contain a cycle. A snark is an uncolourable, cyclically 4-edge connected cubic graph with (paper, p. 4).
A 2-factor of is a spanning 2-regular subgraph : it uses every vertex, and every vertex has degree exactly 2 in . Each component of is a cycle. Say that all 2-factors of are odd if every component of every 2-factor of has an odd number of vertices.
The witness is the graph of Appendix 8.1, given in the paper as a list of higher-numbered neighbours of the vertices :
It has 26 vertices and 39 edges. In Lean it is G81 : SimpleGraph (Fin 26) with paper vertex as .
Because has 26 vertices, it is not the Petersen graph (10 vertices), not the Blanuša-2 snark (18) and not a Flower snark ( vertices). The goal therefore refutes Conjecture 4.11 without formalizing the conjecture's list of exceptions.
The goal splits into five properties of the one graph :
A supporting statement, not from the paper, asserts that has a 2-factor, so that milestone 4 is not vacuous.
The result. Conjecture 4.11 would have characterised a natural extremal class of snarks by a short explicit list. The counterexample shows that the class is not that list: there are snarks outside the Petersen, Blanuša-2 and Flower families in which no 2-factor contains an even cycle. Such graphs are relevant to questions about 2-factor structure, oddness and cycle double covers, where the parity of 2-factor cycles is exactly what the arguments track.
Formalizing it. The result is proved in the paper by exhibiting the graph and checking it by computer; it has not been machine-checked in a proof assistant. A formal proof certifies every property of the printed graph — including that the printed adjacency list decodes to a graph with these properties — and leaves a reusable library of definitions (snarks, cyclic edge connectivity, 2-factors) that other snark statements can import.
Each property is a finite check, but some are large. Cubicity and girth are local. Cyclic 4-edge connectivity quantifies over all sets of at most three of the 39 edges (about ten thousand) and needs, for each, a component analysis of the remaining graph. The odd-2-factor property quantifies over all 2-factors; in a cubic graph these are the complements of the perfect matchings, and has 56 perfect matchings. The obvious route — decide over all subgraphs — is out of reach: there are edge subsets, and the statement is phrased through Mathlib's ConnectedComponent and IsRegularOfDegree, which do not evaluate by kernel computation at this size. Uncolourability has the same problem: the naive search space has colourings.
Conventions committed to:
Fin 26, paper vertex = Lean vertex ; adjacency is the symmetric closure of an explicit edge list G81Edges, so it is decidable.G.lineGraph.Colorable 3 (a proper 3-edge-colouring), never G.Colorable 3.egirth : ℕ∞, so "girth at least 5" is 5 ≤ G.egirth.F on the same vertex type with F ≤ G and F.IsRegularOfDegree 2 — spanning by construction. Oddness is per component: Odd (Nat.card c.supp) for every component c. It is not the parity of the whole vertex set (26 is even).S with S.card < k, any two components of G.deleteEdges S that both contain a cycle are equal.The odd-2-factor property is vacuous for a graph without 2-factors. The goal is not trivialised this way: has 2-factors, and a supporting theorem states it.
Out of scope, because they rest on exhaustive computer enumeration: that is the smallest counterexample, that there is exactly one further counterexample on 34 vertices, Observation 4.10 (all snarks on at most 36 vertices have oddness 2), and Tables 4 and 5. The Petersen graph, the Blanuša-2 snark and the Flower snarks are not defined here; the refutation uses only their orders.
Contributions welcome: proofs of any milestone; general lemmas linking 2-factors of cubic graphs to perfect matchings, and 3-edge-colourings to even 2-factors; decision procedures for cyclic edge connectivity of explicit graphs. The definitions are shared in shape with the other missions of this series and are meant to be reused.
Many noncooperative problems in communication networks, power markets and supply chains are stochastic Nash games. Each player minimizes an expected cost that depends on its own decision and on the decisions of its rivals, and the expectation can only be sampled, not evaluated. A natural distributed way to compute an equilibrium is the best-response scheme: each player repeatedly replies optimally to the rivals' current strategies. In a stochastic game an exact best response is itself an expectation-valued optimization problem, so a practical scheme replies inexactly, running a few stochastic gradient steps per reply. Lei, Shanbhag, Pang and Sen (arXiv:1704.04578v2; Mathematics of Operations Research, 2020) analyse three such inexact proximal best-response schemes: synchronous, randomized and asynchronous. For each they prove a linear rate of convergence and a bound on the total number of projected stochastic gradient steps.
This mission concerns the randomized scheme. In large games it is unrealistic for all players to update at every round; in the paper's model each player independently decides to update with probability . This is the game-theoretic analogue of randomized block-coordinate descent (Nesterov 2012; Richtárik–Takáč 2014). A local Poisson clock per player is a special case (Remark 5 of the paper). The synchronous scheme, the paper's Theorem 1, and the asynchronous scheme are separate missions of this series.
There are players. Player chooses in a compact convex set and minimizes
where is a random vector and the oracle returns sampled gradients with (Assumption 1). A Nash equilibrium is a profile in from which no player can lower its cost by deviating alone.
For the proximal best response to a profile is
The matrix has entries and , built from the extreme curvatures and . Assumption 2 is (spectral norm).
Algorithm 2. At major iteration , each player flips an independent coin with , independent of the past information (Assumption 3). If , the player replaces by an inexact proximal best response with
otherwise . The accuracy is tied to the number of updates the player has made so far. The reply is computed by projected stochastic gradient steps
from , where and is the diameter of . The analysis uses the weighted norm and the constants , and .
Let , , , , and , where . After major iterations, is an -NE, i.e. , and for every player
In the order the proof uses them:
Theorem 2 gives an explicit, non-asymptotic sample complexity for computing a Nash equilibrium of a stochastic game when only a random subset of players acts at each round. Its exponent quantifies the price of randomization: Remark 7 of the paper shows it reduces to the synchronous exponent exactly when every . Lemma 5 is the first linear-rate statement for inexact randomized best responses in this setting. The weighted-norm argument of App. A–B is the device that makes block-randomized fixed-point iterations contract.
The results are proved on paper. None of them has a machine-checked proof, and the platform holds no stochastic Nash game, proximal best-response map or randomized best-response scheme. A formal proof checks every constant of (34), including the interplay of the random inexactness with the random number of steps . The paper does not prove (5): it adapts it from Facchinei–Pang 2009. A formal proof of (5) closes that gap.
The conditional-expectation bookkeeping is where a naive argument fails. The accuracy and the step count are random, being functions of the past coins. The coin must be independent of both the past and the samples the player uses in round . The descent step (A.4) multiplies the coin with the inexactness error, and its factorization uses exactly this joint independence. Bounding the expected work requires the moment generating identities (B.3) and (36) of a binomial count, with two different constants (through ) and (through ). Merging them gives a false bound. Lemma 6 is a stochastic approximation estimate conditional on , at a random, -measurable centre . Applying the unconditional bound for strongly convex SGD pointwise is not enough. On the deterministic side, (5) needs a mean-value argument along a segment in the product space, using the mixed Hessian blocks.
Players are Fin N and player 's space is EuclideanSpace ℝ (Fin (n i)). Costs are functions of the whole profile. The Euclidean norm of the vector of block norms and the weighted norm are written out explicitly, since Lean's norm on the product type is the sup norm. is the operator norm on Euclidean . is an infimum of Rayleigh quotients. The proximal best response is any map satisfying the argmin property on . is any map satisfying the published SpectralProjGrad.Shared.IsProjOnto. Randomness lives on a probability space with a filtration , and conditional expectations are Mathlib's condExp.
Statement repairs, all recorded in the items' Formalization Notes:
A formalization in which the coins are almost surely is the synchronous scheme, not this one. Coins and samples here are genuinely random with the stated laws and independence, and the expectation bounding the work is taken over both.
Reusable infrastructure includes the conditional bound for projected SGD on strongly convex problems (Lemma 6), the binomial moment identities (B.3)/(36), and Lemma 2 and (30). Contributions of intermediate lemmas, such as (A.4)–(A.5), (B.2) and the measurability of the iterates, are welcome as separate theorems.
Many equilibrium problems in operations research have the form of a stochastic Nash game: each of players minimizes an expected cost that depends on the strategies of the others, and the expectation can only be sampled. The paper's introduction lists applications in generation-capacity and power markets and in communication networks (Abada, de Maere d'Aertrycke and Smeers, 2017; Başar, 2007). A natural way to compute an equilibrium is a best-response scheme: each player repeatedly re-optimizes against the current strategies of its rivals. In a large network the players cannot synchronize. They update at different times and see their rivals' strategies with delays.
Lei, Shanbhag, Pang and Sen (arXiv:1704.04578v2; Mathematics of Operations Research, 2020) analyze inexact proximal best-response schemes in three regimes: synchronous, randomized and asynchronous. This mission formalizes the asynchronous one (§5 and Appendix C). It adapts the partially asynchronous iterations of Bertsekas and Tsitsiklis (1989) to stochastic games with inexact, sampled best responses, and it gives an explicit bound on the number of stochastic gradient steps each player needs.
Player chooses in a nonempty compact convex set . A profile is . Player 's cost is , which is convex and twice continuously differentiable in a neighbourhood of . A sampling oracle returns , whose second moment is at most (Assumption 1). A Nash equilibrium is a profile in which each minimizes over .
For , the proximal best response of player to a profile is
The curvature constants and define the matrix with and . Assumption 5 (strict diagonal dominance) asks . It makes , the maximum absolute row sum, smaller than one.
The asynchronous scheme (Algorithm 3) runs on a deterministic schedule. At time the players in update. Player sees the outdated profile and computes with
The other players keep their strategies. Assumption 4 requires every player to update at least once in every consecutive times, and every delay to be at most . The accuracy is , where counts player 's updates so far. The inexact response is computed by projected stochastic gradient steps (43), with step size and . Write , and .
Let , , , and
where . After major iterations, , and player has taken at most
projected gradient steps.
In the order the proof uses them:
Theorem 3 makes the cost of asynchrony explicit. Bounded delays and a bounded update window enter only through the rate per window, . The overall effort stays polynomial in , and the paper's Table 1 summarizes the exponent as for a suitable choice of . The result connects classical partially asynchronous fixed-point theory with the sample-complexity analysis of stochastic approximation. Lemma 7 holds for any inexact solver that achieves the accuracy (38), not only for the stochastic gradient loop, so it applies to other subproblem solvers as well.
The paper proves these results by hand. As far as is known, no part of them has been machine-checked: there is no formal treatment of stochastic Nash games, of proximal best-response maps, or of asynchronous iterations with delays in Mathlib or on this platform. A formalization would check the induction over windows in Appendix C, whose index bookkeeping has several printed slips. It would also make precise which properties of the delays the argument needs.
The obvious argument does not carry over from the synchronous case. There, one step of the scheme contracts the whole error vector by in one norm. Here a step updates only some players, and each of them uses information up to steps old. No single step contracts anything. The proof has to show that every window of steps contracts the worst-case expected error by a factor , with the delays absorbed into the root . This requires a nested induction with case distinctions on the window position (Appendix C). The analysis also mixes three layers: a deterministic contraction of the exact best response; conditional expectations, Jensen's inequality and adaptedness for the inexact responses; and an stochastic-approximation bound for the inner loop, which in turn needs strong convexity, the first-order optimality conditions and nonexpansiveness of the projection.
Players are indexed by Fin N. Player 's space is EuclideanSpace ℝ (Fin (n i)), and costs are functions of the whole profile: is f i (Function.update y i z). The projection is any map satisfying the published predicate SpectralProjGrad.Shared.IsProjOnto. The proximal best response is a map constrained by an argmin predicate on . and are Rayleigh-quotient infima and suprema of second Fréchet derivatives, and is the maximum absolute row sum. The probability space carries a filtration to which the iterates are adapted. The inner-loop -algebras are parameters satisfying the inclusions the proof uses. Conditional expectations are Mathlib's condExp.
Statement repairs and implicit hypotheses, each recorded in the item it affects:
The special case , of Theorem 3, Corollary 3 (cyclic updates) and Theorem 4 are not stated.
The goal cannot be met trivially. The schedule is a parameter, not "every player at every step". The sampled gradients may be genuinely random, since the second-moment hypothesis is an inequality. is tied to by its argmin property, and is a Nash equilibrium. Each expectation in a conclusion is of a bounded measurable quantity, so it cannot vanish by non-integrability.
The development needs the following:
The projection and strong-convexity lemmas, and (5) itself, are reusable for the synchronous and randomized missions of this series. Proofs of individual milestones, or of general Mathlib-level facts such as the first-order optimality condition over a convex set, are welcome.
Regularized loss minimization (training a linear predictor with a convex loss and an penalty) covers support vector machines, ridge and logistic regression, and much of classical linear learning. A standard way to solve these problems at scale is dual coordinate ascent: optimize the dual problem one coordinate, i.e. one training example, at a time. Hsieh et al. (ICML 2008) reported that it can outperform stochastic gradient descent when moderately high accuracy is needed. Its theory, however, was unsatisfying (paper, §2): the known linear rates, adapted from Luo and Tseng's analysis of coordinate ascent, have a contraction factor that may be arbitrarily close to (it depends on the smallest nonzero eigenvalue of ), and they bound only the dual sub-optimality, which translates into a much weaker primal guarantee.
Shai Shalev-Shwartz and Tong Zhang (JMLR 14, 2013; arXiv:1209.1873) analysed stochastic dual coordinate ascent (SDCA), in which the coordinate is drawn uniformly at random, and bounded the expected duality gap, hence the primal sub-optimality, with explicit constants. For -smooth losses the bound is linear: iterations. This mission formalizes that result, the paper's Theorem 2.
Timeline:
Let , let be convex, and let . The primal problem is to minimize
The convex conjugate of is . The dual problem is to maximize
and the dual point determines the primal point . Weak duality gives for all , so the duality gap bounds the primal sub-optimality of .
A loss is -smooth if it is differentiable with a -Lipschitz derivative. Procedure SDCA starts from . At iteration it draws uniformly from , independently of the past, chooses to maximize
and sets , . Its outputs are the last iterate, the average with , or a random iterate from the same range. The paper's standing assumptions are , and .
For convex -smooth losses under the standing assumptions, and every ,
and, for ,
for the averaging and the random outputs. The constants are the paper's.
Theorem 2 shows that a stochastic method whose per-iteration cost is a single example converges linearly in the primal objective, through the duality gap, with a condition number that enters additively with rather than multiplicatively. This additive dependence is the benchmark against which later variance-reduced and accelerated methods (SVRG, SAGA, accelerated proximal SDCA, Katyusha) are compared. The duality gap is computable, so the bound also yields a stopping criterion.
The result is proved in the paper. As far as the platform's catalogue shows, no part of it, nor the smoothness/strong-convexity duality for scalar conjugates, has been machine-checked. The mission produces a checked statement of the rate with explicit constants and checked versions of the lemmas reused by the series' other two missions (Lipschitz losses, almost-smooth losses).
The proof is short on paper, but each step crosses between objects that Lean keeps apart. The conjugates are extended-valued: is off a bounded set for many smooth losses (logistic loss), so the dual objective, the coordinate step and the strong-convexity inequality all live in extended reals, and every passage to real arithmetic must be justified by finiteness along the run. The smoothness-to-strong-convexity step (milestone 1) is the classical duality, but Mathlib has no scalar conjugate calculus and no ready statement of it. The expectation is over the coordinate sequence, and the recursion compares expectations over histories of different lengths. The obvious attempt, a deterministic per-sequence bound, fails: the linear rate holds only in expectation.
Data are x : Fin n → EuclideanSpace ℝ (Fin d), φ : Fin n → ℝ → ℝ (convex), lam : ℝ with 0 < lam, and 0 < n. -smoothness is a derivative function φ' with HasDerivAt everywhere and . The conjugate conj and the dual dual are EReal-valued (⨆, never a real sSup). Dual values are converted to reals only under conjuncts asserting their finiteness. The SDCA step is a map Δ : (Fin n → ℝ) → Fin n → ℝ constrained by the argmax predicate IsSDCAStep, which is satisfiable. The run is a fold over an index sequence js : Fin T → Fin n from α⁽⁰⁾ = 0, and is the uniform average over all sequences (the published SAGA.Convex.expectIdx). Indices are 0-based. Lemma 1 and (10) are stated in the conditional one-step form at an arbitrary dual-feasible point, which implies the printed history-averaged form. The goal assumes no dual optimum; milestones 6–7 take a maximizer of as a hypothesis (it exists under the standing assumptions). The random output is stated over the iterates , which is what the proof bounds.
A trivializing formalization is ruled out: no statement takes the step, the conjugate or the expectation as an unconstrained variable, no real-valued toReal absorbs an infinite dual value, and the bounds are stated for the paper's exact iteration counts.
Needed infrastructure: scalar Fenchel conjugates in EReal (Fenchel–Young inequality and equality at subgradients), smooth/strongly convex duality, and averages over finite index sequences. The conjugate facts and the expectation bookkeeping are reusable beyond this mission, by the series' Lipschitz and almost-smooth missions in particular. Proofs of any milestone, and lemmas on EReal conjugates, are welcome.
A snark is a cubic graph that cannot be properly edge-coloured with three colours and that does not reduce to a smaller such graph. Snarks are the smallest possible counterexamples to several central conjectures about cubic graphs, among them the cycle double cover conjecture, Tutte's 5-flow conjecture and the Berge–Fulkerson conjecture, so structural statements about snarks narrow the search for counterexamples to those conjectures.
Permutation graphs are cubic graphs built from two disjoint cycles of equal length joined by a perfect matching, so that the two cycles are induced. The Petersen graph is the classical example: its outer 5-cycle and inner pentagram are joined by five spokes. In his monograph Integer Flows and Cycle Covers of Graphs (1997), C.-Q. Zhang conjectured that the Petersen graph is the only permutation snark that is also cyclically 5-edge connected.
Brinkmann, Goedgebeur, Hägglund and Markström (arXiv:1206.6690v3, J. Combin. Theory Ser. B 103, 2013) built a generator for snarks and enumerated all snarks up to 36 vertices. Among them they found twelve cyclically 5-edge-connected permutation snarks on 34 vertices, which refute Zhang's conjecture (Observation 4.2), and they printed all twelve in Appendix 8.6 of the paper. This mission formalizes the refutation using the first of those graphs.
All graphs are finite and simple. A cycle is a 2-regular connected graph. A graph is cubic if every vertex has degree 3. A 2-factor of is a spanning 2-regular subgraph. The girth is the number of vertices in a shortest cycle of .
A cubic graph is colourable if it has a proper 3-edge-colouring: a map giving distinct colours to distinct edges with a common endpoint. Otherwise it is uncolourable.
A graph is cyclically -edge connected if deleting fewer than edges from never leaves two distinct components that both contain a cycle.
A snark is an uncolourable, cyclically 4-edge connected cubic graph with .
A cubic graph is a permutation graph if it has a 2-factor consisting of two induced cycles. Equivalently, its vertex set splits as with both induced subgraphs and cycles. A permutation snark is a snark that is a permutation graph.
The Petersen graph is the graph on with the outer cycle , the spokes , and the inner pentagram .
Zhang's Conjecture 4.1. Let be a cubic cyclically 5-edge-connected permutation graph. If is a snark, then must be the Petersen graph.
The witness is the first graph in Appendix 8.6 (p. 36). It is given as a list of higher-numbered neighbours of the vertices ; decoded, it has 51 edges. In the Lean development the paper's vertex is i - 1 : Fin 34.
that is, there is a finite cubic, cyclically 5-edge connected permutation snark that is not isomorphic to the Petersen graph. This is SnarkGen.Zhang.observation_4_2.
Each milestone is a property of asserted by the heading of Appendix 8.6, "The 12 cyclically 5-edge connected permutation snarks on 34 vertices":
The goal follows from milestone 7 directly. Two supporting theorems are included: cyclic -edge connectivity is monotone in , and the paper's remark (p. 9) that every permutation snark has order .
Zhang's conjecture predicted that the Petersen graph is isolated among highly connected permutation snarks. Its refutation shows that this is false, and the twelve 34-vertex graphs went on to serve as counterexamples to further conjectures in the same paper (Conjectures 5.17, 5.20 and 5.21, about cycle double covers containing a prescribed 2-factor). They are also listed in the House of Graphs database.
The refutation in the paper is a computer result: the graphs were found by an exhaustive search, and their properties were checked by programs. A formal proof would replace that check with a machine-verified one that is independent of the generator. It would also produce reusable certified tools for finite cubic graphs: a kernel-checked test for uncolourability, cyclic edge connectivity, and girth. No machine-checked proof of any of these properties of is known to exist.
The statements are short, but none of the properties of follows from a general theorem; each must be checked on the specific graph. The obvious approach, to unfold the definitions and let a decision procedure enumerate, does not scale:
The definitions are stated in terms of Mathlib's general notions (line graphs, walks, connected components), not in terms of a computable representation. Connecting them to an efficient computation is the main work.
Graphs are SimpleGraph V with [Fintype V]. The conventions are as follows.
G.lineGraph.Colorable 3, a proper 3-colouring of the line graph. It is not a vertex colouring of .S ⊆ G.edgeSet with S.card < k. Components and cycles are taken in G.deleteEdges S.5 ≤ G.egirth, the extended girth, which is for acyclic graphs.Type and reads "must be the Petersen graph" as Nonempty (H ≃g petersen).The conjecture keeps every printed hypothesis, including the redundant "cubic". Dropping "permutation graph" or "cyclically 5-edge connected" would make the refutation easier, since other cyclically 5-edge-connected snarks are known. The cyclic connectivity must be computed in the graph after deletion and must require both components to contain a cycle; otherwise it degenerates into ordinary edge connectivity, which is at most 3 for cubic graphs and would make the conjecture vacuous.
Proofs should be checked by the Lean kernel. The decision procedures for colourability and cyclic connectivity are the reusable part of this mission, and contributions that build them for arbitrary finite cubic graphs are welcome.
Out of scope.
The lost-sales inventory model with a positive lead time is one of the basic models of inventory theory. A retailer reviews stock once per period, places an order that arrives periods later, and loses (rather than backlogs) any demand that cannot be met from stock on hand. Lost sales are the norm in retail, where a customer facing an empty shelf buys elsewhere. The optimal policy is the solution of a dynamic program whose state is the on-hand inventory together with the whole pipeline of outstanding orders. The state dimension therefore grows with the lead time, and computing the optimal policy is intractable beyond small : for a lead time of four and geometric demand the dynamic program already has 228,581 states (Zipkin 2008a, Operations Research 56(5), 1256–1263).
Heuristics (base-stock, myopic, cost-balancing) have been studied at length. Reiman (2004) analyzed an open-loop policy that orders one unit at fixed intervals in a continuous-review lost-sales model with Poisson demand. Zipkin (2008a) observed numerically that ordering the same constant amount every period performs well already at lead time four. Huh, Janakiraman, Muckstadt and Rusmevichientong (2009) proved that order-up-to policies are asymptotically optimal as the lost-sales penalty grows. Goldberg, Katz-Rogozhnikov, Lu, Sharma and Squillante proved that a constant-order policy is asymptotically optimal as the lead time grows, with an explicit threshold. This mission formalizes that result, Theorem 1 of their paper.
Fix a holding cost per unit left over at the end of a period, a lost-demand penalty per unit of unmet demand, a lead time , and a horizon . Demands are i.i.d. with a law on that has a finite third moment and is not deterministic. At the start of period the system holds inventory and a pipeline of outstanding orders. First arrives; then an order is placed and joins the end of the pipeline; then is realized, and
The system starts empty. A policy chooses each order from the information available before the period's demand, possibly with randomization. Problem (1) is
For let , the steady-state waiting time of a GI/D/1 queue. For the constant-order policy orders the random amount (drawn independently of the demands) in the first period and in every later period. The best constant is (the smallest minimizer). With the quantile of , , the standard deviation and the skewness of , set and
For all , and ,
The milestones follow the paper's argument in its order:
The theorem says that the policy which ignores the state entirely, ordering the same amount every period after a single randomized first order, loses at most a factor against the optimal policy once the lead time exceeds an explicit threshold. The threshold depends only on , and the demand law. Optimal policies are out of computational reach precisely when is large, so this is the first guarantee of near-optimality whose computation does not grow with the lead time. The paper's Corollary 2 (the ratio tends to as ) follows directly.
The result is proved in the paper (up to the correction below); this platform holds no formalization of it or of its lemmas. A formalization would produce reusable statements about suprema of random walks with negative drift (Lemma 9, (26)), a quantitative central limit theorem for Lipschitz test functions (Theorem 11), and the finite-horizon lost-sales problem built on the published model of this platform.
The obvious comparison fails. An optimal policy may vary its orders arbitrarily over time, so its pipeline need not look like a constant stream. Comparing it period by period with gives nothing, because the inventory of is driven by an unbounded random-walk supremum.
The paper instead bounds the optimal cost over any consecutive periods by the cost from the most favourable state. It then has to show that the average of that state's pipeline stays bounded away from uniformly in . This last step is the crux. The components of may vary considerably over the window, and a qualitative central limit theorem is not enough: the argument needs an explicit rate (Theorem 11) with constants that survive summation over windows. On the probabilistic side, the expectations of random indices at which random walks attain their maxima are not adapted to the demand filtration. They are controlled only through the distributional identity of Lemma 9 and the geometric tail (26).
The model is the published CappedBaseStock_Model. Its parameter record supplies , and the penalty (field p; the record is called prm). Its demand law supplies a probability law on with finite positive mean. The finite third moment and non-determinism are explicit hypotheses. and are the published newsvendorLevel and backorderCost. The conventions:
A correction. As printed, the second term of (p. 5) and of Corollary 12 (p. 14) lack a factor . The proof of Corollary 12 establishes , and the printed bounds are not invariant under rescaling the demand. Both are stated here with the factor restored, and each item's note says so.
Neither a long-run average cost nor a restricted comparator (stationary, Markov, or bounded-order) may replace the finite-horizon OPT. The demand law may not be specialized, and may not order in its first period: each change makes the goal a different, easier theorem.
A complete development needs Lindley-type recursions and the stationarity of the GI/D/1 waiting time, Chernoff and moment bounds for random-walk maxima, a Stein-method CLT rate, and the existence of optimal policies for a finite-horizon problem with a continuous state. The random-walk and CLT parts are independent of inventory theory and reusable. Proofs of any milestone are welcome, as are alternative proofs of the goal.
The scalar Bernstein and Bennett inequalities bound the upper tail of a sum of independent, zero-mean random variables that are bounded above: the tail is governed by the total variance at moderate deviations and by the uniform bound in the far tail. Many questions in randomized numerical linear algebra, matrix completion, covariance estimation, graph sparsification and statistical learning reduce to the same question for a sum of independent random matrices, where the quantity of interest is the largest eigenvalue or the spectral norm of the sum rather than a scalar.
Ahlswede and Winter (2002) introduced a matrix Laplace transform method based on the Golden–Thompson inequality. Oliveira (2010) and Gross (2011) proved matrix Bernstein-type bounds with this method. Tropp (arXiv:1004.4389, Found. Comput. Math. 12 (2012)) replaced the Golden–Thompson step with Lieb's concavity theorem, obtaining a master tail bound for independent sums (Theorem 3.6) from which matrix Bennett and Bernstein inequalities follow with the variance parameter , the natural analogue of the scalar variance. This mission formalizes §6 of that paper.
Timeline:
All matrices are complex matrices with . For a self-adjoint (Hermitian) matrix , is its largest eigenvalue and its spectral norm. The semidefinite order means that is positive semidefinite. Functions of a self-adjoint matrix are defined spectrally: if , then ; this gives the matrix exponential and, on positive-definite matrices, the matrix logarithm . The trace is .
A random matrix is a measurable map on a probability space ; its expectation is taken entrywise. A finite sequence of random self-adjoint matrices is independent if the maps are mutually independent.
The setting of the goal: are independent random self-adjoint matrices with
and the total variance is . Bennett's function is for .
For every , the following chain holds:
and the last term is at most for and at most for . The first inequality is the matrix Bennett inequality, the second the matrix Bernstein inequality, and the case split the split Bernstein inequality.
Lemma 6.8 (the matrix mgf bound under ) and Theorem 6.2 (matrix Bernstein, subexponential case: , split as and ) are included as further theorems.
Matrix Bernstein is the most used inequality of the paper: it bounds the spectral norm of a sum of independent bounded random matrices with only a logarithmic dimensional factor, and it is the standard tool behind sampling bounds for matrix completion, randomized low-rank approximation, spectral sparsification, covariance estimation and the analysis of random features. Theorem 6.1 assumes only an upper bound on the largest eigenvalue of each summand, so it applies to summands with unbounded smallest eigenvalues; applied to and separately it controls both tails.
The results are proved in the paper. As far as the local catalog shows, no machine-checked proof of the matrix Bennett or Bernstein inequality for complex Hermitian matrices exists; the platform has a matrix Bernstein statement for real symmetric matrices in a different form (Wainwright, Theorem 6.17), still open, and scalar Bennett and Bernstein inequalities. Formalizing Theorem 6.1 produces a reusable matrix concentration inequality together with its two ingredients, the matrix mgf bound of Lemma 6.7 and the scalar inequality relating Bennett's and Bernstein's exponents.
The scalar argument multiplies moment generating functions of independent summands. For matrices, unless and commute, so does not factor; the master bound of Theorem 3.6 rests on Lieb's concavity theorem for , which is not in Mathlib. The mgf bound of Lemma 6.7 needs a semidefinite comparison between functions of a random matrix, the transfer rule on the spectrum , and the operator monotonicity of the logarithm. The remaining steps (optimizing over , the inequality between and the Bernstein exponent) are real analysis.
Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; is the supremum of the real spectrum; is the operator norm on ; and are Mathlib's continuous functional calculus cfc; the semidefinite order is Mathlib's MatrixOrder; expectation is entrywise. A random matrix is a measurable map, each is Hermitian at every , independence is iIndepFun, and the measure is a probability measure. The bound is assumed almost surely; no lower bound on the eigenvalues is assumed. The paper's standing regularity (§2.2) is made explicit as integrability of the entries of and (and of where its expectation is taken). The infimum over in Theorem 3.6 and Corollary 3.7 is stated for every admissible .
The printed formulas divide by and , so and are hypotheses of Theorems 6.1 and 6.2; with Lean's convention , the case would turn the Bennett bound into the trivial value , so the statement is not allowed to degenerate there. The chain is a conjunction of the probability bound and the inequalities between consecutive bounds, so the weaker reading "the probability is below each bound" does not satisfy it.
A complete development needs the matrix Laplace transform method, Lieb's theorem (or a substitute), operator monotonicity of the logarithm, the transfer rule for the functional calculus, and the scalar inequality . The first four are reusable for every matrix concentration inequality of this paper and beyond. Contributions to any milestone are welcome.
Regularized loss minimization over linear predictors is the training problem behind support vector machines, logistic regression, ridge regression and their many variants. Given examples , one minimizes an average of convex losses of the predictions plus a quadratic penalty. Dual coordinate ascent (DCA) solves the Fenchel dual of this problem by optimizing one dual variable at a time; it has been the workhorse of linear SVM solvers such as LIBLINEAR (Hsieh et al., ICML 2008). Before Shalev-Shwartz and Zhang's work, the available analyses of DCA either gave linear rates with constants depending on unknown problem quantities or did not control the duality gap, which is the quantity a practitioner can actually monitor as a stopping criterion.
Shalev-Shwartz and Zhang (2013) analysed stochastic dual coordinate ascent (SDCA), where the coordinate is picked uniformly at random, and proved explicit bounds on the expected duality gap. For Lipschitz losses (hinge loss, absolute loss) the bound is iterations, which matches stochastic gradient descent when the accuracy is low and improves on it when is small compared with . This mission formalizes that result, Theorem 1 of the paper, together with the lemmas of its proof.
Timeline. Hsieh, Chang, Lin, Keerthi and Sundararajan (2008) proposed dual coordinate descent for linear SVMs and proved linear convergence with an unspecified constant. Shalev-Shwartz and Zhang (arXiv 2012, JMLR 2013) gave the first explicit duality-gap rates for SDCA, for Lipschitz and for smooth losses. Proximal and accelerated variants followed (Shalev-Shwartz and Zhang, Math. Program. 2016).
Fix examples (Euclidean norm), convex losses and a regularization parameter . The primal problem (1) is to minimize
The convex conjugate of a scalar function is . The dual problem (2) is to maximize, over ,
Weak duality gives for all , so the duality gap bounds the primal sub-optimality of .
A loss is -Lipschitz if for all . The paper's standing assumptions are , and .
Procedure SDCA starts from . At iteration it picks a coordinate uniformly at random, chooses maximizing
and sets and . The averaging option outputs and . Let maximize and write for the dual sub-optimality.
For convex -Lipschitz losses under the standing assumptions, if and
then
The constants and are the paper's.
In the order the proof uses them: the one-coordinate increase (10); the identity ; Lemma 1 (expected dual increase at least times the gap minus ); Lemma 2 (, ); Lemma 3 ( outside ); Lemma 4 (); the recursion after (13); the rate (14), ; and the averaged duality-gap bound of p. 16.
Theorem 1 makes the duality gap of SDCA a certified stopping criterion with an explicit iteration count. Because the gap upper-bounds the primal sub-optimality, it also gives a primal guarantee for the averaged output . It covers non-smooth losses, the hinge loss in particular, where linear rates are not available. The analysis pattern, a lower bound on the expected dual increase by the duality gap (Lemma 1) followed by a recursion for the dual sub-optimality, was reused in the analyses of proximal, accelerated and mini-batch dual methods.
The result is proved in the paper; to the best of current knowledge it has no machine-checked proof. The mission produces a formal account of the primal–dual pair of regularized loss minimization with extended-real conjugates, a formal SDCA run with uniformly random coordinates, and the complete chain of lemmas. Lemma 1 is stated with a general strong-convexity modulus , as in the paper, so it serves the smooth-loss analysis as well.
The obvious first idea is to treat SDCA as stochastic coordinate ascent on a concave function and import a standard rate. That fails: is neither smooth nor strongly concave for Lipschitz losses, and its domain is a box, so the per-coordinate progress cannot be bounded by a gradient norm. The argument instead compares the exact coordinate maximizer with an explicit interpolation towards a sub-gradient, which needs the conjugate's value at a sub-gradient (Fenchel–Young equality) and its infinite values outside .
The rate (14) is not a plain geometric recursion. It needs a burn-in phase and then an induction with a step size that changes with , and the duality gap of the output has to be recovered from the dual progress by Jensen's inequality over the averaged iterates. Everything happens in expectation over the coordinate sequence, while the dual values have to be kept finite along every run.
Lean conventions:
EuclideanSpace ℝ (Fin d), examples and losses are indexed by Fin n, and is inner ℝ w x.EReal supremum, and is EReal-valued. Real values of are used only where the same statement asserts that they are finite.Δ : (Fin n → ℝ) → Fin n → ℝ constrained by an arg-max predicate (IsSDCAStep). Any maximizer is admissible, and one exists for convex real losses.js : Fin T → Fin n, started at , with .SAGA.Convex.expectIdx, a published definition).A real-valued conjugate, which returns where the supremum is infinite, or an unconstrained step map would make the statements false or vacuous. The EReal conjugate and the arg-max predicate rule both out.
Infrastructure needed: Fenchel–Young for scalar convex functions, the existence of sub-gradients of convex real functions and their bound by the Lipschitz constant, Jensen's inequality for the convex and the concave , and the algebra of uniform averages over . The conjugate and sub-differential definitions and the duality-gap identity can be reused beyond this mission. Proofs of any milestone are welcome, as are lemmas on EReal sums that keep the finiteness bookkeeping short.
Many equilibrium problems in operations research, such as networked Cournot competition, power markets and communication networks, are stochastic Nash games: each player minimizes an expected cost that depends on the rivals' strategies and on a random vector whose law is accessible only through samples. Best-response schemes, in which every player in turn solves its own optimization problem given the others' latest strategies, are the natural distributed method for such games. In the stochastic setting no player can compute an exact best response, because evaluating requires the expectation itself. Lei, Shanbhag, Pang and Sen (arXiv:1704.04578v2; Mathematics of Operations Research, 2020) analyze inexact proximal best-response schemes in which each best response is approximated by a finite number of stochastic gradient steps, and they ask how many sampled gradients each player needs to reach an approximate equilibrium.
The deterministic theory of proximal best responses, including the contraction matrix used here, is due to Facchinei and Pang (Nash equilibria: the variational approach, 2009, §12.6; reference [19] of the paper). The present mission covers the paper's first scheme, the synchronous one, in which all players update simultaneously.
There are players. Player chooses from a closed, compact, convex, nonempty set ; a profile is , and is the profile with its -th block replaced by . A Nash equilibrium is a profile such that every minimizes over .
Assumption 1 asks that each be convex in and twice continuously differentiable near , that the sampled gradients be unbiased for , and that . For the proximal best response is
The matrix has entries and , where is the least eigenvalue of over and the largest spectral norm of the mixed block over . Assumption 2 is (spectral norm).
Algorithm 1 starts from a deterministic . At major iteration every player computes with , by running projected stochastic gradient steps
and setting . A random profile is an -NE if .
With , , , , , , and , the iterate after major iterations is an -NE, and player uses at most
projected stochastic gradient steps. The goal fixes the paper's explicit expression, not its summary.
Theorem 1(a) shows that the synchronous inexact scheme keeps the linear rate of the exact best-response iteration, with factor arbitrarily close to , and turns it into a sample complexity explicit in , in the number of players and in the game's constants. Choosing gives a bound of order for any (Theorem 1(b)), close to the of a single stochastic convex program; the dependence on is mild, which matters for games with many players. The same building blocks (the contraction (5), Lemma 2, Lemma 3 and (30)) are reused by the randomized and asynchronous schemes of the same paper.
The result is proved in the paper; it has not been machine-checked. A formalization adds a verified proof of the complexity bound together with fully explicit hypotheses: several conditions that the paper leaves implicit or states imprecisely (listed under Formalization scope) are made exact, and the Lean statement records which version of each is used.
The arithmetic of Theorem 1(a) from Proposition 4, Lemma 3 and (30) is routine. The weight lies elsewhere. The contraction (5) is quoted from Facchinei–Pang and not proved in the paper; it needs the variational optimality conditions of the two proximal problems and a mean-value argument along a segment of for the partial gradient, which mixes the Hessian blocks and . Lemma 3 is a conditional-expectation argument about a stochastic approximation recursion: the iterate must be shown measurable for the nested -fields generated by the samples, and the conditional unbiasedness and moment hypotheses must be combined with the tower property and the projection's nonexpansiveness. Proposition 4 then needs conditional Jensen to pass from (8) to the Euclidean norm of block errors.
Players are Fin N, player 's space is EuclideanSpace ℝ (Fin (n i)), profiles are dependent functions, and is Function.update y i z. The Euclidean norm of the vector of block distances is written out (blockDist), since Mathlib's norm on profiles is the sup norm; is the operator norm of Matrix.toEuclideanCLM Γ. and are the infimum and supremum of Rayleigh-type quotients of the second derivative over and unit vectors. The proximal BR is any map minimizing the proximal objective on (unique there), and is any map satisfying the published SpectralProjGrad.Shared.IsProjOnto. The -fields and are generated by the samples. Every expectation carries an integrability hypothesis.
Statement repairs, each recorded in the item's Formalization Note:
The goal is not trivialized by deterministic gradients: the sampled gradients are random, constrained only by conditional unbiasedness and a conditional second-moment bound, the proximal BR is tied to by its argmin property, must be a Nash equilibrium, and the norms are Euclidean. A deterministic instance (, on a ball, exact gradients) satisfies every hypothesis jointly.
Needed infrastructure: optimality conditions for constrained strongly convex minimization, the mean-value inequality for partial gradients of functions on convex sets, conditional expectation of vector-valued functions with the tower property and conditional Jensen, and the nonexpansiveness of Euclidean projection. The contraction (5) and Lemma 3 are reusable beyond this mission. Proofs of any milestone are welcome.
A matrix Gaussian series , a sum of fixed self-adjoint matrices each multiplied by an independent standard normal variable, is the simplest sum of independent random matrices. It already appears in the analysis of random designs, in compressed sensing, in randomized numerical linear algebra and in quantum information, wherever one needs to know how large the spectrum of a random linear combination of matrices can be. Its Rademacher analogue , with random signs, plays the same role in symmetrization arguments.
For real coefficients the answer is classical: is normal with variance , so its upper tail is at most . Tropp's paper (arXiv:1004.4389v7) shows that the same bound holds for the largest eigenvalue of a matrix series, with an explicit dimensional factor and with the variance parameter .
Timeline. Noncommutative Khintchine inequalities (Lust-Piquard 1986; Lust-Piquard and Pisier 1991) control the moments of matrix Rademacher and Gaussian series and imply tail bounds of this type. Ahlswede and Winter (2002, arXiv:quant-ph/0012127) introduced the matrix Laplace transform method, whose bounds depend on the sum of the norms . Oliveira (2010, arXiv:1004.3821) obtained bounds of the same form as Theorem 4.1. Tropp (2012) derived the result from a master inequality built on Lieb's concavity theorem (1973), which produces the norm of the sum, , as variance parameter. The paper itself notes that Theorem 4.1 and Corollary 4.2 are not new results; the contribution is the route through the master bound.
Fix a dimension . Matrices are complex arrays; a matrix is self-adjoint if it equals its conjugate transpose. For a self-adjoint , is its largest eigenvalue, and is the spectral norm, the operator norm on with the Euclidean norm. Functions of a self-adjoint matrix are defined through its eigen-decomposition: , (for positive-definite ), . The semidefinite order means that is positive semidefinite.
A random matrix is a measurable map from a probability space into the complex matrices; its expectation is taken entry by entry. A Rademacher variable takes the values with probability each; a standard normal variable has law .
The data of the mission are fixed self-adjoint matrices and independent scalar variables , all standard normal or all Rademacher. The variance parameter is
For all ,
For fixed matrices and ,
The result. Theorem 4.1 is the template for every inequality in the paper: a scalar tail bound carried over to matrices at the cost of a factor , with a variance parameter that is the norm of a sum rather than a sum of norms. The difference matters: can exceed by a factor of , and §4 of the paper shows that both the variance parameter and the dimensional factor in (4.3) are needed in general. Corollary 4.2 transfers the bound to the largest singular value of a rectangular series, which covers Gaussian matrices with nonuniform variances (§4.3).
Formalizing it. The theorem is proved in the paper; the work here is to formalize that proof. The milestones are reusable beyond this mission: Theorem 3.6 and Corollary 3.7 are the common entry point of the Chernoff, Bernstein and Azuma missions of this series, and the Rademacher half of Lemma 4.3 is used again in the matrix Azuma mission. No machine-checked proof of these matrix inequalities was found in Mathlib or on the platform when this mission was drafted.
The scalar argument bounds by the product of the individual mgfs, using . For matrices this identity fails when the summands do not commute, and the trace inequality that replaces it for two matrices (Golden–Thompson) has no analogue for three or more. Controlling the trace mgf of a sum of many noncommuting independent matrices therefore requires a genuinely matrix-analytic input with no scalar counterpart; the naive product bound is not available. A second difficulty is infrastructural: matrix functions, the semidefinite order and expectations of random matrices must be combined in a single setting.
Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; self-adjointness is IsHermitian; , , are Mathlib's continuous functional calculus cfc; is Mathlib's Loewner order under MatrixOrder; is the supremum of the real spectrum; is the operator norm on . Expectation is entrywise, and the paper's standing regularity assumption is made explicit as entrywise integrability of every matrix whose expectation is taken. The infimum over is stated pointwise: the bound is asserted for every at which the mgfs exist, which is equivalent to the infimum form. Independence is iIndepFun of the scalar variables, and "Gaussian or Rademacher" is the disjunction of two hypotheses, never a mixture of laws.
The variance parameter is the norm of the sum ; a formalization with , with a constant different from , or with the dimensional factor omitted is a different theorem. At , Lean's division by zero makes the bound the trivial ; this is the only degenerate case and it is valid.
The development needs: the spectral calculus for Hermitian matrices, monotonicity of the trace exponential, operator monotonicity of the matrix logarithm, Lieb's theorem, and moments of the Gaussian. These are reusable well beyond this paper; proofs of the milestones, of supporting matrix-analysis lemmas, and alternative routes (for instance through noncommutative Khintchine inequalities) are all welcome.
Sums of independent random matrices appear wherever a large matrix is built from random pieces: sample covariance matrices in statistics, random sparsification and sampling in numerical linear algebra, random graphs and their Laplacians, and compressed sensing. The basic question is how far the largest eigenvalue of such a sum can stray above its typical value. For sums of independent real random variables the answer is given by the classical inequalities of Chernoff, Hoeffding and Bernstein, all derived by the Laplace transform method: bound the tail by the moment generating function, and use independence to factor the moment generating function of the sum.
Ahlswede and Winter (2002) showed that a matrix analogue of the Laplace transform method exists, and Oliveira (2010) refined the starting inequality. Tropp's paper (arXiv:1004.4389) replaced the Ahlswede–Winter decoupling step by a consequence of Lieb's concavity theorem (Lieb 1973) and obtained a single master tail bound from which matrix versions of the Gaussian-series, Chernoff, Bernstein and Azuma inequalities follow with sharp variance parameters. This mission formalizes that master bound, the first of five missions covering the paper.
Timeline:
All matrices are arrays of complex numbers with . A matrix is self-adjoint (Hermitian) when ; it then has real eigenvalues, and denotes the largest one. For a function and a self-adjoint with unitary and diagonal, . This defines the matrix exponential of every self-adjoint matrix and the matrix logarithm of every positive-definite matrix, with . The trace exponential is .
A random self-adjoint matrix is a measurable map from a probability space to the self-adjoint matrices. Its expectation is the matrix of the expectations of its entries. A finite sequence is independent when the maps are jointly independent. The matrix moment generating function and matrix cumulant generating function of are
which may fail to exist for some . In the Lean development these objects are lambdaMax, mexp, mlog, trExp and mean in the namespace MatrixTail.Master.
For independent random self-adjoint matrices and every ,
It contains no constants and no assumption beyond independence: every later inequality of the paper specializes it.
The master bound reduces every tail estimate for of an independent sum to semidefinite bounds on the individual cumulant generating functions. The paper's matrix Gaussian and Rademacher series bound, matrix Chernoff inequality and matrix Bernstein inequality are each one such bound away from it, and the matrix Bernstein inequality in particular is a standard tool in randomized numerical linear algebra, matrix completion and covariance estimation. Missions II–IV of this series take the master bound as their first milestone.
All results here are proved in the literature. What remains is formalization: none of Lieb's concavity theorem, the matrix Laplace transform bound or the subadditivity of matrix cumulant generating functions is in Mathlib, and a machine-checked Lieb theorem would be reusable throughout quantum information theory (strong subadditivity of entropy, joint convexity of relative entropy).
The scalar argument factors , which needs . For non-commuting matrices , so this step fails. The Golden–Thompson inequality handles two summands but its three-matrix analogue is false, so it does not iterate. Lieb's concavity theorem is the deep input; it does not follow from elementary properties of the exponential, which is neither operator monotone nor operator convex. On the formal side, the matrix functional calculus of Mathlib carries little of the trace-function theory the statements rely on.
Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d] wherever appears; for the largest eigenvalue would be and the bound would fail at . Exponential and logarithm are Mathlib's continuous functional calculus cfc. Random matrices are measurable maps for the Borel σ-algebra on the entries, independence is iIndepFun, and P is a probability measure. Expectation is entrywise.
The paper's standing assumption that expectations exist is made explicit and only where an expectation is taken: every entry of is integrable for the in question. The infimum over is stated as the bound for every at which the moment generating functions exist; since an inequality is equivalent to for every , and the paper treats a non-existent moment generating function as , this is exact. A real-valued infimum over , or dropping the integrability hypotheses, would make the statements trivially true through Lean's default values ( of an unbounded set and the integral of a non-integrable function are ); the formalization rules both out.
Useful infrastructure beyond this mission: trace inequalities for cfc on Hermitian matrices, monotonicity of the trace exponential in the semidefinite order, and Lieb's concavity theorem itself. Contributions of any of these as standalone lemmas are welcome.