Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The shortest-path problem in a graph of convex sets (SPP in GCS), introduced by Marcucci, Umenberger, Parrilo and Tedrake (arXiv:2101.11565, SIAM J. Optim. 2024), asks for a path through a directed graph whose vertices carry convex sets, together with a point in each visited set, minimizing a sum of convex edge lengths. It models motion planning around obstacles, hybrid-system control and other problems that mix a discrete choice with continuous positions. The paper formulates it as a mixed-integer convex program whose only nonconvexity, before relaxation, is a family of bilinear equalities that couple the continuous positions with the flow variables .
Section 7 of the paper studies the convex relaxation used for these bilinear equalities in isolation. Products of valid inequalities linearized by are the idea behind the McCormick envelope (McCormick 1976) and the Reformulation-Linearization Technique of Sherali and Adams. This mission formalizes the paper's result that the relaxation is exact at every extreme point of the polytope , which is the property that makes the mixed-integer formulation exact at binary flows.
Fix and . Points of are written .
Always , and is convex.
Let be compact and convex, let be a polytope and let be an extreme point of . Then for all and ,
The result. In the paper's mixed-integer program each vertex contributes a bilinear set in which is the convex set at and is the polytope of flows on the edges at . Binary flows corresponding to a path are extreme points of these polytopes, so Lemma 7.4 says that replacing by loses nothing at the integer points of the program. This gives the paper's second, geometric proof that its mixed-integer convex formulation is exact (Theorem 5.7). By Remark 7.5 the lemma also extends a known property of the first-level Reformulation-Linearization Technique for bilinear programs with binary variables from polytopes to compact convex sets . Proposition 7.1 is what makes the relaxation finite: it replaces the infinitely many inequalities of by one perspective-cone constraint per facet of .
Formalizing it. The results are proved on paper; none of them has a machine-checked proof. The formalization also settles the exact hypotheses. Three statements of this section are false as printed (see Formalization scope), and the corrected versions are posed here with the counterexamples recorded. The perspective cone, the cone of valid inequalities and their duality (Lemma 4.9) are general convex-analysis facts that recur across conic and disjunctive programming.
The direction is one line, since . The converse at needs three ingredients that are each standard and none of which is in Mathlib in this form.
Proposition 7.1 as an equality needs an affine Farkas lemma, and its printed proof skips the case of the valid inequality .
is Fin n → ℝ, inner products are dotProduct, is Z *ᵥ c and is Matrix.vecMulVec x y. Triples are (x, y, Z) in (Fin n → ℝ) × (Fin m → ℝ) × Matrix (Fin n) (Fin m) ℝ. A polytope is given by a finite family (c i, d i) over a Fintype index and the hypothesis Bornology.IsBounded; extreme points are Mathlib's Set.extremePoints ℝ, never a predicate defined through active constraints. The dual cone uses the pairing on the product, not an inner product.
Hypotheses added relative to the page, each with a counterexample to the printed form:
Several hypotheses are dropped where they are not needed, which strengthens the statements: nonemptiness of throughout, and boundedness and finiteness in the inclusion of Proposition 7.1 and in the active-constraint milestone.
Trivializing formalizations ruled out: quantifies over all of and is not replaced by (7.3) in the goal; is never allowed to be merely closed in the goal; the hypotheses of the goal are satisfiable (, is checked in Lean).
A complete development needs the bipolar theorem for closed convex cones in , the closedness of the cone over a compact convex set, the active-constraint characterization of extreme points, and a finite affine Farkas lemma. All of these are reusable well beyond this mission and are welcome as separate contributions.
Practical algorithms for nonlinear programming do not stop at an exact Karush–Kuhn–Tucker (KKT) point; they stop when an approximate stationarity test passes. Sequential optimality conditions formalize what such tests certify: they are properties of a feasible point phrased through sequences and multiplier estimates, and every local minimizer satisfies them without any constraint qualification. The question that links them back to classical theory is which conditions on the constraints guarantee that a point satisfying a sequential condition is in fact a KKT point. Andreani, Martínez, Ramos and Silva call these strict constraint qualifications and ask, for each sequential condition, for the weakest one.
For the Approximate KKT condition (AKKT) the answer, the Cone Continuity Property, was given by Andreani, Martínez, Ramos and Silva in 2016 (SIAM J. Optim. 26(1)). Section 2 of the present paper treats the Scaled-AKKT condition, which divides the stationarity residual by the size of the multipliers. This scaling appears in the stopping criteria of practical codes and in complexity analyses of nonlinear programming methods. Scaled-AKKT is weaker than AKKT, and the paper uses it as the first, self-contained example of the analysis it then carries out for AGP, CAKKT and SAKKT.
Fix and continuously differentiable functions , , where carries the Euclidean inner product and norm . The feasible set is , and is fixed. An index is active when .
For an objective , the point satisfies KKT if there are and with , for inactive , and .
Scaled-AKKT holds at for if there are sequences , and with , such that for every , and
where is the supremum norm of a multiplier vector.
The Mangasarian–Fromovitz constraint qualification (MFCQ) holds at if are linearly independent and some satisfies for all and for all active . The cone of active gradients is
For a constraint system and a feasible ,
The forward implication says that (2.3) is a strict constraint qualification for Scaled-AKKT; the backward implication says that every strict constraint qualification for Scaled-AKKT implies (2.3).
The result separates Scaled-AKKT sharply from AKKT. For AKKT the weakest strict constraint qualification (the Cone Continuity Property) is implied by many classical conditions, including CPLD and RCPLD. For Scaled-AKKT it is essentially MFCQ, a much stronger requirement. A stopping test of the Scaled-AKKT type therefore certifies a KKT point only under MFCQ, apart from the degenerate case of a full active cone. The other sections of the paper characterize the weakest strict constraint qualifications for AGP, CAKKT and SAKKT, using the same "iff over all objectives" template that this mission formalizes in its simplest form.
The paper's argument is a half-page sketch. A formalization makes explicit several points it leaves implicit: the role of the in the scaling factor, the vanishing of inactive multipliers forced by the complementarity limit, and the theorem of the alternative that converts failure of MFCQ into a nonzero solution of (2.4). None of these results is formalized on Prove2Me or, to our knowledge, in Mathlib.
The forward direction splits on whether the multipliers stay bounded, and the unbounded case requires normalizing by and extracting a convergent subsequence. Along that subsequence one must check that the normalized multipliers have supremum norm exactly one, that the normalized objective gradient tends to zero, and that inactive multipliers tend to zero; only then does the limit contradict MFCQ. The backward direction needs a theorem of the alternative (Motzkin or Gordan type) for the active gradients, together with linear dependence of the equality gradients. The paper uses it without stating it. It also needs a vector with . The printed text chooses , which has the wrong sign for the objective ; milestone 6 is stated for every , so the sign issue does not propagate.
is EuclideanSpace ℝ (Fin n); the constraints are index families Fin m → E → ℝ and Fin p → E → ℝ; gradients are Mathlib's gradient. Multiplier vectors live in Fin m → ℝ and Fin p → ℝ, whose Mathlib norm is the supremum norm, while residuals use the Euclidean norm. Standing hypotheses: every , is (the paper's "continuous first-order derivatives"), every objective in the goal is , and is feasible. The objective is quantified inside the equivalence, so the left side of the goal depends on , , alone. "or" is inclusive. The cone condition is equality of the cone with all of , not with its linear span. KKT carries both the sign condition and complementarity. MFCQ is defined in its primal (direction) form; defining it as "no nonzero nonnegative null combination" would make milestones 4 and 5 hold by definition, and that reading is excluded. Milestone 2 omits the MFCQ hypothesis present in the paper's sentence because the bounded case does not use it.
A complete development needs subsequence extraction in finite-dimensional spaces, continuity of gradients of functions, and a theorem of the alternative for finitely many vectors. The last two are reusable beyond this mission. Proofs of individual milestones are welcome independently.
Multistage stochastic linear programs model decisions taken over time under uncertainty: reservoir releases in hydro-thermal scheduling, production and inventory plans, capacity expansion. Their standard solution method, stochastic dual dynamic programming (SDDP, Pereira and Pinto 1991), approximates each stage's cost-to-go function from below by cutting planes. This gives a lower bound on the optimal value and a candidate policy, but no guaranteed upper bound: in the risk-neutral case the policy's expected cost is estimated by Monte Carlo simulation.
Planners who are averse to risk replace the expectation in each stage by a coherent risk measure (Artzner, Delbaen, Eber and Heath 1999), nested stage by stage so that the resulting dynamic risk measure is time consistent (Ruszczyński and Shapiro 2006). Under such a nested objective, simulation no longer estimates the cost of a policy: the nested risk of a policy is not an average over sampled scenarios. Philpott, de Matos and Finardi (2013) address this by an inner approximation of the cost-to-go functions from above, built from convex combinations of finitely many points with known upper bounds. Their Proposition 5 shows that the optimal value of the resulting first-stage problem bounds the nested risk-adjusted cost of the policy defined by the inner approximation. This gives a deterministic upper bound that complements the SDDP lower bound, and they apply it to the Brazilian hydro-thermal system.
There are stages. The decision at stage is ; are matrices and . Stage 1 is deterministic: . For a random outcome ranges over a finite set , independently of earlier stages, and enters through the right-hand side . The feasible set of stage given the previous decision is
A coherent risk measure maps random costs to and is subadditive, monotone (), positively homogeneous and translation equivariant (). Larger is worse: these are costs. Each stage carries a one-step coherent risk measure on random costs over . It is extended to costs in by whenever some outcome has infinite cost.
For fix points and numbers . The inner approximation is the lower boundary of the convex hull of the pairs :
which is off the convex hull of the points, with . The policy's stage problem (13) and the first-stage problem (8) are
The numbers are upper bounds when for all and . A policy defined by the inner approximation, , takes at each state and outcome an action solving (13), and a first-stage action solving (8). The actual risk-adjusted cost of over stages is
with no future term at . The nested risk-adjusted cost of the policy is .
The bound holds for every , every family of coherent , every choice of points satisfying the upper-bound property, and every minimizing selection .
Proposition 3, the risk-neutral case . Proposition 4, the subgradient rule for given by its dual representation. The existence of a policy , which shows that the hypotheses of the goal can be met.
Proposition 5 makes the inner approximation a certificate. Any policy computed by minimizing against has nested risk-adjusted cost at most , a number obtained by solving one linear program. Together with the lower bound from outer approximation it brackets the risk-adjusted optimal value. The gap then measures the quality of a risk-averse SDDP policy without simulation, which the nested objective does not allow. The bound covers every coherent nesting used in practice, such as mixtures of expectation and CVaR.
The results are proved in the paper. None of them is machine-checked. A formalization adds a precise account of the infinite values the paper does not discuss: infeasible stages, points outside the convex hull, and the extension of to . It also pins down the exact form of the upper-bound hypothesis the induction needs.
The obvious reading of the hypothesis on p. 16, " is an upper bound on " with the true value function , does not support the induction. The policy does not act optimally, so its cost can exceed the true value, and the inductive step compares with the policy's own stage value , not with . The hypothesis that works bounds the risk-adjusted optimal value of the policy's stage problem (13) at the points, which is what the paper's Upper Bound Computation actually computes.
The second difficulty is infinite values, which the paper never discusses. A risk measure is defined on real random costs, yet stage problems can be infeasible, is off a convex hull, and a convex combination may put zero weight on a point whose bound is . Every inequality of the paper has to be re-read in , and the extended-real arithmetic must not silently produce a value the paper does not intend.
Vectors are Fin n → ℝ, all stages share and , and costs that may be infinite are EReal. Minima are EReal infima, on an empty set. Attainment of a minimum is never built into a definition: the policy is a selection with a minimizing property, required at every state where the stage problem is feasible. Stages are natural numbers. Points and bounds are indexed by the stage of the function they define, so pts s j is and qv s j is . Stagewise independence is built in: ranges over whatever happened before.
Standing assumptions made explicit in the statements:
The risk measures act on real random costs and are extended by when some outcome has infinite cost. In Proposition 4, is given by its dual representation (10); the representation theorem itself is not part of the mission. The existence statement adds solvability of and boundedness below of the last-stage program, without which (8) or the last stage has no solution.
The goal is not to be trivialized. Its hypotheses mention neither nor the induction claim; the policy must minimize at every feasible state, not only along visited states; and the statement is for general and general coherent , not the expectation. The bound is trivially true when and is informative when lies in the convex hull of the stage-1 points.
A complete development needs:
The first two are reusable for any SDDP-type development. Proofs of the milestones in any order are welcome.
Multistage stochastic programs model sequential decisions under uncertainty: hydro-thermal scheduling, inventory and capacity planning, portfolio management. The dominant solution methods, Stochastic Dual Dynamic Programming (SDDP, Pereira and Pinto 1991) and its relatives CUPPS and DOASA, never compute the Bellman (future-cost) functions of the problem. Instead they build outer approximations of them by cutting planes: affine minorants obtained from the optimal values and Lagrange multipliers of one-stage subproblems. Practitioners run these methods on very large problems, so the question of whether, and in what sense, the approximations converge is of direct practical relevance.
Earlier convergence proofs (Philpott and Guan 2008; Shapiro 2011) rely on linear stage problems, where only finitely many distinct cuts can be generated and convergence is finite. Girardeau, Leclère and Philpott (Math. Oper. Res. 2015) prove convergence for convex stage problems, where infinitely many distinct cuts may appear and finite termination is lost. This mission covers the first half of that paper: the deterministic multistage problem (§2), whose proof contains the whole scheme of the argument. The stochastic scenario-tree version is the companion mission of this series.
Fix a horizon . States lie in and controls in ; values are in . The data are state sets , control multifunctions , stage costs , linear dynamics , a final cost and an initial state . The problem (1) is
The Bellman functions are on and elsewhere, with .
Assumptions (H₁) require to be a convex multifunction with convex compact values; and to be convex, lower semicontinuous and proper; and to be finite and Lipschitz on . They also require extended relatively complete recourse (ERCR): for some , on the enlarged set (a -neighbourhood inside the affine hull of ) the cost is finite and some admissible control leads into .
The cutting-plane method keeps approximations , starting from and with . At iteration it runs forward from . At each stage it solves the one-stage problem with in place of , which gives a minimizer , the optimal value and a Lagrange multiplier of the constraint . It then adds the cut
and moves to . The approximate cost-to-go is .
For every run of the method and every ,
The first limit says the computed decisions become optimal for the true Bellman functions; the second says the cuts become exact at the visited states. Nothing is claimed away from the generated trajectories.
In the order the proof uses them:
Companion items state that runs exist under (H₁) and give Kelley's cutting-plane lemma (Lemma 2.1), the warm-up result of §2.
Theorem 2.1 is a convergence guarantee for cutting-plane decomposition of nonlinear convex multistage problems. It does not depend on finitely many dual extreme points, so it covers problems with nonlinear convex costs and convex control constraints. The result is the template for the stochastic Theorem 3.1, which covers SDDP, CUPPS and DOASA as special cases of a general node-selection scheme. Along the way the paper isolates ERCR, a constraint qualification that is exactly what bounds the Lagrange multipliers and makes the cuts uniformly Lipschitz.
The result is proved in the paper; as far as is known it has no machine-checked proof. This mission produces a Lean statement of the deterministic algorithm, with extended-real Bellman functions, cut validity, and multiplier selection as a predicate on runs. It also supplies the statements of the reusable lemmas: marginal-function convexity, the monotone-minorant lemma, Kelley's method. Formal proofs of the milestones, alternative arguments, and explicit Lipschitz constants are all open.
The naive argument, "the approximations increase and are bounded by , so they converge", only gives pointwise convergence of to some limit below . It does not show that the limit equals at the states actually visited, and the visited states change from iteration to iteration. The proof must control cuts computed at one state when they are evaluated at another. This needs a uniform bound on the multipliers . That bound comes from ERCR (moving a distance in every direction of the affine hull stays where the cost is finite), together with Lipschitz continuity of on a compact set lying inside the relative interior of its domain. Without ERCR the multipliers can be unbounded and the argument breaks. A second difficulty is the backward induction itself: the conclusion at stage uses both limits at stage , and passing from to needs a compactness argument (Lemma 5.2).
States are EuclideanSpace ℝ (Fin d) and controls EuclideanSpace ℝ (Fin p); costs and value functions are EReal-valued. Convexity of an extended-real function means convexity of its epigraph. Minima are EReal infima ( over an empty set), with attainment stated separately. is extended by outside .
The Lagrange multiplier condition is encoded by (12): lies in the direction space of and is a subgradient, on , of the stage optimal value at . A run is a predicate on : any minimizer and any multiplier are allowed. The paper's iteration is Lean's k + 1.
Standing assumptions added to (H₁), all used by the paper's proofs:
Deviations from the page:
Limits are Tendsto … (𝓝 0) in EReal. There, convergence to forces the differences to be eventually finite, so a value of cannot make a limit hold for free. The goal's hypotheses are exactly (H₁) and the run predicate. Statements that only assert the existence of a good run, or bound instead of the cuts, are not formalizations of Theorem 2.1.
A complete development needs:
All three are reusable well beyond this mission. Proofs of any milestone are welcome, as are proofs of the companion items.
A firm that sells differentiated products sets more than prices. It chooses quality levels (features, materials, reliability) and the ancillary services that come free with a product, such as a factory warranty or free maintenance for a fixed period. Wang, Ke and Cui (SSRN 3766191; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2020.0947) study the joint choice of price, quality and service duration when consumers choose according to the multinomial logit (MNL) model.
A firm allowed to make more decisions can never earn less: it may always ignore the extra instruments. The question this mission formalizes is what happens to consumers. A natural guess is that every new instrument lets the firm extract more of the consumers' surplus. Section 2.3 of the paper (Proposition 5) shows that under MNL demand this guess is wrong: consumer surplus also rises, so more control is a "win–win". The welfare measure is the logit consumer surplus of Anderson, de Palma and Thisse (Discrete Choice Theory of Product Differentiation, MIT Press, 1992).
The mission is the sixth of a series on the paper; each mission defines its own copy of the model in its own namespace.
There are products . Product has a price , a quality level and a service duration , which must lie in a fixed interval . The parameters are: , the consumers' sensitivity to quality; , the utility of one unit of service time; , so that producing one unit at quality costs ; and , so that service costs per unit of time. The sign of is free: higher quality may make service cheaper (), dearer (), or leave it unchanged ().
A consumer buys product with the MNL choice probability
where the is the outside option of buying nothing. With market size one, the firm's profit is
and the bracket is the markup of product . Consumer surplus is
Three problems are compared, at the same pre-determined qualities and durations :
Section 5.1 adds the manufacturer's short-term problem (10): qualities are fixed, and the firm also chooses which products to offer.
For every maximizer of each of the three problems,
The inequalities are weak; equality holds, for instance, when the pre-determined are already optimal.
The result separates two effects that are usually conflated. More instruments raise profit; Proposition 5 says that under MNL demand the extra profit comes from serving more consumers (fewer choose the outside option), not from extracting more surplus from each. Proposition 8 states the corresponding structure for a firm whose product designs are already fixed: offer everything, use extreme service durations, and keep markups equal across products.
The paper proves these results; none is formalized. A machine-checked development produces the welfare comparison together with the price step of the MNL multi-product pricing problem (equal markups at every optimum, uniqueness of the optimal profit as a fixed point) as reusable statements, and pins down the boundary cases of Proposition 8 that the printed statement leaves implicit.
The ordering of profits is immediate from the nesting of feasible sets. The obstacle is translating it into consumer surplus: consumer surplus is not monotone in profit along arbitrary price vectors, and the argument needs that at every maximizer of each problem all markups are equal to , with the optimal profit. That requires a global optimality analysis of the multi-product MNL pricing problem: the profit is not concave in prices, and both the uniqueness of the fixed point and the characterization of all maximizers (not only a stationary point) must be established. Comparing values with defined as the optimal profit, without linking them to the maximizers, proves nothing about consumer surplus.
Fin N (0-based); is arbitrary and is allowed. The outside option is the in the denominator, not a product.A formalization in which the maximizers are given by the paper's closed-form prices, in which are defined as optimal values and only is compared, or in which there is a single product, would make the goal trivial or different and is ruled out.
Contributions are welcome on the MNL price step (equation (17)), which is reusable for any multi-product logit pricing model, and on the per-product separation of the duration choice in Proposition 8.
Firms that sell durable goods set three things at once: a price, a quality level, and the length of an ancillary service that comes free with the product, such as a warranty. Wang, Ke and Cui (SSRN 3766191; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2020.0947) study these joint decisions under multinomial logit (MNL) demand. For a monopolist offering several products they show (their Theorem 1) that each service duration is extreme (the shortest or the longest allowed), each quality is set product by product, and all markups are equal.
A natural question is whether that structure survives competition. In practice, quality and warranty terms are long-term strategic choices while prices react to rivals; if competition changed the optimal qualities and durations, the monopoly analysis would say little about real markets. Section 2.4 of the paper answers the question for an oligopoly of single-product firms. This mission formalizes that answer, Theorem 2.
There are firms; firm sells product . Product has a quality sensitivity , a base service cost per unit time , a marginal effect of quality on service cost (of either sign, or zero), a production-cost coefficient (cost ), and a service utility per unit time . Firm chooses a price , a quality and a service duration .
A consumer buys product with the MNL choice probability
where the is the outside (no-purchase) option. The payoff of firm is its markup times its market share:
A Nash equilibrium is a profile with every such that no firm can raise by changing its own triple , jointly, to any other triple with duration in . The monopolistic case is problem (4): one firm maximizes over all prices and qualities in and durations in . Finally, the duration index of product is
Assume for all , , and for all . Then
for every optimal solution of the monopolist's problem, which exists. The goal compares with any monopoly optimum and does not presuppose the monopoly formulas of Theorem 1.
The proof in the Online Supplement (pp. 2–3) passes through the following statements, which are the mission's milestones:
The result. Theorem 2 says that the quality and service rules of the monopoly are robust to competition: each firm sets quality where marginal consumer utility equals marginal cost, and offers the shortest or the longest service, regardless of what its rivals do. Only prices respond to competition, and they fall. The proof also shows that the competitive aggregate exceeds the monopolist's, so more consumers buy and consumer surplus is higher than under monopoly. Uniqueness makes comparative statics well defined.
Formalizing it. The theorem is proved in the paper and, to our knowledge, not formalized anywhere. A formal proof requires the MNL price-competition equilibrium argument (existence and uniqueness through a one-dimensional aggregate), which is a standard tool in operations management and industrial organization (Anderson, de Palma and Thisse 1992) and has independent reuse value. Making the argument precise also exposes two points the paper leaves implicit: the tie case in the duration choice, and the domain on which the bound holds.
The game is not concave: is not concave in firm 's own strategy (its best attainable value is convex in the duration , which is why durations end up extreme), and strategies are unbounded in price and quality, so the standard existence theorems for concave games with compact strategy sets do not apply. Writing down the first-order conditions and solving them produces candidates, but it shows neither that a candidate is a global best response nor that no other equilibrium exists. Uniqueness also fails without the no-indifference condition (see below).
Fin N (0-based); is arbitrary. The outside option is the 1 + in the denominator, not an element of Fin N.CarbonDoubleCount.Planner.IsPureNash) with Function.update: deviations are unilateral and joint in , not coordinate by coordinate.Formalizations that do not count: a price-only game with qualities and durations fixed at the monopoly values (that is the paper's reduction, not the theorem); a two-firm version; an equilibrium notion checked one coordinate at a time; or an equilibrium assumed rather than proved to exist.
A complete development needs real analysis of one-variable functions (monotonicity, the intermediate value theorem, maximization of -type functions) and finite sums. The pure-Nash definition and the MNL price-competition milestones (4–8) are reusable beyond this paper. Proofs of any milestone, and alternative arguments for the price-equilibrium uniqueness, are welcome.
Firms that sell durable goods compete on price, on product quality and on the services bundled with the product: a factory warranty, free maintenance, technical support. Wang, Ke and Cui (SSRN 3766191; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2020.0947) study the joint choice of all three when consumers choose among the firm's products according to a multinomial logit (MNL) model. Their first result (Theorem 1, the subject of mission I of this series) is that when each product may receive its own service duration, every optimal duration is the shortest or the longest allowed.
In practice many firms do not differentiate service across products: every Apple product, for example, comes with the same one-year factory warranty. The paper's Section 3 therefore studies a benchmark in which one uniform service duration is attached to all products, and compares it with differentiated service to measure the value of service differentiation. Theorem 3, the goal of this mission, says that the extreme-duration structure survives the uniformity constraint.
The pricing side builds on a line of work on multi-product pricing under logit demand. Hanson and Martin (1996) showed that the MNL profit is not jointly concave in prices; Li and Huh (2011) and Gallego and Wang (2014) showed that, nevertheless, optimal markups (price minus cost) are equal across the products of a firm under the MNL and nested logit models.
A firm sells products, . For product :
The firm chooses prices , qualities and service durations . Under the MNL choice model (2) a consumer buys product with probability
the being the no-purchase option. With unit market size, the total expected profit (3) is
Service durations lie in an interval , the shortest and longest durations the firm may offer.
The uniform-duration problem (7) adds the constraint for all :
Problem (7) has an optimal solution whose uniform duration is an endpoint. The goal says nothing about the optimal prices, qualities or profit value; those belong to the milestones.
is unique, and it is the optimal profit over prices and qualities, attained at , . 2. . is differentiable with . 3. The numerator. has nonnegative derivative. 4. Quasi-convexity. is quasi-convex in . 5. (25). The root equation is equivalent to with , so increases with . 6. Convexity of . is convex in .
Milestones 2–4 and 5–6 are the paper's two routes from (24) to Theorem 3. A further item states the universal reading of Theorem 3 (every optimal uniform duration is or ) under and the non-degeneracy assumption that some product has or .
Theorem 3 is the basis of the paper's Section 3. It shows that a firm restricted to one service policy should still go to an extreme, and it makes the uniform benchmark a comparison of two candidate durations. Comparing that benchmark with Theorem 1's differentiated optimum measures the value of service differentiation, which the paper reports numerically. Equation (24) also gives the optimal profit at every uniform duration as the root of a scalar equation, which is the form any sensitivity analysis in starts from.
On the formal side, the paper's results are proved on paper but, as far as is known, none is machine-checked. The mission requires formalizing the reduction of the joint MNL price–quality problem to a scalar fixed point (the equal-markup property of Li and Huh, extended to quality), an implicit-function derivative and a Cauchy–Schwarz step, or alternatively a convexity argument. The equal-markup reduction is shared with missions I and VI of this series.
The obvious argument fails at the first step: the MNL profit is not jointly concave in the price vector (Hanson and Martin 1996), let alone in prices, qualities and the duration together, so "maximize a concave function and check the endpoints" does not apply. The extreme-point structure holds only after prices and qualities have been optimized out, and that requires knowing the optimal profit at each exactly: as the root of (24), a fixed-point equation in which appears on both sides. The global optimality in (24) is itself the hard part, since a first-order condition alone does not give a global maximum of a non-concave function on .
Conventions committed to in Lean:
Fin N, 0-based; is allowed. The outside option is the constant in the MNL denominator, not a product.fun _ => t; the goal assumes .These formalizations would trivialize the goal and are ruled out: a single product (then Theorem 3 is Theorem 1(a)); qualities fixed rather than chosen; a duration vector instead of one shared ; and an existential statement in which may be any point of .
The definitions needed are the MNL choice probability and profit, plus the scalar functions , and of the proof. Mathlib's QuasiconvexOn, ConvexOn, HasDerivAt and Finset.sum_mul_sq_le_sq_mul_sq cover the rest. A proof of (24), the global optimality of equal markups and per-product quality under MNL, would be reusable across the whole series. Contributions to any milestone are welcome.
Dynamic pricing asks a seller to post prices to a stream of customers and learn demand from purchase decisions alone. Luo, Sun and Liu study the contextual version in which a customer's valuation is linear in a covariate vector plus noise with an unknown distribution (arXiv:2109.07340v2; Mathematics of Operations Research, 2024). Their DIP policy estimates the linear part, discretizes the remaining price residual, and then runs an upper-confidence-bound rule on the discretized problem. Because the linear part is only estimated, the discretized problem is not an ordinary linear bandit: its reward parameter drifts from period to period by an amount controlled by the estimation error. The paper calls this a perturbed linear bandit (PLB) and proves an upper bound for it whose dominant extra term is linear in the perturbation size times the horizon.
This mission formalizes the matching statement: no algorithm can avoid that linear term. It is the paper's Proposition 2 (p. 22), proved in its Appendix A (pp. 44–46).
Fix a dimension . A perturbed linear bandit with perturbation constant consists of parameters , finite action sets and noise variables , with for all periods . In period an algorithm sees the action set and the history of its past actions and rewards, plays , and observes the reward
The algorithm may randomize. The parameters are never observed.
For a central parameter the paper defines the parameter set
so any sequence in has perturbation at most .
The PLB regret over periods compares each action with the best action of the current period:
The expectation is over the algorithm's randomness and the noise.
For every with positive entries (and ) there is depending only on such that for every with and every algorithm there are parameters and action sets with
The formal statement also records that the constructed instance is a PLB with perturbation , that its action sets are nonempty, and that every action has a single nonzero entry with , which places the hard instance inside the class covered by the paper's upper bound (Lemma 3, Conditions 1 and 3).
The result. Lemma 3 of the paper bounds the regret of its M-LinUCB algorithm on a PLB by a -type term plus . Proposition 2 shows that the second term is not an artefact of the analysis: an adversary who may move the parameter inside a box of width forces every algorithm to pay order . In the pricing application the perturbation is proportional to the estimation error of the linear part, so the lower bound explains why the paper's pricing regret bound (Theorem 1) carries a term linear in the accumulated estimation error. The result also separates the PLB from the zero-perturbation linear bandit, where regret is achievable.
Formalizing it. The proposition is proved in the paper; it has not been machine-checked. A formal proof requires an explicit model of randomized, history-dependent algorithms interacting with an adversarially chosen but deterministic parameter sequence, which the mission supplies. The model and the two-point construction are reusable for other two-hypothesis lower bounds in linear and contextual bandits.
The obvious argument fixes one hard instance and shows that every algorithm suffers on it. That fails: for a fixed parameter sequence, an algorithm that always plays the optimal action of that sequence has zero regret. The instance must therefore be chosen after the algorithm, and it must be chosen period by period, because the law of the period- action depends on the rewards of periods , which depend on the parameters already chosen. The parameters must nevertheless be deterministic: the adversary may react to the law of the algorithm's action, not to its realization. Making this recursive construction precise, together with the measurability needed for "the probability that " to be meaningful, is the main formal work. The arithmetic of each period is elementary.
A second point concerns the dimension: the construction needs two distinct coordinates, and for the statement fails, since every parameter in is then positive and playing the largest action has zero regret.
Fin d (0-based); periods are 1-based. Vectors are Fin d → ℝ, and is Mathlib's sup norm on that type. Action sets are finite sets (Finset). The maximum over an empty action set is set to ; every statement requires nonempty action sets.Contributions welcome: proofs of the two milestones, the measurability of the recursively defined actions, and the summation step from the per-period bound to the goal.
Quadratically constrained quadratic programs (QCQPs) minimize a quadratic function subject to quadratic inequality and equality constraints. They model trust-region subproblems, robust least squares, max-cut and many problems in signal processing and control. They are NP-hard in general, so practice relies on convex relaxations, and the standard one is the Shor semidefinite (SDP) relaxation. The SDP relaxation lifts variables to an positive semidefinite matrix, which is expensive for large .
For an important subclass, the simultaneously diagonalizable QCQPs (SD-QCQPs), a much cheaper relaxation is available: after a change of variables all quadratic forms are diagonal, and the products can be relaxed by new variables . This is a second-order cone (SOCP) relaxation, studied by Ben-Tal and den Hertog (2014) and Locatelli (2016) for the trust-region problem with additional constraints and related problems. Whether one may use the SOCP relaxation in place of the SDP relaxation without losing anything, for the optimal value and for the convex-hull description, is the question settled here.
This mission formalizes Proposition 1 of A. L. Wang and F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs (Math. Program., 2021; arXiv:1911.09195v3), §4.2.1 and App. A, together with Lemma 9 of §4.2.
A QCQP (1) in variables has data , , for , with constraints of which the first are inequalities. Writing ,
The SDP relaxation (3) uses and the lifted variable with :
Its projected epigraph (4) is the set of for which some satisfies these constraints together with .
A family is simultaneously diagonalizable (SD) if there is an invertible with every diagonal (Definition 4); an SD-QCQP is a QCQP whose matrices are SD (Definition 5). Changing variables by gives a diagonal QCQP (10): with , so with . For it, the SOCP relaxation (11) is
and (12) is the set of for which some satisfies these constraints and .
The dual set is .
For a diagonal QCQP (10),
No regularity assumption is made; both values may be or .
For any SD-QCQP, is polyhedral.
The result. Proposition 1 transfers every SDP-tightness and convex-hull criterion to the SOCP relaxation of an SD-QCQP. The paper's main theorems give sufficient conditions for and for under the assumption that is polyhedral; Lemma 9 shows this assumption holds for every SD-QCQP, and Proposition 1 then gives the same conclusions for an SOCP with only additional variables and convex quadratic constraints instead of an semidefinite matrix (Remark 12). The value identity was first recorded by Locatelli (2016); the set identity is, according to the authors, new in the paper.
Formalizing it. The result is proved in the paper; no machine-checked version is known. The mission produces Lean definitions of the QCQP, its Shor relaxation, its projected epigraph and the lifted SOCP relaxation that are shared with the other missions of this series on the same paper, and a checked transfer from SDP to SOCP relaxations that downstream tightness results can use.
The argument is short on paper; the formal work is in the matrix bookkeeping. The inclusion needs a Schur complement for a block matrix whose top-left block is the scalar , in the block indexing , and the identity inside a trace of block products. The reverse inclusion needs an explicit lifted matrix, and its positive semidefiniteness is a global property of an matrix that the coordinatewise inequalities do not give entry by entry. The value identity is an identity of infima in the extended reals, where either side may be , so real arithmetic on the values is not available.
QCQP N m with symmetric , vectors , scalars and . Constraint is the paper's constraint , an inequality iff .EReal, so infeasibility gives and unboundedness . is , and in the SDP is symmetric.IsUnit U.Matrix.fromBlocks positive-semidefiniteness results), traces of block products, and EReal infima. A reusable lemma "" is welcome beyond this mission.A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. The class contains nonconvex problems such as binary programs, max-cut, the trust-region subproblem and many problems in signal processing and control. A standard convex approximation is the Shor semidefinite programming (SDP) relaxation, which replaces the rank-one matrix by a positive semidefinite matrix . The relaxation always gives a lower bound; the question studied by Wang and Kılınç-Karzan (arXiv:1911.09195v3, Math. Program. 2020, doi:10.1007/s10107-020-01589-9) is when it is tight, either in the sense of objective values or in the stronger sense that the relaxation describes the convex hull of the problem's epigraph.
Earlier exactness results are of two kinds. One kind concerns special structure: one constraint (the S-lemma, the trust-region subproblem), or two constraints under extra conditions. The other kind, due to Beck (Quadratic matrix programming, SIAM J. Optim. 2007, Corollary 4.4), exploits block symmetry: if every quadratic form is of the form with , the SDP bound equals the optimal value. The paper under formalization recasts both kinds in one framework. Its convex hull results (Theorems 1 and 2) assume that a certain dual set is polyhedral, and its Proposition 3 shows that without polyhedrality the convex hull result can fail. This mission is about Theorem 7, which removes the polyhedrality assumption at the price of a larger symmetry parameter.
Fix variables and constraints. For let with a symmetric matrix, and . The QCQP is
Its epigraph is . With and , the Shor relaxation imposes , for inequalities and for equalities; its projected epigraph is the set of for which some symmetric satisfies these constraints and . Always .
For write and , and let . Assumption 1 asks that (1) be feasible and that for some that is nonnegative on the inequality indices.
The quadratic eigenvalue multiplicity (Definition 3) is the largest integer such that and, for every , for some symmetric matrix . Here is block diagonal with copies of , and for , the vector has -th block . Every QCQP has multiplicity at least .
A supporting item (not a milestone) states the expansion used in the induction step: for with symmetric and unit , (p. 30).
The result. Theorem 7 is the convex hull counterpart of Beck's value-exactness result: under Assumption 1 and enough block symmetry, the Shor relaxation does not merely give the right optimal value but describes exactly, so every linear objective in over the relaxation is exact. It needs neither the polyhedrality of nor the attainment Assumption 2 used elsewhere in the paper. Problems with this structure include quadratic matrix programs (Beck 2007), in which the variable is a matrix and every quadratic form is a trace . The companion Theorem 8 (a separate mission of this series) relaxes to at the price of intersecting with the optimal hyperplane, and Remark 14 records that the authors conjecture these thresholds are sharp.
The formalization. Theorem 7 is proved in the paper; no machine-checked proof of it, or of the Shor relaxation's convex hull results in general, is known. The milestones isolate the three ingredients of the proof as reusable statements: the dual description of (Lemma 1, shared with the polyhedral results of the paper), conic duality applied to a Kronecker-structured SDP, and a rank-reduction argument for Kronecker-structured quadratic forms.
The inclusion is immediate; the content is the reverse inclusion. A point of comes with a matrix , and the naive idea is to decompose into rank-one pieces and move along them. In this fails in general: moving along an arbitrary direction changes each constraint by a first-order term that cannot be controlled, and Proposition 3 of the paper exhibits a QCQP with . The theorem therefore depends on the Kronecker structure and on the count in an essential way, and on an exact dual certificate, whose existence needs the strict feasibility of Assumption 1 and a dual attainment theorem for SDPs that is not yet in Mathlib.
All objects are defined locally in the namespace QCQPTightness.MultHull.
Fin N → ℝ; constraints are indexed by Fin m, the paper's constraint being index , and index is an inequality iff . The standing assumption (p. 1) is a hypothesis of the goal.EReal, so an empty or unbounded set never produces the junk value of a real infimum. "" is stated as for all .PosSemidef and PosDef; is convexHull ℝ in .Fin N by ; uses the same map.IsQuadEigMult k) exactly as Definition 3. The milestones are stated for an arbitrary explicit representation , which makes them at least as strong. Milestone 2 carries , which the paper notes always holds.A complete development needs: SDP strong duality with dual attainment under a Slater condition (the platform's ConvexOptimization.sdp_strong_duality states a related form), the spectral decomposition of a positive semidefinite matrix into rank-one terms, Kronecker product identities for block-diagonal matrices, and the existence of nonzero solutions of underdetermined homogeneous linear systems. The duality and Kronecker lemmas are reusable beyond this mission; proofs of any milestone are welcome.
Manufacturers rarely sell a bare product. A laptop, a vacuum cleaner or a car comes with an ancillary service (a factory warranty, maintenance, technical support) whose length the firm chooses together with the price and the quality of the product. The three decisions interact: a longer warranty makes a product more attractive to consumers but costs the firm more, and how much more depends on quality, since a more reliable product fails less often while a more complex one may be costlier to service. Firms in practice offer very few service options across large product lines: Amazon's Fire tablets come with either a 90-day or a 1-year warranty, and Dyson's vacuum cleaners with either a 2-year or a 5-year warranty.
Wang, Ke and Cui (SSRN 3766191; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2020.0947) study the joint choice of price, quality and service duration for a firm selling substitutable products to consumers who choose according to the multinomial logit (MNL) model. Their first main result, Theorem 1, explains the observation above: under MNL demand, every product's optimal service duration is either the shortest or the longest allowed. The same theorem gives the optimal quality in closed form and shows that all products carry the same optimal markup, extending the equal-markup property of MNL price optimization (Li and Huh 2011, doi:10.1287/msom.1110.0335; Li, Rusmevichientong and Topaloglu 2015, doi:10.1287/opre.2015.1355) to quality and service.
A firm sells products . For product it chooses a price , a quality level and a service duration in a fixed interval of admissible durations. The parameters of product are:
A consumer buys product with the MNL probability
the in the denominator being the option to buy nothing. The markup of product is , and with the market size normalized to one the firm's total expected profit is
The firm solves problem (4): maximize over , and . In Lean the model is PriceQualityService.Joint.Model (attraction, choiceProb, markup, profit, and the exponent below as durationExponent).
Write . Theorem 1 asserts that problem (4) has an optimal solution with
where is the unique real solution of
and that equals the optimal profit. The goal also states the converse: every optimal solution has this quality and price structure, and, when , every optimal duration of a product with or is or .
The milestones follow the proof in Appendix B: the fixed-point form (15) of the profit; the price step (each markup is ); the price-only optimum (17); the quality step (18); the duration step (19); uniqueness of the root ; and Proposition 2, which says which endpoint is optimal for each product.
Theorem 1 reduces a -dimensional nonconcave optimization over prices, qualities and durations to a choice between two durations per product, decoupled across products, plus a one-dimensional equation for the common markup. Proposition 2 then settles each product's duration by comparing a threshold built from its own parameters with the midpoint . The same reduction underlies the later results of the paper: the oligopoly equilibrium, the uniform-service problem, the nested logit extension and the consumer-surplus comparisons all rest on the fixed-point characterization of the optimal profit.
The theorem is proved in the paper; no machine-checked proof exists. This mission formalizes the model and the theorem with its explicit constants, including the uniqueness of , the claim that is the optimal profit, and the existence of an optimum, which the paper's argument takes for granted. The fixed-point form of MNL profit is a reusable tool for any MNL pricing model with additive utilities.
The profit function is not concave in prices, qualities or durations jointly, so first-order conditions alone do not identify a maximum. The obvious argument (set every partial derivative to zero) yields stationary points without showing that any of them is a global maximum, and says nothing at the boundary of , where the optimum actually lies. The three decisions are also coupled through the shared MNL denominator: changing one product's price or quality changes every product's demand, so the claim that each quality is set from the product's own parameters, and that all markups coincide, is not visible coordinate by coordinate. Finally, the statement must hold for every sign of : for the dependence on the duration is linear rather than quadratic, and when moreover every duration is optimal, so the "every optimum is extreme" clause has to exclude exactly that case.
Fin N, 0-based; the paper's product is index . Any is allowed; for the optimal profit is .Fin N.A formalization that fixes or identical products, fixes the sign of , states only first-order conditions, or defines or the optimum by the paper's formula is not this theorem and is ruled out.
The development needs only real analysis from Mathlib: the exponential function, monotonicity of one-variable functions, convexity of composed with a convex quadratic, and finite sums. Proofs of any milestone, alternative arguments for the goal, and reusable lemmas on the fixed-point form of MNL profit are welcome.
Car dealers, electronics retailers and office suppliers sell products whose prices and features are set upstream by manufacturers, and bundle each product with a service of their own: maintenance, repairs or a warranty. The dealer's short-term problem is then purely combinatorial. Which products should be carried, and which of them should come with a long rather than a short service? Longer service makes a product more attractive to consumers but costs the dealer more per unit sold, and the cost per unit of service time depends on the product's quality.
Wang, Ke and Cui (SSRN 3766191, accepted at Manufacturing & Service Operations Management) study price, quality and service decisions under multinomial logit (MNL) and nested logit demand. Section 5.2 of the paper treats the dealer's problem and shows that its solution has a two-threshold structure. This mission formalizes that result, Theorem 5, together with the steps of its proof in the Online Supplement.
The single-service version of the question is classical: under MNL demand with fixed prices, the profit-maximizing assortment consists of the products with the highest margins, a revenue-ordered (here: markup-ordered) assortment (Talluri & van Ryzin 2004). Theorem 5 extends this to two service options per product, where the choice is between three actions for each product (not offered, short service, long service) and the margin of each action differs.
There are products . Product has a fixed price and quality , a quality sensitivity , a service utility per unit time , a unit production cost , and a service cost per unit time . Two service durations are available: a short one and a long one .
The dealer chooses two disjoint sets : products in are offered with service duration , products in with , and the others are not offered. A product offered with duration has attraction and markup . Under MNL demand with an outside option, product is bought with probability
and similarly with for (eq. (12)). The dealer's expected profit, with market size one, is
and problem (13) is to maximize over disjoint pairs .
Two orderings of products appear in the answer. The short-service markup is . The adjusted markup is
A markup-ordered assortment is a set of the products with the highest values of ; an adjusted markup-ordered set is a set of the products with the highest values of .
Assume , and for all . There are thresholds such that, with and ,
Part (a) of the paper (a markup-ordered assortment is an optimal offer set) and part (b) (long service on an adjusted markup-ordered subset of it, short service on the rest) are one statement about the same .
Problem (13) has feasible pairs. Theorem 5 reduces the search to at most pairs indexed by two thresholds, and it says which products deserve the long service: those with the highest adjusted margin , which charges each unit of service cost at the rate rather than at . The paper's managerial reading is that high-margin products go with long service, as with retailers that attach longer warranties to expensive items.
The result is proved in the paper; none of it is machine-checked. A formal proof gives a verified two-service extension of the MNL revenue-ordered assortment theorem, and the fixed-point reduction (milestones 1 and 2) is a reusable device for MNL assortment problems with several options per product.
The profit is a ratio of sums, so exchanging one product's service changes every choice probability, and pairwise exchange arguments do not directly compare assortments. The naive idea of ranking products by a single margin fails: the long-service margin and the short-service margin order products differently, and the long service also raises the product's attraction. Neither ordering alone decides which products get long service. The adjusted markup is the breakpoint at which long and short service become equally profitable, and the three breakpoints must line up for the threshold structure to hold. This ordering uses : with a negative service cost the long service can be optimal for a product whose adjusted markup is below that of a product left unserved, and part (b) fails.
Fin N (0-based); is allowed. All parameters are arbitrary real vectors and real numbers; prices and qualities are fixed data, not decisions.Finset (Fin N) with Disjoint Sl Ss; optimality is a global inequality against every disjoint pair.max and elementary real analysis. Proofs of any milestone, and alternative routes to Theorem 5, are welcome.A firm that sells durable products with an attached service (a warranty, a maintenance plan, a support contract) chooses three things for each product: its price, its quality, and how long the service lasts. Wang, Ke and Cui (SSRN 3766191, Manufacturing & Service Operations Management, 2022) study this joint decision when consumers choose among the products according to a discrete choice model. Under the multinomial logit (MNL) model they show that every product's optimal service duration is either the shortest or the longest available, so that the products split into a short-service group and a long-service group.
That conclusion suggests a different model of the consumer. In business procurement, and more generally when the buyer first decides how long a product will be used, the consumer plausibly chooses a service duration first and a product second. The two-stage nested logit (NL) model (Ben-Akiva 1973; McFadden 1980) captures exactly this: the two service groups become nests, and products within a nest are closer substitutes than products in different nests. Section 4 of the paper asks whether the MNL structure of optimal qualities and prices survives in this model. This mission formalizes its answer, Theorem 4.
Price optimization under the nested logit model has a substantial literature. For prices alone, the optimal prices within a nest share one markup and the problem reduces to a one-dimensional fixed point (Li & Huh 2011; Gallego & Wang 2014). Theorem 4 adds quality as a decision, with production cost quadratic in quality and service cost depending on quality.
There are two nests . Nest contains products , and every product of nest is sold with the same fixed service duration . Product of nest has parameters (quality sensitivity), (base service cost per unit time), (marginal effect of quality on service cost), (production-cost coefficient) and (service utility per unit time). The firm chooses a price and a quality for every product.
The total attractiveness of nest is . With upper-level scale parameter (the nest coefficient is ; the lower-level scale is normalized to ), a consumer chooses nest with probability
buys nothing with the remaining probability, and, having chosen nest , picks product with probability . The probability of buying product of nest is . The markup of a product is its price minus production cost minus service cost , and the firm's expected profit (market size one) is
The firm maximizes over all real price and quality vectors. When the model is the MNL model.
Let . The equation
has a unique real solution . With ,
and is the only maximizer.
The milestones follow the paper's proof in the Online Supplement:
The result. Theorem 4 has two consequences. First, each product's optimal quality depends only on its own parameters and its nest's service duration, not on any other product, although all products are substitutes. At this quality, the marginal production and service cost of quality equals the consumer's marginal utility from it. Second, every product in both nests carries the same markup, : the optimal profit plus the reciprocal of the nest coefficient. A pricing problem with prices reduces to finding the root of a single monotone function. Proposition 7 of the paper uses these closed forms to compare consumer surplus with and without quality control under the NL model.
Formalizing it. The paper's proof writes down first-order conditions and assumes an optimum exists. The goal here is global optimality and uniqueness over all real prices and qualities, which the paper does not prove. A complete formalization needs the existence of the maximizer or a direct upper bound, together with the first-order identities. The related platform item DLevelNestedLogit.Pricing.stationary_point_iff (Li et al. 2015) characterizes stationary points of the price-only revenue in a -level nested logit model. It has no costs and no quality, and it is not used here. No result of this mission has a machine-checked proof yet.
The profit is not concave in prices (under the nested logit model, concavity is known only after a change of variables to market shares, Li & Huh 2011), so a first-order condition does not by itself certify a global maximum. The paper's argument shows only that any optimum satisfies the stated formulas. For a global result, the critical points must be shown to coincide with the maximizers, and the profit must be bounded above by everywhere, including at decisions where markups differ across products of a nest or are negative. The two reductions, to nest markups and then to the scalar , are only valid at the optimum and have to be carried out with that in mind. The exponent makes concave rather than linear in the nest attractiveness. This is the step where the MNL argument does not transfer verbatim.
Nest (s, l). Products of nest are Fin (m x), 0-based. Nests may be empty: an empty nest has , , and contributes nothing.Real.rpow of nonnegative sums of exponentials.The following versions are trivializing and are excluded: only (the MNL case), a single nest, first-order conditions in place of global optimality, fixed qualities, or an optimum defined by the paper's formula.
The definitions (Model, MarkupProblem, Optimum) are self-contained and can be reused for other nested logit pricing results. Contributions are welcome on each milestone, on a sorry-free derivative of in , and on an existence result for the maximizer.
Discrete-time linear iterations with entrywise nonnegative appear wherever a quantity is redistributed along the edges of a network: consensus and tracking protocols for multi-agent systems, positive switched systems, and Markov-type averaging schemes. Such an iteration converges to zero exactly when the spectral radius , the largest modulus of an eigenvalue, is less than one. For a sub-stochastic matrix (all row sums at most one) the classical bound settles marginal stability, and strict stability needs only one row of sum below one that "reaches" the others.
Shi, Zheng, Shao and Cheng (arXiv:2004.01867v2, SIAM J. Control Optim. 2021) study bipartite tracking over signed networks, where asynchronous updates and larger step sizes produce iteration matrices with some row sums above one. For these matrices the norm bound is useless: . Their §2.2 introduces super-stochastic matrices and gives conditions under which the spectral radius is nevertheless below one. These conditions are what the later sections use to allow larger control gains than a sub-stochastic analysis permits. This mission formalizes the main spectral result for a single super-stochastic matrix, Theorem 2.6, together with its companions Theorem 2.7 and Theorem 2.8 (products).
Let be a real matrix. Its -th row sum is , and its infinity norm is . The eigenvalues of are complex numbers, and is the largest of their moduli.
is super-stochastic (Definition 2.5) if for all and there is a set of rows with for and otherwise. The rows split into
A non-zero element chain from row to row is a list of entries , all non-zero, with consecutive indices distinct; is its number of elements. The theorem assumes one chain from some for each , and is the largest number of elements among these chains. The constants are
For a sequence , the product is ordered with later factors on the left, .
If and are non-empty, the chains exist, and
then
Theorem 2.6 is a stability criterion that applies when the standard norm test fails because some row sums exceed one. The criterion is computable: it needs only the row sums, the smallest positive entry and the lengths of paths in the directed graph of from rows of sum below one to the remaining rows. Theorem 2.8 extends this to products, which is the form needed for switched systems in which every subsystem may be individually unstable () while the periodic product is stable. The paper's tracking results for second-order and general linear agents (§§5–13) use these product bounds.
On the formal side, Mathlib has the spectrum of a matrix, Gershgorin's circle theorem and the norm on matrices, but no bounds on the spectral radius in terms of row sums along paths, and nothing on sub- or super-stochastic matrices. None of these results has a machine-checked proof. The mission produces the first formal version of these chain arguments and a reusable eigenvalue–norm inequality for real matrices.
The obvious argument — — fails at once, because . One has to pass to a power and show that every row sum of drops below one. For the rows of the drop comes only from the deficit of a row of , transported along a chain whose length varies from row to row; the bound must be made uniform in the length, which is where and the exponents enter, and where the growth factor competes with the gain . Formally, the induction mixes matrix powers, row sums of products and the indexing of chains. The final step needs the inequality between eigenvalues of , viewed over , and the infinity norm of a power of , which is not available in Mathlib in this form.
All statements live in the namespace SubSuperStoch.SuperSpec. Matrices are Matrix (Fin n) (Fin n) ℝ with -based indices. Row sums, the infinity norm (a supremum over Fin n, equal to when ), the complex spectrum, chains, super-stochasticity and ordered products are defined in one definitions file. Committed conventions:
A trivializing formalization is excluded: the hypotheses are satisfied by the paper's own example on p. 9 (, , , , radicand ), checked in Lean.
Contributions welcome: proofs of the milestones, the general eigenvalue–norm inequality (reusable for any spectral-radius argument over real matrices), and the two companion theorems.
Polyak's heavy-ball method and Nesterov's accelerated gradient method for strongly convex functions (NAG-SC) are the two classical momentum methods of smooth convex optimization. With step size and momentum they differ only by a gradient-correction term, yet NAG-SC is accelerated for every -strongly convex, -smooth objective while the heavy-ball method can fail to converge outside the quadratic case (Lessard, Recht & Packard 2016). The classical continuous-time limit cannot see this difference: as both methods converge to the same low-resolution ODE (Su, Boyd & Candès 2016 treat the convex analogue).
Shi, Du, Jordan & Su (2018/2021) keep the terms of the limit and obtain high-resolution ODEs, one per method, which do distinguish the two algorithms. This mission formalizes their convergence theorem for the high-resolution ODE of the heavy-ball method (Theorem 2 of arXiv:1810.08907v3). A companion mission in the same series treats the high-resolution ODE of NAG-SC (Theorem 1), whose only difference is a Hessian-driven damping term .
Work in with the standard inner product and Euclidean norm . A function belongs to if , is differentiable and convex in the form , and for all . It belongs to if moreover and
and to if in addition is twice continuously differentiable with a Lipschitz-continuous Hessian. Write for the minimizer of .
Given a step size and an initial point , the high-resolution ODE of the heavy-ball method is
for . The initial velocity matches the first step of the discrete method. The paper's Lyapunov function is
For , every step size , and every ,
The result. Theorem 2 gives a linear rate for the heavy-ball ODE with an explicit constant, valid for every objective and every step size up to . Read next to Theorem 1 (rate , constant for the NAG-SC ODE), it shows that at the continuous level both high-resolution ODEs converge at the accelerated rate; the paper locates the difference between the two discrete methods in the discretization, where only the gradient correction of NAG-SC lets the Lyapunov argument survive (its Theorems 3 and 4 and §3.3). The Lyapunov function (3.3) is the NAG-SC function (2.4) with the term removed, and the two coincide at .
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked proof exists. The mission produces a checked chain from the ODE to the rate: a one-sided derivative computation along a trajectory in , a differential inequality, a Grönwall-type integration, and a closed-form estimate of from the initial conditions and -smoothness. The derivative computation and the Grönwall step reuse directly in the companion missions on the NAG-SC and NAG-C high-resolution ODEs.
The algebra is short; the formal difficulty is analytic. The derivative of must be obtained by the chain rule from a one-sided derivative of at and 's differentiability, and the derivative of the two squared norms from those of and . Passing from Lemma 3.2 to is a comparison argument for a function known only to have one-sided derivatives on ; the naive route through requires a monotonicity theorem for functions with derivatives within a half-line. Finally, the estimate of needs and , both consequences of -smoothness and that must be derived from the class definition, and the constant needs a one-variable inequality in .
is EuclideanSpace ℝ (Fin n), is Mathlib's gradient, and is fderiv ℝ (gradient f) x. The classes , , are structures carrying the paper's first-order inequalities (§1.4, p. 8), with ; the Lipschitz constant of the Hessian is existential, as the paper fixes none. The minimizer is a point with for all .
A solution of (1.10) is a pair of curves with , , the derivative of and the derivative of at every , both taken within ; values for play no role. The theorems quantify over every such solution. Existence and uniqueness (the paper's Propositions 2.1–2.2) are not assumed, and no a priori bound on or is added. Derivative claims assert that the derivative exists and has the stated value or bound, so a statement cannot hold merely because a derivative is undefined. The goal states the decay of with the printed constant ; it does not assume any decay of , and an ODE predicate in which is not the derivative of would be a different, trivial statement.
All drafts live in the namespace HighResODE.HeavyBallODE, with one definitions file (classes, ODE, Lyapunov function). Contributions are welcome at every milestone; a general lemma " within implies " and the -smoothness estimates around a minimizer are reusable well beyond this mission.
Nesterov's accelerated gradient method minimises a smooth convex function to accuracy in gradient evaluations, and a -strongly convex one in ; both counts match the lower bounds for first-order methods. Nesterov's own analysis (Y. Nesterov, Introductory Lectures on Convex Optimization, 2004, Ch. 2) proceeds by estimate sequences, an algebraic device that certifies the rate but says little about where the method comes from. Since Su, Boyd and Candès (arXiv:1503.01243), accelerated methods have been read as discretisations of ordinary differential equations, with convergence proved by discrete Lyapunov functions.
H. Luo and L. Chen, From differential equation solvers to accelerated first-order methods for convex optimization (arXiv:1909.03145, Math. Program. 2022), introduce the NAG flow, a first-order system in a position , an auxiliary variable and a scaling parameter whose Lyapunov function decays exponentially for every . In §6 they show that Nesterov's general scheme of optimal method (Algorithm 1) is itself a corrected semi-implicit discretisation of this flow, and they reprove its rates with one Lyapunov function that covers and at once. This mission formalises that analysis, Theorem 6.1.
Let be a real Hilbert space with inner product and norm . A function with gradient map belongs to () if it is continuously differentiable and -convex,
and to if moreover is -Lipschitz, with . A point minimises globally.
Algorithm 1 (Nesterov accelerated gradient method) takes and . For it computes the positive root of , sets and
chooses any with the sufficient decrease (for instance the gradient step ), and sets
The Lyapunov function is
and (89).
For , every run of Algorithm 1 has and
All four conclusions are part of the goal: (98) alone does not carry a rate.
A companion item states (103) of Remark 6.3 for Algorithm 1: with , , , .
Theorem 6.1 recovers, by a Lyapunov argument, the optimal rates of Nesterov's method in both regimes: for convex and for strongly convex once , with the parameter moving between them automatically. It covers every sufficient-decrease choice of , not only the gradient step, and it places Nesterov's method in the same family as the predictor–corrector and gradient-corrected schemes of §5, whose analyses share the Lyapunov function (74) and the rate lemmas of Appendix B. Comparing (99) with the rate of those schemes shows that Nesterov's method is slightly faster per step, with the same complexity.
The result is proved in the paper; the proof of (100) is omitted as similar to that of (88). Nesterov's rates for related parameterisations have been stated on this platform (Bubeck's monograph, Theorems 3.18–3.19), but not for Algorithm 1 with the adaptive parameter , and no machine-checked proof of Theorem 6.1 or Lemma B.1 is known. A formalisation checks the omitted step, pins down where is used, and adds a discrete Lyapunov toolkit for accelerated methods in Hilbert space.
Reading Algorithm 1 directly gives a three-sequence recursion with no visible monotone quantity: itself need not decrease. The contraction (98) holds only for the specific combination (74), and only after the cross terms in produced by the -update are matched exactly against the sufficient-decrease step; any slack in the step rule leaves a positive gradient term. A second difficulty is uniformity in : when the linear factor equals , so the rate must come from a separate estimate of in terms of the step sizes, which are defined only implicitly by a quadratic equation.
NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace); the paper's duality pairing and dual norm are the inner product and the norm (Riesz identification).gradf : V → V with HasGradientAt f (gradf x) x at every point; Mathlib's gradient is not used.IsS1 and IsS11; includes and , and the upper bound (4) is a consequence, not an assumption.IsNAGRun of hypotheses on given sequences, one per step. Step 2 records only (the page writes , but occurs when , and is a conclusion of the theorem). Step 5 is an inequality, not the gradient step. The step sizes are not replaced by a closed form.A statement that assumes the contraction (98) for arbitrary sequences, or fixes to the gradient step, or states only (98), would not be Theorem 6.1 and is ruled out: the goal quantifies over all runs of Algorithm 1 and states all four conclusions.
Contributions welcome: proofs of Lemma B.1 (a self-contained statement about real sequences), the algebraic milestones 1–3, and the convexity steps 4–5. The definitions are local to this mission and duplicate those of the other missions of the series, to be merged later.
The alternating direction method of multipliers (ADMM) solves linearly constrained problems
by alternating a minimization in , a minimization in and a multiplier update. It is one of the standard methods for distributed optimization, statistical learning and signal processing, and in practice it is often applied to nonconvex or (see Boyd et al., Distributed optimization and statistical learning via the alternating direction method of multipliers, 2011, doi:10.1561/2200000016).
For convex problems, ADMM with is classically Douglas–Rachford splitting (DRS) applied to the Fenchel dual of (1.2) (Gabay 1983). The dual reading needs convexity. Themelis and Patrinos (arXiv:1709.05747v4, §5; SIAM J. Optim. 30(1), 2020, doi:10.1137/18M1163993) prove a primal equivalence instead: for arbitrary and for every relaxation parameter , one ADMM update is one DRS step on a reformulation of (1.2) built from image functions. A primal equivalence for was noted earlier by Bauschke and Koch (2015, Rem. 3.14) for , and Yan and Yin (2016, Thm. 1) showed that this case loses no generality. This mission formalizes the general statement and the convergence theorem for nonconvex ADMM that the paper derives from it.
All spaces are Euclidean, , , , . A function is proper if it never takes the value and is finite somewhere. The proximal mapping of with stepsize is the set
For and a linear map , the image function is
The -augmented Lagrangian of (1.2) is . One ADMM update with penalty and relaxation maps to :
One DRS step with stepsize and relaxation on maps to , where and . The reformulation of (1.2) is
that is, and . The regular subdifferential is , the limiting one .
Let be proper, large enough that every ADMM subproblem has a solution, and . With , , and the same expressions at , and ,
together with , , , and .
Proposition 5.2(i)–(iii) (properness of , , ), Proposition 5.3 (), the inclusions (5.3a) and (5.3b), and the identity .
Theorem 5.5(vi): if is surjective, is -smooth and , then . Theorem 5.6: under Assumption II and in the ranges of Theorem 4.1 with , decreases by per step, , cluster points are KKT points with common cost, and the iterates are bounded when is level bounded.
Theorem 5.5 reduces nonconvex ADMM to nonconvex DRS: any descent, convergence or rate statement for DRS on becomes one for ADMM, with the Douglas–Rachford envelope becoming the augmented Lagrangian (5.5(vi)). This is how the paper obtains Theorem 5.6, with explicit penalty bounds for every permitted by Theorem 4.1, under assumptions weaker than earlier nonconvex ADMM analyses (Li and Pong, 2015, doi:10.1137/140998135, require and coercivity).
The results are proved in the paper. No machine-checked proof of a primal ADMM–DRS equivalence is known; the platform holds formalizations of proximal ADMM variants and of convex DRS for monotone operators, but not of image functions. The mission produces a reusable library of image functions and their proximal and subdifferential calculus, and a precise statement of relaxed ADMM in the nonconvex, extended-real setting.
The individual steps are short, but the objects are extended-real and set-valued. An image function may equal , and its infimum need not be attained; that is proper and that the infimum is attained at must be derived from the solvability of the ADMM subproblems, not assumed. The proximal mappings are multivalued, so the equivalence is an inclusion between argmin sets, and the algebra relating , and has to be matched to the relaxation exactly. The subgradient claims require regular subdifferentials of extended-real functions, and (v) requires the optimality condition of the -subproblem, whose quadratic term couples with the residual. Theorem 5.6 additionally rests on the whole DRS convergence analysis of §4.
Points are EuclideanSpace ℝ (Fin _), matrices are continuous linear maps, is ContinuousLinearMap.adjoint, and is the operator norm. Extended-real functions are EReal-valued; the image function imageFn is the EReal infimum over , so it is off the range and may be . Proximal mappings and are sets, and an ADMM update (IsADMMStep) is any selection of minimizers in the order . The two subproblems minimize the terms of that depend on the minimized variable, because the dropped constant may be at a starting point and would make every a minimizer. "Large enough penalty" is SubproblemsSolvable. The regular and limiting subdifferentials are the published IsRegularSubgrad and LimitingSubdiff.
Added hypotheses: and proper in Theorem 5.5 and 5.5(vi), and proper in Proposition 5.2(i). The page omits them, and they are necessary: for every is the whole space while is not proper. Claim (v) is stated as the existence of with , which is stronger than the distance bound and avoids the distance to an empty set. Theorem 5.6 uses the constants of Theorem 4.1 as derived in its proof ((4.8), (4.10)); the printed (4.3) has the sign of one entry of a max reversed and the printed (4.5) an extra factor , and both are then false (counterexamples in the companion mission on DRS convergence). Theorem 5.6 adds ; its run is indexed so that the paper's is the term , with the starting triple at index .
The goal does not assume the DRS relations or (5.3a)–(5.3b), and are defined from the ADMM iterates by (5.2), not chosen independently; a formalization that quantifies over an arbitrary prox selection, or that hard-codes , is a different statement.
Needed infrastructure: image functions and their proximal calculus, regular subgradients of extended-real functions under linear maps, and, for Theorem 5.6, the DRS convergence theory of §4 (formalized in the companion mission I of this series). Proofs of individual milestones are welcome independently.
Nesterov's accelerated gradient method minimises a smooth convex function to accuracy in gradient evaluations, and a -strongly convex one in , which is optimal for first-order methods. The method's original derivation by estimate sequences gives little insight into why it accelerates. Since Su, Boyd and Candès (arXiv:1503.01243) a large literature reads accelerated methods as discretisations of second-order ordinary differential equations and proves their rates with Lyapunov functions transported from the continuous to the discrete setting.
H. Luo and L. Chen, From differential equation solvers to accelerated first-order methods for convex optimization (arXiv:1909.03145, Math. Program. 2022), introduce the NAG flow, a first-order system in a position variable , a velocity-like variable and a scaling parameter , whose Lyapunov function decays exponentially for every . They then show that standard ODE-solver constructions applied to this flow (implicit Euler, Gauss–Seidel splitting, predictor–corrector, gradient correction) produce explicit methods with accelerated rates, and that Nesterov's method is one of them. This mission formalises the paper's analysis of the predictor–corrector scheme of §5.2, its first explicit accelerated method.
Let be a real Hilbert space with inner product and norm . A function with gradient map belongs to (with ) if it is continuously differentiable and -convex:
It belongs to if moreover is -Lipschitz with . The value (plain convexity) is allowed throughout. A point minimises globally.
The method keeps two iterates , a step size and a parameter that evolves by the implicit parameter equation
The predictor–corrector scheme computes a predictor , then , then the corrector :
Every line is linear in the unknown, so one step costs one gradient evaluation. The Lyapunov function is
The Gauss–Seidel step (80) is the scheme without the predictor: and the -update evaluated at .
If and the step sizes satisfy , then every run of (83) with (73) satisfies
with . All three conclusions are part of the goal; (86) alone would not carry the rate.
Theorem 5.1 gives a single explicit method, with one gradient call per step and no restart, whose rate is when and when and ; the parameter interpolates between the two regimes automatically. Both rates are the optimal ones for first-order methods. The same Lyapunov argument, with Lemma B.2 as its rate engine, is reused in the paper for the gradient-corrected scheme (Theorem 5.2), Nesterov's method (Theorem 6.1) and the composite methods of §7, so the milestones of this mission are the shared core of the series.
The result is proved in the paper, with the proof of Lemma B.2 omitted as similar to that of Lemma B.1. No machine-checked proof of Theorem 5.1, Lemma 5.1 or Lemma B.2 is known. A formalisation checks the omitted proof, fixes the exact hypotheses of each step (which estimate needs only -convexity and which needs the Lipschitz gradient), and supplies a reusable discrete Lyapunov toolkit for accelerated methods in Hilbert space.
The obvious approach, imitating the continuous argument with the Gauss–Seidel splitting (80), fails: Lemma 5.1 leaves the cross term , which has no sign, and bounding it by Cauchy–Schwarz as in (82) produces a positive gradient term that destroys the contraction. The predictor–corrector scheme is designed so that this cross term cancels exactly against the descent inequality for between and , and the remaining square vanishes only under the precise step rule . Turning the contraction into the rates (87)–(88) requires lower bounds on that hold uniformly in , which is the content of Lemma B.2. When the linear-rate bound is vacuous, so the rate must come from a separate estimate.
NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace); the paper's duality pairing and dual norm are the inner product and the norm, by the Riesz identification.gradf : V → V with HasGradientAt f (gradf x) x at every point; Mathlib's gradient, which is at non-differentiable points, is not used.IsS1 and IsS11. The class includes and ; the upper quadratic bound (4) is a consequence, not an assumption.A statement that assumed and derived only the rates, or that quantified over arbitrary sequences rather than runs of (83), would be Lemma B.2's corollary and not Theorem 5.1; the goal quantifies over runs of the scheme.
The development needs elementary Hilbert-space identities, the descent inequality (4) for functions with Lipschitz gradient, and real-sequence estimates for products and square roots. The same definitions and Lemma B.2 recur in the series' missions on Theorems 5.2, 7.2 and 7.3. Proofs of any milestone, and of (4) as an auxiliary lemma, are welcome.
Accelerated first-order methods, beginning with Nesterov's 1983 scheme, reach the optimal iteration complexity among gradient methods for smooth convex minimization, but their classical derivations ("estimate sequences") give little insight into why acceleration works. A line of work started by Su, Boyd and Candès (arXiv:1503.01243) reads accelerated methods as discretizations of second-order ordinary differential equations and proves their rates with Lyapunov functions: a quantity that decreases along the continuous trajectory and, after discretization, along the iterates.
Luo and Chen (arXiv:1909.03145, Math. Program. 2022) introduce the NAG flow, a first-order system in two variables with a time-varying parameter , and derive several accelerated methods from it as numerical ODE solvers. Their §4 treats the simplest discretization, the fully implicit (backward Euler) scheme. It is not a practical method by itself, since each step solves a nonlinear equation, but it is the case in which the continuous Lyapunov argument transfers to the discrete level almost word for word, and it is the benchmark for the semi-implicit and explicit schemes of §§5–7. This mission formalizes its convergence theorem, Theorem 4.1.
Let be a real Hilbert space with inner product and norm ; the duality pairing is identified with the inner product. Let and . The function belongs to the class if it is continuously differentiable with gradient and satisfies the -convexity inequality
For this is convexity, for strong convexity. A global minimiser of is fixed throughout.
Given positive step sizes and , the implicit scheme (72)–(73) relates consecutive iterates and by
All right-hand sides are evaluated at the new iterate, which is what makes the scheme implicit. The Lyapunov function (74) is
For with and every run of (72)–(73) with and ,
No condition links to or to any smoothness constant, and need not have a Lipschitz gradient.
A companion item states (76): each step of (72) is a proximal point step with explicit , and .
Theorem 4.1 gives a linear rate for every convex , not only strongly convex ones, as long as ; larger steps give faster decay. It is the exact discrete counterpart of the exponential decay of the NAG flow (Lemma 3.2 of the paper), and the semi-implicit and explicit schemes of §§5–7 are analysed by comparison with it: their proofs follow the same difference computation and must control the extra terms that the implicit scheme does not produce. Through (76), the implicit scheme is an extrapolated proximal point method, close to Güler's accelerated proximal point algorithm when .
The result is proved on paper. To the knowledge of this mission it has no machine-checked proof. Formalizing it fixes the exact hypotheses of the discrete Lyapunov argument (in particular that and are what make the dropped squares nonpositive) and provides the algebraic identities reused by the later schemes of the paper.
The argument is algebraic, but the bookkeeping is where it can fail. The difference produces terms in , , , and , which must cancel or carry the right sign exactly. The naive attempt, to bound by as in an explicit Euler analysis, fails: the implicit scheme controls the decrease by the new value , and the contraction factor comes from solving for it. The -terms close only because (73) is also discretized implicitly, so that , not , multiplies .
is a type with NormedAddCommGroup, InnerProductSpace ℝ V and CompleteSpace V. The gradient is an explicit map gradf : V → V with HasGradientAt f (gradf x) x at every point, and continuity of gradf encodes "continuously differentiable". The class , the Lyapunov function, one step of (72)–(73), and a run are definitions; the scheme's equations are kept in the page's difference-quotient form, as hypotheses on given sequences. Nothing asserts that the implicit system has a solution, and iterates are not defined by choice. Sequences are indexed from .
Conventions committed to: is a global minimiser (the paper's standing assumption that is nonempty); and as on p. 16; the one-step milestones that divide by assume , which along a run follows from (73). The prox in (76) is stated as membership in the argmin through the published predicate GoldenRatioVI.Shared.IsProxPoint.
A trivializing formalization is ruled out: the goal is stated for sequences satisfying the scheme (72)–(73) itself, never for sequences assumed to satisfy (75), and no Lipschitz-gradient class or step-size rule from later sections is imported.
The definitions of and are shared with the other missions of this series and will be consolidated. Contributions welcome: proofs of the identities, of (75), of the goal, and of (76).
Nesterov's accelerated gradient method minimises a smooth convex function to accuracy in gradient evaluations, against for plain gradient descent, and this rate is optimal for first-order methods (Nesterov 2018). The method is usually presented through estimate sequences, which certify the rate but say little about where the iteration comes from. A line of work starting with Su, Boyd and Candès (2016) and Wibisono, Wilson and Jordan (2016) reads accelerated methods as discretisations of ordinary differential equations, with a Lyapunov function carrying the convergence proof from continuous to discrete time.
Luo and Chen introduce the NAG flow, a first-order system in a position variable , a velocity-like variable and a damping parameter , which covers the convex case () and the strongly convex case () in one equation. They then examine which numerical schemes for this flow keep its exponential Lyapunov decay. The implicit scheme does (Theorem 4.1), but needs a proximal step. The explicit Gauss–Seidel splitting (80) does not: its one-step estimate leaves a positive term (Lemma 5.1). Section 5 repairs it in two ways. This mission formalises the second one, from §5.3: a gradient correction step appended to the splitting.
Let be a real Hilbert space with inner product and norm . A differentiable function with gradient belongs to () if
and is continuous. It belongs to if moreover is -Lipschitz with , and . A global minimiser of is assumed to exist.
The scheme carries a step size and a damping parameter governed by the implicit recursion
Given , the gradient-corrected scheme (91) computes
The first two lines are the Gauss–Seidel splitting (80) with output . Both can be solved explicitly, so one step costs one gradient evaluation, at . The third line is a gradient descent step from .
The discrete Lyapunov function is
and the proof also uses the intermediate value (84).
If and the step sizes satisfy , then every run of (91) together with (73) satisfies
with (89). The paper states (87) and (88) by reference to Theorem 5.1; the goal writes them out.
Theorem 5.2 gives an explicit, one-gradient-per-step method with the accelerated rate for convex and the accelerated linear rate for strongly convex . The convex and strongly convex cases are covered by a single Lyapunov argument, with no restart and no prior knowledge of whether beyond its value in (73). The analysis is modular: (92) holds for any correction step with the decay property (94). Section 7 of the paper reuses it for composite problems, replacing the gradient step by a proximal gradient step.
This result is proved in the paper; nothing here is open. To our knowledge none of these statements has been machine-checked. A completed mission gives a checked Lyapunov proof of an accelerated method on a general Hilbert space, with the step sizes left as arbitrary roots of rather than fixed by a closed formula. The paper omits the proof of Lemma B.2 ("Similarly, …"), so formalising it supplies a missing argument.
The naive analysis of the Gauss–Seidel splitting fails. The term in (82) is positive, so this estimate yields no contraction of for any step size; the paper notes that the splitting (80) "does not lead to the contraction property" (p. 19). The correction works only because and share and , and differ only in the -value at against . The step-size rule then has to cancel the two gradient-norm terms exactly. The rates (87)–(88) need a second, independent argument: a discrete comparison for the product under the coupled recursions for and (Lemma B.2). The descent inequality (94) requires the quadratic upper bound (4), which the formalization does not assume. It must be derived from the Lipschitz continuity of on a Hilbert space.
All statements live in the namespace NAGFlow.GradCorr, with one definitions file NAGFlow.GradCorr.Setting. The conventions are as follows.
[NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]. The paper's duality pairing and dual norm are the inner product and the norm (Riesz).gradf : V → V with HasGradientAt f (gradf x) x at every point, never Mathlib's gradient. The classes are the structures IsS1 and IsS11. IsS11 contains and ; inequality (4) is not assumed.IsGCRun, IsGammaRun), indexed from . The two implicit lines are kept as equations. and are part of IsGammaRun.zpow), and (88) is stated for .The goal quantifies over runs of the scheme (91) itself. A version that assumes the contraction (92), or that fixes by a formula that makes (91) degenerate, would not be this theorem.
The development needs the quadratic upper bound for -smooth functions on a Hilbert space, a one-step Lyapunov estimate for the splitting, and the scalar sequence analysis of Lemma B.2. The last two are shared with the predictor–corrector and composite missions of this series. Lemma B.2 and the bound are statements about real sequences only and can be reused independently. Contributions to any milestone are welcome.
Many problems in signal processing, statistics and control are posed as composite convex minimisation: minimise , where is smooth and is convex but possibly nonsmooth or extended-valued (an penalty, a nuclear norm, the indicator of a constraint set). Proximal gradient methods handle through its proximal operator and through its gradient. Their accelerated versions, Nesterov's composite method (Nesterov 2013) and FISTA (Beck–Teboulle 2009), reach the optimal rate for convex problems, and separate variants exist for the strongly convex case.
Luo and Chen (arXiv:1909.03145, Math. Program. 2022) derive accelerated methods as discretisations of a single ODE, the NAG flow, and analyse every scheme with one discrete Lyapunov function. Section 7.2 extends their corrected semi-implicit scheme from smooth to by replacing with the composite gradient mapping. The result is Algorithm 2 (Semi-APGM). It calls the proximal operator once per iteration, and Theorem 7.2 shows that it has the same rate as the smooth methods, in the convex and the strongly convex case at once.
is a real Hilbert space with inner product and norm . The smooth part has gradient and lies in the class , with and . That is, is -convex,
and is -Lipschitz. The nonsmooth part is proper, closed and convex, with effective domain . The subdifferential is . The proximal operator is
With step , set and , the composite gradient mapping. Fix a minimiser of .
Algorithm 2 starts from and . For it chooses with and sets
The Lyapunov function is .
For every run of Algorithm 2 with ,
and, for ,
In attack order:
The theorem gives a single accelerated proximal gradient method whose rate interpolates between for and the linear rate for (when ). Neither the method nor its parameters change between the two regimes. Lemma 7.1 is the only property of that the proof uses, so the same analysis covers constraints (an indicator ), sparsity penalties and any other proximable term.
The result is proved on paper; this mission formalizes it. The paper's argument is short because it reuses the smooth case: "proceed as the proof of Lemma 5.1 and use Lemma 7.1". A machine-checked version has to carry out that reuse explicitly. It also has to supply the proximal facts the paper cites as well known ((112)) and the proof of Lemma B.2, which the paper omits. None of these statements is known to be formalized in Lean.
There is no single hard step. The work is in three places.
Reading Algorithm 2 as a gradient method on does not work, because is not differentiable. All smoothness has to come from through Lemma 7.1.
All objects are defined locally under NAGFlow.APGM. A complete development needs elementary convex analysis in Hilbert space (prox optimality, the descent lemma (4) from the Lipschitz gradient) and the scalar recursion of Lemma B.2. The proximal facts and Lemma B.2 can be reused by the other missions of this series (Theorems 5.1, 5.2 and 7.3) and by any accelerated-method formalization. Contributions are welcome on any milestone, in any order.
In distributed control, many convergence questions come down to one test: is the spectral radius of a nonnegative iteration matrix strictly below one? Consensus and tracking protocols for multi-agent systems (MASs) produce such matrices. The agents that hear the leader directly give rows whose sum is below one, and the agents that only average their neighbours give rows that sum to exactly one. When the agents update asynchronously, the matrices change from step to step, and eigenvalue computations on each matrix give little insight. Conditions read off the sign pattern and row sums of the matrix are much easier to use.
Shi, Zheng, Shao and Cheng (arXiv:2004.01867, SIAM J. Control Optim. 2021) develop such conditions for sub-stochastic and super-stochastic matrices. They then apply them to asynchronous bipartite tracking over signed networks: agents that cooperate or compete must track a leader's state or its negative. This mission covers the first block of results, the spectral bounds for sub-stochastic matrices in §2.2 (pp. 4–6). The classical background is the Perron–Frobenius theory of nonnegative matrices and the convergence analysis of products of stochastic matrices in consensus problems (Ren–Beard 2005).
Let . Write for the row sum of row , and for the infinite norm. is the spectral radius, the largest modulus of a complex eigenvalue of .
is sub-stochastic (Definition 2.1) if for all and for every . Its rows split into
Two numbers measure how far is from stochastic:
the largest row sum below one and the smallest positive entry.
A non-zero element chain from to is a list of entries
that are all non-zero, with consecutive indices distinct (, , …, ). Each entry has the later index as its row. The chain's number of elements is . If for each a chain with is given, is the largest number of elements among them.
In the Lean development these are rowSum F i, normInf F, specC F (the complex spectrum), IsSubStochastic F and IsChain F c L, all in the file SubSuperStoch.SubSpec.Setting.
If is sub-stochastic, and are non-empty, and every is the end of a non-zero element chain starting in , then
If is sub-stochastic, for all , and has exactly one element, then
Its proof uses the eigenvector bounds (2.3) and (2.4) for the two largest coordinates of an eigenvector. These bounds are also drafted, with the denominators cleared.
Theorem 2.2 replaces an eigenvalue computation with a reachability check on the zero pattern of together with two scalar quantities, and the bound it gives is explicit. In the paper it is the basic tool for the products of sub-stochastic matrices (Theorem 2.4) and for the convergence of asynchronous bipartite tracking over signed digraphs (§3 onward). In that setting, "every row of sum one is reached by a chain from a row of sum below one" becomes "every follower is reachable from the leader." Theorem 2.3 covers matrices with a zero diagonal and a single unit row, and there the bound needs no chain condition at all.
The results are proved in the paper. Nothing in this mission is formalized anywhere we know of. Mathlib has Gershgorin's circle theorem and the spectrum of a matrix, but it has no row-sum or chain criterion for nonnegative matrices and no stated link between the spectral radius of a power and its infinite norm. A complete formalization would supply a reusable stability criterion for nonnegative matrices, a statement of in eigenvalue form, and machine-checked versions of the inequalities that the paper's control results rest on.
The obvious first idea is to bound by . That fails: whenever is non-empty, , so it only gives . Strict stability cannot be seen in any single row of . Each unit row only becomes deficient after the deficit of a row in has propagated to it along a chain, and this happens at different powers for different rows. The proof needs one power that works for every row at once, and it has to control how the deficit decays (a factor of per chain element). For Theorem 2.3 the difficulty is different: no power of need have norm below one, so the argument has to work with an eigenvector directly.
Matrices are Matrix (Fin n) (Fin n) ℝ with 0-based indices. is stated as for every in the complex spectrum of , never as a real supremum and never over real eigenvalues only. , and are passed as values together with IsGreatest/IsLeast hypotheses over exactly the printed sets, so an empty set cannot produce a default value. The hypothesis "there exist chains for each " is encoded with a length function len: for every unit row there is a chain of len k elements from some deficient row to , and is the largest len k over the unit rows, i.e. the longest of the chosen chains. The -st root is the real power .
The formalization does not assume , and it does not assume that every row lies in . Either assumption would make the goal a one-line consequence of the norm bound. The chain direction is fixed (the entry has row ), and is the least positive entry; a chain in the opposite direction, or the least entry overall, gives a different statement.
Needed infrastructure: row sums of powers of nonnegative matrices, the relation , and Gershgorin's theorem applied to . The eigenvalue-power bound and the chain bound are reusable outside this paper. Proofs of any milestone are welcome, as are alternative proofs of Theorem 2.3.
Accelerated first-order methods, above all Nesterov's accelerated gradient (NAG) method, minimize a convex function with an -Lipschitz gradient to accuracy in gradient evaluations, and a -strongly convex one in , against and for gradient descent. Since Su, Boyd and Candès (arXiv:1503.01243) read Nesterov's method as a discretization of the ODE , a line of work has tried to derive accelerated methods from continuous-time models with a Lyapunov function, e.g. Wibisono, Wilson and Jordan (arXiv:1603.04245) and Wilson, Recht and Jordan (arXiv:1611.02635).
Luo and Chen (arXiv:1909.03145, Math. Program. 2022) propose a single ODE, the NAG flow, that covers the convex case and the strongly convex case at once, through a time-dependent scaling factor . Its Lyapunov function decays like for every . The rest of their paper discretizes this flow (implicit, predictor–corrector, gradient-corrected and semi-implicit schemes; missions 3–8 of this series) and transfers the decay to the discrete Lyapunov function. This mission formalizes the continuous result, Lemma 3.2 of the paper, on which those discretizations are modelled.
Let be a real Hilbert space with inner product and norm . A function is in the class if it is continuously differentiable and, for some ,
the -convexity of (strong convexity when ). It is in if moreover is -Lipschitz with . A global minimizer of is assumed to exist.
The scaling factor solves , :
It is positive for all and tends to ; for it is .
The NAG flow is the first-order system
or, equivalently, the second-order equation
Its Lyapunov function is
If with , then (57) has a unique solution , and
In particular for all , with no dependence on in the rate.
The lemma gives one continuous model whose energy decays at the rate uniformly in , without separate treatment of the convex and the strongly convex cases. The paper's discrete results (Theorems 4.1, 5.1, 5.2, 6.1, 7.2 and 7.3) prove the discrete counterpart by mimicking the computation (61)–(63) step by step, so the continuous identities are the template of the whole paper. The integral term in (60) also bounds when .
The result is proved in the paper; nothing in this mission is open. To our knowledge neither the NAG flow nor its Lyapunov analysis has been formalized in Lean or another proof assistant. The mission produces a machine-checked well-posedness theorem for a non-autonomous ODE in a Hilbert space whose coefficient is unbounded on when , and a machine-checked Lyapunov computation that later missions can mirror in discrete time.
The Lyapunov computation (61)–(63) is a direct, if careful, calculus exercise. The work lies elsewhere. Existence and uniqueness on the whole half-line do not follow from a single application of a local Picard–Lindelöf theorem: the vector field is globally Lipschitz in , but with a constant of order , which grows like when . A local existence theorem on a short interval does not by itself give a solution on , and uniqueness must hold relative to with one-sided derivatives at . Passing from the differential inequality (59) to (60) requires to be differentiable relative to , including the endpoint , and the integrand to be continuous, so the regularity of the solution has to be carried through every step.
InnerProductSpace ℝ V, CompleteSpace V); the paper's duality pairing and dual norm are the inner product and the norm (Riesz).gradf with HasGradientAt f (gradf x) x for every and gradf continuous; Mathlib's gradient is not used. includes and .derivWithin x (Ici 0)), so one-sided at . Every curve differentiated this way is assumed or on , so the junk value of derivWithin at a point of non-differentiability never enters.A complete development needs: a global existence and uniqueness theorem for Lipschitz non-autonomous ODEs on with locally bounded Lipschitz constant (Mathlib's IsPicardLindelof and ODE_solution_unique_of_mem_Icc are the starting points), and one-sided calculus for and . The global existence result for half-line ODEs is reusable well beyond this mission. Contributions are welcome on any milestone independently.
Douglas–Rachford splitting (DRS) minimizes a sum by alternating between the proximal mappings of the two terms. It is one of the most used first-order methods in signal processing, statistics and control, and, through its dual interpretation, it is the engine behind the alternating direction method of multipliers (ADMM). For convex problems its convergence theory is classical. In nonconvex problems — sparse regression with penalties, rank constraints, phase retrieval, feasibility problems with nonconvex sets — DRS is used routinely, but its theory is recent and depends on how the stepsize and the relaxation are chosen.
Themelis and Patrinos (SIAM J. Optim. 30(1), 2020; preprint arXiv:1709.05747v4) prove that when is -smooth and -hypoconvex and is merely proper and lower semicontinuous, DRS converges subsequentially to stationary points for stepsizes and relaxations in an explicit range. Their §4.2 then shows that these ranges cannot be enlarged: it constructs problems on which DRS fails as soon as the stepsize or the relaxation leaves the range. This mission formalizes that tightness half.
Timeline. Lions and Mercier (1979) proved convergence of DRS for maximal monotone operators. Li and Pong (Math. Program. 2016) gave the first nonconvex analysis, for and a stepsize bound well below . Themelis and Patrinos (2017–2020) introduced the Douglas–Rachford envelope, extended the analysis to all relaxations, reached the bound , and proved with the examples of §4.2 that the bounds are tight.
Write . A function is proper if it is never and finite somewhere. A differentiable is -smooth if is -Lipschitz, and -hypoconvex if is convex; an -smooth function is -hypoconvex for some , and is strong convexity.
The proximal mapping of with parameter is the set
which may be empty or contain several points. Given , one DR-iteration with stepsize and relaxation maps to through
A DRS run is a sequence obtained by iterating this step with any selection from the proximal sets. Its residual is . A point is a fixed point if some admissible step gives .
The paper's standing assumption (Assumption I) is: is -smooth and -hypoconvex, is proper and lower semicontinuous, and . The positive result needs ; Theorem 4.7 asks what happens beyond it.
For every , and there are and satisfying Assumption I such that
The pair may depend on , and only, never on , or the starting point.
For every , and there are , with additionally strongly convex such that, for every , every and every run, either is a fixed point or the residual does not vanish. A further milestone is the expansion identity from its proof.
The result. Theorems 4.7 and 4.8, together with the paper's convergence theorem, give a sharp map of the parameters for which nonconvex DRS is guaranteed to work under Assumption I. For practitioners they say that the stepsize cannot be traded for a larger one without structure on , and that over-relaxation beyond fails even when is strongly convex. The paper's Theorem 4.9 summarizes these facts as tightness of the bound .
Formalizing it. The results are proved on paper but not machine-checked anywhere. The formalization contributes a precise, selection-robust statement — the claim covers every run, including runs through points where a proximal set has two elements — and records two places where the printed statement and the proof do not match (see Formalization scope). Explicit proximal computations for piecewise-quadratic functions and indicators of finite sets, which the milestones need, are reusable for other counterexamples in splitting methods.
The claim is about every run, not one. A proximal set may contain two points, and a counterexample that works for one selection can fail for another. This is exactly what happens at in the paper's example: one admissible selection stays at a minimizer for ever.
The second difficulty is the dimension: the paper's functions live on while the theorems are stated on , and the construction has to be lifted so that the extra coordinates neither create fixed points nor make the residual vanish. Finally, for and large the proximal mapping of is empty or multivalued, so the analysis of a run must not assume a closed-form update.
is EuclideanSpace ℝ (Fin p); is real-valued and is EReal-valued and never . The proximal mapping is a set and a run is any selection; no proximal function is chosen. Every reciprocal bound is multiplied out: is 1 < γ * L, is γ * L < 1, is γ * negPartR σ < 1, so that imposes no constraint. The milestones are stated on , as in the paper.
Departures from the page, each disclosed in the items:
A formalization in which is improper, or in which the argmin is empty, would make the claim degenerate; properness and the argmin clause are part of the existential and rule that out. Weakening p4 to "some run" or "some starting point" is not this theorem.
Contributions welcome: proofs of the milestones (piecewise-quadratic proximal mappings, the prox of ), the lift from to , and the two theorems.
Nesterov's accelerated gradient method for -strongly convex, -smooth functions (NAG-SC) reaches accuracy in gradient steps, against for gradient descent (Nesterov, 1983; Nesterov, 2004). Polyak's heavy-ball method has the same accelerated behaviour on quadratics but not in general, and the two methods share the same classical continuous-time limit, the ODE . That limit therefore cannot explain why one method accelerates and the other does not.
Shi, Du, Jordan and Su (arXiv:1810.08907v3, 2018; Math. Program. 2021) keep the terms of the step size when passing to the limit. The resulting high-resolution ODEs differ between the two methods: the one for NAG-SC contains a gradient correction , a Hessian-driven damping term absent from the heavy-ball ODE. Their Theorem 1 shows that the high-resolution ODE of NAG-SC converges linearly at the accelerated rate , with an explicit constant tied to the step size.
Timeline. Polyak (1964) introduces the heavy-ball method; Nesterov (1983) the accelerated gradient method. Su, Boyd and Candès (2016) derive the low-resolution ODE of Nesterov's method for convex functions. Alvarez, Attouch, Bolte and Redont (2002) study inertial systems with Hessian-driven damping. Shi, Du, Jordan and Su (2018) obtain the high-resolution ODEs and the rates of their Theorems 1–6. Attouch, Chbani, Fadili and Riahi (2020) treat the closely related dynamics .
Let carry the Euclidean inner product and norm . For , is the class of differentiable convex functions , in the sense for all , whose gradient is -Lipschitz. adds that is with a Lipschitz-continuous Hessian . For , is the subclass of of -strongly convex functions:
Write for the minimizer of .
Fix a step size and a starting point . The high-resolution ODE of NAG-SC, (1.11), is
with and . The initial velocity matches the first step of NAG-SC. The Lyapunov function (2.4) is
In Lean these are IsS2 f μ L, IsNAGSCODE f μ s x0 X V (with V the velocity ) and lyap f μ s xs X V t, in the namespace HighResODE.NAGSCODE.
For , and every solution of (1.11), for all ,
Milestones 1–5 hold for every step size . The restriction enters only the goal and, through , milestone 6.
Theorem 1 is the continuous-time half of the paper's explanation of acceleration. With it gives , a linear rate at the accelerated exponent . The Lyapunov function (2.4) is the template from which the paper builds the discrete Lyapunov function (2.6) for NAG-SC itself, and the bracket in Lemma 3.1 is what that discretization uses (Remark 3.3). The heavy-ball ODE (1.10) lacks this term (Lemma 3.2), and that difference is the paper's account of why NAG-SC accelerates and heavy ball does not.
The result is proved in the paper; no machine-checked version is known. A formal proof needs a one-sided differential inequality along a trajectory in , a Grönwall-type integration, and an elementary but delicate rational inequality in . The milestones isolate each of these steps. The Lyapunov computation is also reusable for the sibling missions of this series on the heavy-ball and NAG-C ODEs.
The algebra in (3.4) is routine once the derivative exists. The work is in making that derivative rigorous. Differentiating needs the chain rule for and for . The second uses : the time derivative of is . All derivatives are one-sided at . Passing from to (3.2) needs a comparison argument on , not just a pointwise derivative bound. The constant of the goal rests on the coefficient inequality of milestone 6, and that inequality is tight: its left side tends to as , so no crude estimate closes it.
is EuclideanSpace ℝ (Fin n), is Mathlib's gradient f, and is fderiv ℝ (gradient f) x v. The classes are structures in the first-order form of p. 8. requires ContDiff ℝ 2 f and an existential Lipschitz constant for the Hessian, because the page fixes none. The minimizer is a point with for all .
A solution of (1.11) is a pair of curves with these properties:
Values for are irrelevant. Existence and uniqueness of the solution (the paper's Proposition 2.1) are not assumed: every statement quantifies over every solution. Derivative claims are stated as the existence of a one-sided derivative with the claimed value or bound, never through deriv, which returns where no derivative exists. The ODE predicate fixes as the derivative of , so cannot be chosen freely. The goal assumes only the ODE and the class, never the Lyapunov decay. The initial velocity uses as in (1.11); footnote 4 (p. 5) drops the , a printed slip.
All six milestones are stated. Solvers are welcome to work on any of them. A general one-sided Grönwall lemma on and the chain rule for would serve the other ODE missions of this series as well.