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?
An online learning algorithm chooses a decision before seeing each round's data and is judged by regret: how much more loss it incurs than a fixed decision chosen in hindsight. Statistical learning asks a different question. After seeing data drawn from a distribution, how small is the decision's expected loss on another draw? Chapter 3 of Orabona's textbook connects these settings. It shows that a deterministic online rule with a pathwise regret guarantee also controls expected loss when its input data are independent samples. The chapter's high-probability result is the target here.
The distinction matters when an online guarantee is already available. A regret theorem holds for every loss sequence, including adversarial sequences, yet it does not by itself state what a learner achieves on future data from a distribution. The conversion supplies that statistical reading. It applies to the sequence of predictions produced along one sample path, with no need to select an empirical-risk minimizer from the full decision set. Chapter 3 also studies finite-set validation, in which a separate sample selects one candidate from a fixed collection Orabona, Chapter 3.
The decision set is a subset of Euclidean space . A data point belongs to a measurable space and is drawn according to a probability distribution . The loss lies in for every and , and is measurable as a function of when is fixed. Its true risk is . For a sample drawn independently from , round presents the loss function .
A deterministic online algorithm produces predictions in . Its prediction uses only . For a fixed competitor , its regret is . A proposed regret bound is required to hold on every sample path and for every competitor . The risk comparison uses a minimizer of the full expression , whose existence the theorem assumes.
The goal is Theorem 3.10, with and :
The minimum includes both risk and normalized regret. The theorem controls the average risk of the produced predictions; it does not require to be convex or claim the risk of their average decision. This makes the result applicable to decision sets and losses beyond the convex setting of the chapter's expectation result.
The first milestone is the two-sided bounded-martingale inequality of Theorem 3.9. A second milestone is the displayed concentration estimate in the proof of Theorem 3.10, which compares average true risk with average observed loss for the adaptive predictions. The final milestone is Theorem 3.17: if a fixed nonempty finite set is evaluated on fresh data and minimizes its empirical risk, then
with probability at least Orabona, pp. 27–32.
The goal gives a direct way to read an online regret certificate as a distributional risk certificate. The bound retains the competitor-dependent function inside the minimization: a decision with slightly larger risk but substantially smaller regret bound may give the better guarantee. Its deviation term has the exact constant and confidence dependence stated in the textbook. The finite-set theorem supplies a distinct validation guarantee for choosing one candidate from a fixed collection; it applies even when the risk is not convex.
Formalizing these results adds the probability layer absent from a deterministic regret statement: independent samples, a prediction rule constrained by past observations, true risk as an integral, and probability events for the adaptive sequence. Related online-to-batch statements already exist in the platform's developments of Hazan's online convex optimization text and Mohri, Rostamizadeh and Talwalkar's Foundations of Machine Learning. They use different algorithm and loss models and do not state this competitor-dependent bound. The present mission records the precise Chapter 3 formulation as an open formal proof target; the local Lean statements compile, but their proofs are not supplied.
The observed loss uses a prediction chosen from earlier observations, while the event in the goal concerns its expected loss . Treating the predictions as fixed would ignore their dependence on the sample history. Allowing a prediction to inspect the current sample would break the comparison. The required concentration statement therefore has to retain the exact information available at each round. The comparator in the final bound is fixed before the samples are observed, while the online predictions remain sample dependent Orabona, proof of Theorem 3.10.
For the finite-set result, the selected predictor depends on the validation sample. A concentration estimate for a single fixed predictor does not immediately give the asserted guarantee for that selected predictor. The finite set must remain fixed before sampling, and the statement must account for every possible selected member.
The Lean decision space is EuclideanSpace ℝ (Fin d). Samples are functions under the infinite product measure of ; their values at index zero are unused. The algorithm is a function of the full sample path constrained by a non-anticipation predicate: changing samples from round onward cannot change . Regret is against a fixed , with sums over rounds . The pathwise regret guarantee quantifies over every sample path, so it cannot be replaced by an expected-regret assumption.
The integral defining is used with the book's measurable losses on , avoiding an undefined-integral convention. Measurability of each prediction, realized loss, and realized risk is stated explicitly where a probability event uses them. These regularity conditions make the probability statements meaningful and are the only extra conditions beyond the textbook's mathematical setup. A minimizer represents the assumed minimum in Theorem 3.10. The finite-set minimum is a real infimum whose input is nonempty, finite, and bounded. The positive horizon guards division by ; guards the logarithms. In Theorem 3.9, and make its printed tail formula valid, including at the threshold boundary.
A complete development needs Mathlib's infinite product measure, filtration and martingale interfaces, conditional expectation or conditional moment bounds, and the sub-Gaussian concentration library. The risk, regret, non-anticipation, and empirical-risk definitions can be reused for later stochastic learning results. Contributions that establish the concentration milestone, connect it to the regret identity, or prove the finite-set validation statement all fit this scope.
Coordinate descent changes one component of a parameter vector at a time. This matters when evaluating or updating a single component is cheaper than handling the full vector, for example in problems with sparse features. The coordinate chosen at each step can be random or selected from the current gradient. Karimi, Nutini, and Schmidt study these choices for objectives that satisfy a Polyak–Łojasiewicz (PL) inequality, a condition that controls objective error by the size of the gradient without assuming convexity. Their Theorem 3 gives an explicit expected rate for uniform random coordinates, while §3.2 gives a rate for the greedy Gauss–Southwell choice. Karimi, Nutini, and Schmidt (2016), §3
The question is how much of the familiar full-gradient linear rate survives when an update sees only one coordinate. The theorem answers this with a dimension factor: each uniform draw accesses one of coordinates, and the rate depends on . The same paper relates the greedy rule to earlier work on coordinate descent and boosting; this mission treats its stated greedy rate as a companion result, using the same coordinate update. Karimi, Nutini, and Schmidt (2016), §§3.1–3.2
Let , and let be differentiable. Write for coordinate of its gradient and for the corresponding standard basis vector. The paper's coordinate-wise upper bound (5), with , is
Here ranges over the coordinates. The bound concerns motion along one coordinate. It is the exact smoothness condition used in Theorem 3. Let be a global minimizer and put ; thus the solution set is nonempty and is an attained optimal value. The PL inequality (3) with says
The randomized coordinate-descent step (6) draws uniformly from the coordinates, independently at each time, and sets . The initial point is arbitrary. For draws, expectation means the average over all words , each assigned weight . In particular, at the empty word has weight one and the iterate is .
The Gauss–Southwell rule instead chooses a coordinate with the largest ; ties may be resolved in any way. Its rate uses a PL inequality in the maximum-coordinate norm, , with constant . Karimi, Nutini, and Schmidt (2016), pp. 5–6
For every , the goal is the paper's expected suboptimality bound
The target includes the specific update (6), the coordinate condition (5), and the PL inequality (3). The three milestones are the paper's displayed one-coordinate decrease, its uniform expected decrease involving , and the resulting conditional expected gap contraction. They are indexed to the proof of Theorem 3 on page 5. Karimi, Nutini, and Schmidt (2016), Theorem 3 and proof
The companion target is the rate stated in §3.2 when the maximum-norm PL inequality holds:
This bound applies to any run that chooses a maximizing coordinate at every step. The different PL modulus is part of the statement; it need not equal the modulus in Theorem 3. Karimi, Nutini, and Schmidt (2016), §3.2
Theorem 3 gives a quantitative guarantee for a method that reads one gradient component per update. The guarantee depends on the attained optimum, the coordinate smoothness constant, the PL modulus, and the number of coordinates. It applies to objectives satisfying PL even when convexity is unavailable. The companion result records how the stated rate changes when the coordinate is selected by the largest gradient component and the PL condition is measured in the corresponding dual norm. Karimi, Nutini, and Schmidt (2016), §3
The paper proves these claims, but this mission asks for machine-checked proofs of their exact hypotheses and constants. A complete development will make the finite random experiment explicit and give reusable definitions for coordinate updates and expectations of finite coordinate-choice histories. The PL predicate is already published in the theorem library; the coordinate model and the results here remain to be formalized.
A bound for a single coordinate update depends on one component of the gradient. An arbitrary coordinate can have a zero component even when the full gradient is large, so a pointwise decrease with the full gradient norm cannot be asserted for every choice. The theorem instead concerns the expectation over a uniform choice and then over the complete history of choices. The main formal difficulty is keeping those two levels of expectation aligned with a state that itself depends on earlier draws. For the greedy companion, the selected coordinate may not be unique; the statement must cover every maximizing choice without assuming a fixed tie-breaking rule.
The vector space is EuclideanSpace ℝ (Fin d). The shared definitions give (5), the step (6), the iterate produced by a word Fin k → Fin d, and the expected gap as a real finite sum. The published ShiOptRates.PolyakLojasiewicz predicate represents (3) after multiplying both sides by two. Every theorem using uniform draws assumes ; every step with assumes . The goal also states differentiability, an explicit global minimizer, and . No convexity is assumed. A free real number called would change the PL condition and could invalidate the rate, so the formal statement uses throughout.
The index-word average is an exact finite representation of independent uniform sampling, including . It does not sample coordinates without replacement. The companion theorem represents the maximum-norm PL condition by requiring its inequality at every maximizing coordinate, which is equivalent for , and quantifies over every run satisfying the Gauss–Southwell update relation. Useful contributions include proofs of the three displayed milestones, the passage from one draw to the word average, and the greedy companion. The paper's optional remark on sampling proportional to coordinate-specific constants and its exact-coordinate-minimization remark are outside this proposal.
An assortment decision determines which products a seller makes available to a customer. When customers differ, the seller may first choose a limited collection of products and then decide which of those products to display to each arriving customer. This is a concrete way to represent personalized product pages or offers with a common inventory or display budget. The benefit of that second decision is not immediate from a single-customer model: personalization can remove products that dilute one type's purchases while retaining them for another type. El Housni and Topaloglu quantify this benefit for a mixture of multinomial logit choice models.
Their Theorem 3.1 compares optimal expected revenue with and without customer-type customization. It gives a universal factor depending only on the number of types and an explicit family showing that this order can occur. The result is already proved in the authors' SSRN version of December 7, 2021. This mission concerns the statements and proof in that version; the published Operations Research article appeared in 2023 and may use different numbering.
There are products and customer types . Product earns revenue when purchased. Customer type arrives with probability , with . Its preference weight for product is ; the no-purchase alternative has weight one. An assortment offered to type yields MNL expected revenue
The seller may initially carry at most products. In the customized assortment problem (CAP), it chooses and, after seeing the type, offers a subset . For a fixed carried set, write and for any collection of types. Thus is the expected personalized revenue. In the mixed multinomial logit problem (MMNL), the same carried assortment is offered to every type. Both models obey the same first-stage cardinality limit:
This formulation follows §2 and §3 of the December 2021 SSRN version, pp. 5–7. A zero preference weight is allowed: the authors' tightness instance assigns zero to products a type does not consider.
For every valid model and every first-stage budget , the target is
The factor counts customer types, not products. The result covers as well: both values are zero. It does not assume the products are sorted by revenue, since the numerical indexing convention in §2 is unnecessary for this comparison and is incompatible with the paper's tightness family.
The same theorem says that there are instances for which the CAP value is times the MMNL value. The formal target uses the instance constructed in its proof, pp. 8–9 and records the explicit bound implied there:
In this family . With , the parameters are , , and when and zero otherwise. The proof chooses and . The goal also asserts that this family satisfies the model assumptions. The accompanying milestones are the paper's typewise comparison, the CAP lower bound, equation (3.1), its two term bounds, and the MMNL upper bound.
The universal inequality limits the improvement that type-specific displays can offer in this model using only the number of types. The family in the second part shows that no bound independent of can replace it across all valid instances. Thus the comparison locates the possible value of customization even when the seller may carry every product. It also distinguishes the effect of a shared display from the effect of the common product budget, since the example has .
The paper already proves both claims. A complete formal development would check the exact MNL revenue formula, the two finite optimization problems, and the asymptotic example within one Lean environment. It would leave reusable definitions for personalized and common assortments under a mixture of choice models. The statements in this draft compile with proof placeholders; this mission does not claim that the theorem has a machine-checked proof yet. It welcomes proofs of the listed milestones, lemmas about finite maxima and nonnegative MNL revenue, and a proof of the combined goal.
For each type, personalization maximizes revenue over its own subset of ; MMNL must use one subset for all types. Exchanging the sum over types with a maximum over assortments would erase that distinction and is generally invalid. A simple comparison of the two optima gives the first inequality but cannot explain the precise factor or why it can be approached in order. The tightness family also balances rapidly changing revenues and arrival probabilities against preference weights. Its boundary case has , so a claim needing would miss a valid member of the family.
Lean represents products by Fin n, customer types by Fin m, and assortments by Finset (Fin n). The paper's one-based product is Lean's index i.val + 1: becomes a ^ (i.val + 1), and becomes b ^ (m - i.val). The preference function takes product first and type second, matching . The common revenue calculation imports the published ChoiceCDLP.MNL.mnlObjective with no-purchase weight one.
All maxima are Finset.sup' over nonempty finite families. The feasible family contains the empty assortment for every natural-number budget; the personal subassortment family contains the empty set as well. This makes the values genuine finite maxima, including at zero budget. No real sSup fallback value is used. The standing assumptions are positive revenues, nonnegative preference weights, nonnegative arrival probabilities, and a probability sum of one. The explicit instance is restricted to , has positive MMNL value, and satisfies each standing assumption. These conditions exclude a vacuous ratio based on zero MMNL value or an instance outside the model.
The complete development needs elementary facts about finite sums, powers, ordered Finsets, finite maxima, and nonnegative rational functions. The MNL objective is already a separate published definition; the paper-specific CAP, MMNL, and instance definitions are local. The proof targets are the claims printed in the December 2021 SSRN version, with the constant disclosed as an explicit pin from its proof.
Gradient descent on a smooth function converges at a linear rate (the optimality gap shrinks by a constant factor each step) under strong convexity. Many problems in machine learning and statistics are not strongly convex: least squares with a rank-deficient design, logistic regression on separable or degenerate data, and some non-convex objectives. Over roughly 25 years several weaker conditions were proposed that still give linear convergence. Examples are the error bound of Luo and Tseng, restricted strong convexity, essential strong convexity, weak strong convexity, and quadratic growth (also called optimal or semi-strong convexity). Each came with its own proof, usually assuming convexity. How these conditions relate to one another was rarely made explicit.
Karimi, Nutini and Schmidt (arXiv:1608.04636, ECML PKDD 2016) put the Polyak–Łojasiewicz (PL) inequality (Polyak, 1963) at the centre. Their Theorem 2 orders seven conditions by strength for functions with a Lipschitz gradient, without convexity. It shows that PL is equivalent to the error bound and implies quadratic growth. For convex functions it shows that the four weakest conditions coincide. The equivalence of EB and PL is a special case of a result of Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234, Theorem 5). Zhang (arXiv:1606.00269) independently related RSI, EB, PL and QG.
Let be differentiable with gradient . The paper's standing assumptions (§2, p. 2) are:
For every , denotes a projection of onto : a point of at distance from . Each of the following conditions involves a constant , which may differ between conditions (Appendix A, pp. 11–12):
Read each condition as "it holds for some ". For with a Lipschitz-continuous gradient,
and if is also convex,
The goal states no constants, because the constant may change along the chain.
The appendix proves a subset of the arrows, each with an explicit constant. The rest follow by transitivity.
One further milestone is display (20). Under PL, satisfies at every .
The result. Theorem 2 shows that QG is the weakest of the seven conditions. QG alone does not rule out non-global local minima, so it cannot guarantee that gradient descent reaches a global minimizer. Among the conditions considered, PL and the equivalent EB are therefore the most general that still give linear convergence to a global minimum. The paper's Theorem 1 gives that rate under PL with a one-paragraph proof. For convex , RSI (there called restricted strong convexity), EB, PL and QG are one condition. A rate proved under any of them transfers to the others, up to the constants of the milestones.
Formalizing it. The result is proved on paper, and the arrows of Appendix A are short, except PL → QG. A machine-checked version adds three things. It fixes a precise meaning for when is not convex and a nearest point is not unique. It records the correct constant in EB → PL: the printed text says , while the displayed argument yields . It puts PL → QG for non-convex on a checked footing; the acknowledgments note an earlier error in this proof. No formalization of these implications is known to be on the platform or in Mathlib.
Most arrows are one-line rearrangements or the Cauchy–Schwarz inequality. EB → PL also needs the quadratic upper bound implied by the Lipschitz gradient, and at a global minimizer.
The obstacle is PL → QG without convexity. The natural first idea fails. Integrating along the segment from to uses no information from PL, because the gradient along that segment is unrelated to the gap . The implication is global: it converts a pointwise bound on the gradient into a lower bound on in terms of the distance to a possibly non-convex set . Any proof has to bound the distance to by the length of some path into it that is controlled by . Building such a path in Lean, with its existence, its arrival at in finite time and a bound on its length, needs analysis that is not yet assembled in Mathlib for this purpose.
EuclideanSpace ℝ (Fin d), abbreviated E d. Gradients are Mathlib's gradient. The Lipschitz gradient is the literal hypothesis ∀ x y, ‖gradient f x - gradient f y‖ ≤ L * ‖x - y‖ with 0 < L, together with Differentiable ℝ f.xstar with ∀ y, f xstar ≤ f y, and is f xstar. In WSC, is written .p with IsProjSel f p: p x lies in and ‖x - p x‖ = Metric.infDist x X*. Every condition, and Theorem 2, refers to an arbitrary such selection. ESC's "" is p x = p y for that same selection. No Classical.choose is used.ShiOptRates.PolyakLojasiewicz f (gradient f) μ fstar (definition ShiOptrates_FunctionClass), i.e. . This is the paper's (3) multiplied by 2.Holds C := ∃ μ, 0 < μ ∧ C μ independently on each side of every arrow. Convexity is ConvexOn ℝ Set.univ f.p is constrained by IsProjSel, not free, and the goal's hypotheses are satisfiable: with , satisfies all of them and SC with . A formalization that fixed one for the whole chain, or replaced by an unconstrained map, would be a different theorem.Stochastic models of chemical reaction networks in cell biology routinely combine species present in a handful of copies with species present in thousands, and rate constants that differ by orders of magnitude. Simulating such a system exactly is expensive, and model reduction replaces it with a lower-dimensional limit. A systematic approach, developed by Ball, Kurtz, Popovic and Rempala (2006) and by Kang and Kurtz (arXiv:1011.1672), normalizes species numbers and rate constants by powers of a large parameter and derives limits as on several time-scales.
For such limits to exist, the normalized species numbers must stay of order one. For a single species this is the species balance condition: either the fastest reaction producing it is as fast as the fastest reaction consuming it, or the time-scale considered is short enough that the imbalance does not show. Kang and Kurtz observed (arXiv:1011.1672v1, §3.2, p. 9) that this is not enough: a collection of species can be produced collectively at a different order of magnitude from the rate at which it is consumed, even when every member is balanced. They therefore impose a balance condition on every nonnegative linear combination of species, which is infinitely many conditions. Section 3.4 of their paper proves combinatorial lemmas that reduce the work of checking them. This mission formalizes the lemmas on positive combinations of two weight vectors.
A reaction network has species and reactions. Reaction consumes molecules of and produces ; its net change is the vector . Each species carries a scaling exponent and each reaction an exponent ; put
the order of magnitude (as a power of ) of the rate of reaction .
A weight vector describes the linear combination . Its sign sets (Definition 3.1) are
the reactions that increase and decrease . Maxima are taken in , with , and is the maximum.
Fix a time-scale exponent . Condition 3.2 holds for if either the balance equation
or the time-scale constraint
holds, with when .
Let , , and suppose
Then (i) if Condition 3.2 holds for and , it holds for ; and (ii) if (3.7) holds for and , it holds for .
Condition 3.2 must hold for every before the limit theorems of the paper's Sections 4–5 apply. Lemma 3.8, together with the decomposition over strongly connected components (Lemma 3.4, the subject of the first mission of this series), turns that infinite family into finitely many checks for many networks: once the condition is known for some generating vectors, it propagates to their positive combinations whenever the sign sets do not conflict. Remark 3.9 gives a condition on the stoichiometry alone under which they do not conflict, and Lemma 3.10 reduces checking balance along a ray of combinations to finitely many breakpoints.
The results are proved in the paper (arXiv:1011.1672v1, pp. 15–19; published in Ann. Appl. Probab. 23(2), 2013), but none is formalized anywhere to our knowledge. The printed proof of Lemma 3.10 is a sketch that treats only the first breakpoint of the ray ; a machine-checked proof would settle it in full. The definitions of the sign sets, the balance equation and the time-scale constraint are reusable for the other missions of this series.
The proofs are elementary, and the work lies in the bookkeeping. Every statement mixes three conventions: maxima over sets that can be empty (value ), a time-scale constant that can be , and strict versus weak sign conditions on . Lemma 3.8 is a case analysis on which disjunct of Condition 3.2 holds for each of and ; the obvious idea of applying (3.16)–(3.17) alone fails in the case where both vectors are balanced at the same level ((3.34) in the paper), where only upper bounds are available. That case needs the disjointness hypothesis to get the matching lower bounds (3.35)–(3.36). Lemma 3.10 needs an argument along the whole ray , : the sign pattern of changes at finitely many values of , and balance has to be tracked through each change, not only the first.
Species are Fin s and reactions Fin r (0-based indices; are arbitrary naturals). ν k i is ; , and are real numbers, and is defined from rather than taken as a free parameter. A combination is c₁ • θ₁ + c₂ • θ₂ on Fin s → ℝ. Maxima are Finset.sup into WithBot ℝ, so the maximum over the empty set is and is ⊔. is an EReal defined by cases: if , otherwise the difference of the two maxima computed in (or if no is positive). Every statement carries the paper's standing assumptions , and .
These choices rule out the trivializing encodings: a real-valued maximum with a default value of on the empty set would make the balance equation hold spuriously; a subtraction in EReal would turn into ; and dropping or would change which reactions lie in the sign sets of the combination. In Lemma 3.8 the disjointness of the sign sets is a disjunction, as printed, and the second paragraph's "Condition 3.7" is read as the balance equation (3.7).
The development needs only finite sets, finite sums and order on ; no probability theory is involved. Lemmas about Finset.sup into WithBot ℝ over unions and subsets are reusable. Proofs of the milestones, of the goal, and of Lemma 3.10 are all welcome.
Chemical reaction networks can contain reactions whose rates differ by powers of a large scaling parameter. A species may then change on one time scale while other combinations of species remain nearly fixed until a later one. This matters when replacing a detailed network by a smaller model: the quantities retained at the first scale need not be the quantities that evolve at the next. Kang and Kurtz formulate this separation using the reaction exponents and the changes made by each reaction, before analyzing the stochastic process limits in their paper. This mission concerns the algebraic separation of the first two natural time scales in Lemma 4.4, rather than a convergence theorem for the stochastic processes.
A reaction network has a finite set of species and a finite set of indexed reactions. For reaction , the nonnegative integer is the number of molecules of species consumed, and is the number produced. Its net change is . The two reaction vectors may coincide; allowing such a reaction does not make it change any species. The paper introduces a nonnegative abundance exponent for each species and a real rate exponent for each reaction. The exponent relevant to a reaction under that abundance scaling is §2 and §3.2.
A nonnegative vector assigns weights to the species. The weighted quantity changes by when reaction occurs. Define and as the reactions for which this dot product is respectively positive and negative. Let be the greatest among indices with . The natural time scale of this combination is
An empty maximum is , so a combination unaffected by every reaction has . In particular ; the unused value of has no effect. A coordinate vector gives a single species' scale . The first time scale is (3.5), Definition 3.1, and (4.1).
At scale , define . It contains every reaction meeting that exponent equation, including one that leaves species unchanged. Let consist of the coordinate vectors for which is nonempty, and let be the coordinate projection onto their span. The nonnegative combinations whose projection is unchanged by each such reaction form
The second time scale is . This is the paper's minimum over : despite the infinite set of eligible vectors, every finite value of is a difference of one of finitely many and one of finitely many §4, p. 21.
The first milestone compares each weighted combination with the species in its positive support and identifies among all nonnegative combinations:
The second milestone is the first sentence of Lemma 4.4. For and , a nonzero implies . The goal is the lemma's strict separation:
These statements and their source order are on p. 21 of the preprint. The goal allows , which represents the absence of a later changing combination in .
The strict inequality says that the quantities eligible for the second scale cannot move at the first scale. It makes the two-scale terminology precise for this exponent model and separates an algebraic fact about reaction vectors from the later analysis of stochastic limits. A reduced process on the second scale requires additional stability and convergence conditions; Lemma 4.4 alone supplies neither. The paper explicitly discusses that limitation immediately after its proof on p. 22.
This mission packages the reaction-exponent definitions and the scale-separation statements as Lean declarations. Their proof obligations remain open in the proposal. Reusable parts include the finite reaction indexing, real-valued net-change vectors, the explicit convention for empty maxima, and the extended-real scale definitions. A complete development may also establish supporting facts about the finite range of and the coordinate projection; such facts are useful beyond this lemma. The paper's stochastic limit theorems are outside this mission's scope.
Checking separately that every has does not establish : an infimum of strictly larger values can still equal . The statement needs the finite-range property of the scale function, together with the interaction between the fast-reaction equation defining and the projected orthogonality condition defining . Empty reaction sets and zero weighted combinations also require explicit extended-real values. Replacing their scales with a default real number would change the claim Lemma 4.4, pp. 21–22.
Species and reactions are Fin s and Fin r; their indices begin at zero, while the paper numbers them from one. The stoichiometric arrays have natural-number entries, and are real-valued, and theorems carry . The sets of changing reactions and the positive support of are finite sets. Empty maxima use a bottom-extended real, while , , , and live in extended reals. Finite scale differences are calculated in the reals before conversion. The formulas define from and construct from ; neither is a free input. No extra positivity condition is imposed on .
The coordinate projection retains the indices belonging to . The infimum for ranges over all of , including the zero vector and combinations unchanged by every reaction. The goal assumes that some reaction changes a species. Without this necessary nondegeneracy condition, and the strict conclusion is false. It adds no condition on the initial stochastic state: the assumption at the start of §4 belongs to its process-limit statements. The paper develops at-most-binary mass-action rates in §2, but Lemma 4.4 uses only the indexed reaction vectors and their exponents; the Lean declarations expose exactly those algebraic data.
Nesterov's accelerated gradient method minimizes a smooth convex function with an error of order after steps, against for plain gradient descent, and this rate is optimal among first-order methods. Its momentum coefficient has long been regarded as delicate. Su, Boyd and Candès (arXiv:1503.01243, J. Mach. Learn. Res. 17(153), 2016) model the method by the ordinary differential equation and ask what the constant means. Their §4 replaces by a parameter , in the ODE and in the algorithm, and finds a threshold: for the inverse-quadratic rate survives, for it can fail.
This mission formalizes the discrete half of the "high friction" case : Theorem 6 of the paper, which gives the rate and a weighted summability bound for the generalized Nesterov scheme in the composite (proximal) setting of Beck and Teboulle (SIAM J. Imaging Sci. 2009).
Timeline. Nesterov (1983) introduced the method with momentum . Beck and Teboulle (2009) extended it to composite objectives (FISTA). Su, Boyd and Candès (arXiv 2014, JMLR 2016) proposed the parameter and proved Theorem 6. Chambolle and Dossal (J. Optim. Theory Appl. 2015) and Attouch and Peypouquet (SIAM J. Optim. 2016) then used the same family with to prove weak convergence of the iterates and the faster rate.
Let be a real Hilbert space. The objective is , where
A minimizer of is assumed to exist, and . For a step size , the proximal map is , and the proximal subgradient is
Given , the generalized Nesterov scheme (19) produces and from a starting point by and, for ,
For this is Nesterov's method (FISTA when ). The proof uses the auxiliary points and the discrete energy
For and , for every ,
The two bounds are proved together and stated as one theorem, as on the page.
The result shows that the constant in Nesterov's momentum is a threshold, not a tuned value: every larger keeps the guarantee, with an explicit constant . The second bound does not follow from the first. It says the gap cannot stay of order along any set of indices of positive density, and it is the starting point of the later and iterate-convergence results for .
On the formal side, the platform already has the basic inequality (22) and a version of the energy argument with the weaker coefficient , under the strict step condition and with bounds in terms of . This mission adds the paper's sharper energy decrease (20), allows the step , and expresses both bounds through the initial distance alone, which requires the first step of the scheme to be part of the hypotheses. To our knowledge no machine-checked proof of Theorem 6 exists.
The argument is elementary in structure but exact in its constants. The obvious route, a Lyapunov energy that decreases, gives a decrease coefficient of order ; obtaining the paper's coefficient requires the precise algebra relating , , and . The objective takes values in , so every manipulation must respect extended-real arithmetic: itself may lie outside the domain of , and the passage from (20) to (21) cancels a term that may be infinite. The first iterate must be tracked separately, because the bound is in terms of while the momentum formula is only meaningful from .
The Lean development works in a real Hilbert space H (InnerProductSpace ℝ H, CompleteSpace H); ℝⁿ is a special case. It reuses three published items: ThreeOpSplitting.ConvexRates.Problem (IsProperClosedConvex, IsProx), NesterovFB.Rates.Algorithm (the objective theta, the extrapolation extrap, gradMap , zSeq and energy , with the algorithm's parameter set to ), and the proved theorem NesterovFB.Rates.eq9_prox_grad_inequality, which is (22). A new definition NesterovODE.GenScheme.IsGenNesterovRun states (19) for every , the case being the first step .
Conventions committed to:
EReal, and real coefficients enter through the coercion. is finite for , and so is .P with IsProx s h P.s * L ≤ 1, with 0 < L.tsum.Dropping the first-step hypothesis would make the goal false, since would then be arbitrary; stating the bound in terms of instead of would be a different, weaker theorem. Contributions welcome: proofs of the milestones, and EReal bookkeeping lemmas for coefficient-weighted inequalities that are reusable for other accelerated proximal methods.
In a congestion game, each player chooses resources and pays a cost that depends on how many players use each chosen resource. Such games model shared facilities and network use, where independently chosen strategies can cost more in total than a coordinated choice. The price of anarchy measures this inefficiency by comparing the social cost of an equilibrium with the minimum social cost. A familiar way to bound it is to prove a smoothness inequality that applies to every pair of strategy profiles. That inequality has a useful reach: once established, it bounds not only pure Nash equilibria but also broader equilibrium notions. The question in this mission is how much that reach costs in sharpness. Roughgarden (2015) proves that for congestion games it costs nothing at the level of the worst case over any fixed collection of allowed resource cost functions.
For affine resource costs, earlier analyses had already identified a worst-case value of , attained by a finite congestion game and matched by a smoothness bound. The 2015 paper asks whether this agreement reflects affine costs or a general property of congestion games. Its Theorem 5.8 gives the latter answer, even when the collection of allowed functions is infinite and has no prescribed formula. The mission treats the theorem at that generality, while giving the finite positive case and the boundary case their own supporting targets. Roughgarden (2015), §§2.3 and 5.
A finite congestion game has a finite player set, a finite resource set , and for each player a nonempty set of subsets of called strategies. Each resource has a cost function . For a strategy profile , its load is the number of players whose selected strategy contains . Player pays , and the social cost is . A profile is a pure Nash equilibrium when no player can lower its own cost by changing its strategy alone. These are the objects of Example 2.5 in Roughgarden (2015).
Fix a nonempty set of resource cost functions, each nonnegative, nondecreasing, and not identically zero on positive loads. The class contains every finite congestion game whose resource functions belong to . It permits any finite number of players and resources and any nonempty strategy families. The pure price of anarchy is the largest equilibrium-to-optimum cost ratio in one game, allowing when an equilibrium costs more than zero but the optimum costs zero.
A game is -smooth if, for every two feasible profiles , the sum of the player costs after each player individually switches from to is at most . The set consists of pairs with that satisfy this inequality for every game in the class. A related resourcewise set asks, for every , current load , and comparison load , that
Its best ratio is , with value if there is no admissible pair. The bounded-load versions and use and . Roughgarden (2015), equations (34)–(36) and (41).
Theorem 5.8, in the form of equation (34), is the goal:
It applies to every nonempty set satisfying the standing cost-function conditions, whether finite, countable, or uncountable. Neither the number of players nor the number of resources is fixed. The equality is stronger than the routine upper bound from smoothness: it says that the best upper bound available from a uniform smoothness argument matches actual worst-case pure-equilibrium inefficiency. Roughgarden (2015), Theorem 5.8 and (34).
The paper also identifies the common value with :
The milestone list follows the paper's statements: the general upper bound; nonnegativity of ; passage from resource constraints to game smoothness; the bound for one game; the two finite optimization lemmas; the finite lower-bound theorem; the infinite-price boundary case; the countable case; and the characterization by . The finite lower-bound target uses the one-sided conclusion established in the proof of Theorem 5.6. Roughgarden (2015), §§5.1–5.5.
The equality rules out a uniform improvement of the worst-case pure price-of-anarchy bound by using features of pure Nash equilibrium that a smoothness argument ignores. In this domain the broader applicability of smoothness does not force a worse class-wide bound. For a chosen cost-function family, the resourcewise characterization expresses that bound through explicit inequalities rather than a search over every possible finite game. Roughgarden (2015), §§2.4 and 5.5.
The result is proved in the paper. The remaining work here is a machine-checked proof of its formal statement and supporting theorems. The published congestion-game model supplies loads, player costs, feasible profiles, and pure Nash equilibria. The definitions of smoothness parameters and prices of anarchy built for this mission can also support later work on other cost-function classes and equilibrium bounds. The goal statement itself is a proof target, not an already verified result.
The smoothness inequality immediately gives an upper bound on equilibrium costs, but it does not by itself show that a game attains or approaches that bound. The difficult direction relates a small family of resourcewise constraints to actual games with inefficient equilibria. For finite positive cost-function sets, the optimum parameter value may be attained or may be approached only at infinity in parameter space; the two cases have different statements in Lemmas 5.3 and 5.5. The general theorem must also cover functions that vanish at a positive load, unbounded worst-case ratios, and sets of functions of arbitrary cardinality. Simply optimizing a bound for one fixed game would miss the supremum over the entire class. Roughgarden (2015), §§5.2–5.4.
Lean represents players and resources by Fin k and Fin m and quantifies over every . A strategy is a finite resource subset, a strategy family is finite and nonempty, and all costs are real-valued at each load. The value is unrestricted because it is unused in a player's cost and is multiplied by zero in (35). The all-zero function is excluded as in §5.1. Nonemptiness of , stated at the start of that section, is carried into the finite optimization lemmas because their conclusions select functions from . Zero-player and zero-resource games are allowed and do not raise the worst-case supremum.
Prices of anarchy and the values are extended nonnegative reals. Thus an empty smoothness-parameter set has infimum ; a positive equilibrium cost over zero optimum gives ; and a game with no equilibrium contributes zero to the supremum. The paper's finite congestion games with nonempty strategy sets do have pure equilibria. The conversion of a real ratio into this type does not truncate admissible class-wide ratios: if some cost function has , a one-resource game forces the ratio to be at least one; if none does, the parameter set is empty. Smoothness and optimum quantify over feasible profiles only. These choices prevent the equality from becoming vacuous through an empty real infimum, total division by zero, or a supremum over a fixed small game size.
The complete development needs finite-set sums, function updates, extended nonnegative infima and suprema, and the published congestion-game definitions. Reusable contributions include lemmas about the resourcewise parameter sets and their relation to game smoothness. The paper's uncountable approximation paragraph has a gap for flat cost functions; the theorem remains the stated target, and a formal proof may use a different argument at that stage. Roughgarden (2015), pp. 31–32.
Nesterov's accelerated gradient method (Nesterov, 1983) minimizes a smooth convex function with the update
and, for step size , attains . The rate is optimal among first-order methods, yet the classical proof proceeds by an "estimate sequence" argument that offers little insight into why the momentum coefficient works.
Su, Boyd and Candès (arXiv:1503.01243, J. Mach. Learn. Res. 17, 2016) showed that, as , the iterates track the solution of the second-order ordinary differential equation
under the time identification . Their Theorem 3 is the continuous-time counterpart of Nesterov's rate. Its short proof by an energy (Lyapunov) function became the template for a large literature on continuous-time models of accelerated methods, including Wibisono, Wilson and Jordan's variational perspective (PNAS 2016) and Attouch, Chbani, Peypouquet and Redont's analysis of the damped system (Math. Program. 2018).
This mission formalizes Theorem 3 and the three steps of its proof.
Let and let carry the Euclidean inner product and norm . For differentiable, is its gradient.
In the Lean development these are IsFL, IsFinfty, IsSolution f 3 x₀ X V and energy f xstar X V t, in the namespace NesterovODE.Rate, where V is the velocity .
For every , every minimizer , every and every solution of (3),
Theorem 3 is the statement that makes the ODE a faithful model of Nesterov's scheme at the level of rates: under , the bound (7) reproduces the discrete bound (6) with the same constant 2. The paper also shows that the constant cannot be improved (p. 8). The energy is the continuous analogue of the potential used in discrete proofs, and the same template, with other weights, gives the paper's later results on the generalized damping and on strongly convex objectives.
The result is proved in the paper. As far as the platform and Mathlib are concerned it is not formalized: Mathlib has the calculus (derivatives of inner products and norms along curves, the first-order characterization of convexity, monotonicity from a sign of the derivative) but no statement about this ODE. A machine-checked proof establishes the Lyapunov argument for the singular-at-zero system, including the endpoint where only one-sided regularity is available, and supplies reusable lemmas for the other missions of this series and for formalizations of inertial dynamics with vanishing damping.
The algebra is short; the care lies in the analytic bookkeeping that the paper leaves implicit.
EuclideanSpace ℝ (Fin n), is Mathlib's gradient f. is 0 < L ∧ ConvexOn ℝ Set.univ f ∧ ContDiff ℝ 1 f ∧ LipschitzWith L (gradient f) with L : NNReal.HasDerivAt rather than deriv, so no derivative silently takes the default value ; the solution predicate is satisfiable (for , , the zero curve is a solution), so the goal is not vacuous.Contributions welcome: proofs of the three milestones and of the goal; general lemmas on the derivative of and ; and the first-order convexity inequality in gradient form, which the strongly convex and generalized-damping missions of this series also need.
Gradient descent is often introduced with strong convexity as the condition that gives a geometric reduction in objective error. That condition excludes useful smooth objectives whose minimizer is not unique and some nonconvex objectives. Karimi, Nutini, and Schmidt place the Polyak–Łojasiewicz inequality at the center of a more general account: it controls the objective gap using the squared gradient norm without requiring convexity. Their paper uses it to analyze gradient, coordinate, stochastic, and proximal gradient methods, and identifies settings including least squares and logistic regression in which the condition is useful. Karimi, Nutini, and Schmidt, §1–2
This mission isolates the paper's first rate theorem and its immediate analytic setting. The question is whether the ordinary gradient step with length has a global geometric rate when the objective has a Lipschitz gradient, attains its minimum, and satisfies the PL inequality. The claim applies to every initial point, even when the function is nonconvex. It also gives a precise test case for deciding which properties of smoothness and optimality must be represented explicitly in Lean. Karimi, Nutini, and Schmidt, Theorem 1, p. 2
Let be a natural number and let be a differentiable objective. Its gradient at is , with the Euclidean norm and inner product denoted by and . An -Lipschitz gradient means that for every , with . The corresponding quadratic upper bound is the paper's inequality (2):
The optimization problem is unconstrained. It has a nonempty set of solutions: choose a global minimizer , so for every , and write . This notation ties the reference value to an attained optimum. The PL inequality with constant is
Given any starting point , the gradient descent run is the sequence specified by . The term “linear convergence” here refers to a geometric bound on the difference in objective values, not to a claim that the points approach a particular minimizer. Multiple minimizers are allowed. These conventions are those of §2 and Theorem 1 of the source. Karimi, Nutini, and Schmidt, p. 2
The mission goal is the paper's Theorem 1. For every starting point and every ,
The target includes the gradient update itself. Its three milestones record the source's analytic path: the quadratic upper bound (2) from the Lipschitz gradient assumption, the one-step decrease displayed in the proof, and the one-step PL contraction displayed immediately afterwards. The latter two are linked to proved platform theorems whose exact-gradient specializations give the source's displays. Karimi, Nutini, and Schmidt, Theorem 1 and proof, p. 2
The mission also states the paper's observation that an exact line search over all real step sizes has the same function-value rate. Two companion claims record that a stationary point under PL is a global minimizer, and that -strong convexity implies PL with the same . These claims locate the rate theorem among the conditions discussed in §2.2 and Appendix B; they are separate from the goal and its milestone list. Karimi, Nutini, and Schmidt, pp. 3, 14
The rate bounds the objective error at each finite iteration, with an explicit factor . It explains why uniqueness of the minimizer and convexity are not prerequisites for this particular function-value guarantee. It does not by itself assert a rate for the distance to the solution set, a rate for individual iterates, or convergence to a uniquely determined point. The strong-convexity companion shows that the classical strongly convex case fits inside the same PL framework. Karimi, Nutini, and Schmidt, §§2–2.2 and Appendix B
For formalization, the mission adds the precise bridge from a literal Lipschitz-gradient hypothesis to the quadratic upper-bound form used by the existing step results. It also states the complete source theorem with an attained optimum, a genuine gradient, and the update rule, rather than treating any reference value or gradient-like map as interchangeable with those objects. The two published one-step theorems are already machine checked on Prove2Me; the five source-specific draft statements in this proposal remain targets until their proofs are supplied and verified. This distinction matters because the previously published geometric-rate theorem assumes , while Theorem 1 does not state that restriction.
Smoothness controls the change in during a gradient step through the size of the gradient. A geometric rate needs the change to be related to the remaining objective gap. That relation does not follow from smoothness alone; the PL inequality supplies the additional control. Another issue is that the factor may be negative if . The source does not exclude that parameter range, so the formal theorem must handle it without inserting an extra hypothesis. An exact line search raises a distinct issue: its asserted minimum along a line must be attained, and the chosen next iterate must be a point realizing it. Karimi, Nutini, and Schmidt, Theorem 1 and following paragraph, pp. 2–3
Lean represents as EuclideanSpace ℝ (Fin d), so is included and denotes a one-point space. It uses Mathlib's gradient on an explicitly differentiable , ordinary real scalars and norms, and a sequence indexed by natural numbers. The fixed step is written with and requires . The minimizer witness and its global-minimality property are explicit; the PL predicate uses exactly as its reference value. The PL inequality is represented in the equivalent form . The goal assumes the literal Lipschitz bound on gradients; equation (2) is a milestone conclusion. No convexity and no condition are added.
The exact line-search companion quantifies over every real step size and requires an attained minimizing iterate. The stationary-point consequence retains differentiability but does not need the -Lipschitz gradient bound. The strong-convexity companion uses the first inequality in Appendix A and the implication in Appendix B, with the same on both sides. The shared ShiOptRates predicates for the quadratic upper bound and PL inequality are referenced as published definitions. Useful contributions include proofs of the Lipschitz-to-quadratic-bound bridge and the paper-specific results, as well as reusable facts about gradients on Euclidean spaces. A freely chosen or a default value of gradient at a nondifferentiable point would change the mathematical claim; the goal excludes both.
Stochastic gradient (SG) methods are the default algorithms for training machine-learning models: when an objective is an average over a very large number of training examples, computing its full gradient even a few times is infeasible, while the gradient of a single randomly chosen example is cheap. The classical convergence theory of SG rates its expected suboptimality under strong convexity — the rate of Nemirovski, Juditsky, Lan and Shapiro (2009) — yet common models such as least squares with a rank-deficient design and logistic regression are convex but not strongly convex.
Karimi, Nutini and Schmidt (2016) observed that the much older Polyak–Łojasiewicz (PL) inequality of Polyak (1963) is enough to recover linear rates for gradient descent and its variants without any convexity. Their Theorem 4 transfers this observation to SG: under PL alone, SG with a decreasing step attains the rate known from the strongly convex case, and SG with a constant step converges linearly to a neighbourhood of the optimum whose size is proportional to the step. This mission formalizes that theorem.
Let and let carry the Euclidean norm . An index ranges over a measurable space with a probability measure , and each index has a differentiable component function . The stochastic optimization problem (7) is to minimize
of which the finite sum (8) is the case of the uniform distribution on indices. The component gradients are unbiased: for every .
The SG method (9) starts from a point and, given step sizes and indices drawn independently from , iterates
The iterate is a random vector, a function of .
The standing assumptions on (§2 of the paper) are:
Theorem 4 adds a second-moment bound along the iterates: for every iterate .
Under the assumptions above,
The second-moment bound is assumed separately for the run of each scheme, with the same constant .
The result. Theorem 4 places SG under PL on the same footing as SG under strong convexity: the same rate, with constants depending on , and only, and no convexity. Since PL holds for least squares with any design matrix and, over any compact set, for logistic regression (§2.3 of the paper), the theorem gives explicit SG rates for these models. The constant-step bound quantifies the practitioners' rule of halving the step when progress stalls: halving at least halves the noise floor .
Formalizing it. The result is proved, in a short argument, in the paper. To our knowledge no machine-checked proof exists: the existing Lean formalizations of SG rates on Prove2Me concern stationarity of non-convex objectives under a variance bound, a different noise model with a different conclusion. The remaining work is to formalize the paper's proof, which requires a usable treatment of expectations over an i.i.d. index sequence (conditioning the step from on the past) — infrastructure that every later analysis of a stochastic first-order method can reuse.
The deterministic content is elementary: the descent lemma, unbiasedness, the PL inequality, a telescoping sum and a geometric series. The difficulty is probabilistic bookkeeping. Recursion (10) takes the expectation of a one-step inequality with respect to alone, holding fixed; this is legitimate because is independent of , of which is a function. Making this precise requires measurability of the iterates in the sample path and a Fubini-type decomposition of the product law into the first coordinates, the -th coordinate and the rest. A second subtlety is that the second-moment bound holds only at the iterates, not at every point, so the one-step bound must be applied pointwise in the path, on a set of full measure, rather than once and for all.
The space is EuclideanSpace ℝ (Fin d) and is Mathlib's gradient. The index law is an arbitrary probability measure on a measurable space, and the path law is the infinite product Measure.infinitePi (fun _ => ν); the run is a deterministic function sgRun of the path. The Lipschitz-gradient assumption is stated literally on ; the PL inequality is the published predicate ShiOptRates.PolyakLojasiewicz f (gradient f) μ (f xstar) (inequality (3) multiplied by 2); the solution set is a point xstar with ∀ y, f xstar ≤ f y, and is f xstar, never a free real.
Every expectation of a gap is a lower Lebesgue integral of with values in , which equals because is the minimum; no integrability side condition can make a bound hold by default. The second-moment bound is the lower Lebesgue integral of , required for almost every path and every . Unbiasedness and problem (7) carry explicit integrability, so a non-integrable gradient cannot turn them into trivialities.
The second-moment bound is deliberately not imposed at every point . With the bound at every point, everywhere, so by PL, while along the gradient-ascent flow grows exponentially unless it vanishes; hence would be constant and the theorem vacuous. Along the iterates the hypothesis is met by non-constant objectives such as .
Additions relative to the page, all disclosed in the statements: each is differentiable; is jointly measurable, so that the iterates are random variables; the constant step is positive; the decreasing-step rate is stated for ; and "each has an -Lipschitz continuous gradient" is read as a condition on , the only one the proof uses. The page's proof of the constant-step bound writes the exponent where is meant; the statements follow the theorem's (correct) form.
Contributions welcome: the measurability of the run, the conditioning step for infinitePi, the deterministic one-step bound, and the two scalar recursions, each of which is reusable for other SG analyses.
In episodic reinforcement learning, an agent learns the rewards and dynamics of a system while choosing actions that determine which states it observes. A bound on the number of states and actions alone does not prescribe how to explore: a policy can be valuable because it earns reward, because it visits an uncertain state-action pair, or both. Foster, Kakade, Qian, and Rakhlin introduced the decision-estimation coefficient (DEC) to measure this trade-off in interactive decision problems. Their tabular reinforcement learning example gives an explicit policy distribution with a bound depending on the horizon and the sizes of the state and action sets Foster et al., §5.2.
The target is Proposition 5.6 of that paper. Its policy-cover inverse gap weighting strategy, or PC-IGW, places weight on policies that cover state-action pairs under an estimated model, while accounting for their estimated loss in reward. The paper also gives a posterior-sampling bound for a dual DEC in Proposition 5.4. PC-IGW addresses the frequentist coefficient with an explicit distribution and the constant Foster et al., Propositions 5.4 and 5.6.
A tabular Markov decision process has a finite state set , a finite action set , and decision layers. At layer , state , and action , a model supplies a transition distribution and a reward distribution . Every model shares the initial state distribution . A randomized nonstationary policy supplies an action distribution for each layer and state; all such policies form Foster et al., Example 1.2.
The trajectory law records the sequence of states, actions, and rewards generated by and . The final transition reaches a deterministic terminal state and contributes no model-dependent factor to this law. The policy's value is . Write for any value-maximizing policy and for the probability of visiting at layer . The squared Hellinger distance between two trajectory laws has the normalization , with no factor Foster et al., §2, Eq. (5).
Given an estimated model and , Algorithm 4 chooses, for each , a policy that maximizes
Let be the resulting set of distinct cover policies. The PC-IGW distribution gives each weight , where makes the weights sum to one. Proposition 5.7 states that this positive normalizer is unique and lies in Foster et al., Algorithm 4 and Proposition 5.7.
The main target is the explicit-policy inequality of Proposition 5.6. For and , the distribution from Algorithm 4 satisfies, for every normalized tabular model ,
The uniform quantifier over is the paper's supremum over its model class. Because this is a bound for a particular distribution , it certifies the stated DEC bound. The Lean goal expresses that explicit distribution and its inequality directly; it does not introduce a separate supremum over all models and infimum over all distributions. The milestone list records the unique normalizer, the exploration-bias display (59), the cover comparison (61), the local and global simulation estimates, the Hellinger information inequalities, and Lemma 5.2's change of measure Foster et al., pp. 36–38 and Appendices A.2, F.1.
The result controls the cost of exploration for a finite-horizon model class by with a specified constant. Its importance is the constructive policy distribution: the bound applies to the strategy returned by Algorithm 4, rather than asserting only that some distribution exists. In the paper, this bound combines with estimation and the general DEC-to-regret result to obtain a tabular regret guarantee; the authors also use the policy-cover idea as a starting point for their bilinear-class treatment Foster et al., §§5.2.2–5.2.3 and 7.
The paper result is proved. This mission asks for machine-checked proofs of its finite-alphabet statements; the draft theorems currently carry sorry. Its MDP interface includes reward distributions, full trajectory laws, occupancy probabilities, backward values, and local divergences. Those definitions can be reused for other tabular DEC results. Published FoundationsRL definitions already provide the discrete Hellinger and total-variation distances and a proved comparison between them. A separate published MDP interface records reward means, which cannot represent the reward-kernel Hellinger terms in this result Foster and Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making.
The cover is chosen using occupancies under , while the regret is evaluated under any in the class. An ordinary value bound for one fixed policy does not by itself control this mismatch. The page's intermediate expressions also divide by an average occupancy that may be zero. A formal statement must still cover state-action pairs that the policy distribution never visits, without assigning meaning to a zero-denominator ratio. The final inequality uses Hellinger distance between whole trajectories even though local simulation estimates are expressed through transition and reward kernels. Keeping those two levels of comparison aligned is the main mathematical burden Foster et al., pp. 37–38.
There is also a reward-bound issue in the appendix. Lemma F.3 uses continuation values in at states visited under , including states that may be unreachable under from the shared initial law. The paper states an almost-sure bound on total episode reward, but that statement alone does not control every such continuation value Foster et al., Lemma F.3, p. 107.
State, action, and reward alphabets are finite and nonempty. Probability laws and expectations are finite vectors and sums. Policies may randomize; the cover condition compares its choice against every valid randomized nonstationary policy. Layers use zero-based Fin H indices, while the paper uses . All models share . The terminal transition is omitted from the trajectory law and from one-step divergence sums. Duplicate cover policies are merged, as required by the paper's set . The selector must maximize value over valid policies, and the algorithm's weights must sum to one; these conditions exclude a free policy choice or an unnormalized pseudo-law.
The paper assumes almost surely. The local simulation lemma's stated bound needs two disclosed additions here: nonnegative stage rewards, and the same total-reward bound on every supported suffix started from any state. RewardsNormalized records them. The change-of-measure and global-simulation milestones use the weaker episode-only condition where sufficient. The cover comparison is cross-multiplied so it remains meaningful when an occupancy is zero. The goal's right side is a real number with , , and nonempty , so its divisions and size factors have the intended meaning.
A complete development needs the finite trajectory law, the policy-cover normalizer, occupancy bounds, the two simulation lemmas, Hellinger comparison inequalities, and the change-of-measure result. Contributions to these foundations, to the exact constant in Proposition 5.6, and to later generalizations of the cover are within scope. The abstract DEC infimum over all randomized policies is a later interface target; this mission's goal is the stronger, explicit-strategy certificate printed first in the proposition.
In episodic reinforcement learning, an agent acts repeatedly in an unknown system and must learn which policy earns the largest expected reward. Even when states and actions are finite, the agent's choices change which data it observes. Foster, Kakade, Qian, and Rakhlin use the decision-estimation coefficient (DEC) to connect this information constraint to regret across interactive decision problems. Their tabular example asks for an explicit bound in terms of the horizon, the numbers of states and actions, and an information penalty Foster et al., §5.2.
The result here is the posterior-sampling bound of Proposition 5.4. It gives a uniform constant, rather than a rate stated only with asymptotic notation. Its role is to show that a policy drawn from a distribution of model-optimal policies controls the Bayesian or dual DEC in a tabular class. The same article also studies a frequentist policy-cover strategy with a different coefficient; this mission isolates the posterior-sampling argument and the information inequalities it needs Foster et al., Propositions 5.4 and 5.6.
A tabular Markov decision process has a finite state set , a finite action set , and decision layers. At layer , state , and action , the model supplies a transition distribution and a reward distribution . Every model has the same initial state distribution . A randomized nonstationary policy supplies an action distribution at each layer and state. This is the policy class used in Example 1.2, including genuinely randomized policies Foster et al., Example 1.2.
The trajectory law records states, actions, and realized rewards over one episode. Its weight on a trajectory is the product of the shared initial probability, the policy probabilities, reward-kernel probabilities, and transitions between consecutive decision layers. The state after layer is a deterministic terminal state. Therefore the last model transition contributes no factor to the recorded law. The reward value of an outcome is given by a fixed map , and the value of a policy is . The occupancy is the probability of visiting state-action pair at layer Foster et al., §2.
For each model, denotes a policy maximizing over . Let be a prior on models. Posterior sampling here means drawing a model and using . The model whose performance is evaluated is a separate draw ; these two draws must remain independent. The reference model is denoted . Squared Hellinger distance has the paper's normalization , with no factor of one half Foster et al., Eq. (5).
The main target is the policy-specific inequality of Proposition 5.4. For , it asserts
The claim holds for each finitely supported prior in the finite-alphabet representation. It directly gives the same upper bound when the dual DEC is defined as the supremum over such priors and the infimum over policy distributions. The Lean goal states the inequality for posterior sampling itself; no real supremum is needed to express that stronger, explicit claim. The reference model belongs to the normalized tabular class, which is the case actually proved in §5.2.1. The printed proposition also names reference models outside the class and points to the later general result Foster et al., p. 33.
The milestones are the conditional-to-joint Hellinger inequality of Lemma A.9, both inequalities of Lemma A.11, the global and local simulation lemmas F.2 and F.3, the change-of-measure statement in Lemma 5.2, and the unnumbered posterior-sampling decoupling inequality on pp. 34–35. Together they identify the stated estimates on which the proposition rests Foster et al., Appendices A.2 and F.1.
The bound quantifies the price of learning the dynamics and rewards while selecting policies. Its explicit dependence on and is linear, and its dependence on the horizon is quadratic. In the paper, this estimate feeds the DEC-based analysis of tabular reinforcement learning and provides a comparison point for the policy-cover bound and later extensions beyond tabular models Foster et al., §5.2.
This formalization supplies a reusable interface for tabular MDPs with reward distributions: a full trajectory law, policy value, occupancy, backward values, and local divergences. The published FoundationsRL divergence definitions and a proved TV–Hellinger comparison can be reused. None of the seven statements has a machine-checked proof yet. A finite-horizon MDP object already published elsewhere records deterministic reward means and does not express the reward-kernel Hellinger distances required here.
A value difference is controlled by total variation between complete trajectory laws, but the proposed bound is expressed through local transition and reward discrepancies and ultimately through squared Hellinger distance between whole trajectories. These quantities average under different model-policy laws. Moving between them while retaining the exact constants in Lemma 5.2 is the central obstacle. A direct bound for a policy paired with the same model does not supply the double expectation in the target: the performance model and the policy-generating model are independent under posterior sampling.
The reward convention adds a second obstacle. Section 5.2 sets the reward space to and also assumes that total episode reward lies in almost surely. A model's continuation values at states it cannot reach from are not controlled by the episode condition. The local simulation bound is nevertheless asserted under the reference model's occupancy, which may visit such states.
State, action, and reward alphabets are finite; reward distributions are finite probability vectors. The paper allows general measurable reward spaces, so the finite reward alphabet is a declared scope restriction. Layers are indexed by Fin H, starting at zero, while the source labels them . The terminal transition is omitted from trajectory products and local discrepancy sums. The initial distribution is a separate parameter shared by all models. Priors and policy laws have finite support, as in the paper's discrete-topology convention for model distributions. Every policy quantified in a theorem is checked to be a probability kernel, and each selected is checked to maximize value over valid randomized policies.
RewardsNormalized expresses both standing conditions of §5.2: reward values lie in , and under every randomized policy every trajectory of positive probability has total reward . The proposition and its decoupling milestone use it. The Appendix F simulation lemmas and Lemma 5.2 use EpisodeTotalInUnitInterval, which expresses only the total-reward condition stated in those lemmas.
The target uses the full trajectory law in . Replacing it with one-step kernel distances would change Proposition 5.4. A valid model is a family of probability kernels, a valid policy is a family of action distributions, and the model selector must really choose an optimum; these checks prevent the expected inequality from becoming true through zero-weight pseudo-laws or a free, suboptimal policy selector. The definition and Hellinger lemmas can support later tabular DEC missions as well.
Interactive decision methods often need an estimate of an unknown outcome law after each round. A learner can be good at decisions only if its model of the observations is accurate where future decisions will sample. Foster, Kakade, Qian and Rakhlin measure this accuracy by a cumulative squared Hellinger distance and use it in their regret bounds for decision making with structured observations. They connect that estimation quantity to online log-loss regret, a standard objective for sequential probability prediction. The connection lets a regret guarantee for a density predictor supply the estimation guarantee needed by a decision method. Foster et al., Appendix A.3 and §4.1.1.
This mission isolates the online estimation result, Lemma A.14, from the rest of the paper. It addresses a learner that predicts a conditional outcome distribution before the next covariate and outcome are revealed. The covariates may respond to the entire preceding history. This matters in interactive decision making, where the learner's earlier choices change what it observes next. Foster et al., pp. 75–76.
There are rounds. At round , the learner has a history of past covariates and outcomes. It predicts a probability distribution for every possible next covariate . Nature draws from a history-dependent distribution , then draws from the conditional law of a distinguished true expert . An expert class indexed by supplies laws ; realizability means is the actual outcome law at every round. The prediction is selected from the past history, before is observed. Foster et al., Assumption A.1, p. 76.
For a predicted distribution , the log loss on observation is . The learner's log-loss regret is its cumulative log loss minus the smallest cumulative loss of an expert in . This is a realized quantity: both sums use the covariates and outcomes that actually occurred. The squared Hellinger distance is
The Hellinger estimation error is different from a sum evaluated only at realized covariates. At each round it averages over the conditional law of the next covariate , given , then sums these conditional errors. Thus the error measures prediction quality in the distribution the learner is about to face. Foster et al., (99)–(100), pp. 75–76.
The main target is Lemma A.14 (102): for every ,
The coefficient and the absence of a factor in are part of the claim. The probability is under the complete history law generated by the adaptive covariate process and the true expert. Foster et al., Lemma A.14, p. 76.
The first milestone is Lemma A.4, an anytime conditional exponential-moment bound. It controls one event on which an adapted inequality fails at any horizon through , without replacing it by a single fixed-horizon claim. The second milestone is the affinity identity used in the proof of Lemma A.14:
The proposal also states the expectation clause from (101) and the predictable-mask clause (103), which bounds error accumulated only on rounds selected from the past. Foster et al., pp. 70, 76, 79.
The high-probability bound lets an online density estimator serve as an estimation oracle for the paper's interactive decision bounds. A user can choose a predictor because it has a log-loss regret guarantee, then obtain control of Hellinger estimation error under adaptive observations. The expectation clause supplies the corresponding average guarantee. The masked clause handles applications that evaluate accuracy only on rounds selected before the current observation. Foster et al., Proposition 4.1 and Lemma A.14.
The result is already proved in the source paper. This mission asks for machine-checked proofs of the finite-alphabet statements and a reusable interface for sequential probability kernels, conditional error and log-loss regret. The published FoundationsRL Hellinger definition supplies the same normalization used by the paper; the mission does not propose a new distance. These items have no machine-checked proof in this proposal yet. The source also gives Vovk's aggregation guarantee for finite expert classes, but that algorithmic bound is outside the current item list. Foster et al., Lemma A.15, p. 76.
The quantity to be bounded is conditional on the past. A pathwise distance at the observed is a different random quantity and does not give (102). Adaptive covariates add another dependence on history, while the learner must choose its prediction before seeing . A fixed covariate law would therefore omit a central feature of the theorem. The anytime milestone likewise concerns all prefixes of one process at once; separate claims at each fixed horizon do not preserve its statement. Foster et al., pp. 70, 75–79.
The log-loss formula also has a boundary. A zero predicted probability gives infinite loss in the paper, whereas Lean's real logarithm returns a finite default at zero. The formal statements must keep that default from affecting a positive-probability observation. Squared Hellinger distance has its own normalization convention, so the affinity identity checks the factor needed in the high-probability constant.
The paper uses measurable covariate and outcome spaces and regular conditional densities. This mission specializes to finite covariates , finite outcomes , and a finite nonempty expert class . Each kernel is represented by a nonnegative vector summing to one. Complete histories are finite sequences, and the probability of a history is the product of its covariate and true-expert outcome probabilities. Expectations and event probabilities are finite sums. Time is indexed from zero; round in Lean corresponds to round in the paper.
The learner, experts and covariate kernel may all depend on preceding history. The learner and experts predict a law for every possible covariate while seeing only that history. A Boolean mask for (103) has the same information restriction. The Hellinger error sums conditional averages over the next covariate, and the probability guarantee is expressed as a bound on the total mass of histories where the displayed inequality fails.
The real-valued log loss requires one additional condition: on every complete history of positive probability, the learner and every expert give the observed outcome positive probability at every round. The condition is imposed only where the history law has support. It excludes Lean's default value for ; it is a scope restriction from the paper's extended-valued formulation. A normalized history law and a distinguished true expert are explicit, so the probability statement cannot be discharged by an empty event space or an unnormalized zero law. The sequential-kernel definitions can be reused in other finite online learning results, and the probability, affinity, expectation and masked bounds are separate proof targets.
In online selection, candidate items reveal themselves one at a time and an algorithm must decide immediately whether to keep each one. When the kept items must form a matching, accepting one edge can prevent a later edge sharing an endpoint from being accepted. A fractional solution supplies useful marginal probabilities, but it does not by itself specify which active edges can be kept under an unfavorable arrival order. Online contention resolution schemes provide that missing rounding step: they turn independent edge activity into a feasible online selection while guaranteeing each edge a chance of selection. Feldman, Svensson, and Zenklusen introduced the strong selectability guarantee used here, which protects an edge even against an arrival order chosen with knowledge of all random outcomes (Feldman–Svensson–Zenklusen, §1.1).
This mission isolates the matching result of their paper. It concerns a degree relaxation that is weaker than the full matching polytope, so the result applies even when the input fractional point satisfies only local vertex constraints. The source states the existence theorem as Theorem 2.7 and gives its numerical guarantee explicitly (Theorem 2.7, p. 13).
Let be a finite graph. An edge has two distinct endpoints; multiple edges may have the same endpoints. A matching is a set of edges with no shared vertex. For a vertex , write for its incident edges. The degree relaxation is
Since each edge meets a vertex, these constraints also give . Every matching has a characteristic vector in . The degree relaxation can contain points outside the convex hull of matchings, which makes the theorem stronger than a statement restricted to the matching polytope (§2.2, p. 13).
For , the active set includes each edge independently with probability . A greedy family is a downward closed family of matchings containing the empty set. A greedy online scheme accepts an active edge if adding it to the already accepted set remains in . The family may itself be random, sampled independently of .
An edge is selectable for a realized active set and greedy family when every member with can be extended by while staying in . Thus selectability promises acceptance regardless of which eligible active edges preceded . A scheme is -selectable if this event has probability at least for every and every edge. The probability includes both the active-set draw and any random family draw (Definitions 1.3–1.5, pp. 3–4).
For every and every finite loopless graph ,
Equivalently, for each and each edge , the probability that is selectable is at least . The statement includes edges with ; the selectability event concerns the ability to add an edge, rather than the probability that it becomes active. The milestones are the steps the source states in its proof, in attack order (proof of Theorem 2.7, pp. 13–14):
Taking , the deterministic greedy scheme whose family is the set of all matchings is -selectable for , :
This companion is weaker than Theorem 2.7 for every and is not used by it (Remark, p. 14).
The theorem gives a constant probability bound against the paper's strongest, “almighty” arrival-order adversary. The guarantee is available from vertex degree inequalities alone. Consequently it applies to points of the exact matching polytope as well, without asking the online rounding procedure to exploit its additional odd-set inequalities. The paper places this result beside analogous existence claims for matroids and knapsacks in Theorem 1.8, and uses greedy schemes as components in more general selection results (Theorem 1.8, p. 4).
The existence theorem is proved in the source; it is an open formalization target here. A completed Lean development would supply a reusable finite model of independent active sets, random greedy families, edge selectability, and matching degree relaxations. It would also put the exact constant and its endpoint cases under machine checking. The definitions can support future formalizations of the paper's combination and application results, although this mission claims only Theorem 2.7 and its local proof milestones.
The local degree constraints bound the fractional weight at each endpoint separately, while selectability must survive conflicts at either endpoint under any arrival order. Merely ensuring that the algorithm outputs a matching gives no lower bound for a particular edge: the adversary can expose competing active edges first. The theorem therefore asks for a stronger event that certifies an edge could be added after every eligible previously selected matching. The numerical guarantee must hold uniformly over all edges, even when a coordinate is zero (Definitions 1.4–1.5, pp. 3–4; proof of Theorem 2.7, p. 13).
The ground set is the finite edge type . The published EdmondsMatching65.Polyhedron.Graph structure represents a graph by a map from edges to unordered pairs of vertices and includes a proof excluding self-loops; its matching predicate is reused directly. This admits parallel edges, a harmless generalization of the page's graph language. Incident edge sets and matchings are finite sets. The polytope is the set of real edge vectors satisfying precisely the nonnegativity and vertex degree inequalities above. Scaling is the pointwise set operation , so remains meaningful. The parameter range is explicit.
Probability is represented by finite sums of product weights. A randomized scheme is a weight function on finite greedy families, independent of the active-set draw. Each family contains the empty set and lies inside the matchings; allowing an empty family would make selectability vacuous. The degree inequalities keep relevant coordinates in , so active-set weights are genuine probabilities. The source's ratio is given its continuous value at . For inputs outside the nonnegative domain, which the theorem never uses, that inclusion probability is also assigned to keep the distribution well formed. These choices and the loopless graph convention are recorded with the draft statements.
The formalization needs finite product probability identities, elementary exponential inequalities, and set facts about matchings and incident edges. Contributions proving the six listed milestones, the deterministic Remark, or the full existential theorem are welcome. The finite model of active sets, greedy families and selectability is shared with the other missions of this series (matroids, knapsack, combinations of schemes, submodular rounding).
Social networks exhibit triadic closure: two people with a common friend are more likely to be friends themselves than two people chosen at random, and the more common friends they have, the more likely they are to be connected. The principle goes back to sociology (Granovetter 1973) and is documented on large network data sets (see the Enron e-mail graph in Figure 1 of Fox, Roughgarden, Seshadhri, Wei and Wein).
A common computational task on such networks is to list all maximal cliques, the groups of mutually connected vertices that cannot be enlarged. On an arbitrary graph this is hopeless in the worst case: Moon and Moser showed in 1965 that an -vertex graph can have maximal cliques, and that no graph has more (Moon and Moser 1965). Yet clique enumeration on real social networks runs quickly. Fox, Roughgarden, Seshadhri, Wei and Wein proposed a distribution-free graph class, defined by a coarse form of triadic closure, on which the worst case is provably polynomial. This mission formalizes their first bound, for the class of weakly -closed graphs (Theorem 2.2 of the paper, also stated as Theorem 1.5), together with the peeling argument that proves it.
All graphs are finite, simple and undirected. For a graph with vertex set and a vertex , is the set of neighbours of ; for , is the subgraph induced by . The common neighbours of two vertices are the vertices of .
Every -closed graph is weakly -closed, but not conversely. The paper's example: a clique on vertices with one edge removed is not -closed for any , but it is weakly 1-closed (order and last).
In the Lean development these objects are IsCClosed, IsBadPairIn, IsWeaklyCClosed, maxCliquesIn, numMaxCliquesIn and numMaxCliques, in the namespace CClosedGraphs.Peeling.
For all positive integers and , every weakly -closed graph on vertices satisfies
The milestones follow the proof of Theorem 2.1 in §2.1 and the remark that extends it to Theorem 2.2. Fix a graph, an induced subgraph and a vertex . A maximal clique of is of type 1 if , of type 2 if and is maximal in , and of type 3 otherwise.
For fixed , the theorem makes the number of maximal cliques of a weakly -closed graph polynomial in , against for general graphs. Since all maximal cliques can be listed in polynomial time per clique, this makes maximal-clique enumeration fixed-parameter tractable in on the class. The paper's Theorem 2.3 turns the proof into an enumeration algorithm. Weak -closure is the version that matters in practice: Table 1 of the paper reports social networks with thousands of vertices that are weakly -closed for modest while being -closed only for much larger . The bound is the starting point of the paper's sharper Theorem 3.1 () and its lower bound Theorem 4.1, which are separate missions of this series.
The result is proved in the paper, and the proof is short. No machine-checked proof of it or of the Moon–Moser bound exists in Mathlib at the pinned revision or on Prove2Me. This mission produces both, together with a reusable vocabulary for counting maximal cliques of induced subgraphs. Proofs of the sharp Moon–Moser values, or of the sharper in the recursion, are welcome as further contributions but are not milestones.
The counting argument is elementary. The work lies in two places. First, the Moon–Moser bound is not in Mathlib and needs its own proof, and its exponential bound must be handled with real powers. Second, the type decomposition must be handled exactly: a type-3 clique is charged to a pair , and the charge has to be injective while ranges over all vertices outside . The degenerate cases are real. When is isolated in and , the clique is of type 3 and . The peeling for weakly -closed graphs must also follow the given vertex ordering, with closure checked in the shrinking induced subgraphs rather than in .
SimpleGraph (Fin n). Auxiliary statements are generic over a finite type with decidable equality.Fin n with . The set is .Set.ncard, which is exact on a finite type. "At least " is , not .Three trivializing readings are ruled out. The count is of maximal cliques, not of all cliques or of cliques of a given size. A bad pair needs at least common neighbours, not more than . In the weakly closed definition, common neighbours are counted inside , not in ; counting them in would make the hypothesis stronger and the theorem weaker.
A complete development needs a Moon–Moser lemma for induced subgraphs, the injections behind milestones 2 and 4, and a peeling induction over a vertex ordering. The first two are reusable for any maximal-clique counting argument. The induced-subgraph counts numMaxCliquesIn are also used by the later missions of this series, which repeat the definitions in their own namespaces.
Minimum-cost flow is a standard model for routing a quantity through a network while paying a cost on each arc. Unit capacities arise when each input arc can carry at most one unit; they include flow formulations of several matching and assignment problems. Goldberg, Kaplan, Hed and Tarjan analyze a cost-scaling algorithm for this setting. Their second-phase argument depends on a bound on the excess left in a pseudoflow when every excess vertex has undergone enough potential increases. This mission formalizes that bound, Lemma 5 of their STACS 2015 paper. The published paper gives an running-time bound for its unit-capacity algorithm; the running-time statement itself is outside this mission.
A network has a finite vertex set and an arc set that contains both orientations of each input arc. Write . Every input arc has capacity one; its reverse has capacity zero and opposite cost. Write for the number of input arcs, so . The paper assumes no parallel or antiparallel input arcs, allowing an arc to be identified by its ordered endpoints. Costs are antisymmetric between orientations.
A pseudoflow assigns an antisymmetric quantity to each arc and respects its capacity. Its excess at is the sum of incoming flow. Positive excess means that has flow to discharge; negative excess is a deficit. A circulation is a pseudoflow with zero excess at every vertex. An arc is residual for when its residual capacity is positive. For vertex prices , its reduced cost is . A pseudoflow is -optimal at when every residual arc has reduced cost at least . These are the paper's conventions on p. 408.
At the start of a cost scale, let be a circulation that is -optimal at prices . During the scale, is a pseudoflow that is -optimal at prices . The potential increase in scale units is . Put . The second phase begins when every excess vertex has ; the paper also states that every deficit then has and that the levels are integral. The remaining excess is .
The comparison graph has arcs and vertices . An excess–deficit cut meets every path in this graph from an excess vertex to a deficit vertex. Thus a cut is measured among comparison arcs, not among arbitrary arcs of the original network. Lemmas 3 and 4 of the paper establish the level and cut bounds on which the excess estimate rests.
The goal is Lemma 5 on p. 410, stated with both constants obtained in its proof. Under the cost-scale conditions above, and the divisibility conventions in footnotes 5–6, its two cases are
The second case also assumes that six divides the integer ; the first uses divisibility by three. The goal keeps the two conclusions separate so that the stronger bound is retained when determines the scale. Its milestone list follows the paper: Lemma 3 bounds by three on an arc of ; Lemma 4 bounds total excess by a cut; and the proof of Lemma 5 supplies the cut bands and the two size estimates. The bands use the exact three-level and six-level ranges printed on p. 410.
The result connects a condition on price increases to a numerical bound on the amount of flow still needing discharge. Combined with the paper's time per unit of remaining excess, this is the bound needed for its second-phase running-time estimate. The two regimes show how the same cost-scale state can be controlled by either the number of input arcs or the number of vertices. Without the excess bound, the paper's argument gives no comparable limit on the remaining work at the phase transition.
The paper proves Lemma 5, but this particular unit-capacity excess argument has no matching theorem in the platform catalog checked for this mission. The network, circulation and pseudoflow interfaces are already published as reusable definitions from earlier cost-scaling work. A completed machine-checked development would add the cut argument and band counts to those interfaces. Those facts can also support other analyses that compare an entry circulation with an intermediate pseudoflow; this mission does not claim to formalize the algorithm's entire execution or its running-time model.
The main obstacle is linking local price inequalities to a global bound on excess. A reduced-cost inequality controls a single residual arc, while excess may move through a path and is measured over many vertices. The comparison graph is essential: on a residual arc outside , the level difference used by Lemma 3 is not available. Counting all residual arcs as if they were comparison arcs would therefore not justify the cut bound. There is a separate counting issue: the represented network has both directions of each input arc, so using for changes the constant in the square-root case.
Lean represents the network by a finite symmetric arc set with real capacities and antisymmetric real costs. A local unit-capacity predicate marks each reverse pair as capacities or ; counts the capacity-one orientations. Flows are real valued as on p. 408. Integer costs on that page are generalized to real costs because Lemmas 3–5 use only antisymmetry and reduced-cost inequalities. No result here depends on cost integrality.
The formalization takes the cost-scale state as hypotheses: , entry circulation and -optimality, current -optimality, integral levels, level at least at excess vertices, and zero level at deficits. It takes as a natural number equal to and records the paper's divisibility simplifications. The indexed pigeonhole milestones also require so their index ranges are nonempty; the goal includes the zero-arc boundary without requiring an index. Cuts use reachability after deleting a subset of , equivalent to meeting every excess-to-deficit path. The proof of Lemma 5 prints “cut in ”; the formalized claim uses , the graph for which Lemma 3 gives the required level control and Lemma 4 states its bound.
The definition layer, path-cut lemma and finite counting arguments are the reusable infrastructure. Contributions that establish these exact statements, their necessary elementary flow identities, or a machine-checked goal proof are in scope. Counting with reverse arcs, allowing cuts outside , using arbitrary real levels in place of integral ones, or replacing both cases by the weaker bound does not express this target.
Lower bounds for interactive decision making (bandits, reinforcement learning, and the general decision making with structured observations framework of Foster, Kakade, Qian and Rakhlin, arXiv:2112.13487) compare what a learner observes under two different environments. A learner's whole interaction history is generated one step at a time: each observation is drawn from a conditional law that depends on everything seen before. Statistical estimation guarantees, by contrast, are stated one step at a time, as bounds on the divergence between the conditional laws at each round. Passing from the per-step guarantees to a statement about the laws of entire histories requires a chain rule for the divergence in use.
For the Kullback–Leibler divergence the chain rule is an identity. The paper's guarantees, however, are stated in the squared Hellinger distance, which is bounded, symmetric, and the natural loss for density estimation with the logarithmic loss. Hellinger distance has no exact chain rule. Lemma A.13 of the paper (App. A.2, p. 73) supplies an approximate one, losing a factor logarithmic in the number of steps, and the paper uses it in the proof of its main regret lower bound (Theorem 3.2, via App. C.1.3).
Fix and finite sets . A sequence is with , and denotes its prefix; .
For probability distributions on a finite set, the squared Hellinger distance, the Hellinger distance and the Kullback–Leibler divergence are
the last one set to when charges a point that does not. Note that the paper's carries no factor , so .
A family of sequential kernels assigns to each and each prefix a probability distribution on . Its sequential law is the law of under :
For a second family with law , the quantity controlled by per-step estimation is
In Lean these are IsSeqKernel, seqLaw and condHellingerSum, with hellingerSq and klDivDiscrete the published discrete divergences.
The constant is the paper's; the shape that matters downstream is the logarithmic dependence on with no assumption on the kernels beyond their being probability kernels.
If and for every , prefix and event , then .
The result. Inequality (97) converts per-round Hellinger estimation error into a bound on the Hellinger distance between the laws of complete interaction histories, under no boundedness assumption on likelihood ratios. In the paper this is the step that lets the lower bound of Theorem 3.2 relate any algorithm's behaviour under a reference model to its behaviour under alternatives, and hence express the minimax regret through the decision-estimation coefficient. Without it, only the KL chain rule is available, which requires bounded likelihood ratios (the situation of (98)) or loses more than a logarithmic factor. Lemma A.11, a milestone here, is used independently in the same lower bound and in the paper's tabular reinforcement learning analysis.
Formalizing it. The lemma is proved in the paper; no machine-checked proof exists. The published layer on the platform has the discrete divergences and the comparisons of Lemmas A.5 and A.10; the sequential-law objects, the triangle inequality, the convexity of , the discrete chain rule and Lemma A.11 are new. A completed development gives a reusable chain-rule toolkit for any later formalization of lower bounds over adaptive interaction histories.
The squared Hellinger distance does not tensorize along adaptive sequences: the natural attempt to write as a product of conditional affinities fails because the conditional affinities are random, depending on the prefix, and their expectation does not factor. Bounding by and applying the KL chain rule fails in the other direction: the conditional KL divergences are not controlled by the conditional Hellinger distances unless the likelihood ratios are bounded, and in (97) they are not. The difficulty is to obtain a bound that pays only for an unbounded ratio, with explicit constants that survive the final numerical comparison.
Fintype, distributions are probability vectors, expectations are finite sums. Coordinates are indexed by Fin n (0-based) and the alphabets may differ from coordinate to coordinate.P i x of the whole sequence that is a probability vector and depends only on the coordinates j < i; this is what makes seqLaw P the law the paper describes.Contributions welcome: proofs of any milestone and of the fact that seqLaw is a probability vector.
Neural networks trained by empirical risk minimization are sensitive to small, deliberately chosen perturbations of their inputs ("adversarial examples"). A standard defence is adversarial training: at each step, perturb the training example to increase the loss, then take a gradient step at the perturbed point. Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571, ICLR 2018) recast adversarial training as distributionally robust optimization over a Wasserstein ball around the data distribution, and replaced the hard ball constraint by a Lagrangian penalty. The resulting procedure perturbs each example by solving a penalized inner maximization, and the paper shows that, when the penalty is large enough relative to the smoothness of the loss, this inner problem is strongly concave and therefore tractable.
This mission formalizes the paper's computational guarantee, Theorem 2: stochastic gradient descent on the penalized robust objective, with an inexact adversary, reaches an approximate stationary point at the rate of smooth nonconvex stochastic optimization. The analysis follows Ghadimi and Lan's argument for nonconvex SGD (arXiv:1309.5549), adapted to a gradient oracle that is biased by the inexact inner maximization.
Parameters live in and data in a set ; both spaces carry the Euclidean norm . Data are drawn from a probability distribution on .
A transportation cost measures how expensive it is to move a data point to . Assumption A: is continuous, , and for each the map is -strongly convex. The canonical example is .
A loss has partial gradients and . Assumption B: these gradients are Lipschitz in each argument,
For a penalty , the robust surrogate and the robust objective are
By Wasserstein duality, equals the worst-case expected loss over all distributions , penalized by times the transport distance from to .
Algorithm 1 (with and constant stepsize ): from , for , draw independently, find an -approximate maximizer , meaning , and set .
Let , , , and assume for all . With and ,
for every constant stepsize . The goal is this bound at the balancing stepsize.
The result. Theorem 2 certifies that the robust training procedure is no harder, in iteration count, than ordinary nonconvex SGD: the stationarity measure decays as , and the inexactness of the adversary enters only as an additive term proportional to , independent of . This is what licenses running a few steps of gradient ascent for the inner problem rather than solving it exactly. It also explains the role of the penalty: the guarantee requires , so smoothness of the loss in the data (smooth activations rather than ReLUs) is what makes the robust problem tractable.
Formalizing it. The result and its proof are published; nothing here is open. To our knowledge none of it is machine-checked. A formal proof would add a verified Danskin-type theorem for strongly concave suprema with explicit Lipschitz constants (Lemma 1), which is reusable well beyond this paper, and a verified nonconvex SGD analysis with a biased oracle, including the measure-theoretic bookkeeping (independence of the fresh sample from the current iterate, differentiation under the integral) that the paper's proof compresses into one line.
The deterministic inequalities (31), (32) and the bias bound are short. The weight sits elsewhere. First, Lemma 1 requires differentiability of a supremum over a possibly unbounded set, with the maximizer depending on ; the paper invokes a Danskin-type theorem that is not in Mathlib, and the cost is not assumed differentiable, so the first-order optimality conditions for the inner problem must be derived from strong convexity alone. Second, the expectation step uses , which needs both differentiation under the integral sign for and the independence of from along the run. Third, finiteness of every expectation along the run is not assumed and must be propagated from step to step.
Lean representation: and are EuclideanSpace ℝ (Fin d) and EuclideanSpace ℝ (Fin m); is a set in the latter. The loss is a function on all of ; its partial gradients are required at points of and the Lipschitz conditions on only. Strong convexity is Mathlib's StrongConvexOn, whose modulus convention matches the paper. Suprema are sSup over the image of . is a Bochner integral, and is assumed -integrable for every . The run is driven by (Measure.pi). The expectations in the conclusion and in the variance hypothesis are lower Lebesgue integrals in ; the -term of Theorem 2 is moved to the right-hand side.
Hypotheses made explicit that the paper leaves implicit: (the paper writes but divides by ); nonempty, convex and closed; Lipschitz constants nonnegative; , , , ; bounded below (so is a real number); integrability of ; ; joint measurability of the oracle ; and, in (32) and the later milestones, , which the paper assumes "in the rest of the proof". Lemma 1 is specialized to the Euclidean norm, the case Theorem 2 uses. The cost is not assumed differentiable.
A trivializing formalization is ruled out: the run uses an oracle tied to by the -gap and to by membership, is the supremum of the penalized loss over , is its -integral, and the hypotheses are satisfiable (for instance , , , a point mass, ). Expectations as lower integrals prevent a non-integrable from being read as .
Infrastructure a complete development needs: the descent lemma for functions with Lipschitz gradient; first-order characterizations of strong concavity on a convex set; a Danskin/envelope theorem for strongly concave suprema; differentiation under the integral for ; and conditional-expectation bookkeeping for Markov-type recursions driven by i.i.d. samples on a finite product space. The first three are reusable in any minimax or bilevel analysis. Contributions to any milestone, or to these supporting facts as separate lemmas, are welcome.
A prophet inequality compares an online decision maker, who sees random inputs one at a time and must commit irrevocably, with a "prophet" who sees all inputs in advance. The classic single-item version (Krengel–Sucheston, Samuel-Cahn) says that a well-chosen fixed threshold earns at least half of the expected maximum. In mechanism design the same statement reads: a posted-price mechanism, which offers each arriving buyer a take-it-or-leave-it menu of prices, extracts a constant fraction of the optimal expected welfare, and does so in a way that is truthful, simple and order oblivious.
Dütting, Feldman, Kesselheim and Lucier (SIAM J. Comput. 49 (2020)) reduce the construction of such prices to a deterministic question. If, for every fixed valuation profile , one can find prices that are balanced — high enough to pay for the welfare an early allocation destroys, low enough that whatever is still feasible stays affordable — then the expected prices , suitably scaled, give a prophet inequality. This is their Theorem 3.2 for -balanced prices. For combinatorial auctions with bundles of size at most , MPH- valuations and related settings, the natural prices only satisfy a weaker condition, in which the affordability bound may also spend a multiple of the benchmark welfare. Theorem 3.5, the subject of this mission, is the extension theorem for that weak balancedness; it is what turns the paper's Theorem 4.1 (bundle size ) and Theorem 1.6 (MPH-) into - and -approximate posted-price mechanisms.
There are agents . Agent has an outcome space containing a null outcome ; outcome profiles are . For , gives to the agents in and to the others, and keeps only the agents before . The feasible profiles form a set that is downward closed ().
Agent has a valuation , drawn independently from a known distribution ; . The welfare of is , and (zero on ). An allocation rule maps every valuation profile to a feasible outcome.
A pricing rule assigns prices to outcome offered to agent given the partial allocation , with when . In the posted-price mechanism the agents are approached in index order; agent sees the prices and buys a utility-maximizing outcome, utility being .
A family of sets of profiles is exchange compatible if for every , and . Given and , a pricing rule is weakly -balanced (Definition 3.4) with respect to and if for every
A collection is weakly balanced if one exchange-compatible family works for every .
If is weakly -balanced with , then with
the posted-price mechanism with prices , approaching agents in index order, satisfies
The result. Theorem 3.5 is the second of the paper's two extension theorems. Its hypothesis is a deterministic, full-information property of prices, which is often checkable by a direct combinatorial argument; its conclusion is a Bayesian guarantee for an online, truthful mechanism. The paper instantiates it with weakly -balanced fractional prices for combinatorial auctions with bundle size at most (Theorem 4.1) and for MPH- valuations (Theorem 1.6), obtaining approximation ratios linear in and , where -balancedness alone would not apply.
Formalizing it. The theorem is proved on paper; no machine-checked version exists. The mission produces a formal account of the sequential posted-price mechanism with history-dependent prices (an online run defined by recursion over the agents), of the ghost-sample argument, and of the case analysis in . The definitions are general enough that the paper's applications — and other balanced-price arguments — can be stated on top of them. The printed proof has a slip: (A.1) is printed as an equality but only the inequality "" holds; the formalization states the inequality.
Two steps carry the content. First, the utility bound (A.1): agent could have bought its part of the deviation , but that deviation is defined from the run on a different profile. The argument needs that the partial allocation does not depend on — the mechanism is online — and that exchanging with an independent copy preserves the joint law. Making this exchange rigorous on a product measure, and handling an empty (where no deviation exists and the bound must come from ), is where the work lies. Second, is a supremum that need not be attained, so "buy your part of OPT" must be replaced by near-optimal selections and a limit.
The tempting shortcut of treating weak balancedness as -balancedness and applying Theorem 3.2 does not work: property (b) of Definition 3.1 bounds prices by a multiple of alone, which can be zero while is not.
Agents are Fin n, 0-based: the paper's agent is index , and "the order they are indexed" is the order of Fin n. Prices take values in ENNReal with ; price sums are never converted to reals, and property (a) passes its right side through ENNReal.ofReal (a negative bound becomes , which is the page's meaning). is the real supremum sSup, zero on the empty set, meaningful because values lie in .
Valuations are given by type spaces and an evaluation . The type spaces are countable with discrete σ-algebras — a disclosed restriction of the paper's general distributions, which makes every function measurable and every bounded one integrable. The null outcome is assumed free at feasible partial allocations ( for ): every pricing rule in the paper has this property, and the proof needs its consequence . Exchange compatibility is required for all , as printed. The agents' behaviour is a choice rule that sees only the agent's own type and the earlier agents' outcomes and maximizes utility at every feasible partial allocation; at infeasible ones no requirement is made. The constant is written literally inside the posted prices, never as a free parameter.
The milestones (A.1)–(A.4) are stated for an arbitrary , and (A.1)–(A.2) for an arbitrary selector into in place of the maximizer, with an explicit zero when ; both are generalizations of the printed steps. A statement in which the agents' optimality hypothesis can never be met, or in which an infinite price sum is read as , would make the goal vacuous; the encoding above excludes both, and a sorry-free one-agent instance in the workspace confirms that all hypotheses of the goal can hold together.
Needed infrastructure: product measures and the swap of one coordinate with an independent copy, lower integrals of ENNReal-valued prices, the recursion defining the run, and near-maximizers of bounded suprema. The model and mechanism definitions are reusable for the paper's other extension theorem (Theorem 3.2) and its applications. Contributions are welcome on any milestone; the pure inequality of Case 2 is self-contained.
A two-stage stochastic programme chooses a decision before an uncertain parameter is revealed and pays a cost . When is known only through data points, or through a law with many atoms, the expected cost is expensive to optimize, and practitioners replace the law by a small set of reduced scenarios. Classical scenario reduction chooses these scenarios to be close to the data in a Wasserstein distance, without looking at the cost (Dupačová, Gröwe-Kuska and Römisch, 2003; Rujeerapaiboon, Schindler, Kuhn and Wiesemann, 2022). Bertsimas and Mundru (Operations Research, 2023) propose problem-dependent scenario reduction: the distance between two scenarios measures how much the optimal decision for one costs when evaluated on the other. Their method needs, for each cluster of data, the scenario that minimizes a cost-dependent dissimilarity, which they replace by a convex upper bound, problem (16).
Theorem 3 of the paper is the sanity check for that upper bound. For the simplest cost to which it applies and a single reduced scenario (), under a symmetry assumption on the law, the minimizer of the upper bound is the mean of , which is also what Wasserstein scenario reduction returns for . This mission formalizes that statement.
Decisions and parameters both live in , with the Euclidean inner product . The feasible set is a polytope
for a matrix and a vector , assumed nonempty and bounded. The cost is , a special case of the piecewise bilinear costs of (15) (take , , ).
An optimal-decision map is any function with for every ; for a vector , is the whole set of minimizers. The set of cost-reducing parameters is
For a candidate reduced scenario , the per-scenario upper-bound loss is
For this cost it is the optimal value, in the auxiliary variables , of the per-point linear programme in (16). With a random parameter of law , the upper-bound objective for is . The squared cost for Wasserstein reduction to one atom is ; (4) takes its square root, which preserves minimizers.
Assumption 5 (p. 24) asks:
Under Assumption 5, for every measurable optimal-decision map ,
The page's "the solution … is simply the mean" is read as "the mean is a minimizer", which is what the proof concludes; uniqueness is not claimed.
The upper bound (16) is the computational core of the paper's Algorithm 1: each alternating-minimization step solves one instance of it per cluster. Theorem 3 is the only result in the paper that identifies its minimizer in closed form, and it shows that, in a symmetric case, the cost-aware reduction agrees with the classical one at . It is the paper's justification that the upper bound is a sensible surrogate and not an arbitrary convex relaxation.
The argument is a variant of the mean-minimizes-the-surrogate result of Elmachtoub and Grigas for the SPO+ loss (Management Science, 2022, Proposition 6(a)), with both terms clipped at zero and with a law living only on instead of all of . Theorem 3 is proved on paper; it has not been formalized, and on Prove2Me the Elmachtoub–Grigas statement is posed but open. The work here is to formalize the known proof, including the measure-theoretic steps the paper treats in one sentence each: integrability of the loss, exchange of the subdifferential and the expectation, and the almost-sure uniqueness of linear minimizers over a polytope.
Convexity of the objective and a vanishing subgradient at would settle the theorem, but two steps of that argument are not routine. First, the objective is not differentiable everywhere, and the subdifferential of is not in general the expectation of the pointwise subdifferentials: the exchange needs the integrable bound of milestone 2 and the almost-sure uniqueness of milestone 3. Second, that uniqueness is a statement about the geometry of polytopes and about the law of the reflected parameter together: neither convexity nor absolute continuity alone gives it. The clipping at zero adds a third point: one has to check that it is inactive at almost surely, which is where Assumption 5a's support condition on and Assumption 5b enter. Dropping either half of Assumption 5a breaks the argument: a two-atom symmetric law can put both atoms where is a whole edge, and a law charging the complement of can make the first clipping active at .
EuclideanSpace ℝ (Fin d) and is ⟪z, ξ⟫_ℝ. Decision and parameter spaces coincide (), as the cost requires.polytope P qv, with the hypotheses that it is nonempty and bounded (§1 of the paper assumes nonempty and compact; the polytope is closed).SmartPTO.Fisher.xi, SmartPTO.Fisher.zstar and SmartPTO.Fisher.Wstar; "symmetric about its mean" is the published SmartPTO.Fisher.CentrallySymmetric.zsel with the hypothesis that zsel ξ is a minimizer for every , and it is assumed measurable (needed for ; not on the page). The theorem holds for every such selection; uniqueness of minimizers is not assumed.Useful infrastructure, reusable beyond this mission: support functions of polytopes and their directional derivatives; the fact that a linear function has a unique minimizer over a polytope for Lebesgue-almost every cost vector; differentiation of convex integral functionals under the integral sign. Contributions of any of these as stand-alone lemmas are welcome.
The source is the authors' accepted manuscript (MIT DSpace, "Submitted to Operations Research"), not the published article; all page and theorem numbers refer to the manuscript, whose printed page numbers equal its PDF page numbers.
Online combinatorial optimization is a repeated game in which a learner selects, round after round, a structured object (a subset of fixed size, a path, a matching, a spanning tree) encoded as a 0/1 vector, and an adversary assigns a cost to every coordinate. It models routing, ranking, scheduling and many other sequential decision problems in operations research and machine learning, and it contains prediction with expert advice as the special case of one-hot vectors.
The most widely used algorithm for this game is the exponentially weighted forecaster, which keeps a weight on every action and multiplies it by after each round. Applied to a combinatorial action set it is called EXP2 (Audibert, Bubeck and Lugosi), or Expanded Hedge in the full-information case (Koolen, Warmuth and Kivinen, COLT 2010). Its standard analysis gives regret of order , while online mirror descent with the negative entropy (Component Hedge) achieves , which is optimal. Koolen, Warmuth and Kivinen left open whether a better tuning or a better analysis of EXP2 could close this gap.
Timeline.
Fix integers (the dimension) and (the number of rounds). An action set is a nonempty finite set whose elements all have the same number of ones: for every . At each round :
The regret after rounds is
EXP2 with learning rate starts from the uniform distribution on and updates, for every ,
In the Lean development IsBinaryActionSet A m is the action-set condition, exp2Weights A η z t is , and exp2Regret A η z n is against a fixed loss sequence . thmOneSet d, adv1 d and adv2 d ε are the action set and the two adversaries of the paper's proof.
For with a multiple of , there is an action set with constant such that for every some adversary with losses in makes EXP2 pay
The action set is chosen before the learning rate, and the adversary after it.
The result. Theorem 1 shows that the gap between EXP2 and mirror descent with the negative entropy is not an artefact of the analysis: on an action set with , where the optimal rate is of order , no learning rate brings EXP2 below . Exponential weights over the actions are therefore provably suboptimal in online combinatorial optimization, which motivates working with the convex hull of (mirror descent) rather than with the actions themselves. The construction is also a template for algorithm-specific lower bounds: two adversaries, one punishing large and one punishing small learning rates.
Formalizing it. The result is proved in the paper (App. A, with Lemma 3 in App. C); to our knowledge none of it is machine-checked. A formalization yields a checked algorithm-specific lower bound for exponential weights, an exact closed-form regret computation for EXP2 on a structured action set, and a rigorous proof of Lemma 3, whose printed proof checks numerically before an asymptotic argument with Stirling's formula.
The statements are elementary, but each step hides a real computation. The first adversary requires the exact distribution of EXP2 on a set of actions over alternating rounds, and a regret identity rather than a bound. The second requires controlling EXP2's expected loss over all rounds against a constant adversary on the same exponentially large set. Lemma 3 is the hardest piece: at it is tight at , while the ratio tends to as ; the printed proof verifies numerically, so a formal proof needs an argument valid for every . A naive attempt to prove the goal with a single adversary fails: one adversary only defeats either large or small learning rates.
Fin d → ℝ with entries in , so is the dot product. Coordinates and rounds are 0-based: the paper's odd rounds are the even indices.Finset.inf'; every statement requires nonempty, so no junk value enters.Contributions welcome: proofs of the milestones, a proof of Lemma 3 by any method, and reusable lemmas on exponential weights (normalization, closed form, monotonicity of weights along a constant adversary). The paper's proofs are in its App. A and App. C.
Stochastic gradient methods are the standard tool for minimizing an objective that can only be accessed through noisy gradient samples. Training a machine-learning model on sampled data, simulation-based optimization, and stochastic programs with endogenous uncertainty are all of this kind. In many of these applications the objective is nonconvex: the loss or the regularizer of a learning problem may be nonconvex, as may the expected cost of a simulation model.
Before 2013 the complexity theory of stochastic approximation (SA) was essentially a convex theory. Robbins and Monro (1951) introduced the method. Polyak and Juditsky (1992) and Nemirovski, Juditsky, Lan and Shapiro (2009) established optimal rates for convex problems, and Lan (2012) unified the smooth, nonsmooth and stochastic convex cases. None of these results covered nonconvex objectives. Ghadimi and Lan (2013) gave the first non-asymptotic complexity bound for a stochastic gradient method on a smooth nonconvex problem. The bound is stated for the expected squared gradient norm at a randomly chosen iterate, and it is the result this mission formalizes.
The problem is
where is differentiable and bounded below, and its gradient is -Lipschitz: for all . This class is written . The function need not be convex.
The gradient is accessible only through a stochastic first-order oracle: at the -th query point it returns , where are random variables and is a Borel function. Assumption A1 asks that for every , conditionally on the past, is an unbiased estimate of , and that its error has second moment . The noise variables need not be independent of each other or of the iterates.
The randomized stochastic gradient (RSG) method takes an initial point , an iteration limit , stepsizes and a probability mass function on . It draws a random index , runs
and outputs . The mass function used in the main theorem is
The constants are and, in the convex case with minimizer , .
If for , , and has the mass function above, then under Assumption A1
where the expectation is over and the noise. Any stepsize sequence below is allowed, so the goal does not fix a step rule, and the step rules of the paper's corollaries follow from it.
Theorem 2.1 b) bounds by when is convex with a minimizer. Corollary 2.2 specializes both bounds to the stepsizes :
and the analogous bound with for in the convex case.
Theorem 2.1 a) is the basic guarantee for stochastic gradient descent on smooth nonconvex objectives. With the stepsizes of Corollary 2.2 it shows that oracle calls suffice to reach . The paper builds two further methods on it: a two-phase variant with large-deviation guarantees, and a zeroth-order variant (RSGF) that uses Gaussian smoothing when only function values are available. Later analyses of variance-reduced and adaptive stochastic methods for nonconvex problems measure their improvements against this bound.
The result is proved on paper; no machine-checked proof of it is known. A formalized fixed-step bound of the form "some iterate among the first has small expected squared gradient" exists, but it is a different statement: it has no randomized output and no general stepsizes. A complete formalization would check the measure-theoretic content that the paper treats informally: integrability of the iterates' gradients, the conditional-expectation step under dependent noise, and the role of the independence of .
The algebra of (2.8)–(2.9) is routine. The difficulty is in the probability. The noise may depend on the past, so the cross term vanishes only in conditional expectation, and only once is known to be measurable with respect to the past. Its integrability is not assumed anywhere: must be shown to have a finite second moment from the recursion, the Lipschitz gradient and Assumption A1. The randomized output adds a second step, where is rewritten as a weighted average. This needs independent of the noise, and has to be exhibited as a measurable function of the noise sequence. A proof that replaces by the deterministic weighted average skips exactly this step.
EuclideanSpace ℝ (Fin n). is the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth f g L, with the gradient given as a map . is the greatest lower bound of the range of , not an arbitrary lower bound.Stochastic programs and chance-constrained models in operations research contain expectations of the form
where is a random input under an unknown distribution , is a decision and is a known loss. In practice is seen only through i.i.d. data . Distributionally robust optimization (DRO) replaces the unknown expectation by the worst case over a set of plausible distributions, and a recurring question is how large that set should be so that the robust value is a statistically valid bound, without being needlessly conservative.
The usual answer, for divergence-based sets on a finite support of size , sets the radius from a quantile (Ben-Tal et al. 2013). This guarantee holds simultaneously for every function of the distribution, and so it is loose for a single expectation, and it degrades as grows. H. Lam (arXiv:1605.09349, Operations Research 2019) observed that if the ball is placed around the empirical distribution and measured with the Burg entropy, the right radius uses one degree of freedom, whatever the support. The DRO bounds then form an asymptotically exact confidence interval for . The mechanism is the empirical likelihood method of Owen (Owen 1988; Owen 2001).
Timeline:
Data: are i.i.d. random elements of a measurable space under . A decision is fixed, and is measurable with .
The empirical Burg-entropy divergence ball of radius is the set of weight vectors on the data points
with . It is the -divergence ball around the uniform weights for the Burg generator . Let be the -quantile of the law, i.e. for . The empirical DRO bounds are
For a sample and a value , the profile empirical likelihood statistic is
equal to when no weight vector is feasible.
The event is two-sided and joint. No rate is claimed.
Theorem 2 says that a robust optimization formulation with a data-driven Burg ball of radius yields an asymptotically exact confidence interval for an expected loss, independently of the support size of . Proposition 2 is the bridge: it identifies the DRO interval with the empirical likelihood confidence region, so any distributional result on transfers to the DRO bounds. This is the pointwise basis of the paper's later results on feasibility of chance and expectation constraints.
The result is proved in the paper, and Theorem 1 is classical. To our knowledge none of these statements has a machine-checked proof. Formalizing them requires the empirical likelihood theorem in Lean, which is reusable well beyond DRO (empirical likelihood tests and intervals for means). The Open platform theorem GenEmpLik.Coverage.theorem_3 (Duchi, Glynn and Namkoong) implies the goal when its decision set is the single point and its generator is with radius ; it is a different, more general statement and is not proved. Likewise the Open GenEmpLik.Expansion.lemma_7 implies Lemma 3, and the Proved NumStochOpt.ListScheduling.lemma_8_1_i_max_over_sqrt_ae gives Lemma 3 after passing to .
Proposition 2 is a finite-dimensional convexity statement, but it needs attainment of the minimum defining , which holds only because the objective blows up at the boundary of the simplex. The central difficulty is Theorem 1. The optimal weights are explicit only through a Lagrange multiplier that solves a nonlinear equation; to expand one must first show , which requires controlling the largest observation by Lemma 3 together with the law of large numbers for , and then bound the cubic Taylor remainder of uniformly in . A direct appeal to the central limit theorem for the sample mean does not suffice, since is an implicitly defined optimal value, not a smooth function of the mean.
ξ : ℕ → Ω → Ξ, measurable, mutually independent and identically distributed, indexed from ; the size- sample is fun i : Fin n => h x (ξ i ω).MemLp (h x ∘ ξ 0) 2 together with 0 < variance. Positive variance cannot be dropped: for a constant loss the coverage is .gaussianReal 0 1 {y | y^2 ≤ q} = ofReal (1 - α) with ; it is not a free parameter, and it is not the normal quantile.GenEmpLik.Expansion.robustMean burg (q/2) (its ball has radius , so ); the lower bound is its infimum twin robustLower. The ball uses the published probUncertaintySet and phiDiv.elStat minimizes over strictly positive weights with the empty infimum equal to . Lean's junk value therefore never enters: a formalization with and real logarithms would admit boundary weights with spurious finite divergence and is ruled out. For the value sets of the DRO bounds are nonempty and bounded, so the real infimum and supremum are not junk values.Contributions welcome: proofs of Proposition 2 and Lemma 3 (from the Proved reference), the KKT analysis (49)–(52), and a Lean empirical likelihood theorem.
A set of agents must share a set of indivisible goods, each agent valuing bundles of goods by her own valuation. Two fairness notions dominate the literature. Envy-freeness up to any good (EFX), introduced by Caragiannis, Kurokawa, Moulin, Procaccia, Shah and Wang (EC 2016), asks that no agent prefer another's bundle once any single good is removed from it. The maximin share (MMS), proposed by Budish (JPE 2011), asks that every agent receive at least what she could secure by splitting the goods into bundles herself and taking the worst one.
Neither notion is known to be achievable in full. Whether complete EFX allocations always exist is open in general. Complete MMS allocations need not exist: Procaccia and Wang (EC 2014) gave a counterexample with three agents, and the best known approximation factors for additive valuations are (Ghodsi et al., EC 2018) and (Garg and Taki, arXiv:1903.00029). Amanatidis, Birmpas and Markakis (IJCAI 2018) showed that every complete EFX allocation is a -MMS allocation.
Caragiannis, Gravin and Huang (EC 2019) showed that EFX can be achieved if some goods are left unallocated, with no bound on how many. Chaudhury, Kavitha, Mehlhorn and Sgouritsa (arXiv:1907.04596, SODA 2020, SIAM J. Comput. 2021) relax completeness instead: some goods may be "donated to charity". Their Theorem 8 produces an EFX partial allocation in which nobody envies the donated set and the donated set has fewer goods than there are unenvied agents. This mission formalizes their Theorem 14: such an allocation also gives every agent a maximin-share guarantee that improves as more goods are donated.
Agents are and goods are , . Agent has a valuation , assumed additive: for every .
A (partial) allocation gives agent the bundle , the bundles being pairwise disjoint. The pool of unallocated goods is , and .
the maximum over partitions of into possibly empty bundles. Agent 's maximin share in the instance is .
The three conditions of Theorem 8 on are:
For every allocation with pool satisfying conditions 1–3, and every agent ,
The factor ranges from when to when .
Theorem 14 shows that leaving goods unallocated is not merely a cost: under conditions 1–3, each donated good buys a quantitative improvement of every agent's maximin-share guarantee, interpolating between the factor the bound gives when the pool is empty and a factor tending to when nearly goods are donated. Together with Theorem 8 it shows that a single allocation can be simultaneously EFX, envy-free towards the charity, small in its charity, and approximately MMS. The same reduction (Proposition 13 applied to a carefully chosen sub-instance) is the template for the paper's -groupwise-maximin-share result, Theorem 16, formalized in mission III of this series.
The result is proved in the paper; no machine-checked proof of it, of Proposition 13, or of the existence of EFX allocations with bounded charity is known to exist. The mission produces a formal maximin-share definition on arbitrary subsets of goods with an arbitrary number of bundles, a formal proof of the monotonicity of the maximin share under removal of agents and goods (Proposition 13, which the paper quotes without proof), and the guarantee itself. Combined with mission I of this series (Theorem 8), it yields the printed existence statement.
The guarantee compares an agent's own bundle with a benchmark defined over all partitions of all goods, while EFX and the source condition speak only about the allocation at hand. The obvious attempt, summing over all agents and adding the pool, gives only a factor near and ignores the pool's size. Agents holding a single good are the obstruction: EFX gives no bound on the value of their bundles relative to , and the benchmark is defined on the full instance, which contains them. Proposition 13, the comparison of maximin shares across instances, is a combinatorial statement about all partitions of the original instance and requires nonnegativity of the valuations: with a good of negative value it fails.
Agents are Fin n (0-based) and goods Fin m; the set is the whole of Fin m. Valuations are functions Fin n → Finset (Fin m) → ℝ; additivity is the sum formula together with nonnegativity, which is the paper's codomain . An allocation is a family of pairwise disjoint finsets and the pool is always computed as the complement of their union, never taken as a free parameter. Sources are agents of indegree zero in the envy graph (nobody envies them), not agents who envy nobody. The maximin share is a supremum over labellings Fin m → Fin k' restricted to of the minimum bundle value; it is used only with , which every statement has in its hypotheses or derives from them (in the goal, condition 3 forces ). Every cardinality is cast to before division or subtraction, and under condition 3, so no division by zero occurs.
The goal is posed as an implication for every allocation satisfying conditions 1–3, rather than as the paper's "there exists an allocation"; the paper's proof of the MMS bullet uses only those three conditions, and existence is Theorem 8. The Nash-social-welfare bullet of Theorem 14 is not posed: it depends on Lemma 12, which takes the allocation of an earlier paper as a black box. The goal cannot be trivialized by a free pool, by overlapping bundles, by zero agents (condition 3 excludes them), by a junk maximin share over zero bundles, or by natural-number division; the statement keeps all three conditions, each of which is needed.
Contributions welcome: a library-quality maximin-share API for additive valuations (attainment of the maximum, monotonicity, the proportional bound), which is reusable for other MMS results; proofs of the milestones; and the final assembly.