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.
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?
In many production and service settings a single resource is shared by several parties, each judging the outcome only by how its own work is treated. Multi-agent scheduling studies this situation. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) introduced the two-agent single-machine model in which two agents, A and B, each own a set of jobs and each minimize their own objective. Their paper treats two questions: the constrained problem, minimizing A's objective subject to a bound on B's, and the Pareto problem, describing every schedule that cannot be improved for one agent without hurting the other.
For the Pareto problem the first quantity of interest is the number of distinct trade-offs, because the natural way to compute the whole front is to solve the constrained problem repeatedly with a decreasing bound (the paper's scheme PP, Figure 4, p. 239). Enumeration of this kind is polynomial exactly when the number of nondominated pairs is polynomially bounded. This mission formalizes the paper's bound for the case where both agents minimize a maximum of regular cost functions (§11.1, pp. 239–240).
Agent A owns the jobs and agent B owns , with . Every job has a processing time . All jobs are available at time . A schedule is an ordering of all jobs; the machine processes them in that order from time without idle time, so the completion time of a job is the sum of the processing times of the jobs up to and including it.
Each A-job carries a cost function and each B-job a cost function , all nondecreasing (regular). The agents' objectives are the maximum costs
This covers the makespan and maximum lateness of each agent as special cases.
A schedule is nondominated if no schedule satisfies and with at least one inequality strict. The pair of a nondominated schedule is a nondominated pair, and the schedule corresponds to that pair. Write for the set of nondominated pairs. Different nondominated schedules can share a pair; the problem asks for , with one schedule per pair. Job precedes job in if comes before in the ordering.
The paper prints the bound . It is off by one: with , unit processing times and , the schedules AB and BA give the two nondominated pairs and . The goal states , the bound the printed argument supports once the first schedule is counted.
The bound places among the two-agent problems whose Pareto front has polynomially many points. Combined with the polynomial algorithm for the constrained problem (Theorem 4.1 of the same paper), it means the full front can be listed with polynomially many constrained solves. The structural content is an order statement: as the bound on agent B tightens along the front, B-jobs overtake A-jobs and never fall back, so each of the (A-job, B-job) pairs changes order at most once. The same question for other pairs of objectives is the subject of later work on multi-agent scheduling, collected in the monograph of Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal (Springer 2014).
The result is published but, to our knowledge, has no machine-checked proof. Formalizing it also fixes the printed off-by-one error in the statement. The overtaking lemmas are of independent use for other pairs of regular min-max objectives.
The obvious argument walks along the front and charges each step to one (A-job, B-job) pair that changes order. Two things must be secured. First, the charged pair must change order in a consistent direction; schedules corresponding to a pair are not unique, and nothing forces two arbitrary representatives of different pairs to agree on the order of the jobs they do not charge. Lemma 11.2 asserts that representatives can be chosen so that no B-job falls back behind an A-job, and establishing it requires control over every job pair simultaneously, not one at a time as in Lemma 11.1. Second, a step must change at least one order. The tempting proof looks at a B-job attaining and argues that the jobs it overtakes include an A-job; this fails for an arbitrary choice of that B-job, since another B-job with a flatter cost function can be the one that moves. Finally, the count of reversals bounds the number of steps, not the number of pairs; the first pair has to be added.
Jobs are Fin nA ⊕ Fin nB (Sum.inl h is , Sum.inr k is , 0-based). A schedule is a duplicate-free list containing every job, and completion times are prefix sums of processing times; this is the published sequence model MooreLateJobs.Shared.completionTime (Moore 1968), reused as a reference item. Processing times are real and nonnegative; costs are real-valued and Monotone; so that both maxima exist. Nondominance compares against all schedules of all jobs. Precedence compares first positions in the list.
The count is over pairs, , measured with Set.encard, so finiteness is part of the goal. Counting nondominated schedules instead would be a different and false statement: permuting jobs inside a block often leaves both maxima unchanged. The printed bound is replaced by and the reason is given in the goal's statement; stating a larger bound "to be safe" or the printed one would make the mission either weaker than the paper's argument or false. The scheme PP and the choice of in it are not formalized; they are the paper's computation device, not part of the theorem. In the exchange claim the paper's σ and σ̃ are schedules of consecutive pairs; the milestone states it for any two nondominated schedules with the two strict inequalities, which includes that case. Running times are not formalized.
A complete development needs elementary facts about completion times when one job is moved within a sequence, the simultaneous statement of Lemma 11.2, and a counting argument along the front. Contributions of reusable lemmas about job moves in the sequence model are welcome.
A probability distribution on the real line is self-decomposable (of class L) if its characteristic function satisfies for every , with again a characteristic function. Equivalently, a random variable can be written as with a copy of independent of . Class L consists exactly of the limit laws of normalized sums of independent summands, and its members are infinitely divisible, absolutely continuous (when nondegenerate) and unimodal.
None of this transfers to counting variables: apart from , no random variable on satisfies , because leaves the lattice. Steutel and van Harn (Memorandum COSOR 78-07, 1978; Ann. Probab. 7 (1979) 893–899) replaced scalar multiplication by binomial thinning, which keeps the variable integer valued. The resulting notion of discrete self-decomposability later became the basis of integer-valued autoregressive (INAR) time-series models (Al-Osh and Alzaid, 1987).
Timeline:
A distribution on is a sequence with ; its probability generating function (p.g.f.) is . The generating function of a sequence is written .
The -thinning of a variable with p.g.f. is with independent Bernoulli() variables ; its p.g.f. is . A distribution with p.g.f. is discrete self-decomposable (Definition 2.1) if for every
with a p.g.f.; in variables, .
A distribution is infinitely divisible if for every its p.g.f. is the -th power of a p.g.f. When , its canonical sequence is the unique solution of
Throughout §2 the paper assumes .
For a distribution with :
for some and some p.g.f. of a distribution with , the pair being unique; and
Theorem 2.2 reduces discrete self-decomposability, a condition quantified over all and over unknown factors , to a single monotonicity condition on the sequence computed recursively from . It is the entry point of the rest of the paper: combined with Theorem 2.3 it gives unimodality of every discrete self-decomposable distribution (Corollary 2.4), and §3 shows that discrete stable distributions are discrete self-decomposable. In time-series modelling it identifies the marginals that a stationary INAR(1) process can have for every .
The result has been proved since 1979; to our knowledge none of it is formalized in any proof assistant, and Mathlib has neither probability generating functions on nor infinite divisibility. The mission produces a machine-checked version of the canonical form together with the compound-Poisson characterization of infinite divisibility on (Lemma 1.2), which the paper only cites.
The forward direction is not a consequence of (2.1) for any single : one factorization constrains very little, and the information sits in the whole family of factors , , which are not given explicitly. Turning that family into a statement about needs a passage to a limit of p.g.f.'s, and the fact that such a limit is again a p.g.f. (the continuity theorem for p.g.f.'s, Feller vol. 1, p. 280) is not in Mathlib. The paper does not prove Lemma 1.2 either; it cites Feller and Steutel. For the converse, nonnegativity of the canonical sequence is not enough: the obvious attempt to show that has nonnegative coefficients fails for infinitely divisible in general, and the monotonicity of is exactly what is needed. Finally, every identity is stated between real functions on , and passing to identities between coefficients requires the uniqueness of power-series coefficients on a real interval.
p : ℕ → ℝ with ∀ n, 0 ≤ p n and HasSum p 1; the p.g.f. is the real function pgf p z = ∑' n, p n * z ^ n. All identities between p.g.f.'s are required for real (or for (1.4), (2.4), (2.6), (2.7)), not for complex ; p.g.f.'s agreeing on have equal coefficients, so this is equivalent. is Lean's deriv of pgf p.Reusable beyond this mission: the p.g.f. and infinite-divisibility vocabulary, Lemma 1.2 (compound Poisson characterization), and Lemma 1.1. A continuity theorem for p.g.f.'s on , and the uniqueness of power-series coefficients from values on , are welcome as independent contributions.
Firms that change prices over time face customers who remember past prices. A large empirical literature in marketing documents reference price effects: demand depends not only on the current price but on how that price compares with a price the customer expects, and losses (prices above the reference) weigh more than gains of the same size, the loss aversion of prospect theory (Tversky and Kahneman 1991; Kalyanaram and Winer 1995). Most dynamic pricing models with reference effects form the reference price by exponential smoothing of past prices (Popescu and Wu 2007; Kopalle, Rao and Assunção 1996; Fibich, Gavious and Lowengart 2003).
Psychology suggests a different memory process. Under the peak-end rule (Kahneman et al. 1993), people evaluate a past sequence of experiences mainly by its most extreme and its most recent episode. Nasiry and Popescu (INSEAD Working Paper 2009/20/DS/TOM; published in Operations Research 59(6), 2011) build a dynamic pricing model in which the reference price is a weighted average of the lowest price seen so far and the last price, and characterize the firm's optimal long-run and transient pricing. This mission formalizes the core of that analysis: the steady states (Section 3.1) and the convergence of optimal price paths (Section 3.2).
A firm sets a price in the price set in every period . The base demand is non-negative, bounded, continuous and decreasing on , with , and the base profit is non-monotone and strictly concave (Assumption 1). With sensitivities to surcharges and discounts, demand at price and reference price is
and the short-term profit is . It equals of the two smooth profits .
Given an initial minimum price and last price , the minimum price evolves as and the peak-end reference price is
With discount factor , the firm's value function is
An optimal price path is a price sequence in attaining ; a steady state is a state , , from which the constant path is optimal.
Two thresholds organize the answer. Let and be the roots in of
so that , and let , , . For , let be the root of
For every initial state with in , an optimal price path exists, and every optimal price path is monotone and converges:
The limit depends only on the initial minimum price.
In attack order: monotonicity of (Lemma 1); the identity and supermodularity of (Lemma 2); the upper bounds by smooth problems with one-dimensional state (Lemma 3); the unique steady state of each smooth problem (Lemma 4); two families of steady states (Lemma 5); the full set of steady states
(Proposition 1); Claims 1–4 and the invariance of the regions (Proposition 2: when , and when ); and Claim 5 (for the price eventually falls to or below).
The result gives a complete description of optimal pricing under peak-end anchoring with loss-averse consumers. A continuum of steady states exists, and the one reached is set by the remembered minimum price alone. A firm facing a low minimum price raises prices toward ; with an intermediate minimum it settles exactly at that minimum; with a high minimum it cuts prices down to and then holds them there. Optimal paths are monotone, so the model predicts no cyclical discounting under loss aversion. The comparison with Popescu and Wu (2007) in Section 3.3 of the paper and the robustness results of later sections (heterogeneous markets, non-linear reference effects) build on these statements.
The paper's results are proved on paper; none is formalized. The mission produces a machine-checked model of a non-smooth, two-dimensional dynamic program defined directly as a supremum over price sequences, the reduction of its steady states to smooth one-dimensional bounds, and the convergence theorem.
Both the per-period profit (through the kink at ) and the state transition (through ) are non-smooth, so neither the Euler equation nor standard concavity arguments for the value function apply directly. The Bellman objective need not be concave in the price, and the value function is not differentiable on the diagonal . Supermodularity of yields monotone optimal policies only within a region where the minimum price stays fixed, and showing that the state never leaves its initial region (Proposition 2) is itself a comparison of optimal paths against steady states. Existence of an optimal path is needed in its own right, because the value function is a supremum over an infinite-dimensional set.
All declarations live in PeakEndPricing.Convergence. Conventions fixed in Lean:
minPrice m0 q n is and refPrice at index is the reference price faced by .tsums, never "a solution of the Bellman equation". On the domain of the theorems all series converge and the families are bounded, so the junk values of ⨆ and ∑' are not reached.A goal stated without the existence of an optimal path would hold vacuously if no path attained ; existence is therefore part of the goal. Contributions are welcome on general infrastructure that is reusable beyond this mission: existence of optimal paths for discounted problems over compact action sets, the principle of optimality for sequence formulations, and Topkis-type monotonicity of optimal paths for supermodular objectives.
Multivariate multipoint evaluation asks for the values of one polynomial at points of . Kedlaya and Umans showed that this problem is equivalent to modular composition, the computation of for univariate polynomials, and that fast algorithms for it yield the fastest known algorithms for factoring univariate polynomials over finite fields (Kedlaya–Umans, Dagstuhl Seminar Proceedings 08381, 2008; journal version SIAM J. Comput. 40(6), 2011, doi:10.1137/08073408X). Modular composition is the bottleneck of the factoring algorithms of von zur Gathen and Shoup (1992) and Kaltofen and Shoup (1998), so a near-linear multipoint evaluation algorithm translates directly into a faster factoring algorithm.
The paper gives two such algorithms. Section 4 works over any ring and is not algebraic: it lifts the problem to the integers and reduces modulo many small primes. Section 6, the subject of this mission, gives an algebraic algorithm, using only ring operations, for fields of small characteristic. Its correctness rests on one identity, Lemma 6.1, which lets the evaluation of the -variate at a point be read off from the evaluation of a single univariate polynomial at a related point of an extension ring.
Let be a prime and a finite field of characteristic . Fix integers and . Let be a power of with (the paper takes the least such power), and let be a polynomial of degree that is irreducible over . Then:
Three maps connect the problem to :
In the Lean development these are K, R, h, ι (the inclusion ), sigma i (), E, S, sigmaInv i ( on ), gAlpha, phi, pi, gIter () and fStar, in the namespace KedlayaUmans.FrobeniusLift.
For every with degree at most in each variable and every ,
The result. Lemma 6.1 is the correctness half of Theorem 6.2: to evaluate at points one computes the lifts , evaluates the one univariate polynomial at all of them by fast univariate multipoint evaluation, and projects back with . Since univariate multipoint evaluation runs in nearly linear time, the identity turns a multivariate problem into a univariate one at the cost of the degree growth . Corollary 6.3 turns this into an operation count of for every , provided and the characteristic satisfies .
Formalizing it. The lemma is proved in the paper; no machine-checked version is known to exist. This mission states it for the objects exactly as constructed in Section 6 (an explicit interpolant for , the canonical-representative projection for ) and splits its proof into the five steps above. The definitions of the rings and , the Frobenius powers on a ring that is not a field, and the Kronecker substitution into a quotient ring are reusable for formalizing other uses of the Frobenius-lift technique, such as the Parvaresh–Vardy codes and their Guruswami–Rudra instantiation, which the paper names as the inspiration for this algorithm (§1.5, p. 6).
The obvious attempt is to treat as evaluation at and push it through . This fails: is a unit, not zero, so evaluation at does not factor through , and is not a ring homomorphism. The identity holds only because the polynomial is already reduced modulo , which requires both the degree bound and the fact that raising to the power does not raise the degree of modulo . The second fact depends on being fixed by and on . The equality further needs that does not kill the leading coefficient in , a ring with possible zero divisors. Finally, interpolation must happen in , not a field, which is possible only because the nodes lie in the subfield .
F with [Field F] [Fintype F] [CharP F p], a prime ([Fact p.Prime]). is a polynomial over ZMod p with [Fact (Irreducible P)]; is P.natDegree and is p ^ P.natDegree. is AdjoinRoot of mapped to F; is never assumed to be a field and is never assumed irreducible over F.m ^ 2 * d < h, which contains the paper's case. is a hypothesis.IsPrimitiveRoot η (h - 1), equivalent to generating since .∀ i, f.degreeOf i ≤ d - 1.Fin m, starting at ; substitutes for .Lagrange.basis over the field at the nodes , mapped into , with coefficients . is the remainder modulo (AdjoinRoot.modByMonicHom) evaluated at .A formalization that takes to be any element satisfying (6.2), or defines as a ring homomorphism, would make the goal trivial or false; both are ruled out because and are explicit definitions with no hypotheses attached, and (6.1) and (6.2) are milestones to be proved.
Infrastructure a full proof needs: the Frobenius on polynomial rings in characteristic (, cf. Mathlib's expand and map_frobenius_expand), Lagrange interpolation transported along a ring homomorphism from a field, degree bounds for MvPolynomial.eval₂, and reducedness of (from separability of over the perfect field ). Proofs of any milestone, and alternative arguments, are welcome.
A vendor holding a finite stock of a product must set prices over time without knowing how many customers will come. Each price does two things: it earns revenue now, and through the sales it generates it reveals information about demand that improves future prices. This tension between earning and learning is central in revenue management with demand uncertainty, in retail markdown pricing, and in online selling. Optimal Bayesian policies for such problems are characterized by a Hamilton–Jacobi–Bellman equation that has no closed-form solution, so practice relies on heuristics, and the question is which heuristics come with guarantees.
Farias and Van Roy introduced decay balancing and proved that, for exponentially distributed reservation prices and a Gamma prior on the arrival rate, it earns at least one third of the optimal expected discounted revenue, uniformly over all problem parameters (V. F. Farias, B. Van Roy, Dynamic Pricing with a Prior on Market Response, Operations Research 58(1):16–29, 2010, doi:10.1287/opre.1090.0729). They describe it as the first heuristic for problems of this type with a uniform performance guarantee. This mission formalizes that guarantee and the chain of results leading to it. The source is the authors' manuscript of January 20, 2009 (MIT DSpace); its printed page numbers coincide with the PDF page numbers, and all theorem and page numbers below refer to it.
Customers arrive according to a Poisson process with rate . Each has an independent reservation price with density and tail ; a customer facing price buys one unit if it is available and is at most his reservation price, and otherwise leaves. The hazard rate is . Assumption 1 (p. 5) asks that be differentiable with support and that be non-decreasing. The exponential law with mean has .
The vendor starts with units and a Gamma prior on with shape and rate (density , mean ). After sales the posterior is Gamma with and , so the state is . A policy sets the price; the expected discounted revenue at rate is
the supremum over all measurable non-negative policies. With known, the same problem has value . Assumption 2 (p. 9) asks that be differentiable in .
Decay balancing uses the approximation , , and posts the price solving the balance equation (5), p. 13,
The optimal price solves the same equation with in place of . The constant
measures the cost of uncertainty for a prior of shape .
For exponential reservation prices with mean , every , , , :
In attack order:
Theorem 2 gives a guarantee that depends only on the coefficient of variation of the prior. Theorem 3 removes even that dependence for exponential reservation prices: whatever the inventory, prior, discount rate and price scale, decay balancing loses at most a factor of three. The analysis also yields reusable facts about Bayesian pricing: knowing the rate helps (), the decay-balance characterization of optimal prices, and comparison with a vendor who does not learn.
All results are proved in the source, using Dynkin's formula, an HJB verification argument (Appendix E) and a coupling of sales processes. None of them is machine-checked. The mission asks for a formal development of the known proofs.
The obvious route to Theorem 3 would chain Theorem 2 at the initial state. That fails because blows up as , so for a diffuse prior Theorem 2 gives no constant bound. The paper instead compares the two systems only up to the first sale, after which the shape parameter is at least . This needs two things: a coupling in which the optimal system never sells first, and Lemma 12, which bounds the value of one extra unit without a decreasing-returns property in (none is known). Lemma 12 itself rests on a numerical inequality involving the Lambert function.
At the foundational level, neither Mathlib nor the platform has a counting process whose intensity is a random rate times a state-feedback price. Defining and faithfully is part of the mission.
Reusable pieces are the Gamma–Poisson sales process in the b-clock, the incomplete Gamma function, and the known-rate pricing problem. Proofs of any milestone, of the p. 6 revenue identity, and of Assumptions 1–2 for the exponential law are welcome.
Related platform work in other models: Gallego–van Ryzin known-demand pricing (GVRPricing), Talluri–van Ryzin (RevenueManagement), Bitran–Caldentey (PricingRM.DetHeuristic), and the Bayesian bounds of Satia–Lave (SatiaLave.Bayes).
Steepest descent is the oldest method for unconstrained minimization: to minimize a smooth function , it moves from the current point along the negative gradient . It is the prototype of every first-order method, and its worst-case evaluation complexity — how many iterations it may need before the gradient norm drops below a tolerance — is the reference point against which faster methods are measured.
For a function that is bounded below and has a Lipschitz continuous gradient, steepest descent with a suitable step-length rule reaches within iterations (Nesterov, Introductory Lectures on Convex Optimization, 2004, p. 29). Whether this bound is tight on nonconvex problems remained open until Cartis, Gould and Toint (preprint 15 October 2009; SIAM J. Optim. 20(6), 2010) built explicit one-dimensional examples showing that it is essentially sharp. The same paper shows that Newton's method can be as slow, and that the bound of cubically regularized Newton methods is also tight; those results are the other missions of this series.
Timeline:
Let be twice continuously differentiable, bounded below, with a derivative that is bounded and Lipschitz continuous. The paper calls these standing assumptions AS.0. Write for the gradient.
Steepest descent with step lengths starts at and sets
The step lengths are only required to lie in a fixed interval (condition (2.6))
Such step lengths can be produced by a Goldstein–Armijo linesearch, which accepts a step when the decrease lies between and for fixed constants .
Fix and put . The mission's definitions (namespace SlowConvergence.SteepestDescent) record the paper's prescribed data: iterates xk, steps sk, values fk, gradients (gk), and the quintic pieces p with the quantities , , of (2.11)–(2.15).
For every , every and every step-length sequence with , there is satisfying AS.0 on all of on which the steepest descent run from has
No constant (Lipschitz constant, gradient bound, lower bound) is fixed in the goal; only its existence is asserted.
The result. Since is arbitrary, the example shows that the upper bound for steepest descent cannot be improved to for any under AS.0, even with a standard Goldstein–Armijo linesearch. It separates steepest descent from second-order methods with better worst-case bounds, and it is the template for the Newton and regularized-Newton examples of the same paper. A matching upper bound for gradient descent with step is formalized elsewhere on the platform (ShiOptRates.gd_exact_rate); together the two describe the complexity of the method up to the exponent .
Formalizing it. The result is proved on paper; to our knowledge no machine-checked version exists. The mission adds a statement in which the method, the function class and the iteration count are fixed precisely. It also corrects three printed slips that a formal check exposes: the iteration count is off by one, the Goldstein–Armijo interval is printed reversed, and an intermediate step of (2.17) is false while its end bounds hold.
Matching prescribed values and gradients at the iterates is easy one point at a time. The difficulty is doing it with uniform control. The interval lengths shrink like , so a naive interpolant has second derivatives growing with , and the gradient is then not globally Lipschitz. The prescribed values must also decrease at a rate whose sum stays finite, or the function is unbounded below. Both constraints pin the exponent: the construction works only because makes the iterates escape to infinity while keeps finite. A further step remains: the paper's function lives on and must be extended to all of without losing any property of AS.0.
The problem is one-dimensional: f : ℝ → ℝ, the gradient is deriv f, and the second derivative is iteratedDeriv 2. AS.0 is ContDiff ℝ 2 f, BddBelow (Set.range f), a global bound on |deriv f|, and LipschitzWith L (deriv f). Every property holds on all of ; the paper constructs on and says it extends smoothly to the negative reals, and that extension is part of the goal.
Conventions:
Real.rpow with base .Infrastructure needed: quintic Hermite interpolation on intervals, gluing piecewise polynomials into a function on along an unbounded increasing knot sequence, a extension to the negative reals, and bounds for real -series. The gluing lemma and the extension are reusable for the Newton and regularized-Newton missions of the series. Contributions of any milestone, of a construction of the glued function of (2.16), or of a direct proof of the goal are welcome.
Multivariate multipoint evaluation asks for the values of a polynomial over a ring , with individual degrees at most , at given points of . Kedlaya and Umans showed that, over finite fields and rings , this problem can be solved in time nearly linear in the input size , for (Kedlaya–Umans 2008, §4). Through their reduction of modular composition, the computation of , to multipoint evaluation (§3 of the same paper), this gives the first nearly-linear-time algorithm for modular composition over finite fields. That in turn gives the fastest known algorithms for factoring univariate polynomials over , with bit operations for a randomized algorithm on degree- polynomials (abstract and §8).
Timeline. Brent and Kung (1978) gave the baby-step/giant-step algorithm for modular composition (J. ACM 25). Huang and Pan (1997) improved the exponent using fast rectangular matrix multiplication. Kaltofen and Shoup (1998) introduced the factoring framework that the factoring application builds on (Math. Comp. 67). Kedlaya and Umans (2008, SIAM J. Comput. 2011) gave the multimodular algorithm formalized here, together with an algebraic algorithm for small characteristic.
Let and write for the integers modulo . Every element of has a lift, its representative in . For , replaces each coefficient by its lift; lifts a point coordinatewise.
Algorithm MULTIMODULAR with degree parameter and rounds takes (degree at most in each variable) and a point . It lists the primes at most , reduces and modulo each , and evaluates the reductions . It does this directly when , and by recursion with rounds otherwise. It then returns, reduced modulo , the unique integer in congruent to modulo every .
Let be monic of degree and . The lift of is its representative of degree at most , with coefficients lifted to , an element of . Put
Algorithm MULTIMODULAR-FOR-EXTENSION-RING runs in four steps.
For monic of degree , , , , every of degree at most in each variable, and every :
In the order the paper's proofs use them:
The result makes multivariate multipoint evaluation exact and fast over every finite ring of the form , which includes every finite field . Combined with the paper's reduction from modular composition (Theorem 3.1) it yields modular composition of degree- polynomials over in bit operations (§7). That is the step on which the paper's improvements to univariate polynomial factorization, irreducibility testing and minimal-polynomial computation rest (§§7–8). The same algorithm gives a data structure answering polynomial-evaluation queries in time polylogarithmic in the degree (§5).
The theorem is proved in the paper; nothing in it is open. As far as is known, no part of it has been machine-checked. This mission formalizes the correctness of both algorithms exactly as the paper defines them, step for step, including the Chinese-remainder recombination, the explicit prime threshold , and the base- digit recovery. Lemma 2.4 is an explicit Chebyshev-type lower bound on the primorial, valid for all , and is reusable independently of this mission.
The recursion itself is routine. Two points carry the content. The first is the explicit prime threshold: the algorithm uses only primes up to , so its correctness depends on the explicit inequality of Lemma 2.4 for every , not on an asymptotic prime-number estimate. The small cases are part of the claim. The second is the extension-ring step: the integer produced over must determine the polynomial exactly. That needs simultaneous control of its degree and of every coefficient, against the specific constants and . A bound on evaluated at a point does not by itself suffice.
Lean represents as ZMod r with (NeZero r, excluding ZMod 0 = ℤ), polynomials as MvPolynomial (Fin m) _ with variables indexed , and as AdjoinRoot E for a monic E with E.natDegree. "Degree at most in each variable" is ∀ i, f.degreeOf i ≤ d - 1. is the natural logarithm; the paper does not fix a base, and the natural log is the strongest reading of Lemma 2.4. The primes for real are the primes . Each algorithm is defined for a single evaluation point, since the paper processes the points independently. The leaf evaluates at directly; that value is what Theorem 4.1's FFT algorithm outputs. is as printed on p. 15; p. 16 prints .
The hypotheses and are not written in the paper but are needed. For , , the threshold is , no prime is used, and MULTIMODULAR returns . For the inequality and the degree bound both fail.
Only correctness is formalized. Every running-time bound in Theorems 4.1, 4.2, 4.4 and Corollaries 4.3, 4.5 is out of scope. The Chinese-remainder step and the digit step are defined from the residues and from alone: an algorithm that evaluates in and reduces it, or that computes in directly, would make the theorems trivial and is not the algorithm stated here.
Needed infrastructure: explicit primorial lower bounds (Mathlib has primorial and Chebyshev's ), the Chinese remainder theorem for several moduli (ZMod.prodEquivPi), bounds on evaluations of polynomials with nonnegative coefficients, and uniqueness of base- representations of polynomials. Lemma 2.4 and the base- uniqueness are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 2.4.
Quasi-Newton methods replace a costly exact Hessian with an operator updated from successive changes in position and gradient. A secant update must map the observed step to the observed gradient difference . Many operators satisfy that one equation, so the choice of update needs another criterion. Gilbert and Lemaréchal's working paper studies variable-storage quasi-Newton algorithms and, in its Annex, characterizes familiar update formulas by how little they change the previous operator. The Annex treats real Hilbert spaces, rather than only matrices on Euclidean space, and allows the underlying scalar product and the weighting operator to vary. Its least-change characterization is the subject of this mission.
The source is the August 1988 IIASA Working Paper WP-88-121. A revised journal article appeared in 1989, but the theorem numbers and printed page references here belong to the working paper. The work is a formalization of a result proved in that paper; the mathematical question is not open.
Let be a complete real inner-product space. A continuous linear operator is the current Hessian approximation. A step and a gradient difference determine the quasi-Newton equation for the updated operator . Write , where is the perturbation. The source restricts to the Hilbert–Schmidt class , so its size can be measured by an orthonormal basis :
The index set need not be countable; membership in means the displayed family is summable. The value is independent of the chosen orthonormal basis. For , the paper's bracket operator is . The order of its arguments matters.
The nonsymmetric feasible set is . For a self-adjoint , the symmetric problem uses . A bijective continuous operator weights the symmetric objective . The vector records how this weight changes the update. Both the feasible set and the weighted objective matter: taking a minimum over every bounded operator would change the problem.
The goal is Proposition A.2 on printed p. 28 of the working paper. Suppose , is bijective, and . With and , define
The target asserts that belongs to and is the unique minimizer of over . Its formula depends on only through . No positivity condition on or on is part of this result.
The milestones follow the source's supporting statements in order. They establish that the Hilbert–Schmidt sum is independent of the orthonormal basis and defines a norm on its domain; that the operator norm is bounded by this norm and the Hilbert–Schmidt class is stable under multiplication by bounded operators; the bracket identity ; the two bracket composition identities; Proposition A.1, the unique nonsymmetric least-change update for ; and its instance , Broyden's update (A.5). The goal adds self-adjointness and a single two-sided weight.
The Annex then draws consequences of the goal, which are further milestones: the instance is the psb (Powell symmetric Broyden) update; Proposition A.3 states that for nonzero a self-adjoint positive operator ( for ) with exists if and only if for a bijective , if and only if ; with the weight becomes and (A.7) becomes the dfp (Davidon–Fletcher–Powell) update (A.8); and (A.9) is a product form of the dfp update from which its positivity follows when is self-adjoint positive and .
The theorem gives a precise optimization property to a rank-two symmetric secant formula. It identifies the operator selected by the weighted least-change criterion and guarantees there is no other feasible minimizer with the same value. Taking the weight to be the identity yields the psb update, and taking with yields the dfp update, so two of the classical symmetric secant formulas are least-change updates for different weights. Proposition A.1 similarly characterizes the rank-one update that becomes Broyden's formula when its right weight is the identity. These consequences explain why the familiar formulas arise from a common variational question, as the Annex states.
The paper supplies a mathematical proof. The remaining formalization work is to represent the Hilbert–Schmidt class, its norm and ideal property, the weighted objectives, and the exact minimization claims in Lean, then prove those claims. Mathlib supplies Hilbert spaces, Hilbert bases, bounded linear maps, adjoints, and the rank-one operator corresponding to the paper's bracket. The statements drafted for this mission compile, but they carry sorry and have no machine-checked proof from this mission yet. A completed development would leave reusable Hilbert–Schmidt and rank-one operator results beyond this quasi-Newton application.
The secant equation alone fixes an operator on only one vector. Even in two dimensions, a rank-one perturbation can satisfy that equation while failing to preserve self-adjointness. Requiring self-adjointness leaves many candidates, and minimizing the two-sided weighted Hilbert–Schmidt norm must distinguish exactly one of them. In infinite-dimensional spaces the norm also has a domain: some bounded operators have an infinite square sum. A formulation that silently assigns a finite default value to a nonsummable operator could turn the least-change claim into a different assertion. These are the mathematical and formal obstacles the milestone list exposes.
Lean uses an arbitrary complete real inner-product space, with no finite-dimensional or separability assumption, and an arbitrary HilbertBasis index type. Each theorem takes a basis parameter; the basis-independence milestone states why this represents the paper's basis-free norm. The reusable definitions for the bracket and the Hilbert–Schmidt square sum are separate from the paper-specific feasible sets. bracket u v abbreviates Mathlib's rankOne ℝ u v, with paired with the input. A bijective bounded operator is represented by a continuous linear equivalence ; the bounded inverse theorem makes this equivalent to the paper's bijective member of . The definition of applies the adjoint of to .
Lean's real tsum has a default value when the family is not summable, so the Hilbert–Schmidt norm is used as a norm only for operators satisfying the explicit summability predicate. Both and include that predicate. The ideal-property milestone covers the weighted operators in the two objectives. The hypothesis is exactly the proposition's condition; it entails , so no extra nonzero-denominator hypothesis is imposed. The statement spells out “unique solution” as feasibility, minimality over every feasible perturbation, and equality of every feasible minimizer with . The paper prints “problem (A.5)” in Proposition A.2, but (A.5) labels Broyden's displayed formula; its preceding paragraph defines the relevant symmetric minimization as (A.6). This mission formalizes (A.6).
In Proposition A.3 and (A.9), "positive" is the paper's strict notion for , not the non-strict positivity of Mathlib. The identity (A.9) is stated for self-adjoint and , the setting of the Annex's symmetric problem; the paper's sentence before the psb formula repeats the "(A.5)" misprint and is read as (A.6) in the same way.
The definition layer, basis independence, operator-ideal property, bracket results, both least-change propositions, and the Broyden, psb, dfp and positivity statements are welcome proof targets. The scaling results of §4.1 are outside this mission.
Modular composition asks, given univariate polynomials over a ring, for . It is the bottleneck step in the classical algorithms for factoring univariate polynomials over finite fields (Cantor–Zassenhaus, von zur Gathen–Shoup, Kaltofen–Shoup), for irreducibility testing and for computing minimal polynomials. Brent and Kung (1978) gave an algorithm using operations for degree , and for three decades no algorithm with a near-linear operation count was known in general.
Kedlaya and Umans (Dagstuhl Seminar Proceedings 08381, 2008; journal version SIAM J. Comput. 40(6), 2011, doi:10.1137/08073408X) obtained near-linear modular composition over finite fields, and with it asymptotically faster algorithms for factoring polynomials over finite fields. Their route has two halves: a reduction of modular composition to multivariate multipoint evaluation (Section 3), and new fast algorithms for the latter (Sections 4 and 6). This mission formalizes the correctness of the first half, Theorem 3.1. The paper notes that Shoup and Smolensky used essentially the same transformation in an unpublished 1992 manuscript.
Throughout, is an arbitrary commutative ring. Variables are indexed from .
MULTIVARIATE MULTIPOINT EVALUATION (Problem 2.1): given with individual degrees at most and points , output .
MODULAR COMPOSITION (Problem 2.2): given with individual degrees at most , and of degree at most with the leading coefficient of a unit, output , the unique with and .
The inverse Kronecker map (Definition 2.3) is the -linear map that sends the monomial to , where is the base- expansion. It trades individual degree for number of variables: every individual degree of is below .
The algorithm of Theorem 3.1 takes , sets and , receives points whose differences are units, and
for all , , with individual degrees , of degree with a unit, and distinct with unit differences. The right-hand side is stated through the characterization of the remainder (divisibility by and degree below ).
A supporting theorem states that the interpolation formula over a commutative ring (Figure 1) recovers every polynomial of degree from its values at nodes with unit differences.
Theorem 3.1 says that modular composition is no harder than one multivariate multipoint evaluation with variables, individual degrees below , and points, up to quasi-linear univariate work. Combined with the paper's fast multipoint evaluation algorithms this gives modular composition over in bit operations, and from there the paper's improved bounds for polynomial factorization, irreducibility testing, minimal polynomials and modular power projection (Sections 7–8). The converse reduction (Theorem 3.3) shows the two problems are essentially equivalent.
The paper's proof of correctness is a short paragraph; the operation counts are the paper's main concern. This mission makes the correctness exact: the algorithm is defined step for step, and its output is proved equal to the specification. As far as the platform's corpus shows, neither the inverse Kronecker map nor this reduction has a machine-checked statement; the running-time half is not part of this mission.
The obvious argument substitutes for and invokes the inverse Kronecker identity. Two points keep this from being immediate. First, is linear but not multiplicative, and it discards base- digits beyond position ; the identity holds only for individual degrees at most , which here requires . Second, the algorithm never sees itself, only its values at points: interpolation recovers it only if its degree is below , which is why Step 2 reduces modulo before substituting, and interpolation over a ring (not a field) needs the unit-difference hypothesis throughout. Mathlib's Lagrange interpolation is stated over fields, so the ring version must be handled directly.
CommRing R); there is no field or nontriviality assumption.Fin m; the new variables are Fin m × Fin ℓ; points are Fin N'.MvPolynomial.degreeOf; "degree at most " is natDegree ≤ N - 1.Nat.clog d₀ d and ; is not a free parameter.Ring.inverse of the node differences.MvPolynomial.eval, which is exactly the output of Problem 2.1.Step 5 is the interpolation formula applied to the computed values and nodes alone; it is not defined as the polynomial , and the goal is the six-step output, not the congruence alone, so the statement cannot be closed by unfolding definitions.
Useful infrastructure, reusable beyond this mission: base- digit manipulation of exponent vectors, Lagrange interpolation over commutative rings with unit node differences, and remainders modulo polynomials with unit leading coefficient. Proofs of any milestone, and of the supporting interpolation theorem, are welcome independently.
Many objectives in statistics and machine learning are neither smooth nor convex, yet are well behaved in a weaker sense: robust phase retrieval, blind deconvolution, robust PCA and training with piecewise-linear losses all lead to weakly convex functions, functions that become convex after adding a fixed quadratic. For such functions the plain subgradient method remains the method of choice, and the natural question is how fast it reaches approximate stationarity. Davis and Drusvyatskiy (SIAM J. Optim. 2019) gave the first such rate, measured by the gradient of the Moreau envelope, of order .
Das Gupta, Van Parys and Ryu (Math. Program. 204 (2024) 567–639) introduced BnB-PEP, a branch-and-bound method for solving nonconvex performance-estimation problems to global optimality, and used it to construct optimal and efficient first-order methods. Their one fully analytical result (§6.3) is a new potential-function analysis of the subgradient method on weakly convex functions with bounded subgradients. It produces an explicit stepsize and a rate that strictly improves on the Davis–Drusvyatskiy bound for all large enough . The certificate was found numerically; the paper then gives a classical proof that can be checked by hand. This mission formalizes that result.
Work in with the Euclidean norm. A function is -weakly convex if is convex. For such , a vector is a subgradient of at , written , when
The class consists of the -weakly convex whose subgradients all satisfy . Since exactly when , the paper sets and writes ; here the normalized bound is written (Lean: InWeakClass 1 L f, with subgradients IsWeakSubgrad 1 f x g).
For the proximal point is the unique minimizer of , and the Moreau envelope is the minimum value
(Lean: SAGA.Convex.IsProxPoint f (1/ρ̂) x y and moreauEnv ρ̂ f x). The envelope is continuously differentiable, and its gradient is a subgradient of at the prox point . With , the paper's choice, small means that is near a point that is nearly stationary for .
The method is for , where each is arbitrary. One writes , , assumes a global minimizer and the initial condition , and sets .
For the stepsize , provided ,
The bound holds for every choice of subgradients along the run.
For , , and , the potentials satisfy
In proof order: the Moreau-envelope facts of §6.3.1; the one-step inequality (32) for an arbitrary point; the telescoping display after (32); the closed form (44) of with nonnegativity; Theorem 1; the closed form (45) of its bound in ; the majorant (46) with Bernoulli's upper bound; and the minimizer of (46) with its value.
The result. Corollary 1 gives an explicit, non-asymptotic rate for the most basic method of nonsmooth nonconvex optimization, with explicit constants and an explicit stepsize. As the bound is asymptotic to , and the paper shows it is strictly below the earlier bound once . It also bounds . It shows that computer-assisted performance estimation can produce closed-form guarantees beyond the convex, interpolable function classes where PEP is usually applied.
Formalizing it. The result is proved on paper twice (pp. 622–627), but nothing about weakly convex functions, their subdifferential or the Moreau envelope in the nonconvex regime is formalized on the platform, and the convergence analysis has not been machine-checked. A complete development formalizes the potential-function proof and supplies reusable facts about weakly convex functions and the Moreau envelope.
The scalar part of the argument ((44)–(46) and the plug-in) is elementary algebra and one Bernoulli inequality. The analytic weight sits in two places. First, the Moreau envelope of a nonconvex function: showing that the real infimum is attained at the prox point, that the envelope is differentiable with gradient , and that this gradient is a subgradient of at with the weak-convexity modulus (not the modulus that the prox inequality gives directly). Second, inequality (32): it is not a consequence of convexity, since is not convex, and it must hold for an arbitrary current point and an arbitrary subgradient, with parameters fixed in advance. The obvious route through descent of itself fails: need not decrease for nonconvex , which is why the potential uses the envelope at the iterates.
The carrier is EuclideanSpace ℝ (Fin d), and is real-valued and defined everywhere. The weak-convexity modulus is normalized to , and the Lean name L is the paper's ; the general class follows by scaling and is not stated. The subdifferential is the weak-convexity inequality above. For weakly convex it equals the Clarke, Fréchet and limiting subdifferentials, so it is the paper's abstract in every admissible instance. The convex subdifferential of is not used: it can be empty for nonconvex and would make the statements vacuous. The run is given by sequences x g y : ℕ → E, with g k an arbitrary subgradient at x k for , and y k tied to x k by IsProxPoint f (1/2) for . is not free: it is . The Moreau envelope is a real ⨅; it is finite and attained in this regime, and the first milestone proves this. The parameters of Theorem 1 are pinned by hypotheses, not chosen existentially.
Two hypotheses are made explicit. Corollary 1 is stated "in the setup of Theorem 1", which requires ; for the prescribed stepsize this is , and it is carried as the hypothesis . It fails for and whenever is large relative to . Inequality (32) is stated for one arbitrary step, under the nonnegativity of the alternate proof's weights (, , ). The minimizer is assumed, as in the paper; the remark on p. 627 that suffices is not used.
Useful contributions include basic lemmas on weakly convex functions (existence of subgradients, strong convexity of the prox subproblem), differentiability of the Moreau envelope for , the weighted-sum identity behind (32), and Bernoulli's upper bound for .
Large optimization problems often split into blocks owned by different agents (subsystems of a power grid, vehicles in a formation, scenarios of a stochastic program) that are coupled only through a few linear constraints. Distributed optimization methods solve such problems by letting each agent work on its own block and exchanging a small amount of information, typically a vector of prices for the coupling constraints. The classical method of this kind is dual decomposition (Everett 1963; Bertsekas and Tsitsiklis, Parallel and Distributed Computation, 1989): fix the prices, let every agent solve its own subproblem, then update the prices by a gradient or Newton step on the concave dual function. Dual decomposition is reliable for strictly convex problems but has no convergence guarantee for nonconvex ones.
Houska, Frasch and Diehl (SIAM J. Optim. 26 (2016)) proposed ALADIN (augmented Lagrangian based alternating direction inexact Newton), which adds a proximal term to the agents' subproblems and replaces the price update by a coupled equality-constrained quadratic program. ALADIN is used in distributed model predictive control and in power-system optimization. Remark 4.2 and Appendix A of the paper explain where it sits relative to the classical method: if the proximal term is switched off (), the price update of ALADIN is exactly a regularized Newton step of dual decomposition. Lemma 5 is the precise statement of that equivalence, and it is the goal of this mission.
The problem (1.1) has blocks :
with , twice continuously differentiable, and . One iteration of Algorithm 2 (ALADIN) starts from a primal point and prices and does the following.
and the new prices are .
On the dual-decomposition side, (A.3) is the gradient of the dual function at , and the (inexact) dual Newton step (A.4) with a symmetric negative semidefinite scaling matrix and step size is
where plays the role of a Levenberg–Marquardt regularization parameter.
Assume every strictly convex, every convex, of full row rank, positive definite, and . Then for every , with
the matrix is invertible and
The result. Lemma 5 places ALADIN on a known map. With it inherits the convergence theory of dual decomposition for strictly convex problems for small step sizes, independently of how crude the approximations , are, as long as . It also reinterprets the augmented-Lagrangian parameter as the inverse of a dual Levenberg–Marquardt parameter, and it isolates the proximal term as the only ingredient that distinguishes ALADIN from dual decomposition and makes the nonconvex analysis of the paper possible.
Formalizing it. The lemma is proved in the paper; to our knowledge no machine-checked proof exists. A formal proof certifies an identity whose printed form contains a typo (see below), and produces reusable linear-algebra facts: the closed-form solution of an equality-constrained strictly convex quadratic program via the reduced inverse , the semidefiniteness of , and the closed-form maximizer of a regularized concave quadratic.
The proof is a chain of exact eliminations, and the work is in carrying each one out without losing a sign or a hypothesis. The step most easily done wrong is the minimization over : the constraint couples the block coordinates, the minimizer is expressed through the inverse of (invertible only because has full row rank). A second trap is the sign convention for : it must agree with footnote 4 (), or the conclusion flips. The tempting shortcut of treating the max–min dual of (3.3) abstractly runs into the fact that strong duality and attainment are not free; working from the KKT system of (3.3) avoids that.
Vectors are Fin n → ℝ; blocks are indexed by Fin N; matrices are Mathlib Matrix over Fin index types; the gradient is the vector of partial derivatives computed with fderiv. The step-1 output is a local minimizer of the decoupled problem together with KKT multipliers (the paper assumes LICQ for the lower-level constraints). The QP (3.3) and enter through the KKT system of (3.3), not through a closed-form expression: defining or by the formula of the conclusion would make the goal true by definition and is ruled out. is the formula (A.3); that it is the gradient of the dual function is a cited fact the lemma does not use. The invertibility of is part of the conclusion, because Mathlib's matrix inverse returns on a singular matrix.
Correction of (A.6). As printed, (A.6) has the bracket . This is a typo for , as in (A.5) on the same page and as the explicit minimization over forces; with the printed bracket the identity fails already for , , , . The mission uses the corrected matrix and writes the pseudo-inverse as an inverse, which it is under the hypotheses.
The hypotheses of strict convexity of , convexity of and are kept as on the page although the identity does not use them. The related platform draft GoldfarbIdnani.DualQP.properties_2_6_to_2_9 (not proved) states properties of the same reduced inverse; it is not imported. Proofs of the four milestones and of the goal are welcome; the milestones are self-contained matrix and calculus facts and can be attacked independently.
Many large optimization problems arising in networked control, smart grids, distributed estimation and resource allocation have a separable objective with coupled affine constraints: agents each own a variable and a private cost , and only a linear constraint ties them together. Distributed algorithms for such problems let each agent solve a small local problem and exchange only a few aggregated quantities. For convex problems the standard method is the alternating direction method of multipliers (ADMM), which converges at a linear rate; for nonconvex problems ADMM can diverge (Houska, Frasch and Diehl give a two-variable example in §2 of their paper).
Houska, Frasch and Diehl (SIAM J. Optim. 26 (2016)) proposed ALADIN (augmented Lagrangian based alternating direction inexact Newton method), which combines the decoupled augmented-Lagrangian subproblems of ADMM with a coupled equality-constrained quadratic program borrowed from sequential quadratic programming (SQP). Their local convergence analysis (§7) rests on one stability result for the decoupled subproblems, Lemma 3, which this mission formalizes. Similar statements are classical for augmented Lagrangian methods: Bertsekas analyzes minimizers of augmented Lagrangians under perturbation of the multiplier (Constrained Optimization and Lagrange Multiplier Methods, 1982, Prop. 4.2.3), and Nocedal and Wright give a related analysis (Numerical Optimization, 2nd ed., 2006, Thm. 17.6).
Problem (1.1). Given , , () and ,
All and are twice continuously differentiable (the paper's standing assumption in §3). The multiplier of the coupling constraint is , that of is .
A KKT point is feasible, satisfies for every , and has with . It is regular if
The decoupled subproblems. In step 1 of ALADIN, given the current primal and dual iterates , a penalty and positive semidefinite scaling matrices , agent solves
with . These problems are nonconvex in general and are solved to local optimality.
Let be a local minimizer of (1.1) with a regular KKT point, and let satisfy
Then for every sufficiently small ball of radius around the origin of there are constants such that for all with the problems (3.2) have local minimizers , unique in , with
The constants are not specified: the goal asserts only the shape of the estimate, not values of .
Lemma 3 is the bridge between ALADIN and the local theory of SQP. Once the decoupled minimizers are known to exist, to be locally unique, and to stay within a linear distance of , the full-step variant of ALADIN behaves locally like an inexact SQP method, and the paper derives its local quadratic convergence estimates (with exact Hessians and a suitably large ) from this. Without the lemma the local subproblems could jump between distant local minimizers of a nonconvex objective, and no local rate could be claimed.
The result is proved in the paper, in a short paragraph that delegates the main step to the regularity of the KKT point. No machine-checked version of this lemma, of the sensitivity theory of parametric nonlinear programs it rests on, or of ALADIN exists, as far as a search of the Prove2Me catalogue and Mathlib shows. Formalizing it means supplying the argument the paper leaves implicit: a parametric local-minimizer theorem for inequality-constrained problems under LICQ, strict complementarity and a second-order condition.
The obvious argument applies the implicit function theorem to the stationarity condition of (3.2), . That works only without inequality constraints. With constraints, the local minimizer satisfies a KKT system involving the multipliers and complementarity, which is not a smooth equation; one has to fix the active set, use strict complementarity to show that it does not change nearby, and use LICQ of the active constraints to make the reduced KKT matrix invertible. The second difficulty is uniqueness: the implicit function theorem gives a unique KKT point near , but the lemma claims uniqueness among local minimizers within a ball in the primal variable alone, so the multipliers of any nearby local minimizer must be shown to lie near . Third, the hypothesis is the positive definiteness of on all of , not only on the critical cone; the subproblems inherit their second-order condition from it rather than from the SOSC of (1.1).
Vectors are Fin n → ℝ with Mathlib's sup norm, blocks are indexed by Fin N, matrices are Mathlib Matrix over Fin index types, and Fin m → ℝ. Gradients and Hessians enter through Fréchet derivatives (fderiv), with written fderiv ℝ (fderiv ℝ g) z d d. LICQ is stated as linear independence of the active gradients in . The "sufficiently small open set " is read as every ball of radius in the sup norm of , with allowed to depend on but not on ; is read through the -component, . Local minimizers are local minimizers on the feasible set and are required to be feasible. The hypotheses and come from the paper's standing assumptions (§3 and Algorithm 2, step 1).
A trivializing formalization is ruled out: the goal keeps all four conclusions (local minimality, membership in the -ball, uniqueness in that same ball, and the bound), since the bound alone is satisfied by ; and it quantifies over every small ball rather than asserting the result for one neighbourhood. The hypotheses are satisfiable: a sorry-free check with , , , , , , is in the development.
Needed infrastructure: a parametric implicit-function argument for KKT systems with a fixed active set, persistence of LICQ and of strict complementarity under perturbation, and second-order sufficiency for inequality-constrained problems. These pieces are reusable well beyond this mission, for any sensitivity or local-convergence analysis of nonlinear programs (SQP, augmented Lagrangian, interior-point methods). Proofs of any milestone, alternative routes (for instance via Robinson's strong regularity), and general lemmas on second-order sufficient conditions are welcome.
Most stochastic dynamic programs that arise in operations research are too large to solve exactly. In practice one computes a heuristic policy and estimates its expected reward by simulation, which gives a lower bound on the optimal value. To know whether the heuristic is good enough one also needs an upper bound. Brown, Smith and Sun (Oper. Res. 2010) give a general way to produce such bounds: relax the requirement that decisions use only the information available when they are made, and charge a penalty for using the extra information.
The idea grew out of option pricing. Rogers (Math. Finance 2002) and Haugh and Kogan (Oper. Res. 2004) bounded the price of an American option from above by letting the holder see the whole future and subtracting a martingale; Andersen and Broadie (Manag. Sci. 2004) built such martingales from approximate exercise policies. Brown, Smith and Sun (2010) extended this to general finite-horizon dynamic programs, to arbitrary penalties, and to imperfect information relaxations in which the decision maker learns some, but not all, of the future. The paper illustrates the framework on an adaptive inventory problem and on pricing American options under stochastic volatility and interest rates.
Uncertainty is a probability space . Time is . The natural filtration describes what the decision maker knows at the start of each period, with . An action sequence is , and is the set of feasible sequences. A policy chooses a sequence for each outcome; it is adapted to a filtration if each action is -measurable. The adapted policies form ; the measurable policies form . The total reward is , and the primal problem (1) is
A filtration is a relaxation of if for all ; the perfect-information relaxation has . A penalty is a function ; it is dual feasible, , if for every . The dual bound of is .
In recursive form, the feasible actions in period form a set , each is -measurable and depends on , and the value functions are and
Given generating functions depending on , Proposition 2.2 builds the penalty
The ideal penalty is this penalty for .
For every relaxation of , and
a primal-optimal also attains the right side; and under perfect information almost surely.
Theorems 2.1 and 2.3 say that information-relaxation duality has no gap: the optimal value of a dynamic program can be computed, in principle, as a minimum over penalties of a problem in which the decision maker sees more. Theorem 2.3 adds that the gap is closed by one explicit penalty, built from the value functions, simultaneously for every relaxation. This is the justification for the practical recipe of the paper and of the literature that followed: choose generating functions that approximate the true value functions, and the resulting dual bound approaches the optimum. Under perfect information, part 4 of the goal says the ideal penalty removes all randomness from the penalized reward of an optimal policy.
The paper defers its proofs to an electronic companion; none of these results has a machine-checked proof. This mission produces a checked version of the duality layer for general finite-horizon dynamic programs on a filtered probability space, with conditional expectations as in Mathlib. Weak duality, strong duality and complementary slackness are stated for arbitrary feasible sets and rewards and are reusable for any information-relaxation argument; the recursive statements give a verified link between the Bellman recursion and the primal problem.
The duality statements of §2.2 are elementary once expectations exist; the work is in §2.1 and §2.3. The claim that is the optimal value of (1) needs two facts that the paper asserts without proof: that the supremum in (2) is -measurable, and that near-optimal actions can be selected measurably, so that a nonanticipative policy comes within of even when the suprema are not attained. Neither holds for general action spaces without measurable-selection arguments, which is why this mission fixes a countable action set. A second difficulty is the evaluation of action-indexed conditional expectations at a random action: conditions , where each is only defined up to null sets, one for each . The induction must also carry these almost-sure identities through suprema over actions.
The Lean development lives in the namespace InfoRelax.IdealPenalty. Periods are Fin (T + 1); actions take values in one type X (the disjoint union of the per-period action sets); filtrations are Mathlib Filtrations of the ambient -algebra; conditional expectation is condExp. Primal values, dual bounds and dual values are in EReal, taken over the adapted-policy sets, so that no supremum or infimum silently returns . Penalties in are required to be integrable along every measurable policy, and the reward is assumed integrable along every policy in the general statements: without this, a Bochner integral of a non-integrable function is and the statements become vacuous. The value functions (2), the dual value functions (10), the penalty of Proposition 2.2 and are definitions computed from the data, never variables constrained by hypotheses.
The recursive statements fix a countable action set with the discrete -algebra, bounded period rewards, and generating functions bounded almost everywhere. Identities between value functions are almost sure. The general results (Lemma 2.1, Theorems 2.1–2.2, Proposition 2.1) assume none of this. The optional identity (5), which exchanges a supremum over policies with an expectation of a pathwise supremum, is not formalized: for a general dual feasible penalty the pathwise supremum need not be integrable.
Contributions welcome: the measurable-selection lemma for countable action sets, the tower-property argument for action-indexed conditional expectations evaluated at adapted policies, and proofs of the milestones in any order.
Worst-case iteration counts are the standard way to compare unconstrained optimization methods on nonconvex problems. For finding an approximate first-order critical point, a point with , steepest descent needs at most iterations on functions with a Lipschitz gradient. The cubic regularization of Newton's method needs at most iterations on functions with a Lipschitz Hessian. This bound was proved by Nesterov and Polyak (2006) for exact global model minimization (doi:10.1007/s10107-006-0706-8). Cartis, Gould and Toint (2009a, 2011) extended it to the adaptive variant ARC with approximate model minimization (doi:10.1007/s10107-009-0286-5).
An upper bound alone leaves open whether a better analysis could lower it. Cartis, Gould and Toint (SIAM J. Optim. 20(6), 2010, doi:10.1137/090774100) settle this for three methods by explicit one- and two-dimensional examples. This mission formalizes the third: the bound for ARC is sharp up to an arbitrarily small loss in the exponent.
Timeline:
Let be twice continuously differentiable, and write , . At an iterate , with a regularization weight , the cubic model (1.3) is
One iteration of the Adaptive Regularization with Cubics (ARC) algorithm, in the variant considered here, proceeds as follows.
The parameters satisfy and . In Lean the model is SlowConvergence.ARC.model, the ratio rho, and a run is the predicate IsARCRun f γ₁ γ₂ η₁ η₂ x s σ.
The paper fixes and sets . It then prescribes iterates , with , and function values (5.3). At the iterates it prescribes gradients , Hessians and weights (5.4).
For every there are a function and a run of ARC on it from , , with the following properties:
The goal fixes no Lipschitz constant or Hessian bound; it asserts the existence of the example, which is the paper's claim.
The example shows that the upper bound of Nesterov–Polyak and Cartis–Gould–Toint cannot be improved to for any , even in one dimension and with exact global model minimization. It also shows that adaptive weights do not help: the run is valid for every choice of the algorithm's parameters. Together with the paper's other two examples, it separates the worst-case orders of steepest descent and Newton's method () from that of ARC (). The paper ends by asking whether is optimal among all second-order methods. That question was answered later by Carmon, Duchi, Hinder and Sidford (2020) for a broad algorithm class.
The paper's argument is a construction checked by hand plus a plot of the first sixteen intervals. No machine-checked version of this lower bound is known to exist. A formal proof would certify every interpolation identity, the uniform third-derivative bound and the gluing into a globally function. The upper bounds of Nesterov and Polyak are separate statements on the platform (CubicNewton.Nonconvex.*) and are not proved there.
Checking the algebra at the iterates is routine; the difficulty is the function. The piecewise quintic must be twice continuously differentiable across infinitely many knots. Its second derivative must be Lipschitz with one constant on the whole line, although the intervals shrink like . This requires a third-derivative bound that does not grow with . The obvious first idea is to interpolate values and slopes with cubics; it fails, because the second derivative must vanish at both ends of every interval to match . A further step is that the knots go to only because , which is where enters. Finally, must be extended to without losing boundedness below or the global Lipschitz bound.
f : ℝ → ℝ, = deriv f, = deriv (deriv f), for the norm. The model uses the true second derivative of the same , not a free approximation . The step is a global minimizer of the model; uniqueness is not required.Data (iterates, values, gradients, the model built from them) and Pieces (the quintics , ). Proofs of the polynomial identities and of gluing infinitely many polynomial pieces into a function with a global Lipschitz second derivative are reusable for the paper's other two examples. Proofs of the milestones, of the gluing lemma, and of the goal are all welcome.CubicNewton.Shared.cubicModel and IsCubicStep are the same model and step in with ; they are not imported here.Methods for smooth unconstrained minimization, , are compared by how many evaluations of and of its gradient they need, in the worst case, to reach an approximately first-order critical point, an iterate with . For steepest descent with a Lipschitz gradient the answer is (Nesterov, Introductory Lectures on Convex Optimization, 2004, p. 29). Nesterov and Polyak (2006) showed that globally minimizing a cubic regularisation of the second-order model, with the exact Hessian and a global Lipschitz constant, improves this to .
The adaptive regularisation with cubics (ARC) framework of Cartis, Gould and Toint makes that idea practical: the Hessian is replaced by an approximation , the Lipschitz constant by an adaptive weight , and the global model minimizer by any step that does at least as well as a Cauchy point. Part I (Math. Program. 127, 2011) proved global convergence; Part II (Math. Program. 130, 2011) counts evaluations. This mission covers the first count of Part II (§§2–3): with only the Cauchy condition on the step, ARC needs iterations, the same order as steepest descent and as trust-region methods (Gratton, Sartenaer and Toint, SIAM J. Optim. 19, 2008).
Let be continuously differentiable (AF.1), , and the Euclidean norm. At iterate , with a symmetric matrix and a weight , the cubic model is
Algorithm 2.1 (ARC) takes parameters , , and a starting point . At iteration it
For , and are the successful and unsuccessful iterations among . The complexity results use three assumptions: AM.1, for all ; AF.4, on an open convex set , with ; and a lower bound . Optionally, (2.10): on very successful iterations, for some . The constants are
Let with , and let be the first iteration with . Then
and, if (2.10) holds,
The constants are kept exactly as printed. The first bound counts gradient evaluations and the second counts all iterations, which is the number of function evaluations.
The corollary establishes that the ARC framework, whatever step it takes beyond the Cauchy point and whatever symmetric it uses, is never worse than steepest descent in evaluation count. It is the baseline against which Part II measures its second-order variant ARC(S), whose bound is the subject of a separate mission in this series. Theorems 2.1 and 2.2 are generic: they convert any per-iteration model decrease and any bound on into iteration counts, and are reused verbatim for ARC(S).
The results are proved in the paper. No machine-checked proof of any of them exists on Prove2Me or, to our knowledge, elsewhere. The work here is to formalize the known proofs: the Cauchy-point analysis of Part I (quoted, not reproved, in Part II), the Taylor-remainder estimate of Lemma 3.2, and the counting arguments. Formalizing also checks the printed statements: two of them need a small correction (see Formalization scope).
Each step is elementary, but the statements are about a nondeterministic algorithm: and are choices, so every bound must hold for all admissible choices, not for one convenient run. The constants are explicit, and the ceilings interact: the printed proof of (3.17) adds the ceilings of (3.15) and (3.22), which does not by itself give ; the bound must be derived from the unrounded estimates. Lemma 3.1 i) requires a careful one-dimensional analysis of with an indefinite . The ratio is a quotient, and its denominator must be shown positive before any comparison with , is meaningful.
The space is EuclideanSpace ℝ (Fin n); is Mathlib's gradient f; is a continuous linear operator with IsSelfAdjoint, and is the operator norm. A run is a predicate IsARCRun on the sequences ; the Cauchy condition is stated as for all , which is equivalent to comparing with the Cauchy point and avoids defining an argmin. The run is infinite; a run that the paper would stop at extends trivially, and every statement only concerns iterations with . Lean's x / 0 = 0 gives (unsuccessful) when ; Theorem 2.2 assumes (2.6), , up to its horizon, and §3's results need nothing extra because makes the denominator positive.
"" is stated as: every with for all satisfies (and similarly for ). This asserts that is finite without presupposing it. Statements with are given for every finite .
Two corrections to the printed text are built in. In Theorem 2.1 the bound is assumed for : as printed () the theorem fails for , iteration unsuccessful, . In AF.4 the set must contain the trial points as well as the iterates, because Lemma 3.2 applies the Lipschitz bound on the segment .
A trivializing formalization is ruled out: the goal quantifies over every admissible step and weight update rather than one particular choice, keeps (2.10) out of the first conclusion, and keeps every constant as printed rather than replacing it by an existential.
A complete development needs the one-dimensional cubic analysis behind Lemma 3.1, a mean-value bound for functions along a segment, and finite counting over Finset.range. The generic counting results (Theorems 2.1, 2.2) are reusable for every ARC variant. Proofs of any milestone, and of the goal from the milestones, are welcome.
Quasi-Newton methods minimize a smooth function using gradients only, while building up an approximation to the inverse of the Hessian matrix from the changes of gradient they observe. They are the default algorithms of unconstrained nonlinear optimization: BFGS and its limited-memory variant L-BFGS sit inside most numerical optimization libraries and most large-scale fitting codes in statistics and machine learning.
The family starts with William C. Davidon's Argonne report ANL-5990 of 1959, Variable Metric Method for Minimization, rejected by a journal in 1957 and published only in 1991 as the first article of the SIAM Journal on Optimization, with a preface by the author (DOI 10.1137/0801001). The report's body describes a flowchart algorithm; its Appendix describes "a simplified method embodying some of the ideas" of that algorithm, in one and a half pages. That simplified method is what is now called the symmetric rank-one (SR1) update, and the Appendix contains its quadratic-termination property: on a quadratic, after at most steps the trial matrix equals the inverse Hessian, and the next step lands at the minimum.
Timeline.
Vectors are elements of and matrices are real . Fix a symmetric positive definite matrix and a point , and let
a quadratic with constant Hessian and minimum point . Its gradient is , display (6) of the Appendix.
The method keeps a point and a symmetric trial matrix , which plays the role of . Write . One iteration is
a full step with no line search followed by a symmetric rank-one update. With the two scalars
footnote 2 of the Appendix fixes the coefficient on a quadratic to , which makes the paper's quality measure of (4) vanish. Write for the step and for the change of gradient. The paper writes , , for the current quantities and , , for the updated ones, and uses the letter both for the number of variables and for the scalar ; here the number of variables is .
If is symmetric and for every , then
This is the sentence after (8) on p. 17: "After no more than steps (for which ), will equal and the following step will be to the exact minimum."
The termination theorem says that on a quadratic the rank-one update recovers the exact inverse Hessian from gradient differences, without line searches and without positive definiteness of the trial matrix, and then takes the Newton step. This is the property that justifies the name "variable metric": the metric converges to the one that makes the problem trivial. The secant equation (8) and the persistence of earlier secant equations (7) are the template for the analysis of every later quasi-Newton update, and the SR1 update remains in use in trust-region methods because it does not force positive definiteness.
The result is classical and its proof is short; what this mission adds is a machine-checked version stated in the paper's own form. In particular the hypothesis is the paper's: only that each of the first coefficients is defined. Textbook statements of SR1 termination often assume in addition that the steps are linearly independent; the paper does not, and the formal goal does not either. No Lean formalization of SR1, DFP or BFGS termination was found in Mathlib or on Prove2Me. On Prove2Me, the related open targets are L-BFGS termination (Nocedal 1980) and conjugate-gradient termination (Hestenes–Stiefel 1952); the definitions here are independent of theirs.
Each update changes by a rank-one term, and nothing in a single step forces to be : the coefficient depends on the current iterate and the update could, a priori, destroy what earlier steps achieved, as general rank-one updates do. The obvious count — steps, conditions — does not by itself give independent conditions on ; the steps produced by the method are not chosen to be independent, and the only hypothesis available is that the denominators are nonzero. The difficulty is to get the full conclusion from that hypothesis alone, without assuming independence, positive definiteness of , or a line search.
Vectors are Fin n → ℝ with 0-based indices, matrices Matrix (Fin n) (Fin n) ℝ; is u ⬝ᵥ (H *ᵥ v) and is vecMulVec (H *ᵥ g) (H *ᵥ g). The definition file DavidonVM.Termination.Method provides quad, grad, Nval, Mval, the run predicate IsRunWith for an arbitrary gradient field and coefficients, and IsQuadRun for the quadratic with ; DavidonVM.Termination.Delta provides the update and the quantity of (4).
Committed conventions, each a reading of something the paper leaves implicit:
A statement of the goal with the extra hypothesis " are linearly independent", or with assumed, would be a weaker theorem than the paper's and is ruled out. The case is trivial; the hypotheses are jointly satisfiable for (checked locally).
Welcome contributions: proofs of the four milestones and the goal; general facts about rank-one updates (determinant and positive definiteness, Sherman–Morrison form of the inverse) that the further statements need and that are reusable for DFP, BFGS and trust-region analyses.
Betweenness centrality measures how much of the communication in a network passes through a node. Freeman's original measure (Freeman 1977) counts the fraction of shortest paths between each pair of nodes that pass through it, and Brandes' algorithm (Brandes 2001) made it computable on large graphs. Variants replace shortest paths by maximum flows (Freeman, Borgatti and White 1991), random walks (Newman 2005) or load-splitting rules (Goh, Kahng and Kim 2001), and group variants measure the traffic that passes through a set of nodes (Everett and Borgatti 1999).
Dolev, Elovici and Puzis (technical report 2009, J. ACM 2010) define routing betweenness centrality (RBC): given the actual routing scheme of a communication network and its traffic matrix, the RBC of a node is the expected number of packets that pass through it. Each of the measures above is a special choice of routing scheme. The application is the placement of traffic monitors: the RBC of an ordered sequence of monitors is the expected number of packets sampled by all of them in order, which measures, for example, redundant inspection along a path.
Let be a finite set of nodes. A routing scheme assigns to every source , current node , next node and target a number , the probability that forwards to a packet with source address and target address . Routing decisions are independent. The scheme is assumed to be
A route from to is a sequence of nodes from to whose every hop has positive forwarding probability; its probability is the product of the hop probabilities. For nodes and a sequence :
A traffic matrix gives the number of packets sent from to , and sampling rates give the fraction of passing packets a monitor at samples. The target dependency is , and the RBC of the sequence of distinct nodes is
For a source-oblivious scheme and a sequence of distinct nodes, ,
The right side is the value returned by the paper's Algorithm 6. The identity contains no running time and no constant: it states the exact equality the algorithm relies on.
The goal reduces the RBC of a sequence of monitors to arithmetic on precomputed single-node quantities, instead of a pass over the routing graph of every source–target pair. This is what makes repeated evaluation of candidate monitor sequences, as in greedy or search-based placement, affordable on large networks. Eqs. (1) and (9) are the recursions behind the paper's algorithms for the RBC of single nodes; Eq. (9) replaces the loop over all source–target pairs by a loop over targets.
The paper's proof of Lemma 1 is an argument about conditional probabilities of informally described events. A formalization fixes what "the probability that a packet passes through " means, as a sum over a finite set of routes, and checks the factorization against that definition, including the corner cases the prose passes over: sequences with repeated nodes, a first node equal to the source or to the target, and the source in the sum over all sources. No machine-checked version of these identities is known.
Dependency chaining is a Markov property: after the packet reaches , its future does not depend on its past. The obvious argument splits every route through into a prefix ending at and a suffix starting there. Two points need care. First, the suffix must be a route of a packet with source , which is where source-obliviousness enters; for source-dependent routing the lemma is false. Second, the prefix probabilities must sum to while the suffix probabilities sum to one, which requires that no packet is lost: this is where totality of the forwarding probabilities and loop-freeness (every walk reaches the target in at most steps) are needed. The passage from Lemma 1 to the goal then requires the sum over all sources, including , where Lemma 1 does not apply.
Nodes form a type V with [Fintype V] [DecidableEq V]; probabilities, traffic and sampling rates are real numbers; sequences are Lean lists, indexed from . Routes are repetition-free lists, and every dependency is a finite sum over them; no infinite sums, suprema or measure theory are used. The definitions file bundles the standing assumptions in IsRoutingScheme and source-obliviousness in IsSourceOblivious.
The paper's probabilities are informal. The following readings are explicit:
Defining by the recursion (3) or the product (16), the target sequence dependency by (17), or the sequence RBC as the sum over targets of the chained product would make the goal true by definition; every dependency here is a sum of route probabilities, and the RBC of a sequence is the double sum of Eq. (4).
The running-time claims of the paper are out of scope. Lemma 2 of the paper (p. 17) is false as printed for a nonempty monitor set and is not posed. Contributions welcome: proofs of the milestones, a general lemma that the total route probability from any node is one under a total loop-free scheme (reusable for absorbing Markov chains on finite DAGs), and the prefix–suffix decomposition of routes.
Training a neural network with nonsmooth activations (ReLU, max-pooling, absolute values) means running a stochastic gradient method in which the "gradient" is whatever the automatic differentiation library returns. For nonsmooth programs that output is in general neither a gradient nor a Clarke subgradient: the chain rule fails for the Clarke subdifferential, and the same function written in two ways can receive two different derivatives at the same point. Bolte and Pauwels (TSE Working Paper 1044, 2019; published in Mathematical Programming, 2021) introduced conservative set-valued fields as a class of generalized derivatives that is closed under the operations automatic differentiation performs and still carries enough information to analyse descent methods.
The framework is used in the analysis of nonsmooth automatic differentiation and of stochastic subgradient methods in machine learning (for instance Bolte and Pauwels, NeurIPS 2020). The present mission formalizes the first structural theorem of the theory.
Write for Euclidean space with inner product . A set-valued map assigns to each a subset ; it has closed graph if is closed in . A path is absolutely continuous if it is differentiable almost everywhere and ; it is a loop if .
Definition 1. is a conservative field if it has closed graph, nonempty compact values, and for every absolutely continuous loop
The integrand is Lebesgue measurable (Lemma 1), so the condition is that circulations along loops vanish, as for gradient fields in classical vector calculus, but with a maximum over the set in place of a single vector.
Definition 2. A function is a potential for (and is a conservative field for ) if for every and every absolutely continuous path from to
Examples: the gradient of a function; the Clarke subdifferential of a semialgebraic locally Lipschitz function; the output of forward or reverse mode automatic differentiation on a program built from definable elementary functions (the subject of the companion mission in this series).
If is a conservative field and a (locally Lipschitz continuous) potential for , then for Lebesgue-almost every , is differentiable at and
The result. Theorem 1 says that a conservative field, although set-valued and possibly far from any subdifferential, differs from the gradient of its potential only on a Lebesgue-null set. Several consequences in the paper rest on it: the Clarke subdifferential of is contained in the convex hull of every conservative field for , so it is the minimal convex-valued conservative field (Corollary 1), and a Fermat rule at local extrema of (Proposition 1). Combined with the companion result that automatic differentiation produces conservative fields, it implies that the derivatives returned by automatic differentiation agree with the gradient outside a Lebesgue-null set.
Formalizing it. The theorem is proved in the paper; this mission formalizes the known proof. No conservative-field calculus exists in Mathlib or on the platform. The mission produces the definitions of conservative fields and potentials in Lean, a measurability result for marginal functions of closed-graph set-valued maps along absolutely continuous paths, and an almost-everywhere identification of measurable selections with gradients that can be reused for other "derivative equals selection almost everywhere" statements.
The obvious argument runs: is locally Lipschitz, hence differentiable almost everywhere by Rademacher's theorem, and at a point of differentiability must be . The second step fails. Conservativity is an integral condition along curves, and it says nothing about the value of at an individual point of differentiability; a pointwise argument cannot exclude extra elements of . The identification therefore holds only almost everywhere and has to be extracted from integral information, which brings in three ingredients absent from Mathlib: measurability of for closed-graph compact-valued maps with no local boundedness assumption; measurable selections of such maps, including a countable family dense in every value (a Castaing representation); and, for Remark 3(d), the local boundedness of conservative fields (Borwein, Moors and Wang). Passing from "almost every point of every line" to "almost every point of " also requires measurability of the exceptional set, which is not automatic.
is EuclideanSpace ℝ (Fin p), Lebesgue measure is volume, and a set-valued map is EuclideanSpace ℝ (Fin p) → Set (EuclideanSpace ℝ (Fin p)). A path is a function ℝ → ℝ^p satisfying AbsolutelyContinuousOnInterval γ 0 1 (Mathlib's – definition on , equivalent there to the paper's); its values outside are irrelevant and is deriv γ. The maximum and minimum over are sSup and sInf of the image of a nonempty compact set, hence attained.
Since Lean's integral of a non-integrable function is , Definitions 1 and 2 require the circulation to be integrable in addition to having the stated integral; without this conjunct every field with non-integrable circulations would count as conservative, which is a trivializing reading excluded here. Likewise "" is formalized as differentiability of at together with set equality , because Lean's gradient is where is not differentiable. Definition 2 is the paper's form (2) with base point ; the min-form and the forms (3)–(4) are consequences, not definitions. Measurable selections appear as hypotheses (Borel measurable with ); their existence is not claimed by any milestone. The local Lipschitz hypothesis of Theorem 1 is kept as printed, and local (not global) Lipschitz continuity is used throughout.
Theorem numbers and pages refer to the TSE Working Paper 1044 version (October 2019), not to the Mathematical Programming typesetting.
Welcome contributions: a Castaing representation / Kuratowski–Ryll-Nardzewski selection theorem for closed-graph compact-valued maps on ; Rademacher's theorem for locally Lipschitz functions; Fubini-type "null on every line implies null" lemmas on EuclideanSpace; the fundamental theorem of calculus for absolutely continuous vector-valued paths.
Bounded-confidence opinion dynamics model a population in which each agent repeatedly moves its opinion towards the opinions of those agents whose views lie within a fixed distance of its own. Introduced in discrete time by Krause (1997) and studied as the Hegselmann–Krause model, these systems are a standard test case for multi-agent coordination with state-dependent communication: who talks to whom depends on the current state, so the interaction graph changes over time and the linear consensus theory does not apply. Simulations show that opinions settle into clusters that are further apart than the confidence radius, and that the distances between clusters are larger than the radius would force. Explaining those distances is a long-standing question in the area (Lorenz 2007).
Blondel, Hendrickx and Tsitsiklis (SIAM J. Control Optim. 2010) study the continuous-time version, first for finitely many agents and then for a continuum of agents. The continuum model is the limit of a large population and captures the intercluster distances observed in simulations. This mission formalizes the continuum part of the paper, Section 3: well-posedness for regular initial opinions, convergence to clusters, and the intercluster distance bound of Theorem 6.
Agents are indexed by with Lebesgue measure. An opinion function gives the opinion of agent . Write for the bounded measurable opinion functions and for the nondecreasing bounded ones. For , is the set of whose increase rate is at least for all , and the set with rate at most . A function is regular if it lies in for some ; the uniform profile is regular.
Two agents are connected when their opinions differ by less than . The interaction operator is
Given an initial condition , a solution of (3.2) is a measurable , , with each and
The differential form (3.1) is .
is the set of nondecreasing whose distinct values are pairwise more than apart; the set of nondecreasing whose values, for almost every pair of agents, are equal or at least apart. A fixed point is an for which (3.2) started at has the unique solution . A cluster of is a value held by a set of agents of positive measure , its weight.
For a regular , a solution of (3.2), and almost everywhere: any two distinct clusters of satisfy
and agrees almost everywhere with a member of that is a fixed point.
Theorem 6 turns the qualitative picture "opinions freeze into clusters at least one unit apart", which already follows from Theorem 5, into a quantitative statement depending on the cluster weights: two clusters of equal weight are at least apart, and a light cluster can sit closer to a heavy one. This matches the intercluster distances observed in simulations of large populations and yields Corollary 1 of the paper, a necessary condition for the stability of an equilibrium in the sense. Theorem 4 is of independent interest: the right-hand side of (3.1) is discontinuous in the state, a two-valued initial profile admits two different solutions, and well-posedness holds only under the slope bounds.
The results are proved in the paper. Nothing in this mission has a machine-checked proof yet. Formalizing it means building a small theory of integral equations with a state-dependent, discontinuous kernel on -type spaces of opinion profiles: a contraction argument on short intervals, its continuation, monotone convergence of partial integrals, and an a.e. limit argument with Fatou's lemma and Fubini.
The obvious route to Theorem 4, Picard–Lindelöf, fails: is not Lipschitz on , because a small perturbation of opinions can switch the connection indicator on a set of positive measure. Lemma 1 restores the Lipschitz property only at functions with a positive increase rate, so existence and uniqueness require a contraction on a carefully chosen set of profiles together with a proof that the dynamics keep the increase rate positive (Lemma 2), and a continuation argument whose step size shrinks as the lower slope decays. For Theorem 6, convergence alone gives only ; the extra term comes from agents trapped between two clusters, whose existence relies on the continuity in of every , which the a.e. limit does not have.
Opinion functions are ℝ → ℝ, and only their values on Set.Icc 0 1 matter; a trajectory is x : ℝ → ℝ → ℝ with x t α , time real with . Lebesgue measure on is volume.restrict (Set.Icc 0 1), and uses its product measure. The slope conditions are written multiplied out for . Explicit readings of the paper's phrases:
Tendsto … atTop (𝓝 l) to a real limit; "except possibly for a countable set": a countable exceptional set; "a.e.": almost everywhere for Lebesgue measure on .A trivializing formalization is ruled out: clusters are distinct with positive weight, regularity requires a positive lower slope, the solution predicate forbids the junk value of a non-integrable time integral, and is checked to be regular, so no hypothesis is vacuous.
The development needs an integral-equation solution theory for a discontinuous kernel, the Banach fixed point theorem (Mathlib ContractingWith), Grönwall-type estimates, countability of discontinuities of monotone functions, Fatou's lemma and Fubini. Lemmas 1 and 2 and the lower bound in Theorem 4 are reused by the companion mission on the discrete-to-continuum approximation (Theorem 7). Contributions are welcome on every milestone, and in particular on the slope estimates, which are self-contained.
Many problems in statistical learning, signal processing and distributed optimization minimize a sum of a large number of convex components over a convex set: a data-fit term per sample plus a regularizer or constraint per sample. When is large, a method that processes one component per iteration is often far cheaper per step than one that evaluates the whole sum. Incremental methods do exactly this. The incremental subgradient method of Nedić and Bertsekas (SIAM J. Optim., 2001) takes a subgradient step on one component at a time; the incremental proximal method replaces some of these steps by proximal steps, which are more stable and are cheap when a component has a closed-form proximal map (an term, an indicator of a simple set).
Bertsekas, Incremental Proximal Methods for Large Scale Convex Optimization (Report LIDS-P-2847, MIT, 2010, revised 2011; Math. Program. 129 (2011), doi:10.1007/s10107-011-0472-0), combines the two: each component is split as , with a proximal step on and a subgradient step on , followed by a projection. The paper analyzes two ways of choosing the component at each iteration, a fixed cyclic order and a randomized order. This mission covers the randomized order (§4 of the paper); its companion mission covers the cyclic order.
Let be a nonempty closed convex set and let , , be convex. The problem is
with optimal value , possibly , and optimal set , possibly empty. is the Euclidean projection on and a subgradient of at .
At iteration a component index is drawn and, with stepsize , one of three updates is applied:
The implicit equations are proximal steps: in (42), minimizes over . The randomized order means that is uniformly distributed over and independent of the past history (Assumptions 3(a), 4(a)). The growth conditions (Assumptions 3(b), 4(b)) ask for a constant bounding, with probability 1 and for every component , the norms of the subgradients used by the step that would be taken if were , and the decrease of , along that step by times its length.
If and , then
and if in addition and , then with probability 1 the iterates converge to some (which may depend on the sample path).
Proposition 9 says that a randomized incremental method with a diminishing stepsize solves the problem exactly, almost surely, under conditions that do not require differentiability, bounded level sets, or strong convexity. Propositions 7 and 8 quantify the constant-stepsize regime: the error bound is , smaller by a factor of than the worst case of the cyclic order (Proposition 4 of the paper). This is the paper's argument for randomization, and the same comparison recurs in the later literature on stochastic and incremental methods.
The results are proved in the paper. As far as known, none of them is machine-checked: Mathlib has conditional expectation, filtrations and Doob's martingale convergence theorem, but not the Robbins–Siegmund almost-supermartingale theorem in the form used here, and no incremental or stochastic proximal method has a formal convergence proof on the platform. The mission produces a formal model of a randomized algorithm with implicit (proximal) steps, a formal Robbins–Siegmund special case, and a complete a.s. convergence proof that other stochastic-approximation formalizations can reuse.
The deterministic estimate behind (58) is the one of the cyclic analysis with the sampled component in place of the cyclic one. The new difficulty is the conditioning step: needs the step that would be taken for each component to be a function of the past, and to be independent of it, and both must be stated so that the conditional expectation is that of an integrable function. The obvious route from (59) to part 2 of the goal fails: (59) gives, for each , an event of probability 1, and is in general uncountable, so the events cannot be intersected directly. Part 1 must also handle , where no point of is available.
EuclideanSpace ℝ (Fin n); components are indexed by Fin m (), with .EReal, so is represented and the and statements are in EReal.A formalization in which the would-be steps may depend on , or in which is only assumed uniform, would let a step pick its component adversarially; the measurability and independence hypotheses rule this out, and none of the hypotheses is unsatisfiable (a sorry-free instance with is checked locally).
Needed infrastructure: the Robbins–Siegmund special case (Proposition 2), conditional expectation of a function of an independent uniform index and a past-measurable quantity, and existence of a countable dense subset of a closed set in . The supermartingale theorem and the conditioning lemma are reusable beyond this mission. Proofs of the milestones, of the goal, and of reusable lemmas about projections and proximal steps are welcome.
Bounded-confidence opinion dynamics model a population in which each individual revises an opinion, represented by a real number, by looking only at opinions close to its own. The best-known example is the discrete-time model of Krause (1997), also called the Hegselmann–Krause model, in which every agent moves to the average of the opinions within distance 1 of its own. Such models are studied in the social sciences as models of consensus formation and polarization, and in control theory as prototypes of multiagent systems with state-dependent interaction topology: the communication graph is not given in advance but is determined by the state itself, which is what rendezvous algorithms for mobile robots and flocking models share (Lorenz 2007; Olfati-Saber, Fax, Murray 2007).
Blondel, Hendrickx and Tsitsiklis (SIAM J. Control Optim. 48 (2010)) study the continuous-time, symmetric counterpart of Krause's model. Each opinion is continuously attracted by every other opinion differing from it by less than 1, with an intensity proportional to the difference. Simulations show convergence to clusters, groups of agents sharing a common value, with distinct clusters at distance at least 1 and typically close to 2. This mission formalizes the first of the paper's results: convergence to clusters at least 1 apart for finitely many agents.
Timeline.
There are agents, labelled . Agent holds a real opinion at each time , and is a continuous function of time. Agent is a neighbour of agent at time when ; the inequality is strict, and every agent is its own neighbour. The intended dynamics are
The right-hand side jumps whenever a pair of opinions crosses distance 1, so (1.1) usually has no differentiable solution. The model is therefore the integral equation
Solutions of (2.1) need not be unique. The two-agent initial condition is a fixed point, but the agents can also start attracting each other immediately. An initial condition is proper if (a) (2.1) has exactly one solution with ; (b) the set of times at which is not differentiable is at most countable and has no accumulation point; and (c) agents that meet stay together: implies for all . That solution is then a proper solution.
The set of equilibria is
The average opinion is , and is the sum of squared differences from it.
Every proper solution of (2.1) converges to a limit in :
that is, all limits exist and two agents with different limits end at distance at least 1.
The result. Theorem 2 establishes the clustering behaviour seen in simulations for every proper solution. The paper's Theorem 1 states that almost every initial condition is proper, so the conclusion covers almost every initial condition. The lower bound 1 on the distance between clusters is the baseline that the paper's continuum analysis improves to . Average preservation and the decrease of (Proposition 1) are the structural facts that the continuum model also has.
Formalization. Theorem 2 is proved in the paper; no machine-checked version exists on Prove2Me or, as far as is known, elsewhere. The mission produces a Lean definition of solutions of a discontinuous integral equation with a state-dependent neighbour graph, and a convergence proof for it. The remaining work is to formalize the known argument, from the integral equation to the existence and location of the limit.
The obvious approach treats (1.1) as an ODE and differentiates along trajectories. That fails because the right-hand side is discontinuous in the state. A solution is only an integral solution, it may fail to be differentiable, and derivative identities such as (2.3) hold only outside an exceptional set of times. Every step from a derivative sign to a monotonicity or limit statement therefore has to go through the integral equation, not the differential one. A second obstacle is that pairs of agents at distance exactly 1 sit on the discontinuity of the interaction rule. This is where uniqueness fails (footnote 3 of the paper) and why conditions (a)–(c) are hypotheses. A decreasing Lyapunov function alone does not give convergence of the trajectory to a single point, so Proposition 1 does not by itself settle Theorem 2.
Agents are Fin n. Time is ℝ, and only values at enter. A trajectory is x : ℝ → Fin n → ℝ. A solution of (2.1) is continuous on and satisfies (2.1) for every and every , with the neighbour set Finset.univ.filter (fun j => |x τ i - x τ j| < 1). The integrand is also required to be interval-integrable on ; for a continuous trajectory this always holds. Explicit readings of the paper's phrases:
Tendsto x atTop (𝓝 xstar) in Fin n → ℝ, with real time;The paper's sortedness convention ("we assume … that the components of proper initial conditions are sorted") is a hypothesis only of the partial-sum milestone. Theorem 2 is stated for every proper solution. A formalization that dropped condition (a), restricted solutions to sorted, differentiable or eventually constant trajectories, or replaced (2.1) by the differential equation would prove a different, and in parts trivial, statement. These are excluded.
The work needs interval integrals and the fundamental theorem of calculus for integrands with jumps, monotonicity from almost-everywhere derivative signs, and bounded monotone convergence. The definition of solutions of (2.1) and the equilibrium set is reusable for the stability results of the same paper (Theorem 3), which are not part of this mission. Contributions are welcome at every milestone, as are alternative convergence proofs, such as the paper's reference [9], that avoid symmetry.
Online covering models decisions that must be made as requirements arrive. A planner knows the cost of each available resource, but learns the requirements one at a time and cannot undo an allocation already made. This occurs, for example, when requests for network service or elements needing coverage appear over time. The central question is how much more an online fractional allocation can cost than a best allocation chosen after all requirements are known. Buchbinder and Naor study this question through a paired covering and packing linear program and give an online scheme for arbitrary nonnegative constraint coefficients, not only incidence coefficients in (Buchbinder and Naor, 2009, §§2–4).
The result targeted here is Theorem 4.1 of that paper. It concerns the fractional covering scheme of §4, before the separate extension to box constraints in §4.1. The theorem is a statement about the particular phased scheme, so the scheme's state and update rule form part of the mathematical setting. The online requirement also matters: after each new constraint, earlier allocations remain in force (Buchbinder and Naor, 2009, pp. 4, 8).
Let be a finite nonempty set of primal variables and let index constraints in arrival order. The known cost of variable is . Constraint has coefficient for variable ; when it arrives, the online algorithm learns its coefficients. The normalized offline covering problem minimizes over subject to for every constraint considered. Its packing dual maximizes over subject to for each . The finite data and sign conventions are those of Figure 1 (Buchbinder and Naor, 2009, pp. 3–4).
The scheme accepts a parameter and asks for coverage only to . It maintains a sequence of phases. The first phase bound is times the least ratio among the positive coefficients of the first constraint. The bound doubles at a restart. Within a phase, the vector begins at zero, the initial primal allocation is , and the allocation subsequently follows the exponential expression on page 8. The current phase may need to process constraints already seen in earlier phases. Old phase vectors are retained: the actual online allocation is the coordinatewise maximum of the current and all finished phase vectors. Thus resetting a phase does not retract an earlier allocation (Buchbinder and Naor, 2009, p. 8).
For every nonempty arrival prefix of length , a run of the phased scheme exists. Every completed run has output satisfying
and, for every nonnegative offline comparison vector satisfying for each ,
The paper states the ratio as . Its closing display on page 9 yields the explicit factor used here. The benchmark uses the unscaled covering constraints of Figure 1; replacing them with constraints at would change the guarantee (Buchbinder and Naor, 2009, Theorem 4.1 and proof, pp. 8–9).
The milestone list follows the four claims printed under Theorem 4.1. A finished phase has dual objective at least ; every phase dual vector satisfies the packing constraints; the sum of phase primal costs through the current phase is less than ; and the actual allocation covers every arrived constraint to . These are statements about the phase records of the scheme, including a partly processed round that ends in a restart (Buchbinder and Naor, 2009, pp. 8–9).
The theorem gives a cost guarantee for a general online covering problem while allowing arbitrary nonnegative coefficients. It separates the cost paid by an allocation from the level of coverage requested through . Its four claims identify the quantities that make the guarantee meaningful: the dual vector certifies a lower bound for an offline comparison, the phase costs control the online expenditure, and the output remains feasible as constraints arrive. The same primal–dual setting is used elsewhere in the paper for online packing and for applications of covering and packing methods (Buchbinder and Naor, 2009, §§3–5).
The paper proves Theorem 4.1. This mission asks for a machine-checked account of the known result and of the scheme to which it applies. A published formal restatement, OnlinePrimalDual.GeneralPacking.theorem14_3, already gives a ratio conclusion under an assumed ratio bound and an assumed weak-duality inequality; those hypotheses contain the main work needed here. The present goal instead quantifies over runs generated by the update rule and asks both that a run exists and that all such runs satisfy the guarantees. The published general instance definition is reused, so the finite covering and packing data have a shared interface.
An online allocation cannot be evaluated solely from its final vector. A phase restart resets the working dual vector and restarts the constraint scan, while allocations from completed phases still affect the actual output. A statement about arbitrary vectors with a presumed cost bound would leave out this behavior. The continuous update also requires a precise stopping event when coverage or the phase cost reaches its threshold. The cost guarantee is sensitive to which condition wins if both occur together, and to whether a phase can restart indefinitely. Those details must be represented before any claim about completed phases has the paper's meaning (Buchbinder and Naor, 2009, pp. 8–9).
Lean uses OnlinePrimalDual.GeneralPacking.GeneralInstance I (Fin m) for the coefficient matrix and costs. A nonempty finite type represents the primal variables; Fin m supplies the ordered constraints. The theorem assumes , , and a positive coefficient in every constraint. The last condition makes each arriving constraint coverable and makes the first ratio minimum nonempty; zero coefficients are omitted from that minimum. The paper treats infeasible all-zero rows implicitly. The minimum is over a finite nonempty set, so the real infimum in the Lean definition equals the ordinary minimum. All sums are finite and all logarithms are natural.
The run is an event relation with three events: arrival of one new constraint after all known constraints have been processed, completion of a covered round at its first stopping time, and restart at the cost cap while coverage remains deficient. A restart doubles , records the old phase, resets the dual variables, and resumes at the first known constraint. The state records the current phase and all finished phases; the output takes their coordinatewise maximum. A simultaneous coverage and cost event counts as covered. Reaching the cost cap models the continuous stopping time behind the paper's wording that the cost “exceeds” the bound. The theorem asserts run existence, so a ratio claim cannot hold merely because the run relation has no witness.
The explicit instantiation in this mission is , from the page 9 closing display. The first-phase case is bounded there by times the optimum and is included in the same stated coefficient. The comparison vector must satisfy the original level-one constraints. Theorem 4.2, which adds upper bounds on variables and appears in §4.1, is outside this mission. The run definition, phase-cost and coverage functions, and the four claims are reusable infrastructure for later work on continuous online primal–dual schemes.
Many optimization problems in machine learning, signal processing and distributed computation have an objective that is a sum of a large number of component functions: one per data point, per sensor, or per processor. Evaluating the whole sum, or a subgradient of it, at every iteration is expensive when is large. Incremental methods process one component at a time, cycling through the components or sampling them, and update the iterate after each one. Incremental gradient and subgradient methods go back to the training of neural networks and to least squares; incremental proximal methods replace the subgradient step of a component by a proximal step, which is more stable and handles nonsmooth terms exactly.
Bertsekas (LIDS-P-2847, 2010, rev. 2011; Math. Program. 129 (2011)) proposed a unified family that mixes the two: each component is split as , a proximal step is taken on and a subgradient step on , followed by a projection onto the constraint set. This mission formalizes the convergence analysis of that family under the cyclic order of component selection.
Timeline. Incremental subgradient methods were analysed by Nedić and Bertsekas (SIAM J. Optim. 12 (2001)) for cyclic and randomized orders. Incremental proximal methods were studied by Bertsekas (Optimization for Machine Learning, 2011, ch. 4). The 2011 paper combines the two analyses; its cyclic-order results are Propositions 3–6.
Let carry the Euclidean norm and inner product . The data are a nonempty closed convex set and real-valued convex functions , . The problem is
with optimal value , possibly , and optimal set , possibly empty.
A subgradient of a convex at is a vector with for all ; is the point of nearest to . At iteration one component is processed with stepsize . The three iterations are
The -subgradient is taken at the new point, which makes the -part a proximal step (Proposition 1). In the cyclic order ; a block of consecutive iterations is a cycle, and is constant within a cycle.
The analysis assumes that the subgradients the iteration uses are bounded by a constant and that, at each cycle start , the function values at the intermediate points of the cycle differ from those at by at most times the distance (Assumption 1 for (19), (20); Assumption 2 for (21)). Both hold, for example, when all , are polyhedral or Lipschitz.
If and , then
and if moreover and , then for some . Both parts are one item, as in the paper.
Proposition 6 is the exact-convergence guarantee for the cyclic incremental subgradient-proximal methods: with a diminishing, non-summable stepsize they reach the optimal value whatever the starting point, and with square-summable stepsizes the iterates converge to a single optimal solution. It covers the pure incremental subgradient method () and the pure incremental proximal method () as special cases, and it is the template for the randomized-order analysis of the companion mission. Proposition 4 quantifies what a constant stepsize achieves.
These results are proved in the paper. None of them, nor the underlying estimates, is formalized on the platform or, to our knowledge, in Mathlib. The mission produces machine-checked versions of the proximal-step lemma for extended-real-valued functions on a constrained set, of the cycle estimate (27) with its explicit constants, and of the deterministic supermartingale convergence lemma, all reusable for other incremental and proximal methods.
The obvious argument treats one cycle as one step of a subgradient method on . It fails because within a cycle the subgradients are taken at the intermediate points or , not at , and the proximal steps use subgradients at the points they produce. The error between and at those points must be controlled through the drift of the iterates during the cycle, and the bookkeeping differs between (19)/(20) and (21), which is why differs. For the second part of Proposition 6, convergence of the values in the sense does not by itself give convergence of the iterates, and may contain more than one point.
EuclideanSpace ℝ (Fin n). Components are Fin m (0-based), so is k % m, and the paper's with becomes with z (k + j). is assumed (NeZero m).IsProj: a nearest point of ), not a choice function.Step between , , and the two subgradients it uses, with the -subgradient at the point the paper names. A run records these subgradients, so Assumptions 1–2 bound exactly them. The assumptions are not replaced by Lipschitz continuity, which is only a sufficient condition (p. 9).EReal; is allowed and no boundedness is assumed.MoreauProx.Characterization.GammaZero) and its subgradients, with relative interiors as Mathlib's intrinsicInterior.The goal cannot be satisfied vacuously: a sorry-free check confirms that the hypotheses hold together (for , , , , ). Restricting to Lipschitz components, to bounded-below , or to would state a weaker theorem and is ruled out.
Proofs of any item are welcome, as are general lemmas (the projection theorem as a variational inequality, the subdifferential sum rule under the relative-interior condition) that the proofs need.
Classical scheduling theory optimizes one objective for one decision maker. Many shop floors are shared: two departments, two customers or two firms submit jobs to the same machine, and each cares only about how its own jobs are treated. Agnetis, Mirchandani, Pacciarelli and Pacifici, Scheduling Problems with Two Competing Agents (Operations Research 52(2), 2004), set up this two-agent scheduling model and classified the complexity of its single-machine cases for the standard objectives (maximum of regular cost functions, number of late jobs, total weighted completion time). The paper started a line of research on multi-agent scheduling; its notation is the standard one in that literature.
This mission covers the paper's first case, §4: both agents measure a schedule by the largest cost among their own jobs. It is the case with a polynomial greedy algorithm, and it serves as the template for the paper's other cases.
Agent A owns jobs and agent B owns jobs . Each job has a processing time ; all jobs are available at time . A schedule is an ordering of all jobs, processed on one machine one after another from time without idle time, so the completion time is the sum of the processing times of and the jobs before it. Each A-job has a nondecreasing cost function and each B-job a nondecreasing (the costs are regular). The two objectives are
The constrained optimization problem asks for a schedule minimizing among those with (the feasible schedules). A schedule is nondominated if no schedule has and with one inequality strict.
The backward rule of §4 builds a schedule from the end. With the set of unscheduled jobs and the time at which the next job placed will end, it places last any unscheduled B-job with ; if there is none, it places last an unscheduled A-job of least ; if neither exists, it stops and declares the instance infeasible.
The paper justifies the rule by a reduction to Lawler's single-agent problem (Lawler 1973): every job gets one cost with values in , equal to for A-jobs, to for a B-job meeting the bound at time and to for one violating it.
Both parts hold for every tie-breaking. The printed theorem states a running time ; only the correctness half is a target.
The theorem shows that the two-agent problem with maximum-cost objectives is no harder than its single-agent counterpart: a greedy rule that gives priority to any B-job still within budget and otherwise serves agent A's cheapest job is optimal. Theorem 4.2 turns this into a point of the Pareto frontier with one more optimization, without the binary search over that §3 of the paper describes for the general case. In §11 the paper enumerates nondominated pairs by repeatedly solving the constrained problem, and §11.1 bounds their number for this case.
None of these results has a machine-checked proof that we know of. The single-agent theorem of Lawler is the subject of the published Prove2Me statement LawlerPrec.MinMax.lawler_rule_optimal, which is open; its costs are real-valued, so it does not apply directly to the costs of the reduction. This mission's results are self-contained and can be proved either through such a generalization or directly.
The rule is nondeterministic: any eligible B-job may be chosen, and ties among A-jobs are broken arbitrarily, so the optimality claim is about every possible output, not one canonical sequence. Lawler's exchange argument has to be carried through the extended-real costs, where a B-job's cost jumps from to at its deadline, and the ordering by B-first priority has to be shown to be one of Lawler's least-cost choices. The completeness half needs that a stuck state (no A-job left and every remaining B-job over budget at ) rules out every schedule, not just the rule's.
Fin nA ⊕ Fin nB (Sum.inl h is , Sum.inr k is , 0-based). Schedules and completion times reuse the published definition MooreLateJobs.Shared.completionTime (Moore 1968): a duplicate-free list containing every job, processed from time without idle time.IsBackwardRuleSeq): at every position of the sequence, with the jobs at positions and the completion time at position , the job there is an eligible B-job if one exists in , and otherwise an A-job of least in . "Ties are broken arbitrarily" means the property admits every choice. "The rule stops" means no sequence through that state has the property, so "the rule completes" is the existence of a complete sequence with the property.EReal with only maximum and order; "1|prec|f_max" is taken with the empty precedence relation. "Finite objective value" means the minimum is a real number.The definitions (two-agent model, maximum costs, constrained problem, nondominance) are reusable by the rest of this series. Proofs of the milestones, and a generalization of Lawler's theorem to extended-real costs, are welcome.
Balanced truncation is the standard method for reducing the state dimension of a linear control system while keeping its input–output behaviour: states that are both hard to reach and hard to observe are discarded. Its justification rests on two Gramians, the solutions and of a pair of Lyapunov equations, whose quadratic forms measure how much input energy a state costs to reach and how much output energy it produces. For linear systems the facts are classical: the image of the controllability Gramian is the reachable subspace, and the kernel of the observability Gramian is the unobservable subspace.
Bilinear systems, in which the input multiplies the state, are the simplest nonlinear extension of linear control systems. Their generalized Lyapunov equations have the same form as the Lyapunov equations of linear stochastic systems with multiplicative noise, which is why Benner and Damm treat the two classes together. Balanced truncation was extended to them using the solutions of generalized Lyapunov equations (Al-Baiyat and Bettayeb, 1993; Gray and Mesko, 1998, both as cited by Benner and Damm). Benner and Damm, in Lyapunov Equations, Energy Functionals, and Model Order Reduction of Bilinear and Stochastic Systems (SIAM J. Control Optim. 49(2), 2011, doi:10.1137/09075041X), examine which of the linear-system energy interpretations survive for bilinear systems. Their Theorem 3.1 is the structural result that does survive: the kernels of the Gramians still identify states that are unreachable from the origin and states that produce no output, so these states can be eliminated without changing the transfer behaviour.
Fix and real matrices , , . The bilinear control system (3.1)–(3.2) is
with state , input and output . The homogeneous system (3.5) drops the term : , . The same indexes the bilinear terms and the columns of . Write for a solution with input and initial state , and .
An admissible input is a function that is integrable on every interval . A solution with is a continuous satisfying
The generalized Lyapunov equations (3.6) are
A solution of the first is a controllability Gramian and a solution of the second an observability Gramian. "" means is symmetric nonnegative definite; and are its image and kernel.
(a) If solves the first equation of (3.6), then for every admissible input
(b) If solves the second equation of (3.6) and , then for the homogeneous system (3.5) and every admissible input
The result. Part (a) says that a state outside cannot be reached from the origin by any input, so its controllability energy is infinite; part (b) says that a state in is indistinguishable from the origin at the output, so its observability energy is zero. Together they justify the first step of balanced truncation for bilinear systems (Remark 3.2 of the paper): the system can be restricted to and projected along without changing its input–output map, after which the Gramians are nonsingular and can be balanced. The theorem needs neither stability of nor uniqueness of the Gramians, so it applies to every nonnegative definite solution of (3.6). The rest of §3 of the paper shows that the finer, quantitative energy estimates of the linear case fail for bilinear systems; this qualitative statement is what remains exact.
Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof yields a reusable invariance principle: a subspace that is invariant under every vector field is invariant under the flow of the input-driven system, for merely integrable inputs. It also yields the linear-algebra lemmas relating kernels of nonnegative definite solutions of generalized Lyapunov equations to the system matrices, which are used throughout model reduction and stochastic stability theory.
The algebraic part (milestones 1, 2, 4) rests on the fact that for a nonnegative definite matrix , forces , applied to the terms of the Lyapunov equation tested against a kernel vector. The passage from the vector field to trajectories is where care is needed. The paper's sentence " whenever , so is invariant" is not by itself an argument: tangency of a vector field to a subspace implies invariance only together with a uniqueness or Gronwall-type estimate, and here the field depends on time through an input that is only integrable, so is merely absolutely continuous and exists only almost everywhere. A pointwise "the derivative points into the subspace" argument therefore does not apply as stated, and the step needs an estimate on the component of orthogonal to the subspace.
The Lean development uses states Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the matrix–vector product *ᵥ, and indices as Fin m. and are LinearMap.range and LinearMap.ker of Matrix.toLin' P; "" is Matrix.PosSemidef, which includes symmetry. Admissible inputs are integrable on every (this contains , the input space of the paper's energy functionals). A solution is a function continuous on whose integrand is integrable on every and which satisfies the integral equation for all ; no uniqueness of solutions is presupposed, and the theorem is asserted for every such solution.
Two reading decisions are fixed. First, part (b) is stated for every admissible input , not only for as printed in the theorem: the paper's proof concludes " for all , implying ", and the theorem's clause "i.e., " (with a maximum over inputs) needs this form. The statement contains the printed one. Second, the clauses "i.e., " and "i.e., ", which restate the conclusions through the energy functionals (3.3)–(3.4), are not formalized.
The statements must not be trivialized: assuming positive definite makes (a) empty (), assuming stable or the Gramians unique adds hypotheses the paper does not have, and a solution notion requiring trajectories for integrable inputs would make the solution set empty. None of these is used. A local check confirms the hypotheses have content: for , , , the matrix is a nonnegative definite solution of (3.6) with .
A complete development needs Mathlib's facts on nonnegative definite matrices, interval integrals of vector-valued functions, and a Gronwall inequality with an integrable coefficient. The flow-invariance lemma for input-driven linear-in-state systems is reusable beyond this mission. Contributions welcome: proofs of the five milestones, and the passage from vector-field invariance to trajectory invariance.