Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Every financial application in the rest of this book — terminal wealth maximization, portfolio choice with consumption, index tracking, hedging — takes as given that the underlying market admits no risk-free profit: an arbitrage opportunity. Ruling this out is not a modeling nicety but a structural necessity, since a market with arbitrage has no sensible notion of a fair price at all. Bäuerle and Rieder's Chapter 3 fixes the discrete- and continuous-time market vocabulary the rest of the book builds on, and proves the one structural fact about no-arbitrage that the later chapters actually invoke: that the whole-horizon, global absence of arbitrage is equivalent to a much simpler one-period condition, checked separately at each stage. This reduction — not the deeper fundamental theorem of asset pricing (existence of an equivalent martingale measure), which the book does not prove in this section — is what turns a statement about strategies over the whole time horizon into something checkable stage by stage, exactly the form needed to embed a no-arbitrage assumption into a dynamic-programming argument.
An -period financial market with risky assets consists of a probability space with filtration , trivial; a riskless bond with deterministic interest rate on (so ); and risky assets with relative price changes , -measurable and a.s. strictly positive (). A portfolio (trading strategy) is an -adapted process , , ; is the money invested in asset on . Its value before/after trading at time is , ; is self-financing if a.s. for every interior . An arbitrage opportunity is a self-financing with , a.s., with positive probability. The relative risk process is the excess return of asset over the riskless rate.
This is the weakest stable statement that captures the reduction: it asserts the equivalence of the global, whole-horizon absence of arbitrage strategies with a one-period static condition on the relative risk vector, without asserting the stronger (and here unproved) existence of a martingale measure.
No further milestone is formalized in this mission: this chapter's only other theorem, Theorem
3.3.1 (binomial-tree weak convergence to Black-Scholes), needs the Skorokhod topology on the
space of càdlàg paths, absent from Mathlib and out of scope to construct here — see the
Formalization scope section and HARD.md.
Theorem 3.1.5 is the tool that lets every later chapter's "assume the market has no arbitrage" hypothesis be checked and used one period at a time rather than as a global existential statement over an intractably large space of strategies. It is also the precise, minimal claim this section proves: contrasted with the full fundamental theorem of asset pricing (no arbitrage existence of an equivalent martingale measure, due to Harrison–Kreps 1979 and Dalang–Morton–Willinger 1990 in this discrete-time generality), Theorem 3.1.5 is a strictly weaker, purely measure-theoretic reduction that requires no separating-hyperplane or martingale-measure construction to state (only to prove). The definitions this chunk formalizes alongside it — portfolios, self-financing, arbitrage, and utility functions with the Arrow-Pratt risk-aversion coefficient — are the vocabulary every financial mission of this book (Chapters 4, 6, 9, 11) is built from.
Formalizing it contributes the exact discrete-time, filtration-indexed statement of the
reduction — a result absent from the platform (searched "arbitrage", "self-financing",
"martingale measure", "utility function"; the one related hit,
LinearOptimization.no_arbitrage_iff_state_prices, is a static single-period linear-programming
duality statement — no-arbitrage iff nonnegative state prices exist for a fixed return matrix —
a different equivalence for a different, non-stochastic model, not reused here).
The direction "local no-free-lunch at every stage no arbitrage" is the easy one: an arbitrage strategy, unwound via the recursive wealth formula, forces a violation of the local condition at some stage by a stopping-time argument on the first period where the wealth increment is a.s. nonnegative and not a.s. zero. The converse, "an arbitrage opportunity forces the local condition to fail somewhere," is the direction that needs the reduction of the whole-horizon problem to a single period: the natural first attempt (induct forward from ) does not directly work, because whether a strategy is an arbitrage is a statement about the terminal wealth , and a violation at an early stage does not obviously propagate; the book's proof instead identifies, from an arbitrage strategy, the last stage at which the one-period condition fails and constructs a genuinely one-period arbitrage there — an argument that needs care with the a.s.-qualifiers at every step (the difference between " a.s." failing to imply " with positive probability" only up to null sets is exactly where the measure-theoretic bookkeeping matters).
The market is represented via DiscreteFinancialMarket, bundling the probability space,
filtration, and the two primitives (, ) actually used; price processes
are not separately represented, since they would only be running products of these two
primitives with no further role once the relative risk process is derived. Filtration is
represented directly as a monotone family of sub--algebras with a trivial Fam 0, not
via Mathlib's Filtration structure, to avoid instance-juggling that would add no content here.
Adaptedness/predictability and the a.s. conditions of every definition are exactly the book's
own. Definitions 3.2.1-3.2.2 (the continuous-time portfolio and its self-financing condition,
needed by chunk 09b's jump-market model) use an abstract StochasticIntegral operator taken
as given data, since Mathlib has no general theory of integration against an arbitrary càdlàg
semimartingale (only specific constructions such as Itô integration against Brownian motion);
this is a deliberate infrastructure gap flagged for whoever eventually needs to instantiate it,
not a hidden simplification of the definition's own content, which states the self-financing
equation exactly as the book writes it.
Theorem 3.3.1 is not formalized in this mission and is recorded in HARD.md. The theorem
asserts weak convergence of the whole path of the binomial-tree price process to the
Black-Scholes-Merton stock price on the Skorokhod space of càdlàg functions with the
Skorokhod topology — a materially stronger and more setup-heavy claim than finite-dimensional
convergence in distribution, and the book explicitly names this topology (it is not left
implicit). Mathlib has no formalization of or the Skorokhod topology, and building
either from scratch (the space of càdlàg functions, the Skorokhod metric via time-warpings, the
tightness criteria needed for Donsker-type invariance principles) is a substantial undertaking
outside the scope of a single milestone; weakening the claim to convergence of
finite-dimensional distributions, or silently substituting an unnamed alternative topology
(e.g. uniform convergence, under which the claim would in fact be false, since the discretized
paths have jumps the limit does not), would misstate the theorem rather than state a smaller
piece of it faithfully. A general-purpose Skorokhod-space/Skorokhod-topology formalization in
Mathlib — reusable well beyond this book — is the prerequisite contribution that would unlock
this result.
No trivializing formalization: NoArbitrage quantifies over all self-financing portfolios
(Portfolio M, an unrestricted adapted process, not a finite or parametrized family), and the
one-period condition of part b) quantifies over all -measurable — narrowing either quantifier (e.g. to strategies with bounded positions) would
state a weaker, easier claim than the book's own theorem.
Supervisory control theory, introduced by Ramadge and Wonham (SIAM J. Control Optim. 25(1), 1987), models a manufacturing cell, a communication protocol or a resource-sharing system as an automaton whose transitions are events, some of which an external controller may disable. A controller, the supervisor, is itself an automaton that watches the event sequence and, in each of its states, decides which controllable events are currently allowed. The framework is the standard model for logical (untimed) control of discrete event systems and is the subject of textbooks such as Cassandras and Lafortune (Springer, 2008) and Wonham and Cai (Springer, 2019).
A practical concern is supervisor size. The synthesis procedure of the paper (§9) produces a supervisor whose automaton records exactly as much of the past as the desired closed-loop language requires, but there are many other supervisors realising the same behaviour. The paper's second main result, the quotient structure theorem (Theorem 10.1, p. 223), explains how they are related: any supervisor with two natural economy properties is obtained from a canonical one, built on a recognizer of the closed-loop language, by lumping states. This is the structural starting point of the later literature on supervisor reduction.
A generator is : a state set , a finite alphabet of events, a partial transition function , an initial state and marker states . Extending to strings gives the generated language (strings along which is defined from ) and the marked language (those that end in ). The closure of a language is its set of prefixes. Throughout, is trim: . A recognizer for a language is an accessible generator whose marked language is .
A subset of events is controllable. A supervisor is where is an accessible deterministic automaton with possibly infinite state set and is a state feedback map; events outside are always enabled. The closed loop runs and in lockstep and allows from iff and are defined and . Its languages are , (marker set ) and .
is complete if never refuses an event that the plant can execute and enables: , and imply . It is proper if it is complete and .
A projection is a surjection with , , wherever is defined, and .
For a language , strings are -equivalent if for all . The automaton is -reduced if -equivalent strings of lead to the same state, and -trim if every state is reached by a string of .
Let be complete, , , with -reduced and -trim, and let be a trim recognizer for . Then there are and such that satisfies
Proposition 8.1 (p. 219): for complete and a projection , (i) is unique; (ii) ; (iii) is complete; (iv) nonblocking, nonrejecting and proper transfer in both directions.
The displayed steps of the proof of Theorem 10.1 (pp. 223–224): is well defined on ; it is a projection once and ; follows from two enablement conditions; is complete; and .
Theorem 10.1 says that the reduction properties the synthesis procedure of §9 guarantees are exactly what makes a supervisor a quotient of the canonical supervisor on a recognizer of . Combined with Proposition 8.1, which shows that a projection preserves every closed-loop language, completeness and properness, it identifies supervisors with the same behaviour up to state lumping. This is the basis on which supervisor reduction and the comparison of supervisor realisations rest.
The result is proved in the paper. What this mission produces is a machine-checked version of the model (generators with partial transitions, supervisors with infinite state sets, the closed loop, completeness and properness) and of the two results above. No formalization of Ramadge–Wonham supervisory control was found on Prove2Me at the time of drafting; the definitions of this mission are reusable by any later mission on the theory, including the synthesis results of the first mission of the series.
The mathematics is elementary; the difficulty is bookkeeping with partial functions. Every step compares runs of three automata (the plant, and the recognizer) that may be undefined at different strings, and a proof must track at each string which of them is defined. The tempting shortcut of treating the projection condition as full commutation, for all , is not available: the page asks for it only where is defined, and Proposition 8.1 (ii) holds only because completeness of compensates for transitions that has and lacks. Likewise, the map of Theorem 10.1 is defined through arbitrary representatives, and its well-definedness uses both that recognizes with all states marked and that is -reduced.
The alphabet is a Lean type α with [Fintype α] (the page's , which is Lean syntax); strings are List α, is s ++ [σ]. A generator is a structure with its own state type in Type and a partial transition δ : α → Q → Option Q; its extended transition is the left fold. The feedback map has type X → Ec → Bool, and " enabled at " means or ; the page's is the same object under this extension. The closed loop is run from without forming its accessible part, which changes none of its languages. Existential statements over supervisors quantify over state types in Type.
Standing assumptions that are hypotheses of every theorem: finite; trim, stated as 𝒢.L = pre 𝒢.Lm; every supervisor automaton accessible. Theorem 10.1 and its proof steps also assume complete, -reduced and -trim, and a trim recognizer for with all states marked, and is built on that given rather than on a recognizer chosen by the prover. The conclusion names and as the languages of , not as free variables. A projection predicate that drops , surjectivity or the marker equation would make the goal's clause (ii) trivially satisfiable by a constant map; the sanity check shipped with the mission rules this out on the primitive plant of §2.3.
Contributions welcome: proofs of the milestones, lemmas relating the fold-based extended transition to concatenation, and a reusable library for closed-loop runs.
Most concrete applications of Markov Decision Theory — inventory control, cash management, linear-quadratic regulation, sequential games — have data that does not change from one period to the next: the same state space, action space, transition mechanism and reward apply at every stage, only discounted by a fixed factor per period. Bäuerle and Rieder's Chapter 2, §2.5 specializes the general finite-horizon theory of the previous sections to this stationary case, and §2.6 shows the specialization at work on three classical models: a card game with a famously boring answer, a firm's cash-management problem, and stochastic linear-quadratic control. Together they demonstrate the payoff of the abstract theory: once the Structure Assumption is checked for a stationary model, the general machinery (the Forward Induction Algorithm) produces the concrete optimal policy — a critical-level -type control for cash management, a linear feedback law for LQ control — with no further case-specific argument.
A stationary Markov Decision Model is a Markov Decision Model (Definition 2.1.1) whose data does not depend on the stage: the reward at absolute time is and the terminal reward at time is , for a fixed discount . For a policy sequence (each a decision rule with ), the reward-to-go is and the value function is . The operators , , are the stationary counterparts of §2.3's non-stationary operators. The (stationary) Structure Assumption (SAN) asks for sets , with , , and every having a maximizer in .
A firm's cash level moves under i.i.d. shocks; each period the firm transfers to a new level at linear cost , pays a convex, coercive holding cost (), and the level becomes . Modeled as a stationary MDM with , , :
with , and the optimal policy transfers up to below it, down to above it, and does nothing in between. This is the weakest stable statement: it asserts the existence of critical levels with the stated recursive characterization, not any closed form for itself (which depends on 's exact shape and is not computable in general).
Three milestones build toward and alongside it: the Reward Iteration theorem and stationary Structure Theorem (Theorems 2.5.3-2.5.4, the general machinery instantiated), the trivial-but- sharp red-and-black card game (Theorem 2.6.1), and the stochastic linear-quadratic problem (Theorem 2.6.3, a Riccati-type recursion with random coefficients).
Theorem 2.6.2 is the textbook derivation of -type control, the dominant policy structure in inventory theory and cash management: a firm should act only when its state leaves a band, and should act to bring it exactly to the band's edge, never further. Its proof pattern — verify (SAN) with the convex functions of at most linear growth, extract the critical levels from the derivative conditions of a one-stage minimization — is the template used across the inventory-control literature for essentially every variant of this problem. Theorem 2.6.1's answer ("no strategy beats stopping immediately") is a genuine, if minimal, comparative-statics fact: a positive-content instance of collapsing to functions constant on the game's absorbing set, forcing every action to be a maximizer. Theorem 2.6.3's Riccati-type recursion, with random transition coefficients, generalizes the classical deterministic-coefficient LQR (linear-quadratic regulator) of control theory; the recursion governs mean-variance and quadratic-hedging problems return to in later chapters of this book (Chapters 4 and 6).
None of the three examples' specific results were found on the platform (searched for
"comparative statics", "convex Markov decision", the exact model names, and "bang-bang"/"LQR"
adjacent terms). BertsekasDP.riccati_completion_of_square is the platform's one close relative
to Theorem 2.6.3: it solves the deterministic-coefficient LQR by a completion-of-squares
argument, not the random-coefficient recursion here, so it is cited as related work rather than
reused. The proofs themselves are complete and self-contained in the book (a few pages each,
using only single-variable convex analysis and elementary linear algebra); this mission
contributes the formal statement of each, in its full generality (general convex , general
random coefficient pairs), as the task for a sorry-free proof.
The cash-balance proof's central step is showing the minimizer of the one-stage problem is of critical-level form for every in the candidate class — not just for the particular sequence that eventually arises. The obvious shortcut, guessing the form of directly and verifying it solves the Bellman equation by substitution, fails because are themselves defined only implicitly, via one-sided derivative conditions on ; there is no closed form to substitute except in degenerate special cases (e.g. quadratic). The genuine content is the general argument (convexity of the one-stage objective forces a unique critical-level minimizer structure, and this structure is preserved under ) that lets the induction go through for an arbitrary convex, coercive . For Theorem 2.6.3, the natural first attempt — solve the deterministic LQR recursion and substitute expected coefficient matrices for the random ones — is not obviously valid, since in general; the correct recursion genuinely involves the joint second moments of , which is exactly what the standing positive-definiteness assumption on (not on itself) is there to make precise.
The stationary vocabulary (StationaryMarkovDecisionModel, its operators, J, (SAN)) is
restated independently of chunk 02a's non-stationary vocabulary — drafts in this series cannot
import one another, and the book itself keeps the two notationally separate ( vs. ,
related by , a relation this mission does not separately formalize
since no listed result needs it). Theorem 2.6.3's stochastic LQ problem is explicitly
non-stationary in the book's own text, so a second, NS-prefixed restatement of the non-
stationary model and value function (via the Bellman recursion established as Theorem 2.3.8,
not the sup-over-policies primitive — the same simplification chunk 02c makes for its own V)
is introduced solely for that one theorem. The card game (Theorem 2.6.1) is formalized on the
concrete state space and action space Bool, with the model's
exact transition density, reward and terminal reward given as hypotheses on an abstract
StationaryMarkovDecisionModel, matching the book's own discrete-density notation
(introduced in the text following Theorem 2.5.4) rather than
built from an explicit PMF/Kernel construction — a lighter-weight but equally precise
formalization, since the density equations pin the kernel exactly. The stochastic LQ problem
uses Matrix (Fin m) (Fin m) ℝ and needs a MeasurableSpace (Matrix m n α) instance Mathlib
does not provide (Matrix is a non-reducible def for m → n → α); this mission supplies it by
transport across the definitional equality. Random matrix moments are
computed entrywise as ordinary Bochner integrals against the joint law of .
A trivializing formalization is ruled out on two fronts: the cash-balance critical levels
are existentially quantified as functions of , not fixed constants (dropping
the index would silently claim a single band works for every horizon length, which is false in
general); and the card game's "every strategy is optimal" is stated as a universally-quantified
claim over all policy sequences, not weakened to mere existence of an optimal one. Reusable
infrastructure: the jointMatMean/xQx helpers and the MeasurableSpace (Matrix m n α)
instance are generic and available to any later chunk needing random-matrix moments (none of the
remaining chunks' briefs currently list one, but Chapter 4's mean-variance and LQ-flavored
missions may). sorry-free proofs of all five items are welcome contributions; Theorem 2.5.3's
short inductive proof (unwinding the accumulator definition against the operator-composition
recursion) is likely the easiest entry point.
BertsekasDP.riccati_completion_of_square
on the platform).Single-machine sequencing with deferral costs asks how to order jobs when the price of finishing a job depends on when it finishes. A job completed at time incurs the cost ; lateness penalties, holding costs and service-level penalties are special cases. Two objectives are standard: the sum of the costs, studied by McNaughton (Management Science 6(1), 1959) and Lawler (Management Science 11(2), 1964), and the maximum cost, the bottleneck objective, which asks that no single job be charged too much.
At the end of his 1968 paper on minimizing the number of late jobs (Moore, Management Science 15(1)), J. M. Moore added a short section, suggested by E. L. Lawler, showing that the maximum-cost problem reduces to a family of feasibility problems with due-dates. Each such problem is settled by one sort, by Jackson's earliest-due-date rule (J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, UCLA Research Report 43, 1955). This reduction is the unconstrained case of what later became Lawler's algorithm for (Lawler, Management Science 19(5), 1973).
Timeline:
A finite nonempty set of jobs is processed on one machine that starts at time and runs without idle time or preemption. Job has processing time . A schedule is an ordering of with each job appearing exactly once, and is the completion time of in : the sum of the processing times of and of every job before it.
Each job has a deferral cost , which is continuous, bounded and non-decreasing. The maximum deferral cost of is
For a cost level , the generalized inverse is the latest time at which job can be completed at cost at most . Following the paper's definition (p. 108), with times :
For each , is a schedule ordered by the "due-dates" , with ties broken arbitrarily. has no late jobs if for every .
In Lean these are IsSchedule, completionTime, Pstar, NoLateAt and maxCost in the namespace MooreLateJobs.MaxDeferral.
Let satisfy: (1) has no late jobs; (2) for every , has at least one late job. Then for every schedule of ,
This is the last sentence of the section (p. 109). The goal takes with its two properties as given, so it needs no hypothesis beyond the model.
The result. The theorem turns a min–max problem over all schedules into a monotone one-parameter feasibility question. Each value of is checked by a single sort, and the optimal level is the threshold where feasibility switches on. The same threshold structure underlies bottleneck scheduling and the backward rule for . Special cases include minimizing the maximum lateness, , clipped to be bounded, and minimizing the maximum weighted tardiness.
Formalizing it. The result is classical and proved on paper, but no machine-checked proof of it, or of Jackson's lemma, is known to exist. The mission would produce a checked Jackson lemma for extended-real due-dates, a verified generalized inverse of a monotone continuous function with the paper's case analysis, and the threshold argument connecting them. Jackson's lemma is shared with part I of this series (minimizing the number of late jobs).
The reduction is short on paper. The work is in the edge cases that the paper passes over:
Conventions committed to in Lean:
ι with decidable equality, and the job set is J : Finset ι, assumed nonempty in the goal. Processing times are t : ι → ℝ with 0 ≤ t i: this is added, because the page never states it but processing times are durations.P : ι → ℝ → ℝ, each continuous, bounded (∃ M, ∀ s, |P i s| ≤ M) and monotone, as on p. 108. The Introduction's assumption has no counterpart, since the problem has no given due-dates, and it is not assumed.Pstar f y : EReal, with every time in the definition ranging over . If the level set is unbounded, its "max" does not exist, and the value is fixed to . The final case is "otherwise", which for continuous monotone is the paper's case (c).SD : ℝ → List ι such that SD y is a due-date-ordered schedule for every . Theorems hold for every such family, so every tie-break is covered.The goal is not the trivializing statement "every on-time is optimal", which is false for large . It concerns exactly the threshold level . The minimum is over all schedules of , not over the only.
The needed infrastructure is list permutations, prefix sums and Finset.sup', plus basic facts about sSup of closed sets bounded above in ℝ, and the intermediate value theorem. The Jackson lemma and the generalized inverse are reusable beyond this mission. Contributions are welcome on any milestone, in any order. The goal depends only on the Jackson lemma and on properties of Pstar.
Not in scope: the remark that "can be found to whatever accuracy is desired by a binary search technique" (computational), and the sum-of-costs problem the section contrasts itself with.
Quadratic minimization problems with a combinatorial sign pattern in their Hessian arise throughout applied mathematics: discretizations of elliptic boundary-value problems such as the Poisson equation, resistor-network energy functionals, and the Dirichlet forms of Markov-process potential theory all produce a symmetric matrix whose off-diagonal entries are nonpositive and whose rows are diagonally dominant (Fukushima, Oshima, and Takeda, Dirichlet Forms and Symmetric Markov Processes, De Gruyter, 1994). Such matrices are exactly the diagonally dominant symmetric M-matrices of classical numerical linear algebra (Berman and Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994). Murota's Discrete Convex Analysis (SIAM, 2003) identifies the combinatorial content of this sign pattern with a discrete convexity property — submodularity, and its strengthening translation submodularity — of the associated quadratic form, and shows that passing to the Legendre-Fenchel conjugate of such a quadratic form (i.e., inverting the matrix) transports this property to a dual combinatorial property, an exchange axiom, on the conjugate side. This mission formalizes that correspondence for the special, matrix-algebraic case of quadratic forms — the case in which Murota's book gives a self-contained proof using only the classical Farkas lemma, before generalizing the same conjugacy to a much broader class of functions in Chapter 8.
Let be a finite ground set (identified with in the book) and let be a symmetric real matrix. has off-diagonal nonpositivity if for all , and diagonal dominance if for every row . The associated quadratic form is for . For write , for the componentwise maximum and minimum. A function is submodular if for all , and has translation submodularity if the stronger inequality holds for every , where is the all-ones vector (ordinary submodularity is the case ).
On the conjugate side, for write , , and let denote the -th unit vector ( denotes the zero vector). A function has the exchange property if for all and there exist and such that for every . The Legendre-Fenchel conjugate of is ; two functions are conjugate to each other when and . For positive-definite symmetric , the quadratic forms and are conjugate to each other exactly when and are matrix inverses of one another.
Goal (Theorem 2.11). For conjugate strictly convex quadratic forms and as above,
This is the mission's capstone: the statement leaves the correspondence at the level of the two named combinatorial properties, without hard-coding which of the two properties is verified in a given application, so it survives exactly as strongly as the underlying conjugacy fact does.
Supporting milestones, in the order the book develops them: Proposition 2.4 (off-diagonal nonpositivity plus diagonal dominance implies positive semidefiniteness); Proposition 2.6 (off-diagonal nonpositivity is equivalent to plain submodularity of ); Theorem 2.7 (the full sign pattern is equivalent to translation submodularity of ); Proposition 2.9 (conjugate quadratic forms correspond exactly to inverse matrix pairs); Theorem 2.12 (a nine-way equivalence, for a nonsingular symmetric , among membership in the matrix class , two sign-consistency inequalities on the columns of together with their strict forms, two directional-derivative reformulations of the exchange property together with their strict forms, and the exchange property itself together with its strict form); Proposition 2.13 (the Farkas lemma in equality form, together with the strict variant valid for a nonsingular coefficient matrix); and Proposition 2.14 (the class is closed under taking principal submatrices).
The M-natural exchange property is the function-level analogue of the base-exchange axiom for matroids, and translation submodularity is the analogue, on the "primal" side, of ordinary submodularity for set functions; Chapter 2's quadratic-form case is the historical and pedagogical entry point for the general conjugacy Chapter 8 proves for the full M-convex/ L-convex function classes. Establishing it here, in the self-contained matrix-algebraic setting, isolates exactly which properties of a quadratic form are combinatorial (tied to the coordinate axes) rather than purely convex-analytic (rotation-invariant): submodularity and the exchange property are not preserved by an orthogonal change of variables, in contrast to ordinary convexity, which Proposition 2.4 shows the same sign pattern also implies.
Formalizing this mission produces the first Lean statement, in this project's namespace, of a genuine conjugacy theorem between a primal-side and a dual-side combinatorial convexity property for a concrete function class; nothing of this kind is yet proved (or, so far as the platform's own search shows, formalized at all) elsewhere on the platform. The nine-way equivalence of Theorem 2.12 is a substantial independent contribution beyond the goal itself, since it is what makes the goal's proof possible via elementary linear algebra rather than the general convex-analytic machinery Chapter 8 needs.
The naive approach to Theorem 2.11 tries to derive the exchange property for directly from the defining supremum in the conjugate relation , differentiating under the sup; this fails because the exchange property compares along a specific combinatorial direction tied to two coordinates, not along an arbitrary direction, and no naive first-order argument isolates the right pair without already knowing the sign pattern of . The book's actual route is Theorem 2.12: it reduces the exchange property to a column-wise sign-consistency statement on itself (conditions (b)/(c)) via the identity , and closes the loop back to membership in using the Farkas lemma applied to the linear system — a genuinely matrix-algebraic argument that does not generalize verbatim to non-quadratic M-/L-convex functions, which is exactly why Chapter 8 needs a different (convex-analytic) proof for the general case.
Vectors and matrices are indexed by a general finite type V ([Fintype V] [DecidableEq V])
rather than a fixed Fin n, matching this project's convention elsewhere and letting
Proposition 2.14's principal-submatrix statement reuse the class predicate at the restricted
index type directly. Quadratic forms are real-valued ((V → ℝ) → ℝ, using Matrix.mulVec and
dotProduct) since this chapter's functions are always finite everywhere; the Legendre-Fenchel
conjugate is EReal-valued via sSup, since a supremum over an infinite domain need not be
finite in general even though it is finite here. Every min(0, \dots)-based condition in
Theorem 2.12 and the exchange axioms is unfolded as the logically equivalent disjunction over the
finitely many terms achieving the minimum, rather than reified via Finset.inf/WithTop
machinery — a faithful, checked-equivalent simplification, not a narrowing (see
MODERATION_NOTES.md). "Nonsingular" is Matrix.det ≠ 0. No numeric constant needs
instantiation anywhere in this mission. The formalization does not trivialize: the goal's
exchange property is stated for the specific combinatorial direction with , — not an arbitrary
direction, which would reduce the exchange property to a restatement of ordinary convexity and
discard the entire combinatorial content the mission is about.
Infrastructure needed: Matrix.PosDef/Matrix.PosSemidef/Matrix.IsSymm (present in Mathlib);
everything else (submodularity, translation submodularity, the exchange axioms, the
sign-consistency conditions) is defined fresh in DiscreteConvex.CombinatorialB. A solution to
the goal will likely want Proposition 2.9, Theorem 2.12, and the Farkas lemma (Proposition 2.13)
as lemmas; contributions completing any of the seven milestones independently, or supplying the
Schur-complement induction behind Proposition 2.4, are welcome.
Monotone variational inequalities cover convex minimisation, convex–concave saddle-point problems, Nash equilibria of monotone games and complementarity problems, and they are the standard model for these in optimization and operations research. First-order methods for them (extragradient, forward–backward–forward, reflected and projected gradient methods) need a stepsize below , where is a global Lipschitz constant of the operator. That constant is often unknown, too pessimistic, or nonexistent: in composite minimisation with a locally smooth term, or in saddle-point problems with bilinear-plus-nonlinear couplings, the operator is only locally Lipschitz. The usual remedy is a linesearch, which costs extra operator or prox evaluations per iteration and complicates the complexity accounting.
Y. Malitsky, Golden Ratio Algorithms for Variational Inequalities (preprint 2018, Optimization Online 6598; published in Mathematical Programming, 2020, doi:10.1007/s10107-019-01416-w) proposes the Explicit Golden Ratio Algorithm (EGRAAL): its stepsizes are computed in closed form from the last two iterates, it uses one evaluation of and one proximal step per iteration, and it needs neither a Lipschitz constant nor a linesearch. This mission formalizes its main convergence theorem, Theorem 2 of the preprint.
Let be a finite-dimensional real inner product space with norm . Let with domain , and . The variational inequality (1) asks for
Its solution set is . The standing assumptions are: (C1) ; (C2) is proper, convex and lower semicontinuous; (C3) is monotone on , for .
The proximal operator is . Write for the golden ratio. Algorithm 1 (EGRAAL) takes , , a parameter and a cap , sets , , , and for computes
with the convention in the middle term. The paper uses the bifunction .
If is locally Lipschitz continuous and (C1)–(C3) hold, then for every run of Algorithm 1 there is with
Nothing is fixed beyond the paper's parameter ranges: , , and the starting points are arbitrary. The two sequences share one limit.
The result. Theorem 2 shows that a monotone variational inequality with a locally Lipschitz operator can be solved by a method whose stepsizes adapt to the local curvature of at no extra cost: one evaluation and one prox step per iteration, and no global constant and no backtracking. Because is only ever evaluated at the prox outputs , the method also applies when is undefined or badly behaved outside the feasible set, where reflected-gradient methods can fail. The same analysis gives an ergodic rate and, under an error bound, an -linear rate (§2.2 of the preprint; not part of this mission). The paper also derives fixed-point algorithms for demi-contractive operators from it.
Formalizing it. The theorem has a published proof; to our knowledge no machine-checked version exists, and Mathlib has no proximal operator, no theory of monotone variational inequalities and no Fejér-monotonicity lemma. This mission produces a formal convergence proof for an adaptive first-order method with a nonsmooth convex term, together with reusable pieces: the prox-inequality for extended-real-valued convex functions, a finite-dimensional Fejér convergence lemma, and a formal model of an adaptive-step algorithm with the rule.
The usual convergence argument for projected or extragradient methods bounds the cross term using a global Lipschitz constant and a fixed stepsize. Here neither exists. The stepsize at iteration depends on the iterates, and the energy that decreases changes from step to step, since it involves . Local Lipschitz continuity gives a usable constant only once the iterates are known to be bounded, and boundedness has to come from the energy inequality. Stepsizes that tend to would also break the argument (Lemma 2 excludes this for bounded runs). The last step, identifying cluster points as solutions, needs lower semicontinuity of and a limit in the prox-inequality along a subsequence with convergent stepsizes.
is a real InnerProductSpace with FiniteDimensional ℝ E. is a map E → EReal; (C2) is a structure: never takes the value , is finite somewhere, has a convex epigraph in , and is LowerSemicontinuous on . is a total map E → E, and every hypothesis on it (monotonicity, Lipschitz bounds) is restricted to . The variational inequality is stored as , with , which avoids extended-real subtraction. is an argmin predicate, so it never produces a junk value. The algorithm is a predicate on the four sequences, written for index . The rule is a case split: if the step is . No condition such as or is imposed.
"Locally Lipschitz" is formalized as Lipschitz on every bounded subset of . This is the property the proof of Lemma 2 uses. It agrees with local Lipschitz continuity when is closed (for example for a closed convex , or finite everywhere) and is stronger otherwise. Eq. (27) is stated for , where and are defined. Lemma 1 carries the hypothesis of its cited source, without which it is false.
The statements are not vacuous: , satisfy (C1)–(C3) and the Lipschitz hypothesis, and admit a run of Algorithm 1 with . A proof of Theorem 2 must hold for every run with the paper's parameters, not only for such degenerate data.
Contributions welcome: the prox-inequality and the existence of the prox for proper convex lsc (both reusable beyond this mission), the Fejér lemma, the algebraic estimates (18) and (24), and the energy inequality (27). Once these are in place, Lemma 2 and the cluster-point argument complete Theorem 2.
Newton's method converges quadratically near a non-degenerate minimum, but on its own it has no global guarantee: far from a minimizer the Newton step may increase the objective, and at points where the Hessian is indefinite it may not even be a descent direction. For most of the method's history, the global behaviour of second-order methods was controlled by line searches or trust regions whose worst-case complexity was not quantified.
Nesterov and Polyak (Math. Program. Ser. A 108 (2006) 177–205) proposed regularizing the Newton model by a cubic term and proved global worst-case rates for the resulting method on several problem classes. This mission is the third in a series formalizing that paper. It concerns the class of gradient dominated functions of degree two, for which the gap to the optimal value is bounded by a multiple of the squared gradient norm. For this class the paper shows that the method first converges linearly and then superlinearly, with explicit constants and without convexity.
The class itself predates the paper by four decades. Polyak (USSR Comput. Math. Math. Phys. 3 (1963)) introduced the inequality to prove linear convergence of gradient descent without convexity; related inequalities are due to Łojasiewicz. Under the name Polyak–Łojasiewicz condition it has become a standard assumption in the analysis of first-order methods, for example in Karimi, Nutini and Schmidt (2016). Theorem 7 of Nesterov and Polyak is the corresponding result for a second-order method.
Let be a closed convex set, and let be twice differentiable on with gradient and Hessian . The Euclidean norm is , and on matrices it is the spectral norm. The standing assumptions of the paper are:
For the cubic model of at is
A cubic-regularized Newton step is any global minimizer of over . Write and .
Method (3.3). Fix . At iteration , choose such that , and set . The choice always passes this test.
Gradient domination of degree two (Definition 3 with ). The function attains its minimum over at some , and for a constant
The minimizer need not be unique. Two examples:
Two quantities appear in the targets. With , they are
For every run of method (3.3) on a gradient dominated function of degree two, both of the following hold.
The constants , , and are the paper's, and neither weakened nor improved.
In the order a proof would use them:
The result shows that on the Polyak–Łojasiewicz class, cubic regularization has two properties at once.
As the authors note, this is the only class in the paper where the initial gap enters the complexity of the first phase polynomially, through .
The result has been proved on paper since 2006. As far as the platform's catalog shows, none of the paper's statements has a machine-checked proof. This mission produces:
Once Lemma 7 and the recursion (4.17) are in hand, deriving the two rates is elementary scalar analysis. The difficulty sits upstream.
The second-order condition. Proposition 1 is a statement about the global minimizer of a nonconvex function of variables. The first-order condition (2.5) alone does not give it: a stationary point of the cubic model that is not a global minimizer can violate it. The inequality (2.11) on which every rate rests needs Proposition 1.
Lemma 7 needs two facts. First, the new iterate stays in , where the Lipschitz bound applies. Second, the monotonicity of on , which lets the unknown be replaced by .
The phases. Both need bookkeeping with nonnegative quantities under fractional powers. Along a run, the gap must be shown to be nonnegative and non-increasing before any power of it is taken.
The following conventions are fixed:
EuclideanSpace ℝ (Fin n) with arbitrary . The gradient and Hessian are maps g and H, with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every . At boundary points these are two-sided derivatives. The Lipschitz condition uses the operator norm on E →L[ℝ] E, which is the spectral norm.T is a global minimizer of the cubic model", and every lemma about is stated for every such T. The value is written as plus the model at that minimizer, with no infimum over an expression.Real.rpow of nonnegative numbers.Trivializing formalizations are ruled out. Using a stationary point in place of a global minimizer of the model, allowing , or requiring the domination inequality on all of rather than on would each change the theorem. None of these is done. A worked instance (, ) checks that the hypotheses are satisfiable.
A complete development needs Taylor estimates for a map with Lipschitz derivative on a convex set, the optimality conditions of the cubic subproblem (Section 5 of the paper characterizes its global minimizers through a one-dimensional dual problem), and some real-power arithmetic. The Section 2 lemmas are reusable for every other mission in the series and for any analysis of cubic-regularized or trust-region methods. Contributions are welcome at every level:
Newton's method converges quadratically near a non-degenerate minimizer, but classical theory says little about its behaviour far from one: the pure Newton step can move uphill, diverge, or be undefined when the Hessian is singular. For decades the global analysis of Newton-type methods consisted of convergence statements without rates. Nesterov and Polyak (Math. Program. 108, 2006) replaced the quadratic model of Newton's method by a cubic-regularized model and proved, for the first time, global worst-case complexity bounds for a second-order method on several problem classes, including classes of non-convex functions.
This mission covers one of these results: on star-convex functions, the method reduces the optimality gap at the rate (Theorem 4 of the paper). Star-convexity is a weakening of convexity that only asks for convexity along segments towards the global minimizers. It includes non-convex functions such as on , and, as the paper notes, it arises in sum-of-squares problems such as .
Timeline.
Let be a closed convex set with nonempty interior, and let be twice differentiable on , with gradient and Hessian . A starting point is fixed, and is assumed large enough to contain the level set in its interior. Assumption 1 is that the Hessian is Lipschitz continuous on with constant :
where the matrix norm is the spectral norm.
For a parameter and a point , the cubic model is
The cubic step is any global minimizer of over (Eq. (2.4)), and is the model value.
Method (3.3) takes parameters . At iteration it finds such that , and sets . The choice always passes the test.
A function is star-convex (Definition 1) if its set of global minimizers is nonempty and, for every , every and every ,
Write for the optimal value, and when is bounded.
Assume is star-convex, is bounded with , and . Then every run of method (3.3) satisfies
The constants are those printed on p. 189. The bound depends on the problem only through and ; the lower parameter and the choice of within are free.
The result. Theorem 4 gives a global function-value rate for a second-order method on a class that contains non-convex functions, with no assumption on the Hessian at the minimizer. The method needs no knowledge of the class: the same iteration (3.3) that yields second-order stationarity rates on general functions yields on star-convex ones. This adaptivity is the paper's main message for Section 4. The analysis also serves as the template for Theorems 5, 8 and 9 of the paper (star-convex with a non-degenerate minimum, and the convex case).
Formalizing it. The theorem has been proved in the paper, and to our knowledge it has not been machine-checked. A complete formalization produces:
These are the pieces needed for the paper's other rates and for later variants (accelerated and adaptive cubic regularization).
The argument has three parts, and each needs some care.
The first is the Taylor bound (2.3) on a convex set , under a Hessian that is Lipschitz only on . The Hessian is given as the derivative of a gradient map, not as a smooth function on all of .
The second is keeping the iterates inside . Lemma 4 and the diameter bound apply only to points of . So the iterates must be shown to stay in the level set, and the points used in the estimate must also lie in .
The third is the passage from the one-step inequality to the explicit constant in (4.2). The one-step inequality is a minimum over of a cubic in . It has two regimes (the unconstrained minimizer lies inside or beyond it), and the recursion for must be carried through without losing the constant or the factor . A generic "sublinear recursion" lemma gives the rate only up to a constant, which is not the printed theorem.
EuclideanSpace ℝ (Fin n) with arbitrary. The gradient and Hessian are maps g and H with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every . These are two-sided derivatives, also at boundary points of ; the iterates lie in . The Hessian norm is the operator norm.IsCubicStep). Every statement about it holds for every such minimizer.IsCubicNewtonRun, with a 0-based index.IsStarConvexFn quantifies over , as in display (4.1). It requires and the inequality for every global minimizer.Metric.diam F, with Bornology.IsBounded F as a hypothesis. It is the diameter of itself, not of the level set.Ruling out trivial formalizations. Without the boundedness hypothesis, Metric.diam F is , and the goal would assert outright. The formalization keeps boundedness, the nonemptiness of and the global-minimizer reading of , so that the hypotheses describe the paper's class and not a degenerate one. The hypotheses are satisfiable: for example, on with the closed unit ball, and .
Contributions are welcome at every level: proofs of the milestones, and general-purpose lemmas on Taylor bounds with a Lipschitz Hessian on convex sets. Those lemmas are reusable for missions I, III and IV of this series, which formalize the paper's other rates.
The edit distance between two strings is the least total cost of a sequence of single-character insertions, deletions and replacements that turns one string into the other. It underlies spelling correction, sequence alignment in computational biology, and file comparison. Wagner and Fischer (J. ACM 21, 1974) computed it for strings of length in time by filling an matrix. Masek and Paterson (J. Comput. System Sci. 20, 1980) lowered this to with a "Four Russians" block method: the matrix is cut into blocks, and the effect of every possible block is tabulated in advance.
The tabulation only pays off if the number of possible blocks is small. The paper guarantees this under two hypotheses: the alphabet is finite, and the edit costs are discrete, that is, all integer multiples of one constant. Its §4 asks whether discreteness can be dropped, and answers no with an explicit example whose costs are , , and . This mission formalizes that example.
Timeline:
Let be an alphabet and the null string. An edit operation is a pair of strings of length at most one other than : a replacement when both are symbols, a deletion when , an insertion when . results from by if and . A cost function assigns a nonnegative real to each edit operation; , , . The edit distance is the minimum of over sequences of edit operations taking to . For fixed strings, , where ; this is the edit matrix. A step is the difference of two horizontally or vertically adjacent entries, or , and the possible steps of are the steps of all edit matrices of all pairs of strings. The cost set is discrete if some has every element of as an integer multiple.
An edit path is a sequence of matrix cells in which each cell increases , or both by one: a deletion of (cost ), an insertion of (cost ), or a replacement of by (cost ). The eccentricity of is .
The example. with
Let . The infinite strings and are and with a written into both, at each even position where , so that and each contain exactly letters . The first is at position . is the minimum cost of an edit path from to through points all of eccentricity at least .
For the example's , and ,
The first part gives at least distinct steps in the edit matrix of and ; the second is the negation of the conclusion of the paper's Lemma 4. The goal fixes no constants and no growth rate beyond "at least one new step per diagonal position".
A further item records that the example satisfies every other condition of the paper: its costs are nonnegative and normalized (), but is not discrete.
The block algorithm precomputes one table entry per block and per pair of initial step vectors, so its preprocessing is polynomial in only when the number of possible steps is bounded independently of the strings. The example shows that without discreteness the steps can grow with even over a three-letter alphabet with nonnegative normalized costs, so the table size becomes of order and the method gives no speedup. It explains why the finite-alphabet, non-discrete case is left open in the paper's conclusion.
The paper's result is proved on paper; no machine-checked version is known to exist, and Mathlib has no edit distance at the pinned revision. The formalization produces exact closed forms for three diagonals of a nontrivial edit matrix with irrational entries, a formal link between edit distance over arbitrary edit sequences and minimum-cost paths, and a verified counterexample to the naive generalization of the algorithm. The sibling mission of the series formalizes the algorithm and Lemma 4.
The central difficulty is Lemma 5: a lower bound on the cost of every path confined to a band of eccentricity, not only the straight diagonal. A path may leave its diagonal, pay for a deletion and an insertion, and travel along another diagonal whose 's may or may not line up. The bound must hold uniformly in , and , and it depends on the floor function and on precise inequalities between and . Checking that the straight diagonals are optimal for small does not suffice: the -densities are chosen so that even and odd diagonals cost almost exactly the same per step, and a periodic placement of 's would let one diagonal eventually undercut another.
Strings are Lists; the infinite strings , are functions read from index , and is the list of their first symbols. An edit operation is a pair of Option values other than . The edit distance and are real infima (sInf) of nonempty sets of nonnegative reals, so they coincide with the paper's minima. has indexing and indexing (the paper's Figure 4 prints across the columns). is . The constraint of applies to every point of the path, endpoints included. Costs use Real.pi itself.
Pinned statements: the paper states Theorem 5 about the running time of Algorithm Y ("Discreteness is a necessary condition for Algorithm Y to run in time on length strings and step sequences"); its proof establishes that the number of distinct steps grows linearly with the string length, which is what the goal states. Running time is not formalized. The §2.3 milestone is stated, as in the paper, for all strings and every nonnegative cost function satisfying the §1.1 normalization ; both standing assumptions are hypotheses. The paper's standing assumption is used only for running times and is omitted.
The example must be the paper's: replacing by a rational, or quantifying over "some" cost function or "some" strings, makes the goal false or empty, and the edit distance must be the minimum over edit sequences, not a recurrence.
Needed infrastructure: edit sequences and their costs, the reduction of edit sequences to edit paths, and bounds on with (Mathlib's irrational_pi and Real.pi_gt_d2). The edit-distance definitions are shared in shape with the sibling mission and are reusable. Proofs of any milestone are welcome.
A buyer and a seller negotiate over one indivisible good. Each knows the good's worth to themselves but not to the other side, so each shades their offer to exploit the other's uncertainty, and some mutually profitable trades fail. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this as a one-shot game of simultaneous sealed offers and computed its equilibria in closed form for uniformly distributed values.
That closed-form equilibrium became the reference example of bilateral trade with two-sided private information. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) proved that no mechanism can guarantee efficient trade in this setting and showed that, for uniform values, the equilibrium of the sealed-offer game with attains the largest expected gains from trade of any incentive-compatible, individually rational mechanism. The later literature on the -double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) studies the same game and uses the linear equilibrium as its benchmark.
A seller has reservation price and a buyer has reservation price , both in with . Each knows their own value. Each believes the other's value is uniformly distributed on : the distribution functions are on . In Lean this belief is the measure unif v̄, Lebesgue measure conditioned on .
Under the Bargaining Rule, the seller asks and the buyer offers simultaneously. If the good is sold at for a fixed ; if there is no sale. On a sale the seller earns and the buyer ; otherwise both earn zero. The case gives the buyer the right to make a take-it-or-leave-it offer, gives it to the seller, and splits the difference.
An offer strategy maps values to offers: for the seller, for the buyer. Against , a buyer with value who offers earns in expectation
and against a seller with value asking earns . These are buyerProfit and sellerProfit. The pair is an equilibrium (IsEquilibrium) if, for every value in , each player's prescribed offer maximises their expected profit over all real offers.
Write and . If and are measurable and
then is an equilibrium. The statement leaves the no-trade branches free, as the paper does: a seller whose value exceeds every serious bid may ask anything at least , and a buyer whose value is below every serious ask may bid anything at most .
The goal is the conjunction of milestones 2 and 3, by definition of equilibrium. Milestone 1 is the step the paper actually writes down; it records the necessary first-order conditions and does not by itself give the global best-response property.
The result. Example 1(a) is the explicit equilibrium from which the paper derives the probability of trade, , and each party's ex ante profit as a function of (Example 1(b)–(c)). It is the equilibrium shown by Myerson and Satterthwaite to be second-best efficient at , and it is the standard test case against which other double-auction equilibria and mechanisms for bilateral trade are compared.
Formalizing it. The result is proved in the literature but, to our knowledge, has not been machine-checked. The paper itself only observes that the linear branches satisfy the first-order conditions; the global statement (no deviation to any real offer is profitable, including deviations that reach the other side's no-trade types) is left to the reader. A formal proof closes that gap and yields reusable facts about expected profits under uniform beliefs. The two companion missions of this series formalize the paper's Theorem 2 (the linked differential equations in general) and Example 1(b)–(c) (trade probability and expected profits).
First-order conditions do not suffice. A seller can ask below the lowest serious ask and trade with buyers on the free lower branch, whose bids are only bounded above; a buyer can bid above and meet sellers on the free upper branch, whose asks are only bounded below. The best-response inequality must hold for every such deviation and for every admissible choice of the free branches, so it cannot be read off from the linear strategies alone. The expected profit is a piecewise function of the offer, with the pieces determined by where the offer meets the opponent's linear branch and the free branches, and the inequality must be shown on each piece and at the boundaries, uniformly in including the endpoints and , where one of the free ranges is empty.
Values and offers are real numbers; strategies are functions , and their values outside are irrelevant because the beliefs give that set measure zero. Beliefs are the probability measure unif v̄ = volume[|Icc 0 v̄]; expected profits are Bochner integrals against it, written over the opponent's value rather than against an offer density. The value intervals are closed; ties trade; deviations range over all of ; ranges over the closed interval .
The strategies and are assumed measurable. Without this a deviation's expected profit could be the junk value of a non-integrable Bochner integral; with it, all integrands are bounded on the trade event. The inline coefficient of the page is read as , the reading under which the buyer's lowest serious bid equals the seller's lowest serious ask, as in the paper's Figure 1.
The claim is the sufficiency direction only; the paper states that other equilibria exist, and a statement that every equilibrium has the linear form would be false. The canonical linear pair satisfies all hypotheses, so the goal is not vacuous.
Useful infrastructure includes integrals of piecewise-affine functions against the uniform measure on an interval and the distribution function of volume[|Icc 0 v̄]. Contributions welcome: proofs of the milestones, and lemmas computing and in closed form on each piece.
Many optimization problems ask for a subset of a finite ground set that maximizes a function with diminishing returns: the cut of a graph or a directed graph, the value of a facility-location configuration, the entropy of a set of random variables, or a welfare function in combinatorial auctions. These functions are submodular but typically non-monotone: adding elements can decrease the value. Max Cut and Max Directed Cut are the textbook special cases. Unconstrained maximization of a nonnegative non-monotone submodular function is NP-hard, and before Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) no constant-factor approximation was known for general such functions in the value-oracle model.
The paper gives several algorithms. A uniformly random set achieves of the optimum (a separate mission of this series). This mission concerns the paper's first deterministic algorithm: a local search that repeatedly adds or removes a single element while the value improves by a factor larger than , and returns the better of the final set and its complement. The key structural fact behind it, that a local optimum of a submodular function dominates all its subsets and supersets, goes back to Cherenin (1962) and Goldengorin, Tijssen and Tso (1999).
Timeline. Cherenin (1962) and Goldengorin–Tijssen–Tso (1999): local optima dominate comparable sets. Schäffer and Yannakakis (SIAM J. Comput. 1991): finding an exact local optimum of Max Cut is PLS-complete, which is why the algorithm here uses an approximate improvement threshold. Feige–Mirrokni–Vondrák (FOCS 2007; SIAM J. Comput. 2011): the and guarantees of this mission, and for a randomized "smooth" local search. Buchbinder, Feldman, Naor and Schwartz (SIAM J. Comput. 2015): a randomized double-greedy -approximation, which is optimal in the value-oracle model by the lower bound of the same 2011 paper.
Let be a finite ground set with elements. A set function assigns a real number to every . It is submodular (Definition 1.1) if
and symmetric if for all . Throughout the section of the paper formalized here, is nonnegative. The algorithm may query for any (a value oracle). The optimum is .
A set is a local optimum if for every and for every . It is a -approximate local optimum (Definition 3.2) if for and for .
Algorithm LS with parameter and :
In Lean these are Submodular, SymmetricSetFun, OPT, IsLocalOptimum, IsApproxLocalOptimum, lsStep, IsLSRun, IsLSTerminal and lsOutput in NonmonotoneSubmod.LocalSearch.
For nonnegative submodular on a nonempty and , every run of Algorithm LS, with any choice of starting singleton and of improving elements, satisfies:
The last line is the explicit content of the printed bound of oracle calls: it gives steps of at most queries each, and in particular termination.
The result. Theorem 3.4 is the deterministic constant-factor approximation of the paper that first gave guaranteed approximation factors for maximizing general nonnegative submodular functions ("Prior to our work, to the best of our knowledge, no guaranteed approximation factor was known", p. 1135), and the bound for symmetric functions matches the value-oracle lower bound proved in the same paper (so it is optimal for symmetric functions among algorithms using polynomially many queries). Local search with a multiplicative acceptance threshold was subsequently used for constrained non-monotone submodular maximization (matroid and knapsack constraints, Lee–Mirrokni–Nagarajan–Sviridenko 2010).
Formalizing it. The result is proved; to our knowledge neither the theorem nor Lemmas 3.1 and 3.3 has a machine-checked proof. The mission produces a reusable finite model of set functions and single-element local search over Finset, with the algorithm stated as a nondeterministic step relation, so that the guarantee is proved for every tie-breaking rule. The same model is the starting point for formalizing other local-search guarantees.
The natural first idea, to argue from an exact local optimum via Lemma 3.1, does not apply: LS stops at an approximate local optimum, and the error per element must be accumulated along a chain of up to single-element changes between and or . This accumulation is where the nonnegativity of enters (the lemma fails for negative-valued ), and where the factor in the final ratio comes from. The running-time bound requires relating to the best singleton, which uses submodularity on sets of all sizes and breaks down on a one-element ground set. A further bookkeeping difficulty is the algorithm itself: its steps are ordered (removals only when no addition applies), and the termination bridge must use that order.
X : Type with [Fintype X] [DecidableEq X]; subsets are Finset X; is Finset X → ℝ; complements are Sᶜ. is (Fintype.card X : ℝ).∀ S, 0 ≤ f S (standing assumption of §3); Lemma 3.1 and the termination bridge are stated without it, as they need none.Finset.sup'), never a supremum with a default value.S : ℕ → Finset X with S 0 = {v} for any maximum-value singleton v and consecutive sets related by an LS step; the theorems quantify over all runs. Steps use strict inequalities, termination their negation, exactly as printed.Contributions welcome: proofs of the milestones, general lemmas about chains of single-element changes in Finset, and the derivation of the goal from them.
A variational inequality asks for a point of a set at which a vector field points "into" : for every . It is the common form of the first-order optimality conditions of constrained optimization, of complementarity problems, and of equilibrium models in economics and traffic networks. In many of these models the feasible set itself depends on the decision: the admissible actions of one agent are restricted by the current state, as in the impulse-control problems of Bensoussan and Lions that motivated quasi-variational inequalities, where .
D. Chan and J. S. Pang, The generalized quasi-variational inequality problem (Math. Oper. Res. 7 (1982) 211–222), unify the quasi-variational inequality with the generalized (set-valued) variational inequality of Fang and Peterson (JOTA 1982). Their §§3–4 prove existence by fixed-point theorems for set-valued maps; §5 takes a different route and characterizes solutions as fixed points of a composite projection map. Theorem 5.3, the subject of this mission, gives conditions under which that map is a contraction, so that its fixed point exists, is unique, solves the problem, and is computed by plain fixed-point iteration from any starting point. It is the algorithmic result of the paper, and an early instance of the projection methods for strongly monotone quasi-variational inequalities studied since (e.g. Nesterov and Scrimali 2011).
Throughout, carries the Euclidean inner product and norm .
Given point-to-set mappings and of into itself, the generalized quasi-variational inequality problem is to find vectors and with
When is point-to-point, is read as the singleton .
For a set and a point , the projection is the point of nearest to , ; it exists and is unique when is nonempty, closed and convex.
Theorem 5.3 concerns the special structure in which the feasible set moves by translation: fix a nonempty closed convex set and a point-to-point mapping , and put
For a step length and a point-to-point , the projection map is
The mappings and are assumed Lipschitz continuous with constants , (, ) and strongly monotone with constants , (, ).
For each with
the map is a contraction (Lipschitz with a constant independent of the points), it has a fixed point , the point solves , and the iterates converge to from every initial vector . All four conclusions are stated together.
The result. Theorem 5.3 turns an existence question into a computation: under Lipschitz and strong monotonicity assumptions, a quasi-variational inequality with translated feasible sets has exactly one solution reachable by projection iterations, each of which is a projection on the fixed set (a convex quadratic program when is polyhedral). The step-size window it gives is explicit in , so it certifies a convergent method before any iteration is run. The closing remark of the paper (p. 222) reads each step as solving the GQVI under a zero-th order approximation of , the viewpoint behind later splitting methods.
Formalizing it. The result is proved in the paper; the proof is short, but its constants and the equivalence of the two contraction conditions are easy to get wrong. A machine-checked version fixes the exact hypotheses (no sign conditions on the constants, Euclidean geometry), and produces reusable pieces: the translation identity for projections, nonexpansiveness of the Euclidean projection on a closed convex set, and the projection characterization of quasi-variational inequalities (Theorem 5.1).
Banach's fixed-point theorem does the last step; the work is the estimate. The naive bound, projection nonexpansiveness applied directly to , fails because the sets and differ: two projections on different sets are not controlled by the distance of the projected points alone. The translation identity separates the moving part from a projection on the one set , at the cost of the additive term in the constant. The remaining square must be expanded with the inner-product cross terms bounded by the monotonicity constants in the right directions, including the cross term between and . Finally, the condition "bracket " is equivalent to the stated -condition only when , which must be derived from the hypotheses rather than assumed.
EuclideanSpace ℝ (Fin n), with Mathlib's Euclidean norm and inner product; Fin n → ℝ (sup norm) would change every constant. No assumption is made; at all statements hold trivially.proj that returns a junk value only when no nearest point exists; under the hypotheses of every statement using it, the nearest point exists and is unique, so proj is the paper's . Theorem 5.1 is stated relationally (nearest-point predicate IsProj) to avoid junk values altogether.ContractingWith c F with c : ℝ≥0: c < 1 and a Lipschitz bound with that single constant. A constant allowed to depend on the points, or a Lipschitz bound without c < 1, is not a contraction and would trivialize the goal; so would a projection whose junk value is reachable (e.g. with empty), which makes unrelated to the paper's map. The fixed point must be linked to the GQVI and to the iteration from every starting point.Real.sqrt; its radicand is nonnegative under the hypotheses when .ContractingWith.fixedPoint and ContractingWith.tendsto_iterate_fixedPoint (Banach), exists_norm_eq_iInf_of_complete_convex and norm_eq_iInf_iff_real_inner_le_zero (projection on convex sets), and the platform theorem VectorSpaceOpt.min_distance_convex_set. A general lemma that the Euclidean nearest-point map of a closed convex set is 1-Lipschitz is reusable well beyond this mission and is welcome as a separate contribution.Quadratic programming, the minimisation of a quadratic function subject to linear inequality constraints, is a basic subproblem of nonlinear optimisation (sequential quadratic programming, trust-region methods) and a model in its own right in portfolio selection, least-squares estimation and control. The classical solution methods are active-set methods: they keep a set of constraints treated as equalities, minimise over the resulting affine set, and then decide which constraint to drop or add (Gill, Murray and Wright, Practical Optimization, 1981; Fletcher, Practical Methods of Optimization, Vol. 2, 1981). Their finite-termination proofs need either a nondegeneracy assumption (linearly independent active constraints) or an anti-cycling rule, because under degeneracy the choice of the constraint to drop, made from Lagrange multiplier estimates, can cycle.
Calamai and Moré (Mathematical Programming 39, 1987) showed that the gradient projection method can take over the step that leaves a working set. Their Algorithm 6.1 alternates two kinds of step: an arbitrary non-increasing step that adds constraints to the working set until the equality-constrained subproblem is solved, and a single projected-gradient step once it is solved. Theorem 6.2 states that this algorithm terminates at a stationary point for every quadratic that is bounded below on the feasible polyhedron, with no nondegeneracy assumption and no anti-cycling rule. The same paper's Sections 2–4 (the subject of the first two missions of this series) supply the properties of the gradient projection step that the argument uses.
Timeline of the ingredients:
Let be a finite-dimensional real inner product space (the paper's with a general inner product). The feasible set is a polyhedron
with active set . The objective is a quadratic function with self-adjoint but not necessarily positive semidefinite, so may be nonconvex. Its gradient is taken with respect to the inner product of .
The projection into is , and a point is stationary if for every .
A gradient projection step from is with satisfying the sufficient decrease condition (2.1) with a constant , the condition (2.2) that or for some at which the decrease test (2.3) with constant fails, and the upper bound (3.2).
A working set is a set ; problem (6.2) is , over an affine set that ignores the inequality constraints outside .
Algorithm 6.1 produces iterates and working sets from :
For every quadratic bounded below on , all constants , , , and every run of Algorithm 6.1,
The theorem makes no assumption on the boundedness of the iterates and none on the linear independence of the constraints.
Theorem 6.2 separates the two roles an active-set method plays: solving equality-constrained subproblems, for which any method that does not increase may be used, and choosing the next working set, which the gradient projection step does. The consequence is a finitely terminating quadratic programming algorithm for nonconvex quadratics that needs neither nondegeneracy nor an anti-cycling rule, and a template for large-scale bound-constrained and linearly constrained solvers that combine projection steps with subspace minimisation.
The result is proved in the paper and is classical; no machine-checked version is known. A formalization produces a checked finite-termination theorem for an active-set method on degenerate problems, together with reusable pieces: the projection onto a polyhedron as a total function with its variational inequality, the descent estimate of a projected step, and a predicate describing active-set runs with working sets, which other active-set algorithms can reuse.
The obvious argument — each step decreases and there are finitely many working sets — fails on two counts. First, step (b) only guarantees , so values alone do not rule out infinitely many iterations; the nesting of working sets and the final clause of step (b) are what bound consecutive (b)-steps. Second, a gradient projection step taken at a solution of (6.2) can in principle leave unchanged, and nothing in the algorithm's rules says directly that it makes progress; that it does so at every non-stationary iterate is a property of the projection and of the step conditions (2.1)–(2.2), not of the algorithm. A further point is that the minimum of (6.2) is taken over an affine set, not over , and the link between the value at a step-(a) iterate and later iterates runs through the requirement .
The space is a finite-dimensional real inner product space E; is Mathlib's gradient. Constraints are indexed by Fin m, working and active sets are Finset (Fin m), and a run is a predicate IsAlgorithm61Run on three sequences , , indexed from . The run does not stop by itself; "the algorithm terminates at a stationary iterate" is rendered as the existence of an index with stationary. The projection is argmin made total by a junk value that is unreachable when is nonempty, closed and convex. The paper's "" between working sets is inclusion. A quadratic function is with symmetric and no definiteness assumption.
A trivializing formalization — a run predicate that forces to be stationary, or that no sequence satisfies — would make the goal empty; the step rules here are the paper's verbatim, and a run on with starting at the non-stationary point satisfies the predicate. Replacing step (a) by "any step that strictly decreases " would assume the central fact and is not acceptable.
A complete development needs: the variational inequality of the projection (Lemma 2.1(a)), the descent estimate (2.5), the characterisation of stationary points as fixed points of the projected step, and a finiteness argument over the finitely many subsets of Fin m. Proofs of the milestones, of these auxiliary facts, and of the goal are all welcome.
Many combinatorial optimization problems on graphs are linear programs over a polytope whose inequality description is unknown. The stable set polytope is the standard example: maximizing a linear function over it is the maximum weight stable set problem, which is NP-hard, and no complete inequality description is known for general graphs. A productive line of work, begun in V. Chvátal's 1975 paper On certain polytopes associated with graphs (J. Combin. Theory Ser. B 18 (1975) 138–154), asks instead how such descriptions behave under graph operations: if descriptions are known for small graphs, can one write one down for a graph built from them?
Section 5 of that paper answers this for substitution, the operation that replaces a vertex of one graph by a whole second graph. Substitution contains three familiar constructions as special cases: duplicating a vertex, forming the join of two graphs, and forming the lexicographic product (composition). Duplication is one of the two ingredients of Lovász's proof of the perfect graph theorem (Lovász 1972); substitution in general is the operation under which perfection is preserved, and graphs built from simple pieces by substitution are a recurring source of classes with tractable stable set polytopes.
All graphs are finite, undirected and loopless. A stable set of a graph is a set of vertices no two of which are adjacent. Write for the set of incidence vectors of stable sets (the zero–one vectors with stable), and
for the stable set polytope. A finite system of linear inequalities in the variables is a defining linear system of when its set of solutions is exactly .
Let and be graphs with , and let . The graph obtained from by substituting for has vertex set . Its edges are the edges of , the edges of , and every edge joining a vertex of to a neighbour of in . In Lean the vertex type is the disjoint sum {u : V₁ // u ≠ v} ⊕ V₂ and the graph is substitute G₁ v G₂.
For let
be a defining linear system of , with finite index sets and real coefficients, and put for . Then
is a defining linear system of . The statement fixes no particular system for or : any defining systems of the two pieces produce one for , with rows besides nonnegativity.
where and are the maxima of over with and respectively, and is the maximum of over .
Theorem 5.1 gives an explicit construction: from a polyhedral description of and it writes one of , row by row, with no loss. Specialized to it gives Corollary 5.2 of the paper, a defining linear system for the join ; applied repeatedly it gives defining systems for lexicographic products, and applied with it describes the effect of duplicating a vertex. Applied to clique systems, whose coefficients are 0 and 1, the rows of (5.1) are again clique inequalities of , so the class of graphs whose stable set polytope is described by nonnegativity and clique inequalities is closed under substitution.
The result has been proved in print since 1975. As far as a search of the Prove2Me catalogue shows, none of it, including Proposition 2.1 and the substitution operation itself, has a machine-checked statement or proof. The mission asks for a formal proof of the theorem and of the two combinatorial and polyhedral steps it rests on. The definitions of , and graph substitution, and the LP characterization of Proposition 2.1, are reusable by every other mission on stable set polytopes and on polyhedral descriptions of 0–1 sets.
That every point of satisfies (5.1) is a short case check on stable sets of . The difficulty is the reverse inclusion: that no point outside satisfies (5.1). The first idea, taking a point that satisfies (5.1) and splitting it directly into a point of and a point of , fails: (5.1) couples the two input systems through products of their coefficients and right-hand sides, and a fractional solution of (5.1) carries no evident decomposition into the two pieces. Nothing is assumed about the signs of the input coefficients, so the rows of (5.1) can mix positive and negative terms, and the positive part in place of is what keeps the system valid when .
The polyhedral step behind Proposition 2.1, relating a convex hull of finitely many points to an inequality system through linear programming duality, is not available in Mathlib in this form and has to be built.
SimpleGraph on a Fintype with decidable equality; the substituted graph lives on {u : V₁ // u ≠ v} ⊕ V₂, which builds in .IsIndepSet); is convexHull ℝ (S G), never the solution set of an inequality system.a : J → V → ℝ, b : J → ℝ. The nonnegativity rows are kept as a separate conjunct ∀ u, 0 ≤ x u everywhere; Proposition 2.1 is false without them. "Defining linear system" is set equality of the solution set with .[Nonempty V₂]) in Theorem 5.1. The paper's graphs have nonempty vertex sets and its proof picks a vertex of ; with , and , (5.1) is just and the theorem fails. The validity milestone does not need it.sSup over a finite set that always contains the zero vector or the incidence vector of , so no junk value of sSup can occur.Contributions welcome: a proof of Proposition 2.1 (the reusable core), the combinatorial decomposition, the validity case check, and the assembly of the goal.
Minimizing a smooth function subject to linear inequality constraints is the core subproblem of much of nonlinear optimization: bound-constrained problems, quadratic programs, and the subproblems of sequential quadratic programming and augmented Lagrangian methods all have this form. Methods for these problems are usually built from two parts, one that decides which constraints hold with equality at the solution and one that solves the resulting equality-constrained problem quickly. The first part only pays off if the decision stabilizes after finitely many iterations; otherwise the fast local method never gets to run.
Calamai and Moré (Math. Programming 39, 1987) proved that this stabilization is a property of the limit point, not of the algorithm. Any feasible sequence that converges and whose projected gradients tend to zero identifies the active constraints of a nondegenerate limit in finitely many steps. This is the result that later active-set and gradient-projection methods for bound-constrained and linearly constrained problems invoke to justify switching to a fast local phase.
Timeline.
Let be a finite-dimensional real inner product space (the paper's with a general inner product) and let be continuously differentiable on the feasible set, with gradient taken with respect to the inner product of .
The feasible set is a polyhedral set
for constraint normals and scalars . The active set at is .
A direction is feasible at if for all sufficiently small . The tangent cone is the closure of the set of feasible directions. The projected gradient is the point of closest to :
A point is stationary if for all . It is a Kuhn–Tucker point if with . It is nondegenerate if the active normals are linearly independent and the multipliers satisfy for every .
A Lagrange multiplier estimate is a map . It defines the binding set . The estimate is consistent if whenever , the point is a nondegenerate Kuhn–Tucker point, and for every .
Let be an arbitrary sequence in converging to . If and is nondegenerate, then
The sequence need not come from any particular algorithm. The goal asserts eventual equality of the index sets, not inclusion.
The result. Theorem 4.1 separates identification from convergence. Any method that keeps its iterates feasible and drives the projected gradient to zero inherits finite identification, whatever its step-size rule or search direction. After identification the constrained problem is locally an unconstrained problem on the affine subspace , so Newton-type or conjugate-gradient methods can take over. Theorem 4.2 carries the same conclusion to methods that drop constraints according to the signs of multiplier estimates. The companion missions of this series use the result: the gradient projection method drives the projected gradients to zero (mission I), and a gradient projection algorithm for quadratic programs terminates finitely (mission III).
Formalizing it. The theorems are proved in the paper. No machine-checked version of the projected gradient, of tangent cones of polyhedra with their active-set description, or of finite active-set identification is known to exist. Formalization adds a reusable account of tangent cones and polar cones of polyhedral sets and of the equivalence between stationarity and the Kuhn–Tucker conditions for linear constraints, together with a method-independent identification theorem stated at the level of generality of the paper.
Two different limits are involved. Convergence is enough to show that no inactive constraint of is active at for large . The hard direction is the converse: a constraint active at might be inactive at infinitely many , approached from the interior. Convergence of the points alone cannot rule this out. The projected gradient is also not continuous, because the tangent cone changes when a new constraint becomes active. So the hypothesis cannot be passed to the limit naively. Both nondegeneracy conditions matter: without linear independence, or with a zero multiplier, the statement fails.
The space is a real inner product space E with [FiniteDimensional ℝ E], and is Mathlib's gradient. "Continuously differentiable on " means DifferentiableAt ℝ f x for every together with ContinuousOn (gradient f) Ω. The constraints are indexed by Fin m. is polyhedron c δ, and is activeSet c δ x : Finset (Fin m).
The tangent cone is defined as the closure of the feasible directions, not by the polyhedral formula, which is a milestone. The projected gradient is the nearest point of to , chosen by a choice function that returns only when no nearest point exists. That never happens at a point of a polyhedral set.
Nondegeneracy is bundled as IsNondegenerate c δ f x*: , the family is linearly independent, and positive multipliers represent . "For all sufficiently large " is ∀ᶠ k in Filter.atTop.
In Theorem 4.2 the paper leaves one condition implicit: the estimate at must be the Kuhn–Tucker multiplier vector, . Without it the statement is false, so it is an explicit hypothesis. Consistency is required only along feasible sequences and only in the coordinates .
A formalization that assumes , assumes the active sets are eventually constant, weakens nondegeneracy to nonnegative multipliers, or concludes only inclusion is not the paper's theorem and does not satisfy this mission.
Needed infrastructure: tangent cones of convex sets, the Moreau decomposition into a closed convex cone and its polar, Farkas' lemma in a general inner product space, and orthogonal projections onto subspaces spanned by linearly independent vectors. The polyhedral tangent-cone and Kuhn–Tucker results are reusable beyond this mission. Proofs of any milestone are welcome, as are auxiliary lemmas on polyhedral cones.
Minimizing a smooth function over a closed convex set on which projection is cheap (a box, a ball, a simplex) is a routine subproblem in large-scale optimization. Box-constrained minimization is the inner solver of augmented Lagrangian methods, and bound-constrained least squares, image restoration and density estimation all have this form. The classical gradient projection method of Goldstein and of Levitin and Polyak needs only gradients and projections, but with constant or monotone Armijo step lengths it is slow.
Spectral projected gradient (SPG) methods, introduced by Birgin, Martínez and Raydan (paper), combine three ingredients. The first is the projection. The second is the Barzilai–Borwein (spectral) step length , an inverse Rayleigh quotient of the average Hessian along the last step. The third is the nonmonotone line search of Grippo, Lampariello and Lucidi, which compares a trial value with the worst of the last objective values instead of the current one. The paper defines two variants. This mission concerns SPG1, which backtracks along the projection arc , as in Bertsekas's analysis of the Armijo rule for gradient projection. The companion mission concerns SPG2, which backtracks along a fixed feasible direction.
Timeline:
Let be nonempty, closed and convex, with the Euclidean inner product and norm . Let have continuous partial derivatives on an open set , and write . The orthogonal projection is the unique point of nearest to . The scaled projected gradient is for and . A point is a constrained stationary point if for all .
The parameters are an integer , reals , a sufficient-decrease constant and safeguards . Algorithm SPG1 (Algorithm 2.1) starts from and . At iteration it does the following.
replace by any . When (1) holds, set and . 3. Spectral step. With , and , set if , and otherwise .
The first trial of each backtracking is the spectral step , not . The sufficient-decrease term in (1) is , with no factor .
In Lean these objects are written as follows:
P with the predicate IsProjOnto Ω P;scaledProjGrad P f t;IsConstrainedStationary Ω f;nonmonotoneRef f x M k;SPG1Test;IsSPG1Run Ω f P M αmin αmax γ σ₁ σ₂ x α.For every infinite run of SPG1 and every accumulation point of ,
The statement fixes no parameter values, and it assumes neither convexity of nor a bounded level set.
Theorem 2.2 is the global convergence guarantee for SPG1. It holds without monotone decrease of and with no restriction on the spectral step beyond the safeguards. Lemma 2.2 carries Bertsekas's curvilinear Armijo analysis, stated for monotone gradient projection, over to the nonmonotone spectral setting. The projection-arc search is the natural one when is a box or a polyhedron: there the arc is piecewise linear and each trial point is feasible by construction.
Status: the theorem is proved in the literature. This paper's proof reads "Use Lemma 2.2 with the proof technique of [7]", and Lemma 2.2 is quoted from Bertsekas's Nonlinear Programming (Lemma 2.3.1 and Theorem 2.3.3 (a)). No Lean formalization of this theorem, of the Armijo analysis along the projection arc, or of the monotonicity of is known. The mission produces a formal proof and a reusable Lean interface for projection-based first-order methods on convex sets.
For monotone descent methods, the usual argument shows that decreases, so the total decrease is finite and the per-iteration decrease tends to zero. That argument fails here, because need not decrease. Only the window maximum is nonincreasing, and a small decrease of this maximum does not by itself give a small decrease at the iterates that approach a given accumulation point .
Along the projection arc there is a second obstacle. The decrease predicted by (1) is , and depends nonlinearly on : for the trial point is not a rescaling of the first one. So small accepted steps do not translate into small multiples of a fixed direction, as they do for SPG2. The step lengths may also tend to zero, is only on a neighbourhood of , and no Lipschitz constant for is available.
Space and data. The space is EuclideanSpace ℝ (Fin n) with inner ℝ and the 2-norm. is a total function EuclideanSpace ℝ (Fin n) → ℝ with ContDiffOn ℝ 1 f U on an open U ⊇ Ω, and is Mathlib's gradient f. Every trial point is a projection, so the algorithm evaluates and only at points of .
Iteration and trials. Iterations are indexed from . The backtracking choice (2) is universally quantified. At each iteration, a run carries a finite trial list with and ; test (1) fails at every trial but the last and holds at the last.
Step size. is given by Step 3 exactly.
Accumulation point. An accumulation point is MapClusterPt x̄ atTop x.
Lemma 2.2 (i). The paper names the domain but defines only for , so the milestone is stated on .
Excluded simplifications. None of the following is SPG1:
Nor is a goal that states instead of the variational inequality, or one that adds convexity of , a Lipschitz gradient or a bounded level set.
Non-vacuity. The hypotheses of the goal are satisfiable. Take , , , , , , , and . Then the iterates with form an infinite run with accumulation point .
Infrastructure. A complete development needs:
iInf form, norm_eq_iInf_iff_real_inner_le_zero) and the nonexpansiveness of the projection;The projection lemmas, including Lemma 2.2 (i), are reusable for any gradient projection method and are welcome as separate contributions.
Many decision problems in operations research are solved in two stages: a model predicts the unknown cost vector of a linear optimization problem from features, and the predicted costs are then passed to a solver. The smart predict-then-optimize (SPO) loss of Elmachtoub and Grigas measures the quality of a prediction by the excess true cost of the decision it induces, rather than by the prediction error itself. El Balghiti, Elmachtoub, Grigas and Tewari study how well the empirical SPO loss generalizes. Their margin-based bounds (Theorems 4 and 5 of the paper) require a geometric condition on the feasible region, the strength property, and a way to compute the distance to degeneracy that enters the margin loss.
Section 5 of the paper verifies this condition in the two cases that matter in practice. For strongly convex regions it is Theorem 7 (mission III of this series). This mission covers the other case, §5.2: feasible regions that are polytopes given by a list of points, which includes the unit simplex of multiclass classification and the feasible regions of shortest-path, assignment and other combinatorial problems written as convex hulls.
Let be a finite-dimensional real vector space (the paper's ) with a norm . A cost vector is a linear functional on ; its value at is written , and its dual norm is .
The feasible region is a polytope with a known convex hull representation: pairwise distinct points and
Redundant points (points that are convex combinations of the others) are allowed. For a cost vector , is the problem , and an optimization oracle is any map with for every .
If is not a singleton, then for every oracle , has the strength property with parameter
The result. Formula (10) turns the distance to degeneracy, defined as an infimum over an infinite non-convex set, into a minimum of explicit ratios that needs one oracle call. This makes the margin SPO loss of the paper computable for polytopes. The strength claim, combined with the paper's Theorems 4 and 5, yields margin-based generalization bounds for the SPO loss over any polytope with a known vertex list, with a dependence on the hypothesis class through its multivariate Rademacher complexity rather than through a Natarajan dimension. For the unit simplex it recovers known margin bounds for multiclass classification (Example 8).
Formalizing it. The results are proved in the paper; to our knowledge none of them is machine-checked. A formalization produces, beyond the four statements, a Lean account of the normal fan of a polytope presented by a point list, its interplay with uniqueness of linear-optimization solutions, and distances to its boundary measured in a dual norm. These are standard facts of polyhedral theory that Mathlib does not yet state in this form.
The obstacle is that is a distance to the degenerate set, and that set is neither convex nor given by inequalities: it is a union of lower-dimensional pieces of the normal fan, so no projection formula applies, and its description depends on which points of the representation are redundant. Relating a dual-norm ball around to the finitely many inequalities of eq. (9) is where the argument needs care. A Euclidean shortcut is not available: the norm is arbitrary, and the numerator of (10) and the distance are measured in different norms. A second trap is the oracle: at a degenerate it may return a point that is not among the , and (10) must still hold.
StrongDual ℝ E, whose operator norm is the dual norm. Interiors and distances in the cost space use that norm.v : Fin K → E, injective, with = convexHull ℝ (Set.range v). Nonemptiness, compactness and convexity of (the paper's §2 standing assumptions) follow from this representation; Proposition 2 and the diameter identity add , which is that nonemptiness.S.Nontrivial. Without it , and the strength property holds for free; with it, and is a genuine distance. The goal's parameter is stated to be positive, so the Lean conventions on unbounded or one-point sets and cannot trivialize it.Metric.infDist to ; is Metric.diam, correct here because is bounded. Minima and maxima over finite index sets are stated with IsLeast/IsGreatest, so no junk value of min' or sInf enters.Many computations in numerical linear algebra, statistics and computational physics need the trace of a matrix that is never formed explicitly: may be an inverse, a matrix function , or a product of large operators, and the only affordable access is a routine that returns or for a given vector . Monte Carlo trace estimators handle this setting: draw random vectors and average the quadratic forms , each of which costs one matrix–vector product.
Avron and Toledo (J. ACM 2011) compare such estimators by the number of samples that guarantee relative error with probability , and by the number of random bits each sample consumes. Hutchinson's estimator (Hutchinson 1990) and the Gaussian estimator need random bits per sample. Section 8 of the paper studies two estimators that sample only from the standard basis vectors and so need about bits per sample, which allows the samples to be generated in advance. The plain version has a sample bound that depends on how uneven the diagonal of is; the mixed version first multiplies on both sides by a random orthogonal mixing matrix of the kind introduced by Ailon and Chazelle (2006) for the fast Johnson–Lindenstrauss transform and used by Avron, Maymounkov and Toledo (2010) in least-squares solvers. This mission formalizes the resulting sample bound, Theorem 8.4.
Let , let be symmetric positive semi-definite, and let be the standard basis of .
A random variable is an -approximator of if
(Definition 4.1).
The unit vector estimator with samples is
where are independent uniform random samples from (Definition 3.4). Each term is a diagonal entry of chosen uniformly at random. Its behaviour is governed by
which lies between and .
A random mixing matrix is , where the seed is a fixed orthogonal matrix and is diagonal with i.i.d. Rademacher entries, (Definition 3.5). The seed enters through
which satisfies ; normalized DFT and Hadamard matrices attain , DCT and DHT matrices have (p. 8:5).
The mixed unit vector estimator is
with as above, independent of (Definition 3.6). It is the unit vector estimator applied to , whose trace equals .
For every orthogonal seed , every symmetric positive semi-definite , every , and every ,
Theorem 8.2 alone shows that the unit vector estimator can need order samples: when the trace is concentrated on one diagonal entry, . Theorem 8.4 removes the dependence on entirely. For a Fourier-type seed with the bound becomes samples for every positive semi-definite , while each sample still costs about random bits, and the bits of are drawn once. Among the estimators of the paper this is the only one with both an -independent sample bound and logarithmic randomness per sample (Table I, p. 8:5). Lemma 8.3 is a standalone statement about randomized orthogonal transforms that is used well beyond trace estimation, in the analysis of subsampled randomized Hadamard transforms, sketching-based least squares, and fast Johnson–Lindenstrauss embeddings.
All results of the mission are proved in the literature: Lemma 8.3 in the cited works, the rest in the paper. As far as the platform's catalogue shows, none has a machine-checked proof. The mission produces checked statements of the paper's Section 8 with their exact constants, a probability model for random sign matrices and uniform basis-vector sampling that other randomized linear-algebra missions can reuse, and, once proved, a checked instance of Hoeffding's inequality applied to a concrete estimator.
The obvious argument for Theorem 8.4 applies Theorem 8.2 to . That matrix is random, so Theorem 8.2, which is a statement about a fixed matrix, cannot be applied directly: the proof must condition on , use that the samples are independent of , and combine a failure event over with a conditional failure event over the , each with probability at most . The second difficulty is Lemma 8.3: each entry is a Rademacher sum whose coefficient vector has squared norm at most , and the bound needs a sub-Gaussian tail for such sums together with a union bound over all entries. Bounding the diagonal of through the diagonal of alone does not work: each mixed diagonal entry depends on all entries of , including the off-diagonal ones.
Everything is over . The paper allows complex unitary seeds; since the estimator uses the transpose , the mission takes real orthogonal (). Matrices are Matrix (Fin n) (Fin n) ℝ, "symmetric positive semi-definite" is Matrix.PosSemidef, and is assumed throughout. The sample spaces are explicit product measures: indices uniform on Fin n with , the diagonal of with the -fold Rademacher product law, and, for , the product of the two, which makes and the independent as the paper assumes implicitly. Probabilities are Measure.real. and are maxima over finite nonempty index sets; uses real division, whose value at is irrelevant because a positive semi-definite matrix with zero trace is . The sample-count thresholds are exactly the paper's constants.
Deviations from the page, all recorded in the items' Formalization Notes: Definition 3.4 and Theorem 8.2 are stated for positive semi-definite rather than positive definite (the proof uses only ); Table I's entry for the mixed estimator, which disagrees with Theorem 8.4, is not used; the proof of Theorem 8.4 prints the conditional failure probability as "" where is meant, and no statement copies it; Remark 8.5 ("for some small ") has no pinned constant and is not stated.
A formalization in which is an arbitrary orthogonal diagonal matrix, the are correlated with , or the law of the estimator is assumed rather than constructed would make the goal either false or a restatement of its hypotheses; the product-measure model rules this out.
Needed infrastructure: Hoeffding's inequality for bounded i.i.d. sums (in Mathlib as sub-Gaussian moment generating function bounds), a sub-Gaussian tail for Rademacher linear combinations, conditioning on one factor of a product measure, and the spectral theorem for real symmetric matrices. The Rademacher sign model and the random-mixing-matrix entry bound are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 8.3, are welcome.
The k-median problem asks to open facilities among a set of candidate sites so that the total distance from clients to their nearest open facility is as small as possible. It is a basic model of facility location and of clustering, and it is NP-hard, so the question studied in approximation algorithms is how close a polynomial-time method can get to the optimum.
Local search is the method most used in practice: start from any facilities and repeatedly replace a few of them by others whenever this lowers the cost. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave the first analysis of a local search for k-median with a bounded performance guarantee using only medians. For single swaps they proved a locality gap of (Theorem 3.2, the subject of the first mission of this series); allowing up to facilities to be exchanged at once improves the gap to , which the paper notes improves on the -approximation of Charikar and Guha. That -swap bound is the result this mission formalizes.
Timeline (as recounted in §1 of the paper):
A metric instance consists of a finite set of clients, a finite set of facilities and a distance on that is nonnegative, symmetric and satisfies the triangle inequality; is the cost of serving client by facility .
For a nonempty set of open facilities, each client is served by its nearest open facility, and
Fix an integer . A -swap deletes a set of at most facilities and adds a set of the same size. The -swap neighbourhood of is
and is locally optimum when for every . The locality gap is the supremum, over instances, of the ratio between the cost of a locally optimum solution and the cost of a global optimum.
In Lean the instance is MetricInstance Cl Fa with the distance on Cl ⊕ Fa, the cost is kmCost I S hS (defined only for nonempty S), and local optimality is IsPSwapLocalOpt I p S hS, all in the namespace LocalSearchFL.MultiSwap.
For every metric instance, every integer , every , every locally optimum with , and every nonempty with ,
This is the bound concluded at the end of §3.4 (p. 553, announced p. 551). The comparison solution is arbitrary, not only an optimum, which is the strongest form printed.
The bound shows that the simplest optimization heuristic, stopped at any local optimum, is within a constant factor of optimal for metric k-median, and that the factor tends to as the neighbourhood grows; the paper's tight example (§3.5, given for and stated to generalize to every ) shows that the analysis cannot be improved for this neighbourhood. Combined with the standard -improvement rule (p. 548), it yields a polynomial-time -approximation. The analysis template (charging each client's reassignment through a bijection of , and averaging the local-optimality inequalities of carefully chosen swaps) was reused for facility location, capacitated variants and k-means.
The result has been proved since 2001. What this mission adds is a machine-checked proof: no formalization of the k-median problem or of any locality-gap bound is known to exist in Mathlib or on this platform. The combinatorial milestones (capture, the partition of Claim 3.1, the weighted swaps, the bijection of Property 3.2) are independent of the metric and are reusable in any local-search analysis of clustering objectives.
For single swaps each facility of is paired with one facility of and a direct counting argument suffices. With -swaps, a facility of may capture several facilities of at once, and a group of facilities of may jointly capture a facility of that none of them captures alone. Pairing facilities one by one then fails: the clients of a captured facility cannot be reassigned cheaply unless the capturing set is swapped out together with everything it captures. Swapping whole groups is only allowed when a group has at most members; larger groups must be split into single swaps, and the weights must be chosen so that every facility of is counted exactly once while no facility of is counted more than times. Getting the constant (rather than a weaker one) depends on this exact accounting.
Cl, Fa with Fintype and DecidableEq; solutions are Finset Fa. The distance is real-valued on Cl ⊕ Fa; d x x = 0 is not assumed (the paper neither states nor uses it).kmCost I S hS ≤ (3 + 2 / (p : ℝ)) * kmCost I O hO, with the constant computed in .Needed infrastructure: finite sums over clients, Finset.inf', permutations (Equiv.Perm), and a weighted double-counting argument over the swaps. Proofs of the combinatorial milestones and alternative routes to the goal are welcome.
Line searches are the step-size rules inside most methods for smooth unconstrained minimization : steepest descent, conjugate gradient, quasi-Newton and limited-memory methods all choose a direction and then a step along it. Classical Armijo and Wolfe rules are monotone: they require . Grippo, Lampariello and Lucidi (SIAM J. Numer. Anal., 1986) observed that insisting on monotone decrease can slow a method down, and proposed comparing with the maximum of the last function values instead. That max-based rule discards good function values and depends strongly on , and Dai showed that R-linearly convergent iterates can violate it for every fixed memory .
Zhang and Hager (SIAM J. Optim., 2004) replaced the maximum by a weighted average of all previous function values. Their averaged nonmonotone line search is used in practical codes, for example with L-BFGS and in later nonmonotone spectral and conjugate-gradient methods. This mission formalizes the paper's first main result: global convergence to stationary points for nonconvex .
Let be continuously differentiable, with gradient at the -th iterate. The Nonmonotone Line Search Algorithm (NLSA) has parameters
It maintains weights and reference values :
with chosen at each step. The iterates are , where the step satisfies one of two rules, fixed for the whole run:
The choice gives , the monotone line search; gives .
The direction assumption asks for constants with (2.4) and (2.5) for all sufficiently large . The level set is , and is the set of points whose distance to is at most , where .
Suppose is bounded from below, for every , the direction assumption holds, and is Lipschitz continuous on (Wolfe rule) or on (Armijo rule). Then
and if ,
so every limit of a convergent subsequence of iterates is a stationary point. No convexity is assumed.
Theorem 2.2 is the convergence guarantee that makes the averaged reference value usable in practice: any direction method whose directions are uniformly gradient-related (for example L-BFGS with bounded Hessian approximations) inherits stationarity of its limit points when combined with this line search, for every choice of the weights . The monotone Wolfe and Armijo results are the special case . The same estimates, (2.8) and (2.15), are the input to the paper's second main result, R-linear convergence for strongly convex (Theorem 3.1, a separate mission in this series).
The result is proved in the paper. It has no machine-checked proof that this mission is aware of: the platform has monotone backtracking statements for convex problems, but no nonmonotone line search, no Wolfe conditions and no Zoutendijk-type global convergence theorem for nonconvex . A complete development also provides reusable Lean statements of the Wolfe and Armijo conditions and of step-size lower bounds under local Lipschitz continuity of the gradient.
Each step is elementary, but the argument has several places where a naive formalization fails. The Lipschitz hypothesis is only local: on for the Wolfe rule, on the -neighbourhood for the Armijo rule. So the proof must first show that every iterate stays in even though is not monotone. This needs and the monotonicity of , and then that the Armijo rule's rejected trial point lies in . The Armijo lower bound uses the maximality of the integer exponent and a first-order Taylor bound along a segment. The passage from (2.14) to (2.6) and (2.7) uses the two growth bounds on . The first gives only , since does not force .
The space is EuclideanSpace ℝ (Fin n) with the Euclidean norm, is ContDiff ℝ 1, and the paper's row vector acting on is the inner product of Mathlib's gradient f x with . , and are defined by recursion from the run. A run is an infinite sequence satisfying the update, , and the chosen rule at every . The stopping test is not modelled. The Armijo exponent ranges over (it may be negative since ), and "largest" is IsGreatest. and the distance to are computed in , so unbounded directions give .
The following repairs and readings of the printed statements are made:
The following formalizations would make the goal trivial or empty and are ruled out:
liminf, which is for a divergent sequence;Welcome contributions: proofs of the milestones in the listed order, and general lemmas on Wolfe and Armijo steps under local gradient Lipschitz continuity, which are reusable for other line-search methods.
Many computations in numerical linear algebra, statistics and computational physics need the trace of a matrix that is never formed explicitly: may be an inverse, a matrix function , or a product of large operators, and the only affordable access is a routine that returns for a given vector . Examples include log-determinants and the generalized cross-validation criterion in statistics, counting eigenvalues in an interval, and charge densities in electronic-structure computations. Monte Carlo trace estimators handle this setting: draw random vectors , and average the quadratic forms , each of which costs one matrix–vector product.
Hutchinson (1990) introduced the estimator with Rademacher vectors and computed its variance. Avron and Toledo (J. ACM 2011) replaced variance statements with sample bounds: how many samples guarantee relative error with probability . Section 6 of their paper proves one such bound for an entire class of estimators at once, the normalized Rayleigh-quotient trace estimators, which contains Hutchinson's estimator and the unit vector estimator. This mission formalizes that bound (Theorem 6.1).
Let be symmetric positive semi-definite, with eigenvalues and rank . Write for the largest eigenvalue and
defined for ; it is the condition number of on its range.
A normalized Rayleigh-quotient trace estimator of with samples is
where are independent random vectors in with and for each (Definition 3.2). The vectors need not be identically distributed. Hutchinson's vectors ( entries, i.i.d. uniform) and the vectors with uniform are instances.
A random variable is an -approximator of if
(Definition 4.1).
For every nonzero symmetric positive semi-definite , every , , and every normalized Rayleigh-quotient estimator of ,
The result is distribution-free within the class: it needs only normalization and unbiasedness, so it covers Hutchinson's estimator, the unit vector estimator and any future normalized scheme with one argument. For well-conditioned matrices of full or nearly full rank the required number of samples is , independent of . For ill-conditioned matrices the bound degrades with , which is the reason the paper proves sharper estimator-specific bounds in Sections 7 and 8; Theorem 6.1 is the baseline those results are compared against (Table I, p. 8:5).
The theorem is proved in the paper. No machine-checked version of it, or of any sample bound for trace estimators, is known to exist. The formalization adds a precise statement of the class of estimators on a general probability space, a corrected threshold (see below), and a Lean development that connects Mathlib's spectral theorem for symmetric matrices with its Hoeffding inequality for independent bounded variables.
Each step is short on paper; the work is in the interfaces. The eigenvalue inequality of milestone 1 requires relating the number of nonzero eigenvalues (with multiplicity) to and handling the maximum and minimum over the nonzero spectrum. Milestone 2 is the Rayleigh-quotient bound , which is a consequence of the spectral decomposition rather than a one-line identity. Milestone 3 applies Hoeffding's inequality to summands that are bounded only almost surely, are not identically distributed, and whose mean is fixed by hypothesis rather than computed; the two-sided bound must be assembled from two one-sided tails, and the event must be rescaled to a statement about the sum . A naive attempt that fixes a particular distribution for the (Rademacher, say) proves a different, narrower theorem and does not settle the goal.
Matrix (Fin n) (Fin n) ℝ with A.PosSemidef and A ≠ 0; eigenvalues are Mathlib's IsHermitian.eigenvalues. is lambdaMax (the maximum eigenvalue) and is kappaF (maximum over minimum of the finite set of nonzero eigenvalues); both are Finset.max'/min'/sup' of nonempty finite sets. is a placeholder, and every statement assumes .z : Fin M → Ω → Fin n → ℝ satisfying IsNormalizedRayleighSample P A z: each measurable, the family mutually independent (iIndepFun), almost surely, and . The estimator is universally quantified over this class. Unbiasedness is required for the given only, as on the page. Probabilities are P.real of events; is a natural number and is (M : ℝ)⁻¹.IsNormalizedRayleighSample.Cost and benefit allocation problems arise whenever several parties share a joint undertaking: towns building a common water supply, divisions of a firm sharing overhead, users of a multi-purpose reservoir. They are modelled as cooperative games, and a rule that divides the joint value among the players is an allocation procedure. The standard such rule, the Shapley value, was characterized by Shapley (1953) through efficiency, symmetry, a dummy axiom and additivity. Additivity (the allocation of a sum of two games is the sum of the allocations) is a mathematical convenience with little direct appeal in applications, and it has been the most criticized of the four axioms.
H. P. Young's paper Monotonic Solutions of Cooperative Games (Int. J. Game Theory 14, 1985) studies allocation procedures through monotonicity: how a player's allocation should respond when the game changes. Its Theorem 1 shows that the core is incompatible with coalitional monotonicity for five or more players (the subject of the sister mission of this series). Its Theorem 2, the subject of this mission, shows that efficiency, symmetry and a single monotonicity axiom — strong monotonicity — determine the Shapley value, with no additivity axiom at all. The result is widely cited as Young's axiomatization of the Shapley value, usually in the form with the marginality condition (7) that the paper states in its remarks.
Timeline:
Fix and the player set . A game is a function on the coalitions with ; superadditivity is not assumed. An allocation procedure is a map assigning to each game a vector with (efficiency).
The marginal contribution of player to coalition (Eq. (3)) is
defined for every . The Shapley value is
The axioms:
A primitive game () takes the value on coalitions containing and elsewhere.
For every map from games on to ,
Both directions are part of the goal: the Shapley value has the three properties, and it is the only map that has them.
Efficiency and symmetry of the Shapley value are supporting theorems of the existence half; the paper uses them without separate statement.
The result. Theorem 2 shows that additivity is not needed to single out the Shapley value: a player's payoff is pinned down by symmetry, efficiency, and the requirement that it respond monotonically to that player's own marginal contributions. This gives the Shapley value a justification that can be checked directly in applications — a division that improves its marginal contributions to every coalition is never penalized — and the marginality form (7) is the standard starting point for characterizations on restricted classes of games and for extensions to games with a variable player set.
The formalization. The theorem is proved and classical; no machine-checked proof of it is known to exist. The mission produces a checked proof of Young's characterization together with reusable infrastructure: marginal contributions, the unanimity-game basis of the space of games (a Möbius-inversion statement on the subset lattice), the Shapley value on unanimity games, and the Shapley value's efficiency, symmetry and monotonicity for the published ShapleyValue definition. These are the ingredients of most other axiomatizations of the Shapley value (Shapley 1953, Hart–Mas-Colell's potential) and are useful beyond this mission.
The existence half is a direct computation. The uniqueness half cannot proceed by linearity, since is not assumed additive: knowing on each primitive game says nothing directly about on their sum. The obvious idea — decompose into primitive games and add up — therefore fails. What must be controlled instead is how much of a game each player "sees" through the marginal-contribution vector alone, and how symmetry and efficiency distribute what remains. The formal proof also has to manage the dependence of the argument on a minimal-length expression (9) while keeping all comparisons inside the class of games with .
Fin n: the paper's player is the Lean index . The player set is fixed, and is a single map Game n → Fin n → ℝ, as in the paper; no lower bound on is needed (at both sides of the goal hold).Game n := {v : Finset (Fin n) → ℝ // v ∅ = 0}. The normalisation is essential: on arbitrary set functions a constant game would receive per player from every efficient symmetric procedure, but from the Shapley formula, and Theorem 2 would be false.Supermodularity.Cooperative.ShapleyValue, written as a sum over with weight ; it agrees term by term with the formula above.Contributions welcome: proofs of the milestones in any order, general lemmas on unanimity-game expansions over Finset powersets, and alternative proofs of the uniqueness half.
Every packet-switched network — an internet router, a data-center fabric, a wireless base station — must decide, timeslot by timeslot, which of many competing transfers to schedule under shared physical constraints (link capacities, interference between simultaneous transmissions). Walton (2015) introduced the random proportional scheduler (RPS): rather than solving a combinatorial scheduling problem exactly, RPS picks a randomized link configuration whose mean matches the proportionally-fair allocation of Kelly (1997) applied at the link level, then disaggregates the resulting transfer budget across competing packet classes by independent random selection. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Sections 12.6-12.7 to this policy, and closes the book with Theorem 12.28: under an explicit load condition, RPS is stable. This mission formalizes that closing result and the machinery beneath it. It is the fourteenth and final mission of a series covering the book chapter by chapter; the series as a whole runs from the equivalence of stochastic-processing-network stability and fluid-model stability (mission I, Theorem 3.5/6.2) through discrete-time, slotted packet networks (missions XII-XIV), and this mission's own goal theorem is the last numbered result the book proves.
A packet network with fixed routing (Section 12.6) has I packet classes; each class i
routes, after one hop of processing, deterministically to a single successor class or exits the
network — encoded here as a function . The K
links are indexed by , and a matrix assigns each class to the single link its next
transfer uses; denotes the classes belonging to link . At the start of a
timeslot, is the vector of class-level packet counts and the
corresponding link-level counts. The RPS algorithm (four steps, page 245 of the printed book):
(a) solve the concave program (Eq. 12.57), where is the finite set of feasible link configurations
and its convex hull; (b) randomize a link configuration with mean ;
(c) transfer packets over link ; (d) select which packets to transfer uniformly
at random from each link's queue. This makes a discrete-time
Markov chain. The function is exactly the proportionally fair (PF) allocation function
of Section 10.1, applied here with the link-level demand vector in place of the PF model's
job-class demand vector.
Here is the vector of external arrival rates, the resulting vector of total (external plus internally routed) arrival rates into each class, and the input-output matrix determined by . The load condition (12.50) is the natural feasibility requirement — average link traffic strictly below some feasible mean capacity — and the theorem asserts it is also sufficient for stability.
Lemma 12.23 is an almost-sure convergence result for a residual process tracking the gap between RPS's actual per-class transfers and their conditional means — a bounded martingale-difference sum, hence governed by the strong law of large numbers. Theorem 12.24 is the RPS fluid equation: along any fluid limit on the event where both Lemma 12.12's arrival-process SLLN and Lemma 12.23's residual-process SLLN hold, every occupied class's departure rate is pinned to . Proposition 12.26 identifies the resulting RPS fluid model as literally a special case of the PF fluid model of Section 10.4 (one demand group per link, playing the role of the PF model's reduced allocation set), and Theorem 12.27 is this chapter's own version of the fluid-to-stochastic transfer theorem (Theorem 6.2's slotted-time analogue, restricted to RPS): fluid stability of the RPS model implies positive recurrence of .
The result itself. Theorem 12.28 closes the loop the book opens with proportional fairness in Chapter 10: PF was introduced there as a static resource-allocation rule with no queueing content; Theorem 12.28 shows that layering PF onto a genuinely dynamic, multi-hop, discrete-time packet network — RPS — inherits stability under exactly the load condition one would hope for, with no loss from the randomized disaggregation step (d) of the algorithm. Combined with Theorem 12.8 (packet-network stability implies subcriticality, mission XII) and Eq. (12.50)'s equivalence to that subcritical region under fixed routing, this makes RPS maximally stable: it is stable whenever any Markovian policy could be.
Formalizing it. A live prior-art check (GET /theorems?q=proportional+scheduling) finds no
relevant hits on the platform. This mission's genuine content is Proposition 12.26's reduction:
rather than re-deriving an entropy-Lyapunov stability argument specific to RPS, it identifies the
RPS fluid model precisely with mission IX's PF fluid model under an explicit correspondence, so
that Theorem 12.28(a) is a direct instance of mission IX's own Theorem 10.5 and Theorem 12.28(b)
a direct instance of this mission's own Theorem 12.27. This is the payoff the whole
proportional-fairness apparatus (missions IX-X) was built for.
The central subtlety is that Theorem 12.24's departure-rate equation is stated in terms of a
class-indexed process , while the chapter's own general fluid-equation machinery
(Theorem 12.13, mission XII) is built around an activity-indexed process — a distinction that
matters when a packet network has more service types than classes. Under Sections 12.6-12.7's own
fixed-routing model, however, the book's remark that " ... is an I-vector of actual
packet transfers by class" (page 245) collapses this distinction: each class has a single
associated activity, so the activity-indexed and class-indexed views coincide, and the RPS fluid
model can be built directly on the same class-indexed apparatus the PF fluid model (Section 10.4)
already uses. Missing this identification is the natural way to get stuck restating Proposition
12.26 as a mere analogy rather than the literal equivalence the book states. A second difficulty
is Lemma 12.23 itself: its proof cites Feller's strong law for bounded martingale-difference
sequences as an external fact rather than deriving it, so a faithful statement must commit to an
explicit representation of "martingale difference sequence" (a filtration and Mathlib's
Martingale predicate) even though no full measure-theoretic construction of the underlying
probability space is attempted.
Classes and links are Fin-indexed; route : Fin I → Option (Fin I) records each class's
deterministic routing successor (none meaning exit), and the resulting input-output matrix
and routing matrix are derived from it rather than taken as independent data (this chunk
verifies , the identity Proposition 12.26's reduction to the PF model relies on).
The RPS optimization apparatus (psi, groupAggregate, the PF fluid-model predicate) is restated
verbatim from mission IX, and the general packet-network fluid equations restated from mission
XII, since concurrently-drafted chunks in this series never import one another's Lean files even
within a shared sub-namespace. The formalization does not admit a trivializing reading: the load
condition in Theorem 12.28 is a genuine strict inequality against the convex hull of feasible
configurations (not weakened to or to a single configuration), RPSFluidStable quantifies
over every solution of the RPS fluid model (not a hand-picked one), and Proposition 12.26 is
stated as a two-sided equivalence, not a one-directional inclusion that would understate "special
case." Contributions completing the five by sorry proofs are welcome, particularly Lemma 12.23's
martingale strong law (Feller 1971, Theorem 3, Section VII.8) and Theorem 12.24's fluid-limit
argument (mirroring mission XII's own Theorem 12.13 proof).
Retailers of fashion and seasonal goods sell a fixed stock over a short season and routinely cut the price part-way through it. The markdown trades off two effects: a late discount keeps early, high-valuation customers paying the full price, while an early discount reaches customers whose interest in the product fades as the season goes on. Aviv and Pazgal (MSOM 2008) build a two-price model of this trade-off with Poisson arrivals and valuations that decline exponentially over the season, and compare sellers facing myopic customers, who buy as soon as the current price is acceptable, with sellers facing strategic customers, who may wait for the discount.
This mission formalizes the benchmark of that comparison in which the problem can be solved in closed form: myopic customers who all share the same base valuation, so that the only source of price discrimination is the decline of valuations over time. Proposition 4 of the paper identifies the optimal premium price, discount price and discount time, and the paper's Proposition 5 and Example 1 then measure how much strategic behaviour costs the seller against it.
The season is . Customers arrive as a Poisson process with rate , so is the expected number of arrivals in the season. Every customer has base valuation , and a customer's valuation at time is for a fixed decline parameter (equivalently with ; is the fraction of the valuation left at the end of the season). In the paper's notation this is the case , , of a family of Gamma-distributed base valuations with mean and coefficient of variation ; the tail of the base valuation is for and otherwise.
The seller posts a premium price on and a discount price from the discount time on, and has unlimited inventory. A myopic customer arriving at buys at once iff ; otherwise the customer waits and buys at iff . A customer arriving after buys iff the current valuation is at least . The expected numbers of buyers in the three groups are the segment rates , and , and the expected revenue is
For a price let , the time at which the valuation has fallen to , and write , . The reduced objective is
every maximizer of together with every with attains , and, if , the maximizer is unique,
and every with is optimal.
For :
Proposition 4 gives an explicit optimal markdown policy in a model where segmentation happens purely by arrival time: it shows that the discount time is not pinned down but can be placed anywhere in the interval in which the valuation lies between the two prices, and that for strongly declining valuations the optimal prices do not depend on at all. The paper uses it as the benchmark against which the strategic-customer equilibrium of Proposition 5 and the losses of Example 1 are measured.
The result is proved in the paper by a short argument; nothing in it has been machine-checked. A formal development makes the three observations of the proof precise (in particular, that prices outside are dominated, which the paper leaves implicit) and supplies the omitted calculus for the special case.
The revenue is defined through integrals of a step function of time, and the reduction to needs these integrals evaluated in every configuration of , and , including prices above (nobody buys) and below (everyone buys, at a needlessly low price). The paper's proof covers only and asserts the domination of the remaining prices without argument. The special case is a constrained two-variable maximization of a function that is not jointly concave; the unconstrained critical point must be shown to be feasible exactly when , and boundary points of the region must be excluded.
Everything is over . Logarithms are Real.log, powers are real powers, the segment rates are interval integrals ∫ t in a..b of the tail , and with . The model definitions (, , and the revenue) are stated for a general tail , decline factor, season length and discount time and then specialized.
The following readings of the paper's words are fixed:
IsGreatest of the set of attainable revenues.The decimals and are not stated. A formalization that restricted prices to in the revenue maximization, or that fixed in advance, would assume half of what the proposition proves and is ruled out. Welcome contributions include general lemmas evaluating interval integrals of indicator functions of intervals, and the domination argument for prices outside .
Robust optimization (RO) protects a decision against every parameter value in an uncertainty set. For a decision and a parameter with objective to be maximized, the robust problem around a nominal parameter with a deviation set is
When deviations are not adversarial, this formulation is known to be conservative (Delage and Mannor, 2010; Xu and Mannor, NIPS 2006). A common remedy in practice is uncertainty set shrinkage: fix and solve the same problem over the shrunken set . The heuristic is easy to implement, but the meaning of the set is unclear, and it has lacked a justification.
Section 4.2 of Xu, Caramanis and Mannor (2012) supplies one, using the paper's distributional interpretation of RO: the shrunken problem approximately solves a distributionally robust stochastic program (DRSP) with two scenarios. This mission formalizes that result, Theorem 4.1, and its two corollaries.
Let carry the Euclidean norm and its Borel -algebra, and let be the set of Borel probability measures on . Let be any set of decisions and . Fix , a deviation set , and . Write .
The two-scenario set is
A distribution in describes a system that is, with probability at least , in a normal state where the parameter equals , and otherwise in an abnormal state where the parameter deviates by an element of . The DRSP value of a decision is .
Two further quantities enter. The radius of the deviation set is . The curvature bound is a constant with
where is the Hessian of at and is the positive-semidefinite order. In the Lean development these are scenarioSet x₀ Δ (1 - α), drspValue, devRadius Δ and HasBoundedHessian (f v) h, all in the namespace DistInterpRO.Shrinkage.
If is twice differentiable with for all , then for all
Corollary 4.2 (p. 104): if every is linear, the shrunken value equals the DRSP value exactly. Corollary 4.3 (p. 105): if is star shaped, every is convex with and has Hessian bounded by , then the shrunken value lies between the DRSP values over and , where requires only .
The result gives a physical meaning to the parameter of the shrinkage heuristic: is a lower bound on the probability that the system is in its nominal state. The error vanishes when the objective is linear in the parameter (Corollary 4.2), which covers linear programs with uncertain costs and Markov decision processes with uncertain rewards; in that case shrinkage is exactly a two-scenario DRSP. The paper also shows by example (p. 104) that without a curvature condition the two problems can differ, so the Hessian bound is the operative hypothesis.
The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it adds a checked link between the discrete two-point structure of the DRSP value and the smooth analysis of the shrunken minimum, with every standing hypothesis written out (see below). The mean-value and gradient-Lipschitz steps are general facts about functions on Euclidean space with bounded Hessian and are reusable elsewhere.
Two points need care. First, the step from the Hessian bound , a bound on a quadratic form, to the Lipschitz bound on the gradient requires the operator norm of the Hessian, which equals the largest absolute value of its quadratic form only because the Hessian is symmetric; symmetry of second derivatives must be invoked for a function that is merely twice (Fréchet) differentiable, not twice continuously differentiable. Second, the DRSP value is an infimum over an infinite-dimensional set of measures; identifying it with the two-point value requires both a construction of a near-optimal measure and a lower bound valid for every admissible measure, including measures that spread their abnormal mass over all of .
is EuclideanSpace ℝ (Fin m) with its Borel -algebra. Measures are Measures, and membership in includes IsProbabilityMeasure. Infima are real infima over subtypes; integrals are Bochner integrals.
The formalization makes the following readings explicit:
The Lean functions drspValue and devRadius return on an empty or unbounded input; the hypotheses above exclude those inputs, so no statement holds through a junk value. A formalization that dropped would make the inequalities hold or fail for the wrong reason and is ruled out.
Contributions welcome: the Lipschitz-gradient lemma for bounded Hessians in Euclidean space, the evaluation of the two-scenario DRSP value, and the combination into Theorem 4.1 and its corollaries.