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?
Online learning studies decisions made before their costs are known. An algorithm selects a point, observes a loss, and repeats. Regret compares its accumulated loss with the loss of one fixed point chosen after the sequence is known. Upper bounds show what a particular algorithm can guarantee; a lower bound shows what every algorithm must sometimes suffer. The distinction matters when deciding whether a rate such as can be improved by changing the update rule. Chapter 5 of Orabona's Online Learning: A Modern Introduction Using Convex Optimization addresses this question for online linear optimization.
The chapter begins with bounded decision sets and then examines unbounded decision spaces. On bounded sets, the main result gives a quantitative obstruction with an explicit constant for every deterministic algorithm. The book compares that order with the regret upper bound for online subgradient descent: the square-root dependence on the number of rounds is optimal up to a constant factor under the same loss-scale and diameter parameters (Orabona, Theorem 5.1 and discussion, pp. 50–51). The same chapter shows a different phenomenon for unprojected subgradient descent with steps that decay too slowly: its regret can have order for (Orabona, Theorem 5.4, p. 52).
Let be a nonempty subset of Euclidean space . On round , a deterministic online algorithm selects using only the loss vectors from rounds . It then observes and pays the linear loss . The adversary may select any loss vectors satisfying . This is the online linear optimization protocol used in the chapter; it also supplies lower bounds for online convex optimization because linear functions are convex (Orabona, §5.1, p. 50).
For a fixed competitor , define
The competitor is fixed across all rounds, although it may be selected after the loss sequence. The algorithm must make its own choices causally. These two quantifier positions are part of the mathematical claim. In particular, the hard sequence and competitor can depend on the algorithm, while the algorithm cannot use a future loss vector to choose its current prediction.
The bounded setting also uses the diameter . The theorem assumes is closed, bounded, and convex, and that . In finite-dimensional Euclidean space, closedness and boundedness make compact, so this maximum exists. The positive diameter excludes a singleton feasible set, where the algorithm and the only comparator coincide. These hypotheses and the diameter convention are stated in Theorem 5.1, pp. 50–51.
The goal is the chapter's Theorem 5.1. For every deterministic algorithm on such a set , every positive integer , and every nonnegative loss scale , there are bounded loss vectors and a competitor for which
The book prints the exact factor . The scale appears in its conclusion and in the restriction but is not introduced before that sentence, so the formal statement quantifies it explicitly. At , the bound reads zero; for it gives a positive lower bound when and (Orabona, Theorem 5.1, pp. 50–51).
Three milestones support and contextualize the goal. The first is the real-coefficient, lower-bound case of Khintchine's inequality, which controls the mean absolute value of a weighted sum of independent random signs (Orabona, Theorem A.14, p. 296). The second is the finite first-moment principle: a random sequence whose expected loss is at least has an outcome with loss at least (Orabona, §5.1, p. 50). The third records the lower-bound example for unprojected online subgradient descent with step size :
This last target uses the book's threshold and (Orabona, Theorem 5.4, p. 52).
The goal rules out an worst-case regret guarantee for deterministic online linear optimization under a fixed positive loss scale and positive diameter. Because the result applies to every nonempty bounded closed convex with , it does not rely on a symmetric feasible set or a chosen cube. The explicit constant permits direct comparison with concrete algorithmic guarantees. Theorem 5.4 separately identifies a failure mode for unprojected online subgradient descent on an unbounded domain. Both conclusions are proved in the book; the remaining task here is to give their statements and supporting objects machine-checkable Lean meanings, then prove them in Lean. Hazan's related lower bound uses a hypercube instance and an unspecified absolute constant, so it is related context rather than the same formal target.
A hard sequence must be chosen after the algorithm is fixed and must respect the algorithm's information at every round. A sequence selected independently of that quantifier order need not be hard: an algorithm tailored to a known sequence can choose its best fixed point on every round. The bound must also hold on any convex body with positive diameter, including sets whose geometry is asymmetric. The proof therefore needs a way to extract a uniform numerical lower bound from only the diameter and the loss norm bound, while retaining the algorithm's causal dependence on earlier losses (Orabona, §5.1, pp. 50–51).
Lean represents by EuclideanSpace ℝ (Fin d), with vectors and decisions indexed from round one; index zero is unused. A deterministic algorithm is a function of a full loss sequence together with an explicit non-anticipation condition. Its outputs are required to lie in . Regret is a finite sum against one fixed competitor. The positive horizon, positive diameter, closedness, boundedness, convexity, and nonemptiness are explicit. This rules out trivializing the goal by using a singleton domain, an anticipatory algorithm, or a fixed hard sequence that precedes the algorithm's quantifier.
The Khintchine milestone uses the uniform distribution on a finite Boolean cube; each Boolean coordinate represents an independent Rademacher sign. Its expectation is an ordinary finite average and is always defined. The finite first-moment milestone uses arbitrary nonnegative weights summing to one. Theorem 5.4 uses linear losses of norm at most one in arbitrary positive Euclidean dimension, which are convex and -Lipschitz. Its auxiliary function is used only for , where the printed formula's denominators are nonzero. The separate limiting claim about and the later coin-betting lower bounds are outside this mission's current milestones. Contributions establishing the Rademacher inequality, the geometric lower bound, the causal regret argument, and the unprojected descent example all fit this scope.
In online convex optimization, a learner chooses a point before seeing the loss assigned to that round. Its performance is measured against a fixed point that could have been chosen after the full sequence became known. A learner that merely minimizes accumulated past losses can react sharply when successive losses favor different points. Follow-the-Regularized-Leader (FTRL) changes that decision by adding a regularizer to the past losses. Chapter 7 of Orabona's Online Learning: A Modern Introduction Using Convex Optimization develops the resulting regret guarantees for a general norm, time-varying regularizers, and convex losses. This mission targets its first explicit square-root regret bound, Corollary 7.6, together with the equality and stability statements used to analyze the algorithm.
The general-norm formulation matters because different feasible sets make different norms natural. A Euclidean constraint set and a simplex, for example, need not give useful bounds under the same geometry. The chapter states the central inequality using the norm of the learner's decisions and the corresponding dual norm of loss subgradients. Its regularizer may vary with time, which lets the same result describe a learning-rate schedule chosen before each loss is observed.
Let be a nonempty, closed, convex subset of a finite-dimensional real normed space . In round , the learner outputs , then receives a loss function and incurs . For a fixed comparator , regret is . The comparison point stays the same across all rounds; it is not a round-by-round optimum.
FTRL supplies a sequence of regularizers . At the start of round , it selects any minimizer of the regularized cumulative loss
The sum contains only past losses. Its empty value at means minimizes . The analysis also names and ; that extra iterate occurs after the last charged round. A loss subgradient at is a continuous linear functional with for every . Its operator norm is the dual norm . The norm in the strong-convexity and stability statements is the norm on .
The goal is Corollary 7.6 on printed page 102. Let be closed and -strongly convex on , with , and let . The round- regularizer is , with . If the losses are subdifferentiable on , the first target is the bound, for every and every choice of subgradients ,
The last sum records the change in the regularizer; it is part of the stated result. The second target uses losses that are -Lipschitz on an open neighborhood of and the specified schedule , for :
The goal records both conclusions. Its milestones are the exact regret identity of Lemma 7.1, the stability inequality and minimizer assertion of Lemma 7.5, the proximal-regularizer variant of Lemma 7.7, and the linear-perturbation stability result of Lemma 7.49. The last result extends the chapter's stability theme beyond the immediate proof of Corollary 7.6.
The second inequality gives an explicit bound with a comparator-dependent regularization term, without imposing a finite diameter on . The first inequality retains the complete dependence on the chosen step sizes and on changes in the regularizer. A reader can therefore see what a schedule must control before specializing to the square-root choice. These are results already proved in the cited textbook; the open work in this mission is their Lean formalization, along with proofs of the stated milestones.
Formalizing the chapter would provide reusable statements about minimizers of strongly convex functions, subgradients in a dual normed space, and the stability of regularized minimization. The identities and stability bounds also connect FTRL's update rule to regret estimates without tying the interface to a single Euclidean norm or a single learning-rate choice. The definitions are intended to be usable by later chapters that employ linearized or optimistic FTRL, although those later results are outside this mission's goal.
The algebraic regret identity is exact, but it still contains the losses on both sides of the comparison. It does not by itself provide an explicit upper bound. The challenge is to control the change between successive minimizers while the objective and regularizer both change, then retain the correct index shift in the regularizer terms. In the general-norm setting, a subgradient is a dual vector; treating it as a primal vector would change the inequality's meaning. The corollary also has two quantifier patterns: its first bound covers every admissible subgradient sequence, while its second uses a particular learning-rate schedule and a Lipschitz condition.
The Lean development uses a finite-dimensional real normed space. Losses and regularizers are real-valued functions on that space, and minimization is restricted to . This is the chapter's finite-valued regime of its broader extended-real notation. A closed function on is represented by the closed epigraph of its restriction. Strong convexity is Mathlib's StrongConvexOn; a subgradient is a continuous linear functional and its operator norm is the book's dual norm. Subdifferentiability is required at every feasible point. The Lipschitz condition is stated on an open set containing , as on the page.
Indices start at for rounds and at for step sizes. The theorem requires , positive step sizes, and positive values for every quantity used as a denominator. The minimum is supplied by a point attaining it, and an FTRL run is a sequence of actual minimizers through round . This rules out a sequence of arbitrary feasible decisions or a regularizer schedule unrelated to . The first inequality retains the regularizer-change sum even when step sizes are not monotone. The book's one-line proof remarks that this change is nonpositive under an unstated monotonicity condition; the printed statement itself does not impose that condition.
The definition layer and all four milestone statements are in scope. Contributions proving any of them, or developing general lemmas about closed strongly convex objectives and dual-space subgradients that they need, fit this mission. The only simplification is replacing extended-real losses by real-valued losses on the feasible region, so no infinite value or undefined extended-real subtraction enters a displayed bound.
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.
In stochastic programming the objective is an expectation that cannot be evaluated, and an algorithm sees only noisy gradients drawn from a stochastic first-order oracle. Stochastic gradient descent and its relatives are the standard methods. For convex the optimal rate is known: Lan's accelerated stochastic approximation method (Lan, Math. Program. 2012) reaches an expected optimality gap of order after oracle calls. For smooth nonconvex , Ghadimi and Lan's randomized stochastic gradient (RSG) method (arXiv:1309.5549, SIAM J. Optim. 2013) bounds the expected squared gradient norm at a randomly chosen iterate, but it is only nearly optimal when happens to be convex.
Saeed Ghadimi and Guanghui Lan (arXiv:1310.3787v1, 2013; Mathematical Programming 156, 2016) combined the two lines: the randomized stochastic accelerated gradient (RSAG) method has a guarantee for nonconvex problems, and with suitable step sizes it attains the optimal rate on convex ones. This mission formalizes that result, Theorem 3 of the paper, together with the steps of its proof in §3.1.
Let be differentiable with Lipschitz gradient: for all , with . Gradients are available only through a stochastic oracle: at its -th call, with input , it returns , where are random variables on a probability space and is jointly measurable.
Algorithm 3 (RSAG). The inputs are , step sizes , for , , , an iteration limit , and a probability mass function . A termination index with is drawn first, independently of the noise. With , for ,
and the method stops at and outputs . The oracle error is .
Assumption 1 asks that the oracle be unbiased, , with variance . The paper does not require the to be independent.
The weights are , , and for a horizon
Fix . The expectations are taken over and .
a) If is bounded below with , for , and (3.4), then
b) If is convex with a minimizer , is nonincreasing (2.10), and (3.6), and (3.7), then
The goal keeps every printed constant and leaves the step sizes free. Corollary 3 specializes them; it is not part of this mission.
Part a): the quadratic bound (2.1) (already proved on the platform); a pathwise one-step inequality for (p. 16); a stochastic version of (2.17) bounding ; the summed inequality with martingale terms (pp. 16–17); its expectation (p. 17); the identity expressing as a -weighted average (p. 17); Theorem 3 a). Part b): Lemma 1 (p. 4); the convexity bound (2.21); (3.10) with a sign corrected; the stochastic version of (2.22); (3.11); its two consequences at (p. 18); the weighting identity for (p. 18); Theorem 3 b).
The result. Theorem 3 gives one stochastic first-order method with two guarantees. On a nonconvex problem it finds an approximate stationary point with an explicit bound on . On a convex problem its optimality gap matches the lower bound for stochastic convex optimization, which the RSG method does not. The method does not need to know which case it is in; only the step-size policy changes. Later work on accelerated and variance-reduced methods for nonconvex stochastic problems builds on the same analysis, and Theorem 4 of the paper extends it to composite problems with mini-batches.
Formalizing it. The result is proved in the paper and, as far as we know, has not been machine-checked. A formal proof would check the bookkeeping that a reader usually takes on trust: the nested sums in and , the conditional-expectation arguments that make a martingale difference sequence, and the passage from fixed horizons to the random output . The printed proof has small errors (see Formalization scope), so the formal statements record the corrected forms.
The deterministic analysis of the AG method (Theorem 1) bounds along a single trajectory. In the stochastic case the same chain produces cross terms and . These cross terms do not vanish pathwise, and the variance terms come with coefficients involving that grow backwards in time. The obvious argument would take expectations termwise. It fails unless one shows that each cross-term coefficient is measurable with respect to the past, so that its product with has zero mean under conditional unbiasedness. This also requires square-integrability of every iterate, which the hypotheses do not state and which has to be established by induction. A second difficulty is the random output: the bound is on , an integral over and the noise jointly, so the independence of from the noise has to be used explicitly.
EuclideanSpace ℝ (Fin n) (the published GhadimiLan.RSG.E n). is the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth Ψ g LΨ, with , and .GhadimiLan.RSG.AssumptionA1 applied to the middle points: for a filtration to which the noise is adapted, a.s. and . This conditional form is what the paper's martingale-difference step uses. It holds when the are independent, and it allows dependent noise, as the paper does.The following versions would make the goal trivial and are excluded: a deterministic oracle ( hard-wired), fixed to , an oracle not tied to , and an unconditional unbiasedness hypothesis too weak to support the martingale step.
A complete development needs conditional expectations of vector-valued random variables, square-integrability of the iterates, and the independence calculus for the random index. These parts are reusable for the companion RSG and mini-batch RSAG missions. Contributions are welcome on any milestone. The pathwise milestones (one-step bound, (2.17), (2.21), (2.22), (3.10)) need no probability theory.
The simplex method for linear programming moves from vertex to vertex along the edges of a polyhedron. A lower bound on the number of pivots of any edge-following method is the graph diameter of the feasible polyhedron: the largest number of edges needed to connect two of its vertices. Whether this diameter is bounded by a polynomial in the dimension and the number of facets is the polynomial Hirsch conjecture, open since the 1950s. The original Hirsch conjecture, , was refuted for unbounded polyhedra by Klee and Walkup (1967) and for bounded ones by Santos (2012) (doi:10.4007/annals.2012.176.1.7).
Timeline.
A polyhedron is the set of solutions of finitely many linear inequalities,
It need not be bounded. A vertex of is a point for which some half-space satisfies , equivalently an extreme point of . Two vertices are adjacent when for some half-space ; the segment is then an edge. A path of length is a sequence of vertices with consecutive vertices adjacent, is the least such , and the diameter is over pairs of vertices. A -polyhedron is a -dimensional polyhedron with facets, and
the maximum taken over bounded and unbounded polyhedra alike. All logarithms are to base 2.
The goal fixes no constant beyond the paper's own exponent and leaves no case of , or boundedness open.
The result. The bound is never larger than the Kalai–Kleitman bound. It equals the true value in dimensions 1 and 2, and it depends on only through the Hirsch quantity . Since , it is also symmetric under linear-programming duality, which exchanges the roles of and . For fixed it is polynomial in . It applies to the unbounded feasible regions that arise in practice in linear programming.
Formalizing it. The theorem has been proved since 2014. The platform has a proof of the bounded case only: Hirsch.todd_bound assumes , a nonempty interior and Bornology.IsBounded. This mission's goal extends it to all polyhedra, bounded or not, and to . That is the statement the paper proves, and the one an analysis of the simplex method on unbounded feasible regions needs. The unbounded form of Lemma 1 and the common-facet bound are open on the platform as items of the Kalai–Kleitman series and are reused here. Klee's unbounded three-dimensional bound has no formal proof on the platform: the published Hirsch.klee_three_dimensional_bound and Hirsch.dimension_three_bound cover bounded polyhedra only. The bounded recursion Hirsch.kalai_kleitman_recursion and the bounded facet reduction Hirsch.facet_reduction are proved and may serve as models.
Two steps are hard. The first is the unbounded case. Statements proved for polytopes do not transfer directly, because an unbounded polyhedron may have no vertices or a single one, unbounded edges (rays) that are not edges of the graph, and redundant or implicit-equality rows. Each geometric milestone must hold for these. The second is Klee's three-dimensional bound, which the paper cites without proof. Assuming boundedness to apply the published polytope versions is ruled out: Klee and Walkup showed that unbounded and bounded diameters differ from dimension four on, so the unbounded case carries content of its own. The arithmetic milestones are elementary but sensitive to edge values of and the real power.
All statements use the published definitions Hirsch.Hpoly, Hirsch.Adj and Hirsch.DiamLE (Hirsch_model). Vertices are Set.extremePoints ℝ. DiamLE P B says that any two extreme points are joined by a walk of exactly steps, each step staying put or crossing an edge. So the bound includes connectivity of the vertex–edge graph.
DiamLE (Hpoly a b) B. This ranges over all polyhedra given by inequalities in , including lower-dimensional, empty and redundant ones. It is equivalent to the paper's statement: a lower-dimensional polyhedron of dimension with facets has .Real.logb 2 and the power is Real.rpow. A distance is at most exactly when it is at most the floor , abbreviated toddBound d n in the milestone on the ten cases. The clause is a separate conjunct, because in Real.rpow.Trivializing encodings are excluded: no Bornology.IsBounded hypothesis; no definition of by sSup over , which would be on unbounded families; no use of Hirsch.gdist, which is when no walk exists; and no dropping of the clause.
Contributions are welcome on every milestone. A complete development needs facial structure of unbounded polyhedra (facets as polyhedra one dimension lower, tight rows at vertices), the relaxation argument of Lemma 1, Klee's three-dimensional argument, and real-power and logarithm estimates. The facet machinery and Klee's bound are reusable for any diameter result on unbounded polyhedra.
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.
Many graph-colouring questions ask whether a proper colouring can be produced indirectly, from local data, instead of being assigned vertex by vertex. In the 1-2-3 Conjecture, the colours are produced by weighting the edges of a graph and colouring each vertex with the sum of the weights at it. Karoński, Łuczak and Thomason asked in 2004 whether weights from always suffice (J. Combin. Theory Ser. B 91 (2004)). The question started as a local version of the irregularity strength problem, where all vertices, not only adjacent ones, must receive different sums. It became one of the most studied problems on graph labellings. Surveys: Seamone (arXiv:1211.5122) and Grytczuk (DOI 10.1016/j.ejc.2020.103213).
Timeline.
Let be a finite simple graph and write for the neighbourhood of a vertex . A -edge-weighting is a function . The weighted degree of is
Two adjacent vertices have a coloring conflict if . The weighting is vertex-coloring if no edge is a coloring conflict, that is, if is a proper vertex colouring of .
If has a connected component consisting of a single edge (a component isomorphic to ), then for every , so no weighting is vertex-coloring. This is the only obstruction.
The proof uses a few further objects:
The Lean names are wdeg G ω v for , IsWeighting G k ω, IsVertexColoring G ω, NoK2Component G and IsGoodPartition G U R B.
If no connected component of is isomorphic to , then there is with
Every finite connected graph with has a vertex-coloring -edge-weighting. This is the statement the case analysis of the proof establishes. Theorem 1 follows by treating each component separately.
In the order the proof uses them:
The result. Theorem 1 settles a conjecture that was open for nineteen years. The constant is optimal: the triangle has no vertex-coloring -weighting (two of its three edges get the same weight, and then two vertices tie), and deciding whether a vertex-coloring -weighting exists is NP-complete (Dudek and Wajc, 2011). Theorem 1 also closes the sequence of upper bounds on the number of weights needed. Variants remain open: total weightings with vertex weights and edge weights (the 1-2 Conjecture), and list versions.
Formalizing it. The theorem is proved, in a 16-page paper. As far as is known it has no machine-checked proof. A formal proof would verify the case analysis at the end of the paper (pp. 11–14, about fifteen sub-cases with three auxiliary graphs), which is where errors in such arguments usually hide. The flow lemma is quoted from the 2023 paper and not reproved here. Formalizing it means proving an integral max-flow statement for a specific unit-capacity network, and the result can be reused for other flow-based weighting arguments.
The obvious approach is to fix the weights greedily, edge by edge or vertex by vertex. This fails because changing one edge weight changes two weighted degrees at once, so a repair at one vertex can create a conflict at a neighbour. With only three weights there is no room to absorb this. Every earlier bound above used the extra weight as slack.
The difficulty in the paper is parity. The construction needs the set of blue vertices to have even cardinality, and cannot always be made even. The proof therefore removes one or two vertices, applies one of three base lemmas, and re-inserts the vertices. That re-insertion may need one more round of weight changes along a path. Each sub-case has to keep track of parities, of exact weighted degrees on , and of the connectivity of simultaneously.
Representation.
SimpleGraph V on a finite vertex type V with decidable adjacency. The paper's "graph" is a finite simple graph: weighted degrees are finite sums, and the proof uses a maximum cut and vertex orderings.ω : Sym2 V → ℕ on unordered pairs. IsWeighting G k ω requires for every edge of ; values on non-edges are unconstrained and never used.G.neighborFinset v. Since in Sym2, the single sum equals both sides of Theorem 1's displayed inequality.G.between R B, induced on wherever that vertex set is not all of .Conventions that differ from the page. There are two, both disclosed in the item statements:
Lemma 5's condition is stated in , and Lemma 3's is computed in .
Ruled out. None of the following formalizations is faithful:
Infrastructure. A complete development needs:
The flow and cut definitions are stated for arbitrary finite graphs and can be reused. Contributions are welcome at every level: proofs of individual lemmas, general flow-decomposition results, and the final case analysis.
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 a stochastic multi-armed bandit, a player repeatedly chooses one of arms and receives a random reward drawn from the chosen arm's unknown distribution. The classical lower bounds of Lai and Robbins (1985) and Burnetas and Katehakis (1996) describe the regret of good strategies when the horizon tends to infinity: it grows like , with a constant determined by Kullback–Leibler divergences. They say nothing about small horizons.
Garivier, Ménard and Stoltz (Math. Oper. Res., 2019; arXiv:1602.07182v3) show that the regret has a definite shape over the whole range of : it is almost linear at first ("explore first"), and only afterwards logarithmic ("exploit next"). Their §3 gives three non-asymptotic lower bounds for the initial phase, each for a natural class of strategies. This mission is the third of them, Theorem 4 (p. 13): a collective lower bound on the total number of pulls of all suboptimal arms. It is the bound that remains informative when many arms are suboptimal, and it is the one illustrated for large in the paper's §3.4.
A bandit problem is a family of probability distributions on , each with an expectation . A model is a set of such distributions, and is in when every . Put .
At each round a strategy chooses an arm from the past rewards (possibly with auxiliary randomization) and observes a reward . The number of pulls of arm up to round is , and is the expectation when interacts with .
The set of optimal arms is , of cardinality , and the set of worst arms is , the arms of smallest mean. The paper defines a partial order: when for every optimal arm of and for every other arm. Two classes of strategies enter the theorem.
With the Kullback–Leibler divergence, the constant of the theorem is
The Bernoulli divergence is , (5).
For every model , every strategy pairwise symmetric for optimal arms and monotonic on , every bandit problem in and every ,
Theorem 4 bounds the regret from below through , (13). While is small compared with , the right-hand side of the theorem is of order , so the regret is linear: a reasonable strategy cannot avoid spending a constant fraction of the first rounds on the suboptimal arms. Unlike the per-arm bounds of Theorems 2 and 3, the bound concerns all suboptimal arms at once and does not degrade as grows; §3.4 of the paper shows numerically that it gives the stronger regret bound for many arms.
The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. A formal proof would exercise the published canonical bandit model of the platform (StochasticBandit, BanditPolicy, banditMeasure) on a genuine lower-bound argument with two auxiliary bandit problems, together with a local Pinsker inequality for Bernoulli divergences in that is reusable in other bandit lower bounds.
The obvious attempt applies the fundamental inequality (6) to and an alternative in which one suboptimal arm becomes optimal, as in Theorem 2. That gives a bound arm by arm, which deteriorates with and does not see the number of optimal arms; it also needs a hypothesis of the type "smarter than uniform", which is not assumed here. Nothing is known about how a general behaves on itself, so the two hypotheses on must carry all the information, and both are weak: Definition 3 only constrains pairs of optimal arms with equal laws, and only through the joint distribution of their pull counts under the canonical bandit measure; Definition 4 only compares problems ordered by . On the analytic side, the classical Pinsker inequality loses the factor and gives a weaker theorem, so a local refinement is required, and every divergence is valued in .
Arms are indexed by Fin K (the paper's arm is index ), with assumed in the goal. A bandit problem is the published BanditAlgorithm.StochasticBandit K, a strategy is a published BanditPolicy K (a family of Markov kernels from histories to arms; every strategy of the paper with auxiliary uniform randomization induces one with the same law of arms and rewards), and is the integral of the pull count against banditMeasure. A model is a Set (Measure ℝ) whose members are probability measures with an integrable identity, the standing assumption of §1.1–§1.2. Definitions 3 and 4 leave implicit and are read "for all "; in Definition 3 equality of distributions is equality of the image measures of the pair of counts, not of their expectations. , and take values in ; the goal assumes , since otherwise the printed bound is and a real-valued conversion would silently replace by . The Bernoulli divergence is defined as the divergence between two Bernoulli laws on , so it is where (5) is, rather than a finite junk value. The auxiliary problems of the proof are not constructed; the milestones quantify over them with their defining properties.
The paper's "In particular" clause, for , is not stated: it follows from the main display only when (at the main bound is negative), and whether it holds in general is not known here.
A formalization that weakens the strategy classes (full permutation symmetry, or equality of expected counts in Definition 3), drops the requirement that the problems lie in the model, or uses a real Bernoulli divergence with finite values at does not count.
A complete development needs the fundamental inequality (6) on the canonical bandit model (the subject of mission I of this series; the chain rule for the divergence of bandit measures is already proved on the platform), the symmetry argument on the canonical measure, Lemma 6 and Lemma 2. Contributions of any of these, and of the identity integrated against banditMeasure, are welcome; Lemma 6 and the symmetry lemma are reusable beyond this mission.
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.
A stochastic multi-armed bandit learner repeatedly selects one of finitely many arms and sees only the reward from the selected arm. The learner must gather information about uncertain rewards while trying to select high-mean arms. Expected regret summarizes the lost reward relative to always selecting an optimal arm, but regret alone does not explain how much sampling each particular arm must receive. Garivier, Ménard, and Stoltz study this allocation question directly in Explore First, Exploit Next: The True Shape of Regret in Bandit Problems. Their Section 3 gives lower bounds for small horizons, before the longer-run logarithmic behavior becomes dominant.
The paper's first small-horizon result concerns strategies that allocate at least a uniform share to every optimal arm, on every problem in a specified model. This requirement excludes a strategy that always selects one fixed label and succeeds only when that label happens to be best. Such a requirement still permits many adaptive policies; it constrains their performance on optimal arms rather than prescribing their decisions round by round. The result establishes a compulsory initial allocation to every arm, including one whose mean is below the best mean. It is Theorem 2 on page 10 of the pinned arXiv:1602.07182v3.
A bandit problem consists of probability laws on . At each round, a strategy chooses an arm using the observed past and randomization, then receives an independent reward drawn from that arm's law. The mean reward of arm is . Write , and call an arm optimal when . The count is the number of times arm is chosen during the first rounds. These objects and the information available to a strategy are specified in Section 1.1, pages 2–3.
A model is a collection of possible arm laws, each a probability measure with an expectation. The notation means that every arm law belongs to . A strategy is smarter than uniform on when, for every bandit problem in the model, every optimal arm , and every integer , it satisfies
This is Definition 2 on page 10. It imposes a lower bound on each optimal arm, even when several arms tie. The requirement is evaluated across the whole model, so a strategy cannot be declared smarter based only on its behavior on the one problem used in the theorem.
For a law , a real threshold , and the model , the information number is the infimum of over those whose mean exceeds . The infimum is if there is no such . This is the definition on page 4. It measures how close an arm law is, in Kullback–Leibler divergence, to another admissible law that would give it a mean above the present optimum.
The main target is Theorem 2. For a model , a strategy smarter than uniform on it, a bandit problem , every arm , and every integer , the finite- case states
The theorem includes optimal and suboptimal arms. Its printed companion says that when , the arm receives at least expected selections. In the formal statement this threshold is , which also expresses the intended case . Both claims come from Theorem 2, page 10.
The milestone list follows the source's intermediate claims. Lemma 6, page 20 bounds Bernoulli relative entropy using the maximum of over an interval. The proof of Theorem 2 on page 11 states that Bernoulli relative entropy increases in its second argument on the interval starting at its first argument. The same page applies the paper's fundamental inequality (6) to the fraction of rounds spent on one arm, then states a lower bound against a single alternative arm law. These are the four curated milestones for the main theorem.
The theorem turns a model-relative performance condition into a numerical constraint on early sampling. If an arm's law is close in divergence to a law that would make it best, then the bound keeps its expected pull count near the uniform allocation until the horizon is large enough for the term under the square root to matter. It identifies the divergence scale at which this particular guarantee becomes weak. The paper contrasts this absolute bound with later relative and collective bounds that capture different dependencies on the number of arms in Section 3, pages 10–14.
The mathematical result is proved in the paper. The remaining work in this mission is a machine-checked development of the statement and its source-backed intermediate inequalities in the canonical stochastic-bandit model. The published bandit structure, policy kernels, and information number provide reusable foundations. Shared definitions supply the Bernoulli divergence, model predicate, and expected pull counts; the local strategy class makes the hypothesis of this particular theorem explicit. The Bernoulli inequalities and the pull-count change-of-measure statement can be reused in other lower-bound results.
A performance condition about optimal arms does not directly constrain an arm that is suboptimal in the problem of interest. The small-horizon bound must remain valid even though the strategy may adapt to observed rewards, and the relevant alternative arm laws can have divergences approaching an infimum without attaining it. The paper's lower bound is therefore sensitive to the exact orientation of the two bandit problems, the expected count multiplying their divergence, and the boundary conventions for Bernoulli relative entropy. Replacing the infimum with a chosen alternative or changing a divergence to an ordinary real with an arbitrary boundary value would alter the statement.
Lean uses arms Fin K, indexed from zero; the paper indexes them from one. The horizon is a natural number, and counts are integrated against the probability measure on -round histories generated by a stochastic kernel policy. Such kernels represent the arm-and-reward histories induced by the paper's strategies with auxiliary randomization. The model is a set of probability measures on whose identity function is integrable. The published StochasticBandit, BanditPolicy, and ConsistentBanditPolicy definitions supply the basic problem, history measure, pull count, means, and .
Bernoulli divergence and take values in . The real square-root formula assumes : when it is infinite, the paper's right-hand side is , while converting infinity directly to Lean's real value would produce a false numerical bound. The starting bandit problem is explicitly in , a condition needed for the proof's use of Definition 2 on a one-arm modification, although the printed quantifier on page 10 omits it. The arm parameter guarantees ; every target assumes , so its real divisions by and have the stated meaning.
A faithful development must retain Definition 2's quantification over all model problems and each optimal arm, rather than only over the bandit problem used in the conclusion. It must use the full Bernoulli relative entropy, including infinite endpoint values, and the infimum over precisely those model laws with mean greater than . The local instance of (6) also assumes integrable arm rewards in both bandit problems, as Section 1.1 requires. Contributions that establish the four milestones, the companion threshold claim, or reusable count-integrability and divergence facts are in scope.
In a stochastic multi-armed bandit, a decision maker repeatedly chooses one of several unknown reward sources. Sampling an arm reveals its reward but uses a round that could have been spent on a better arm. A good strategy must therefore reduce sampling of inferior arms, yet it cannot stop sampling them too early: it must still distinguish the current problem from a nearby one in which an apparently inferior arm is best. This tension produces the logarithmic lower bounds that benchmark bandit algorithms.
Garivier, Ménard and Stoltz revisit that benchmark in Explore First, Exploit Next. Their Theorem 5 gives a finite-horizon lower bound with explicit terms beyond the leading logarithm. It concerns every uniformly super-fast convergent strategy on a well-behaved model, not a particular algorithm. The distinction matters when comparing an algorithm's upper bound to what any strategy with that uniform performance guarantee must pay. The theorem is proved in the paper; this mission asks for a machine-checked statement and proof of that established result.
There are arms. Arm has an unknown probability distribution over real rewards, with finite mean . The vector is a bandit problem. Its best mean is , and the gap of arm is . An arm with is suboptimal. A strategy selects an arm each round using the previous arms and rewards, possibly with randomization. Write for the number of times it selects arm by round , and for the expected count under the problem .
A model specifies the probability distributions that an arm may have. All its laws have a finite first moment, and a bandit problem is in when every arm law belongs to it. For a law and a target mean , the paper's minimal information cost is
where an empty infimum is . This measures how much the law of an arm must change to make its mean exceed . The Bernoulli divergence used in the intermediate change-of-measure bound keeps its infinite values at the boundary.
Let be the interior of the set of expectations of laws in . A model is well behaved when positive functions and satisfy, whenever , , , and ,
A strategy is uniformly super-fast convergent with constant when for every problem in , every suboptimal arm, and every . The same constant applies throughout. Finally, records the inverse-squared gaps of all suboptimal arms.
For each suboptimal arm let . The goal is Theorem 5, with and
For every satisfying , , , and , the target is
The milestones follow the paper's displayed bounds: the one-alternative inequality (15), the optimized inequality (17), the inverse-information-cost bound after (17), and the product inequality quoted immediately before Theorem 5. They preserve the same constants and the same .
The leading term is the familiar distribution-dependent sampling barrier. The explicit , , and quantify the correction at a finite horizon; the paper observes that their combined contribution has order under its conditions. This makes the result useful when an algorithm's upper bound includes a second-order term and one wants to know the scale that a lower bound permits. It also identifies precisely which model regularity and uniform strategy guarantee support that comparison.
Formalizing Theorem 5 would add a reusable finite-horizon lower bound to the bandit library. The published definitions of stochastic bandits, policies, pull counts, and supply the base model; this mission adds the paper's well-behavedness and super-fast convergence predicates and states the intermediate inequalities as separate targets. The paper's proof is established mathematically, while these mission statements remain open Lean theorems until solvers supply machine-checked proofs.
The information cost is an infimum over alternative reward laws, so the finite-horizon bound must remain meaningful when the feasible set is empty or its divergence is infinite. The displayed formulas also divide by that information cost and use logarithms of quantities involving the strategy's uniform constant. For Theorem 5, the explicit correction factors must all lie in the range where the paper's final product inequality applies. A purely asymptotic statement would discard exactly the constants and horizon conditions that distinguish this theorem.
Arms are Fin K, so the paper's arm has Lean index . A strategy is represented by Markov kernels on observed arm-reward histories; its expected pull count is an integral of a bounded count. The model consists of probability measures on with integrable identity. The information cost and Bernoulli divergence live in ; a finite positive cost is converted to a real number only where a displayed reciprocal requires it. The goal contains a suboptimal arm, which rules out the empty-arm and single-arm cases. The model's witness functions are total in Lean, with requirements only on their paper-defined domains.
The theorem explicitly assumes and , which are implicit in the paper's use of and . It also assumes : the printed proof invokes a product inequality requiring that sign, although the theorem prints only . The version of (17) in the milestone list assumes in the case of a negative logarithm. These conditions and the model's integrability prevent vacuous or totalized-value readings of the lower bound. Contributions toward the four displayed milestones, the required measure-theoretic change of measure, and the finite-horizon arithmetic are in scope.
A seller with several goods can sell them one at a time or offer a mechanism that links allocation and payment across goods. Separate selling asks the seller to solve a one-good pricing problem for each item. A general mechanism can offer lotteries and menus whose outcomes depend on the buyer's whole valuation vector. The difference matters because the buyer's private information covers several values at once, and an optimal multidimensional mechanism need not resemble an ordinary posted price. Hart and Nisan ask how much revenue is guaranteed by simple selling rules when the joint valuation distribution is unrestricted apart from the stated independence assumptions (Hart and Nisan, arXiv:1204.1846v3).
This mission isolates their two-good, identically distributed result, Theorem B. The paper first gives a one-half guarantee for two independent goods with potentially different distributions, then improves the guarantee to when their distributions agree. The improvement is a claim about every probability law on nonnegative values. It assumes neither a density nor a regularity condition on the tail of that law. The paper proves the result in Appendix A.1 after stating it in the introduction (Hart and Nisan, pp. 6 and 31–35).
There is one risk-neutral buyer and one seller. For two goods, the buyer's private valuation is a vector with . Values are additive: receiving both goods is worth . The seller knows the distribution of the vector but not the realized values. In this mission, and are independent and have the same arbitrary probability law on . A law, rather than a named pair of random variables on a probability space, carries all the data needed by the revenue quantities.
A direct mechanism takes a reported pair and returns an allocation probability for each good and a real payment to the seller. The buyer's payoff from reporting truthfully is . The mechanism is incentive compatible (IC) if truthful reporting is at least as good as any other report for every possible valuation, and individually rational (IR) if truthful payoff is nonnegative everywhere. These requirements hold on the whole nonnegative orthant, as in Section 2.1 of the paper (Hart and Nisan, pp. 11–14).
Write for the expected payment under a valuation law and for the supremum of over feasible, IC, IR mechanisms. For one good, write . The separate-selling revenue for two identically distributed goods is . Equation (1) of the paper identifies the one-good value with the supremum of posted-price revenue ; the supremum formulation covers laws for which no maximizing price exists (Hart and Nisan, p. 12; Myerson, 1981).
The goal is the exact upper bound written at the start of the paper's proof:
Equivalently, separate selling guarantees at least of optimal revenue whenever the ratio has an ordinary meaning. The inequality itself is the stable formulation at zero and infinite revenues. The formal goal uses the exact constant , not the rounded percentage in the theorem's prose (Hart and Nisan, Theorem B, p. 6; proof, p. 31).
The milestones include the one-good posted-price identity, the fact that nonnegative payments suffice when optimizing, symmetrization for identical independent goods, Lemma 19's lower-valuation revenue bound, equation (12), and the two expectation estimates and final numerical bound used after it. Proposition 5's IC characterization is also a draft theorem, though it is not a milestone. Each statement retains its source's domain and the constant . The final inequality for the right side of (12) is stated for every nondecreasing allocation function into , as required by the paper's argument on pp. 33–35.
Theorem B gives a distribution-free quantitative guarantee for an easy-to-describe selling rule in a setting where the optimal rule may depend on the buyer's entire two-dimensional private type. Its guarantee is stronger than the one-half guarantee for merely independent goods stated as Theorem A. The conclusion concerns the best revenue available from all feasible IC and IR mechanisms, so the benchmark includes randomized allocations and payments depending on both reported values (Hart and Nisan, pp. 6 and 11–13).
The formalization target is a machine-checked version of a proved result, not a new conjecture. The proposal currently contains compiled Lean statements with unproved theorem bodies. A completed development would prove the stated inequality and its selected supporting results. It would also supply reusable definitions for direct mechanisms with additive nonnegative values, extended-real revenue, optimal revenue as a supremum, and symmetry of two-good mechanisms. No machine-checked proof of these proposed Hart–Nisan statements is claimed here.
The one-good posted-price formula does not directly control an arbitrary two-good mechanism: allocation of either good and the payment can depend on both reported values. Applying a one-good bound separately to the two coordinates therefore leaves terms that depend on the other coordinate. In particular, a direct comparison between each marginal posted-price optimum and the total payment loses the improved constant. The proof has to control the dependence created by a joint mechanism while retaining the exact numerical estimate. A second formal difficulty is that an admissible mechanism can have a negative expected payment even though optimal revenue is nonnegative, while an unrestricted law can give infinite optimal revenue. Replacing every expectation by an ordinary real integral or clipping each mechanism's revenue would change Lemma 19 and the intermediate inequalities (Hart and Nisan, pp. 31–35).
Valuations are finite vectors ; the main theorem fixes . The two-good law is the product of the same one-good probability measure in both coordinates, so independence and identical distribution are built into the data. The model represents allocation probabilities as real numbers with explicit bounds . It requires IC and IR pointwise on all reports. No positive transfer (NPT) means and is imposed only on supporting statements where the paper uses it. Following the paper's footnote 12, admissibility also requires the payment function to be measurable.
An individual expected payment is an extended real difference of positive and negative Lebesgue integrals. For IC mechanisms, the negative part is finite because the payment is bounded below by its value at zero. Optimal revenue is the supremum of the nonnegative clips of admissible mechanisms' expected payments; the zero mechanism makes this the same supremum as in the paper. Lemma 19 and equation (12) keep individual revenue in the extended reals. Supporting inequalities that write as a real number explicitly assume ; Theorem B does not. Integrals of bounded threshold functions use ordinary real expectation, while the nonnegative term uses a nonnegative Lebesgue integral. The goal cannot be satisfied by a correlated joint law, a bounded-support special case, a vacuous assumption on , or a rounded constant.
The reusable work includes one-good posted-price revenue for arbitrary laws, a nonnegative-transfer reduction, a faithful single-mechanism revenue type, and probability identities for two independent coordinates. Theorem A, Theorem 7, Theorem 16, and a full formalization of the paper's other selling rules are outside this mission.
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.
The Decision-Estimation Coefficient (DEC) of Foster, Kakade, Qian and Rakhlin (arXiv:2112.13487) is a single complexity measure that bounds the minimax regret of interactive decision making (bandits, reinforcement learning, and their structured variants) from above and from below. Its lower bound (Theorem 3.2 of the paper) states that every algorithm suffers expected regret at least a constant times , so concrete lower bounds on regret follow from concrete lower bounds on the DEC of localized model classes.
The multi-armed bandit is the first test of this program. Its minimax regret is classical (Auer et al., 2002; Audibert and Bubeck, 2010). Section 5.1 of the paper recovers it through the DEC: posterior sampling (Proposition 5.1) and inverse gap weighting (Proposition 5.2) bound the DEC by from above, and Proposition 5.3 bounds it by from below. The lower bound is proved through a hard family of models (Definition 5.1, Lemma 5.1), the device that the paper reuses for linear, ReLU and gap-dependent lower bounds in §§6–7.
A decision space is a finite set; here , the arms. A model assigns to every arm a distribution over rewards in (observations are trivial). Its mean reward is , and is an optimal arm. The squared Hellinger distance between distributions on a finite set is (no factor , the paper's (5)).
For a class of models, a reference model and , the DEC (2) is
With , the -localized class (12) is .
A reference model and models , , form an -family (Definition 5.1) if there are with , , and . is the Bernoulli distribution with mean .
For arms, and every , with ,
The mission also states monotonicity of the DEC in the class (the step from the family to the localized class), Proposition 5.1 (posterior sampling bounds the dual square-loss DEC by ), and Proposition 6.7, the gap-dependent variant: for bandits with gap exactly , some in the class has . Proposition 5.2 (inverse gap weighting) and the decoupling step of Proposition 5.1 are already proved on the platform and are included as references.
Proposition 5.3 is the DEC half of the minimax lower bound for multi-armed bandits: combined with Theorem 3.2 and , it shows that the general DEC theory loses nothing in rate on the most basic interactive problem, and that the upper bounds of Propositions 5.1 and 5.2 are tight up to constants. Lemma 5.1 is reusable: any lower bound on the DEC of a class can be obtained by exhibiting a hard family, and the paper uses it for linear bandits (Proposition 6.2), ReLU bandits (Proposition 6.6) and gap-dependent bounds (Propositions 6.7, 6.8).
The results are proved in the paper. As far as is known, none of them is machine-checked. A formal development provides a verified Bernoulli Hellinger bound, a reusable hard-family lemma for the DEC as published on the platform, and the first verified DEC lower bound for a concrete class.
The DEC is an inf-sup, so a lower bound must hold against every exploration distribution . A natural first attempt picks a single alternative model and compares; this fails because can concentrate on the arm where that alternative differs and then the Hellinger penalty cancels the regret. The family must be spread so that no single is good for all of its members at once, and the constants must balance the regret term against the information term at the chosen . In Lean, an additional difficulty is that the DEC is written with real sInf/sSup, which are on empty or unbounded sets: every lower bound requires showing that the relevant sets are nonempty and bounded, and passing from the family to the localized class needs monotonicity of the DEC, which the paper uses without comment.
m : S → Y → ℝ with every m π a probability vector; expectations are finite sums. The DEC is the published FoundationsRL.GeneralDM.decGf, the Hellinger distance hellingerSq, the mean reward fM.Y = Bool, reward on true), a subclass of the paper's all-distributions-on- class. The DEC is monotone in the class and the localized class shrinks with the class, so the Bernoulli lower bounds imply the paper's.piStar with the hypothesis that it picks a maximizer of ; every statement holds for every such selector, so for whichever maximizer the paper meant (the reference has every arm optimal).decGf evaluate to the junk value ; the goal is stated over a class containing with bounded rewards, so the inequality is the genuine one, and its right side is strictly positive.Contributions welcome: proofs of the milestones in attack order, sorry-free lemmas on nonemptiness and boundedness of the DEC's inner sets (reusable for every DEC lower bound in this series), and a proof of the gap-dependent companion.
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).