Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Online 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.
A retailer who orders a seasonal product before demand is known faces the newsvendor trade-off. Ordering too much leaves unsold stock, and ordering too little forgoes sales. A risk-neutral newsvendor orders a critical fractile of demand. A risk-averse one orders less, since inventory is a risky investment, and this reduction has been shown under constant and decreasing absolute risk aversion (Eeckhoudt, Gollier and Schlesinger, Management Science 41(5), 1995, doi:10.1287/mnsc.41.5.786). Agrawal and Seshadri (2000) and Chen and Federgruen (2000) reached related conclusions.
Demand for many products moves with traded financial quantities: a stock index, a commodity price, an exchange rate. V. Gaur and S. Seshadri (Manufacturing & Service Operations Management 7(2), 2005, pp. 103–120, doi:10.1287/msom.1040.0061) ask what happens when the newsvendor can trade a financial instrument correlated with demand. Their Proposition 7 answers one half of the question: hedging moves the risk-averse newsvendor's order up, towards the risk-neutral quantity. This mission formalizes Proposition 7 and the steps of its appendix proof. The source is the published article, a library scan.
Let be the price at time of a traded asset, with law on . Demand is with . Here is the scaled forecast error, independent of , with law , and . The unit selling price, cost and salvage value are . In the paper's scaled units ((11), p. 110) these collapse into one cost parameter with and , and an initial-wealth term .
A hedge is a portfolio with time- payoff for a nondecreasing function , and time-0 price . It is a fair gamble, (display (12)). A firm that stocks units and shorts units of the hedge ends with the scaled wealth (14)
A decision maker with utility ranks by , and maximizes it over .
The absolute risk aversion is and the absolute prudence is . The utility displays DARA or CARA when is decreasing or constant, and DAP when prudence is decreasing or constant.
The hedge ratio is bounded by , chosen so that is nondecreasing in for . Beyond the firm over-hedges: its expected profit falls as the asset price rises.
For an increasing, concave, differentiable utility with constant or decreasing absolute risk aversion and constant or decreasing absolute prudence,
stated as: is nondecreasing on .
Proposition 7 reverses the conclusion of Eeckhoudt et al. Those authors find that an additional uncorrelated background risk lowers the risk-averse newsvendor's order. Here a correlated financial position that offsets the inventory risk raises it. Hedging therefore increases expected profit as well as reducing variance, and brings a risk-averse firm's operational decision closer to the risk-neutral one. The result is one of the basic statements linking operational and financial risk management in supply-chain finance.
The formalization adds three things.
The obvious argument signs the cross-partial derivative directly: , with of mean zero. That needs the sign of a covariance between and , a weight that depends on both and and is not monotone in either.
The paper first conditions on and splits the weight into two terms. The first is a conditional mean of . The second is concentrated on the sell-out event. Each term then needs its own monotonicity in .
Neither ingredient can be dropped. Without the conditional mean payoff decreases in and the first term changes sign.
Two further obstacles are technical:
Representation.
MDPFinance.FinancialMarkets.arrowPrattCoefficient, referenced rather than redefined.Conventions.
Integrability. The goal and the increasing-differences milestone assume integrability of , , and of their products with on the whole region, which is the regularity the proof uses. Without it a Bochner integral would silently be : the objective would be constant in and every a maximizer. A hypothesis set that forces would also trivialize the goal. A sorry-free check file exhibits the utility class, the standing assumptions and the -condition with for , with equal probability and .
Infrastructure and contributions. A one-variable Chebyshev association inequality for monotone functions is needed. So are differentiation under the integral, or an integrated mean-value argument, for piecewise-linear payoffs, and the step from increasing differences plus a unique maximizer to a monotone argmax. All three are reusable. Proofs of the milestones in any order are welcome, as are alternative arguments that avoid the cross-partial derivative altogether.
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.
Interior-point methods solve linear, second-order cone and semidefinite programs in polynomial time, and they are the engine of most conic optimization software. The general theory of Nesterov and Nemirovskii (1994) covers any convex cone with a self-concordant barrier, but its methods are essentially primal and short-step: their analysis controls the barrier only inside a unit Dikin ellipsoid around the current point. Practical codes for linear programming, in contrast, use symmetric primal-dual methods that take long steps, a large fraction of the way to the boundary.
Nesterov and Todd (1997) isolated the class of cones and barriers for which the primal-dual long-step theory of linear programming carries over: self-scaled cones with self-scaled barriers. The class contains the nonnegative orthant, the second-order cone and the cone of positive semidefinite matrices, and their products. This mission formalizes the paper's §8 result: a primal-dual potential-reduction method with joint scaling decreases a symmetric potential function by an absolute constant at every iteration, which yields an iteration bound.
Timeline. Todd and Ye (1990) introduced the symmetric primal-dual potential function for linear programming with a short-step method. Kojima, Mizuno and Yoshise (1991) gave a symmetric long-step primal-dual potential-reduction method for linear complementarity problems; their Lemma 2.5 is the linear-programming case of the key inequality posed here. Nesterov and Nemirovskii (1994, §4.5) extended Ye's non-symmetric method to general cones. Nesterov and Todd (1997) extended the method of Kojima et al. to self-scaled cones; the companion paper (1998) treats short-step and functional-proximity variants.
Let be a finite-dimensional real vector space with dual and pairing . Let be a proper cone: closed, convex, with nonempty interior, and pointed (it contains no line). Its dual cone is .
A -self-concordant logarithmically homogeneous barrier for is a convex function on that tends to at the boundary, satisfies the self-concordance inequality , the bound , and for . Its conjugate barrier is
is -self-scaled (Definition 2.1) if for all , and . For , the scaling point is the with .
The distance to the boundary is measured by
so for ; local norms are .
The problem is the primal-dual pair , with surjective. For the primal-dual potential is
One iteration from a strictly feasible : take the scaling point and ; solve
put , , and accept any with .
with and , and the same bound for every accepted step , whose iterate is again strictly feasible. The constant is the paper's.
In attack order: the structure of Hessians (Theorem 3.1), existence and uniqueness of scaling points (Theorem 3.2), convexity of (Lemma 3.1) and the third-derivative bounds (Corollary 3.2 (i)–(ii)); the long-step Hessian comparison (Theorem 4.1), its corollaries (Corollary 4.1 (i)–(ii)), the barrier estimate (4.8) (Theorem 4.2) and the scalar monotonicity facts (Proposition 4.1); separability along orthogonal boundary directions (Lemma 5.1, Theorem 5.1) and the key inequality
and unique solvability of the projection system (Proposition 6.1).
A constant decrease of per iteration gives, through the bound of Nesterov–Nemirovskii (Theorem 8.1 of the paper), primal and dual solutions within of optimal in iterations when , with step sizes that are long (a fixed fraction of the distance to the boundary) rather than confined to a Dikin ellipsoid. Theorems 4.1–4.2 and 5.2 are reused by the potential-reduction and path-following analyses of the same paper and by later work on symmetric cones.
The results are proved in the paper. They are not formalized anywhere known to us: Mathlib has no self-concordant barriers, and the platform has the definitions of self-scaled barriers (from the companion 1998 paper) but none of these theorems. The mission produces machine-checked versions of the paper's structure theory of self-scaled barriers (§§3–5) and of the per-iteration decrease of its primal-dual method.
The obvious attempt bounds the change of and along the step by self-concordance alone. Self-concordance controls only for , so it cannot certify a step of length , which may be far outside the Dikin ellipsoid. The long-step analysis needs Theorem 4.1, which compares Hessians all the way to the boundary and holds for self-scaled barriers but fails for general self-concordant ones. The constant decrease then needs a lower bound on , where is the scaled norm of the right-hand side of (8.1); that bound is Theorem 5.2, whose proof rests on the separability of along orthogonal boundary directions (Theorem 5.1), a structural property with no analogue for general barriers.
EuclideanSpace), identified through the inner product; is ContinuousLinearMap.adjoint A. is hess F (derivative of gradient F), is fderiv ℝ (hess F) x u, is ContinuousLinearMap.inverse.IsProperCone, IsSelfScaledBarrier, conj, IsScalingPoint, IsPrimalStrict, IsDualStrict, sigma, lnorm (SelfScaledIPM.ShortStep), and ConvexOptimization.dualCone. The barrier definition includes nondegeneracy of on , which follows from the other axioms for a pointed cone. conj K F is a supremum over and is only evaluated at points of . is an infimum, equal to the page's minimum at interior centres.IsProperCone K, IsSelfScaledBarrier K F ν and ; the paper derives from pointedness.SelfScaledLongStep.PrimalDual.Defs): the projection system (6.4), the potential , the system (8.1), and . The projection system is shared, under the same name, with the other missions of this series.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 .Thompson Sampling is the oldest bandit algorithm: Thompson proposed it in 1933 for allocating patients between two treatments (Thompson 1933). It keeps a posterior distribution over the unknown mean reward of every action, draws one sample from each posterior, and plays the action whose sample is largest. It is simple, widely used, and in experiments competitive with index policies designed for optimality. For decades it had no matching theoretical guarantee.
The benchmark for a stochastic bandit algorithm is the lower bound of Lai and Robbins (1985): every consistent policy draws a suboptimal arm at least times in rounds, where is the Kullback–Leibler divergence. A policy that attains this rate is called asymptotically optimal.
Timeline.
There are arms. Arm yields reward with probability and otherwise. Arm is the unique optimal arm: for every . The gap of arm is , and denotes the largest mean among the suboptimal arms.
Thompson Sampling with uniform priors. Let be the number of times arm has been drawn before round and the number of rewards equal to among those draws. With a uniform prior, the posterior of is . In round the algorithm draws, independently, a sample from each posterior, plays , and observes the reward of .
The regret after rounds is
where now counts the draws of in rounds . The Bernoulli divergence is .
The analysis compares the Thompson samples with two index rules. For an arm with successes in draws, at round of a horizon , the KL-UCB index is , and the Bayes-UCB index is the quantile of order of the posterior .
For every there is a constant , depending on and the instance, such that for every horizon ,
Only the existence of is asserted; its value is not fixed, so improvements of the lower-order terms do not invalidate the goal.
The result. Theorem 1 shows that the leading constant of Thompson Sampling's regret equals the Lai–Robbins constant, so no consistent policy does asymptotically better on Bernoulli bandits. It settled a question open since 1933 and is the starting point for later optimality proofs of Thompson Sampling for exponential families and Gaussian rewards. Proposition 1, a summable tail bound on the event that the optimal arm is under-sampled, is the reusable core: it is a deviation inequality for the number of draws of the optimal arm, which a bound on its expectation does not imply.
The formalization. The result is proved on paper; no machine-checked proof of an optimal-constant bound for Bernoulli Thompson Sampling exists. The platform already has the Gaussian frequentist analysis of Lattimore and Szepesvári (Theorem 36.3) and the non-optimal Agrawal–Goyal bound. This mission adds the Bernoulli, Beta-posterior case with the KL constant, the KL-UCB and Bayes-UCB indices with the exploration rate, and the optimal-arm tail bound. Corrected statements are part of the output: the explicit constant printed at the end of Lemma 2's proof is too small, the constant printed for Lemma 3 has the wrong sign, and Lemma 3 as printed quantifies over arbitrary random intervals, which its proof does not support.
The standard proof for an optimistic index policy bounds the draws of a suboptimal arm by an under-estimation term and a concentration term. For Thompson Sampling the under-estimation term is not small: once the posterior of arm is concentrated, is close to in every round. Comparing with a lower confidence bound instead only helps if is large with overwhelming probability, and a bound on does not give that.
Proposition 1 supplies it, and it carries most of the difficulty. It must control long stretches of rounds in which arm is never drawn while several suboptimal arms compete, and it needs the samples of arm conditioned on its successes at a random time while the arm is not played, an optional-skipping step that the paper leaves implicit and that is the main measure-theoretic obstacle in Lean.
Representation. The algorithm is the published Thompson Sampling run (AgrawalGoyalTS_TwoArmed_ThompsonSampling) on the published Bernoulli bandit (bernoulliRelativeEntropy). That run is Agrawal–Goyal's Algorithm 2, which passes each reward through a Bernoulli trial of success probability equal to the reward; for rewards the trial returns the reward almost surely, so the posterior is exactly the paper's. Probabilities are values of tsLaw in , expectations of counts and the regret are lower integrals in , and every bound compares with the embedding of a real right-hand side.
Conventions.
Added hypotheses and corrections.
Trivializations ruled out. Thompson Sampling is not characterized by a predicate that an arbitrary policy could satisfy: it is the published run, which fixes the posterior draws, the argmax and the updates. The constant is quantified as , never , and no real number is extracted from a possibly infinite expectation.
Infrastructure and contributions. A complete development needs Beta–Binomial duality, Chernoff–Hoeffding bounds for binomial tails, optional skipping for the reward stacks of the played arms, and the KL-UCB counting argument. The Beta–Binomial identity is an open milestone shared with the Agrawal–Goyal mission. Proofs of any milestone, in particular Proposition 1, Lemma 4 and the analytic Lemma 3, are welcome; Lemma 3's bound and the index comparison are pure real analysis and reusable beyond bandits.
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.
A sparse graph that approximates a dense one, in the sense that both have nearly the same Laplacian quadratic form, can stand in for it in every algorithm that only reads cuts or solves Laplacian linear systems. Spielman and Teng introduced such spectral sparsifiers and built them in nearly linear time; the construction is the sparsification step of their nearly-linear-time Laplacian solver (arXiv:0808.4134, SIAM J. Comput. 40(4), 2011).
Sampling edges at random works well only inside a graph of high conductance, where no vertex set is separated from the rest by few edges. A general graph is therefore first cut into pieces of high conductance, with few edges running between the pieces. Section 7 of the paper proves that such a decomposition always exists. A similar result was obtained independently by Trevisan (2005). The decomposition theorem, together with the sampling theorem of §6, already shows that every graph has a spectral sparsifier with edges; the algorithmic decomposition of §8, which the fast algorithm uses, is an approximate version of it, and its analysis rests on the same certificate lemma.
Let be a finite simple undirected graph with edges, and write for the degree of vertex . For disjoint , is the set of edges with one end in and one in . The volume of is ; in particular .
For a vertex set and , the conductance of inside is
and the conductance of is over proper subsets, with when . Volumes are always measured with the degrees of , never with the degrees inside the induced subgraph ; consequently is at most the usual conductance of , and lower bounds on transfer to it.
A decomposition of is a partition of . It is a -decomposition if for all , and its boundary is the set of edges between different parts,
In Lean: vol G S, cutEdges G S T , condRel G B S , cond G B , and decompBoundary G P for a Finpartition P of the vertex set, all in the namespace SpectralSparsify.Decomp.
Every graph without isolated vertices has a decomposition with
The constants are the paper's. Both conditions must hold for one and the same partition.
The theorem says that every graph is, after removing at most half of its edges, a disjoint union of pieces of conductance . By Cheeger's inequality each piece then has normalized spectral gap , which is the hypothesis under which the random sampling of §6 produces a spectral approximation; applying the theorem recursively to the removed edges gives the existence of spectral sparsifiers with edges (§7.2). Decompositions of this kind, now called expander decompositions, have become a standard tool in graph algorithms.
The theorem is proved in the paper; to the knowledge of this mission it has no machine-checked proof. What the mission produces is a formal proof of the existence statement with the paper's explicit constant, a formal Lemma 7.2 (the certificate lemma that also drives the approximate version, Theorem 8.1), and reusable Lean definitions of volume, relative conductance and decomposition boundary for finite simple graphs.
The obvious argument, cutting along any sparse set until no sparse set is left, controls the conductance of the final parts but not the number of edges cut: a long sequence of small sparse cuts can remove far more than half of the edges. The difficulty is to show that one well-chosen cut leaves a remainder whose conductance is certified without further search, which is the content of Lemma 7.2. Its hypothesis is a maximality condition over all subsets of , and its conclusion concerns all subsets of , a different set measured with the same ambient degrees, so the two cannot be compared directly. The existence statement then needs a well-founded description of the recursion, a bound on its depth, and an accounting of the cut edges level by level, all against the explicit constant .
Graphs are SimpleGraph V on a finite vertex type with decidable adjacency; vertex sets are Finset V; volumes, conductances and the bound on are real numbers; decompositions are Finpartition (Finset.univ : Finset V); is Real.logb (4/3).
Hypotheses made explicit:
∀ v, 0 < G.degree v) in Theorem 7.1, Lemma 7.2 and the milestones that divide by a volume. The paper leaves it implicit: is for sets of isolated vertices, and with Lean's Lemma 7.2 would be false (one edge plus two isolated vertices is a counterexample). Under the hypothesis forces , and Theorem 7.1 is then trivially true.Conventions: is the minimum over proper subsets, the empty set contributing ; for ; counts ordered adjacent pairs in , which is the edge count for disjoint sets. Neither conclusion of Theorem 7.1 may be dropped: the partition into singletons satisfies the conductance bound and the partition into one part satisfies the boundary bound, so a formalization keeping only one conclusion is trivial.
Not formalized: idealDecomp as an object (step 2 involves a choice, so it is a relation rather than a function; the goal is the existence statement), its termination and depth bound as separate items, the λ-spectral decomposition remark via Cheeger's inequality, the existence sketch for sparsifiers in §7.2, and the algorithmic analogue of §8. Contributions welcome: proofs of the milestones, a formal recursion for idealDecomp, and lemmas on volume and edge-boundary arithmetic that other graph-partitioning missions can reuse.
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;