Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Matroid intersection is one of the founding results of combinatorial optimization: given two matroids on a common ground set, the largest common independent set can be found in polynomial time, and its size equals the minimum of a natural upper bound ranging over all subsets — a min-max theorem in the spirit of König's theorem and Menger's theorem, but for a strictly richer combinatorial structure. Jack Edmonds proved this in 1970, and Jack Edmonds and Rick Giles's subsequent generalization to submodular flows, together with André Frank's discrete separation theorem for submodular and supermodular set functions (1982), placed matroid intersection inside a single unifying framework: submodular function duality. This framework explains, in one stroke, matroid intersection, the base-exchange structure of matroids, and a family of other combinatorial min-max theorems that had previously seemed unrelated.
Murota's Discrete Convex Analysis develops this framework as the theory of M-convex sets: sets of integer vectors satisfying a lattice-exchange axiom that turns out to be exactly equivalent to being the integer points of a base polyhedron of an integer-valued submodular set function. This mission formalizes the chapter's central results: the equivalence of four variant forms of the exchange axiom (Theorem 4.3), the M-convex set / submodular function correspondence (Theorem 4.15), Frank's discrete separation theorem (Theorem 4.17), and Edmonds's intersection theorem itself (Theorem 4.18) — the deepest duality result in the theory of submodular functions and the historical origin of the M-convexity concept that the rest of the book generalizes to real-valued functions.
Let be a finite ground set. A set function with and is submodular (the class ) if
Its base polyhedron and submodular polyhedron are
where ; a supermodular function is one with submodular. A nonempty set is an M-convex set if it satisfies the exchange axiom (B-EXC[Z]): for and in the positive support of , there is in the negative support of with both and , where is the characteristic vector of . A polyhedron is integral if .
For submodular set functions ,
with both sides attained. If are integer valued, is an integral polyhedron and the maximum is attained at an integer point. Dropping the integrality clause and stating only the real max-min equality would leave ordinary LP duality with no discrete content at all; this mission keeps it in the goal at every strength the book proves it.
Theorem 4.3: the exchange axiom (B-EXC[Z]) is equivalent to three variants that impose the exchange condition asymmetrically or only for distinct vectors — groundwork establishing that M-convexity does not depend on which variant is taken as primitive. Theorem 4.15: is M-convex if and only if for some integer-valued submodular — M-convex sets and integer-valued submodular set functions are two descriptions of the same combinatorial object. Theorem 4.17 (Frank): if a submodular dominates a supermodular pointwise, a single vector separates them ( pointwise on every subset), integrally when are integer valued — derived, in the book, as a direct corollary of the goal theorem.
The result itself. Edmonds's intersection theorem is the min-max theorem underlying polynomial-time matroid intersection (a matroid's rank function is submodular, so the classical matroid intersection theorem is the special case both matroid rank functions), and its generality — arbitrary submodular set functions, not just matroid ranks — is what lets Frank's discrete separation theorem, and through it a wide range of combinatorial duality results in network flows, scheduling, and matroid theory, be derived as corollaries rather than proved from scratch each time. The integrality clause specifically is the fact that makes these duality theorems combinatorial: it guarantees that optimal fractional solutions to the underlying linear program can always be taken integral, without which the connection to discrete optimization would be lost.
Formalizing it. No matching item exists on the platform (searches for "submodular set
function", "base polyhedron", "matroid intersection" return no relevant hits; Mathlib's
Combinatorics/Matroid/ develops matroid rank functions, a special case, but not general
submodular set functions or their polyhedra). This mission gives the first formal statement of
the theorem at its natural generality, together with the M-convex-set viewpoint that motivates
the rest of the book, and Frank's separation theorem as an explicit worked corollary.
The real-valued half of Theorem 4.18 is ordinary LP duality applied to a cleverly chosen primal program (maximize over ) and its dual — routine once the right LP is written down. The integrality half is where the combinatorics enters: an optimal dual solution can always be chosen supported on a chain in each 's effective domain (an extremal argument maximizing a strictly convex potential over the optimal dual face), and the incidence matrix of a chain of subsets is totally unimodular — this is the fact, external to ordinary LP theory, that forces an integral optimal solution to exist whenever the data () are integral. A proof that stops at real-valued LP duality, however carefully done, misses this step entirely and cannot produce the integrality clause; total unimodularity of a chain's incidence matrix is the one piece of combinatorics doing all the discrete work in an otherwise classical convex-duality argument.
The ground set is a Fintype with DecidableEq; subsets are Finset V, vectors are
V → ℝ/V → ℤ. Submodular functions take values in WithTop ℝ (exactly ); supermodular functions in WithBot ℝ; comparisons across the two use an explicit
embedding into EReal. The max/min in the goal are stated via IsGreatest/IsLeast sharing a
common EReal witness, so that "both sides attained, at the same value" — not merely "sup
equals inf" — is what the Lean statement asserts, which is essential since the integrality
clause's whole content is about which point attains the maximum.
A trivializing formalization of the goal would drop the integrality clause (leaving unqualified
LP duality) or replace IsGreatest/IsLeast with a bare supremum/infimum equality (losing the
"is attained" content the second half of the theorem needs); both are avoided. Theorem 4.15 is
stated as the existential "iff" (some integer submodular realizes ) rather than
reifying the book's own named bijection explicitly — a deliberate, documented scope
reduction of that one milestone (see MODERATION_NOTES.md), not of the goal. Contributions
building the explicit map, the Lovász extension (needed for Theorem 4.16, not drafted
here), or M-convex-set infrastructure reusable by chunks 06–07 (M-convex functions, which build
on this chapter's vocabulary) are welcome.
Every model in Chapters 2-4 assumed the controller sees the whole state before acting. Real control problems rarely offer that: a machine's true wear level, a customer's private valuation, a hidden regime driving asset returns — these are exactly the situations a decision-maker must act on despite never observing them directly, learning about them only through their effect on what is observed. This is the subject of Partially Observable Markov Decision Processes (POMDPs), introduced independently in operations research (K. J. Åström, Optimal Control of Markov Processes with Incomplete State Information, 1965) and studied extensively since as the right model for sequential decisions under hidden state. The central difficulty such a process raises is structural, not just computational: the state includes a component the controller never sees, so the very theory built in Chapter 2 — which assumes the controller's policies can depend on the full current state — does not apply. Bäuerle and Rieder's Chapter 5 resolves this by an idea with a long pedigree in stochastic control (Bayesian filtering, going back to R. E. Kalman and R. S. Bucy's filtering theory, and D. Blackwell's 1965 discounted-dynamic-programming treatment of the "state of information"): replace the unobservable state by the controller's own belief about it — a probability distribution, updated at every step by Bayes' rule — and show the resulting belief-state process is once again an ordinary, fully observed Markov Decision Model.
A Partially Observable Markov Decision Model (Definition 5.1.1) has data : state with observable and unobservable; feasible actions depending only on ; a stochastic kernel giving the joint law of the next state; initial law of ; rewards ; discount . A policy (Definition 5.1.3) is a sequence of decision rules , each depending only on the observable history — never on any . The objective
(Equation (5.2)) carries an extra expectation over the unknown that Chapter 2's objective never had.
Assuming has a density against reference measures, the Bayes operator and the filter recursion , (Equations (5.3)-(5.4)) compute the posterior law of given everything observed, purely from the observable history. Theorem 5.2.1 confirms is genuinely this conditional law. The filtered Markov Decision Model (Definition 5.3.1) then treats as an ordinary, fully-observed state, with its own kernel (built from and the marginal ), reward , and terminal reward .
under the Structure Assumption of Theorem 2.3.8; and if maximizes for each , then defines a policy optimal for the original -stage POMDP. This is where the reduction pays off: an ordinary Bellman equation, of exactly the form Chapter 2 already solves, for a problem that had no Bellman equation at all in its original, partially-observed form.
Lemma 5.2.2 (the filter-recursion identity, the technical engine behind everything that follows), Theorem 5.2.1 (the filter is truly the conditional law — without this, would be merely a formula, not a meaningful belief), and Theorem 5.3.2 (the value of the filtered model exactly equals the value of the original POMDP, policy for policy — without this, solving the filtered model would solve a different problem).
Theorem 5.3.3 is the standard justification, made precise, for the single most common technique
in applied sequential decision-making under uncertainty: replace an unknown parameter or hidden
state by a running Bayesian estimate, and optimize as if that estimate were the true state. This
technique underlies applications from inventory control with unknown demand to adaptive clinical
trial design, and Chapter 5's own closing application (two-armed Bernoulli bandits, taken up in
chunk 05b) is a direct instance. The reduction also has real content beyond convenience: it
shows the value is unchanged (Theorem 5.3.2), not merely that a good heuristic policy exists —
the filtered model's optimum is the true POMDP optimum, not an approximation to it.
No result of this chapter has a machine-checked proof on Prove2Me at the time of writing, and no substrate exists for POMDPs, filtering, or Bayes-operator constructions on the platform. Formalizing this mission means building, from Mathlib's general kernel and probability-measure infrastructure, the first POMDP/filtering vocabulary on the platform: a policy class restricted to observable histories, a recursively-computable posterior, and the value-equality between a partially and a fully observed reformulation.
The obstacle is not any single hard inequality but a representational one: an admissible policy for the original problem is a function of a growing observable history, not of a fixed-size state, so the value function cannot be written as a simple recursion over a Markov chain the way every earlier chapter's could. The chapter's insight is that the belief — even though it is a probability-measure-valued object, not a point in a fixed Euclidean space — is itself Markov: depends on the observable history only through , never on more of the past. Recognizing this, and giving the right measurable structure to serve as a genuine Borel state space, is what makes Definition 5.3.1's reformulation a legitimate Markov Decision Model rather than an informal analogy. A formalization that let 's type be an unstructured "distribution object" with no Borel structure, or that quietly assumed the value functions of the filtered model already satisfy the Bellman equation, would miss this content entirely.
are abstract measurable spaces; the transition kernel is a genuine
MeasureTheory.Kernel, not assumed to arise from an i.i.d.-noise-driven transition function (the
form every earlier finance chapter's market used) — the chapter's own examples (Hidden Markov
Models, Bayesian models) do not have that special form in general. Observable histories are
represented as (junk-padded) sequences , rather than
dependent finite tuples, with a decision rule's dependence on only the first /
coordinates stated as an explicit locality condition; this avoids Fin-indexed-tuple bookkeeping
while remaining exactly equivalent to the book's own typing. The belief state
is MeasureTheory.ProbabilityMeasure E_Y, giving a genuine measurable
structure via its standard weak-topology Borel σ-algebra — the formalization scope this chunk's
own pitfall demands, ruling out an ad hoc encoding of "the space of distributions." The Bayes
operator and the filtered kernel are carried as data (functions landing genuinely in
ProbabilityMeasure/Kernel types) characterized by their defining ratio-of-integrals or
pushforward formulas, rather than constructed by normalizing a raw measure inline — proving
that normalization is a routine Fubini calculation the book itself does not spell out, and would
be proof content misplaced in a definition. Theorem 5.2.1's conditional-probability statement is
formalized via the book's own Equation (5.5) test-function identity rather than Mathlib's
conditional-expectation-with-respect-to-a-sub-σ-algebra machinery, since the two are equivalent by
the standard characterization of conditional expectation and the test-function form is what the
book's own proofs actually use. The Structure Assumption of Theorem 2.3.8 is restated locally
(existential value-function and decision-rule classes with its three defining clauses), per this
project's rule against importing another chunk's copy of shared machinery. Reusable beyond this
mission: the kernel-based expectation recursion (Ex/Vpi) is natural substrate for any later
mission needing a Markov Decision Process driven by a genuinely abstract stochastic kernel rather
than an i.i.d.-noise transition function. Contributions completing any milestone's sorry, or the
goal's, are welcome.
Many first-order methods in optimization are fixed-point iterations of a nonexpansive map : proximal gradient descent, projected gradient descent, alternating projections, ISTA and Douglas–Rachford splitting (with the conic solver SCS as an instance) all have this form (Zhang, O'Donoghue, Boyd 2020, §4.2). The averaged (Krasnosel'skiĭ–Mann) iteration converges to a fixed point whenever one exists, but it is often slow in its terminal phase. Anderson acceleration (AA) combines the last few iterates through a quasi-Newton update of an approximate Jacobian; it is used for electronic-structure computations and, in the stabilized form studied here, in the solver SCS 2.1. Its type-I variant (AA-I) is often faster in practice than the more studied type-II variant, but it can be numerically unstable, and no global convergence guarantee existed for it on nonsmooth problems.
Timeline (as recounted in the paper's related-work section):
Let satisfy for all (the Euclidean norm), and assume the solution set is nonempty. The residual is , , and the averaged operator is .
Powell's weight. For , if and otherwise, with .
Window matrices. For vectors and , let be their unnormalized Gram–Schmidt orthogonalization (3.2), , and
The matrix norm is the induced operator norm.
Algorithm 3.1 (AA-I-S-m). With parameters , and max-memory : start from , , , and . At iteration , set and , orthogonalize against the current window, and restart the window (memory back to , replaced by ) if the memory would exceed or . Then apply one Powell-regularized rank-one update to obtain and the trial point . The trial point is accepted if (and increases); otherwise .
The only hypotheses are nonexpansiveness of , and the parameter ranges. The limit is not specified: it depends on and the parameters.
The theorem places a quasi-Newton acceleration scheme under the same hypotheses as the plain averaged iteration: nonexpansiveness and existence of a fixed point. It therefore applies at once to the nonexpansive examples of §4.2 of the paper (proximal gradient, projected gradient, alternating projections, ISTA, Douglas–Rachford splitting and SCS), with no smoothness, strong convexity or local assumption. The matrix bounds of Lemma 3.3 and Corollaries 3.4–3.5 are also of independent use: they give explicit, iteration-independent control of the approximate inverse Jacobians of a limited-memory type-I method, an assumption that other globalization frameworks (for example SuperMann) have to impose.
The result is proved in the paper; to our knowledge none of it is machine-checked. Mathlib has neither the Krasnosel'skiĭ–Mann iteration, nor Fejér monotonicity, nor any Anderson-type method. A formalization provides these pieces, checks the index bookkeeping of the restart and safeguard steps, and makes explicit the one place where the printed algorithm and the analysis disagree (line 9 at a window start; see below).
The accelerated step need not decrease the distance to the solution set, so the Fejér argument for averaged iterations does not apply to it directly. The naive fix, bounding , requires a bound on that holds uniformly along the run; without the Powell regularization can be singular, and without the restart rule can grow without bound as the window becomes nearly linearly dependent. The determinant and norm bounds of Lemmas 3.2–3.3 have to be established for arbitrary windows and then connected to the run of the algorithm, where the window, its orthogonalization and the matrices are defined by an intertwined recursion with resets. The safeguard then turns the uniform bound into a summable perturbation of a Fejér-monotone sequence, and the final step needs an Opial-type argument to pass from convergence of distances to convergence of the iterates.
is EuclideanSpace ℝ (Fin n), so all vector norms are Euclidean; matrices are continuous linear maps with the operator norm; is rankOne ℝ u ŝ; is LinearMap.det; inverses are Ring.inverse (zero on singular maps, excluded by Lemma 3.2). The orthogonalization (3.2) is InnerProductSpace.gramSchmidt. Nonexpansive is LipschitzWith 1 f. The algorithm is the predicate IsAAISRun, a deterministic recursion: every run is determined by , the parameters and , and a sorry-free check that runs exist (for ) was built locally. The reset of in line 8 is local to its iteration. is encoded explicitly. Constants are the paper's explicit expressions; no milestone replaces them with an existential constant.
Line 9. The paper prints , derived from (3.3) through , which fails when the window starts afresh (). The mission uses (3.3) there: when , and the printed formula when .
Milestones of §4.1 and Corollary 3.5 carry the hypothesis for all , as the paper does ("we temporarily assume for simplicity that a solution to (1.1) is not found in finite steps"); the goal does not. A goal proved from an unsatisfiable run predicate, or one that assumes a bound on , contractivity of , or that the accelerated step is never taken, is not this theorem. Division by zero in Lean can only occur once a fixed point has been reached, after which all later iterates coincide.
Useful reusable infrastructure includes the Krasnosel'skiĭ–Mann inequality , quasi-Fejér monotone sequences and their convergence, and determinant and norm identities for rank-one updates (the matrix determinant lemma and Sherman–Morrison). Proofs of the window lemmas, of the run invariants (the window matrices coincide with the algorithm's ) and of the convergence steps are all welcome.
A manufacturer that makes several products must decide, before demand is known, how much capacity to buy. It can buy dedicated capacity, one resource per product, or a single flexible resource that can make every product. Flexible capacity pools demand: a surplus of one product's demand can be served by capacity that would otherwise sit idle. A common intuition in the operations literature holds that a flexible strategy is preferable to a dedicated one when the unit costs are equal, and much of that literature therefore assumes the flexible resource costs more (for example Van Mieghem 1998).
Tomlin and Wang (2005) examine when this intuition is valid for firms that are not risk neutral and whose resources may fail. Their answer has two halves. A risk-neutral firm always values flexibility, whatever the reliability of its resources (their Proposition 1). A firm with perfectly reliable resources also always values flexibility, whatever its attitude to risk, as long as it prefers more wealth to less (their Proposition 4). When neither condition holds, dedicated capacity can be strictly preferred (their Remark 1 and numerical study). This mission formalizes the second half.
There are products with a common contribution margin . The random demand vector is , nonnegative, with an arbitrary joint distribution on a probability space. The firm has initial wealth .
The firm chooses its investment to maximize one of three objectives of terminal wealth , with profit :
SF is (weakly) preferred when its optimal objective value is at least that of SD. The flexibility premium is , where the indifference cost is a flexible cost at which the firm is indifferent between the networks; the firm prefers SF as long as .
With perfectly reliable resources and any demand distribution, for every , for the loss-averse objective and for the CVaR objective. In the formalization: for every ,
for each expected utility with nondecreasing, and the loss-averse objective; for CVaR the same with the threshold quantified jointly with the investment.
Proposition 4 shows that the intuition "flexibility is worth at least as much as dedicated capacity at the same price" survives any monotone risk attitude and any demand distribution, provided supply is reliable. Combined with Proposition 1 it isolates the interaction of risk aversion and unreliable supply as the only source of a negative flexibility premium, which is the paper's Remark 1 and the organizing message of its numerical study. The result requires no concavity, differentiability or distributional assumption, so it applies to the loss-averse and CVaR objectives used throughout the paper.
The result is proved in the paper (Appendix A); no machine-checked version is known. A formalization produces a reusable statement of the model, a pathwise pooling inequality, and the passage from a pathwise comparison of two random variables on one probability space to comparisons of expected utilities and of CVaR, which recurs in capacity-pooling and inventory-pooling arguments.
The pathwise inequality is elementary. The work lies in the passage from it to the objectives. The paper cites Levy (1992) for both the expected-utility and the CVaR comparison; the first holds for every nondecreasing , including discontinuous ones, and the second concerns a maximum over a real threshold that is not a priori attained. A formal proof must also make sure every expectation involved is a genuine integral: the utility is arbitrary, so the expected utility is finite only because, for a fixed nonnegative investment and nonnegative demand, both wealths are confined to a bounded interval. Finally, "" is a statement about optimal values, and the optimal SD investment need not exist; the argument has to be run for every SD investment, not for an optimal one.
All declarations live in the namespace MixFlex.Reliable. The probability space is (Ω, μ) with IsProbabilityMeasure μ; demand is a measurable X : Ω → Fin N → ℝ with each coordinate almost surely nonnegative, and no density, independence or integrability is assumed. Expectations are Bochner integrals. Perfect reliability () is built into the wealths (A-4)–(A-5), so the committed-cost fraction does not appear. Standing parameters: , , , , arbitrary. The requirements and nonnegative, measurable demand are made explicit; the page treats them as part of the model.
The premium and the indifference cost are not defined as real numbers, since the indifference cost need not be unique. "" is encoded as "SF is weakly preferred for every ", and "weakly preferred" as "every nonnegative SD investment is matched or beaten by a nonnegative SF investment", with no real suprema. For CVaR the maximum in (8) over the investment and the threshold is encoded in the same matching form. The milestones compare the objectives at the flexible cost , as (A-5) is printed.
A formalization in which the expected utility of a non-integrable wealth defaults to zero, or in which makes the CVaR bracket , would make the comparisons meaningless; the statements exclude both ( with nonnegative demand bounds the wealths; ). "" is also not trivially true: for a flexible cost above SF can be strictly worse.
Out of scope: Propositions 1–3 and 5–8 (Proposition 1 is the companion mission on the risk-neutral premium), Remark 1's negative-premium claim and the numerical study. Welcome contributions: a general lemma that an almost-sure inequality between bounded random variables transfers to expected utilities of monotone functions, and a proof of the CVaR bracket comparison.
The traveling salesman problem (TSP) asks for a shortest closed route through a finite set of points. It is NP-hard, and in practice tours are built by fast constructive heuristics whose output is then improved or used as is. A central question in the analysis of algorithms, raised in this form by Rosenkrantz, Stearns and Lewis in 1977, is how far such a heuristic can be from optimal in the worst case, as a function of the number of points , when the distances satisfy the triangle inequality.
The paper (SIAM J. Comput. 6(3), 1977) answers this for several heuristics. For the general class of insertion methods it proves a logarithmic bound (Theorem 3); for two specific rules, nearest insertion and cheapest insertion, it proves a bound that does not grow with : the tour is less than twice the optimal (Theorem 4), and more precisely at most times the optimal (Corollary, eq. (4.12)). Theorem 5 of the same paper shows the constant is attained, so this is the exact worst case of both rules. These results, with Christofides' 3/2 bound of 1976, are the classical reference points for approximation ratios of TSP construction heuristics and appear in standard OR and approximation-algorithm texts.
A traveling salesman graph has a finite node set with and a distance that is symmetric, nonnegative and satisfies the triangle inequality . A tour is a circuit visiting every node exactly once; its length is the sum of its edge lengths, and OPTIMAL is the least tour length.
A subtour is a tour on a subset of (a one-node subtour has no edges). For , inserts into where it is cheapest: if has at least two nodes, choose an edge of minimizing and replace it by ; if , form the two-node tour on . is the length of minus the length of .
An insertion method builds subtours with and for some , ; INSERT is the length of . With :
The start node and every tie (between candidate nodes, and between candidate edges) are arbitrary. TREE denotes the length of a minimal spanning tree of .
For every traveling salesman graph on nodes and every run of nearest insertion or of cheapest insertion,
Theorem 4 itself, when is not identically zero, is included as a companion statement.
The bound says that two simple and construction rules are never worse than a factor from optimal on any metric instance, a guarantee independent of , in contrast with nearest neighbor and with arbitrary insertion orders, whose ratios the same paper shows can grow logarithmically. Lemma 3 is reusable on its own: any insertion rule satisfying the local inequality (4.5) inherits the bound , and the paper notes that similar arguments apply to nearest addition and nearest merger.
The result has been proved since 1977. The Prove2Me library has a machine-checked proof of the weaker statement for nearest insertion only with constant (SupplyChainTheory.nearest_insertion_bound, from Snyder–Shen, Theorem 10.7) and of (SupplyChainTheory.mst_lower_bound). This mission asks for the paper's full statement: both rules, the exact constant , and the general Lemma 3 via its correspondence between insertion steps and spanning-tree edges. Paired with the tightness result of the companion mission (Theorem 5), it would give a formally verified exact worst-case ratio for both heuristics.
Lemma 2 and inequality (4.5) are local consequences of the triangle inequality; the difficulty is global. The obvious attempt at Lemma 3 charges step to the tree edge joining to its nearest node of , but distinct steps can then be charged to the same tree edge, and the sum of the charges no longer bounds . Any correct argument must control how the insertion order interacts with the structure of an arbitrary spanning tree, which in Lean means reasoning about paths in SimpleGraph together with the evolving subtours. For cheapest insertion the chosen node need not be a nearest node, so (4.5) is not immediate from the rule. Finally, the goal's constant is sharper than the bound obtained from , so the weaker spanning-tree bound already in the library does not suffice.
Nodes are Fin n with (the paper's nodes shifted to ). The distance satisfies the paper's three axioms plus the normalization , which never affects a tour, subtour or tree length. Tours are permutations; OPTIMAL is a minimum over all of them (Finset.inf'). Subtours are lists of distinct nodes with closed length. is encoded as insertion of at a list position whose resulting length is minimal over all positions, which is the minimization of (3.1) over the edges of ; COST is the corresponding minimum increase. The subtour index is 1-based as printed (, final). The distance is taken in , so no default value enters the nearest rule. Spanning trees are SimpleGraph (Fin n) with IsTree; statements about TREE are phrased over every spanning tree (upper bounds) or some spanning tree (bounds on TREE), which is equivalent. Ratios are multiplied out, so the goal needs no nontriviality hypothesis; Theorem 4's strict form carries the paper's exclusion of the identically zero distance (p. 564).
A formalization in which TOUR inserts at an arbitrary rather than a cheapest position, or in which the run fixes the start node or the tie-breaking, would state a different (and, for arbitrary positions, false) theorem; the statements here quantify over every run.
A complete development needs subtour-length lemmas for List.insertIdx, the telescoping identity (3.7), and a spanning-tree edge-assignment argument on Mathlib's SimpleGraph paths; the last two are reusable for other insertion rules and for the companion missions of this series. Proofs of any milestone are welcome independently.
A firm that sells several products must decide, before demand is known, how much production capacity to build and of what kind. Dedicated capacity makes one product; flexible capacity makes any of them. The classic argument for flexibility is demand pooling: capacity that can follow demand to whichever product needs it wastes less than capacity locked to one product (Fine and Freund 1990; Van Mieghem 1998).
When capacity itself is unreliable, as with a supplier that may fail to deliver, a plant that may be disrupted, or a batch that may be rejected, flexibility has a second face. A single flexible resource concentrates the firm's supply in one place, so one failure removes all of it, whereas several dedicated resources rarely fail together. This resource-aggregation effect works against flexibility. Tomlin and Wang (2005) set up a newsvendor network in which both effects are present and ask when a firm should pay more for flexible capacity than for dedicated capacity. Their first answer (Proposition 1) is that a risk-neutral firm facing equal reliabilities and costs never loses by choosing flexibility, whatever the joint distribution of demand. This mission formalizes that answer.
There are products with a common unit contribution margin . The demand vector is random, nonnegative and integrable; its total is .
Two networks are compared. In the dedicated network SD, resource makes only product and has marginal total cost . In the flexible network SF, a single resource, labelled , makes every product and has marginal total cost .
Every resource is unreliable with a Bernoulli yield , . The common reliability is , the yields are mutually independent, and they are independent of demand. Investing in resource delivers capacity and costs : the firm pays the committed cost per unit ordered and a further per unit delivered, with .
The realized profits are
and a risk-neutral firm maximizes the expected profit or over nonnegative investments. Let and be the optimal values. SF is (weakly) preferred if .
The indifference cost is a value of at which , and the flexibility premium is . The firm prefers SF as long as .
The -expected shortfall of a random variable is, for and the lower quantile ,
For any demand random vector :
No distributional form of demand is fixed and no constant is hard-coded beyond the paper's threshold.
and the optimal values are times partial expectations of demand.
Proposition 1 separates the two effects of flexibility under unreliable supply. It shows that for a risk-neutral firm the demand-pooling benefit together with an upside effect of aggregation (one flexible resource succeeds more often than all dedicated ones together) always outweighs the downside aggregation risk. Even with no pooling benefit at all (perfectly correlated demand) the firm is indifferent, not averse. The later results of the paper (loss aversion, CVaR, dual sourcing) are measured against this baseline: a negative premium can appear only once the firm is risk-averse. The expected-shortfall form links newsvendor optimal values to a coherent risk measure, a connection that recurs in inventory risk analysis.
The result is proved in the paper, with a proof that cites Acerbi and Tasche (2002) for two properties of expected shortfall. No machine-checked version exists. A formalization adds three things: a proof for general demand distributions (the paper assumes a joint density and uses the continuous form of expected shortfall); a Lean development of Acerbi–Tasche expected shortfall for general integrable random variables, including subadditivity and affine equivariance; and a reusable model of newsvendor networks with Bernoulli yields and committed costs.
The newsvendor steps (9)–(13) are single-variable concave optimization, but they must be done without a density: the distribution function of total demand may have atoms and flat pieces, so the critical fractile need not be attained or may be attained on an interval, and optimal values must be expressed through lower quantiles. Subadditivity of expected shortfall is the heart of part 1 and is not elementary in the general (atomic) case, which is exactly why the correction term appears. Part 3 requires identifying correlation with almost-sure positive affine dependence, which rests on the equality case of the Cauchy–Schwarz inequality in , and then handling nonnegativity constraints on the investments that the affine change of variables may violate. The obvious shortcut of computing everything from densities is not available, because the goal is stated for every demand vector and part 3 is incompatible with a joint density when .
Randomness lives on one probability space ; demand is X : Ω → Fin N → ℝ and yields are Y : Ω → Fin (N + 1) → ℝ, where dedicated resource is Fin.castSucc n and the flexible resource is Fin.last N. Expectations are Bochner integrals and probabilities are μ.real. The standing assumptions are: , , ; demands measurable, almost surely nonnegative and integrable (integrability is needed for expected shortfall and makes every profit integrable); yields measurable, -valued almost surely with , mutually independent, and independent of demand (the paper states the last in Appendix E). The paper's joint density of demand is deliberately not assumed.
The premium and the indifference cost are not defined as real numbers, because Definition 1's indifference cost need not exist or be unique (for below the threshold both optimal values are for every near ). "" is encoded as "SF is weakly preferred for every ", and "" as "SF and SD are each weakly preferred to the other at ". Weak preference is stated as: every nonnegative SD investment is matched by some nonnegative SF investment; no real supremum is taken. Quantiles in (10) and (12) appear only as parameters with the hypothesis fractile. Part 3 adds square integrability and positive variances, the conditions under which correlation coefficients exist; the threshold milestone adds almost surely positive demand and for its "if" direction. When the Lean value of the threshold is , so part 2 then covers only , where it is true.
A formalization that assumed a joint density, took as a free real satisfying Definition 1, or defined optimal values as real suprema over all of would make parts of the goal vacuous or trivial; each is ruled out above.
Needed infrastructure: single-variable newsvendor optimality for general distributions; the Acerbi–Tasche expected shortfall with subadditivity and affine equivariance; the equality case of Cauchy–Schwarz for correlation. The expected-shortfall and correlation lemmas are reusable well beyond this mission, and contributions of them are especially welcome. Out of scope: the loss-averse and CVaR analyses (Propositions 2–3, §3.2–3.3), the perfect-reliability result (Proposition 4, a separate mission), the dual-sourcing networks (§4) and all numerical results.
For a convex function on , a point is a global minimizer as soon as it is a local minimizer — this is one of the earliest and most consequential facts of convex analysis, and it underlies why local-search and gradient methods can certify global optimality in convex programs. The discrete analogue is not automatic: a function on the integer lattice can be "locally optimal" with respect to any fixed finite neighborhood system and still fail to be a global minimizer, unless the function's discrete structure is compatible with that neighborhood in the right way. Identifying exactly which classes of lattice functions admit a local-to-global optimality principle, and with respect to which neighborhood, is one of the organizing questions of discrete convex analysis.
Integrally convex functions, introduced by Favati and Tardella (1990) and developed systematically by Murota, are the most general class of -valued functions for which such a principle holds. They are defined purely in terms of the classical convex closure of a real relaxation, which lets one import theorems from ordinary convex analysis, but the resulting notion of local optimality — checking only the neighbors obtained by independently nudging each coordinate by , , or (excluding the trivial no-change case) — is a genuinely discrete, dimension-independent statement about functions whose domain can be arbitrarily large. Almost every discrete convex function class studied later in the book, including M-convex and L-convex functions, is a special case of integral convexity, and this mission's goal theorem is the direct ancestor of the optimality criteria (Theorems 6.26 and 7.14) that drive the algorithms in the rest of the book.
Let be a function with nonempty effective domain . The convex closure of is
the pointwise supremum of every affine function minorizing on all of . If agrees with on integer points, is convex extensible. The integral neighborhood of is
and the local convex extension relaxes 's definition by requiring the affine minorant condition only on rather than on all of . Always pointwise, and the two agree on . A function is integrally convex if everywhere on — equivalently, if is a convex function on all of (it is automatically convex on every unit cube with , but need not be convex globally without this extra condition).
A discrete set is hole free if equals the set of integer points in its own real convex hull, and denotes the minimizer set, over , of the linearly perturbed function .
For integrally convex and :
where is the indicator vector of . The right-hand side is a check over at most points (each coordinate independently unchanged, incremented, or decremented), regardless of how large is; this uniform, dimension-only bound is the entire content of the theorem, and is the weakest correct formulation — restricting to a single or letting the right-hand side range over all of would trivialize or falsify the equivalence.
Proposition 3.18: convex extensible hole free for every (and conversely, when is bounded). Proposition 3.19: is integrally convex if and only if every restriction to a finite integer interval is integrally convex — integral convexity is detectable by looking at bounded pieces of one at a time.
The result itself. Theorem 3.21 is what makes integrally convex functions tractable: without it, verifying global optimality on an infinite or exponentially large integer domain would require checking every point. The theorem reduces this to a check whose size depends only on the dimension , not on the size of the domain, and it does so for the widest class of lattice functions for which such a reduction is possible — the class is defined precisely so that this property holds and no wider natural class enjoys it. Every specialized local-optimality theorem later in the book (for M-convex, M-convex, L-convex, and L-convex functions) restricts this same neighborhood-checking principle to a class where the local check can be made even smaller (a single-element exchange rather than a full sign pattern) precisely because those classes are integrally convex plus more.
Formalizing it. No matching item exists on the platform: a direct search for "integrally convex" returns no results, and the theorem's own proof leans on results (Theorem 1.1's local-to-global principle for ordinary convex functions on , and an LP-duality-based alternate formula for ) that are either classical convex analysis or belong to a different chapter of this same book. The remaining work is therefore to give a complete, correct account of the definitional chain — convex closure, local convex extension, integral convexity — in a form a solver can build a proof from directly, and to state the finite local-check equivalence itself exactly at the strength the book proves it, not a plausible-looking weakening of it.
The natural first attempt is to try to prove the "" direction of Theorem 3.21 by a direct induction on the -distance to a global minimizer, moving one coordinate at a time. This fails in general lattice functions (a function that is only "coordinatewise convex" can have strict local minima that are not global), and the theorem's actual proof instead routes through the real relaxation: it shows the neighborhood-check hypothesis forces to be a local minimizer of the local convex extension restricted to the unit ball around , then invokes ordinary convex analysis (local minimality implies global minimality for a convex function on ) to conclude globally minimizes , and finally uses integral convexity () to transfer this back to on . The identification of 's local behavior with 's convexity on a single unit cube — rather than any coordinatewise or separable argument — is the step that makes the class of integrally convex functions exactly the right one for this theorem, and is where a naive combinatorial argument breaks down.
The ground set is , represented as Fin n → ℤ; 's codomain is WithTop ℝ
(exactly ), while the convex closure and local convex
extension take values in EReal (exactly , a complete
lattice, so their defining suprema are total functions with no side conditions). A trivializing
formalization of the goal would quantify the right-hand side over a single fixed pair,
or over all of instead of the sign-pattern neighbors; both are excluded by keeping
universally quantified Finset (Fin n) ranging over the full sign-pattern space
(minus the trivial case, which the equivalence still holds through vacuously).
Checked against the platform (GET /theorems?q=integrally convex, 0 hits) and against Mathlib's
Analysis/Convex/ for the classical facts this chapter's proof would eventually need (ordinary
convex-function local-to-global optimality, LP duality): these are broadly available in
Mathlib's convex-analysis library in some form, but none of them is imported here, since none
appears in the statement of any item this mission drafts — they belong to a proof this pass
does not attempt. Contributions to a shared DiscreteConvex.IntegralConvexity definitions layer
are welcome from chunks 06–09, which specialize integral convexity to M-convex and L-convex
functions and will need the same convex-closure/local-extension vocabulary.
A multiple objective program asks to maximize objectives simultaneously over a feasible set . There is usually no point that is best in every objective, so the object of interest is the set of nondominated criterion vectors: those that cannot be improved in one objective without being worsened in another. Interactive procedures for multiple criteria decision making work by computing nondominated vectors one at a time, by solving a single-objective scalarization, and presenting them to a decision maker.
A scalarization is useful for this purpose only if it is complete (every nondominated vector is the solution of some instance of it) and sound (every solution is nondominated). The weighted-sum scalarization is sound for positive weights but not complete when the feasible region is nonconvex. R. E. Steuer and E.-U. Choo (Math. Programming 26 (1983) 326–344) built their interactive procedure on weighted Tchebycheff distances to an ideal point, following Bowman (1976) and Choo and Atkins (1983). In §3 they treat finite feasible regions with an augmented metric, which requires choosing a small parameter . In §4 (pp. 334–336) they show that a lexicographic version of the weighted Tchebycheff program is complete and sound for any feasible region, including nonconvex continuous ones, with no parameter to estimate. This mission formalizes that result, Theorems 4.5 and 4.6.
Let , , be the set of feasible criterion vectors (the image of under ). A vector dominates if for all and for at least one . The nondominated set consists of the dominated by no .
An ideal criterion vector is a with
where , and is required whenever (i) more than one nondominated vector maximizes objective , or (ii) the only nondominated vector maximizing objective also maximizes another objective. So may touch in coordinate only in a controlled way.
The weight set is the simplex . For the weighted Tchebycheff program minimizes subject to for all and ; its value at a fixed is
The lexicographic weighted Tchebycheff program first minimizes over and then, among the first-stage minimizers, minimizes . The paper writes it as with pre-emptive priority factors. Finally, for the weights of eq. (4.3) are , normalized to sum to one, when for all . When some , is on the coordinates with and elsewhere.
For compact , an ideal vector and ,
The goal is the characterization; Theorem 4.5 is the stronger half with uniqueness and an explicit weight.
Theorem 4.6 says that, as ranges over the simplex, the lexicographic weighted Tchebycheff program returns exactly the nondominated set, for any feasible region: no convexity, no finiteness, no polyhedral structure. Theorem 4.5 adds that each nondominated vector is the unique output for a weight vector computable from the vector itself, which is what an interactive procedure needs to sample reliably. The price, as the paper notes, is two optimization stages instead of one; the gain is that no augmentation parameter must be estimated. The result is a standard entry in the textbook treatment of Tchebycheff scalarizations (Steuer, Multiple Criteria Optimization, 1986; Ehrgott, Multicriteria Optimization, 2005).
The result is proved on paper. To our knowledge no machine-checked version exists in Lean or Mathlib, which has no material on Tchebycheff scalarization of multiple objective programs. The formal statements below also pin down two points the printed text leaves loose: the direction of the priority factors, and a closedness assumption that the proof uses without stating it.
The ⇐ direction and the soundness remark are short: a dominating vector is at least as good in the first stage and strictly better in the second. The work is in Theorem 4.5. The obvious argument is that is the unique minimizer of the first stage with weights ; the paper says so. That is true when in every coordinate, but false when for some : then , and every with ties with , dominated vectors included. For example, with and , the vectors and tie. Only the second stage separates them. Showing that it always selects requires every tied vector to lie below a nondominated vector attaining , which by the ideal-vector rule must be . That existence step fails for sets that are not closed.
Criterion vectors are Fin k → ℝ with [NeZero k] (); objectives are indexed from . , the objectives and the program's variable are eliminated: is a Set (Fin k → ℝ) and the first-stage value is above (the paper's metric uses , which agrees with on ). is Mathlib's stdSimplex ℝ (Fin k). "Minimizes" is global minimization over ; "uniquely minimizes" means every lexicographic minimizer equals as a criterion vector.
Conventions and added hypotheses:
IsLexMin. The printed "" read literally gives the second stage priority; the paper's text on p. 336 and the goal-programming convention it cites give priority. The two-stage reading is encoded, and the program is not replaced by a weighted sum with fixed numbers, which would be the augmented program of §3.Infrastructure needed: dominance and nondominated sets, the ideal vector, the weighted Tchebycheff value, the weights (4.3), and the lexicographic minimizer, all provided as definitions. Proofs will need existence of minimizers of continuous functions on compact sets and a maximal-element argument in the product order on a compact set. Both are reusable for other multiobjective results. Proofs of any item, and faithful statements of Corollaries 4.1 and 4.4 (polyhedral ), are welcome.
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.
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.