Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 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?
A binary error-correcting code is a set of -bit words chosen so that the words stay distinguishable after a few bits have been corrupted in transmission. A code can correct any errors exactly when every two of its words differ in at least positions. The more words the code has, the more information each transmitted block carries. So the central quantitative question of coding theory is how large a code of given length and minimum distance can be. Codes are used in every technology that transmits or stores data, from disks and phones to deep-space probes.
In 1973 Philippe Delsarte showed that an upper bound on this maximum size is the optimum value of an explicit linear program (Delsarte, An algebraic approach to the association schemes of coding theory, Philips Res. Repts. Suppl. 10, 1973). The bound was far stronger than the classical volume argument and remains a standard tool. This mission formalizes the self-contained proof of the bound in §8.4 of Matoušek and Gärtner's textbook (Springer 2007). That proof follows Best, Brouwer, MacWilliams, Odlyzko and Sloane (IEEE Trans. Inform. Theory 24, 1978). The mission also covers the step of Delsarte's original argument that the book isolates as a lemma.
Timeline.
A word is , and a code is any set . The Hamming distance is the number of positions with . The weight is the number of ones in . The word is the entrywise sum modulo 2. For , the restricted distance counts only the differing positions that lie in .
A code has distance if for all distinct (Definition 8.4.1). The quantity is the maximum of over all codes with distance .
For the Krawtchouk numbers are
The distance distribution of a code is
The Delsarte linear program has variables . It maximizes subject to:
For Delsarte's original argument, is the matrix whose entry is when and otherwise. The weights are .
The goal is stated against every upper bound of the objective on the feasible set. No particular optimum value is fixed, so the statement covers every and at once.
The Delsarte bound turns an extremal problem over the subsets of the cube into a linear program with variables. For it gives , while the sphere-packing bound gives . Many entries of the standard code tables rest on this bound or its refinements. The positive semidefiniteness in Lemma 8.4.7 is the starting point of the semidefinite programming bounds of Schrijver and of later work. The same framework also underlies the linear programming bounds for spherical codes and sphere packings.
The theorem is classical and fully proved in the literature. Neither Mathlib nor this platform has a formal statement or proof of it. Mathlib has Hamming distance and binomial coefficients, but it has no , no Krawtchouk numbers and no LP bound for codes. This mission would produce the first formal statement and proof. It would also produce reusable identities on Krawtchouk sums and character sums over .
Two of the program's constraints are immediate once is defined: , and for . The difficulty lies in the Krawtchouk constraints. They do not follow from counting pairs at a single distance. They require a sign-weighted count over all words of weight , and the sum must then be regrouped by the distance of each pair. That regrouping identifies a count of words, split by how many ones they share with a fixed word, with the Krawtchouk number. Formally this is an exchange of finite sums together with a binomial counting identity, and the index bookkeeping, including the range , has to be exact.
The obvious attempt proves the inequality one distance class at a time. It fails because the individual terms have no sign. Only the whole sum is nonnegative.
Fin n → Bool, with bit as true. The book's positions become 0, …, n-1. Codes are Finsets of words, and is Mathlib's hammingDist.Finset.sup over the finite family of codes with distance . This family contains the empty code, so the maximum is attained.Fin (n+1) with no index shift. The constraints are imposed for , so they are vacuous for .Matrix.PosSemidef over .No trivialization. The goal is not stated as "" with a real supremum, which Lean would evaluate to on an empty or unbounded set. Its hypothesis ranges over upper bounds of a feasible program: is always feasible, so the hypothesis is never vacuous.
Contributions welcome. Useful lemmas include:
These are reusable for other LP and SDP bounds in coding theory.
A two-player zero-sum game models any situation in which one party's gain is exactly the other party's loss: a military allocation in the spirit of Colonel Blotto, a sealed-bid contest, rock–paper–scissors. The central question is what each player should do when the opponent is also reasoning about them. John von Neumann answered it in 1928 with the minimax theorem (von Neumann 1928): each player has a strategy guaranteeing the same number, the value of the game, whatever the opponent does. The theorem underlies modern game theory, robust decision making, and the analysis of online learning algorithms, where regret bounds are routinely derived from it.
Section 8.1 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007) presents the theorem as an application of linear programming duality. This mission is the sixth of a series formalizing the capstone results of the book.
Alice has pure strategies and Bob has . A real payoff matrix records Alice's gain, and Bob's loss, when Alice plays her th and Bob his th pure strategy. A mixed strategy of Alice is a probability vector , , ; a mixed strategy of Bob is a probability vector . When the players randomize independently, Alice's expected payoff is
The worst-case payoffs are
over mixed strategies. A mixed strategy of Bob is a best response against if it minimizes ; a mixed strategy of Alice is a best response against if it maximizes it. A pair is a mixed Nash equilibrium (Definition 8.1.1) if each is a best response against the other. Alice's is worst-case optimal if ; Bob's is worst-case optimal if .
The proof in the book passes through three linear programs: the dual of (8.1), which for a fixed maximizes subject to ; program (8.2), the same with as variables subject to , ; and program (8.4), which minimizes subject to , , .
For every payoff matrix with : worst-case optimal mixed strategies exist for both players; for any worst-case optimal of Alice and of Bob, the pair is a mixed Nash equilibrium; and there is a single number , the value of the game, with
for every such pair. The third clause is what distinguishes the theorem from the existence of some saddle point.
The theorem gives a complete prescription for zero-sum play: a worst-case optimal strategy secures at least the value against any opponent, and a worst-case optimal opponent holds the player to at most the value, so both players can announce their strategies in advance without loss. With Lemma 8.1.2(ii) it yields a characterization: a pair of mixed strategies is a Nash equilibrium if and only if both are worst-case optimal. The minimax equality is used downstream in online learning (regret-to-value arguments), in robust optimization, and in Yao's principle for randomized algorithms.
The mathematics is classical and proved; what this mission adds is a machine-checked version in the book's own formulation. The platform already has AGT.zero_sum_minimax (Algorithmic Game Theory I), which proves the existence of a saddle point, and the general FamousTheorems.sion_minimax_theorem. Neither states that every pair of worst-case optimal strategies is an equilibrium with a common value, and neither exhibits the LP route: the dual of (8.1), the programs (8.2) and (8.4), and their duality. The mission records that route statement by statement, so that it can be reused as a worked instance of LP duality.
Lemma 8.1.2 is routine; the entire content is the reverse inequality . The obvious attack, maximizing directly, fails because is a minimum of linear functions and hence not linear, so its maximization is not a linear program as written. The obstacle is removed only by an appeal to LP duality in the proof, together with the facts that the simplices are nonempty and compact, and that the relevant programs are feasible and bounded so that optima exist. None of this is supplied by the pure-strategy structure of the game: pure Nash equilibria need not exist (rock–paper–scissors has none).
Pure strategies are indexed by Fin m and Fin n, with the book's standing assumption carried as hypotheses 1 ≤ m, 1 ≤ n by every theorem; the book's indices become . Mixed strategies are Mathlib's stdSimplex ℝ (Fin m), the payoff is x ⬝ᵥ (M *ᵥ y). is the real sInf and the real sSup of the payoffs over the opponent's simplex; milestone 1 states that these are attained. A mixed Nash equilibrium is defined in the verbal form of Definition 8.1.1 (mutual best responses). Worst-case optimality is defined against all mixed strategies, never as a saddle-point condition, so the goal is not circular with Lemma 8.1.2(iii). LP optimality is stated as "feasible and at least as good as every feasible point", so no supremum over a possibly empty or unbounded feasible set is used.
The book's clause that worst-case optimal strategies "can be efficiently computed by linear programming" is algorithmic and is not part of the formal statement; there is no complexity model. A goal asserting only the existence of worst-case optimal strategies, or only the existence of some equilibrium, would drop the theorem's third clause and is ruled out: the common value is quantified before all pairs of worst-case optimal strategies.
A complete development needs compactness of the standard simplex, continuity of the bilinear payoff, and a strong duality theorem for linear programs in the form of the programs (8.2)/(8.4); the latter is reusable across the whole series. Proofs by other routes (Sion's theorem, a separating hyperplane argument, fixed points) are welcome for the goal; the LP milestones stand on their own as statements about the programs.
Every finite algorithm for linear programming rests on one structural fact: if a linear program has an optimum at all, it has one at a point singled out by finitely many linear conditions. The simplex method walks between such points, and exact complexity analyses, sensitivity analysis and integrality arguments all start from them. Chapter 4 of J. Matoušek and B. Gärtner, Understanding and Using Linear Programming (Springer, 2007, DOI 10.1007/978-3-540-30717-4), establishes this fact for linear programs in equational form, in the definitions that the rest of the book (the simplex method of Chapter 5, duality in Chapter 6, the applications in Chapter 8) uses.
This mission is the second of a series formalizing that book. It fixes the book's notion of a basic feasible solution and of a vertex, and targets the theorem that optimal solutions exist whenever the program is feasible and bounded, and can then be chosen basic.
A linear program in equational form is
where is a real matrix, , , and means every coordinate of is nonnegative. A feasible solution is an satisfying both constraints; the set of them is . An optimal solution is a feasible with for every feasible . The objective is bounded from above if some real satisfies for all feasible .
Throughout Section 4.2 the book assumes that has columns and rank (its rows are linearly independent). For , denotes the matrix formed by the columns of with indices in . A basis is an -element set for which is nonsingular, i.e. its columns are linearly independent. A basic feasible solution is a feasible for which some basis has for every .
A point is a vertex of if and some nonzero satisfies for every : is the unique maximizer over of a nonzero linear function.
For of rank with ,
Both parts are one theorem, as in the book. Part (i) says optimal solutions fail to exist only for the two obvious reasons, infeasibility and unboundedness; part (ii) says an optimum can always be found among basic feasible solutions.
Theorem 4.2.3 gives a finite, if impractical, algorithm for linear programming: enumerate the at most sets , solve , and keep the best nonnegative solution. It is the correctness backbone of the simplex method, which visits basic feasible solutions in a smarter order, and it is the source of the book's claim that a feasible and bounded linear program has an optimal solution. Theorem 4.4.1 identifies this algebraic notion with the geometric corners of the feasible polyhedron, which is what makes statements such as "the LP relaxation has an integral vertex" in later chapters meaningful.
All of these results are classical and fully proved in the book. The value of formalizing them here is the definition layer: later missions of this series (Bland's rule, the central path, the scheduling application) state their results about bases and basic feasible solutions in exactly these definitions, and a proved Theorem 4.2.3 in this form lets them import the existence of an optimal basic solution instead of re-deriving it. Related facts are already machine-checked on Prove2Me in the formulation of Bertsimas and Tsitsiklis (Introduction to Linear Optimization I and II: minimization over polyhedra , extreme points, basic solutions as active linearly independent constraints). Those statements concern a different presentation of the program and a different notion of basic solution; connecting them to the equational-form statements here is itself a welcome contribution.
The obvious argument for part (i), "a continuous function on a closed set bounded above attains its supremum", fails: the feasible set is usually unbounded, and a linear function bounded above on an unbounded closed convex set need not obviously attain its supremum without using the polyhedral structure. The existence of an optimum is exactly the nontrivial content of part (i); compactness is not available.
For milestone 1, the delicate direction is the converse: a set of linearly independent columns indexed by must be completed to an -element basis, which requires the rank- assumption. For Theorem 4.4.1, the direction from vertex to basic feasible solution is not local: a vertex is defined by an optimization property, while basicness is a statement about the support of the point.
All items live in the namespace MatousekLP.BFS and share one definition module, MatousekLP.BFS.EquationalForm. Conventions:
Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the book's indices are 0, …, n-1;A *ᵥ x = b, is 0 ≤ x (pointwise), is c ⬝ᵥ x;Finset (Fin n); " nonsingular" is linear independence over of the family of columns of indexed by the elements of , together with B.card = m;m ≤ n and A.rank = m on every theorem;Set.extremePoints; the book's remark on p. 55 that the two coincide is not used as a definition;A formalization in which "optimal" were defined through sSup of the objective over the feasible set would make part (ii) trivially true or false on unbounded programs; the definitions here rule that out. Dropping the rank hypothesis would make part (ii) false (no basis exists when the rows are dependent), so it is not optional.
Reusable infrastructure: the column-restriction and basis vocabulary, the support set , and the extension of a linearly independent set of columns to a basis of the column space are needed again in the simplex chapter. Proofs of any milestone, and bridges to Mathlib's Set.extremePoints or to the Bertsimas–Tsitsiklis statements on the platform, are welcome.
Almost every screening, auction and regulation model asks the same preliminary question: which allocation rules can be made incentive-compatible by some choice of payments? In the one-dimensional models of auction theory and nonlinear pricing the answer is monotonicity: higher types must receive higher allocations. Many applications are not one-dimensional, though. Examples are multi-object auctions, multi-product pricing, and lotteries over several outcomes. For those, a characterization that uses no structure at all is needed. Rochet (1987) gave one: an allocation rule is implementable exactly when it is cyclically monotone, a condition that originates in Rockafellar's characterization of subdifferentials of convex functions. Later work on dominant-strategy implementation, the "weak monotonicity" literature of algorithmic mechanism design, and revenue equivalence all build on it.
This mission formalizes Chapter 5 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): all nine numbered results of the chapter.
Timeline. Rockafellar (1970, Theorem 24.8) characterized the cyclically monotone maps between vector spaces as the subgradient selections of convex functions. Rochet (1987) extended the idea to arbitrary alternatives and types with quasi-linear utility and proved that implementability is exactly cyclical monotonicity. Krishna and Maenner (2001) proved revenue equivalence on convex type spaces with utilities convex in the type. Bikhchandani, Chatterji, Lavi, Mu'alem, Nisan and Sen (2006) showed that for finitely many alternatives, weak monotonicity (the two-type case of cyclical monotonicity) already suffices on rich, order-based domains. Saks and Yu (2005) proved the same on convex domains.
A designer and one agent choose an alternative from a set . The agent has a type in a nonempty set . With utility function , her payoff from when she pays is . Neither nor carries any structure.
A direct mechanism is a decision rule and a transfer rule . It is incentive-compatible if for all . A decision rule is implementable if some makes it incentive-compatible. It is weakly monotone if for all pairs of types. It is cyclically monotone if for every finite sequence of types with ,
A complete and transitive order of induces a partial order on types: if values every -higher alternative strictly more, relative to an -lower one, than does, and neither type distinguishes -indifferent alternatives. The type set is one-dimensional if any two distinct types are -comparable, and bounded if all utility differences lie in for some . It is rich if, for some reflexive and transitive relation , every function with is some type's utility function. A mechanism is individually rational with outside option if every type does at least as well as with and no payment.
for arbitrary , nonempty and .
Rochet's theorem turns the existence of payments, an infinite system of linear inequalities in unknowns , into a condition on the decision rule alone. It underlies the characterization of implementable rules in multidimensional screening, the taxation principle, and the dominant-strategy characterizations of Chapter 7 (applied agent by agent). Propositions 5.4–5.6 recover the "monotone allocation" results of the one-dimensional chapters from it. Proposition 5.8 is the general form of the payoff-equivalence lemmas used for optimal auctions.
All results are classical and proved on paper, except Propositions 5.7 and 5.8, whose proofs the book omits and refers to the literature. None of them is formalized on Prove2Me. The platform's algorithmic-game-theory series has the weak-monotonicity half in a multi-agent valuation model (types are valuations ), not the abstract-type statement, and has no cyclical-monotonicity or Rochet result.
Necessity is a two-line telescoping argument. Sufficiency needs a transfer rule built from the decision rule, and the first idea fails: prices attached to alternatives chosen pair by pair (which weak monotonicity supplies) need not be globally consistent. Figure 5.1 of the book gives a three-type example that is weakly monotone but not implementable. The transfer must come from a supremum over all finite chains of types starting at a fixed type. The supremum is finite only because of cyclical monotonicity, and no finiteness, compactness or boundedness is available. Proposition 5.8 needs an envelope argument along segments in without differentiability. Proposition 5.7 needs a combinatorial argument that uses richness of the domain.
Alternatives and types are arbitrary Lean types A, Θ with Nonempty Θ, and the utility is u : A → Θ → ℝ. A cycle of length is a map Fin (m+1) → Θ with equal first and last entries, and its summands are indexed by Fin m. Relations are predicates A → A → Prop. For Propositions 5.3 and 5.8, types form a subset S of Ω → ℝ (resp. Fin n → ℝ) used as a subtype. Lotteries are stdSimplex ℝ Ω, and the subgradient inequality is required only at points of S.
The explicit statements are fixed as follows:
Two statements are corrected from the page, each with a counterexample to the literal version recorded in its item:
Both directions of Rochet's theorem are required. The necessity half alone, or a version with finite , finite or bounded utilities, is a different and much weaker theorem and does not close the goal.
The development needs finite telescoping sums, suprema of sets of reals (sSup with an explicit bounded-above argument), convex functions on sets and one-dimensional convex analysis (Proposition 5.8). The definitions file is reusable for Chapters 6–8 of the series. Contributions of alternative proofs, for example Proposition 5.6 through Rochet's theorem, are welcome.
Assumptions of Physics by Gabriele Carcassi and Christine A. Aidala (book, v3.0, 2025) is a programme to derive the mathematical structures of physical theories from explicit physical requirements. Part II, "Physical Mathematics", begins (Chapter 1) by making precise what it means for a statement to be experimentally verifiable, and shows that a single physical requirement (only countably many tests can be run in an indefinite amount of time) is enough to force the familiar structures of point-set topology onto the space of outcomes of any experiment. This mission formalizes that chapter. It is the first mission of a series on the book; all declarations live in the namespace AssumptionsOfPhysics so that later missions can build on them.
A logical context is represented by its set of possible truth assignments, and a statement (up to logical equivalence) by its truth set . Negation, conjunction and disjunction are complement, intersection and union; the certainty is and the impossibility is ; " is narrower than " means , and are compatible when .
An experimental domain is a family of statements that contains and , is closed under finite conjunction and countable disjunction, and has a countable basis : every element of is obtained from by finite conjunctions and countable disjunctions. Its theoretical domain is the closure of under negation, finite conjunction and countable disjunction. A possibility is a non-impossible that, for every , is either narrower than or incompatible with it; denotes the set of possibilities. The verifiable set of a statement is , and the natural topology on is the topology generated by . A domain is decidable if it is closed under negation.
The chapter's results identify the open sets of a topology with verifiable statements and its points with complete experimental answers (possibilities). Second countability and the axiom are thereby derived rather than assumed, and the cardinality bound limits which mathematical objects can carry experimental meaning. Later chapters of the book (domain combination, properties and quantities, ensemble spaces) rely on these facts. The results are proved informally in the book; no machine-checked formalization of them is known to the drafters. A formalization fixes the precise hypotheses under which they hold (for instance, whether a basis must be countable in Propositions 1.46, 1.48 and 1.60) and provides a reusable library for the rest of the series.
The individual statements are elementary, but several of the book's proofs are informal about two points that a formal proof must handle. First, the possibilities must be shown to cover the space of assignments and to be atoms of ; the book argues through minterms of a countable basis, which needs a "disjunctive normal form" for countably generated families. Second, the natural topology is defined via arbitrary unions while experimental domains are only closed under countable disjunction; showing that every open set is still of the form (Proposition 1.57) requires a second-countability / Lindelöf-type argument rather than direct closure.
Statements are subsets s : Set Ω of an arbitrary type Ω (possibly empty); the experimental domain is the structure ExperimentalDomain Ω, whose field stmts is the family . Generation by finite conjunction and countable disjunction (FinConjCountDisj) includes the empty conjunction and the empty disjunction ; generation with negation (NegFinConjCountDisj) includes . Possibilities form the type D.Possibility, which carries the natural topology as an instance; topological notions (SecondCountableTopology, T0Space, T1Space, DiscreteTopology) are Mathlib's. The primitive notion of verifiability (Axiom 1.27) is not modelled separately: membership in is what all results of the chapter use. Statements involving "a basis" quantify over every basis (countable or not), as in the source. Contributions of reusable lemmas, in particular a disjunctive-normal-form lemma for countably generated families of sets, are welcome.
This is the fourth mission of the series on Assumptions of Physics by G. Carcassi and C. A. Aidala (book, v3.0, 2025), formalizing the axiomatic core of Part II, Chapter 4, "Ensemble spaces". The chapter proposes three physically motivated axioms (ensemble, mixture, entropy) that every space of statistical states should satisfy, covering classical probability distributions and quantum density operators alike, and derives from them structure that is usually postulated, for example that mixtures can be "un-mixed" (cancellativity). That is the first step towards embedding ensembles in a vector space. Unlike missions II and III, this mission does not depend on earlier missions.
An ensemble space is a , second countable topological space with a continuous mixing operation (, ) that is idempotent, commutative and associative, and a continuous entropy . The entropy is strictly concave, with equality iff , and bounded above by for a universal function . Two ensembles are orthogonal, , when this bound is saturated, and mixtures preserve orthogonality. An ensemble is a component of if with ; two ensembles are separate if they have no common component. The mixing entropy is .
Cancellativity is what allows affine combinations with negative coefficients, the origin, in this framework, of the vector-space embedding of ensembles (Theorem 4.94) and of negative quasi-probabilities such as Wigner functions. It holds in classical and quantum statistics, and here it is derived from continuity and strict concavity of the entropy instead of being postulated. The results are proved informally in the book; no machine-checked formalization is known to the drafters.
The convex-space axioms are stated in a two-sided associativity form, so every rearrangement of mixtures must be derived from it. The book's proof of cancellativity first propagates the equality from one coefficient to all of by an iteration , and then uses a limit together with continuity of mixing and of the entropy. Strict concavity has to be applied only to non-trivial coefficients.
The structure EnsembleSpace I E bundles Axioms 4.4, 4.7 and 4.55 for a topological space E; mixing coefficients are elements of Mathlib's unitInterval. Real coefficient expressions in the associativity axiom pass through clampI, the projection , and lie in on the stated domain. The universal function is a parameter. Orthogonality is saturation of the upper bound for every . Strict concavity is required for only, since at equality is automatic. The book's Proposition 4.67 uses for , which follows from universality of (any space with two distinct ensembles forces it); the milestone carries this as an explicit hypothesis. Items 3 and 4 of Proposition 4.116 in the book use the normalization from Theorem 4.59; item 3 is stated with and item 4 is omitted. Hull operators, the vector-space embedding (Theorem 4.94), boundedness of lines (Theorem 4.105), the entropic geometry and the standard classical/quantum models (Propositions 4.5, 4.9, 4.56) are left for later missions.
Minimum-cost network flow problems are the largest special class of linear programs met in practice: transportation, distribution, assignment, communication and electric networks, facility location and financial planning all reduce to moving material along the arcs of a directed network from supply nodes to demand nodes at least cost. Chapter 14 of R. J. Vanderbei's Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) develops the network simplex method, and closes with two structural facts that explain why this class is special: simplex bases are spanning trees of the network, and a network problem with integer supplies has integer basic solutions. Vanderbei then uses integrality to prove a classical theorem of combinatorics, König's theorem on regular bipartite graphs. Chapter 15, §5 treats the maximum-flow problem on the same objects and proves the Max-Flow Min-Cut Theorem.
The combinatorial results are older than linear programming. D. König proved in 1916 that every regular bipartite graph has a perfect matching (Math. Ann. 77). The Max-Flow Min-Cut Theorem is due to Ford and Fulkerson (1956, Canad. J. Math. 8) and, independently, Elias, Feinstein and Shannon (1956). The integrality of network bases is the total unimodularity of incidence matrices, known since the 1950s (Hoffman and Kruskal, 1956).
A network has a finite set of nodes and a set of directed arcs . Node carries a supply (negative values are demands) with , and arc carries a cost . The flow on arc is the decision variable. The node–arc incidence matrix has in the column of an entry in row , in row , and elsewhere. The network flow problem (14.1) is
A flow satisfying is balanced; a balanced flow with is feasible. Paths ignore arc directions; the network is connected if every two nodes are joined by a path, which is assumed throughout Chapter 14. A spanning tree is a set of arcs that, on all of and without directions, is connected and has no cycle. Fixing a root node and deleting its row gives the matrix . A set of arcs is a basis if its columns form an invertible square submatrix of , and a basic feasible solution is a feasible flow vanishing off some basis.
For maximum flow, a source , a sink and finite upper bounds are given; all and an extra arc of infinite capacity is added. A feasible flow satisfies , and flow balance. A cut is a node set with , , and its capacity is .
If girls and boys are such that every girl knows exactly boys and every boy knows exactly girls (knowing being symmetric), then there is a bijection from girls to boys with
both extrema attained.
The goal is independent of the network definitions in its statement; the milestones are the book's route to it (14.1, 14.2) and the chapter's other duality theorem on the same objects (15.8, 15.1).
König's theorem is the base case of matching theory: it gives perfect matchings in regular bipartite graphs, hence edge colourings of bipartite graphs with colours, and via Birkhoff–von Neumann-type arguments the decomposition of doubly stochastic matrices. The Integrality Theorem is the reason assignment, transportation and shortest-path problems can be solved as linear programs without an integrality constraint. Theorem 14.1 is the correspondence the network simplex method is built on. Max-Flow Min-Cut is the prototype of combinatorial min–max theorems.
All four theorems are classical and proved. This mission adds machine-checked versions in the book's own formulation: the incidence matrix with Vanderbei's sign convention , bases as square submatrices of with a chosen root, and maximum flow as a circulation through an added return arc. The platform already has network integrality, a tree-solution characterisation and max-flow min-cut in the Bertsimas–Tsitsiklis formulation and a Keller–Trotter max-flow statement; none is stated in this form, and Mathlib has Hall's marriage theorem but no regular-bipartite corollary.
The combinatorial content is small; the difficulty is in the passage between matrices and graphs. Theorem 14.1 needs both directions: the book shows that a spanning tree gives a triangularisable, hence invertible, submatrix and leaves the converse (independent columns form a spanning tree) as an exercise, which requires showing that any cycle, including a pair of antiparallel arcs, yields a linearly dependent set of columns and that acyclic arcs span. The book's proof of König's theorem applies the Integrality Theorem to the girl–boy network, which need not be connected, while Chapter 14 assumes connectedness throughout: the statement of 14.2 does not apply to it verbatim. The step "a feasible problem has a basic optimal solution" is also used and is not stated in the chapter.
Fintype with decidable equality; arcs are a Finset (N × N), so parallel arcs are excluded as in the book, and IsNetwork excludes loops. Flows are real functions on ordered pairs; only their values on arcs matter.Fin n, knowing is one relation between girls and boys, and is a hypothesis: the book's proof divides by , and for the claim is false. No connectedness is assumed.A formalization of the goal as a matching of size in some larger graph, or with the degree conditions on one side only, would be a different theorem; the conclusion is a bijection between exactly the girls and the boys using only acquainted pairs.
Useful infrastructure, reusable beyond this mission: the incidence matrix and its total unimodularity, the undirected graph of an arc set. Proofs of König's theorem through Hall's theorem (Mathlib Finset.all_card_le_biUnion_card_iff_exists_injective) are welcome alongside the book's route.
Chapter IX of von Neumann and Morgenstern's Theory of Games and Economic Behavior asks when a game played by many participants is really several separate games played side by side. The authors' motivation (41.1) is methodological: the general theory of the -person game becomes unmanageable as grows, and one way to gain insight into large games is to isolate classes of games that can be analysed exactly. The first such class consists of games whose players fall into groups that have no dealings with each other — the book's example is the internal economies of two countries whose connections are disregarded (41.2.4). Such a game is the composition of its constituents, and the question of the chapter is how to recognise a composite game from its characteristic function alone and how far a given game can be decomposed.
The answer (§43) is a structure theorem. The groups of players that can be split off form a Boolean algebra of sets; its atoms, the minimal splitting sets, form a partition of the set of players, the decomposition partition ; and every splitting set is a union of blocks of . The book remarks (41.3.3) that the splitting condition (41:7) is exactly Carathéodory's criterion of measurability, transported from measures to characteristic functions. The mission formalizes §43, together with the criterion (42:G) of §42 on which it rests.
Let be a finite set of players. A characteristic function is a real number for every subset (every coalition, including the empty set and ). Write . From 42.4.1 on the book works in the domain of constant-sum games, whose characteristic functions are, by (42:D), exactly the functions satisfying
For with complement , the game is decomposable with respect to and if there are constant-sum games on the players and on the players with for all — formula (41:3). The -constituent is the game on with for (41:4).
A splitting set (43.1) is a satisfying (41:6),
The game is indecomposable if and are its only splitting sets (43.3.1). A minimal splitting set is a splitting set none of whose proper subsets is splitting (43.3.2), and is the system of all minimal splitting sets. The game is inessential (42:F) if it is strategically equivalent to the zero game, i.e. for all , for some reals (the transformation (42:5)).
For every satisfying (42:6:a)–(42:6:c):
The goal combines the partition property and the characterization of all splitting sets; it is the book's own summary of §43.3 and does not presuppose that is a partition.
In attack order: the criterion (42:G) (decomposability (41:6) (41:7)); the closure properties (43:A) (complements), (43:B) (, ), (43:C) (intersections and unions); (43:D) (splitting sets of a constituent) and (43:E) (a constituent is indecomposable iff its set is minimal); (43:F), (43:G) separately; (43:I) (a minimal splitting set is disjoint from, or inside, any splitting set); the restatement (43:H*) ( splits iff every block of lies inside or outside ); and the two extreme cases (43:J) ( = all singletons iff the game is inessential) and (43:K) ( iff the game is indecomposable).
The decomposition partition is canonical: every constant-sum game splits uniquely into indecomposable constituents, and (43:E) identifies them as the constituents on the blocks of . The two extreme cases (43:J), (43:K) show that inessentiality and indecomposability are opposite ends of one scale. Chapter IX uses this structure in §§44–47, where solutions of decomposable games are related to solutions of their constituents ((46:A)–(46:I)); a formal decomposition partition is the prerequisite for that later work, and a candidate follow-up mission.
The results are classical and proved in the book. The mission's contribution is a machine-checked version: a formal definition layer for splitting sets of a set function on a finite set, the Boolean-algebra closure, and the atomic decomposition. The combinatorial core — that the sets satisfying a Carathéodory-type additivity condition form a Boolean algebra of a finite set, whose atoms partition it — is reusable outside game theory (for instance for finitely additive decompositions of set functions). No machine-checked version of these results is known to exist; they are formalized here for the first time as far as a search of the platform shows.
The individual steps are elementary, but the obvious argument for the key closure property (43:C) fails: to show that is splitting one cannot simply add the identities (41:6) for and for , since a pair , is not of the form those identities control, and may be nonempty — the book's footnote on p. 354 singles out overlapping splitting sets as the case its proof is really about. Likewise (43:D) is not a tautology: that a set self-contained within a self-contained set is self-contained in the whole game has to be proved (footnote 1, p. 355). Formally, the main work is bookkeeping of set identities and the passage between subsets of (players of the constituent) and subsets of .
ι with decidable equality (the book's ; in Chapter IX players are also named ). Coalitions are Finset ι, and are the complement Sᶜ in , and is a function Finset ι → ℝ.IsConstantSum), the chapter's domain from 42.5.3 on ("in the remainder of this chapter we will continue to consider constant-sum games", p. 353). is arbitrary: the statements are not restricted to zero-sum games, which would be a weaker special case. (43:K) additionally assumes nonempty ([Nonempty ι], the book's ); every other statement holds without it. (43:E) assumes , since the book's constituent is a game and has at least one player.↥J, ↥Jᶜ; the -constituent is restricted to subsets of ↥J. Sums of sets are unions; "disjunct" is Disjoint.decompositionPartition v is the set of minimal splitting sets; that it is a partition is proved, not assumed. An aggregate of minimal splitting sets is a finite family A, its sum A.sup id; the empty aggregate gives .Finset ι and their atoms, which would shorten (43:F)–(43:H).Consider the classical error-correcting problem. An input vector (the plaintext) is encoded as by a coding matrix with , and an unknown, arbitrary vector of errors corrupts the result, so that only is observed. Can be recovered exactly, and by an algorithm whose running time is polynomial in ? Candès and Tao (2005) answer both questions at once: if a matrix annihilating satisfies a restricted orthonormality condition, then is the unique solution of the convex program , which is a linear program, whenever at most entries of are corrupted, whatever their positions and values. Read for the matrix alone, the same theorem says that minimization (basis pursuit) returns the sparsest solution of an underdetermined linear system. That statement is the mathematical core of compressed sensing, and the restricted isometry constants introduced in this paper became the standard tool of the field.
Timeline. Donoho and Huo (2001), followed by Elad–Bruckstein, Donoho–Elad and Gribonval–Nielsen, proved the equivalence of and minimization for matrices formed by concatenating two orthonormal bases, for sparsity of order , through incoherence. Candès, Romberg and Tao (2004) and Candès and Tao (2004) obtained recovery with overwhelming probability for random matrices at sparsity of order . Donoho (2004) showed for Gaussian matrices that a constant, unspecified fraction of nonzero entries can be tolerated. The present paper (December 2004, published 2005) gives a deterministic sufficient condition, , valid for every matrix, and specializes it to Gaussian matrices with explicit numerical values of the tolerable fraction. Later work, for instance Candès (2008) with the condition , sharpened the sufficient condition; those later results are not part of this mission.
Let be a real matrix with columns , and let be the linear span of these columns. For an index set and real coefficients , write . A vector is supported on when for all ; with this convention is just the product . Norms are the Euclidean norm and the norm .
Definition 1.1. For an integer , the -restricted isometry constant is the smallest quantity such that
for all of cardinality at most and all real coefficients . The -restricted orthogonality constant is the smallest quantity such that
for all disjoint with and . The paper writes for . These numbers measure how far the columns of are from an orthonormal system when only linear combinations of at most columns are considered.
The two optimization problems are
A vector is the unique minimizer of one of these problems when it is feasible and every other feasible vector has a strictly larger objective value.
Let be a real matrix of full rank with , and a real matrix with . Let satisfy
If where is supported on a set of size at most , then is the unique minimizer of .
Let satisfy (1.10) for , and let be supported on a set with . Then is the unique minimizer of with .
Theorem 1.5 is the companion of Theorem 1.4 for the decoding problem, and the mission's milestones are the four lemmas the paper proves on the way: Lemma 1.2 (the numbers control the numbers), Lemma 1.3 (uniqueness of sparse representations under ), and the two dual sparse reconstruction properties, Lemma 2.1 ( version) and Lemma 2.2 ( version).
The result. The guarantee is deterministic and uniform: one condition on , checkable in principle from the matrix alone, ensures that a single linear program recovers every sufficiently sparse vector, with no probability of failure. In the decoding reading, a fixed fraction of the ciphertext can be corrupted arbitrarily and the plaintext is still recovered exactly by convex optimization. The paper shows in its Section 3 that Gaussian matrices satisfy (1.10) with overwhelming probability at explicit values of , and in Section 5 that the same hypothesis yields near-optimal recovery of compressible signals from few measurements; both are consequences of the deterministic core formalized here.
Formalizing it. The theorems are proved in the paper, and no machine-checked proof of them exists. Prove2Me holds a formalization of a different restricted-isometry sufficient condition taken from a textbook (HighDimProb.SparseRecovery.rip_implies_exact_recovery); it uses a different definition of the isometry constant and a different hypothesis, so nothing there can be reused as is. This mission produces the definitions of and exactly as in Definition 1.1, the dual-certificate lemmas, and the two theorems, in a form that later missions on compressed sensing can import. The probabilistic Theorem 1.6, Lemma 3.1 and Corollary 1.7, and the compressible-signal Theorem 5.1, are not targets: see the scope section for why.
The whole proof rests on a dual certificate: a vector with for and for . Given such a , the argument of Section 2.2 is a short chain of inequalities. The first idea every newcomer has is ; this interpolates the signs on and, by restricted orthogonality, its inner products off are small in an sense, but not in the sense required. That is exactly Lemma 2.1: the bound holds only outside an exceptional set of at most indices. Lemma 2.2 removes the exceptional set by an infinite alternating iteration, prescribing values on the previous exceptional set while keeping the values on fixed, and summing a geometrically convergent series.
Two points deserve attention from solvers. First, the paper's proof of Lemma 2.2 prescribes values on sets of size up to () at each step, while the per-step factors it quotes, , are what Lemma 2.1 gives for a set of size ; a proof of the printed constant in (2.4) has to account for this, and the hypothesis of Theorem 1.4 leaves room for a proof with slightly worse per-step factors. Second, Lemma 2.1 is printed with in its bound on the exceptional set, while the inequality (2.3) its proof establishes gives ; the mission states the lemma with , which coincides with the printed form in the case used by Lemma 2.2.
Matrices are Matrix (Fin p) (Fin m) ℝ; a coefficient vector on is a vector in Fin m → ℝ supported on the finite set , and is F.mulVec c. The Euclidean and norms and the inner product are explicit finite sums, so every statement can be checked by hand against the paper. is the span of the columns.
The constants and are the infimum of the set of nonnegative (resp. ) satisfying the defining inequalities for all admissible sets and coefficients. This set is nonempty, closed and bounded below, so the infimum is attained and is the paper's smallest quantity; on the paper's domain the smallest such quantity is nonnegative, so the extra clause only fixes a harmless value in degenerate cases such as . The definitions are total in , and each theorem carries the paper's domain conditions (, and , or as needed) as explicit hypotheses. The hypotheses are satisfiable, since a matrix with orthonormal columns has , so none of the statements is vacuous.
"Unique minimizer" is a strict inequality against every competitor. "Full rank" for the matrix with is injectivity of ; both are standing assumptions of the paper's Section 1.1 and appear as hypotheses of Theorem 1.5. In Lemma 2.1, "a constant depending only on " is a positive function of the real number , quantified before all other data.
Out of scope, with the reason for each: Theorem 1.6 refers to a threshold "given in Section 3.5", which the paper does not contain, and to "overwhelming probability" with unspecified constants; Lemma 3.1 is proved only for and "large enough", with an unspecified threshold and an term quoted from the literature; Corollary 1.7 rests on Theorem 1.6; Theorem 5.1 has an unspecified constant and is explicitly not proved in the paper. A future mission can add these once precise statements are fixed.
Contributions that are welcome: proofs of the four milestone lemmas and of the two theorems; reusable lemmas on the attainment and monotonicity of the constants, on the Gram matrix and its inverse under , and on the duality inequality of Section 2.2. Statements that weaken the hypotheses (for instance to ) belong to a separate mission.
In a Walrasian pure exchange economy, agents trade a fixed stock of commodities, and a price vector is a general equilibrium when aggregate excess demand vanishes. Existence of equilibrium (Arrow–Debreu, 1954) says nothing about how prices reach it. The classical tâtonnement model of Samuelson (1947), , is not derived from any optimization principle, and Scarf (1960) gave economies in which it is not globally stable; see also Smale's survey Dynamics in General Equilibrium Theory (JSTOR 1817235) and the chaotic tâtonnement examples of Bala–Majumdar (JSTOR 25054664).
Lindgren (doi:10.3390/analytics1010003) proposes instead that the economy as a whole chooses a price path by dynamic programming: it minimizes a running cost combining a quadratic transaction cost for price changes and the agents' aggregate minimal expenditure. From the resulting Hamilton–Jacobi–Bellman (HJB) equation the paper derives an evolution equation for the price velocity and a condition under which the value function acts as a Lyapunov function: the equilibrium is approached when price adjustments are large enough. This mission formalizes those derivations.
There are commodities and agents. Prices are vectors , and the paper's implicit summation is written . Agent has an expenditure function (minimal cost of reaching a fixed utility level), and the market weighs agents with constants ; the aggregate expenditure is
The economy controls the price velocity and minimizes the cost functional (eq. (7))
whose value function is . The Hamiltonian (eq. (8)) is
the optimal policy (eq. (9)) is , and the HJB equation (eq. (10)) reads
Here always denotes the gradient with respect to prices. Shephard's lemma identifies the Hicksian demand of agent with . For the stability analysis the paper runs time forward, which reverses the sign of the HJB equation: .
If is and solves the time-reversed HJB equation, and the price path follows the optimal policy , then on any interval on which
the function is strictly decreasing; if moreover , it is strictly positive on .
The paper's contribution is the claim that price dynamics derived from an optimization principle are nonlinear and only conditionally stable, with stability requiring sufficiently fast price changes; the author connects this to volatility clustering in financial time series. The derivations in the paper are formal calculations with the regularity of left implicit. Formalizing them pins down exactly which smoothness assumptions each step needs (for instance, eq. (12) uses equality of mixed partial derivatives, hence a value function), and which facts are imported from outside (the HJB equation itself, Shephard's lemma). The resulting statements are reusable calculus facts about HJB equations with quadratic control cost.
Each step is a short computation on paper; the formal difficulty is in the calculus infrastructure: partial derivatives of functions on , symmetry of second derivatives, the chain rule along a curve, and turning a pointwise negative derivative into strict monotonicity on a closed interval. The HJB equation is taken as a hypothesis on rather than derived from the definition of the value function, because the paper asserts it without proof and a rigorous derivation would require viscosity-solution theory.
All declarations live in the namespace LindgrenPriceDynamics. Prices are functions Fin l → ℝ; partial derivatives are Fréchet derivatives applied to standard basis vectors, and time derivatives are one-variable derivatives in the time argument. The value function is a function J : ℝ → (Fin l → ℝ) → ℝ whose joint regularity is stated for the uncurried map on ℝ × (Fin l → ℝ). The standing assumption is kept; positivity of and is not needed by any stated conclusion and is not imposed. Prices are not restricted to the positive orthant. The goal's large-velocity hypothesis is satisfiable (e.g. , , with small on a bounded interval), so the goal is not vacuous.
This mission formalizes N. Monod, Groups of piecewise projective homeomorphisms, Proceedings of the National Academy of Sciences 110 (2013) 4524–4527, doi:10.1073/pnas.1218426110: the groups of piecewise projective homeomorphisms of the line are non-amenable and have no free subgroups whenever .
The paper opens with the Banach–Tarski paradox and von Neumann's notion of amenability: "Tarski readily proved that amenability is the only obstruction to paradoxical decompositions. However, the known paradoxes relied more prosaically on the existence of non-abelian free subgroups. Therefore, the main open problem in the subject remained for half a century to find non-amenable groups without free subgroups" (p. 1). That problem, the so-called von Neumann conjecture, was answered by Ol'shanskii around 1980, with Tarski monsters. Monod's groups give "straightforward torsion-free counter-examples", "so simple that many additional properties can be established" (p. 1).
Monod's groups are close relatives of Thompson's groups: Thurston's model identifies Thompson's group with piecewise maps of the line with rational breakpoints (p. 2). Whether is amenable is a notorious open problem, and whether is amenable is Monod's Problem 12 (p. 2).
The projective line is OnePoint ℝ, on which acts through by Möbius transformations (mob, using Mathlib's action on OnePoint). For a subring of (A : Subring ℝ; is ⊥, is ⊤), P A is , the set of fixed points of hyperbolic elements (trace of absolute value greater than ).
A homeomorphism of is piecewise in with breakpoints in (IsPiecewiseProjOn A E f) when, off some finite subset of , it agrees near every point with a Möbius transformation from . Monod's (Gpp) is the group generated by the homeomorphisms piecewise in , with breakpoints anywhere, and (Hpp) is its stabilizer of (fixInf). For a subring , (G A) is the subgroup of generated by its elements that are piecewise in with breakpoints in (IsPiecewiseProj A), and (H A) is its stabilizer of ; is H ⊥. GRat is the subgroup of generated by its elements piecewise in with breakpoints in , and HRat its stabilizer of : the rational-breakpoint variants of and (p. 2).
Amenability is Garrido.IsAmenable (a finitely additive left-invariant probability measure on all subsets), and "no non-abelian free subgroup" is Chou.NoFreeSubgroupOfRankTwo; both are published definitions, in the bundles Garrido_Amenability and Chou_Classes. Co-amenable subgroups (IsCoamenable), inner amenability (IsInnerAmenable) and pointwise stabilizers (fixSubgroup), all on p. 3, are defined in the bundle in the same style.
A relation is amenable for a measure (IsAmenableRel μ R, p. 2) when it has a left invariant mean in the sense of Connes–Feldman–Weiss: a positive, unital map from bounded measurable functions on to functions on , linear up to -null sets and invariant under the partial transformations of . volP1 is the Lebesgue measure class on .
The goal is Theorem 1, "The group is non-amenable if " (p. 1), introduced as "the main result of this article". The proof (p. 2) passes to a countable dense subring of , compares the orbits of and on (Proposition 9), and concludes from two facts about measured equivalence relations: the orbit relation of an amenable group's action is amenable, and, by a theorem of Carrière and Ghys, the orbit relation of on is not.
The milestones are, in the paper's order: consists exactly of the elements of piecewise in with breakpoints in ; ; preserves orientation, is left-orderable and torsion-free; Proposition 9; the countable dense subring; the orbit relation of a measurable action of an amenable group is amenable; the orbit relation of on is not amenable (Carrière–Ghys, external); Lemma 13 and Theorem 14 leading to Theorem 2 ( has no free subgroups); Corollary 3; Proposition 6 (bi-orderability); Lemma 16, Proposition 7 (co-amenability of pointwise stabilizers), Proposition 15 and Proposition 5 (inner amenability); and Thurston's identification of the rational-breakpoint variants of and with and .
The result. Theorem 1 and Theorem 2 together make , for instance , a torsion-free counterexample to the von Neumann conjecture, with finitely generated examples (Corollary 3). The groups are concrete enough to carry many further properties (Propositions 5–7).
Formalizing it. Nothing on amenability of groups of homeomorphisms of the line, or on measured equivalence relations, is in Mathlib. Amenability and Følner's theorem are on this platform from Garrido I, the Banach–Tarski paradox from Garrido II, Brin–Squier's theorem from its own mission, and Thompson's and (CannonFloydParry, CannonFloydParry_T) from the Cannon–Floyd–Parry missions.
The algebraic half, Theorem 2 and Propositions 5–9, follows Brin–Squier and elementary dynamics on the circle. The analytic half is the passage through measured equivalence relations in the proof of Theorem 1. The mission defines amenability of a relation as Connes–Feldman–Weiss do, by an invariant mean valued in , which is the form under which an amenable group's orbit relation is amenable without extra set-theoretic hypotheses. The step taken from the literature, that the orbit relation of on is not amenable for countable and dense, rests on Carrière–Ghys's theorem and on Zimmer's theory of amenable actions (Adams–Elliott–Giordano). The milestone is proved (Monod.not_isAmenableRel_mob) by an elementary route that needs neither: a ping-pong argument in that contradicts an invariant mean directly.
OnePoint ℝ and acts through Matrix.SpecialLinearGroup (Fin 2) A; since acts trivially the orbits are those of .OnePoint ℝ, each defined as the subgroup generated by the maps the paper describes; the milestones state that is exactly its set of such maps and that .volP1).The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission extends the best possible constant for complex diagonal matrices from to every real . The result is proved in Lean. The constant and its formula are unchanged from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. For each exponent, it works for every triple of diagonal matrices, whatever their size, and no smaller constant does.
The mission started from a supplied pen-and-paper proof. Lowering the cutoff took more than replacing 256 with 90: several estimates in the original argument had to be strengthened. The research note proves the bound for real entries first, then transfers it to complex entries and shows that the constant cannot be improved. The goal theorem below gives the exact formula and statement.
This is the second step of the sharp diagonal Hlawka campaign, and it reuses the foundation's definitions and supporting results. The campaign invites further improvements below 90, keeping the same formula.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryA Markov chain Monte Carlo sampler is often assembled from simpler parts. A practitioner who has several proposal mechanisms for a Metropolis–Hastings sampler can combine them in two ways. Either each drives its own Metropolis–Hastings kernel and the sampler picks kernel with probability at each step, or the mixture is used as a single proposal inside one Metropolis–Hastings kernel. Both samplers leave the target invariant, so the choice is about efficiency.
Section 4 of Tierney (1998) settles the comparison: when both samplers use the maximal acceptance probability, the second never does worse in terms of asymptotic variances of sample-path averages. The statement that carries this is Proposition 5, an ordering of kernels in Peskun's off-diagonal order; the variance comparison then follows from Theorem 4 of the same paper, the general-state-space extension of Peskun (1973).
Timeline. Peskun (1973) introduced off-diagonal domination for finite state spaces and showed that the Metropolis–Hastings acceptance probability is maximal in that order. A version of Proposition 5 for discrete chains appears in the appendix of Tierney (1991) and in the rejoinder of Besag, Green, Higdon and Mengersen (1995). Tierney (1998) states and proves it for general state spaces, using the measure-theoretic description of Metropolis–Hastings kernels from §2 of the same paper.
Let be a measurable space and a probability measure on it, the target. A proposal kernel is a Markov kernel on . Given a measurable acceptance probability , the Metropolis–Hastings kernel is
where is the point mass at (mhKernel Q α).
Put and . With and (canonDensity), let
(canonR, canonRatio). The set is symmetric, and are mutually absolutely continuous on and mutually singular off it (Proposition 1 of the paper). The Metropolis–Hastings acceptance probability is
(alphaMH π Q), and the kernel with is the maximal Metropolis–Hastings kernel for (maxMHKernel π Q).
For kernels on , dominates off the diagonal, (OffDiagDominates π P₁ P₂), if for -almost every , for all . For a countable family of kernels and weights , the mixture is the kernel (mixKernel β K).
Let be a finite or countable family of proposal kernels and with . Let be the maximal Metropolis–Hastings kernel for and the maximal Metropolis–Hastings kernel for . Then
Both sides use maximal kernels: uses of the mixture proposal, each its own , and the same weights form both mixtures.
A companion item states the maximality of (§3, p. 7): every measurable acceptance probability whose kernel is reversible satisfies -a.e., so the maximal kernel dominates every reversible Metropolis–Hastings kernel with the same proposal.
The result. Proposition 5, combined with Theorem 4 of the paper (off-diagonal domination orders asymptotic variances of reversible kernels), shows that for every function with finite variance the asymptotic variance of under the mixture-proposal sampler is at most that under the mixture of samplers. Per-iteration cost can be higher for the mixture proposal, since then needs the densities of all components; Proposition 5 isolates the statistical side of that trade-off. The maximality companion states the fact behind the name "maximal kernel": is the largest acceptance probability that keeps a Metropolis–Hastings kernel reversible.
Formalizing it. The paper's proof is a computation of about six lines with Radon–Nikodym densities. A formal version must make explicit what the computation leaves implicit: that , defined from one dominating measure, has the same density form for every symmetric dominating measure; that the measure inequality on passes to the kernel-level statement with one null set for all ; and that the mixture proposal and the mixture of kernels are handled as countable sums of kernels. As of September 2026 neither Mathlib nor this platform has a machine-checked version of Proposition 5, of the maximality of , or of reversibility of the Metropolis–Hastings kernel on a general state space; only finite-state Metropolis chains have been formalized on the platform.
The obvious argument works pointwise with densities: write every kernel as a density against a common reference measure and compare of sums with sums of minima. On a general state space there is no common reference measure given in advance, and is only defined up to -null sets, through a Radon–Nikodym derivative with respect to , a measure that differs for and for each . The step that needs care is relating these different versions: the densities of the against a common symmetric , the density of , and the transpose densities , which are densities of only because is symmetric.
The second difficulty is the passage from measures to kernels. The inequality between measures on gives, for each fixed , the kernel inequality for -almost every , with a null set that depends on . The order requires one null set for all , and the diagonal must be removed, which needs the diagonal to be measurable.
The formalization is in Lean 4 with Mathlib, in the namespace TierneyMH.Mixture. The state space is a type E with a σ-algebra; π is a probability measure; proposal kernels are Markov kernels Kernel E E. Acceptance probabilities and densities take values in (ℝ≥0∞); a general is assumed measurable with . is π ⊗ₘ Q, its image under Prod.swap, detailed balance is Kernel.IsReversible. Mixtures are indexed by a countable type ("a sequence", which includes finite families), with weights in ℝ≥0 and HasSum β 1.
Added hypotheses, both labelled in the statements: singletons are measurable (implicit in the paper's and ), on the goal and the maximality companion; and, on the goal only, the σ-algebra of is countably generated. The second is an addition to the paper: it is what makes the exceptional null set in uniform over in the passage from the measure inequality to the kernels. It is not assumed in the measure-level milestones.
is one fixed version, built from Mathlib's rnDeriv exactly as in the proof of Proposition 1 (with , not an arbitrary dominating measure), and all statements are insensitive to the version. The ratio is set to 1 on the null subset of where is infinite, so that and hold everywhere, as Proposition 1 asks.
Trivializations ruled out: is the indicator of times , never an arbitrary acceptance function or a single shared by all components; compares , not (on the rejection masses differ and the comparison is false); and the conclusion is about the Metropolis–Hastings kernels themselves, not about the measure identity alone. All hypotheses are satisfiable, for instance on = Bool with uniform, two proposals and and weights .
Needed infrastructure, reusable for other Metropolis–Hastings results: Radon–Nikodym calculus for product measures and their transposes, countable sums of kernels, and a monotone-class argument over a countable generating family. The Metropolis–Hastings kernel, , and off-diagonal domination are defined identically in the companion missions I (detailed balance, Theorem 2) and II (Peskun ordering, Theorem 4) of this series. Proofs of milestones in any order, and proofs of the goal from the milestones, are welcome.
The discrete logarithm problem modulo a prime asks, given a prime , a generator of the multiplicative group modulo , and a nonzero residue , for the exponent with . Its presumed classical hardness underlies Diffie–Hellman key exchange, ElGamal encryption and the Digital Signature Algorithm. The best classical algorithm known when Shor wrote, Gordon's adaptation of the number field sieve, runs in time .
In §6 of Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer (SIAM J. Comput. 26(5), 1997; doi:10.1137/S0097539795293172, arXiv:quant-ph/9508027), Shor gave a quantum algorithm that uses two modular exponentiations and two quantum Fourier transforms and outputs, with constant probability, a pair from which can be computed. The quantitative core of that analysis is a single number: the circuit produces a "good" output with probability at least . This mission formalizes that bound and the three estimates it is assembled from.
Let be a prime and a generator of , so that are all the nonzero residues. Fix the unknown with and put . Let be the power of with .
The Fourier matrix is the matrix with entries for (§4, eq. (4.1)). Rows index input basis vectors and columns output basis vectors.
The algorithm uses three registers: two holding numbers and one holding a nonzero residue modulo . It starts from the state
(preFourierState), applies to each of the first two registers (finalState), and measures all three registers. The probability of observing is the squared modulus of its amplitude (outcomeProb).
For integers and , the symmetric residue is the residue of modulo in (symmRes). Put
An observed state is good (IsGood) when
Goodness depends only on .
The constant is the one the page carries forward. The goal fixes no threshold on : it is stated for every prime that admits a power of two strictly between and .
The result. The bound is what turns the circuit into an algorithm. Repeating the circuit times in expectation yields a good output, and from a good pair one reads off an equation that determines modulo divisors of (§6, eqs. (6.18)–(6.20)). Together with the quantum Fourier transform circuit and reversible modular exponentiation, this places the discrete logarithm modulo a prime in quantum polynomial time. Every later analysis of quantum attacks on discrete-logarithm cryptography starts from this success probability or a sharpened version of it.
Formalizing it. The result has been proved since 1994–1997 and is textbook material; it is not open. As far as is known, no machine-checked proof of Shor's discrete-logarithm analysis exists. The paper's proof of eq. (6.17) replaces a sum by an integral with an error term whose constant is not given, yet states for every prime. A formal proof must therefore either control that error explicitly or find another argument, and so settles a point the paper leaves informal. Numerically, the smallest value of over good states is about for all primes , so the unconditional claim is not in doubt for small . The page also contains two small slips, recorded under Formalization scope; a complete development pins down exactly what is true.
The exponential sum (6.4) runs over pairs satisfying a congruence modulo , while the phases are taken modulo . The two moduli are unrelated: is a power of two and is arbitrary. Eliminating through the congruence introduces a floor function , and the resulting phase is not linear in . The obvious estimate treats the sum as a geometric series in and bounds it by its first-order phase; this fails because the floor term perturbs every phase by an amount of size up to . Condition (6.11) only keeps this perturbation within of the main phase; it does not remove it. The per-state bound must survive this perturbation uniformly in , and , including small primes where the paper's integral approximation gives no explicit control.
The count of good pairs needs a separate argument about how often a multiple lies within of a multiple of when is large.
Fin q × Fin q × (ZMod p)ˣ → ℂ. The first two registers range over ; the third over the units modulo .finalState is defined this way from (6.1) and . It is not typed in as the closed form (6.3) or (6.4). A formalization that defined the final state by (6.4) directly would make milestone 1 trivial, and is ruled out.Fact p.Prime). The generator is encoded as orderOf g = p - 1. is a parameter, with . is given by q = 2 ^ l together with . No large- threshold is added anywhere.x⁻¹ ^ b in the unit group. is computed in and inside and the congruences, and as natural-number subtraction only where makes it exact. is real.Needed infrastructure: finite exponential sums and their modulus, the symmetric residue and its basic properties, and counting multiples in residue classes of . The exponential-sum estimates of milestones 1 and 2 are reusable in the order-finding analysis of §5 of the same paper. Proofs of any milestone, of the normalization , and of auxiliary lemmas about symmRes are welcome.
Many problems in statistics, signal processing and machine learning minimize a sum of a smooth loss and a nonsmooth regularizer: least squares with an or penalty, and constrained problems in which the regularizer is the indicator of a nonconvex set. The proximal gradient method (also called forward–backward splitting) is the standard first-order algorithm for such problems. Each step takes a gradient step on the smooth part and then applies the proximal mapping of the nonsmooth part, which for many nonconvex regularizers (hard thresholding, projection onto sparse vectors) has a closed form.
For a smooth part whose gradient is -Lipschitz, the classical analysis allows any constant step size , and every cluster point of the iterates is stationary; Li and Pong cite Bredies and Lorenz (Minimization of non-convex, non-smooth functionals by iterative thresholding, preprint, 2009) for this. Attouch, Bolte and Svaiter (Math. Program., 2013) added convergence of the whole sequence when has the Kurdyka–Łojasiewicz property. When is nonconvex, however, is governed by the most negative curvature of as much as by the most positive one, and the admissible step sizes can be much smaller than the convex part of alone would require.
Li and Pong (SIAM J. Optim., 2015; preprint arXiv:1407.0753v6) show that the concave part of imposes no restriction on the step size: it suffices to bound the curvature of after it has been offset by a convex function. This mission formalizes that result, Theorem 4 of their paper. It is the fourth mission of a series on the paper; the first three treat its results on the alternating direction method of multipliers.
Work in with the Euclidean inner product and norm . The problem is
under the paper's standing assumptions: is twice continuously differentiable with a bounded Hessian ; is proper (never , finite somewhere) and closed (lower semicontinuous); and for every and the proximal problem has a minimizer. Neither nor is assumed convex.
A vector is a regular subgradient of at (with ) if for all near , for every . The limiting subdifferential collects the limits of regular subgradients at points with . A point is stationary if
Given a step size and an arbitrary starting point , the proximal gradient method generates by
Any minimizer may be selected. A cluster point of is the limit of a subsequence .
The step-size condition involves a convex function and a constant with
where is the Loewner order on symmetric linear maps.
Suppose is twice continuously differentiable and convex, , (44) holds, and is generated by (43) with . Then
and every cluster point of , if one exists, satisfies .
The goal does not assert that a cluster point exists, nor that the whole sequence converges; both are false without further assumptions.
In the order of the paper's proof:
The result. For a difference of convex functions with being -Lipschitz, (44) holds with and , so the step size may be taken in whatever the curvature of . For an indefinite quadratic the admissible range becomes instead of , and for a concave quadratic every positive step size is admissible. Because the method is a descent method under this rule, its iterates stay in a sublevel set of , so the sequence is bounded whenever is coercive. The same estimates feed the whole-sequence convergence argument for Kurdyka–Łojasiewicz functions.
Formalizing it. The theorem is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it requires the limiting subdifferential of an extended-real-valued function, its closedness property (3), and a Fermat rule for a smooth-plus-nonsmooth sum, none of which is in Mathlib. These are reusable for any nonconvex first-order method analysed through cluster points.
The descent part rests on (45), a descent inequality for whose Lipschitz constant is read off from a two-sided Hessian bound; the familiar descent lemma is stated for alone and does not apply, since may have a much larger Lipschitz constant than .
The stationarity part is where the naive argument fails. Passing to the limit in (47) needs not only but also , because the limiting subdifferential is closed only under -attentive convergence. Lower semicontinuity gives one inequality; the other must come from the minimizing property (43) compared against . The objective may be at , so summability of the steps has to be extracted without assuming a finite starting value.
The space is EuclideanSpace ℝ (Fin n). and are real-valued; takes values in EReal, and every objective value is compared in EReal, never through EReal.toReal. The Hessian is the derivative of the gradient map, a continuous linear self-map; the Loewner order is Mathlib's partial order A ≤ B ↔ (B - A).IsPositive, and both sides of (44) are kept. The regular subgradient is encoded in its -neighbourhood form, and the limiting subdifferential requires all three convergences , , . Stationarity is . The update (43) is a relation on sequences: minimizes the bracket over all of , with no uniqueness and a free starting point. A cluster point is the limit of for a strictly increasing .
Trivializing formalizations are ruled out: (44) is not replaced by " is -Lipschitz", which is the classical special case ; , boundedness of the sequence and existence of a cluster point are not assumed; and a limiting subdifferential without is not used, since that would make stationarity a weaker statement.
Contributions welcome: the closedness (3) and the Fermat rule behind (47) for the limiting subdifferential, a descent lemma from a two-sided Hessian bound, and the telescoping and limit arguments of the proof.
The alternating direction method of multipliers (ADMM) splits a problem of the form into a sequence of simpler subproblems, one in which the nonsmooth term enters only through its proximal map and one in which only the smooth term appears. For convex problems its convergence theory is classical. In signal processing and statistics, however, the method is routinely run on nonconvex models, such as - or -regularized least squares, where is nonconvex and possibly discontinuous and convex theory does not apply.
Li and Pong (arXiv:1407.0753, SIAM J. Optim. 25(4), 2015) gave a convergence analysis of a proximal variant of the ADMM for this nonconvex setting. Their Theorem 1 shows that every cluster point of the iterates is a stationary point. That statement is only informative if cluster points exist. Theorem 2, the subject of this mission, gives conditions on , and under which the whole sequence of iterates is bounded, so that cluster points exist and Theorem 1 applies.
Let . The data are:
The augmented Lagrangian is
and the Bregman distance of is . A sequence is generated by the proximal ADMM if, from arbitrary ,
For a linear self-map , write , and write , for the semidefinite and definite order of symmetric maps. Assumption 1 asks for with (so is surjective), bounds , maps with , with , a bound , and with
Suppose Assumption 1 holds and, with the same and , there is with
Suppose that either (i) is invertible and , or (ii) and . Then
The milestones are the numbered displays of the paper's proof:
The result. Theorem 2 supplies the existence of cluster points that Theorem 1 assumes. The two together give an unconditional statement: under Assumption 1, (29) and either coercivity condition, the proximal ADMM has a cluster point and every one of them is stationary. The hypotheses cover the models that motivate the paper. Least squares with a coercive nonconvex regularizer falls under case (i) with , and a strongly convex quadratic with a regularizer that is bounded below and a general surjective falls under case (ii) (Examples 4–6 of the paper). Boundedness is also a standing hypothesis of the paper's Theorem 3, the Kurdyka–Łojasiewicz argument for convergence of the whole sequence.
Formalizing it. The result has been proved since 2015. As far as a search of the platform shows, neither it nor the underlying Lyapunov-type estimates for the ADMM has been machine-checked. This mission formalizes the known proof. The estimates (20), (30) and (31) are shared with the stationarity analysis of the same algorithm, so they serve any later formal work on nonconvex ADMM variants.
The obvious approach is to bound the iterates by the monotone quantity of Eq. (30). That quantity involves , which contains and is not bounded below a priori, so its decrease alone does not bound anything. The dual term has to be absorbed. It is controlled through and the last primal step, and the part involving is then paid for out of itself. Condition (29) exists to make exactly this trade possible, which is why it couples to the of Assumption 1. The two cases then extract boundedness in opposite orders: (i) goes from through to using invertibility of , and (ii) goes from through to . In case (i) the lower bound on that the argument needs is not assumed and must itself be derived from coercivity and lower semicontinuity.
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and is a continuous linear map with Mathlib's adjoint. , and every inequality containing them live in EReal, stated additively so that no extended-real subtraction occurs.Ruling out trivial versions. A formalization that bounds only , fixes or to an example's values, lets (29) use a fresh , adds a lower bound on in case (i), or assumes minimizers that make the sequence constant proves a different, weaker theorem, and is not the target.
Definitions needed. Proper and closed extended-valued functions, the Hessian as fderiv of gradient, the augmented Lagrangian, the Bregman distance, the proximal-ADMM relation and Assumption 1 are all provided. They mirror the definitions of the companion mission on cluster points of the same algorithm. A solver will need standard facts beyond them: first-order optimality for a differentiable function, the mean-value bound from the Hessian sandwich, and strong convexity of the -subproblem. Proofs of individual milestones are welcome independently.
Approximate policy iteration and policy-gradient methods stop when they can no longer find a direction of improvement. Kakade and Langford (ICML 2002) asked what such a stopping point guarantees. Their algorithm, conservative policy iteration, halts at a policy for which no policy can improve much on as measured under a restart distribution ; the quantity that is small is the optimal policy advantage . Theorem 6.2 of the paper translates this local condition into a global statement: the performance of is close to optimal, with a loss controlled by how well covers the states an optimal policy visits.
The bound is the origin of the distribution mismatch coefficient , which reappears in the analysis of approximate dynamic programming (concentrability coefficients, Munos 2003), of conservative and trust-region methods, and of the convergence of policy gradient methods (Agarwal, Kakade, Lee, Mahajan 2021), where it governs the rate. The performance difference lemma (Lemma 6.1) used in its proof has become a standard tool of reinforcement learning theory.
A finite Markov decision process has a finite nonempty state set , a finite nonempty action set , transition probabilities (for each a probability distribution over ), a reward function with , and a discount factor . A stochastic policy is, for each state , a probability distribution over actions. A state distribution is a probability vector on .
The normalized value function is , where , and . The state–action value is and the advantage is . The discounted future state distribution from is
and the performance of from is .
The policy advantage of with respect to and is : the expected advantage of over on the states itself visits. Its maximum over all stochastic policies is (Definition 4.3). An optimal policy satisfies for every policy and every state . For nonnegative on , (p. 5).
If and is optimal, then for every state distribution
The goal states both inequalities and the outer bound. The evaluation distribution is arbitrary and unrelated to the restart distribution ; taking , the start distribution, gives Corollary 4.5 (p. 5).
For any policies , and any starting distribution ,
The states are weighted by the future state distribution of the new policy , the advantage is that of the old policy .
Theorem 6.2 is the quality guarantee for conservative policy iteration: combined with the paper's Theorem 4.4 (the algorithm stops with after polynomially many calls), it bounds the suboptimality of the returned policy for any target distribution, independently of the size of the state space except through the mismatch coefficient. It also explains the role of the restart distribution: a more uniform makes small. Lemma 6.1 is used throughout later theory, from trust-region policy optimization to the global convergence of policy gradient methods.
Both results are proved in the paper, with short arguments. The contribution of this mission is a machine-checked version of the infinite-horizon discounted statement in the paper's normalization, with the ratios handled exactly, including states where a denominator vanishes. Neither the discounted performance difference lemma for stochastic policies nor the distribution mismatch bound is known to be formalized in Mathlib; a finite-horizon performance difference identity has been formalized separately and is a different statement.
The mathematics is short; the difficulty is in the infinite-horizon bookkeeping. The value function and are infinite series, and Lemma 6.1 relates the series of two different policies: its natural one-line argument uses the Bellman equation for , which is not the definition here, together with interchanges of infinite sums over time with finite sums over states and actions, each of which needs summability. Theorem 6.2 then needs two facts that are not stated as results in the paper: that equals (the supremum over policies is attained by a greedy policy, and ), and that . Reading the ratio with real division would give a false statement when a denominator is zero; the statement avoids this.
States and actions are finite nonempty types; policies and kernels are real-valued functions π s a (the paper's ) and P s a s' (the paper's ), with their distribution properties as explicit hypotheses. The published definitions IsTransitionKernel, IsPolicy, InducedTransition, OccupationDist, InducedReward and PolicyValue from the Foundations of Machine Learning series are reused; is times PolicyValue, the defining series. is the supremum of the policy advantages over stochastic policies, which is the paper's maximum. Optimality of is relative to stationary stochastic policies, the paper's policy class; the existence of an optimal policy (the paper's "well known result", p. 2) is not part of this mission.
Every hypothesis is explicit: rewards in with , , a kernel, and stochastic policies, and state distributions. Each bound is stated multiplicatively: "" is " for every with for all ". When some no such exists and the bound is empty, which matches ; no full-support assumption is made on or . The hypothesis is on the supremum itself, not on the closed form , which is a step of the proof; a formalization that assumed the closed form, or that divided by in real arithmetic, would not be this theorem. The proof of the theorem uses only that is a policy; optimality is kept as a hypothesis because the paper states it.
The proof on p. 7 twice writes ; the inequality it uses, and the one stated on p. 5, is . This slip is in the proof, not in the statement. Pages are PDF pages; the paper has no printed page numbers.
Useful reusable infrastructure: summability and Bellman equations for the normalized discounted value, as a probability distribution with , and attainment of by a greedy policy. Contributions of any of these as separate lemmas are welcome.
Johnson's 1954 paper in Naval Research Logistics Quarterly is the starting point of machine scheduling theory. Its first section solves the two-machine flow shop: items must pass through machine 1 and then machine 2, and an explicit ordering rule minimizes the total elapsed time. Its second section treats three machines. There the problem "loses some of the nice structure of the two-stage case" (p. 65), and the general three-machine problem was later shown to be strongly NP-hard (Garey, Johnson and Sethi, 1976). Johnson nevertheless identifies a restricted case, in which the middle machine is dominated by the first (or the last), where the two-machine rule still gives an optimal schedule. That case, and the structural facts behind it, are the content of this mission.
The three-machine results are still the reference point for polynomially solvable flow shops and for lower bounds in branch-and-bound methods for the general problem.
Timeline.
There are items and three machines. Item needs processing time on machine 1, on machine 2 and on machine 3, in that order. Each machine handles at most one item at a time, and processing is not interrupted.
A schedule assigns each item start times . It is feasible when all start times are at least on machine 1, the processing intervals of distinct items on the same machine do not overlap, and , . The three machines may process the items in different orders. The total elapsed time (makespan) is .
An ordering lists the items, being the item in position . Its as-soon-as-possible schedule processes the items in the order on every machine and starts each item on each machine as early as the rules allow. For an ordering, with positions , Johnson defines
the sums running over the items in the first (resp. ) positions.
Johnson's three-stage rule says that item definitely precedes item when
and calls them indifferent under equality. An ordering is consistent with (IV) when no item placed later is definitely preferred to an item placed earlier.
If every is at least every , then an ordering consistent with (IV) exists, and for every such ordering the as-soon-as-possible schedule of is feasible and satisfies
the "maximum walk" of p. 68. 3. Special case (p. 67). If then , so the makespan is . 4. (III) (IV) (p. 67). Interchanging the items in positions changes and only at , and the interchange is strictly worse for the diagonal terms exactly when (IV) holds. 5. Lemma 4 (p. 67). Relation (IV) is transitive, except when the middle item is indifferent to both others. 6. Mirror case (p. 68). The conclusion of Theorem 2 also holds when every is at least every .
The result. Theorem 2 gives an exact method for a class of three-machine flow shops, in a problem that is strongly NP-hard in general. Lemma 3 says that, for three machines, permutation schedules are dominant; Johnson's example on p. 65 shows this fails for four machines. The closed form of milestone 2 expresses the makespan of any ordering as a longest path in a grid, the device behind most later flow-shop lower bounds.
Formalizing it. All results are proved on paper, some tersely: Lemma 3's proof is two lines and cites the wrong lemma, Lemma 4 is proved by reference to Lemma 2, and the mirror case is asserted without proof. A search of Mathlib and of the platform catalog found no machine-checked proof of any of them. The mission produces a checked account of the three-machine flow shop, including the comparison against all feasible schedules rather than only permutation schedules, and pins down the exact form of the hypotheses (see below).
The interchange argument of the two-machine case does not transfer directly. For a general ordering the makespan involves , and interchanging adjacent items changes terms that depend on everything placed earlier; the page notes that "the decision is not independent of what precedes the interchanged elements". The hypothesis is what makes nondecreasing along the ordering, collapsing the double maximum to the diagonal. A second obstacle is that (IV) is not a total preorder: ties break transitivity, so passing from "no adjacent pair can be improved" to "optimal" needs the all-pairs consistency and the tie exception of Lemma 4. Finally, Lemma 3 is a statement about arbitrary start-time schedules, so the reduction to orderings must handle machines whose orders differ.
Items are Fin n; processing times are real-valued functions A B C : Fin n → ℝ, assumed positive in each theorem that is about schedules (the paper's standing assumption, p. 61). A schedule is three start-time functions; feasibility is spelled out as above with non-overlap written as a disjunction of inequalities. The makespan is the maximum of the machine-3 completion times together with , so the empty instance has makespan . An ordering is an Equiv.Perm (Fin n) with σ k the item in position k; positions are 0-based, so the Lean K u, H v are the paper's , . Statements with maxima over positions assume .
Hypotheses made explicit or corrected:
Optimality in the goal is against every feasible schedule. A formalization that compares only orderings with each other, or that defines the objective as the closed form , would drop Lemma 3's content and is ruled out: the makespan is the latest completion time of a start-time schedule. The existence clause keeps the optimality clause from being vacuous.
A complete development needs finite sums over initial segments of Fin n, Finset.sup', and permutation manipulations (adjacent transpositions, bubble-sort arguments). The feasibility model and the closed form are reusable for other flow-shop results; contributions of general lemmas on adjacent interchanges of permutations are welcome.
Federated learning combines information from several clients without pooling their raw training records. A client may later request removal of its contribution. Retraining on the retained records supplies a natural comparison model, but repeating the training process can be costly. Jin, Chen, Zhang, and Li introduce a linearized learning pipeline and a server-side removal procedure in Forgettable Federated Linear Learning with Certified Data Unlearning, arXiv:2306.02216v3. Their linearization makes the training objective quadratic, so the distinction between an exact Newton correction and an approximate correction can be studied explicitly.
This mission formalizes a corrected finite-run error bound motivated by that analysis. It is not a transcription or validation of the printed Theorem 2. The source audit found that the supplementary argument drops a finite-training term when passing to a limit, uses an invalid general inverse-perturbation inequality, and does not justify its three-term squared-norm constant. The draft preserves the removal problem while stating its error factors explicitly. The source anchors are Section III-C, Theorem 2, PDF pp. 5–6, and supplementary Section C5, PDF p. 16. The preprint first appeared in 2023; this mission fixes the revised May 2026 version so later source changes cannot silently alter its meaning.
A parameter is a vector . Record has a fixed linear feature map , an offset , and a target . Its prediction is . This represents the fixed linearization in the paper's equation (3); arbitrary real targets are permitted, and one-hot classification targets are a special case. Neither approximation accuracy for a nonlinear neural network nor an infinite-width limit is asserted.
Let be the full finite dataset and a nonempty subset of retained indices. Client removal is represented by retaining precisely the indices whose owner differs from the removed client. More general record removals are also allowed. For a fixed regularization parameter , define
Write , , and . Define and let use the full dataset. These reference parameters are computed from the data. The accepted child proofs establish the Hessian positivity and invertibility needed for the error bound; the broader unique-minimizer theorem is a separate supporting statement. The construction comes from Section III-A, PDF pp. 3–4, equations (3)–(5).
A separate nonempty server dataset has Gram operator and regularized Hessian . All operator norms below are Euclidean operator norms. The datasets and feature maps are fixed throughout the probability calculation.
Let be the trained parameter, the parameter returned by retraining on , and an approximate removal correction. The removed parameter is . Their joint probability model has finite outcome space , with masses summing to one. They may be dependent. This covers the outputs of finite randomized runs on finite data with fixed initialization; no independence assumption is used.
For each trained parameter , define the server removal objective and its exact minimizer by
This is the quadratic surrogate in Section III-B, PDF p. 5, equation (6). Define
The corrected goal is
The two completed milestones used by the accepted proof are the surrogate gap bound and the corrected signed removal-error identity:
The broader ridge-structure, exact-Newton-removal and inverse-perturbation statements remain available as separate open theorems. Their milestone entries were removed because the accepted proof does not depend on their full statements.
Formalization note: the completed root is a corrected, paper-derived error bound. Its formal bridge uses the two source-backed child theorems above, anchored to Section III-B (Section 3), PDF p. 5, equation (6), and Section III-C (Section 3), PDF p. 5 and PDF p. 6, Theorem 2; supplementary C5, PDF p. 16, unnumbered displays. The coefficients in the boxed goal are conservative; no optimality claim is made.
The result connects the removal solver's objective gap, the difference between the server and retained Hessians, and the actual optimization errors to an observable parameter discrepancy. Exact Hessian matching sets . Exact removal optimization sets , but finite retraining error still remains. This distinguishes exact optimization of the retained objective from reproducing an unfinished retraining run.
The original paper motivates the comparison; the displayed corrected bound is a new formulation derived from its quadratic setting. The root Lean theorem and its two dependency milestones are now Proved. Their accepted proofs match the original formal statements exactly; the three separate supporting statements remain open. The requested OpenProblem classification describes the formalization task and does not assert that the elementary corrected inequality is an unresolved research conjecture.
An approximate server Hessian cannot be substituted for the retained Hessian without a sensitivity term. A bound on the difference of the Gram operators alone does not bound its action on every parameter vector. Likewise, a small training error relative to the full-data optimum does not imply that the full and retained optima coincide. The displacement therefore remains visible. Formalization must respect the normalization of each empirical objective, the sign of the correction, and the operator norm used in the perturbation estimate.
The model uses finite-dimensional real Euclidean spaces, continuous linear maps and adjoints, finite index sets, a total ring inverse, and finite weighted expectations. Positive regularization must justify every use of the inverse; it is not an invertibility assumption hidden inside the dataset. Nonempty retained and server data exclude division by an empty sample count. Zero-dimensional feature or parameter spaces are permitted and harmless. A finite law on an empty outcome type has no inhabitant because its masses cannot sum to one.
The root theorem quantifies over arbitrary output maps . It is an error-propagation theorem in terms of their actual errors and surrogate gap, not a convergence theorem for a particular implementation. Obtaining algorithm-specific bounds on those quantities is separate future work. In particular, the draft does not import the source's unsupported all-smaller-learning-rates FedAvg contraction claim. It also makes no differential-privacy, distributional indistinguishability, nonlinear-network, or empirical accuracy assertion.
The Lasso (Tibshirani 1996, doi:10.1111/j.2517-6161.1996.tb02080.x) is -penalized least squares regression, one of the standard estimators of statistics and machine learning because it selects sparse coefficient vectors. Explaining why a learned Lasso predictor generalizes is less routine than it looks. The two classical routes are uniform convergence over the hypothesis class and algorithmic stability (Bousquet and Elisseeff 2002, JMLR 2:499–526). The stability route is closed for the Lasso: Xu, Caramanis and Mannor (IEEE Trans. Inf. Theory 56(7), 2010, doi:10.1109/TIT.2010.2048503) showed that its uniform stability bound does not decrease with the sample size, a fact reproduced as Theorem 7 of Xu and Mannor (2012).
Xu and Mannor, Robustness and Generalization (Mach Learn 86 (2012) 391–423, doi:10.1007/s10994-011-5268-1), propose a third route, algorithmic robustness: if the sample space can be split into cells such that a test point in the same cell as a training point has nearly the same loss, then the algorithm generalizes (their Theorem 1). Their Example 6 shows that the Lasso is robust in this sense, with a number of cells given by a covering number and a robustness level depending on the training responses. This mission formalizes Example 6 together with the general criterion it rests on (Theorem 6) and the Lipschitz estimate for the Lasso loss (Lemma 3).
A sample is a point with a response and a feature vector , so the samples live in . The sample space is a compact set, and carries the norm . A training set is .
A learning algorithm maps each training set to a hypothesis ; with a loss , it is -robust (Definition 2, p. 396) if can be partitioned into disjoint sets , fixed independently of the data, such that for every , every training point , every and every ,
For a metric on and , a set is an -cover of if every point of is within distance of a point of ; the covering number is the least cardinality of such a cover (Definition 1, p. 394).
For a coefficient vector let . Given , the Lasso is
a Lasso algorithm returns a minimizer of (5) for each , and the loss is the absolute prediction error . Finally .
For every compact , every , every Lasso algorithm and every ,
The statement holds for every selection of a minimizer, since (5) need not have a unique solution.
Combined with Theorem 1 of the same paper, Example 6 yields a generalization bound for the Lasso of the form with a covering number of the sample space, a bound that uses no stability of the algorithm and no uniqueness of the minimizer. Theorem 6 is the reusable part: it converts any data-dependent local Lipschitz or continuity estimate of the loss into robustness, and the paper derives its examples for the SVM, the Lasso, neural networks and PCA from it. The authors note (p. 404) that the resulting bound is weaker than VC-dimension bounds for linear predictors, since it depends exponentially on the dimension; the value of the example is the method, not the rate.
The results are proved in the paper, with short arguments. No machine-checked version of Theorem 6, Lemma 3 or Example 6 is known to exist. The formal work is to connect Mathlib's covering numbers to partitions of a set, to handle the / pairing on , and to state robustness so that later missions of this series (the generalization bound of Theorem 1, mission I) can consume it.
The constant in the robustness level depends on the training set through , while the partition in Definition 2 must be chosen before the training set is seen. A formalization that lets the cells depend on proves a much weaker, nearly empty statement, so the data dependence has to be carried entirely by and the cells must depend only on and . A cover by balls is not a partition, and the radius of the cover () and the closeness threshold in Theorem 6 () differ by the factor that the diameter of a cell requires. The Lipschitz estimate must bound a Lasso solution without any information beyond optimality, and the pairing between and is the one that makes the constant come out as printed; a Euclidean norm on either side gives a different constant.
ℝ × (Fin m → ℝ), a point being (z^{(y)}, z^{(x)}). Lean's norm on this product is the maximum of the absolute values of all coordinates, which is exactly . is written out as , since the default norm on Fin m → ℝ is the sup norm; is dotProduct w x.Z with IsCompact Z. Robustness (IsRobustOn) asks for cells C : Fin K → Set α that lie in Z, cover Z and are pairwise disjoint (empty cells allowed), chosen before the universally quantified training set; training sets are maps Fin n → α with all points in Z. No measurability is involved anywhere in this mission.Metric.coveringNumber at radius Real.toNNReal (γ / 2): closed balls, centres in Z (the metric space of Definition 1 is itself), value in ℕ∞, converted with toNat. Theorem 6 assumes its finiteness, as the paper does; without that hypothesis toNat would return and the statement would be false for nonempty Z. Example 6 does not assume it: it follows from compactness.A with ∀ s, IsLassoSolution c s (A s); it is not defined by a choice of minimizer. The regularization parameter satisfies , which the paper leaves implicit. The factor is a real division; for it is in Lean, the objective reduces to , and all statements remain true.Useful infrastructure beyond this mission: a lemma turning a finite cover of a set into a partition of it with cells of diameter at most twice the radius, and finiteness of Mathlib's internal covering number for compact sets. Contributions of either as separate theorems are welcome.
Classical generalization bounds control the gap between the expected loss of a learned hypothesis and its average loss on the training sample. The average is sensitive to outliers: when a non-negligible fraction of the sample is corrupted, the mean loss stops describing the quality of a solution, and quantile-type summaries such as the median become the natural measurement. Quantile losses have long been used for this reason in statistics and econometrics (Koenker and Bassett 1978; Huber 1981). The standard tools for proving generalization bounds — symmetrization, Rademacher and VC arguments — are built around the expected loss and do not extend to quantiles in any direct way.
Xu and Mannor (Mach Learn 86 (2012) 391–423) introduced algorithmic robustness: an algorithm is robust if the sample space can be partitioned into finitely many cells such that a test point falling in the same cell as a training point incurs a similar loss. Because the argument works cell by cell and needs no symmetrization, it transfers to loss functionals other than the mean. Sect. 4.1 of the paper uses this to bound the quantile value and the truncated mean of the testing error, and Sect. 5 relaxes robustness to pseudo robustness, which only asks the cell condition for a subset of the training samples. This mission formalizes the resulting Theorem 5 (p. 402), whose proof is Appendix C (pp. 415–418).
Let be a measurable sample space, a set of hypotheses and a loss, with each measurable. A training set consists of i.i.d. draws from a probability measure on ; its empirical distribution is . A learning algorithm is a map , and is the hypothesis learned from .
For a real random variable and a level , the -quantile value is
and, writing , the -truncated mean is
where the second term vanishes when . It is the contribution to of the leftmost fraction of the distribution. For a hypothesis and a measure on put and with .
The algorithm is pseudo robust, with and , if can be partitioned into disjoint sets , fixed in advance, such that every training set has a subset of samples with: whenever and lie in a common cell, . With this is -robustness.
Let and . If is pseudo robust, and , then with probability at least : whenever and ,
The constants are the paper's, and , , , , , and the algorithm are arbitrary.
The result. Theorem 5 shows that any pseudo-robust algorithm has a testing-error quantile and truncated mean that are bracketed by the empirical ones at levels shifted by , up to the robustness tolerance . The quantile of the testing error can therefore be estimated from training data for every algorithm to which the robustness framework applies — among them majority voting, SVMs, Lasso and principal component analysis (Sect. 6 of the paper) — without a separate complexity analysis of the loss class. The pseudo-robust form covers algorithms that are robust only away from a small set of training samples, which is the typical situation in the presence of outliers. The robust case is the paper's Theorem 2 (p. 400).
Formalizing it. The paper states Theorem 5 and proves it in Appendix C; no machine-checked proof exists. The appendix contains misprints (see Formalization scope) and the argument uses minimizers of the loss over each cell, which need not exist; a formal proof settles which steps are sound as written. The definitions of quantile value and truncated mean of a law on developed here are reusable beyond this mission.
The concentration step is the same as for the expected loss: on the event the empirical cell frequencies are close to the cell probabilities. The difficulty is converting this into a statement about quantiles. Quantile values are not linear in the distribution and are discontinuous in the level, so the triangle-inequality argument that bounds the mean-loss gap does not apply. Mass that moves between cells shifts every level of the quantile function, and the up to samples outside carry no guarantee at all, so an arbitrary fraction of the empirical law is uncontrolled. For the truncated mean this must be done for the whole lower tail up to level , not just at one point, and the atoms of the loss distribution (the second branch of the definition) have to be accounted for exactly.
XuMannorRobust.Quantile. is a type with a measurable space structure, an arbitrary type, a training set a function Fin n → Z, and the i.i.d. law the product measure Measure.pi (fun _ => μ).Most generalization guarantees in statistical learning theory bound the gap between training error and expected error through a complexity measure of the hypothesis class: VC dimension, Rademacher complexity, covering numbers. Such bounds are sufficient conditions, and they say little about why a particular algorithm, run on a particular data stream, does or does not generalize. Xu and Mannor (Mach Learn 86 (2012) 391–423) proposed algorithmic robustness as an alternative: an algorithm is robust if a test sample "close to" a training sample incurs a loss close to that training sample's loss. Their first results show that robustness implies generalization (Theorem 1 of the paper, the subject of the first mission in this series).
Section 8 of the paper asks the converse question: is some form of robustness also necessary? The answer is Theorem 8. For a learning method trained on a fixed, growing sequence of samples, generalization is equivalent to a weaker property, weak robustness. The authors present this as evidence that robustness is "an essential property of successful learning", and contrast it with the characterization of learnability by stability (Remark 5 of the paper, citing Shalev-Shwartz et al. 2009; journal version JMLR 11 (2010)): learnability is uniform over all distributions, whereas the generalization studied here is for one distribution and one training sequence.
Let be a measurable space of samples, drawn from an unknown probability measure . Let be a set of hypotheses and a loss with for all (the paper's standing assumption, Sect. 1.1).
expectedLoss).avgLoss).firstN).The method generalizes w.r.t. (Definition 8) if
It is weakly robust w.r.t. (Definition 9) if there are sets with and
A set can be read as a family of perturbed copies of the training set that carries almost all of the probability of the test sample.
for every probability measure , every loss measurable in with values in , every learning method and every training sequence .
Milestones 1–2 give the sufficiency direction; milestones 3–4 give necessity.
Theorem 8 is a characterization, not a bound. The sufficiency half says a quantitative robustness property yields generalization. The necessity half says every method that generalizes along a sequence is weakly robust along it, so no generalization argument can avoid something of this shape. The paper remarks that -robustness for every implies weak robustness, which places Theorem 1's condition inside this characterization. Corollary 6, the almost-sure version (generalization with probability 1 iff almost-sure weak robustness), follows from Theorem 8 applied sequence by sequence.
The result is proved in the paper; no machine-checked proof of it is known. This mission contributes a formal statement of Definitions 8 and 9 in Lean, the two directions of the proof as reusable finite- and asymptotic lemmas, and a place to formalize the bounded-loss law of large numbers for a hypothesis that changes with (Eq. (9)), which Mathlib states for a fixed random variable.
The sufficiency direction is a direct estimate once the expectation of the average test loss is identified with the expected loss; the formal work is in handling the product measure and a set that need not be measurable.
The necessity direction is where care is needed. Eq. (9) is not the weak law of large numbers for a fixed function: the hypothesis changes with , so the concentration must be uniform in the hypothesis, which holds only because the loss is uniformly bounded. Lemma 2 negates a statement with an existential over sequences of sets and a limit; the naive reading "for each some works eventually" does not by itself produce a single sequence satisfying (6) with one limit.
MeasurableSpace, a Measure with IsProbabilityMeasure, an arbitrary type. The learning method is A : (n : ℕ) → (Fin n → Z) → H, the training sequence sStar : ℕ → Z, and Measure.pi (fun _ : Fin n => μ). Indices start at .ℝ≥0∞). The sets need not be measurable; their probability is the outer measure. "For infinitely many " is ∃ᶠ n in atTop.Measure.pi of coordinate functions, a Chebyshev or Hoeffding bound for averages of bounded i.i.d. variables uniform over a family of functions, and a diagonal-sequence construction. The uniform concentration lemma is reusable beyond this mission. Proofs of the milestones, and alternative routes to Eq. (9), are welcome.A learning algorithm maps a training set to a hypothesis. It generalizes when the loss it incurs on the training set is close to its expected loss on fresh data. The classical way to certify this bounds the complexity of the whole hypothesis class the algorithm may output, through its VC dimension, covering numbers or Rademacher complexity. A second approach, algorithmic stability (Bousquet and Elisseeff 2002), looks instead at how the output changes when one training point is replaced.
Huan Xu and Shie Mannor proposed a third notion, algorithmic robustness. An algorithm is robust if the sample space can be cut into finitely many cells such that a test point falling in the same cell as a training point incurs nearly the same loss as that training point. The notion came out of their earlier analyses of support vector machines and the Lasso as robust optimization problems (Xu, Caramanis and Mannor 2009). The conference version appeared at COLT 2010, and the journal version, which this mission follows, is Xu and Mannor, Machine Learning 86 (2012) 391–423.
Robustness is a property of the algorithm and not of its hypothesis class, so it applies to algorithms whose class has infinite VC dimension. The paper's main result for i.i.d. data is Theorem 1 (p. 396). This mission formalizes Theorem 1 together with the steps of its proof.
Throughout, is a measurable space of samples and is an arbitrary set of hypotheses. A loss satisfies for a constant . A training set is , and a learning algorithm is a map , written .
For a probability measure on , the expected error and the training error of the learned hypothesis are
Definition 2 (p. 396). For and , the algorithm is -robust if can be partitioned into disjoint sets such that for every ,
The partition is chosen once, before the training set. Only the tolerance may depend on .
For a partition , the cell count is the number of training points in . The Lean development uses expectedLoss, empiricalLoss, cellCount and IsRobust in the namespace XuMannorRobust.Standard.
Let be -robust and let consist of i.i.d. draws from . Then for every , with probability at least ,
The constants are the paper's and are kept as printed. , , , , , and the algorithm are all universally quantified.
Theorem 1 is the base result of the robustness framework. The later results of the same paper are extensions of it:
Its complexity term depends only on the number of cells , not on any capacity measure of . This is why it gives bounds for algorithms such as support vector machines, Lasso, feed-forward networks and principal component analysis (Sect. 6 of the paper). For those, is a covering number of the sample space. Section 8 of the paper shows that a weak form of robustness is also necessary for generalization.
Theorem 1 is a published result with a short proof. What a formalization adds:
A search of the platform (2026-09-26) found no formal statement of Theorem 1, Definition 2, or the Bretagnolle–Huber–Carol inequality for multinomial vectors. Hoeffding's inequality is already available there in proved form.
The deterministic step, Eq. (4), splits the expected loss over the cells. It then compares the loss within each cell with the loss at the training points in that cell. This needs integration over a partition and some care with cells of -measure zero, where the conditional expectation in the paper's chain is undefined.
The main obstacle is the probabilistic step. The quantity is an deviation of a multinomial vector. A coordinate-wise Hoeffding bound followed by a union bound over the coordinates gives a bound whose deviation level grows linearly in . That is not , and it does not give the constant of Theorem 1. The difficulty is to obtain the exact exponential rate for the deviation as a whole, with no loss in the constant.
Samples are a type Z with a MeasurableSpace, training sets are Fin n → Z, the algorithm is a function (Fin n → Z) → H, and the loss is H → Z → ℝ. The partition is a family C : Fin K → Set Z that is pairwise disjoint, measurable, and covers Z. Empty cells are allowed, as in the paper. The i.i.d. sample law is Measure.pi (fun _ => μ) with μ a probability measure, and enters as a real number.
"With probability at least " is encoded as an upper bound on the outer measure, under , of the set of training sets where the inequality fails. This needs no measurability of .
The paper ignores measurability. The formalization restores it: every is measurable and every cell is a measurable set. Together with this makes the expected error a genuine expectation.
The theorems assume . The Bretagnolle–Huber–Carol step assumes , because the printed inequality is false for . No upper bound on is imposed: for the radicand is negative, the square root evaluates to , and the statements remain true.
Two trivializing readings of Definition 2 are ruled out:
IsRobust the existential over the partition precedes the universal over training sets. If the order were swapped, every algorithm with a -valued loss would be -robust, since it could take the two level sets of its own learned loss as cells. Theorem 1 would then fail for a memorizing classifier.Beyond the paper's text, a complete development needs the integral over a finite measurable partition, a Hoeffding bound for indicator averages, and a union bound over the subsets of Fin K. The multinomial concentration inequality is reusable beyond this mission, in histogram estimators, discretization arguments and the covering-number examples of the paper. Contributions are welcome at every level: proofs of the milestones, and alternative proofs of the Bretagnolle–Huber–Carol step (for instance via the method of types).
A two-stage stochastic linear program with fixed recourse chooses a first-stage decision before a random vector is observed, and then pays for a cheapest corrective action once is known. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning with random demand, and energy dispatch are all written in this form, and every decomposition algorithm of the field (L-shaped, stochastic decomposition, progressive hedging) works on it.
Roger J.-B. Wets' survey Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program (SIAM Review, 1974) collected the structural theory of this model: where the problem is feasible (§4), what the expected cost looks like as a function of (§7), and when the resulting convex program is well behaved (§8). This mission formalizes the second chain, from the polyhedral structure of the recourse function to the stability of the deterministic equivalent program: the existence of an optimal Lagrange multiplier for the first-stage constraints. Stability is what makes the optimal value react at a bounded rate to perturbations of the first-stage right-hand side, and it is the hypothesis under which dual and decomposition methods have something to converge to.
The data are a random element with , , and an matrix, distributed according to a probability measure . The recourse matrix (), the first-stage matrix () and are fixed. The recourse function is
equal to if the second-stage program is infeasible and if it is unbounded.
The weak covariance condition (Definition 2.2) requires , and to be integrable for all indices; it does not require , or themselves to be integrable. The paper also assumes throughout that has full row rank (p. 312).
Expectations use the paper's integral: positive part minus negative part, with each part infinite if its integral diverges or the integrand is infinite on a set of positive measure, and . The expected recourse is and the objective is
The induced constraints are , where and is the support of the distribution of . The fixed constraints are , and . The deterministic equivalent program (8.2) is to minimize over .
A convex program of the form with finite value is stable (Definition 8.1(iv)) if there is with for all , . Equivalently, the dual obtained by perturbing is solvable and has no duality gap.
If the weak covariance condition holds, has full row rank, is a polyhedron and the program is finite, , then
Stability of (8.2) is the regularity property that the dual and sensitivity theory of two-stage programs relies on. It gives a finite Lagrange multiplier for the first-stage constraints, a supporting hyperplane of the perturbation function at , and hence a bounded rate of change of the optimal value under perturbations of . The route through Theorems 7.6 and 7.7 also yields facts that are used on their own: the objective is a convex function that is either finite or identically on the feasible region, and it is Lipschitz with a constant controlled by the weak covariance moments.
The results have been proved since 1974, and Lemma 8.9 is cited there to Walkup and Wets (1969). As far as the platform's catalog shows, none of them is formalized for a general distribution. The platform has finite-scenario versions of related facts from Birge and Louveaux's textbook, Chapter 3: StochasticProg.Recourse.thm6a_Q_lipschitz_convex_finite (the expected recourse is finite, convex and Lipschitz on for finitely many scenarios) and StochasticProg.Recourse.thm5a_K2_closed_convex. A complete development would supply the general-distribution versions, with the paper's own extended integral.
The obvious argument for Theorem 7.7 integrates a pointwise Lipschitz constant of . It fails unless that constant is integrable, and the weak covariance condition, not integrability of , is what has to deliver this, uniformly over the finitely many second-stage bases.
For the goal, convexity and finiteness of the program are not enough. The paper's Example 8.5 has a finite convex deterministic equivalent with an infinite duality gap, and the counterexample under Formalization scope has a finite value and no multiplier. When the domain of has curved boundary, the perturbation function can have infinite slope at ; the polyhedral hypothesis on is what excludes this.
Fin n → ℝ; matrices are Matrix (Fin _) (Fin _) ℝ; row vectors of the paper (, , ) enter through dotProduct. The law is a probability measure on (Fin n → ℝ) × (Fin n̄ → ℝ) × (Fin m̄ → ℝ) × (Fin m̄ → Fin n → ℝ). is the platform definition KallMayer.Recourse.PointwiseRecourse, an EReal-valued infimum. Supports are MeasureTheory.Measure.support.lintegral of the positive part minus lintegral of the negative part, with whenever the positive part is . This is the paper's ; Mathlib's EReal subtraction resolves the other way. A Bochner integral of toReal would be for non-integrable integrands and make every expected-cost statement trivial, and it is not used. is a Bochner integral, legitimate because Definition 2.2 makes each integrable.Integrable.ConvexOn of toReal on the finite branch.PointedCone.FG/DualFG in Mathlib), LP duality with values, the paper's extended integral, and a Kuhn–Tucker theorem for convex programs with polyhedral constraints (Rockafellar, Convex Analysis, Thm 28.2). Corollary 7.3 and Lemma 8.9 contain no probability and are reusable across convex analysis. Proofs of any milestone, and lemmas on the paper's extended integral (monotonicity, subadditivity), are welcome.A two-stage stochastic program with recourse is a linear program in which a decision is taken before a random vector is observed, and a corrective (recourse) decision is taken afterwards at a cost. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning, energy dispatch and inventory models are routinely written this way. Before any algorithm can be applied, the model has to be reduced to a deterministic equivalent program in alone, and the first question is which are admissible at all: the random second-stage constraints induce constraints on that are not written down anywhere in the data.
Roger J.-B. Wets's survey (SIAM Review 16(3), 1974) settled this question for fixed recourse (the recourse matrix is not random) under a weak moment condition on the data. Its §4 shows that the natural definitions of the induced feasibility region agree, that the region is always closed and convex, and that it is a polyhedron, described by finitely many deterministic linear inequalities, whenever the technology matrix is fixed. The last fact is what makes decomposition methods such as the L-shaped method of Van Slyke and Wets (1969) terminate with finitely many feasibility cuts.
Timeline: Dantzig (1955) and Beale (1955) introduce linear programs under uncertainty, under assumptions that make every feasible (relatively complete recourse). Wets (1966) and Kall (1966) begin studying the feasibility region without that assumption; Wets (1966c) introduces the polar matrix used for the polyhedrality result. Walkup and Wets (1967) treat random . The 1974 survey collects these results in the form formalized here.
The data are a fixed real matrix and a random vector with , , and an matrix. The law of is a probability measure on the product space, and its support is the smallest closed set of measure one. The recourse function is
equal to when the program is infeasible and when it is unbounded below. The expected recourse uses the paper's integral: the sum of the positive part and the negative part , with .
The weak covariance condition (Definition 2.2) asks that , and be integrable for all . Write . The candidate feasibility sets for the induced constraints are
A convex polyhedron is a set given by finitely many linear inequalities; and are polyhedra.
If is fixed and satisfies the weak covariance condition, then
so is a closed convex polyhedron. The number of inequalities is not fixed in advance, and may be empty.
Theorem 4.1 and Corollary 4.5 show that three different notions of second-stage feasibility (almost sure, on the support, finite expected cost) coincide, and that feasibility depends only on the distribution of . This justifies computing the feasibility region from the support alone, which is what feasibility-cut algorithms do. Theorem 4.7 guarantees that the deterministic equivalent program is a convex program over a closed convex set, with no moment condition. Theorem 4.10 shows that with a fixed technology matrix the induced constraints are finitely many linear inequalities, even when has an unbounded continuous distribution, so the deterministic equivalent program has a polyhedral feasible region.
The results are classical and proved in the paper. None of them is formalized on Prove2Me for a general distribution. The platform has the finite-scenario analogue of Theorem 4.7's first part, StochasticProg.Recourse.thm5a_K2_closed_convex (Birge and Louveaux, Ch. 3, Thm 5(a)), for finitely many scenarios; it is related work, not a special case in the Lean sense, because its model differs. The mission produces a machine-checked account of the measure-theoretic part (supports, pushforwards, an extended-valued integral with a nonstandard convention) and of the polyhedral part (Minkowski–Weyl for cones).
Two steps resist the obvious approach. First, needs an integrable upper bound for the positive part of on the whole support. is only piecewise linear in , can equal , and , , are not assumed integrable separately, so no single dominating function is at hand; only the products controlled by the weak covariance condition are integrable. Second, Theorem 4.10 intersects infinitely many polyhedra , and an infinite intersection of polyhedra is in general only closed and convex (Theorem 4.7). Showing that finitely many inequalities suffice without any assumption on the shape of the support of is the content of the goal, and the resulting system may be inconsistent, in which case .
Vectors are Fin k → ℝ and matrices are Matrix (Fin m) (Fin n) ℝ; the paper's row vectors and suppressed transposes become Matrix.mulVec. The data space is with its Borel structure, and is a probability measure on the whole space (the paper's sample space only carries ). Readings fixed by the formalization:
Integrable with respect to .EReal subtraction () and the Bochner integral of toReal (zero for non-integrable functions) would both make wrong and are not used.Measure.support; is the support of the pushforward under the (continuous, hence measurable) projection onto .A trivializing formalization is ruled out: a polyhedron indexed by an arbitrary type or by the support would make Theorem 4.10 a restatement of the first part of Theorem 4.7, and a Bochner-integral would make . Neither is used.
A complete development needs Minkowski–Weyl for finitely generated cones (available in Mathlib as PointedCone.FG / DualFG), closedness of finitely generated cones, supports of pushforward measures, and simplicial covers of (Carathéodory). The support and integral lemmas are reusable for every result about recourse functions with general distributions; contributions of such lemmas as separate theorems are welcome.