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?
Coordinate descent methods update one block of variables at a time. They are the method of choice when the number of variables is so large that even one full gradient is too expensive, while a single partial derivative is cheap: support vector machines, -regularized regression, and large sparse least-squares problems are the standard examples. Yu. Nesterov's paper Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012), doi:10.1137/100802001) gave the first global efficiency estimates for randomized coordinate descent, and these estimates started a large literature on random coordinate and block methods.
Many applications carry simple constraints on each block: bounds on each variable, a simplex or a ball per block. Section 4 of the paper shows that randomized coordinate descent handles such block-separable constraints at no loss: a projected block step, chosen uniformly at random, enjoys the same expected rate as the unconstrained method, and a linear rate under strong convexity. This mission formalizes that result, Theorem 5.
The space is split into blocks, with and every . A point is the family of its blocks , and is the point whose -th block is and whose other blocks are zero. Each block carries a Euclidean norm with (3.4).
The objective is convex and differentiable, and its gradient is coordinate-wise Lipschitz (2.2): writing for the -th block of the gradient, there are constants with
The weighted norm is (3.5). The function is strongly convex in with constant if for all (3.1).
The problem is (4.1), with and each nonempty, closed and convex. Its optimal value is , attained at an optimal solution . The constrained coordinate update (4.2) is
The uniform coordinate descent method UCDM (4.5) draws uniformly from and sets . Its expected objective is , the expectation over . The level-set radius is the largest -distance between a feasible with and an optimal solution.
For every ,
and, if is strongly convex in with constant ,
The result. Theorem 5 shows that the cost of a constrained problem with separable constraints is, up to the projection onto each , the cost of the unconstrained one: block steps for accuracy , and under strong convexity. The method needs no knowledge of ; the same iteration attains whichever rate applies. The Lyapunov function of (4.7) needs no level-set argument, so it applies wherever the projected step is cheap.
Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any rate for a randomized constrained coordinate method, appears in the Prove2Me catalogue or in Mathlib. The Prove2Me catalogue holds Bubeck's scalar, unconstrained random coordinate descent results (ConvexOptAlg.CoordDescent.*) and the deterministic Tseng–Yun coordinate gradient descent; neither covers a projected block step. A formalization produces the first verified rate for a randomized method with constraints, and a reusable model of block-structured spaces, block projections and expectations over random index sequences.
The unconstrained analysis of the paper (Theorem 1) bounds the distance to the optimum by a level-set radius and uses the decrease of a gradient step. Neither carries over: with constraints the gradient at the optimum need not vanish, so the decrease of a projected step is not controlled by the gradient norm, and the unconstrained recursion is not available. A different potential is needed, and its one-step estimate (4.7) is the central milestone. For the linear rate, the contraction factor must be shown nonnegative without assuming , which is where footnote 2 enters.
is the dependent product Blocks E , each a finite-dimensional real inner product space whose inner product is the paper's . Indices are 0-based. The dual norm is the operator norm of linear functionals, and is the Fréchet derivative of composed with the block inclusion. Random draws are explicit index sequences, so is the finite average of over all sequences of draws; no measure theory is involved.
Explicit choices where the paper is silent:
A formalization in which the update is an arbitrary point of or an unprojected gradient step, the draws are not uniform, or is the unconstrained minimum, proves a different theorem and is ruled out by the definitions above.
Needed infrastructure: existence and the variational characterization of the minimizer of a strongly convex quadratic over a closed convex set (Mathlib has projections onto closed convex sets in Hilbert spaces), the block descent inequality (2.3) obtained from (2.2), and manipulation of the finite expectations over index sequences (conditioning on the last draw). The block model, the weighted norm and the expectation are shared with the other missions of this series. Proofs of the milestones, and of (2.3) as a supporting lemma, are welcome.
Coordinate descent methods update one block of variables at a time. For problems with millions or billions of variables, where even one full gradient is too expensive to compute or store, a step that touches a single block can be orders of magnitude cheaper than a full gradient step. Nesterov's Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362, doi:10.1137/100802001) gave the first global complexity bounds for randomized coordinate descent on smooth convex functions: choosing the block at random makes the expected progress per step comparable to that of a full gradient step divided by the number of blocks.
Section 5 of the paper asks whether the multistep acceleration of the full gradient method (Nesterov 1983) carries over to the randomized coordinate setting, and answers it with the accelerated coordinate descent method ACDM. This mission formalizes that answer: Theorem 6, the expected rate of ACDM, together with the lemmas of its proof.
Timeline. Nesterov (1983) introduced the accelerated full-gradient method with rate . Nesterov (CORE DP 2010/2; SIAM J. Optim. 2012) proved the rate of random block coordinate descent and the rate of its accelerated variant ACDM. Later work (Lee and Sidford 2013; Fercoq and Richtárik 2015, arXiv:1312.5799; Allen-Zhu, Qu, Richtárik and Yuan 2016, arXiv:1512.09103) made the accelerated scheme efficient per iteration and sharpened its constants.
The space is , split into blocks. A point has blocks , and is the point whose -th block is and whose other blocks vanish. Each block carries a Euclidean norm with .
The objective is convex and differentiable, and has a coordinate-wise Lipschitz gradient: the partial gradient satisfies with constants . The method weighs blocks by these constants through the norm
The function is strongly convex in this norm with parameter if for all ; is plain convexity. A point minimizes , and .
The optimal coordinate step is , where maximizes . ACDM keeps two sequences with and deterministic scalars , . At step it computes from , sets and , forms , draws a block uniformly at random, and updates
, . The quantity is the expectation over the first draws.
For every , with ,
and, when ,
The result. Theorem 6 shows that randomized coordinate descent can be accelerated: the expected error falls as instead of the of the plain method, so after iterations (about full-gradient equivalents) the error is , the rate of the accelerated full-gradient method. For the same scheme converges linearly with a ratio governed by rather than . This is the starting point of the accelerated randomized coordinate methods (APPROX, NU-ACDM, accelerated proximal coordinate gradient) now used in large-scale machine learning.
Formalizing it. The theorem is proved in the paper; to our knowledge neither it nor any accelerated coordinate method has a machine-checked proof. The Lean development pins down a scheme whose correctness rests on a delicate parameter identity and on several conventions left implicit in the text (the range of , the reading of (5.3) at ).
The plain coordinate descent analysis tracks alone and fails to accelerate: one coordinate step gains only of a full gradient step, and a momentum term built naively from coordinate steps does not keep the expected progress. The accelerated proof needs a potential mixing the function gap with a squared distance , weighted by the deterministic sequences and ; the weights must make the cross terms in and cancel exactly after taking the expectation in the drawn block, which is what the coupled choice of achieves. The second difficulty is quantitative: the growth of follows from coupled recursions for and , not from a closed form.
Blocks E, the dependent product of finite-dimensional real inner-product spaces E i over Fin n (indices ); is absorbed into the inner product of E i. The dual norm is the operator norm of E i →L[ℝ] ℝ.Fin k → Fin n; and are finite averages over all sequences with weight . No measure theory is needed.Blocks, partialGrad, CoordLipschitz, coordStep, wnorm, expect) is shared verbatim with the other missions of this series. The coefficient lemmas (5.2), (5.4), (5.5) and the growth bounds are pure real analysis and welcome as standalone contributions; so is a Lean proof of the block descent inequality (2.3)–(2.4) for Euclidean blocks, which the potential inequality needs.ConvexOptAlg.NesterovSmooth.theorem_3_19). https://arxiv.org/abs/1405.4980City logistics often moves goods in two stages: large trucks bring freight from a central depot to a few intermediate satellites, and small vehicles distribute it from the satellites to the customers. The two-echelon capacitated vehicle routing problem (2E-CVRP) is the basic optimization model of such systems; it contains the capacitated location-routing problem as a special case. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) gave an exact method that solved benchmark instances out of reach for earlier algorithms.
Their method does not attack the whole problem at once. It enumerates configurations, sets of first-level (depot–satellite) routes, discards most of them with cheap tests, and solves a second-level problem only for the survivors. The correctness of the method rests on two facts stated in §5 of the paper: the problem decomposes exactly over configurations (Eq. (26)), and the pruning tests of Propositions 1 and 2 never discard the configuration of a solution better than the incumbent. This mission formalizes those facts.
An instance has a depot , satellites and customers , a symmetric cost on the edges (with the fixed vehicle costs folded in), positive integer demands with total , first-level vehicles of capacity , second-level vehicles of capacity at satellite with a global limit , satellite capacities and handling costs .
A first-level route leaves the depot, visits a set of satellites and returns; its cost is the length of the closed walk. A second-level route leaves satellite , visits a set of customers of total demand and returns; its cost is the walk length plus . Formulation chooses binary , and integer deliveries minimizing subject to: each customer on exactly one used second-level route; at most used routes at and in total; load at at most ; at most first-level routes; the deliveries to equal the load leaving ; each used first-level route carries at most . Its optimal value is , when infeasible.
The set of configurations is
For , , and . Problem is with the first-level routes fixed to : second-level routes only at satellites of , real deliveries for , and . Its value is when infeasible.
The bounds of §5.1 use multipliers , , and marginal costs satisfying the penalty system (12), for every route of satellite :
Let be a real number and a feasible solution of of cost less than , with configuration . Then and
Eq. (26) is what makes the method exact: once every configuration that can carry a solution better than the incumbent is examined, the best is the optimum. Propositions 1 and 2 are what make it fast: they remove configurations from before any second-level problem is solved. If a pruning test discarded the configuration of a cheaper solution, the method would return a suboptimal value and still report it as optimal; the formal statements rule this out for every instance, not just the benchmark ones. The capacity constraints (33) play the same role inside : a cut that removed a feasible solution would make the bound invalid.
The paper's proofs are in an electronic companion; none of these statements has been machine-checked before, and none is on the platform. The formalization also records exactly what the tests need: positive demands, integral vehicle counts, and the sign conditions on the multipliers, and nothing about the optimality of the incumbent.
Most statements are elementary counting and Lagrangean weak-duality arguments over finite index sets. The work lies in the bookkeeping between two formulations with different index sets: sums over all satellites, only over , and a solution of one must be turned into a solution of the other. One step is not elementary: has integer deliveries and real ones, so the inequality in (26) needs an integral delivery plan from a fractional one. That is an integrality property of a bipartite transportation problem (routes to satellites, integral capacities and demands), which no counting argument gives.
Satellites and customers are Fin ns and Fin nc, 0-based. The route families and are arbitrary finite families of elementary routes with costs computed along the closed walk; the paper uses all such routes, so every statement here is a generalization. Demands are positive integers; the triangle inequality is not assumed. Binary variables are Bool; optimal values are infima in EReal, with ⊤ for an infeasible problem. A configuration is a Finset of route indices. The penalties are any , , and satisfying (12), not only those producing the paper's bound LD1. Ceilings of and are natural-number ceilings of rationals; those in Proposition 2 are integer ceilings of reals.
The goal departs from the printed proposition in three disclosed ways. Only necessity is stated: the "if" direction is false, because (b)–(e) ignore the satellite capacities . Condition (a), , is omitted: it holds for some optimal solution, not every one (its split-delivery analogue is posed, and open, on the platform as SplitDeliveryVRPTW.Known.exists_optimal_split_customers; it is not reused here). "An optimal solution" becomes "a feasible solution of cost below ", the property the paper's own justification uses. Proposition 2 is stated with as a hypothesis; the paper's computation of by problem (27)–(32) is not formalized, because (32) forces positive deliveries that does not require. The goal is not trivialized by an infeasible hypothesis: feasible solutions of exist on small instances, and a toy instance was checked in Lean.
A complete development needs finite-sum manipulations, Lagrangean weak duality for (12), and, for (26), integrality of bipartite transportation polytopes, which is reusable well beyond this mission. Proofs of any milestone, and a general transportation-integrality lemma, are welcome.
Online convex optimization is a repeated game between a learner and an environment. In each round the learner commits to a vector, the environment then reveals a convex loss function, and the learner pays the loss of its vector. No statistical assumption is made about how the losses are generated; they may be chosen adversarially. Performance is measured against the best fixed vector in hindsight. This model underlies online prediction with expert advice, online regression and classification, portfolio selection, and the analysis of stochastic gradient methods through online-to-batch conversion.
Shai Shalev-Shwartz's survey Online Learning and Online Convex Optimization (Foundations and Trends in Machine Learning, 2011/2012) organizes most first-order online algorithms around a single template, Follow-the-Regularized-Leader (FoReL), and derives their regret bounds from one theorem: Theorem 2.11 (p. 138). Online gradient descent, the experts algorithm with exponential weights, and the bounds of Sections 2.6–2.8 of the survey are instances of it. This mission formalizes that theorem and the lemmas its proof rests on.
Timeline. Follow-the-Leader goes back to Hannan (1957) and the "be the leader" argument appears in Kalai and Vempala (2005). Regularized variants and their analysis via strong convexity were developed by Shalev-Shwartz and Singer (2007) and by Abernethy, Hazan and Rakhlin (2008); the survey (2011) presents the strong-convexity analysis in the form formalized here.
Let be a real normed space with norm and a set of admissible predictions. Rounds are numbered . In round the learner predicts , receives a loss function , and suffers . The regret after rounds with respect to a competing vector is (eq. (2.1))
Given a regularization function , Follow-the-Regularized-Leader predicts
with ties broken arbitrarily; in particular minimizes over . With this is Follow-the-Leader (FTL).
A function is -Lipschitz over if for all . A function is -strongly-convex over a convex set if, for all and with ,
Let be convex on , with -Lipschitz over , and let . If FoReL is run with a regularizer that is -strongly-convex over () with respect to the same norm, then for all
LogRegretOCO.FTAL.ftl_be_the_leader and referenced here.Theorem 2.11 is the result from which the survey's concrete regret bounds are read off. With the Euclidean regularizer it gives the bound of online gradient descent (Corollary 2.12), hence regret after tuning ; with the entropic regularizer over the probability simplex and the norm it gives the -type bounds for prediction with expert advice (Corollaries 2.13–2.14). Through online-to-batch conversion such regret bounds become excess-risk bounds for stochastic optimization.
The survey's proofs are complete, so the formalization adds no new mathematics; it produces machine-checked versions of the FoReL regret theorem, of the stability lemma, and of the quadratic-growth property of strongly convex functions over a general normed space and a general convex constraint set. To our knowledge none of these is in Mathlib. The platform already has the FTL lemma over (proved) and the special case of Lemma 2.8 with and the Euclidean norm (UnderstandingML.strongly_convex_lemma, part 3); the general statements are new here.
Lemma 2.3 and Lemma 2.1 use different round indexings (FoReL's regularizer plays the role of a round-zero loss), so Lemma 2.1 cannot be applied verbatim. The main obstacle is Lemma 2.8 on a constrained set without differentiability: the obvious argument sets the gradient at the minimizer to zero, which is unavailable when is not differentiable or the minimizer lies on the boundary of . A second point is that the strong convexity of must be derived from the convexity of the on , not on all of , and from the strong convexity of on .
Conventions committed to in the Lean statements:
E (NormedAddCommGroup E, NormedSpace ℝ E); no inner product is assumed. Every norm on , including as used in Corollary 2.14, is an instance. The Lipschitz and the strong-convexity hypotheses use the one norm of E, as the theorem requires ("the same norm").StrongConvexOn S σ R, the modulus form above. The survey's Definition 2.4 is stated with subgradients and a pairing ; the two agree for convex functions that have subgradients on , and the Mathlib form needs neither a dual space nor subgradients. With this choice Lemma 2.8 is a genuine lemma, not an unfolding of the definition.E, of which only the values on S matter; convexity is ConvexOn ℝ S. The survey's convention outside is the constraint .w 0 and f 0 are unused. A FoReL run is a predicate on the whole trajectory (IsFoReLRun), so every tie-breaking rule gives a run, and no argmin is chosen.sInf (R '' S). It is attained at whenever a run exists, so it is the true minimum, not a default value. The hypothesis is present only because of the factor .A trivializing formalization would make the run predicate unsatisfiable, so that Theorem 2.11 holds vacuously; the drafted predicate is satisfied by online gradient descent with on (Example 2.3), and that regularizer is -strongly convex, so the hypotheses of the goal are jointly satisfiable.
Out of scope, and welcome as follow-up work: the derived bounds (Corollaries 2.12–2.14), Theorem 2.15 (which needs dual norms), Lemma 2.9, Corollary 2.2 and the doubling trick. Contributions of general lemmas — strong convexity of a convex plus strongly convex function on a set, quadratic growth at a constrained minimizer — are reusable well beyond this mission.
Randomized coordinate descent updates one block of variables per iteration, chosen at random. For problems whose dimension makes even one full gradient expensive (the "huge-scale" problems of the title, such as sparse least squares or truss topology design), a coordinate step can cost a tiny fraction of a gradient step. Nesterov's paper (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362) gave the first global complexity bounds for such methods with non-uniform sampling, and it is the reference point for the later literature on randomized block methods (Richtárik and Takáč 2014, Lu and Xiao 2015, Allen-Zhu et al. 2016).
The first results of the paper (Theorem 1, the subject of a companion mission) bound the expected objective value after k iterations. An expected bound does not say what happens in a single run. This mission formalizes the paper's answer to that question in §3: by running the method on a slightly regularized objective, one run returns an ε-solution with any prescribed probability β, after a number of iterations that grows only logarithmically in 1/(1 − β).
The variable space is a product of blocks; a point has blocks , and is the point whose -th block is and whose other blocks vanish. In this mission each block carries a Euclidean norm with (3.4), and the whole space carries
The objective is convex and differentiable, has a minimizer with value , and its partial gradients are Lipschitz along their own block with constants (2.2): . Write .
The method RCDM (2.6) draws, independently at each step, block with probability and replaces by , where is a maximizer of (1.8). The quantity is the expectation of over the first draws.
The level-set radius is , and for the regularized objective is
It has block constants , so RCDM applied to samples block with probability and steps with .
For , , and
the point produced by RCDM on satisfies
Theorem 4 turns an in-expectation guarantee into a single-run guarantee with an explicit, non-asymptotic iteration count. Its dependence on the confidence level is logarithmic, so very high confidence costs little; and the count replaces the largest eigenvalue of the Hessian, which governs the full gradient method, by the trace-type quantity , which for sparse problems makes groups of coordinate steps competitive with one gradient step. Theorem 2 is the linear-rate result for strongly convex objectives that later analyses of randomized block methods take as their starting point.
The results are proved in the paper. None of them is formalized in the block setting. The scalar Euclidean case of Theorem 2 is proved on Prove2Me as ConvexOptAlg.CoordDescent.theorem_6_8 (Bubeck, Theorem 6.8), and the bound (3.2), for a -strongly convex in any norm, is proved as ConvexOptAlg.CoordDescent.lemma_6_9. This mission adds block variables with general norms (Theorem 2), the regularization constants, the gradient-norm bound, and the high-probability statement itself, which has no formalized counterpart.
The obvious argument fails. Theorem 2 controls the expected suboptimality of , not of , and Markov's inequality applied to does not reach accuracy ε: and differ by an amount comparable to ε, and the contraction factor itself depends on μ. Relating the run on to the original problem requires the global Lipschitz constant of in , which for is the weighted co-coercivity statement of Lemma 2 of the paper and is not a consequence of (2.2) alone without convexity. The constants of (3.11) are exact, including the factor 2 and the ½, so no estimate may lose a constant. Finally, the iterates depend on all previous draws, so even the finite-sum expectations need a careful account of linearity and of conditioning on the last draw.
Blocks E of finite-dimensional real spaces E i indexed by Fin n (0-based for the paper's 1, …, n). Euclidean blocks (3.4) are inner-product spaces, with absorbed into the inner product; Theorem 2 is stated for arbitrary normed blocks. The dual norm of a block is the operator norm of a functional.Fin k → Fin n; expectations and probabilities are finite sums weighted by . No measure theory is involved.Contributions are welcome on the probabilistic bookkeeping for expect (normalization, linearity, conditioning on the last draw, Jensen for a concave function), which is reusable by every mission of this series; on Lemma 2 of the paper in the block setting; and on the milestones in the stated order.
Load balancing on identical parallel links is the example Koutsoupias and Papadimitriou used to define the price of anarchy: the ratio of the social cost of a Nash equilibrium to the social optimum (Koutsoupias–Papadimitriou 2009). Theorem 3 of the journal version is the two-link case. It is the first sharp bound in that paper, and the later two-speed bound is proved by the same comparison.
There are agents and identical links. Agent has traffic and chooses a link. A pure profile assigns each agent a link. The load of link is the sum of the traffics sent there, and the cost of an agent is the load of its own link. A mixed profile gives, for each agent and link , a probability . Agents randomize independently.
The social cost is the expected makespan: the expected value of the maximum link load. The social optimum is the least makespan over pure assignments. The contribution probability is the probability that agent sits on the lexicographically first link of maximum load. The collision probability of agents and is .
Agents are Fin n and links are Fin m, numbered from 0. Payoffs are minus costs, so a Nash equilibrium is a mixed Nash equilibrium of that payoff game.
for every Nash equilibrium on identical links, and every positive traffic vector. This is the goal.
for a mixed profile. This is an identity in the proof of Theorem 3, not a Nash fact.
The bound is what the paper proves for two identical links, and it is tight. The two identities are the rewrite the proof treats as immediate: social cost as a weighted sum of contribution probabilities, and an agent's expected cost as its own traffic plus collisions. Formalizing them records those rewrites as statements with the side conditions the prose leaves implicit, in particular that is a profile of lotteries and that wherever a maximum load is taken.
The statements of this mission are the ones already published under WorstCaseEq.Identical. This proposal gathers them. It does not replace them.
The bound is not the definition of the ratio. Expanding the expectation produces a sum over pure profiles, and the lexicographic choice of the maximum link is there so that exactly one link is credited. Treating as the probability of an arbitrary maximum link makes (7) the wrong inequality. Positivity of the traffics is a hypothesis of Theorem 3, not of the two identities.
The model is the published definition WorstCaseEq_Identical_Model, on top of agt_games. Social cost and contribution probabilities require m nonempty. The expected-cost identity requires a mixed profile and does not require a Nash equilibrium. Theorem 3 fixes and requires every traffic to be positive.
A development that hard-codes two agents, or that proves the bound only for pure equilibria, is not this theorem.
Elias Koutsoupias and Christos Papadimitriou, Worst-case equilibria, Computer Science Review 3 (2009), 65–69. doi:10.1016/j.cosrev.2009.04.003. Theorem 3 and its proof, PDF pp. 2–5.
Many large optimization problems arising in machine learning, statistics and network analysis have so many variables that computing a single full gradient is already expensive, while a single partial derivative, or a gradient with respect to a small block of variables, is cheap. Coordinate descent methods exploit this: at each iteration they update one block of variables only. They are among the oldest methods of numerical optimization, but for a long time their worst-case efficiency was not understood, because deterministic rules for choosing the next coordinate (cyclic order, greedy choice) are hard to analyse globally.
Nesterov (2010/2012) showed that choosing the coordinate at random, with probabilities tied to the coordinate-wise Lipschitz constants of the gradient, yields clean global complexity bounds. This paper started the modern theory of randomized coordinate descent, which was then extended to composite objectives, parallel and accelerated variants, and became a standard tool for huge-scale problems. This mission formalizes the first of its results: the expected sublinear rate of the basic method RCDM (Theorem 1 of the CORE Discussion Paper 2010/2).
The variable is split into blocks, . Write for the -th block and for the point whose -th block is and whose other blocks vanish. Each block space carries a norm with dual norm .
The objective is convex and differentiable, and its set of minimizers is nonempty and bounded; is its optimal value. The partial gradient is the -th block of the gradient. The gradient is coordinate-wise Lipschitz with constants :
for all , and .
For a linear functional , is any maximizer of . The optimal coordinate step is . For let and . The method RCDM starts at and, for , draws independently with and sets . Its expected objective value is , the expectation over the draws .
The weighted norms are and , and the size of the initial level set is
For every ,
The statement holds for every real , every choice of the vectors , and every block decomposition with arbitrary block norms. With (uniform sampling) it reads .
Theorem 1 is the first global efficiency estimate for a coordinate descent method on general smooth convex functions. Its constant is governed by , an average of the coordinate Lipschitz constants, rather than by the global Lipschitz constant of the gradient; for and Euclidean blocks this makes the method competitive with the full-gradient method even when partial derivatives are not cheap, and much faster when they are. The later results of the paper (linear convergence under strong convexity, high-probability bounds, the constrained and accelerated variants, adaptive Lipschitz estimates) reuse the objects and the one-step estimates of this mission.
The result is proved in the paper; nothing in it is open. As far as we know it has not been machine-checked. The platform contains a related item, ConvexOptAlg.CoordDescent.theorem_6_7 (Bubeck's monograph, Theorem 6.7, open), which treats scalar Euclidean coordinates, , and the weaker factor ; together with its proved one-step lemmas (thm_6_7_coord_step, thm_6_7_expected_decrease) it covers the special case of milestones 3 and 5. This mission states the result in the paper's generality: arbitrary blocks and block norms, non-Euclidean dual norms through , every real , and the constant .
The bound is a statement about an expectation, not about individual runs: the recursion on needs Jensen's inequality, , and the fact that every run stays in the initial level set, so that controls along every path. Lemma 2 is the step that links the coordinate-wise condition (2.2) to the weighted full gradient, and it is easy to misjudge: it is false without convexity, since on satisfies (2.2) with arbitrarily small constants. The non-Euclidean block norms add a layer of convex analysis (the dual norm, the vector and its identities) on top of the probabilistic bookkeeping.
Blocks E of finite-dimensional real normed spaces; indices are 0-based. The norm Lean puts on the product is never used; statements use only the block norms and the weighted norms (2.7).E i →L[ℝ] ℝ; the partial gradient is the derivative of composed with the inclusion of block .IsSharpSelection); all results quantify over every selection.Contributions welcome: proofs of the one-step estimates (2.3), (2.4), (2.13), which need a block mean-value argument and the convex analysis of ; Lemma 2, which needs the convex conjugate argument of its proof; and the final summation argument. The block encoding and the identities for are reusable for every other mission of this paper.
Many problems in machine learning are finite-sum problems: minimize the average of loss functions, one per training example,
Two classical methods sit at opposite ends. Full gradient (FG) descent evaluates all gradients per iteration and converges linearly on strongly convex problems, at a cost proportional to per step. Stochastic gradient (SG) descent evaluates one gradient per iteration, independent of , but its error decreases only sublinearly, as .
Le Roux, Schmidt and Bach (arXiv:1202.6258, NIPS 2012) introduced the stochastic average gradient (SAG) method, which keeps the one-gradient-per-iteration cost of SG and attains a linear rate, as FG does. SAG was the first method of this kind and started the line of variance-reduced methods (SVRG, SAGA, Katyusha) that are now standard for finite sums.
The paper has two convergence results. This mission formalizes the second one, Proposition 2: when the number of examples is at least , SAG with the larger step size reduces the expected suboptimality by a constant factor per pass through the data, independently of the conditioning of the problem. Proposition 1 (step size , any ) is the subject of a separate mission.
Let with . The standing assumptions (p. 5, §3, and p. 13, §A.1) are:
Write and , the variance of the gradients at the optimum.
SAG. The state is : a table of stored gradients and an iterate . At iteration an index is drawn uniformly from , independently of the past, and
Warm start. Proposition 2 is about a specific run. The first iterations are stochastic gradient steps from with . SAG is then started from the average , with all set to and step size .
Lyapunov function. For parameters and , the proof uses
at , , .
If , the warm-started run satisfies, for every ,
The constant is the paper's own; the goal fixes it as printed.
In the order the proof uses them:
The result. Proposition 2 gives a rate per pass through the data, , that depends on neither nor once . On p. 6 the paper compares it with the FG rate and the accelerated FG rate . With , , , SAG iterations contract by at the cost of one FG iteration, while FG contracts by and accelerated FG by . The SG warm start replaces a constant proportional to by one of order , so the bound also captures the behaviour of the early iterations.
Formalizing it. The paper's proof is complete, and a machine-checked proof is new; no SAG statement exists on the platform. A formalization would check the paper's long appendix computation (pp. 23–29: a Lyapunov argument with completing the square on block vectors) and fix its slips: on p. 30 the proof writes , where its own Step 2 gives the factor , and the bracket that follows matches . Lemma 1 is shared with Proposition 1, and the SG bound of §A.3 is a standalone result (after Bach and Moulines, 2011).
The obvious approach does not work. SAG's update direction is a biased estimate of : the stored gradients were computed at old iterates. So the usual SG argument, an unbiased step followed by a bound on , breaks down. The proof instead tracks the joint state through a Lyapunov function that couples the table and the iterate, and it needs a function-value term to handle the large step . The one-step bound (pp. 24–28) is an inequality between quadratic forms in . It holds only after completing the square in the block, and it closes only under ; the margin there is small (). The domination step similarly minimizes over .
EuclideanSpace ℝ (Fin p), and the components are indexed by Fin n. and are the published SAGA.Convex.fAvg and SAGA.Convex.gradAvg.SAG.LargeStep.Assumptions. Strong convexity is stated in the paper's form: is convex. Each is convex (§A.1), and gradients are tied to the functions by HasGradientAt.Fin k → Fin n, weighted uniformly (SAGA.Convex.expectIdx), which is the law of independent uniform draws. A conditional expectation given is the average over the indices of one step from an arbitrary fixed state.hybrid draws indices. The SG phase uses the first , index is drawn and unused, and SAG uses the last , from with . The SG step sizes are .hybrid. Every hypothesis is satisfiable: , , , , .ConvexOptAlg.SmoothGD.eq_3_6) are reusable beyond this mission.Plünnecke-type inequalities turn information about a set and one product (or sum) of it into bounds on all of its iterated products. In an abelian group, Plünnecke's theorem (Plünnecke 1970) and its extension by Ruzsa say that implies for every . Such bounds are a basic tool in additive combinatorics, and their non-abelian analogues are used in the study of growth in groups (for example Helfgott's work on ).
Without commutativity the abelian statement is false. Petridis recalls the standard example (p. 2): let be a subgroup and an element with , and put ; then while . Small doubling alone therefore says nothing about tripling.
Timeline.
Let be a group, not necessarily abelian, and let be a finite subset of . Write for the number of elements of a finite set . For finite sets the product set is , and the inverse set is . For , is the product of copies of . For , .
The two hypotheses of the mission, for real numbers and , are
The first is small doubling; the second says that every two-sided "translate" is small. In an abelian group has the same size as , so the second hypothesis follows from the first with .
The proof uses an auxiliary set: a nonempty that grows minimally under right multiplication by , meaning for every nonempty .
For every integer ,
The result. Theorem 1.6 is a non-abelian Plünnecke inequality with explicit, linear-in- exponents. Taking (Tao's setting) gives , so the constant in Tao's theorem can be taken to be , answering Ruzsa's request for an explicit value. Bounds of this shape are the standard way to pass from control of a few products of a set to control of all of its products.
Formalizing it. The result is proved on paper; this mission produces a machine-checked proof. Mathlib already contains the abelian Plünnecke–Ruzsa inequality, Ruzsa's triangle inequality and covering lemma for arbitrary groups, and the Plünnecke–Petridis inequality (Proposition 2.1 of the paper), but no non-abelian bound on under the two hypotheses above. The milestone statements (6)–(11) are each short calculations from these tools and are reusable for other non-abelian product-set estimates.
The obvious argument is to iterate the doubling bound, as in the abelian case. This fails: the example shows that does not control in a non-abelian group, so the second hypothesis has to enter, and it controls only products with a single element in the middle. The difficulty is to bring that hypothesis to bear on , whose factors are all copies of , while losing only a bounded power of and per additional factor and keeping the order of the factors fixed throughout: any step that silently commutes two factors is invalid. The exponents and are exactly what the paper's bookkeeping yields; a looser chain gives a worse but still linear exponent (the paper notes for via a different route, p. 10).
All statements live in the namespace PlunneckeType.Tao and use Mathlib's pointwise Finset operations under open scoped Pointwise, in a group {G : Type*} [Group G] [DecidableEq G], never CommGroup.
X * Y, is X⁻¹, is B ^ h, and is B * {b} * B, with the single element in the middle. Products keep the order printed in the paper.#X cast to ℝ; are real numbers with no sign hypotheses. If is nonempty the hypotheses force ; if is empty every statement reads .2 < h. Under this hypothesis the natural-number exponents 8 * h - 17 and h - 2, and the powers B ^ (h - 1), B ^ (h - 2), are exact. The goal does not claim , where the printed exponent would be negative.Group. A version for commutative groups, or one that adds a hypothesis implying commutativity of the relevant products, is a different and weaker theorem and does not count.Recorded deviations from the printed text: Theorem 1.6 reads "Let be finite a set" (word order; kept verbatim in the milestone text); the strategy paragraph on p. 9 says "cover the middle copy of by ", where the set is ; display (11)'s lead-in writes "" for . The Lean statements use the intended mathematics.
Tools solvers will find in Mathlib (Mathlib/Combinatorics/Additive/): Finset.pluennecke_petridis_inequality_mul (Proposition 2.1), Finset.ruzsa_triangle_inequality_mul_mulInv_mul and its variants (Lemma 4.2, up to Finset.card_inv), Finset.ruzsa_covering_mul (Lemma 4.1, after inverting), Finset.card_singleton_mul, Finset.card_mul_singleton. Lemmas 4.1 and 4.2 are cited results of Ruzsa and are not items of this mission. Proofs of any milestone, and any reusable lemmas on non-abelian product sets, are welcome.
Stochastic gradient descent (SGD) is the standard first-order method for stochastic convex optimization and for training linear predictors on large data sets: at each step it queries a noisy subgradient of the objective, takes a step against it and projects back onto the feasible set. When the objective is strongly convex, the classical online-learning analysis of SGD with step sizes bounds the expected suboptimality of the averaged iterate by (Hazan, Agarwal, Kale 2007). The information-theoretically optimal rate for this problem class is , and it is attained by other algorithms (Hazan, Kale 2011; Juditsky, Nesterov 2010).
This left a concrete question: is the logarithmic factor an artifact of the analysis, or a property of SGD with averaging? Rakhlin, Shamir and Sridharan (arXiv:1109.5647v7, ICML 2012) answer it by exhibiting strongly convex problems on which averaged SGD provably loses the logarithm. The same paper shows that for objectives that are smooth at the optimum the averaged iterate attains , and that averaging only a suffix of the iterates restores in general. This mission is the lower-bound half of that picture; the two upper bounds are sibling missions of the same series.
Points live in , , with the Euclidean norm; for a point , denotes its first coordinate. A stochastic gradient oracle for an objective returns, at a query point , a random vector whose mean is a subgradient of at . Projected SGD on a domain with step sizes , , starts at a point and sets
where is the Euclidean projection onto . The output studied here is the average . Throughout, are independent random variables, each uniformly distributed on .
Example A. , , and the oracle returns . The global minimum over is at , a corner of the box.
Example B. and
Here is -strongly convex and non-smooth along the hyperplane , and its minimizer lies in the interior of . The oracle is state-dependent: which branch it uses depends on the sign of the first coordinate of the query point. In both examples is a subgradient of at and is bounded for fixed .
In Example B, for every , every starting point with , and every integer ,
For fixed this is . The goal is the paper's statement with its constants.
The result. Theorem 4 shows that the guarantee for SGD with full averaging is tight up to constants on strongly convex problems, even when the optimum is interior. It separates SGD with averaging from algorithms that reach , and it is the reason the paper introduces -suffix averaging. It also explains why smoothness at the optimum (the paper's §3) matters: Example B is non-smooth exactly at .
Formalizing it. The result is proved on paper but, as far as the platform's index shows, has no machine-checked proof. Formalization adds a verified lower bound with explicit constants. It also settles the paper's own argument. The printed proof of Theorem 4 relies on Lemma 4 (p. 16), whose first claim uses where the recursion subtracts with up to , so Lemma 4 fails with positive probability. Theorem 4 is believed true, but a complete proof needs a repaired argument. Theorem 3's printed proof uses in step (8), while only gives . Numerical checks of Theorem 3 itself found no violation.
An expectation lower bound on the average needs control of every iterate , not just of the last one, and the iterates form a non-linear Markov chain because of the projection and, in Example B, because of the state-dependent oracle. Upper-bound techniques do not transfer: they bound from above, which says nothing about the sign of . In Example B, the natural first idea is to argue that never stays negative, so that it behaves like the constrained Example A; this is the claim of the paper's Lemma 4, and as stated it does not hold, because a single noise draw near can push the first coordinate below the level the lemma asserts. A proof must handle that event with explicit constants and still produce the slack of the statement.
UnderstandingML.Vec d = EuclideanSpace ℝ (Fin d) with [NeZero d]; the paper's first coordinate is index 0.sgdRun … k is the paper's ; the step at index uses and the noise value at index . The starting point is arbitrary (not ), as in Theorems 3–4.ProbabilityTheory.cond volume (Set.Icc (-1) 3) (uniform on ); a horizon- sequence has the product law UnderstandingML.iidLaw. Expectations are Bochner integrals over it.ProbabilityTheory.cond, which would be the zero measure on a null conditioning event.Quasi-Newton methods such as BFGS were designed for smooth objectives, yet in practice they are routinely run on nonsmooth functions and they often work well there: on many nonsmooth problems the iterates converge to a minimizer at a linear rate, measured against the total number of function evaluations. Lewis and Overton (Math. Program. 141 (2013) 135–163) set out to explain this behaviour. Almost nothing about it is proved, so they analyse the simplest cases in detail.
The very simplest case is the subject of this mission: minimizing the absolute value on the real line. In dimension one the quasi-Newton update is completely determined by the secant equation, so the method is the classical secant method, combined with a bisection-type Armijo–Wolfe line search. Even here the behaviour is far from obvious. Steepest descent on needs about function trials to reach accuracy , because the closer the iterate is to zero, the more bisections its fixed-size step needs. The secant method needs only about , the cost of bisection. Lewis and Overton show that the iterates of the secant method trace out an expansion of the starting point as an alternating sum of powers of two, which accounts exactly for the number of trials.
The objective is on , with gradient at every .
The line search (Algorithm 4.6, p. 147). Given two tests on steps , an Armijo test and a Wolfe test , the line search starts with , and . Each trial examines the current . If fails, it sets . Otherwise, if fails, it sets . Otherwise it stops and returns . The next trial step is when and otherwise. So the line search doubles until the step is bracketed, then bisects.
The tests of §5.1. At an iterate with direction (where ), take the line search objective , the Armijo parameter , and replace the differentiability check by a termination rule. The conditions become
The secant method. Start at with . At step set , let be the step returned by the line search, and put . If the method terminates at the minimizer. Otherwise is the solution of the secant equation with . The -th line search takes trials. The trial points of all line searches, listed in order, give the function trial values .
Alternating binary expansions. For , an alternating binary expansion is a length and integers (with terms when ) such that
It is canonical if either or its last gap satisfies .
Rates (p. 141). A sequence is Q-linear with rate if . A sequence is R-linear with rate if for all , for some converging to Q-linearly with rate .
Let have the canonical expansion . Then the secant method from with satisfies
If , the method terminates at zero after finitely many trials. If , the function trial values converge to R-linearly with rate . All four conclusions are exact: the iterates are equal to the tails of the expansion, and the trial counts are equalities.
The theorem gives a complete description of a quasi-Newton method on a nonsmooth function, in the one setting where the description is exact. It identifies each iterate, counts every function evaluation, and decides termination. Two things follow. After trials the error is below , so accuracy costs about trials, compared with the quadratic count for steepest descent. The analysis also shows that choosing the Armijo parameter is harmless for , which the paper contrasts with the tilted function . The R-linear rate of all trial values is the one-dimensional instance of the rates the paper observes numerically for BFGS on the Euclidean norm in higher dimensions (§5.2). Those rates remain unexplained.
The result is proved on paper: in Lewis–Overton, with the detailed analysis attributed to the companion report [31]. To our knowledge none of it has been formalized. This mission produces a machine-checked account of an algorithm as executed: a bisection line search counted trial by trial, a secant update, and the number-theoretic fact that this process computes an alternating binary expansion. It also states and fixes the two places where the printed text is inaccurate (see Formalization scope).
The first line search is easy to analyse directly: with it returns the unique power of two in . The difficulty starts with the second. The step returned by Algorithm 4.6 depends on the whole bisection history, and the new direction depends on the previous step through the secant update. The statement therefore has to be proved by an induction that carries an exact invariant. That invariant ties , and the line-search bracket to the tail of the expansion, and the trial count to the gap .
A natural first attempt is to describe each line search as "returns the power of two in the Armijo–Wolfe interval". That does not determine the trial count: the count depends on where the bisection starts and in which order it halves, and it uses the specific directions . The R-linear statement adds a further layer. Trial values inside one line search are not monotone, so the dominating Q-linear sequence has to be built over the global trial index, across line searches of different lengths.
The uniqueness half is elementary but needs care. Without canonicity it is false, and a finite expansion has to be told apart from an infinite one.
WithTop ℝ. A trial count is the index of the first trial passing both tests, plus one. Every statement about trial counts also asserts that the line search terminates, so the junk value of an empty stopping set cannot be used. The step is not defined as a closed form: that is what the theorem proves.ℕ∞, the exponents are a : ℕ → ℤ (negative when ), and the powers are integer powers. The series is a HasSum whose terms beyond vanish. Indices start at , as printed.The development needs only Mathlib's real analysis, tsum/HasSum and filters. The expansion definitions and the R-linear predicate can be reused for other rate statements. Contributions are welcome on the line-search invariant, the trial-count lemmas, and the existence and uniqueness of the canonical expansion.
Plünnecke–Ruzsa inequalities bound the size of iterated sumsets: if and are finite subsets of an abelian group with , then for every , where . They are a basic tool of additive combinatorics, used in Freiman-type structure theorems, sum–product estimates and the study of approximate groups. Plünnecke's original proof went through a graph-theoretic argument; Ruzsa simplified and extended it.
G. Petridis, New proofs of Plünnecke-type estimates for product sets in groups (arXiv:1101.3507v3, 2011; Combinatorica 32, 2012, doi:10.1007/s00493-012-2818-5), gave a short, purely combinatorial proof. Its core (Proposition 2.1, p. 5) is that a subset minimising satisfies for every finite , in any group.
In a non-abelian group the hypothesis alone does not control or . Tao (Product set estimates for non-commutative groups, Combinatorica 28, 2008) showed that an extra condition on triple products restores polynomial bounds, without explicit exponents. Petridis' §4 makes Tao's bound explicit for a single set; this mission is §5 of the paper, which treats two sets and of comparable size.
Timeline:
Let be a group, written multiplicatively and not necessarily commutative. For finite subsets write
for the number of elements, ( factors), and for . The order of factors matters: multiplies on the left of .
The three hypotheses of the mission are, for finite and real numbers :
A minimal-growth subset of (with respect to ) is a nonempty with for every nonempty . In Lean this is written cross-multiplied: .
If is nonempty and (1)–(3) hold, there is a nonempty such that for every integer
The same serves every .
Theorem 1.7 extends the Plünnecke–Ruzsa inequality to non-abelian groups with explicit exponents, under hypotheses that are checkable on and alone. Bounds of this kind feed into the theory of approximate groups, where polynomial dependence on the doubling constants is what keeps later structure theorems quantitative. The witness is a large-enough piece of on which all powers of grow at a controlled rate, which is the form in which such bounds are used.
The result is proved in the paper. Mathlib formalizes Petridis' Proposition 2.1 (Finset.pluennecke_petridis_inequality_mul, in any group) and the abelian Plünnecke–Ruzsa inequalities (Finset.pluennecke_ruzsa_inequality_*, for commutative groups), but not the non-abelian estimates of §5. This mission adds them: the corollary on , the comparable-size bound for , and the full Theorem 1.7. Companion missions of this series formalize the abelian Theorem 3.1 and the explicit form of Tao's theorem (Theorem 1.6).
The abelian argument iterates with , which needs , i.e. commutativity. In a non-abelian group and powers of cannot be reordered, so the bound on does not iterate directly. A second obstacle is that the hypotheses control products of and , while the induction needs control of sets such as and , built from inverses; the hypotheses say nothing directly about such sets, and every passage between them and products of and costs further powers of and , which is why the exponents grow like and rather than . The abelian bound should not be expected to transfer unchanged.
All statements use Mathlib's pointwise Finset algebra under open scoped Pointwise, in {G : Type*} [Group G] [DecidableEq G] — never CommGroup. is X * Y, is A * {b} * B, is S * B ^ h with B ^ 0 = {1}, is X⁻¹. Cardinalities are cast to ℝ; are arbitrary reals, with no sign hypotheses beyond what the page states. Exponents are natural numbers, exact under 1 < h (goal) and 2 ≤ h (inductive step).
Conventions committed to:
Proof tools available in Mathlib: Ruzsa's covering lemma (Lemma 4.1 of the paper, Finset.ruzsa_covering_mul), Ruzsa's triangle inequality (Lemma 4.2, Finset.ruzsa_triangle_inequality_mul_mulInv_mul and siblings, with Finset.card_inv), Proposition 2.1 (Finset.pluennecke_petridis_inequality_mul), and Finset.card_singleton_mul. No new definitions are needed. Proofs of any milestone are welcome; the inequalities (15)–(17) of p. 13 are natural auxiliary lemmas for the inductive step.
MAX-2SAT asks for an assignment of Boolean variables that maximizes the total weight of satisfied clauses, each clause being a disjunction of two literals. It is one of the basic constraint satisfaction problems of approximation theory, and its approximability has been studied alongside MAX-CUT since semidefinite programming entered the field.
Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 37(1), 2007) show that, assuming the Unique Games Conjecture, it is NP-hard to approximate MAX-2SAT within any factor greater than
(their Theorem 3), and that their reduction produces balanced instances, in which every variable carries as much weight positively as negatively. Their Theorem 4 shows that for this balanced restriction the bound is tight: a Goemans–Williamson style semidefinite relaxation followed by random-hyperplane rounding approximates Balanced-MAX-2SAT within any factor smaller than . This mission formalizes Theorem 4.
Timeline.
Treat the bit TRUE as and FALSE as (the paper's §7.2 convention). An assignment of the variables is a point . A literal is with a sign ( for the negated variable ); it is true when . A weighted MAX-2SAT instance is a finite list of clauses with , (the two variables may coincide), with nonnegative weights . The satisfied weight of is
An instance is balanced (Definition 12) if for each variable , the expected satisfied weight when and the other variables are uniform equals the expected satisfied weight when and the others are uniform.
The semidefinite relaxation replaces each by a unit vector and the balanced objective by
with optimal value over unit-vector families in every dimension. Hyperplane rounding draws a standard Gaussian vector and sets .
For every balanced instance with nonnegative weights, every , every unit-vector family with , and every standard Gaussian vector ,
with the satisfied weight integrable. The constant is Theorem 3's exact minimum , not its decimal rounding.
The result. Together with Theorem 3, Theorem 4 pins the approximability of Balanced-MAX-2SAT at exactly under the Unique Games Conjecture: the constant arising from the Majority Is Stablest analysis of the hardness reduction coincides with the constant of a semidefinite rounding algorithm. It also explains why the hardness reduction for MAX-2SAT cannot give more than without abandoning balanced instances.
Formalizing it. The theorem is proved in the paper; no machine-checked proof is known to exist. A formal proof produces a verified approximation guarantee for a randomized rounding scheme that holds for every near-optimal vector solution, and a reusable layer for weighted 2-CSPs on : arithmetization, balancedness, the vector relaxation and its rounding. The hyperplane identity is already available on the platform, so the remaining work is combinatorial and analytic rather than probabilistic.
The naive approach, rounding the full arithmetized objective , fails: the relaxation of a linear term has no vector counterpart that random-hyperplane rounding treats correctly, and for unbalanced instances the achievable ratio is different. The whole argument rests on balancedness making the linear terms vanish identically, and the equivalence between Definition 12 (a statement about conditional expectations) and the cancellation of linear coefficients must be established with care, including clauses whose two literals involve the same variable.
The second difficulty is the constant. is defined as a minimum over only, while the per-clause comparison is needed for all inner products , that is for all . Showing that the ratio does not drop below on is a genuine one-variable inequality, not a definitional unfolding. Finally, the expectation must be computed for a genuine Gaussian vector, with the sign convention at handled almost surely.
Fin n → Bool read through pm true = -1, pm false = 1; a literal is (i, r) : Fin n × Bool with r = true for . The two literals of a clause may involve the same variable.m clauses, a clause map, and real weights with a nonnegativity field (Definition 10's "nonnegative weight function").OPT is a maximum over the assignments. SDP is a real supremum over unit-vector families Fin n → Fin d → ℝ in every dimension ; the set is nonempty and bounded above by the total weight.beta is the infimum of the image of , i.e. Theorem 3's attained minimum. Defining it over instead would make milestone 5 definitional and is ruled out.IsStandardGaussianVector (measurable, independent coordinates of law on an arbitrary probability space); the expectation is a Bochner integral and its integrability is part of the conclusion. The rounding outputs FALSE on the null event .Welcome contributions: proofs of the milestones, a bridge from Real.sign (used by the platform's Grothendieck identity) to the -valued rounding, and the one-variable analysis behind the per-clause bound.
Quasi-Newton methods, BFGS above all, are the standard tool for smooth unconstrained minimization. They are also used directly on nonsmooth functions, where in practice they often converge to stationary points with linearly converging function values; the paper documents applications such as the design of low-order controllers (Lewis–Overton 2013, abstract and §1). Theory lags behind: as Lukšan and Vlček wrote, quoted on p. 136, "no global convergence has been proved for standard variable metric methods applied to nonsmooth problems". Methods with proved convergence modify quasi-Newton steps with bundle ideas; the unmodified method remains unexplained.
Lewis and Overton isolate the simplest nonsmooth case in which a complete analysis is possible: the Euclidean norm in the plane, minimized by any quasi-Newton method with an exact line search. The norm is differentiable everywhere except at its minimizer, so the method is well defined until it reaches the solution, yet the function is genuinely nonsmooth at the point the iterates approach. This mission formalizes that analysis (§3.1 of the paper).
Write for the Euclidean norm of and . For , is differentiable with gradient ; at it is not differentiable.
A quasi-Newton method (Algorithm 2.1 of the paper) starts from and a symmetric positive definite matrix . At iteration it
The line search is exact: minimizes . For the norm, the method stops exactly when some iterate equals ; "the algorithm does not terminate" means for every . The BFGS update (2.2) is one particular choice of .
Two plane notions describe the motion of the iterates: the unsigned angle , and the orientation sign of , positive when is a counterclockwise turn of . A real sequence converges to Q-linearly with rate when and (p. 141). Finally, denotes the angle between and .
For every non-terminating run of the method above, with any positive definite secant updates,
and there is with for all large : the iterates eventually rotate in one consistent direction.
Theorem 3.2 is a complete convergence-rate analysis of unmodified quasi-Newton methods on a function that is nonsmooth at its minimizer. It shows that the observed linear convergence is not an artefact of a particular update: the rate and the turn are forced by the exact line search and the secant condition alone, for every positive definite secant update. Proposition 3.3 shows that both constants are attained exactly by BFGS, so the theorem cannot be improved. The paper's experiments for (§3.2, p. 143) suggest similar behaviour, with observed rates growing with , and the authors state that they do not know how to extend the analysis; a formal two-dimensional analysis is the natural base for any attempt in higher dimension.
As far as we know none of these results has a machine-checked proof. A formalization would contribute the first verified statements about quasi-Newton iterations on a nonsmooth function, a reusable form of the exact-line-search orthogonality (Proposition 3.1, valid for any in any dimension), and an explicit, checked BFGS run in closed form.
The analysis rests on rotating and scaling so that , after which every quantity is an explicit trigonometric expression. In a formal setting this "without loss of generality" is not free: one must show that the exact step, the angles, the secant condition and the next direction all transform correctly under rotations and scalings, or carry out the computation in invariant form. The direction is only known up to sign from Proposition 3.1; fixing the sign requires positive definiteness of . The orientation claim is the most delicate part: the paper argues it from approximate values for large , which has to become an exact sign argument that holds eventually. Proposition 3.3 needs an induction through the BFGS formula with exact arithmetic in , including that each updated matrix stays positive definite.
Vectors are Fin 2 → ℝ (or Fin n → ℝ in Proposition 3.1) and matrices Matrix (Fin 2) (Fin 2) ℝ. The Euclidean norm is written out as , since Lean's default norm on Fin 2 → ℝ is the sup norm; with the sup norm every statement would change meaning. The gradient of the norm is the explicit formula . Positive definiteness is Matrix.PosDef, which includes symmetry (Proposition 3.1 needs it). A run is the predicate IsExactNormRun: , positive definite , , exact steps minimizing over all real (equivalent to here, because is a descent direction), and the secant condition whenever the method has not stopped. Non-termination is the separate hypothesis for all . Q-linear convergence of the vectors is read through the real sequence , following the proof's last line. Angles are unsigned and orientation is the sign of cross; "consistent orientation" is an eventual sign, not a limit of signed angles.
Corrections relative to the printed text, each disclosed in the item's Formalization Note:
A trivializing formalization is ruled out: the run predicate keeps positive definiteness and exactness (without them may be an ascent direction and Theorem 3.2 is false), its secant field is guarded so that it never involves the junk gradient at , and Proposition 3.3's existence clause certifies that the predicate is satisfiable.
The development needs elementary plane geometry with arccos, the BFGS update (reused from the published definition ShannoCG.SCONB.bfgsUpdate), and the contraction principle (Mathlib's ContractingWith). Rotation-invariance lemmas for the method would be reusable for any analysis of quasi-Newton methods on norms. Proofs of any milestone, and in particular an invariant treatment of the normalization step, are welcome.
Manufacturers and their suppliers rarely trade on fixed orders. A buyer sends a rolling schedule of intended purchases for the coming periods and revises it every period as its own forecasts change. Left unconstrained, such revisions pass demand volatility up the supply chain and amplify it, the phenomenon studied as the bullwhip effect (Lee, Padmanabhan & Whang 1997). A quantity flexibility (QF) contract limits how far each estimate may move from one period to the next: the buyer commits to a band around its earlier estimate, and the supplier commits to supply anything inside that band. The paper reports QF-type agreements at Sun Microsystems, Solectron, Nippon Otis, Toyota, IBM, Hewlett Packard and Compaq (p. 92).
Tsay & Lovejoy (1999) model a multi-stage chain in which every stage is linked to its neighbours by QF contracts, and ask how the flexibility a node offers its customer, compared with the flexibility it receives from its supplier, determines the inventory the node must carry. This mission formalizes their answer for one node: Proposition 2 (p. 97), which states that a node whose supply side is at least as flexible as its customer side needs no inventory at all.
Time is discrete, . In period a flex node receives from its customer a release schedule : is the quantity sold in period , and is the current estimate of the quantity to be sold in period . The node sends its supplier a replenishment schedule with the same meaning on the purchase side. Its ending stock evolves as
The QF contract on the customer side has output parameters and , , and the output IR (Incremental Revision) constraints (6):
The supplier side has input parameters and the analogous constraints (7) on . The cumulative flexibilities (9), (11) are
on each side, with . The pair of sequences is the side's flexibility profile.
The node follows the Minimum Commitment (MC) policy (21)–(23). From , and it computes, by one recursion on , projected inventories and the new schedule:
The first term of the maximum is the target of (22): the least supply that covers the largest purchase the customer may still make in period . The second term is the least value the supplier contract allows given last period's schedule.
Under the standing assumptions, if (a) the release schedules are nonnegative and obey (6), (b) the node uses the MC policy, (c) and the run starts with , and (d) and for all , then
If moreover and for all , then
Proposition 2 isolates the source of inventory at an intermediate stage of a QF-linked chain: it is the disparity between the node's input and output flexibility, not the volatility of the forecasts themselves. A node supplied at least as flexibly as it serves can meet every contractual obligation with zero stock, and a node with matched flexibility passes every schedule upstream unchanged, acting as a non-distorting conduit of information and material. The paper uses this to argue that supply flexibility beyond the customer's is wasted at the node unless passed downstream (p. 97). Inventory under a flexibility mismatch, where the node amplifies flexibility, is studied numerically in §5 of the paper.
The result has a short proof in the paper, but that proof routes through formula (33), a closed form of the MC schedule as a maximum over all earlier periods, whose proof is omitted and which needs schedules before any starting period. A machine-checked proof must instead argue directly on a run with a definite start. No part of the paper has been formalized before; this mission also produces a reusable formal model of rolling schedules, QF constraints and the MC policy.
The obvious argument shows from the definition of the MC policy at index alone. That fails: is a maximum that includes the carried-over term , which depends on the whole earlier schedule , and that in turn on , and so on back to the initial schedule. Bounding therefore requires control of every component of every earlier schedule, an invariant over both indices that the paper does not state. The start of the run matters: with an unconstrained initial schedule the claim is false. The equal-flexibility part additionally needs a second induction, on within each period, interleaved with the recursion that defines and .
Schedules are functions indexed by ; the release schedules are a function with f t j . The QF parameters are sequences whose value at index is unused. Constraint (6) is stated with the paper's written . The MC policy is defined literally by (21)–(23), for every , as one recursion that interleaves and ; the run starts from a given state at period and applies the policy from period on. All values are real.
The standing assumptions of p. 95 (, ) are hypotheses. Three hypotheses are added to the page's statement and disclosed in each item:
A formalization in which the run sets , or in which the MC step drops the carried-over term in (21) or the positive part in (23), would make the goal trivial; the model rules this out by defining the policy exactly as printed. Condition (d) compares the cumulative profiles, not the parameters termwise. Formula (33) and Propositions 1, 3 and 4 are not part of this mission; Proposition 1 (optimality of MC for the open-loop program) is the companion mission.
Contributions welcome: proofs of the milestones, a proof of the goal through an invariant on , and lemmas about the MC run reusable for the companion mission.
A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, without revealing why it is true. Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012) gave NIZK proofs for Circuit SAT of size for a circuit and security parameter , the first perfect NIZK arguments for all of NP, and the first non-interactive zaps based on a standard cryptographic assumption. These constructions use a single algebraic primitive, the homomorphic proof commitment: a commitment scheme with two kinds of keys, together with a short proof that a committed value is or .
The paper gives two instances of this primitive. One rests on the subgroup decision assumption in composite-order groups. The other, the subject of this mission, rests on the decisional linear assumption of Boneh, Boyen and Shacham (CRYPTO 2004) in prime-order bilinear groups. Prime-order groups are the setting of most later pairing-based proof systems, including the Groth–Sahai proofs (EUROCRYPT 2008), and their decisional-linear instantiation uses commitment keys of the same linear-tuple form as this mission.
A DLIN bilinear group is a tuple : is a prime, and are groups of order , is bilinear ( for all , ), generates , and generates . A triple is a linear tuple with respect to .
The scheme (Figure 2 of the paper) works as follows.
The perfect properties of Section 3 are: homomorphism, perfect binding, perfect extractability, perfect trapdoor opening and its indistinguishability, perfect completeness, perfect soundness, perfect witness indistinguishability (WI), and perfect non-erasure WI. Non-erasure WI asks that a simulator turn the randomness of a proof made with one witness into randomness that explains the same proof under the other witness.
For every DLIN bilinear group, the scheme of Figure 2 is homomorphic on both kinds of key and perfectly binding and extractable on binding keys. On hiding keys it has perfect trapdoor opening and perfect trapdoor-opening indistinguishability. Its 0/1 proof is perfectly complete on both kinds of key, perfectly sound on binding keys, and perfectly WI and perfectly non-erasure WI on hiding keys. Soundness, for example, reads
The milestones follow the paper's proof:
The perfect properties are what the paper's later results consume. Perfect soundness and extractability on binding keys give the perfectly sound NIZK proof of knowledge for Circuit SAT (Theorem 6). Perfect WI, trapdoor opening and non-erasure WI on hiding keys give perfect zero-knowledge (Lemma 8 and Theorem 11) and the adaptive and UC-secure variants of Sections 7 and 8. Theorem 4 transfers all of this to prime-order bilinear groups under the decisional linear assumption.
The theorem is published and its proof is short, but the printed construction contains an error. With the signs of in and as printed in Figure 2, an honest proof fails the fourth and sixth verification equations whenever . A machine-checked proof fixes the corrected construction, under which the paper's own witness-indistinguishability argument goes through. No formalization of this scheme, or of the decisional linear setting, exists on the platform or in Mathlib.
The algebra is modest. The work lies in carrying exponents in through powers in groups of order , and in getting the soundness argument right. An accepted proof only constrains discrete logarithms of the proof elements, so the six pairing equations must first be turned into six equations between exponents. That step is valid only because , and are nondegenerate. Soundness then needs the observation that the product of two specific linear forms vanishes, and it fails outright on a hiding key (). Witness indistinguishability is an exact identity between proofs, which holds only for the corrected prover.
G →* G →* GT, which is equivalent to bilinearity. generates and generates .ZMod p, acting through their representative in .Classical safety-stock formulas assume that demand is stationary: independent and identically distributed around a fixed mean. Many products do not behave that way. Their demand level drifts, and the forecast has to follow it. Graves (A single-item inventory model for a nonstationary demand process, Manuf. Serv. Oper. Manag. 1(1):50–61, 1999) works out what such drift costs in inventory when it is modelled by the simplest nonstationary time series used in forecasting practice. The model is the integrated moving average process of order , for which the exponentially weighted moving average is the optimal forecast (Muth, 1960; Box, Jenkins and Reinsel, 1994).
The paper answers two questions. For one stage under an adaptive base-stock policy, it gives the exact distribution of the inventory, and hence the safety stock. For two stages in series, it shows that the order stream the downstream stage passes upstream is again of the same type, amplified. This is an explicit instance of the bullwhip effect of Lee, Padmanabhan and Whang (1997). The paper then gives the distribution of the upstream inventory. That last distribution, equation (16), is the goal of this mission.
Time is indexed by periods ; operation starts in period . Fix a mean level , a parameter with , a downstream lead time and an upstream lead time . The shocks are independent random variables, each normal with mean and variance .
Downstream stage (§2). The demand is the IMA(0,1,1) process
The forecast , made after observing , is the exponentially weighted moving average
The order , placed in period and delivered in period , follows the adaptive base-stock policy
The inventory at the end of period (negative values are backorders) obeys
where is an initial inventory chosen by the planner. Orders may be negative.
Upstream stage (§3). It sees the orders as its demand. It forecasts them with smoothing constant ,
orders for and for (15), and holds inventory
with initial inventory .
In Lean, IsStage μ α L ε d F q x is the conjunction of (1), (3), (6), (7) and the boundary condition. IsUpstream μ β K q G p y is (11), (14), (15) and its boundary condition. upBeta α L is , and IsTwoStage is the conjunction of the two stages.
For every period (and ), the upstream inventory is normally distributed with
Two further statements of the paper are included as plain theorems: the order amplification (p. 55), stated as: and are independent of with laws and , and the critical-fractile rule (p. 54). Under that rule, setting gives .
Equation (8) is a closed-form safety-stock formula for nonstationary demand. For the standard deviation of the inventory grows faster than , so the textbook square-root law understates the safety stock. Equation (16) carries the formula one stage up a supply chain. With , the upstream safety stock depends on the downstream lead time , not only on the upstream lead time . The paper concludes that shortening the downstream lead time can matter more than shortening the upstream one. P1 and P2 underlie these conclusions: they write each inventory as a fixed linear combination of a bounded window of shocks.
All results here are proved in the paper. None of them, and none of the model's objects, is formalized on Prove2Me or, as far as is known, anywhere else. The mission produces machine-checked versions of the closed forms and distributions. It also produces a reusable statement that a finite linear combination of independent Gaussian shocks is Gaussian, which Mathlib has only for two summands.
The pathwise milestones are inductions on the period, but they are not uniform. The inventory recursion (6) reads orders periods back, so P1 has two regimes: , where every order read is a policy order, and , where some are the boundary orders . The paper treats the second regime only by "direct substitution", and a single statement has to cover both.
P2 is not a second copy of P1. The upstream stage is defined by its own recursions (11), (14), (15). It becomes an instance of the single-stage model only after (10) and the forecast identity have been proved, and P1 must then be applied with parameter and shocks . The distributional statements (8) and (16) need the law of a finite weighted sum of independent normal variables. Mathlib provides the two-variable case; the finite-sum version, with a -indexed window of shocks, has to be built from it.
All sequences are functions ; lead times are natural numbers, cast to in indices and to in coefficients, so no truncated subtraction occurs. The model is a predicate on sequences, and the objects are constrained only by the paper's recursions (1), (3), (6), (7), (11), (14), (15) and the boundary conditions for . None of the closed forms (2), (5), (9), (10), P1 or P2 is built into a definition. In particular the upstream stage is not defined as an instance of the downstream one, which would assume (10). The paper's convention for is implemented by a masked sequence masked ε in P1 and P2, not by a hypothesis. The standing assumption is a hypothesis of every theorem.
In (8) and (16) the shocks live on a probability space . They are measurable and mutually independent over periods (iIndepFun over ), each with law gaussianReal 0 (σ²). The system equations hold for every outcome, and the initial inventory is a constant. "Normally distributed with mean and standard deviation " is the law equality P.map (y t) = gaussianReal m (s²). A statement only about the variance would be weaker than the paper's claim and does not count. The critical-fractile theorem adds and ; without them the inventory is constant and the claim fails.
Contributions are welcome on the finite Gaussian-sum lemma, which is independent of this paper, and on any milestone in any order.
A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, without revealing why it is true. NIZK proofs are a basic building block of public-key cryptography: chosen-ciphertext secure encryption, signature schemes and secure multi-party computation all use them. Groth, Ostrovsky and Sahai, New Techniques for Noninteractive Zero-Knowledge (J. ACM 59(3), 2012; conference versions at Eurocrypt 2006 and Crypto 2006), built the first NIZK proofs for all of NP that are perfectly sound and the first NIZK arguments that are perfectly zero-knowledge, using bilinear groups.
The construction rests on a single primitive, the homomorphic proof commitment: a commitment scheme with two kinds of keys (perfectly binding and perfectly hiding) together with a short non-interactive proof that a commitment contains or . Section 4 of the paper instantiates this primitive in a bilinear group of composite order , building on the encryption scheme of Boneh, Goh and Nissim (TCC 2005); Section 5 gives a second instantiation in prime-order groups. Theorem 2 states that the composite-order scheme of Figure 1 has all the required properties. This mission formalizes the part of Theorem 2 that is an exact mathematical statement.
Timeline: Boneh, Goh and Nissim (2005) introduced the subgroup decision assumption and the encryption in groups of order . Groth, Ostrovsky and Sahai (Eurocrypt 2006) used it for perfect NIZK; the simple 0/1 proof used in Figure 1 is due to an observation of Boyen and Waters (Eurocrypt 2006), as the paper's footnote 7 records. The journal version (2012) presents both instantiations through the abstract notion of a homomorphic proof commitment.
A BGN bilinear group is a tuple where are primes, and are finite commutative groups of order , is bilinear ( for all , ), generates , and generates .
The commitment key is for an element of one of two kinds:
The commitment to a message with randomizer is . The trapdoor opening is . The 0/1 proof for a commitment is , and the verifier accepts when . The extractor computes and searches for with .
For every BGN bilinear group, the scheme above satisfies:
with binding, soundness and extractability on binding keys, and trapdoor opening and witness indistinguishability on hiding keys.
The milestones follow the proof of Theorem 2 (p. 9) and Figure 1 (p. 10): the homomorphic property; perfect binding; the extraction identity ; the trapdoor identity and the uniqueness of openings on a hiding key; the completeness display ; the decomposition of every element as on a binding key; the step " of order or implies or "; perfect soundness; and the uniqueness of the proof on a hiding key, which gives witness indistinguishability.
Theorem 2 is one of the two instantiations on which every exact result of the paper rests. Plugged into the Circuit-SAT construction of Section 6, the binding-key properties give a perfectly sound NIZK proof and a perfect proof of knowledge for every NP relation, and the hiding-key properties give a perfect zero-knowledge NIZK argument. The same composite-order techniques underlie later pairing-based proof systems, notably the Groth–Sahai proofs.
The paper's proof is about one page of group computations and has, as far as the planning of this series found, no machine-checked counterpart. The mission produces a reusable model of composite-order bilinear groups and of the BGN commitment, and checks details the paper leaves implicit: the message space versus exponents taken modulo , the role of the non-degeneracy of , and the order arguments behind soundness.
Each property is elementary on its own, but soundness is not a plain computation: the verifier only sees and , and the conclusion asks for an opening of with message in from a single pairing equation. An argument that only manipulates the equation symbolically cannot reach it; the statement depends on the orders of elements in , on generating (with a degenerate pairing soundness is false), and on and being distinct primes. A second subtlety is that a message is only determined modulo by a commitment under a binding key, while the conclusion asks for a message that is exactly or in .
Fintype.card = p * q; is a homomorphism G →* G →* GT, which is exactly bilinearity; generates and generates (both as hypotheses of the structure BGNSetup).ZMod n; is to the representative of in . The paper's message space is , but is not well defined for in a group of order ; binding and extraction therefore compare messages modulo .Many models in operations management and economics need the demand or valuation distribution to be regular in some way, so that an optimal price, order quantity or contract is unique. Pricing a service to one customer whose valuation has survival function is a typical example. The seller maximizes . The first-order condition is , where is the generalized failure rate and is the ordinary failure rate. When is increasing (the IGFR property, introduced by Lariviere and Porteus 2001), the optimal price is unique and solves .
The best-known regularity class is the class of IFR laws, those with increasing failure rate. Every IFR law has finite moments of all orders (Barlow and Proschan 1965). IGFR laws are a larger class that includes heavy-tailed laws, and Lariviere (2006) identifies exactly which of their moments are finite. The answer is given by one number, the limit of the generalized failure rate. A consequence used in pricing models is that a valuation law with a finite mean has eventually, so the pricing problem has a finite solution.
Let be a nonnegative random variable with distribution function and survival function . Assume has a density . The failure rate is
and the generalized failure rate is . is IGFR if is weakly increasing on . has support , with , if exactly for and for every . For a real , the -th moment is .
The comparison law is the Pareto law with scale and parameter , which has density for . Its generalized failure rate is identically on , and its -th moment is finite exactly when . For a level with , write for conditional on . A random variable is stochastically smaller than if for all real .
In Lean, is its law μ : Measure ℝ, is cdf μ, is survival μ, is failureRate μ φ, is genFailureRate μ φ, and is nthMoment μ n.
Suppose is IGFR with support and , where may be infinite. Then for every real ,
The statement fixes no constants. It covers (all moments finite) and the boundary case (infinite moment).
The two Pareto facts of the §3 preamble come first:
Six claims from the proof follow:
Two consequences stated after the theorem are included as further targets. First, an IGFR law with support and a finite mean has beyond some finite point. Second, a strictly IGFR law with a finite -st moment satisfies the two conditions of Van Mieghem and Dada (1999): has at most one zero, and .
The theorem gives a complete moment criterion for IGFR laws in terms of the single number . Among IGFR laws, finiteness of the mean, the variance or any higher moment can therefore be read off the tail of . One consequence is that a finite mean is enough for the IGFR pricing problem to have a finite solution, which replaces the separate condition " exceeds one at a finite point". The theorem generalizes Lemma 2 of Lariviere and Porteus (2001), and the paper uses it to connect IGFR laws to the Van Mieghem–Dada condition.
The result is proved on paper but has not been formalized. Formalizing it adds three things:
Pareto.lean lacks;The core of the proof is a comparison: a pointwise bound beyond a level becomes a stochastic order against a Pareto tail. This needs the representation , which uses the fundamental theorem of calculus for across the left end of the support, where may have a kink. It also needs to be stated for the conditional law, whose density is a rescaled restriction.
An obvious first attempt is to bound directly by with the given bound on . That bound controls , not , so it says nothing directly. The survival representation is what converts it.
A second obstacle is the boundary case , with finite. A strict margin is no longer available there. It needs the non-strict bound , which follows from monotonicity, and a Pareto law with parameter exactly .
Laws, not random variables. Every statement is about distributions, so is represented by a probability measure μ on ℝ with μ (Set.Iio 0) = 0. In the goal, nonnegativity also follows from the support hypothesis, and the separate hypothesis is kept for uniformity with the other items.
The density version is pinned. and read pointwise, while "Φ has density φ" determines only up to a null set. The predicate IsRegDensity requires and . It also requires to be the right derivative of at every point of and wherever . The exponential law with satisfies all hypotheses of the goal, with .
IGFR is weak monotonicity of on , as printed. On this set , so Lean's convention never enters.
is an extended nonnegative real. The limit hypothesis is Tendsto (fun ξ => ENNReal.ofReal (g ξ)) atTop (𝓝 κ) with κ : ℝ≥0∞. A real-valued would silently drop the case .
Moments are lower Lebesgue integrals ∫⁻ x, ENNReal.ofReal (x ^ n) ∂μ with a real exponent. The Bochner integral would make "finite" automatic, because it returns for a non-integrable function, so it is not used.
Conditioning and Pareto. is Mathlib's ProbabilityTheory.cond μ (Set.Ioi y), always with . The Pareto law is Mathlib's paretoMeasure S k. "Stochastically smaller" is the published definition StochasticOrders.Usual.UsualOrder applied with the identity map.
Trivialization is ruled out. The goal is a full equivalence with a possibly infinite and an infinite-valued moment. It is not the weaker " implies finite", and the hypotheses are jointly satisfiable.
Recorded deviations. The printed bound "" is a slip (it fails for ). Only the finiteness it is used for is formalized. The Pareto moment fact is stated as an equivalence, which contains the printed "only if".
Infrastructure. A complete development needs:
cond and cdf.The survival representation and the failure-rate/Pareto comparisons are reusable for any heavy-tail result stated through hazard rates. Contributions are welcome at every level, including partial results such as the Pareto lemmas alone.
Training a model in machine learning means minimizing an expected loss over a data distribution, using a finite sample from it. Two families of methods dominate. Stochastic gradient methods step along the gradient of the loss at one data point: each step is cheap, but the noise forces small steps and many sequential iterations. Batch methods average the gradient over a large set of points: each step is accurate and parallelizes well, but costs a pass over the data. Bottou and Bousquet (The tradeoffs of large scale learning, NIPS 2007) compared the two by the total work needed to reach accuracy and concluded that stochastic gradient descent is preferable in large-scale learning.
Byrd, Chin, Nocedal and Wu (Sample size selection in optimization methods for machine learning, Math. Program. 2012) analyse a third option: a dynamic batch method, which takes gradient steps on mini-batches whose size grows over the run. A small batch makes early progress cheap; a large batch later makes the steps accurate. Their Theorem 4.2 shows that when the batch size grows geometrically, steepest descent with a fixed step converges linearly in expectation, and their Corollary 4.3 derives from it a total work bound of the same order as stochastic gradient descent. The analysis underlies a line of work on adaptive sampling and variance-controlled batch methods (for example Friedlander and Schmidt, Hybrid deterministic-stochastic methods for data fitting, SIAM J. Sci. Comput. 2012; Bottou, Curtis and Nocedal, Optimization methods for large-scale machine learning, SIAM Review 2018, §5.2).
Let be a probability space of data points ; in the paper is an input–output pair with distribution . The parameter is ( is the number of variables). A per-sample loss is given with gradient in , and the objective is the expected loss (2.1)
The gradient of the objective is the expected per-sample gradient, .
Uniform convexity (4.2): is twice continuously differentiable and there are constants with
Then has a unique minimizer .
For a random vector , is the sum of its componentwise variances. The variance bound (4.22) asks for a constant with
The algorithm. Fix sample sizes and a starting point . At iteration draw a batch of points, independently with law and independently of earlier batches, form the batch gradient (4.19)
and take the dynamic batch steepest descent step (4.24)
The iterates are random, and expectations below are over all batches.
If for all , for some , and (4.22) holds, then
The constants are the paper's. The goal also asserts that is integrable for every .
Milestones 3–6 are the paper's conditional expectations given , stated at a fixed point with the batch drawn afresh.
Theorem 4.2 is the convergence guarantee of the dynamic sampling strategy: it says that the noise of a mini-batch gradient does not destroy the linear rate of steepest descent, provided the batch grows geometrically. The rate makes the trade-off explicit: the optimization contracts by per step, the noise by , and the slower of the two governs. From it the paper's Corollary 4.3 bounds the total number of sample-gradient evaluations to reach by , which places dynamic batch methods on the same footing as stochastic gradient descent in the Bottou–Bousquet comparison, while keeping the parallelism of batch methods.
The result is proved in the paper; to our knowledge no machine-checked proof exists. A formalization produces a reusable account of the one-iteration analysis of a mini-batch gradient step (descent lemma, variance of an i.i.d. sample mean of random vectors, conditional expectation over a fresh batch), and of the passage from a conditional one-step recursion to an unconditional bound over a run driven by an infinite i.i.d. array. Corollary 4.3 is not part of this mission: it involves bounds, a cost model for gradient evaluations and an iteration count treated as a real number.
The arithmetic of the induction on p. 12 is short. The difficulty is in making the probability rigorous. The iterate is random, and the paper's one-step bound (4.27) is a conditional expectation given , with on the right-hand side. Turning it into an unconditional recursion requires that the batch of iteration be independent of , that be a measurable function of the earlier batches, and that and be integrable at every step, none of which is automatic for a run driven by an infinite array of draws. A naive formalization that treats as a fixed point, or as an abstract random vector with a postulated variance bound, skips exactly this content.
The variance identity for a sample mean of random vectors in and the bound from (4.2) are standard but not packaged in this form in Mathlib.
EuclideanSpace ℝ (Fin m). The paper's is written lam (λ is a Lean keyword). (4.2) is ContDiff ℝ 2 J, 0 < lam < L, and the two-sided bound on fderiv ℝ (fderiv ℝ J) w d d.Measure.infinitePi over . The finite-population factor is not modelled.Measure.infinitePi. All three are reusable beyond this mission.Program obfuscation asks for a compiler that turns a program into one computing the same function while revealing nothing beyond what black-box access to the function reveals. Barak, Goldreich, Impagliazzo, Rudich, Sahai, Vadhan and Yang (J. ACM 59(2), 2012; conference version CRYPTO 2001) showed that this "virtual black box" notion cannot be achieved in general. Part of their motivation is an informal reading of Rice's Theorem: since every non-trivial semantic property of programs is undecidable from the code, "the only useful thing you can do with a machine is run it". Section 5 of the paper asks whether a complexity-theoretic analogue holds, and Appendix A asks what the right computability-theoretic statement is once one passes from languages to promise problems.
Classical Rice's Theorem (Rice, 1953) concerns languages: a decidable set of machines closed under functional equivalence is empty or everything. For promise problems the naive analogue (Conjecture A.1 of the paper) is false: the problem "halts everywhere and outputs 1 on 0" versus "halts everywhere and outputs 0 on 0" is decidable, non-trivial, and closed under functional equivalence. Appendix A replaces "trivial" by "decidable by a simulator that only runs the machine", proves that version (Theorem A.2), and shows that the size bound given to the simulator cannot be dropped (Theorem A.4, a separate mission in this series). This mission formalizes Theorem A.2.
A machine is a program for a partial recursive function, identified with its description, a natural number . Its computed function is possibly partial, and means equality of partial functions. The size is the length of the binary description of ; there are at most machines of size .
The bounded run of is
An oracle machine may query at any pair of its choice; is its output on input . Oracle access to is what running provides: one may choose inputs and budgets, but one never sees the code.
A promise problem is a pair of disjoint sets of machines. A machine decides if for and for ; nothing is asked of outside . is closed under if implies and .
A machine is -compatible with if for all and all with , and denotes the set of machines of size that are -compatible with .
If is closed under and decidable, then there is one oracle machine such that for every machine
The result. Theorem A.2 is the precise sense in which a semantic property of programs, decidable from the code on a promise, is decidable without the code: running the program on chosen inputs for chosen budgets, plus a bound on its length, suffices. It is the computability-theoretic counterpart of Conjecture 5.2, the complexity-theoretic statement whose failure (Theorem 5.3, under cryptographic assumptions) is one face of the impossibility of obfuscation. Together with Theorem A.4 it isolates the size bound as the ingredient that makes the generalization true.
Formalizing it. The theorem has a complete proof in the paper, about one page long. No machine-checked version is known: the Prove2Me catalogue has classical Rice's Theorem for index sets of Nat.Partrec.Code (FamousTheorems.rice_theorem, which this proof does not use) but nothing on promise problems, bounded-run oracles, or simulators. A formal proof produces reusable infrastructure: the oracle as a total function on query codes, decidability of compatibility relative to it, and a dovetailing simulator assembled as a uniform oracle program.
Each mathematical step is elementary; the work lies in the effective content. The obvious idea, "query until is known and then decide", fails: is an infinite object, and no finite set of queries pins it down. The paper's simulator instead uses the size bound to restrict attention to finitely many candidate codes, and needs to agree on every surviving candidate at a common budget. Turning this into one oracle program requires enumerating all codes of a given size, deciding compatibility from finitely many oracle answers, comparing bounded runs of , and searching over , all uniformly in and with no access to . Termination holds only on promise instances, since may diverge elsewhere, so the argument cannot assume a total decider.
Machines are Mathlib's Nat.Partrec.Code; descriptions are Encodable.encode; is Code.eval; is Code.evaln t M x : Option ℕ, with none for . The budget of evaln is fuel rather than a literal Turing-machine step count. It is monotone in , converges to , and is primitive recursive in , and these are the only properties of step counts that the proof uses. Inputs are natural numbers, is Nat.size x, and is Nat.size (encode M). Oracle machines are the published uniform oracle programs FriedbergMuchnik.Program with semantics oracleEval (a single syntax tree with an oracle-query instruction, equivalent to relative partial recursiveness). The oracle is the total function sending Nat.pair t x to 0 for and to y + 1 for an output . The simulator's input is the number , since unary versus binary is immaterial here. "" means that the run halts with output . Promise problems carry their disjointness, as in the paper, although no statement uses it. The decider is a Code applied to descriptions and may diverge off the promise.
The trivializing readings are excluded. is chosen before (one program, not one per machine). It receives the size of , never its description, and many machines share each size. It sees only the finitely many oracle answers a halting run queries. The oracle is the bounded-run function , not or the code.
Contributions welcome: proofs of the milestones; a primitive-recursive enumeration of the codes of a given size; a proof that oracle M is uniformly computable from M, which is useful beyond this mission.
Training a machine-learning model usually means minimizing an expected or empirical loss over parameters . Exact gradients of such objectives are expensive, because each one requires a pass over the whole data set; practical methods replace by a cheaper approximation , for instance a gradient computed on a subsample. This raises a basic question for the analysis of optimization algorithms: how accurate must the approximate gradient be for steepest descent to keep its linear rate of convergence?
Byrd, Chin, Nocedal and Wu (Math. Program. 2012) answer this question with a relative-error condition, and use the answer to motivate a rule that increases the sample size during the run. Their §4.1 treats the deterministic case: the approximations are arbitrary vectors, and only a geometric condition linking to is assumed. That deterministic result, Theorem 4.1, is the goal of this mission. The stochastic counterpart (Theorem 4.2, dynamic batch sizes) is a separate mission of the same series.
Relative-error conditions of this kind ("the error is a fixed fraction of the step") appear throughout the literature on inexact gradient and inexact Newton methods (e.g. Bertsekas and Tsitsiklis 2000 on gradient methods with errors), and the condition (4.8) below is the deterministic template for the adaptive sampling tests later developed for stochastic optimization.
Let be twice continuously differentiable and uniformly convex: there are constants such that
Such a has a unique minimizer ; following the paper, it is normalized so that .
Fix . Given a sequence of vectors (the approximate gradients), the fixed-steplength steepest descent iteration is
The approximate gradient at iteration satisfies the relative-error condition if
Write
The constants are those of the paper and are kept explicit.
In the order the paper's proof uses them:
Theorem 4.1 says that the linear convergence of steepest descent on a uniformly convex function survives arbitrary gradient errors, provided each error is at most a fixed fraction of the approximate gradient's own norm. The price is explicit: the per-step contraction factor is instead of a factor of the form with an absolute constant , and the iteration bound (4.11) grows like times a logarithm. Because (4.8) is relative rather than absolute, no a priori bound on the error is needed, and the error may be large far from the solution. In the paper this is the motivation for requiring the sample variance of a subsampled gradient to be small relative to , which leads to the dynamic sample-size rule analysed in §4.2.
The result is proved in the paper (pp. 9–10). No machine-checked proof of it, or of any relative-error inexact gradient method with explicit constants, has been published. A formal proof provides a checked reference statement for inexact first-order methods with the paper's constants, and the milestones (4.5), (4.6), (4.13), (4.14) are reusable facts about strongly convex smooth functions and about relative-error gradient approximations.
Each step is classical, but the proof combines second-order information with metric estimates. The descent estimate (4.15) needs a second-order Taylor bound from the upper Hessian bound in (4.2), which in Lean means passing from a bound on the second Fréchet derivative to a quadratic upper bound on along a segment. The inequalities (4.5) and (4.6) relate the gradient norm to the optimality gap through the lower and upper Hessian bounds and the minimizer, and must be derived without an explicit averaged Hessian unless one is built. The convergence in (4.10) requires turning convergence of the function values into convergence of the iterates, which again uses uniform convexity. Finally, (4.11) is a logarithmic iteration count whose boundary cases (, ) must be handled. A naive reading of the iteration with exact gradients does not apply: the step is , not , and the direction is only known to be a descent direction through (4.14).
The space is EuclideanSpace ℝ (Fin m). Assumption (4.2) is a definition HessianBounds J lam L (with lam for , a Lean keyword): ContDiff ℝ 2 J, 0 < lam < L, and both bounds on the quadratic form fderiv ℝ (fderiv ℝ J) w d d. The gradient is Mathlib's gradient J. The minimizer is a point wstar with J wstar ≤ J w for all w, and J wstar = 0 is a hypothesis of the goal and of (4.17), exactly as in the paper; (4.5) and (4.6) are stated with and without it. The constant is a definition beta θ; it is never a free variable. The approximate gradients are an arbitrary sequence and nothing is random. The iterates are any sequence with w (k+1) = w k - ((1 - θ) / L) • g k for all k.
The one-step claim (4.9) assumes (4.8) only at the index ; (4.10)–(4.12) assume it at every index. (4.11) is stated in the form the proof derives in (4.18): every strictly beyond the bound has . The logarithm is natural; when Lean's convention applies, which is harmless because every iterate is then optimal. No positivity hypothesis on is added.
A trivializing formalization is excluded: the step size is fixed by the paper, and the Hessian bounds are pinned, and the hypotheses are satisfiable, e.g. by with , and .
A complete development needs: a second-order Taylor (or mean-value) bound from a Hessian bound, the strong-convexity inequalities (4.5)–(4.6), and elementary real-analysis facts about geometric sequences and logarithms. The milestones (4.5), (4.6), (4.13) and (4.14) are independent of the iteration and reusable. Proofs of any milestone, and alternative proofs with sharper constants stated as separate theorems, are welcome.
Many classical search algorithms are random walks: a Markov chain on a finite state space is run until it hits a marked state. Szegedy (2004) attached to every such chain a unitary quantum walk , and Magniez, Nayak, Roland and Santha (SIAM J. Comput. 2011, arXiv:quant-ph/0608026) used it to search quadratically faster than the classical walk for every reversible ergodic chain. The search runs Grover-style rotations, and each rotation needs the reflection about the stationary state . Preparing exactly can cost far more than one step of the walk, so the paper builds an approximate reflection from the walk alone, by phase estimation. Theorem 6 of the paper is the guarantee for that circuit, and this mission formalizes it.
Timeline:
is a finite set of size . A Markov chain is a row-stochastic matrix . It is ergodic if some power of has all entries positive. A stationary distribution satisfies , and . The time-reversed chain is defined by , and is reversible if .
The space is with basis . Put and , and
For a subspace , , where is the orthogonal projector onto . The quantum walk is , and the stationary state is .
The discriminant matrix is . Its singular values lie in . The phase gap is , where is the smallest angle in such that is a singular value of .
The phase-estimation circuit acts on . It is
where is the Walsh–Hadamard matrix and is the -point Fourier transform.
The circuit uses and acts on . It is built in three steps:
For ergodic and reversible on states, and every integer :
The milestones follow the order in which the paper's proof uses them:
Theorem 6 replaces the reflection about with a circuit that only calls the walk. Its cost scales as rather than as the cost of preparing . Combined with , where is the eigenvalue gap, this gives the search cost of Theorem 7, up to logarithmic factors. The same approximate-reflection device recurs in later quantum-walk and amplitude-amplification algorithms.
The results are proved in the paper, which takes Theorem 4 from Szegedy and Theorem 5 from Cleve et al. As far as the platform index shows, none of Theorems 4, 5 or 6 has a machine-checked proof. The mission produces three reusable components: a Lean definition of the Szegedy walk and of the phase-estimation circuit, a formal Jordan-type spectral theorem for products of two reflections, and the analysis of phase estimation on an eigenvector.
Most of the work is linear algebra. The proof of Theorem 6 has a short outline: expand in eigenvectors of , apply Theorem 5 to each, and bound each amplitude by . Three steps carry the weight:
EuclideanSpace ℂ (X × X), with the first coordinate the first register.Fin (2^s), and registers by Fin k → Fin (2^s); the all-zeros state is the zero index.Submodule.reflection.Matrix.IsPrimitive.LinearMap.singularValues.Real.logb 2 and the ceiling is Nat.ceil.Deviations from the page.
Only exact statements are formalized. The cost halves (gate counts, calls to -, "", the qubit count, uniformity) are out of scope.
The circuit is the explicit composition above, built from . It is neither "some circuit with properties 2–3" nor anything defined through the projector onto , either of which would make the goal a tautology.
Contributions welcome: proofs of the milestones, Jordan's lemma for two subspaces as a standalone result, and the bound of §3.3.
In an online linear decision problem a decision maker chooses, on each period , a decision from a set , and only then learns a state vector and pays the cost . The online shortest path problem, the experts problem, online binary search trees and list update are all of this form. Kalai and Vempala showed that a single offline optimisation oracle is enough to compete with the best fixed decision in hindsight: Follow the Perturbed Leader plays the leader of a randomly perturbed history (Kalai & Vempala 2005; the idea goes back to Hannan 1957).
Each period of FPL calls the oracle once and may change the decision. When an oracle call is expensive, or when switching decisions carries a cost (rotating a search tree, re-routing traffic), this is wasteful. The same paper introduces Follow the Lazy Leader: versions FLL and FLL* of FPL and FPL* that correlate the perturbations across periods so that the decision rarely changes, while each single period is distributed exactly as before. Lemma 1.2 of the paper is the statement that this works, and it is the result of this mission.
Vectors are elements of ; , and with .
The four algorithms, period :
For every period :
The first line is the FLL half, the second the FLL* half. The constant is the paper's.
Lemma 1.2 transfers every guarantee proved for FPL and FPL* to FLL and FLL*: Theorem 1.1 of the paper bounds expected costs period by period, so equal per-period expectations give the same additive bound and the same multiplicative bound for the lazy algorithms. In addition, the expected number of oracle calls and decision changes over periods is at most , which is at the usual tuning . The paper uses this for online binary search trees with few rotations.
The result is proved in the paper. As far as is known there is no machine-checked proof of it. This mission produces a Lean statement of all four claims and of the six steps of the proof, against explicit Lean definitions of the grid point, the FLL* step and the law sequence . The uniformity of a random-grid point and the invariance of a Laplace law under a Metropolis-type step are reusable facts beyond online learning.
The FLL half asks for the exact law of the grid point , a piecewise translation of whose pieces depend on . The page settles it in one line ("by symmetry"); in Lean it is an equality of push-forward measures, and the obvious attempt, a single change of variables , fails because the shift is different on different pieces of the cube.
The FLL* half is a statement about measures on given as a mixture of point masses. The page argues with densities, pointwise in ; the formal statement is an equality of measures, with the update written as a Measure.bind against a kernel whose two branches move mass in different directions. The density computation of display (8) does not by itself give this equality.
Fin n → ℝ, is dotProduct, is written out as ∑ i, |x i|. States are indexed from 1; s 0 is unused.prefixSum and is perturbLaw n ε from the published definition OracleRO.ApproxFPL.FPL. The oracle is the predicate IsArgminOracle Dset M, and every statement holds for every such .laplaceLaw n ε carries its normalising constant , so it is a probability measure for .fllGridPoint ε x p is the explicit formula . It is the unique grid point in the half-open cube for , and it is measurable. The half-open and closed cubes differ by a null set, and the closed-cube law is used throughout.fllStarJoint ε v ν of , built with Measure.bind and Measure.dirac. The acceptance probability is . The law fllStarLaw ε s t is the recursion started at , not itself.The formalization rules out the following trivializations:
Classical.choose;Welcome contributions:
Measure.bind lemmas for finite mixtures of Dirac kernels;In an online decision problem a decision maker chooses actions one period at a time, and only after each choice learns what that choice cost. The classical instance is prediction with expert advice: each day one of experts is followed, and afterwards every expert's loss is revealed. The goal is a strategy whose total cost is close to that of the best single fixed action in hindsight, whatever the sequence of costs.
Many structured problems have exponentially many actions, such as paths in a graph whose edge delays change daily. Weighted-majority methods keep one weight per action and are then inefficient. A. Kalai and S. Vempala (J. Comput. System Sci. 71 (2005) 291–307) showed that it suffices to be able to solve the offline problem: given total costs, find the best single action. Their algorithm, Follow the Perturbed Leader (FPL), adds a random perturbation to the accumulated costs and calls the offline solver once per period. The idea goes back to J. Hannan (1957); the paper's analysis made it short and broadly applicable, and FPL has since become a standard tool in online learning and online combinatorial optimization.
Timeline.
Decisions and states are vectors in . The decision set is a possibly infinite set and the state set is . In period the decision maker picks , then the state is revealed, and the cost is the dot product . The state sequence is fixed in advance (an oblivious adversary).
Write , with . The offline oracle is a map with
Because costs are linear, the best fixed decision after periods has cost
Three parameters measure an instance, with :
FPL(), for a parameter : in each period , draw uniformly at random from the cube and play . Its expected cost is .
Hannan(): the same rule with uniform on .
For every state sequence and every ,
The constants are the paper's. With the expected regret is at most .
For any state sequence in , any and any ,
This bound needs no knowledge of . It is included as a separate theorem, not a milestone of the goal.
The result. Theorem 1.1(a) reduces online linear optimization over any decision set to its offline counterpart, at the price of one oracle call per period and regret . Applied to online shortest paths, spanning trees and other combinatorial problems it gives efficient algorithms where weighted majority would maintain exponentially many weights. Later uses of FPL (approximate oracles, robust optimization via online learning) start from this bound.
Formalizing it. The theorem has been proved in print for twenty years; it has no machine-checked proof that we know of. The platform already holds a formalization of Ben-Tal, Hazan, Koren and Mannor's approximate-oracle variant (OracleRO.ApproxFPL), which takes a maximising oracle and an oscillation bound and therefore yields a weaker constant () in this setting. This mission states the exact-oracle bound with the paper's constant , where bounds itself. A correct proof must handle that constant carefully; see the next section.
Display (4), Lemma 3.1 and display (5) are finite-sum arguments from the defining property of . Lemma 3.2 is a statement about Lebesgue measure of a cube and its translate.
The central difficulty is the stability step: bounding, period by period, how much worse it is to play than . The obvious argument says that the two perturbed points have laws that agree on a fraction, and on the rest "one can only be larger". Under the printed definition of the difference of two costs can be as large as , so this per-period bound fails for costs of mixed sign: with , and suitable , the per-period difference is , while . The theorem itself, with , remains true, but a proof cannot proceed by the per-period comparison as written. Proving the goal with the stated constant, rather than , is the substantive part of the mission.
Fin n → ℝ; is dotProduct (⬝ᵥ); is written out as ; is the Lean norm ‖x‖, which on Fin n → ℝ is the sup norm. The sets are Dset and S; the diameter is Ddiam.s : ℕ → Fin n → ℝ indexed from (s 0 is unused); the hypothesis is imposed for .IsArgminOracle Dset M: and for all . Every theorem quantifies over all such ; the oracle is never a chosen Classical.epsilon minimiser.OracleRO.ApproxFPL.FPL: prefixSum s t ; perturbLaw n ε, the uniform law on ; and fplExpectedReward M s ε T , which with an argmin oracle is the expected cost of FPL() (its name reflects a maximisation source). Using one integral per period is the paper's own observation that fresh and shared perturbations give the same expectation.Contributions welcome: proofs of the milestones, the goal and Theorem 3.3, and reusable lemmas on uniform laws over translated cubes.