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.
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?
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.
Mean–variance portfolio selection (Markowitz, 1952) trades off the expected terminal wealth of an investor against its variance. In a dynamic setting the problem is time-inconsistent: the variance is not a conditional expectation of a function of terminal wealth, so the dynamic-programming principle fails, and a strategy that is optimal when computed at time is no longer optimal when re-evaluated at a later time. A standard response is to treat the investor at each time as a separate player and to look for a subgame-perfect equilibrium strategy, which no future self wishes to deviate from locally (Björk–Murgoci, Ekeland–Lazrak, and others).
Hu, Jin and Zhou (arXiv:1111.0818v1; SIAM J. Control Optim. 50(3), 2012) define open-loop equilibria for a general class of time-inconsistent stochastic linear–quadratic (LQ) problems and characterize them through a flow of forward–backward SDEs. Their §5 applies this to mean–variance investment in a complete market with a random risk premium, where the weight on expected wealth depends on current wealth (a state-dependent risk aversion, motivated in Björk–Murgoci–Zhou, 2014). Earlier equilibrium results for mean–variance investment (Basak–Chabakauri, 2010; Björk–Murgoci–Zhou) work with deterministic or Markovian coefficients and within feedback classes.
This mission is the third of a series on the paper. Mission I formalizes the general sufficient condition (Theorem 3.2); Mission II treats deterministic coefficients and coupled Riccati equations (Theorem 4.4). This mission targets the explicit mean–variance equilibrium of Theorem 5.4.
Fix a horizon and a probability space carrying a standard -dimensional Brownian motion with its filtration ; write . The market has a deterministic bounded interest rate and a progressively measurable, essentially bounded risk premium with values in . A strategy is a progressively measurable with (the class ); the wealth under solves
At time , with current wealth , the investor's cost is
This is the case of the paper's general LQ problem, with , , , , , ; the mission states it that way. For , and an -measurable square-integrable , the spike perturbs on a short window. A strategy with wealth is an equilibrium (Definition 2.1) if, for all such and ,
The equilibrium is built from , , and two backward SDEs: an indefinite stochastic Riccati equation for ,
and a linear BSDE (5.13) for whose coefficients involve and . A process gives a BMO martingale if for all stopping times .
If solves (5.8) with bounded and , and solves (5.13) with bounded, then
is an equilibrium: the closed-loop wealth exists, and for every closed-loop wealth the strategy satisfies Definition 2.1.
Theorem 5.4 gives the equilibrium of a time-inconsistent mean–variance investor in closed form, linear in current wealth, for a random risk premium. With a deterministic premium it reduces to explicit formulas (§5.4), and for it recovers the equilibrium of Basak–Chabakauri and Björk–Murgoci; for it differs from the feedback equilibrium of Björk–Murgoci–Zhou, which shows that open-loop and feedback equilibria are different notions. The random premium is what makes and the feedback gain unbounded.
The result is proved in the paper; nothing here is formalized elsewhere. The mission produces machine-checked statements of the equilibrium, of solvability of the Riccati-type BSDE (5.8), and of the integrability of a linear SDE with BMO-type coefficients, on the platform's published stochastic-calculus substrate. The definition of BMO martingales and the encoding of open-loop equilibria are reusable beyond this paper.
The verification step that most readers try first, plugging into the wealth equation and applying standard SDE estimates, fails: the gain is unbounded, because is only BMO, so the closed-loop SDE is linear with non-Lipschitz-bounded random coefficients and neither existence of the wealth nor follows from standard theory (Proposition 5.3). The BSDE (5.8) has a driver with quadratic growth in and a singular factor ; it is not covered by the standard theory of stochastic Riccati equations and its solution must be bounded away from zero for the feedback to make sense. Uniqueness in (5.8) and solvability of (5.13) rely on BMO-martingale and change-of-measure facts (Kazamaki) that are not in Mathlib. Finally, the equilibrium property is a statement about every and every perturbation, and the sufficient condition (Theorem 3.3) needs the limit behaviour of conditional expectations as .
Everything is built on the published definition Peng1990_SMP_Stochastic (Brownian motion, , Itô integrals, SDEs and BSDEs as relations). The general LQ model, the spike, the conditional cost and Definition 2.1 are in Model; the adjoint equation on , and condition (3.4) in Adjoint; the market, , , BMO, (5.8), (5.13) and (5.14) in Market. Conventions the statements commit to:
The goal does not assume the BMO properties of and (they are conclusions of Propositions 5.1–5.2), does not assume deterministic or (that is the special case of §5.4), and keeps , ; a formalization that assumes any of these, or that admits the junk value on a non-null set, proves a different theorem. Theorem 3.3, the sufficient condition used in the last line of the proof, is the case of Mission I's goal and is not restated here. Welcome contributions: a BMO and Girsanov library on the Peng substrate, existence for quadratic BSDEs, and a proof of the sufficient condition.
Manufacturers routinely share rolling schedules with their suppliers: each period the buyer commits to a purchase for the current period and issues non-binding estimates for future periods, then revises those estimates as the horizon rolls forward. Unconstrained revisions push forecast risk upstream and are a recognized source of the bullwhip effect. A quantity flexibility (QF) contract bounds how far each estimate may move between consecutive issues, giving the supplier a guarantee in exchange for a commitment to cover any order within the bounds. Tsay and Lovejoy (MSOM 1(2), 1999) model a chain of firms linked by QF contracts and ask how a firm in the middle of the chain, the flex node, should translate the schedules it receives into the schedules it issues. Their answer is the Minimum Commitment (MC) policy, justified by Proposition 1: MC solves the node's open-loop planning problem and never breaks either contract.
This mission formalizes Proposition 1. A companion mission (Quantity Flexibility Contracts and Supply Chain Performance 1) formalizes Proposition 2, on when MC keeps zero inventory.
Periods are . In period the node receives from its customer a release schedule : is bought now, estimates the purchase in period . The node issues to its supplier a replenishment schedule of the same form. Its ending stock is .
The contracts carry parameters and (): output parameters with the customer and input parameters with the supplier. The incremental revision (IR) constraints are, for all and ,
The cumulative parameters are and , so . A convex cost , minimized at , is charged on ending stock.
At period , with , and known, the open-loop program (F-OLFC) chooses and the planned purchases , , to minimize subject to the stock balance (17), coverage (18), the input IR constraints (19) between and , and the cumulative bounds (20).
The MC policy computes and projected inventories by one recursion on : ,
In Lean: QFParams, Acum, Ωcum, IROut, IRIn, mcStep, run, inv, sched, projInvAt (module Model) and stock, Feasible, RelaxedFeasible, objective, lbar, pStar (module FOLFC).
For an MC run from with , against any customer schedules obeying (6), and any convex minimized at zero:
and for every the schedule , with suitable planned purchases, is feasible for (F-OLFC) at period and attains its minimum.
Proposition 1 is what makes MC a well-defined operating rule for an intermediate firm: whatever the customer does within its contract, the node can serve it from stock and its own revisions stay within the supplier's contract, so the chain of contracts composes. Proposition 2 and the paper's simulation study of how flexibility propagates along a supply chain (§§5–6) both assume the node uses MC, and rely on Proposition 1 for that choice being both feasible and myopically optimal.
The paper's optimality argument is sketched: the relaxed solution is attributed to "a straightforward application of Kuhn–Tucker conditions" with details in an unpublished thesis, the equivalence of (32) with (21)–(23) is omitted, and Lemma 1's proof is replaced by intuition. A machine-checked proof supplies these steps. To our knowledge no part of this paper has been formalized before. The mission also fixes the statement: the printed range of (19) makes the optimality claim false, and the claim needs a start of the run that the paper leaves implicit.
The obvious argument treats (F-OLFC) as a lot-sizing problem with minimum lot sizes and observes that the greedy purchases (30) are optimal. That only solves the relaxation. The difficulty is that MC is not stated through (30): it is a recursion on the replenishment schedule with a positive part in the projected inventory, and one has to show that the MC schedule can carry the greedy purchases within the upper bounds of (19) and (20). Those bounds can bind, and whether they do depends on the previous period's schedule, so the optimality claim is not a one-period statement: it needs an induction over the run, through Lemma 1 and the customer's IR constraints. The admissibility half needs the same induction, with the nonnegativity of the schedules carried along.
All quantities are real numbers. Parameters are sequences ℕ → ℝ whose index is unused; schedules are infinite sequences, and the MC recursion runs over all . (6) and (7) are written with replaced by . The standing assumptions , () are hypotheses. is any convex function with for all ; no strict convexity, differentiability or monotonicity is assumed.
The run starts from an arbitrary state (run period ); the MC policy acts from period . The following departures from the printed statement are disclosed:
(F-OLFC) ranges over all real schedules and purchases; the only MC-specific object in the goal is the candidate schedule. Optimality is stated as "feasible, and no feasible point has a smaller objective", never as an infimum, so an infeasible program cannot make it vacuous. The MC step is literally (21)–(23), with the carried-over term and the positive part; a run that sets or drops the max is a different policy.
Infrastructure: the model and (F-OLFC) are self-contained over Mathlib (Finset.prod, ConvexOn). Proofs of the three milestones, and of the monotonicity of a convex function minimized at zero on , are welcome as separate contributions.
In distributed computing, many graph problems (minimum spanning tree, shortest paths, connectivity checks) are solved by processors that sit at the vertices of the input network and communicate only along its edges. When every edge can carry only a few bits per round, the number of rounds an algorithm needs can be far larger than the network's diameter. Understanding by how much is the central question of the CONGEST (here: B) model of Peleg's monograph Distributed Computing: A Locality-Sensitive Approach (SIAM, 2000).
Das Sarma, Holzer, Kor, Korman, Nanongkai, Pandurangan, Peleg and Wattenhofer (SIAM J. Comput. 41 (2012) 1235–1265) proved round lower bounds for a long list of verification problems (is a given subgraph a spanning tree, a cut, a Hamiltonian cycle, …) and for approximating optimization problems such as the minimum spanning tree and shortest paths. Every one of those bounds goes through a single reduction, the Simulation Theorem (Theorem 3.1), which transfers lower bounds from two-party communication complexity to distributed algorithms.
Timeline:
A B-model network is an undirected graph whose vertices are processors with unbounded local computation. Computation proceeds in synchronous rounds; in each round, every vertex sends a message of bits along each incident edge in each direction, then updates its local state from its old state and the messages it received. Two vertices and hold inputs ; all other vertices start without input. A public-coin randomized algorithm additionally lets all vertices read a shared random string. It computes with -error in rounds if, for every , both and output after round with probability at least . is the least such .
In the communication complexity model, Alice holds , Bob holds , one bit is sent per round, and both must output . is the least number of bits of an -error public-coin protocol.
The network consists of paths with vertices each, a complete -ary tree of depth with vertices at level , and spoke edges joining each leaf to on every path. The inputs sit at the two extreme leaves, and . The -right set consists of all path vertices at positions , the leaves with , and their ancestors; the -left set is the mirror image, and , . denotes the vector of states of the vertices of at the end of round .
If a public-coin algorithm on computes with -error in rounds and
then some public-coin two-party protocol computes with -error using at most
The theorem turns any lower bound , such as those for set disjointness and equality, into a round lower bound on : an algorithm with rounds forces . Choosing the parameters gives the paper's bounds of order rounds for verification and approximation problems (§§4–7), and the same reduction underlies a large body of later CONGEST lower bounds.
The result has been proved since 2011. A machine-checked version would provide the first formal model of synchronous bandwidth-limited message passing and of public-coin two-party protocols on the platform, together with a verified reduction between them. No formalization of the theorem, of the B model, or of two-party communication protocols is known to exist in Mathlib or on the platform.
The informal proof is short; the work lies in making the information flow precise. The naive simulation, in which Alice simulates the vertices near and Bob those near , fails because the cut between the two halves contains path edges plus the spokes, and can be large: sending every message across it costs bits per round. The argument must instead let both parties' simulated regions shrink by one path position per round, so that the only messages crossing into Bob's region come from tree vertices with children each. Making this rigorous requires a careful accounting of which vertices belong to , which edges leave , and why the functions that update the configurations do not depend on the other party's input.
(Fin Γ × Fin (d^p)) ⊕ Σ ℓ : Fin (p+1), Fin (d^ℓ); paths are numbered from . The children of are , . are Finsets defined for every , with the paper's special case at . The nodes require .Fin B → Bool) on every directed edge in every round. Optional or variable-length messages would let silence carry information and make the theorem false (e.g. at ).PMF on an arbitrary type, shared by all vertices (resp. both parties); -error requires both outputs to be correct on the same random string, and .sInf, which would be on an empty set; the goal is stated for every algorithm.Contributions welcome: proofs of the milestones, and reusable infrastructure for executions of message-passing algorithms (locality lemmas such as Observation 3.3 hold on any graph).
Assortment optimization asks which subset of products a firm should offer when customers choose among the offered products, or leave without buying. It underlies shelf-space planning in retail, the choice of which fare classes to keep open in airline revenue management, and the selection of items shown on a web page. The multinomial logit (MNL) model is the standard choice model in this literature: when the model parameters are known, the optimal assortment is revenue-ordered, that is, it consists of the products with the highest revenues (Talluri and van Ryzin, 2004; Gallego et al., 2004; Liu and van Ryzin, 2008), so only candidate assortments need to be compared instead of .
In practice the parameters of the choice model are estimated from limited data. Rusmevichientong and Topaloglu (Operations Research, 2012) take a robust view: the parameters are only known to lie in an uncertainty set, and the firm maximizes its worst-case expected revenue. Their main structural result is that the revenue-ordered structure survives this uncertainty, whatever the uncertainty set. This mission formalizes that result and the comparative statics the paper derives from it.
There are products, , and product earns revenue . A customer's choice is governed by a parameter vector (all components strictly positive): is the weight of the no-purchase option and the preference weight of product . When the assortment is offered, the customer buys product with probability
and buys nothing with the remaining probability. The expected revenue of is
The parameters are unknown and lie in an uncertainty set , which is compact and nonempty. The Robust Logit problem maximizes the worst-case expected revenue:
Among the optimal assortments, is one with the smallest cardinality. For a single parameter vector , write and ; this is the classical problem with known parameters. Finally, for , and are the same quantities when every revenue is replaced by .
Equivalently: an assortment is optimal with smallest cardinality if and only if it is the set of products whose revenue strictly exceeds the optimal worst-case revenue. When this set is for some .
Milestones 3–6 are consequences of the goal on the same definitions.
Theorem 3.2 reduces the robust problem, a max–min over assortments and a possibly infinite parameter set, to at most revenue-ordered candidates, each requiring one worst-case evaluation . Applied to a singleton it also reproves the classical revenue-ordered optimality under known MNL parameters, together with the exact tie-breaking description. Corollary 3.5 and Theorem 3.6 say that more uncertainty calls for a larger assortment, and that the robust assortment is the largest assortment optimal for some parameter in ; Theorem 3.7 compares assortments when all revenues shift by a constant, which the paper uses in Section 4 to show that robust dynamic assortments grow with remaining capacity and over time.
The results are proved in the paper; none of them has a machine-checked proof on Prove2Me. The platform has ChoiceCDLP.MNL.top_ranked_optimal (from Liu and van Ryzin, 2008), a statement about top-ranked offer sets for known MNL weights, which is a different statement without uncertainty or tie-breaking. A formal development here gives a checked version of the robust structure theorem stated for arbitrary real revenues, the generality in which the dynamic part of the paper uses it.
The obvious argument fails at the max–min. For known parameters, Lemma 3.1 immediately shows that a product should be added exactly when its revenue beats the current expected revenue; but under uncertainty the minimizing parameter vector changes with the assortment, so one cannot compare and at a single worst-case . The argument has to establish a strict improvement uniformly over and then pass to the minimum, which is where compactness enters: a pointwise strict inequality survives the minimum only because it is attained. The tie-breaking rule is equally essential: a product with can be added to an optimal assortment without changing its worst-case value, so without the smallest-cardinality rule the characterization is false.
Products are Fin n, so Lean index stands for the paper's product . A parameter vector is p : ℝ × (Fin n → ℝ) with p.1 and p.2 i the weight of product ; IsPos p expresses . The expected revenue is the published definition ChoiceCDLP.MNL.mnlObjective. The worst case is a real infimum (sInf), and is a maximum over all subsets of products. is encoded as the predicate IsSmallestOptimal V r S (optimal, and of cardinality at most that of every optimal assortment), not as a choice function, so every statement about is asserted for every optimal assortment of smallest cardinality. and are the same objects for the revenue vector , which is exact since is at those revenues.
Standing assumptions and departures from the page:
The infimum is meaningful only under the standing assumptions (on an empty set it is ), which is why they appear as hypotheses of every statement. A complete development needs continuity of on positive vectors and attainment of minima on compact sets, both available in Mathlib, and finite maxima over Finset (Finset (Fin n)). The lemmas about (milestones 1–2) are reusable for any MNL model. Proofs of any milestone, and alternative proofs of the goal, are welcome.
The source is the authors' manuscript of 20 Sep 2011 of the Operations Research 2012 article; its printed page numbers equal the PDF's page numbers, and all page citations refer to it.
A differential variational inequality (DVI) couples an ordinary differential equation with a finite-dimensional variational inequality whose solution enters the dynamics as a control. Contact mechanics with friction, electrical circuits with diodes, dynamic traffic equilibria, hybrid engineering systems and the continuous-time limits of Nash games all have this form. Pang and Stewart's survey (Math. Program. 113, 2008; author's version hal-01366027) set up a common framework for these models and studied the most direct numerical method: the Euler-type time-stepping scheme, which replaces the time derivative by a difference quotient and solves one static variational inequality per time step.
For the scheme to converge, its iterates must exist and be bounded uniformly as the step goes to zero. Section 7 of the paper proves convergence once such bounds are available (Theorem 7.1). Section 8 supplies them for a class of DVIs in which the algebraic part is not affine: the constraint set is a cone and the VI map is a strongly monotone composite. This mission formalizes that section.
Fix , and dimensions . The data are , , , a map and a set . For ,
The initial-value DVI (6.2) is , , .
With and , the time-stepping scheme (7.2) starts at and computes, for ,
The standing assumptions are:
Choosing orthonormal bases of and of , the map is strongly monotone with some modulus (8.7).
Let be a closed convex cone, (A), (B), (D), (C′), and (E) hold. There is such that for every with and every the scheme has a unique run, and for all small
These are the hypotheses (7.5)–(7.6) of the convergence theorem of §7.
A companion item states Proposition 8.1, the derivative form of (D).
Theorem 8.1 is one of the two routes in the paper to convergence of the time-stepping scheme. The other (Theorem 7.4) needs a linear-growth property of the VI solutions that holds for affine or coercive problems; Theorem 8.1 replaces it by structural assumptions on that cover nonlinear complementarity systems on cones, including the case that yields the initial-value differential complementarity problem (Corollary 8.1). Combined with Theorem 7.1(a), it shows that the Euler trajectories have uniformly convergent subsequences whose limits are weak solutions of the DVI, and so gives existence of weak solutions constructively.
The paper's results are proved on paper but, as far as a search of Mathlib and the platform shows, no part of DVI theory is formalized. The formalization also settles a printed error: the bound (8.10) of Proposition 8.3 carries a factor that its proof does not justify, and the printed statement is false (a one-dimensional counterexample is recorded on the milestone). The milestone states the bound the proof does give; (8.14) and Theorem 8.1 are unaffected.
The obvious argument fails at the multiplier bound. The VI map is strongly monotone, but only with modulus of order , so the solution of each step is bounded only by times the data. This loss is harmless for existence and uniqueness but would destroy the uniform bounds (7.5). Recovering an bound requires separating the components of in , where is blind and only the order- monotonicity of helps, from the components in , where itself is strongly monotone; condition (E) and the cone structure of are what allow the two parts to be tested separately. A second difficulty is that (7.6) needs a Lipschitz bound on with a constant that does not blow up as .
EuclideanSpace ℝ (Fin k); matrices are continuous linear maps; is the adjoint; is the published definition SolodovSvaiterVI.Alg21.viSol Φ K.The development needs: existence for strongly monotone (coercive) VIs on closed convex sets; the implicit-function argument for the -equation of a step; orthogonal decompositions along ; and discrete Gronwall estimates. The VI existence result and the decomposition lemmas are reusable beyond this mission. Proofs of any milestone, and of the existence theorem for strongly monotone VIs as a separate theorem, are welcome.
Networks of coupled oscillators model generators in an electric power grid, pacemaker cells, Josephson junction arrays and many other systems in which units with their own rhythm interact through their phase differences. Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012, doi:10.1137/110851584) show that, after a singular-perturbation reduction, the transient-stability question for a lossy power network with non-uniform generators becomes a synchronization question for a non-uniform Kuramoto model: oscillators with different damping coefficients, different natural frequencies, an arbitrary coupling graph and phase shifts induced by line losses.
This mission concerns the cleanest regime of that model: lossless coupling and natural frequencies proportional to the damping. There the oscillators do more than agree on a frequency; they agree on a phase. For the classic Kuramoto model (Kuramoto, 1975) with identical frequencies, phase synchronization from inside an open half-circle was obtained by consensus methods for nonlinear coupled systems (Lin, Francis and Maggiore, 2007) and by Jadbabaie, Motee and Barahona (2004). Theorem V.10 of Dörfler–Bullo extends this to non-uniform damping, directed coupling with a globally reachable node, and gives an explicit worst-case rate for symmetric coupling. The proof rests on the contraction theory of time-varying consensus protocols (Moreau, 2004).
There are oscillators. Oscillator has a phase on the circle, a damping coefficient and a natural frequency . Oscillators interact through coupling weights (, with ) and phase shifts . The non-uniform Kuramoto model (8) is
The weights define a directed graph with an edge from to whenever ; a globally reachable node is a node to which every node has a directed path. For the closed arc set is the set of configurations whose angles all lie in a closed arc of length .
This mission assumes zero phase shifts, , and proportional frequencies, for all . The phases synchronize exponentially to a trajectory when there are and with for all and .
For the rate, is the Laplacian of a weight array, is its second-smallest eigenvalue (the algebraic connectivity) when , , , , and .
For every solution with , :
Theorem V.10 gives phase synchronization of non-uniform oscillators from every initial configuration inside an open half-circle, for directed coupling graphs that need only a globally reachable node, and identifies the limit phase: anywhere in the initial range in general, the damping-weighted mean under symmetric coupling. The rate separates three effects: graph connectivity (), initial phase cohesiveness () and non-uniformity of the damping (, ). For the classic Kuramoto model the statements reduce to known results ([19] and [33] of the paper).
The result is proved in the paper; no machine-checked proof is known. A formal proof needs a Dini-derivative argument for the maximum of finitely many smooth functions along an ODE, a contraction theorem for linear time-varying consensus with positive, bounded weights on a graph with a globally reachable node, and a Courant–Fischer bound on the weighted disagreement. Each is a reusable piece of infrastructure for networked control and synchronization.
The obvious argument linearizes: , so the model looks like linear consensus. That only holds near the diagonal; from an arc of length close to the effective weights come close to zero and depend on the state, so neither a fixed Laplacian nor a local linearization covers the claimed region. One needs first that the arc never grows, which is a statement about a non-smooth function (the arc length) along trajectories, and then exponential convergence of a consensus protocol whose weights are time-varying and, for directed graphs, non-symmetric, so there is no quadratic Lyapunov function in general. For the explicit rate the disagreement vector is orthogonal to , not to , and the angle between the two hyperplanes has to be controlled.
Angles are represented by real lifts ; the vector field is -periodic in each coordinate, so solutions on the torus are projections of solutions on . is encoded as for all on the initial lift, and every conclusion (invariance, , , the weighted mean, the convergence bounds) refers to that lift and the same continuous lifted trajectory, which is at least as strong as the statement on the torus. A solution is a curve on whose derivative within equals the vector field at every ; statements quantify over every such curve. The model is stated with the paper's general field and hypotheses , ( arbitrary, not set to zero).
Conventions and corrections, each disclosed in the item's Formalization Note:
AlonMilman.PropertyT.lambda1 applied to the symmetric Laplacian.Exponential convergence requires a rate ; a statement with or with a solution predicate that no curve satisfies would be trivial. The synchronous trajectory satisfies the solution predicate, so the hypotheses are satisfiable.
Infrastructure welcome beyond this mission: upper Dini derivatives and comparison lemmas for maxima of differentiable functions, exponential stability of linear time-varying consensus (Moreau's theorem), and Laplacian ordering for entrywise-dominated weights.
A real number is normal in base when every block of base- digits occurs in its expansion with limiting frequency , exactly as it would in a sequence of independent uniformly random digits. It is normal (absolutely normal) when it is normal in every base . Whether the classical constants of analysis, above all , are normal is one of the oldest open questions linking number theory and probability: it asks whether a number defined by geometry has digits that are statistically indistinguishable from random ones.
Timeline.
Large-scale digit computations of are statistically consistent with normality. No base is known in which is normal, and it is not even known that any particular digit occurs infinitely often in its decimal expansion.
A digit sequence is a function ; is the first digit after the point. A word is a finite list of naturals. For , the occurrence count is the number of positions with for every . Overlapping occurrences each count.
The sequence is normal in base (IsNormalSeq b s) if, for every word with all entries ,
The -th base- digit of a real after the point is
The real is normal in base (IsNormalReal b x) if is normal in base . Two remarks:
This is the conjecture in its standard form, normality in every base. The base-ten case is the special case .
None are listed. No decomposition of this problem into intermediate statements is known that would be a faithful attack path, and the mission does not invent one. Proposals for intermediate targets are welcome in the discussion; see the contributions listed under Formalization scope.
The known theorems of the subject (Champernowne's constructions, the Copeland–Erdős theorem, Borel's theorem) concern numbers built to be normal or almost every number; they are not steps toward and are kept in the separate mission Explicit normal numbers: Champernowne and Copeland–Erdős.
A proof that is normal in base would give every finite digit pattern a definite limiting frequency in its expansion. It would be the first normality result for a classical constant not built to be normal. Every known normal number is constructed digit by digit (Champernowne, Copeland–Erdős, Sierpiński, Becher–Figueira) or shown to exist by a measure argument (Borel). Even the base-2 case would settle the Bailey–Crandall programme for .
Formalization status. The goal is open mathematics. The definitions it is stated with are published and are shared with the mission Explicit normal numbers: Champernowne and Copeland–Erdős, where Champernowne's theorems and the Copeland–Erdős theorem have machine-checked proofs.
The constructive results all prove normality from the digit-by-digit description of the number. In particular, the Copeland–Erdős block criterion needs the expansion to be an explicit concatenation of blocks. has no such description. Its known series (Machin-type formulas, BBP) give digits as values of exponential sums, and no known method controls the joint distribution of long digit blocks of such values.
Borel's theorem does not help: it only says that the exceptional set is null, and gives no criterion for deciding whether a given number lies in it. Neither high-precision digit statistics nor irrationality measures for imply normality.
All declarations live in the namespace Normal and use the definition bundle Normal_Core:
count, IsNormalSeq, digit, IsNormalReal;ofDigits b s ;flatten, digitsBE, concatDigits;Committed conventions:
The definitions agree with Borel's, and the mission does not admit a trivialising reading. A real number is not normal merely because it is irrational, and the empty word imposes only the trivial condition.
The bundle also contains a verbatim copy of the integer-arithmetic definition IsNormal from xiangyazi24/agafonov; its equivalence with IsNormalSeq is proved on the platform (Normal.isNormalSeq_iff_isNormal), so results stated in either form transfer.
Welcome contributions:
A real number is normal in base when every block of base- digits occurs in its expansion with limiting frequency , as it would in a sequence of independent uniformly random digits. Borel introduced the notion in 1909 and proved that almost every real number is normal in every base, by an argument that produces no example. This mission collects the two classical papers that do produce examples: Champernowne's construction of and the theorem of Copeland and Erdős, which shows that the concatenation of any sufficiently dense increasing sequence of integers, the primes included, is normal.
Timeline.
A digit sequence is a function ; is the first digit after the point. A word is a finite list of naturals. For , the occurrence count is the number of positions with for every ; overlapping occurrences each count.
The sequence is normal in base (IsNormalSeq b s) if, for every word with all entries ,
The -th base- digit of a real after the point is , and is normal in base (IsNormalReal b x) if is normal in base . The integer part of plays no role; for a rational with two expansions the floor selects the one not ending in repeated 's.
If is an increasing sequence of positive integers such that, for every , the number of exceeds for all large , then the digit sequence obtained by writing the base- expansions of one after another is normal in base . A machine-checked proof is on the platform.
These are the standard examples of explicitly given normal numbers, and the Copeland–Erdős block argument is the model for most later constructions. The mission also fixes a definition of normality for real numbers together with the transfer from digit sequences to reals, which other work on normal numbers can import.
All declarations live in the namespace Normal and use the definition bundle Normal_Core: count, IsNormalSeq, digit, IsNormalReal; ofDigits b s ; the concatenation operators flatten, digitsBE, concatDigits; the Champernowne and Copeland–Erdős constants.
Conventions: digits are read after the point with the floor convention above; frequencies are limits of real quotients; words of every length with entries are quantified; results for real numbers are stated for bases by hypothesis.
The proofs are imported from the repository xiangyazi24/normal and verified by the platform. Their auxiliary lemmas are published on the platform as dependencies of the milestones and are not listed as items of this mission.
The open question whether is normal is a separate mission and is not approached by the methods here, which rely on the number being given as an explicit concatenation of blocks.
Many problems in machine learning and statistics minimize an average of smooth losses, one per training example: regularized least squares, logistic regression, and other forms of empirical risk minimization. Two classical families of methods attack such finite sums. The full gradient method evaluates all component gradients per iteration and converges linearly for strongly convex objectives, but each iteration costs gradient evaluations. The stochastic gradient method evaluates a single component gradient per iteration, so its iterations are cheap, but it converges only sublinearly, at rate , even under strong convexity.
Le Roux, Schmidt and Bach (arXiv:1202.6258, NIPS 2012) introduced the stochastic average gradient (SAG) method, which keeps a table of the most recently evaluated gradient of every component and moves along their average. It evaluates one component gradient per iteration, like the stochastic gradient method, and the paper proves that it nevertheless converges linearly in expectation. SAG was among the first of the variance-reduced incremental methods; SAGA (Defazio, Bach & Lacoste-Julien, 2014), SVRG (Johnson & Zhang, 2013) and their accelerated variants followed. Its predecessor, the incremental aggregated gradient method of Blatt, Hero & Gauchman (2007), selects the components cyclically and had a linear rate only for strongly convex quadratics, without an explicit constant.
This mission covers the paper's first main result, Proposition 1, which uses the step size . The second result, Proposition 2, for the larger step size , is a separate mission of this series.
Let and minimize
Each is convex and differentiable, and its gradient is Lipschitz continuous with constant : for all . The average is strongly convex with constant : the function is convex. Then has a unique minimizer . The gradient variance at the optimum is .
The SAG iteration with step size maintains a state . Starting from and the zero table , for an index is drawn uniformly from , independently of the past, and
The table is refreshed before the iterate moves, so uses the new gradient. Expectations are over the indices only; the data are fixed.
With the constant step size , for every ,
The constants are those printed in the paper.
The proof tracks a quadratic Lyapunov function with and an explicit block matrix (p. 19). The milestones, in the order the proof uses them, are:
Proposition 1 gives a linear rate for a method whose per-iteration cost does not depend on . Measured in passes through the data, its rate per pass is comparable to the full gradient method's, while each pass of SAG touches every component only once on average. The bound depends on the initial point only through and on the data only through , which is zero when every component is minimized at .
The result is proved in the paper and has been widely re-derived, but it has no machine-checked proof that this mission is aware of. A formalization would be the first verified linear-rate theorem for SAG. Lemma 1 is an exact identity, valid for every quadratic Lyapunov function of the same block form, and is reused verbatim in the proof of Proposition 2. Milestones 2, 3 and 7 are general facts (co-coercivity, completing the square, a Schur-complement domination) that recur throughout the analysis of incremental methods.
The iterate alone is not a Markov chain: its evolution depends on the stale gradients in the table, so neither nor decreases in expectation from one step to the next. The obvious first idea, bounding in terms of as for the stochastic gradient method, fails because the cross terms between the table error and the iterate error have no sign. The analysis must therefore control the table and the iterate jointly, through a function of the whole state ; the exact expected one-step change of a general quadratic form in (Lemma 1) is the computation everything else rests on, and it requires careful bookkeeping of block matrices.
is EuclideanSpace ℝ (Fin p) and the components are indexed by Fin n with . The components and their gradients are both given, tied by HasGradientAt; each is convex (§A.1, p. 13), which the proof's co-coercivity step needs; and are the published SAGA.Convex.fAvg and SAGA.Convex.gradAvg. Strong convexity is stated literally as on p. 5, as convexity of . The point is any minimizer of ; uniqueness and are consequences. The restriction used in the proof is not assumed, since it follows from the hypotheses when .
The SAG state is a pair (table, iterate); SAG.SmallStep.step refreshes the table entry and then moves the iterate, and SAG.SmallStep.runFrom applies the steps for a given index sequence. The goal starts from the zero table and fixes the step size . The expectation is SAGA.Convex.expectIdx n k, the uniform average over all index sequences, which is exactly the law of independent uniform indices; a conditional expectation given is the average over the next index from an arbitrary current state. Block matrices are families of blocks (continuous linear maps), and Lemma 1 makes explicit the symmetry of and and the identity that its proof uses. The domination is stated for every : the page's closing remark "for " is stronger than its own computation needs.
The goal bounds the average over all index sequences; a bound for each fixed sequence would be false, and a bound for one sequence would be a different, weaker statement. Proposition 1 is not to be formalized with a free step size, an arbitrary initial table, or a variance quantity other than at : each of these changes the constant .
Needed infrastructure: algebra of finite sums of inner products over block families, the tower property for the uniform average over index sequences, co-coercivity of convex smooth functions (published on the platform as ConvexOptAlg.SmoothGD.eq_3_6), and strong-convexity monotonicity of the gradient. Proofs of individual milestones are welcome, as are alternative proofs of the goal that bypass the Lyapunov function.
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.Transient stability of a power grid asks whether the generators of the network return to synchronous operation after a large disturbance such as a fault or a line trip. In the classical network-reduced model the rotor angles obey second-order swing equations, and stability certificates usually come from energy functions evaluated numerically. Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012) relate this problem to a first-order system of coupled phase oscillators, the non-uniform Kuramoto model, and derive purely algebraic conditions on the network parameters under which the oscillators synchronize. Such conditions read as "the network connectivity dominates non-uniformity, losses and lack of phase cohesiveness" and are checked from the data alone, without simulation.
The paper gives two such sufficient conditions. This mission formalizes the second, Theorem V.5, which measures connectivity by the algebraic connectivity of the lossless coupling and therefore applies to sparse (connected, not necessarily complete) networks. A companion mission treats Theorem V.3, the condition for complete graphs.
Timeline. For the classical Kuramoto model, Jadbabaie, Motee and Barahona (ACC, 2004) and Chopra and Spong (IEEE TAC, 2009) analysed synchronization with the Lyapunov function , and Chopra and Spong proved frequency synchronization under cohesive phases. Dörfler and Bullo (2009–2012) extended the analysis to non-uniform time constants , phase shifts and non-complete graphs, using a weighted Lyapunov function.
There are oscillators with phases , time constants , natural frequencies , coupling weights and phase shifts (), with . The non-uniform Kuramoto model is
In this mission , and its non-zero entries induce a connected graph.
If , then
Lemma V.8 (the identity (36) that replaces by ), Lemma V.9 (a quadratic-form bound by ), the sinc estimate and the bound on the lossy coupling (p. 25), the Lyapunov-derivative bound (37), the sandwich bounds (39) on , the existence and uniqueness of from the analysis of (41), and the eventual entry of every trajectory into .
The condition is checkable from network data: of a weighted Laplacian, two vector norms and the extreme time constants. It applies to sparse networks, where the complete-graph condition of Theorem V.3 does not, and specializes for classical Kuramoto oscillators to (Remark V.7). Through the singular-perturbation argument of Section IV, conditions of this kind certify transient stability of the network-reduced power system.
The result is proved in the paper; no machine-checked version is known. A formalization fixes several points the printed text leaves loose: the norm is written on p. 23 with a double sum that counts each pair twice; the chain defining on p. 25 is printed with its inequalities reversed; and "reaches " holds only asymptotically. The formal statements make each of these precise.
The obvious Lyapunov function, , has a sign-indefinite derivative as soon as the differ, because the coupling is not symmetric. The weighted function restores a symmetric structure, but only through the non-obvious identity (36). After that, the sinusoidal coupling has to be bounded below by a quadratic form on a set where the phase differences stay below , the lossy coupling has to be bounded above uniformly in the state, and the resulting ultimate-boundedness argument has to be run with sublevel sets of , which are ellipsoids rather than balls of unless all coincide. The constants , , come from this mismatch, and the passage from sublevel sets back to balls is the most delicate step.
The prophet inequality of optimal stopping compares a gambler, who sees independent non-negative random values one at a time and must accept or reject each on arrival, with a prophet who sees them all in advance. Krengel, Sucheston and Garling showed that the gambler can secure , and Samuel-Cahn showed that a single threshold suffices. Since Hajiaghayi, Kleinberg and Sandholm (2007) and Chawla, Hartline, Malec and Sivan (2010), prophet inequalities have served as the approximation guarantees of sequential posted-price mechanisms: an online selection rule with a prophet guarantee turns into a truthful mechanism with a revenue guarantee.
The natural multi-choice generalization lets the gambler accept a set of elements, subject to a feasibility constraint. Kleinberg and Weinberg, Matroid Prophet Inequalities (STOC 2012, arXiv:1201.4764), proved that when the feasible sets are the independent sets of a matroid, the factor is still achievable, by an explicit threshold rule, and even when the order of arrival is chosen adaptively by an adversary.
Timeline:
Let be a finite ground set and a matroid; is its family of independent sets. For each a distribution on is given; the weights are independent with , and . Let and .
An online weight-adaptive adversary reveals the elements one at a time: it picks knowing but not . An online algorithm maintains a selected set and, when arrives with its weight, irrevocably accepts or rejects it, keeping independent. A threshold rule offers a threshold computed from the revealed prefix (and when ) and accepts iff .
The algorithm of the paper uses a ghost sample: an independent copy of the weights. Let be a -maximum-weight basis. For an independent set , among the partitions with and a basis, , denote one maximizing . The algorithm (9) sets
For every matroid on a finite ground set, every family of distributions on with finite means, and every online weight-adaptive adversary, the set selected by the algorithm (9) satisfies
The goal is stated for the paper's own algorithm, which is stronger than the existence statement of §3.
earns . 2. The identity behind (9) = (10), and the telescoping identity (Property (2) for ). 3. Lemma 1 (bijective basis exchange, and its weighted form), Lemma 2 ( is a maximum-weight basis of the contraction ), Lemma 3 ( is submodular on subsets of an independent set). 4. Inequalities (11) and (12), and Proposition 2:
pointwise in ; then Property (3) with for the thresholds (9).
The theorem gives the optimal constant: already for a rank-one matroid (choose one element) no online algorithm beats . It covers every matroid with one algorithm, including uniform, partition, graphic and transversal matroids, which model capacity, unit-demand and spanning-tree constraints. Through the reduction of Chawla et al., the paper derives from it order-oblivious posted-price mechanisms that are 2-approximations to the optimal revenue in single-parameter settings with matroid feasibility and, through the adaptive adversary, in multi-dimensional unit-demand settings (§6 of the paper). The decomposition through -balanced thresholds is reused in the paper for intersections of matroids, with factor .
The result has been proved since 2012; it has not been formalized. The mission produces a machine-checked development of the model (online adaptive adversaries, threshold rules, the ghost-sample expectations), of the general reduction (Proposition 1), and of the matroid facts the algorithm relies on, notably the bijective exchange lemma (Schrijver, Corollary 39.12a), which is not in Mathlib.
The obvious argument fixes the order of arrival and compares the algorithm with the prophet item by item. It fails here because the order is chosen adaptively from the revealed weights, so the set of elements still to come is random and correlated with the past. The proof must instead compare the algorithm's realized selection with a ghost optimum built from an independent sample, and bound the value the algorithm forgoes by the value the ghost optimum could still add, . The step that needs matroid structure is Property (3): the total threshold offered to any set that could still be added must be at most half of . The thresholds were computed along the history , not at the final , so the bound requires the submodularity of (Lemma 3) and a weight-dominating exchange between and in the contraction . Neither holds for general downward-closed families.
Fintype α; the matroid is Mathlib's Matroid α with ground set Set.univ; sets are Finset α; contraction is Matroid.contract.F : α → Measure ℝ, probability measures with F x (Set.Iio 0) = 0 (support in ) and Integrable id (F x) (finite means). The weight law is Measure.pi F, and every expectation is a Bochner integral over it. Finite means make , and the integrands of the thresholds integrable, so no expectation is a junk value.The goal fixes the thresholds by (9) through , and the ghost expectation; a statement in which the thresholds are free parameters assumed to satisfy (2)–(3) would be Proposition 1 and is not the goal.
Contributions are welcome at every level: the measurability of the online run, the exchange lemma for Mathlib matroids, the greedy characterization of maximum-weight bases of a contraction, and the probabilistic core (7) of Proposition 1. The matroid lemmas are reusable beyond this mission, in particular by the matroid-intersection mission of the same paper.
Random time changes occur when a process is observed on an operational clock rather than calendar time. In queueing models, for example, an arrival-count path may be evaluated at an evolving service clock. A functional limit theorem for the outer path and another for the clock are useful together only when evaluating one path at the times supplied by the other preserves convergence. Ward Whitt's 1980 paper studies several path operations with this question in mind; composition is its first main operation. The issue is specific to paths with jumps, because a small shift of the clock can move an evaluation across a jump.
Let be nonempty intervals of real time, with , and let be a complete separable metric space. The càdlàg path space consists of paths that are right continuous and have left limits on . Its subspace contains the continuous paths. The nondecreasing clock space consists of càdlàg real-valued paths on that are nondecreasing and take their values in . Its subspace contains the continuous, strictly increasing clocks. For and , composition is the path on .
Convergence uses the Skorohod topology. On a compact interval , let be the increasing homeomorphisms of and let . With denoting uniform distance, Whitt's metric is
Thus close paths may have nearby jumps at different times, provided an increasing time change aligns them. On a general interval, convergence is checked on compact subintervals whose endpoints are continuity points of the limit or endpoints of the full interval. Whitt gives this definition in §2, then gives , , and in §3. All subsets carry relative topologies and products carry product topologies.
For in and in , the first milestone states
The path-space definition and the two preparatory milestones are a small-oscillation partition for a càdlàg path, cited by Whitt from Billingsley, and Whitt's Lemma 2.2, which relates convergence on a compact interval to convergence on the two pieces made by splitting it at a continuity point.
The second case, and the combined goal, also allow the outer limit path to jump. Let mean the endpoints of that belong to . The corrected target is
The goal includes both cases for simultaneously varying and . The endpoint condition is vacuous for an endpoint excluded from . It is part of the strictly increasing clock case only; it imposes no extra restriction when the outer limit path is continuous.
This theorem supplies a precise condition for carrying two path limits through a random time transformation. In particular, the assertion includes convergence of the composed paths as elements of a càdlàg space, not merely convergence of their values at individual times. The distinction matters at jumps: pointwise convergence does not control the placement or ordering of nearby jumps. The result is a deterministic continuity statement that can be paired with probabilistic mapping theorems when the corresponding random paths are available.
Whitt proved the composition theorem in 1980, subject to the endpoint issue described below. The formalization work here is to construct its path-space interface in Lean, state the corrected continuity theorem with every domain condition visible, and eventually replace the open sorry proofs with checked proofs. The interface can also support the paper's later results on reflection, first passage, and time reversal; those results are separate missions. No proof of this mission's goal is claimed yet.
The tempting argument is to use separate continuity of and and then substitute into the first convergence. That argument loses control of evaluations near a jump of . A time change may align a jump of with the corresponding jump of , while the clock may cross those times differently. Continuity of the outer limit path removes that difficulty in one case; in the other, the clock must be continuous and strictly increasing. The source explicitly shows that composition is not continuous on all of (§3, p. 75).
The endpoints impose a further obstruction because increasing homeomorphisms of a closed time interval fix its endpoints. Bauer's Remark on p. 75 observes a failure at the right endpoint. There is a symmetric failure at the left endpoint, so the statement here includes both. This is a correction to the printed theorem, not a new claim that the uncorrected theorem is true.
Paths are represented as total functions , with only values on the named interval used. The domain assumptions OrdConnected and Nonempty express nonempty real intervals. The outer interval is also required to have nonempty interior: the formal convergence predicate checks only compact intervals with , so on a one-point it imposes nothing, and the case would fail for constant outer paths with different values. A clock's range condition is explicit, as is nondecreasingness for every prelimit clock. Membership of all paths in the relevant càdlàg spaces is part of the convergence predicates. The output predicate likewise requires every composition and its limit to be càdlàg. This rules out the trivialization in which one merely proves convergence of selected point evaluations or assumes the compositions already have the conclusion's path-space properties.
The compact uniform distance and the infimum over time changes take values in . They use the actual metric on , not a real supremum with a default value on an unbounded set. A time change is a total function whose restriction to the compact interval is continuous, strictly increasing, and onto. Continuity at a time means continuity relative to the path's interval. The general-interval convergence predicate checks the compact intervals specified by Whitt and requires each sequence member to belong to . The theorem is written as sequential continuity; Whitt's spaces are metrizable, making that equivalent to topological continuity. The real-valued clock space uses the relative topology inherited from real-valued càdlàg paths.
The endpoint correction is exact in the Lean statement. At the right endpoint, take , , for , and . Then is zero while . At the left endpoint, take , , , , and . The outer paths converge in on , but the compositions disagree at . Both examples show why continuity of at the image of every included endpoint is required in the case.
The development needs the càdlàg definition, metric and convergence predicates, compact restriction lemma, and the finite oscillation partition. Their definitions and lemmas are reusable for other functionals on path spaces. Contributions that prove the milestones and goal under the stated hypotheses are welcome. This mission does not formalize the Borel measurability or probability-measure machinery discussed elsewhere in Whitt's paper; Theorem 3.1 itself is a deterministic continuity claim.
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.
Random coordinate descent minimizes a smooth convex function by updating one coordinate at a time, chosen at random. Each iteration needs a single partial derivative instead of the full gradient, which is what makes the method usable on problems whose dimension is in the millions or billions ("huge-scale" problems). Nesterov's paper Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362, doi:10.1137/100802001) gave the first global efficiency estimates for such methods and started a large literature on randomized block and coordinate methods.
The basic method RCDM of the paper takes, along coordinate , a step of length , where is a Lipschitz constant of the -th partial derivative along the -th coordinate. For simple functions these constants are known; for more complicated ones they are not, and a practical method has to estimate them on the fly. Section 6.1 of the paper analyses a backtracking strategy with restore for this purpose and proves that it keeps the efficiency of RCDM up to a constant factor. This mission formalizes that analysis, Theorem 7 of the paper.
Write and for the -th standard basis vector of , . The function is convex and differentiable, attains its minimum , and its partial derivatives are coordinate-wise Lipschitz with constants ((2.2) with one-dimensional blocks):
The weighted norm and its dual are and ((2.7) with ), and
measures the size of the initial level set, being the set of minimizers.
The random adaptive coordinate descent method RACDM (6.1) keeps estimates , initialised with given lower bounds . At iteration it
The loop test uses only the sign of one partial derivative and never a function value. With (the expectation over ) and the number of partial derivatives computed in iterations , Theorem 7 states three facts about this method.
This is the rate of RCDM, ((2.14)), with a larger constant.
The result shows that the constants in RCDM need not be known: a method that starts from any lower bounds and adjusts them by doubling and halving converges at the same rate, and pays on average about two partial derivatives per iteration plus a logarithmic one-time overhead. This is what makes random coordinate descent applicable to functions whose coordinate smoothness is not available in closed form, and the doubling-with-restore pattern recurs in later adaptive and accelerated coordinate methods (the paper itself indicates the same technique for its accelerated method, (6.5)).
The theorem is proved in the paper; to our knowledge no machine-checked proof exists. The known-constant analogues for scalar coordinates are on Prove2Me in Bubeck's §6.4 development (the one-step and expected decreases are proved there; the rate is open). This mission adds a formal model of the adaptive method itself, including its doubling loop as a first-failure search, and the three statements of Theorem 7 on top of the published coordinate-descent definitions.
The analysis of RCDM rests on the one-step bound , which follows from the smoothness of along the coordinate line. For RACDM the step uses an estimate that may be smaller than , and then the same argument gives no decrease at all: a step that is too long can increase . The method never checks function values, so the decrease has to be extracted from the sign test alone, and it holds only because is convex along the line, not merely smooth. A second point is that the estimates are random and depend on the whole history, so the expected decrease must hold for every state the method can reach; this is what item 1 secures. The counting statement needs the exact number of loop iterations, so the loop has to be modelled as the least number of doublings after which the test fails, not as some number of doublings.
The formalization works with scalar coordinates (, as the paper does in §6.1) on EuclideanSpace ℝ (Fin n), coordinates indexed . It reuses the published definition ConvexOptAlg_CoordDescent_Defs: IsCoordSmooth f g L is (2.2) with an explicit gradient map , wnorm L 1 and wnormDual L 1 are and , and rcdExpect L 0 k is the expectation over uniform draws as a finite weighted sum. The mission's own definition NesterovRCD.Adaptive.RACDM encodes the trial point, the number of doublings (a minimum over ), one iteration, the run along an explicit sequence of draws, and the count .
The following choices are made explicitly.
A trivializing encoding is ruled out: the loop count is the least at which the sign test fails (an arbitrary admissible would change the method and make the count meaningless), the draws are uniform, and the rate is stated in the norm of the true constants , not of the estimates. Contributions welcome: proofs of the milestones, a one-dimensional co-coercivity lemma for convex smooth functions of one variable (reusable well beyond this mission), and the recursion argument from the expected decrease to the rate.
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.
Dynamic programming rests on time consistency: a control that is optimal when viewed from time stays optimal when viewed from any later time. Many problems of mathematical finance lack this property. The continuous-time mean–variance portfolio problem (Zhou–Li 2000) contains a variance, that is, a nonlinear function of an expectation, and state-dependent risk aversion (Björk–Murgoci–Zhou) lets the criterion itself depend on the current state. For such problems an optimal control computed today is abandoned tomorrow, and the HJB equation is not available.
One response, going back to the game-theoretic view of non-commitment (Ekeland–Lazrak, arXiv:math/0604264; Björk–Murgoci, SSRN 1694759), is to replace optimality by equilibrium: a control that no "future self" can improve by deviating on an infinitesimally short interval. Those works consider feedback (Markov) controls. Hu, Jin and Zhou (arXiv:1111.0818v1) define equilibrium within open-loop controls for a general stochastic linear–quadratic (LQ) problem with random coefficients, and characterize it by a flow of forward–backward SDEs, in the spirit of the stochastic maximum principle (Peng 1990). This mission formalizes that characterization: §2 and §3 of the paper, up to Theorem 3.2. The other two missions of the series build on it. Mission II treats a scalar state with deterministic coefficients (Theorem 4.4), and Mission III treats mean–variance portfolio selection (Theorem 5.4).
Let be a standard -dimensional Brownian motion on with its filtration , and let . A control is a process , that is, progressively measurable with . Its state solves the linear SDE
Here is a bounded deterministic matrix function. (), () and () are essentially bounded progressive processes, and . At time , with state and , the cost is
are bounded symmetric processes with , and are symmetric with . The last two terms make the problem time-inconsistent. Given with state , the spike variation at is for . The control is an equilibrium (Definition 2.1) if for every and every such , almost surely
For each , the first adjoint process solves on the BSDE (3.1) with driver and terminal value . The second adjoint process solves the matrix BSDE (3.2) with terminal value . With these, define
Suppose , its state , and for every a solution of (3.1) are given, and suppose satisfies condition (3.4):
Then is an equilibrium control.
Theorem 3.2 is the paper's general tool. Its two explicit results are applications of it. With a scalar state and deterministic coefficients, a pair of coupled Riccati-type equations gives a linear feedback equilibrium (Theorem 4.4). In mean–variance portfolio selection with state-dependent risk aversion and a possibly random risk premium, the equilibrium strategy is found through a quadratic BSDE (Theorem 5.4). Each is proved by exhibiting a solution of the flow (3.6) and checking (3.4). The theorem therefore separates the existence question (solving a flow of FBSDEs) from the equilibrium question. The paper notes that the general existence question remains open.
The results are proved in the paper and have no machine-checked proof. The mission produces a precise statement of open-loop equilibrium for a stochastic LQ problem with random coefficients, together with Lean statements of the spike expansion and of the adjoint flows. Mission II and Mission III restate the same model, and their final steps apply this theorem. Formal proofs of the milestones exercise Itô calculus for linear SDEs and BSDEs with bounded coefficients: product rules, conditional estimates, and uniqueness and sign properties of linear BSDEs. This is infrastructure that Mathlib does not yet have.
The obvious argument is a first-order expansion of in . It fails because the spike changes the control by , which is not small, on a set of small measure. The state's deviation is then of order in , its square contributes at order , and a second-order term appears that a first-order adjoint cannot capture. Two features are absent from the classical maximum principle. The adjoint equations form a whole flow indexed by , because the terminal value of (3.1) contains and . And every statement is conditional on , so the expansion has to hold almost surely at the level of conditional expectations. That rules out arguments based on unconditional expectations.
Brownian motion, , Itô integrals and SDE solutions come from the published definition Peng1990_SMP_Stochastic. The formalization commits to the following conventions.
The conclusion of the goal is Definition 2.1 itself. It mentions neither nor the adjoint processes, so the goal cannot be closed by unfolding. A definition of equilibrium in terms of (3.4) or (3.5) would make Theorem 3.2 trivially true and is ruled out. Condition (3.5) of p. 6 is not a hypothesis of any statement. A degenerate, noise-free example checks that the hypotheses of the goal can hold together.
Contributions are welcome as follows. Proofs of the three milestones are reusable for Missions II and III and for any spike-variation argument. So are general lemmas on linear SDEs and BSDEs over Peng's Itô integral: uniqueness, conditional moment bounds, the Itô product rule, and positivity of linear matrix BSDEs.
A differential variational inequality (DVI) couples an ordinary differential equation with a finite-dimensional variational inequality whose solution acts as an algebraic input to the dynamics. The class contains linear complementarity systems, mechanical systems with unilateral contact and friction, dynamic Nash games and many hybrid engineering models. Pang and Stewart's paper (Math. Program. 113 (2008); author's version hal-01366027v1) set up a unified theory of such systems: existence of solutions, uniqueness, and convergence of numerical time-stepping schemes.
The numerical question is the practical one. A DVI is solved by discretizing time and solving one finite-dimensional variational inequality per step. Whether the discrete trajectories approximate a true solution as the step size shrinks is not automatic: the algebraic variable can switch discontinuously, so the discrete 's need not converge pointwise. Section 7 of the paper answers this for a semi-implicit Euler scheme applied to the initial-value problem, and the answer is also an existence proof for the DVI.
Fix and write . Let be a nonempty closed convex set, let , , and . For , is the set of with for all . The initial-value DVI (6.2) is
The standing assumptions are (A): , and are Lipschitz continuous on (for the metric ), and (B): .
A weak solution is a pair with , integrable on with for almost every , the integral equation for , and the integral form of the VI,
The time-stepping scheme (7.2) uses a step , grid points , a parameter , and :
for . The iterates are turned into functions of time: is the continuous piecewise linear interpolant of the , and is the piecewise constant interpolant equal to on .
Suppose the iterates satisfy the uniform bounds (7.5),
for all small . Then along some ,
If moreover (a) with Lipschitz and (7.6), or (b) with positive semidefinite, then every such limit pair is a weak solution of (6.2).
The proof decomposes into the paper's own steps: Lemma 7.1 (the implicit Euler step is uniquely solvable, with the bounds (7.4)); the uniform step bound , which makes equicontinuous; the fact that a weak limit of -valued functions is -valued almost everywhere; the integral VI (7.7) under (a); the integral equation (7.8); and the weak lower semicontinuity (7.9) of for positive semidefinite , which handles (b).
Lemma 7.2 (a discrete Gronwall bound giving (7.5) from one-step growth conditions), Lemma 7.3 ((7.5) from linear growth of the VI solutions) and Proposition 7.1 (existence of the iterates for small ) are included as further targets: together with Theorem 7.1 they reduce the hypotheses on the iterates to conditions on .
Theorem 7.1 is simultaneously a convergence theorem for a practical numerical method and an existence theorem: any scheme with bounded iterates produces, in the limit, a weak solution of the DVI. Combined with Proposition 7.1 and Lemma 7.3 it yields existence for DVIs whose VI part has linearly growing solution sets, including linear complementarity systems with positive semidefinite , without the upper-semicontinuity machinery of differential inclusions. Case (b) covers monotone linear complementarity systems, the class arising in passive electrical networks and frictionless contact.
The results are proved in the paper. None of them is machine-checked. A formalization would produce a reusable Lean account of Euler polygons, equicontinuity estimates for discrete schemes, and weak limits of constrained sequences, all of which recur in the numerical analysis of nonsmooth dynamical systems.
The obvious argument would pass to the limit in each step of the scheme pointwise. This fails because has no pointwise or strong limit in general: only weak compactness is available. The nonlinear term does not commute with weak limits, so the variational inequality cannot be passed to the limit directly. Each of the two cases supplies the missing compactness or convexity: in (a) the bound (7.6) makes converge uniformly, and in (b) positive semidefiniteness makes the quadratic term weakly lower semicontinuous. Membership also does not follow from pointwise reasoning and needs convexity of .
Vectors are EuclideanSpace ℝ (Fin k), inner products are ⟪u, v⟫_ℝ, and matrices are continuous linear maps with the operator norm. is the published definition SolodovSvaiterVI.Alg21.viSol Φ K. Positive semidefinite matrices are not assumed symmetric.
Step sizes are with an integer , so that the grid ends exactly at . "For all " becomes "for all ", and "" becomes a strictly increasing sequence of 's. The iterates are a family indexed by and are hypotheses of the goal; their existence is the separate Proposition 7.1. Weak convergence in is tested against every function, and the uniform convergence of is on all of . Condition (7.6) is imposed for , because the paper's convention makes vacuous.
A weak solution carries integrability of both integrands as explicit conditions. Without them a non-integrable pair would satisfy the integral conditions vacuously, since a Lean integral of a non-integrable function is zero. The following readings are also excluded: convergence of the scheme only at grid points; a scheme in which solves the VI at instead of ; and a conclusion about one particular subsequence instead of every subsequence along which both limits exist.
A complete development needs: compactness in (Arzelà–Ascoli), weak sequential compactness of bounded sets in , Mazur's lemma on convex combinations, and estimates for piecewise linear and piecewise constant interpolants. The last two items are reusable for other time-stepping schemes. Proofs of any milestone, and of auxiliary interpolation lemmas, are welcome.
Out of scope: the weaker Carathéodory assumption (A′), the implicit scheme (7.3), the cited fixed-point theorems 7.2–7.3, and Theorem 7.4 (which combines Theorem 7.1 with the existence results of §6).
Quasi-Newton methods such as BFGS were designed for smooth objectives, yet in practice they are routinely and successfully applied to nonsmooth functions. Lewis and Overton (Math. Program. 141 (2013) 135–163) study why. A quasi-Newton step needs a step length along each search direction, and on a nonsmooth function the usual line searches have to decide what to do at points where the function is not differentiable. Classical inexact line searches for nonsmooth optimization (Lemaréchal 1981, Wolfe 1975, Mifflin 1977) ask an oracle for a subgradient at such points. Lewis and Overton propose a simpler rule: a trial point at which the objective is not differentiable simply fails the Wolfe test. This mission formalizes the analysis of that line search, §4 of the paper: when an acceptable step exists, when the bisection search finds one, what happens when it does not, and how many trials it takes on a convex function.
Let be an iterate of an optimization algorithm and a search direction. The line search objective is for . Only enters the analysis.
Assumption 4.1. The function is absolutely continuous on every bounded interval and bounded below, and
The number plays the role of the directional derivative .
Armijo and Wolfe conditions. Fix constants in . For ,
An Armijo–Wolfe step is a satisfying both.
Algorithm 4.6. Start from , , . At each trial: if fails, set ; otherwise, if fails, set ; otherwise stop. Then set if , and otherwise. So the search doubles until fails and then bisects the bracket . Write for the state before trial (lsRun), so . The search terminates if some trial passes both tests (Terminates).
Under Assumption 4.1 and :
Theorem 4.7 is the convergence guarantee for the line search used by the BFGS implementation analysed in the rest of the paper. It isolates the only failure mode: a derivative that oscillates as increases to a limit point, which condition (4.8) excludes. The paper notes that (4.8) holds for every semi-algebraic , so the search terminates on the functions met in practice. The same line search is the one whose trial sequence produces the binary-expansion behaviour of the secant method in §5. Theorem 4.5 shows that an acceptable step exists on a set of positive measure, which is why a sampling line search is not defeated by the null set of nondifferentiable points. Proposition 4.11 bounds the work per line search on convex functions.
All statements are proved in the paper. None has been formalized; there is no line search for nonsmooth functions on Prove2Me or in Mathlib. A formalization checks the measure-theoretic argument (absolute continuity and the fundamental theorem of calculus for Lebesgue integrals), the bookkeeping of the bisection, and the complexity count, where the printed upper bound turns out to be false for .
The obvious proof of termination fails: on a nonsmooth function the bisection can land on a kink at every trial, and the paper's §4.2 constructs a convex where it does. Termination therefore cannot follow from Assumption 4.1 alone, and both the existence of acceptable steps and the convergence of the brackets have to be argued through measure: Lemma 4.4 needs the fundamental theorem of calculus for absolutely continuous functions and a supremum argument over almost-everywhere inequalities. The non-termination analysis has to combine the bracket invariant with Lemma 4.4 on every late bracket and with a limit argument for (4.9). The complexity bound needs a careful count of doubling and bisection trials, including the regime where no doubling occurs.
The objective is h : ℝ → ℝ; only its values on enter. Lebesgue measure is volume with values in , and "nonzero measure" is volume S ≠ 0. Limits superior and inferior are computed in EReal. The upper bound is in WithTop ℝ, with . Stopping freezes the state of lsRun. Mathlib's deriv is at nondifferentiable points, so the Wolfe condition, condition (4.8) and (4.9) all state differentiability explicitly.
Deviations from the page, each disclosed in the item's Formalization Note:
Algorithm 4.6 is encoded as the literal state machine; a definition of the search as "some Armijo–Wolfe step" or as an arbitrary nested sequence of brackets would make the goal trivial and is ruled out. The Wolfe condition includes differentiability; without it every kink would pass, since .
A complete development needs absolute continuity (AbsolutelyContinuousOnInterval, with almost-everywhere differentiability and the fundamental theorem of calculus, both in Mathlib), the mean value theorem, and facts about one-sided derivatives of convex functions. Lemma 4.4 and the bracket invariant are reusable for other bracketing line searches. Contributions of the milestones in order, of proofs of the definitions' basic properties (all trial steps are positive, the brackets are monotone), and of the §4.2 non-termination example are welcome.
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.
Fourier analysis of functions on the discrete cube is the main tool behind tight inapproximability results under the Unique Games Conjecture. In the MAX-CUT reduction of Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 2007), soundness rests on the Majority Is Stablest theorem: among bounded functions in which no coordinate has large influence, the majority function is asymptotically the most noise stable. That theorem was a conjecture when the paper was written and was proved by Mossel, O'Donnell and Oleszkiewicz (Annals of Math. 2010) using an invariance principle.
Section 6.2 of the paper records special cases of Majority Is Stablest that have short, self-contained proofs. Theorem 6 is the case where the noise parameter tends to . There the noise stability is dominated by the Fourier weight at level 1, and the statement says that a bounded function with small influences has level-one weight at most , up to an explicit error linear in the largest influence. Bounds on the level-one weight also appear in Talagrand's work on correlation of monotone sets (Combinatorica 1996), which the paper compares against (its Theorem 18), and the level-one inequality is a standard chapter of the analysis of Boolean functions (O'Donnell 2014).
Points of the discrete cube are sign vectors ; following the paper, the bit TRUE is read as and FALSE as . The cube carries the uniform probability measure, so , and real functions form an inner product space with .
For the parity ; the parities form an orthonormal basis, and the Fourier coefficient of at is . The weight of at level 1 is
The influence of coordinate on (Definition 2) is
the expected variance of when all coordinates but are fixed at random and is a uniform sign. The linear part of is , and , , .
Throughout, .
For every , every and every with for all ,
The constant is explicit, and the goal states it exactly as printed.
The result. The constant is sharp: majority on variables has influences of order and level-one weight tending to , which is for a standard Gaussian . Theorem 6 thus identifies the extremal level-one weight of low-influence bounded functions and gives a rate linear in the maximal influence. It is the instance of Majority Is Stablest, obtained without the invariance principle, and level-one bounds of this type are used in hardness reductions and in the study of noise sensitivity.
Formalizing it. The milestones together give a complete formal route from bounded functions to the stated bound, except for one step discussed below. They also produce a reusable layer of Boolean Fourier analysis: Fourier coefficients, level weights, influences in their variance form and the Fourier formula for influences. Mathlib contains no development of influences or level weights on the cube, and the platform has none either; the König–Schütt–Tomczak-Jaegermann inequality, a sharp quantitative central limit bound for Rademacher sums (J. Reine Angew. Math. 1999), has no machine-checked proof.
Status. The published proof's first step, , is valid for Boolean-valued but not for -valued ; for -valued the statement is posed as printed. For with one has , and the argument as written then yields only . Numerical search over small cubes has found no function violating the printed bound. A proof of the goal for bounded , or a counterexample, is therefore a genuine contribution.
The obvious argument replaces by a Gaussian with the same variance and uses . A central limit theorem with an error term is needed, and generic Berry–Esseen bounds give an additive error with a constant far from ; the exact constant requires the sharp Rademacher-sum inequality, whose proof is a delicate analysis of as a function of the coefficients. The second obstacle is the passage from influences to coefficients. For bounded only holds, so a bound on influences controls coefficients only at scale ; feeding that into the chain loses the linear dependence on . Recovering the printed rate for non-Boolean needs an idea beyond the published proof.
A point of the cube is Fin n → Bool, mapped to a sign by pm with pm true = -1 and pm false = 1. Expectations are normalised finite sums, so no measure theory is involved. A function is a real function with the hypothesis ∀ x, |f x| ≤ 1. The influence is defined as on the page, as the average over the cube of , which is the variance in ; it is not defined by its Fourier formula, which is a milestone. The level-one weight is . The constant is written out as 2 * (1 - Real.sqrt (2 / Real.pi)); an existentially quantified constant would be a weaker theorem. The case is allowed.
Two hypotheses are added and disclosed: in Theorem 6 and in the König–Schütt–Tomczak-Jaegermann bound. For each follows from the other hypotheses; for the influence (resp. coefficient) hypothesis is empty and is what the page assumes.
A trivializing formalization would drop the range hypothesis (then scaled dictators refute the bound and the statement is false), define influence through Fourier coefficients (which makes Proposition 7.2 definitional), or weaken the hypothesis of the goal to a bound on the coefficients ; none of these is used here. In particular, the goal is not strengthened to Boolean-valued , where the published proof applies verbatim.
Contributions welcome: proofs of Parseval-type identities for the linear part, of Proposition 7.2, of the elementary quadratic step, of the König–Schütt–Tomczak-Jaegermann inequality, and of the goal itself. The cube layer is reusable for any later formalization of Boolean function analysis.
A differential variational inequality (DVI) couples an ordinary differential equation for a state with a finite-dimensional variational inequality that the algebraic variable must solve at every instant. The class contains complementarity systems from contact mechanics and electrical circuits with diodes, linear complementarity systems from control theory, differential Nash games, and the first-order optimality conditions of optimal control problems with inequality constraints. J.-S. Pang and D. E. Stewart introduced the unified framework in Differential variational inequalities, Math. Program. 113 (2008) (author's version, hal-01366027), and Section 6 of that paper settles the first question any such model raises: when does the initial-value problem have a solution on a whole prescribed time interval?
Before this work, existence results for these systems were tied to special structure: linear complementarity systems with "minimal" and "passive" data, or a given initial condition compatible with the complementarity kernel. Theorem 6.1 gives existence for every initial state under five separate conditions on the variational inequality, each describing a different class of DVIs.
Fix and write . For a set and a map , the variational inequality asks for with for all ; its solution set is . The initial-value DVI studied here is
with nonempty, closed and convex, , , and . Two standing assumptions hold throughout: (A) , , are Lipschitz continuous on ; (B) is bounded on in operator norm.
A pair is a weak solution (in the sense of Carathéodory) on if ; is integrable on with almost everywhere; for , with an integrable integrand; and for every continuous ,
with an integrable integrand. The existence proof passes through the differential inclusion with the set-valued right-hand side
Further objects: the recession cone ; the dual cone ; the VI kernel , the solution set of ; an R₀ pair , one with ; a psd-plus matrix , one with for all and ; and the linear growth property
Under (A) and (B), if any one of the following holds, then (6.2) has a weak solution on for every :
Theorem 6.1 is the existence result behind the rest of the paper: Sections 7 and 8 prove that time-stepping schemes converge to weak solutions of (6.2), and those results are informative only for problems that have solutions. Condition (d) gives existence for every initial state of linear complementarity systems , with , where earlier results required passivity or a compatible initial state. Propositions 6.2–6.5 are results on static variational inequalities in their own right: the linear growth of solution sets in the data had not been a focus of VI theory.
The result is proved in the paper, modulo two cited theorems (Deimling's existence theorem for convex-valued differential inclusions and Filippov's measurable selection lemma). None of it is formalized. A Lean development would supply set-valued upper semicontinuity, Carathéodory solutions of differential inclusions, and existence and linear growth theory for VIs on closed convex and polyhedral sets: material with uses well beyond this paper.
The obvious route, solving the VI for as a function of and substituting into the ODE, fails: the solution map is in general set-valued and discontinuous, so the resulting right-hand side is neither single-valued nor continuous, and classical ODE existence does not apply. The detour through the differential inclusion (6.4) requires convex values, which hold when is monotone but must be proved separately in case (e), where is not monotone. It also requires linear growth (6.5), which for unbounded is a genuine statement about the asymptotics of VI solutions and needs a different argument under each of the five conditions: coercivity, a recession-cone condition, the VI kernel, or a fixed-point argument on polyhedra. Finally, Deimling's theorem and Filippov's lemma are substantial results of set-valued analysis that are not in Mathlib.
Points of are EuclideanSpace ℝ (Fin k); matrices are continuous linear maps, is the operator norm and the adjoint. Data on are curried functions on of which only the values on matter, and Lipschitz continuity on uses the metric . is the published definition SolodovSvaiterVI.Alg21.viSol Φ K. Positive semidefinite matrices are not assumed symmetric. "Monotone" in (a) and Proposition 6.2 means monotone on . The coercivity (6.6) is written in the equivalent form " for with ". Upper semicontinuity is the open-neighbourhood form relative to . In Proposition 6.4 (b) the Lipschitz property is stated on the dual cone , where the paper's proof establishes it (the statement prints ). Nonemptiness of , the paper's standing assumption on variational inequalities, is a hypothesis throughout.
The weak-solution definitions carry explicit integrability conditions on the integrands of the integral equation and of (2.4), and (2.4) is required for every continuous with values in . A definition without those integrability conditions (a Lean integral of a non-integrable function is zero), a variational condition tested only on constant , or (A)–(B) replaced by global boundedness of and would make the goal a different and weaker statement; none of these is used.
Contributions welcome at every level: proofs of the milestones, a general theory of upper semicontinuous set-valued maps and Carathéodory solutions of differential inclusions, and existence results for variational inequalities via recession cones and degree theory.
A spectral sparsifier of a weighted graph is a graph on the same vertices, with few edges, whose Laplacian quadratic form is within a factor of that of on every vector. Spielman and Teng introduced the notion in their work on nearly-linear-time solvers for symmetric diagonally dominant linear systems (Spielman–Teng 2004; arXiv:0808.4134): a sparsifier can replace a dense graph as a preconditioner, and it preserves every cut value up to the same factor, strengthening the cut sparsifiers of Benczúr and Karger (BK96).
Their construction first handles graphs whose edge weights lie in a bounded range. Arbitrary weights need an extra idea, which §10.2 of Spectral Sparsification of Graphs formalizes as Lemma 10.2 (Pullback): when a graph's vertex classes are held together by edges far heavier than those between them, one may contract each class to a single vertex, sparsify the much smaller contracted graph, and pull the result back to the original vertices. The approximation factor degrades only by , where measures the gap between heavy and light weights. The same contraction idea goes back to Benczúr and Karger's treatment of weighted cut sparsifiers.
A weighted graph on a finite set , , is a symmetric function with ; its edges are the pairs with . Its Laplacian quadratic form is
A graph is a -approximation of if for all . We write when for all , for the graph whose weights are the sums, and for the single edge of weight .
Let be a partition of with map . Write for the edges between different parts, , and , . The contraction of under is the graph on with weight for and no self-loops. Given a graph on , a graph on is a pullback of under if every edge of joins different parts, is the contraction of , and for every edge of exactly one edge of has , . A pullback thus has as many edges as .
Let , , let be a -approximation of the contraction of under , and let be a pullback of . Assume (1) each is connected by edges in , (2) every edge in has weight at least , (3) every edge in has weight . Then
Choose representatives ; let , be the copies of , on , and , .
The constants are the paper's; the goal is the lemma as printed.
Lemma 10.2 is the reduction from arbitrary weights to bounded weights in Spielman and Teng's sparsification algorithm (Sparsify, §10.2): the edges of each weight scale are sparsified on a graph in which all much heavier edges have been contracted, so the number of vertices handled at each scale stays small, and the total size of the sparsifier is only a logarithmic factor larger than in the bounded-weight case. The statement itself is purely about quadratic forms and holds for any approximation of the contraction, however it was obtained; it applies equally to later sparsification methods such as sampling by effective resistances.
The lemma is proved in the paper. As far as is known, none of these statements has a machine-checked proof: Mathlib has the Laplacian of a simple graph (SimpleGraph.lapMatrix) but no weighted Laplacian order, no contraction of weighted graphs and no notion of spectral approximation. The mission produces those objects and a complete formal proof of the lemma and its intermediate claims.
The individual steps are elementary, but the proof combines three kinds of bookkeeping. Lemma 10.3 is a Cauchy–Schwarz inequality along a path, which must be applied to a path assembled from two walks inside parts and one edge between representatives; obtaining a simple path of length at most from the connectivity hypothesis requires shortening walks. The summed bounds require recognising that the copies of the unit edges between representatives add up exactly to , which uses hypothesis 3 and the fact that contraction counts each edge between two parts once. Claim (c) needs, in addition, that the total weight of is at most times that of and that each pullback edge has the weight of its image edge. The constants are tight in one place: requires both and .
A natural shortcut, comparing with directly, fails: and have different edges, and their Laplacians are only comparable through the heavy intra-part edges.
A weighted graph is a function w : V → V → ℝ on a Fintype V with IsWGraph w (symmetric, nonnegative, zero diagonal); sums and scalar multiples are pointwise. lapForm w x is , IsApprox σ w̃ w keeps both inequalities of the definition, and GraphLE is . The partition is a surjective map π : V → Fin k (nonempty parts). , are crossPart w π, intraPart w π; hypothesis 1 is reachability, between any two vertices of the same part, in the simple graph of -edges. Representatives are any r : Fin k → V with π (r i) = i, and liftAlong r z places a graph on Fin k on them; the goal does not mention representatives. is Fintype.card V.
Two hypotheses implicit in the paper are explicit: (with the lemma is false), and that every edge of a pullback joins two different parts (contraction cannot see an edge inside a part, so without this a pullback could carry an arbitrary heavy edge and the lemma would be false). In Lemma 10.3 the edge weights are positive and the path has at least one edge.
A trivializing formalization is ruled out: dropping hypothesis 2 or 3, allowing or intra-part pullback edges, or letting the pullback forget the uniqueness of the edge over each makes the statement false or weaker, and stating only one of the two inequalities of -approximation is a different theorem. Every statement here keeps both.
The algorithm Sparsify and its analysis (Lemma 10.4, Theorem 10.5, Proposition 10.6, Theorem 10.7, Lemmas 10.8–10.9) and all running-time claims are out of scope. The weighted Laplacian form, its additivity and nonnegativity, and the transport of a quadratic form along an injective vertex map are reusable beyond this mission; contributions of such general lemmas, and a proof of Lemma 10.3 by Cauchy–Schwarz, are welcome.
A manufacturer must commit to production before its retail customer knows what the market will demand, while the customer would rather postpone its purchase until better information arrives. Left uncoordinated, each firm protects itself: the customer inflates forecasts it is not bound by, and the manufacturer, discounting those forecasts, builds less than the supply chain as a whole should. Quantity flexibility (QF) contracts, used in practice in the electronics and computer industries (Sun Microsystems, Solectron, Nippon Otis and others are cited in the paper), address this by tying the customer's forecast to a band: the manufacturer guarantees supply up to a percentage above the forecast, and the customer promises to buy at least a percentage below it.
Tsay (1999) gives a two-stage model of such a contract with a demand signal that arrives between production and purchase, shows that a supply chain without commitment underproduces, and characterizes when a QF contract restores efficiency. This mission formalizes the efficiency result for the case in which the signal predicts demand perfectly (Proposition 6(a)), together with the steps of the equilibrium that it rests on.
A manufacturer (EM) produces at unit cost and sells to a retailer at unit transfer price ; the retailer sells at price , unsold units are salvaged at at either site, and each unit of unmet demand costs a goodwill loss . The standing assumptions are , and .
Before production, the retailer states a forecast . A QF contract with and obliges the EM to make up to available and the retailer to buy at least . The EM then builds . A demand signal with distribution function is observed, the retailer buys , and market demand is filled from the retailer's stock. In this mission the signal is perfect (): market demand equals , so its distribution equals .
Given , the retailer's profit from buying is
and it buys , the point of the interval closest to . The EM's expected profit (2) is . The retailer's forecast problem maximizes with the EM building . A central planner earns , maximized at
The total flexibility of the contract is .
With , the QF contract with flexibility and transfer price
is system-efficient: the retailer's unique optimal forecast is , the EM's unique optimal production given is , and the resulting expected system profit equals .
The result shows that one contract form, by choosing the transfer price as a function of the flexibility, yields a whole menu of contracts each of which coordinates the supply chain, so that the two firms can trade price against flexibility without losing system profit. Its corollaries in the paper, that any split of expected profit is achievable by some efficient contract and that more flexibility shifts profit to the manufacturer, rest on (4).
The paper prints no proofs ("All proofs are omitted due to space limitations", p. 1341). A machine-checked development supplies them, makes explicit the regularity the argument needs (finite variance, a continuous and strictly increasing , a positive efficient quantity), and gives reusable statements about newsvendor objectives with a clipped purchase. To our knowledge none of these results has been formalized before; the platform's quantity-flexibility theorems in other models (no manufacturer production stage, , retailer side only) do not cover them.
Each firm optimizes its own objective, and the efficient price must work for both at once. Making the retailer's first-order condition hold at pins down , so nothing is left to adjust for the EM, whose incentive to build more than the contracted has to be ruled out separately at that same price. The retailer's objective is an expectation of a non-smooth function of a clipped purchase, so its derivative must be computed through the distribution of on two moving thresholds and , and strict concavity must come from the strict increase of rather than from a density.
All objects live in the namespace TsayQF.EffQF. The law of is a probability measure on with , whose distribution function cdf ν is differentiable and strictly increasing on (the paper's "differentiable and invertible"). Expectations are Bochner integrals; finite variance makes every integrand integrable. Inverse distribution functions are not used: enters as a real number with the hypothesis , which determines it uniquely, and (4) is defined in its printed shape. Optimality is IsMaxOn over the decision's natural set: forecasts in , the EM's production in , purchases in , central production in .
Hypotheses made explicit: in the goal and a positive marginal value of the forecast at in Proposition 3(a), both standing for the paper's presumption that demand is almost certainly nonnegative; (Proposition 3's case). The transfer price is only required to satisfy rather than , because can exceed when . The milestones are the instances of the paper's general statements.
Two modelling choices are fixed. The retailer's forecast objective takes the EM's production to be , as §6.1 does after Proposition 2; the full game in which the retailer anticipates other EM responses is not modelled, and the goal instead verifies that the EM's unique best response at is exactly . The efficient price is the explicit formula (4), not "a price that makes optimal", which would make the goal a tautology; likewise system efficiency is stated as an inequality against at every production level, not by definition.
Needed infrastructure: derivatives of expectations of piecewise-linear functions of a clipped variable, and the newsvendor fractile characterization. Both are reusable for other contract models. Proofs of any milestone, and of the goal from the milestones, are welcome.