Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets equipped with a rank function, or equivalently a family of independent sets, obeying a few postulates abstracted from the linear dependence of the columns of a matrix. The obvious first question about such an abstraction is whether it is genuinely more general than its model, that is, whether there are matroids that do not arise from any matrix. Section 16 of the paper answers it with a seven-element example, now called the Fano matroid , and proves that no real matrix corresponds to it.
The question has had a long life. Representability of matroids over a given field is a central theme of matroid theory: Tutte (1958) characterized the matroids representable over the field with two elements by a single excluded minor, the four-point line , and the regular matroids by three excluded minors, , and its dual; and Seymour's decomposition of regular matroids (1980) rests on the same objects. Whitney's §16 is the starting point of this line: the first proof that the abstract postulates admit matroids outside linear algebra over .
Timeline:
Let be an matrix with columns . For a set of columns, let be the rank of the submatrix formed by those columns. Regarding the columns as abstract elements gives a matroid on with rank function : the matroid of . A matroid corresponds to if it is the matroid of , with elements matched to columns.
A circuit of a matroid is a minimal dependent set. For a circuit of the matroid of , there are numbers with for every row , and exactly for ; the set of such vectors is written when only the support condition is meant. Stacking one such row per circuit gives the circuit matrix of , determined up to nonzero factors on its rows.
A fundamental set of circuits of a matroid with nullity ( the number of elements) is a family of circuits with such that the elements can be ordered with and for ; it is strict if for every .
The matroid of §16 has elements ; its bases (maximal independent sets) are all three-element sets except
The number of rows is arbitrary; the existence clause makes the non-existence statement non-vacuous.
The result. The theorem separates the abstract notion of matroid from linear dependence over : some matroids are not real-representable. It also exhibits that representability depends on the field, because the same matroid is the matroid of a matrix over the integers mod 2 (milestone 8). Everything later written about representability over particular fields, excluded-minor characterizations, and the gap between abstract and linear matroids starts from this distinction. Theorem 32 is of independent interest: it translates statements about circuits of a represented matroid into the vanishing of minors of a normalised circuit matrix.
Formalizing it. The result is classical and its proof is short on paper, but it is not formalized in Mathlib, which has matroids (Matroid, circuits, ranks) but no column matroid of a matrix with a rank-of-submatrix characterization, no circuit matrix, and no Fano matroid. The mission produces those objects and the bridge lemmas (Theorem 29, Lemmas 10–11, Theorem 32) that connect matroid circuits with linear algebra of the circuit matrix. No machine-checked proof of the non-representability of the Fano matroid over in Lean is known to the curators.
The obvious attempt is a direct search: suppose a real matrix has as its matroid and derive a contradiction from the seven dependent triples. This does not work as stated. Each rank condition is a determinantal (nonlinear) condition on the entries, the number of rows is unbounded, and a representation is determined only up to row operations and column scalings, so there is no finite case check and no single linear computation that settles the question. The contradiction has to come from an argument that is invariant under these symmetries, and the milestones (circuit vectors determined up to scaling, fundamental sets spanning, circuits detected by minors) are what such an argument needs to be stated in. The field also matters: the argument must use that in , since over a field of characteristic 2 the statement is false (milestone 8).
Matroids whose ground set is the whole (finite) type. The Fano matroid lives on Fin 7, Whitney's element being k - 1; the seven triples are written out literally. Matrices are Matrix (Fin m) ι K; "the matroid of " means: ground set everything, and the rank M.eRk N of every finite set of columns equals Matrix.rank of the column submatrix.Fin t with , and determinants are of square submatrices in the paper's row and column order.Reusable beyond this mission: the matroid of a matrix over a field, the circuit matrix, fundamental sets of circuits, and the Fano matroid. Contributions welcome: proofs of the milestones, and a proof of the goal by any route, including one that does not go through Theorem 32.
Whitney's 1935 paper introduced matroids as an abstraction of linear dependence among the columns of a matrix. Most of the paper works over the real numbers; its appendix asks which matroids arise from matrices of integers mod 2, that is, matrices with entries 0 and 1 in which rank and dependence are computed over the two-element field. These are today's binary matroids. They include the cycle matroids of graphs (Whitney closes the paper by noting that graphs correspond to mod-2 matrices with exactly two ones in each column) and they are the setting of several later structure theorems: Tutte's excluded-minor characterization of binary matroids (Tutte 1958), Seymour's decomposition of regular matroids (Seymour 1980) and Seymour's theory of binary clutters and max-flow min-cut (Seymour 1977), which underlies parts of combinatorial optimization.
Whitney's answer is an intrinsic postulate, (C*), on the circuits of the matroid, stated without reference to any matrix, and a constructive representation theorem (Theorem 37): a matroid satisfying (C*) is the matroid of a mod-2 matrix, and the matrix is unique once the columns of one base are fixed.
A matroid on elements is given by its independent sets; its circuits are its minimal dependent sets, its rank is the size of a base, and its nullity is . Here is a Mathlib Matroid (Fin n) whose ground set is all of Fin n.
Subsets of the elements are added mod 2: a sum of finitely many sets is the set of elements lying in an odd number of them (for two sets, the symmetric difference). A cycle is a sum mod 2 of circuits; the empty sum is the null cycle . A set is a true sum of sets that have no common elements and whose union it is. Postulate (C*) requires that each cycle be a true sum of circuits.
With , a family is a strict fundamental set of circuits with respect to if , each is a circuit, and contains but no other .
For a matrix over the integers mod 2 with columns , columns are independent (mod 2) if no non-null subset of them sums to the zero column. The matroid corresponding to has the column indices as elements and these independent sets.
Let satisfy (C*), with elements and base . For every matrix mod 2 (any number of rows) whose columns are independent mod 2,
Milestone 7 and the goal together characterize binary matroids as the matroids satisfying (C*).
The result. Theorem 37 and the p. 532 claim give an intrinsic, matrix-free description of the matroids representable over the two-element field, and Theorem 36 parametrizes all of them by arbitrary subsets of a base. Uniqueness in Theorem 37 says that a binary representation is determined by the columns of one base; in modern terms, binary matroids are uniquely representable over GF(2) up to row operations. Every later theory of binary matroids, including graphic and cographic matroids, Tutte's excluded-minor theorem and Seymour's decomposition, starts from this equivalence.
Formalizing it. The results are proved in the paper and in textbooks (e.g. Oxley, Matroid Theory, Ch. 9) but, at the Mathlib revision used here, there is no notion of a matroid represented by a matrix over a field, and no binary-matroid theory. On Prove2Me, the existing binary objects (SeymourMFMC.Binary.*) are binary clutters defined through blockers, not matroids represented by mod-2 matrices. This mission produces the representation predicate for mod-2 matrices, the cycle space of a matroid, and the equivalence between (C*) and binary representability.
Writing down candidate columns is not the hard part; showing that the matroid of the completed matrix is itself, and not merely a matroid sharing some of its circuits, is. Whitney's example at the end of §9 exhibits two different matroids with a common strict fundamental set, so agreement on fundamental circuits does not by itself identify a matroid; any argument must use (C*) on both the given matroid and the matroid of the matrix. A naive comparison of independent sets column by column does not close this gap. Uniqueness likewise depends on the independence mod 2 of the prescribed columns: without it, different completions can give the same matroid.
Matroid (Fin (r + q)) with ground set Set.univ; Whitney's is k - 1, his is the range of Fin.castAdd q, and is Fin.natAdd r (i - 1). Writing removes natural-number subtraction; is not a free parameter, since is required to be a base.sumMod2); cycles are sums over finite sets of circuits; true sums are unions over finite pairwise-disjoint sets of circuits; (C*) is SatisfiesCStar on the circuit family {C | M.IsCircuit C}. These definitions take the circuit family as a parameter, so that the (C₂) milestone is posed for an arbitrary family of sets, as Whitney poses it.Matrix (Fin m) (Fin n) (ZMod 2) with any ; independence mod 2 of columns is LinearIndepOn (ZMod 2) of the columns (the rows of the transpose). IsMatroidOf M A compares all independent sets, not only bases.Contributions welcome: the general fact that the matroid of a vector family over a field exists (a reusable Matroid.ofFun-style construction over any field), the cycle-space lemmas, and proofs of the milestones in any order.
Many problems in imaging, signal processing and statistics are convex minimizations of the form
where is smooth, and are nonsmooth but have computable proximity operators, and is a bounded linear operator, for example a discrete gradient in total-variation denoising. Primal–dual splitting methods solve such problems using only , the proximity operators of and , and applications of and , without ever inverting or computing the proximity operator of .
Condat's 2013 paper (JOTA 158(2):460–479; final author's version HAL hal-00609728v5) introduced Algorithms 3.1 and 3.2, which handle all three kinds of terms at once, allow relaxation and summable errors, and contain earlier methods as special cases. Together with the closely related work of Vũ (Adv. Comput. Math. 2013), it is the standard reference for the "Condat–Vũ" algorithm.
Timeline. Chambolle and Pock (2011) proved convergence of their primal–dual algorithm, without a smooth term and without relaxation, under (J. Math. Imaging Vis. 40). He and Yuan (2012) interpreted it as a proximal point algorithm in a modified metric (SIAM J. Imaging Sci. 5). Condat (2013) added the smooth term , relaxation and errors (Theorem 3.1), and, for , proved weak convergence for relaxation parameters up to (Theorem 3.2), the result of this mission.
Let and be real Hilbert spaces and a bounded linear operator with adjoint and operator norm . Write for the proper, lower semicontinuous, convex functions . For , the conjugate is , the proximity operator is , and the subdifferential is .
Fix , and . The primal–dual inclusion (6) asks for with
then minimizes and solves the dual problem. The paper assumes this inclusion has a solution.
Given , relaxation parameters and error terms , , Algorithm 3.1 iterates, from any ,
Algorithm 3.2 exchanges the roles: it computes from first, then using .
Suppose and , , and
Then for every run of Algorithm 3.1, and for every run of Algorithm 3.2, there is a solution of (6) with and weakly.
Remark 3.2 (the goal with affine, , instead of ) and Theorem 5.2 (the version with composite terms and condition ).
The result. Theorem 3.2 covers the Chambolle–Pock algorithm with relaxation and summable errors, in arbitrary real Hilbert spaces. Over-relaxation often speeds the method up in practice, and the error terms justify inexact proximity operators. Theorem 5.2 extends it to any finite number of composite terms by full splitting. The convergence statement makes no reference to a Lipschitz constant, so it applies whenever the problem has no smooth part.
Formalizing it. The result is proved on paper; no machine-checked version of Theorem 3.2, of the Krasnosel'skii–Mann lemma with errors, or of the proximal point algorithm under the condition is known to exist. A formal proof would supply reusable pieces of monotone-operator theory in Hilbert spaces: weak convergence of Fejér-type iterations, the change of metric induced by a positive operator, and maximal monotonicity of sums with a skew operator.
The algorithm is not a fixed-point iteration of a nonexpansive map in the original inner product: the coupling between the primal and dual steps breaks nonexpansiveness. The difficulty is to find a metric in which it becomes one, to show this metric is equivalent to the original one (which is where , strictly, is needed), and to transfer maximal monotonicity, zeros and summability of the errors to the new metric. Weak convergence in infinite dimension also requires an Opial-type argument rather than compactness. Mathlib provides inner product spaces, the operator norm and adjoints, but neither maximal monotone operators nor resolvents nor Krasnosel'skii–Mann iteration theory.
The spaces are real Hilbert spaces (InnerProductSpace ℝ and CompleteSpace). Functions valued in are EReal-valued, with the published IsProperClosedConvex. The conjugate is an EReal supremum, so can take the value . Proximity operators enter as maps with the published IsProx property; the subdifferential is the published IsSubgradient. The product with the inner product is WithLp 2 (X × Y). Weak convergence is for all . "" means partial sums tend to , and "" means summability of a nonnegative series.
Standing assumptions are hypotheses: , and (6) has a solution. With the smoothness assumption on is automatic. The paper's assumption that (1) has a minimizer follows from the solvability of (6) and is not stated. The goal is a conjunction over the two algorithms, and the limit is chosen after the run.
The condition is strict, , and relaxation is open, . A goal quantifying over no run, assuming the limit exists, or fixing before the initial point would be a different and weaker statement. Proofs of the milestones, of Theorem 5.2 via the product-space identities (49)–(52), and general results on monotone operators are welcome.
Hassler Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets of elements carrying an abstract rank function that behaves like the rank of a set of vectors. Part II of the paper opens with the decomposition of a matroid into components. The question it answers is basic to every later use of matroids: when does a matroid split into independent pieces, and how can the pieces be recognized?
For the matroid of a graph (elements = edges, rank = number of vertices minus number of connected pieces spanned) the components are the 2-connected blocks of the graph, and Whitney's theorem recovers the classical fact that two edges lie in a common block exactly when they lie on a common cycle. Whitney had studied separability of graphs in Non-separable and planar graphs (1932), and footnote 11 of the 1935 paper points out that the theorem identifies König's "Glieder" of a graph with components. Matroid connectivity built on this notion runs through later structure theory: Tutte's higher connectivity, Seymour's decomposition of regular matroids, and the matroid minors project all start from the separation of a matroid into components.
A matroid on a finite ground set is given here by Mathlib's Matroid structure, with rank function for (Mathlib's M.eRk X) and circuits, the minimal dependent sets (M.IsCircuit). Whitney treats every subset as a matroid in its own right, a submatroid, with the rank function of restricted to subsets of . For sets he writes for the union, for the number of elements of , and
for the nullity of .
Rank is subadditive: . A submatroid is separable if it can be divided into two disjoint groups , each containing at least one element, with
and non-separable otherwise. Every single element is non-separable. A component of is a maximal non-separable part of : a nonempty non-separable set contained in no strictly larger non-separable subset of .
For two distinct elements of ,
Components are defined by the rank function, circuits by dependence; the goal asserts that the two descriptions agree.
The result. Theorem 19 makes the component decomposition computable from circuits alone and shows that "lying on a common circuit" is an equivalence relation on distinct elements, a fact that is not evident from the circuit axioms. Theorem 18 adds that the decomposition is the unique one with additive rank. Together they are the starting point of matroid connectivity: the direct-sum decomposition of a matroid, the reduction of many matroid problems (representability, duality of components, Whitney's own Theorems 24–26 on duals of components) to the connected case, and the higher-connectivity theory that followed.
Formalizing it. The results are classical and proved in the paper; nothing here is open. To our knowledge Mathlib at the pinned revision has no notion of matroid connectivity or components, so this mission produces the first machine-checked development of Whitney's §10: the rank-based definition of separability, the disjoint decomposition into components, the circuit characterization, and the ear-type construction of non-separable matroids (Theorem 17). These are reusable for any later formalization of matroid connectivity, including Whitney's results on duals of components.
The two directions of Theorem 19 rest on different machinery. That two elements on a common circuit lie in one component follows from the rank theory (Theorems 13 and 16). The converse is the substantial direction: a component is defined by the failure of rank additivity, which only says that every division of the component is crossed by some circuit (Lemma 9). It does not directly give one circuit through two prescribed elements. Combining circuits that cross different divisions into a single circuit through both and requires the circuit elimination property together with a minimality argument over subsets of the component; the naive attempt of chaining overlapping circuits from to gives a connected chain of circuits, not one circuit.
Matroid α with [M.Finite]; Whitney's matroids are finite. A submatroid is a subset M.E with the rank M.eRk restricted to its subsets; results that Whitney states for "a matroid " are stated for subsets of an ambient finite matroid, which is the same statement applied to the submatroid .ℕ∞-valued M.eRk, finite on a finite matroid, so (10.1) is an equation of natural numbers. Nullity is computed in as the number of elements minus the rank.IsSeparable M X requires two nonempty, disjoint groups with union and additive rank; without nonemptiness every set would be separable. IsNonSeparable M X adds M.E. IsComponent M K requires nonempty, non-separable, and maximal; nonemptiness excludes the empty set, which is vacuously non-separable.Matroid.IsCircuit.M.eRk and circuit elimination (both in Mathlib), the relation between circuits of M ↾ X and circuits of M inside (Matroid.restrict_isCircuit_iff), and finiteness arguments for maximal non-separable sets. Proofs of the milestones, alternative proofs of the goal, and lemmas relating components to Mathlib's direct sums of matroids are all welcome.Many problems in imaging, signal processing and statistics take the form
where and are convex functions whose proximity operators can be computed cheaply, is a linear operator such as a finite-difference gradient, and is smooth. Total-variation denoising, the lasso with a structured penalty, and constrained least squares are of this type. Because is generally not proximable even when is, practical methods split the problem so that each step uses only , , and , without inverting any operator.
L. Condat (J. Optim. Theory Appl. 158 (2013)) introduced a relaxed, inexact primal–dual iteration of this kind; B. C. Vũ (Adv. Comput. Math. 38 (2013)) studied the same structure for monotone inclusions. With the iteration is exactly the method of Chambolle and Pock (J. Math. Imaging Vis. 40 (2011)). They proved convergence in finite dimension assuming , and no errors. He and Yuan (SIAM J. Imaging Sci. 5 (2012)) extended this to a constant relaxation under the same other hypotheses (Condat, §3.1.1). Condat's paper proves three convergence theorems. This mission is the third: in finite dimension and with , the iterates converge under the step-size condition , equality included. Equality matters in practice: one can set and tune a single parameter, as in the Douglas–Rachford method.
Let and be real Hilbert spaces and a bounded linear operator with adjoint and operator norm . Write for the proper, lower semicontinuous, convex functions , and let , . The Fenchel conjugate is , the proximity operator is , and the subdifferential is .
The primal–dual inclusion (6) asks for with
A solution gives a minimiser of the primal problem and a solution of its dual.
Algorithm 3.1 chooses , , relaxation parameters , error terms and an initial estimate , then iterates
Algorithm 3.2 swaps the roles of the primal and dual variables: the dual step comes first, and the primal step uses . Section 5 extends both to (Algorithms 5.1 and 5.2), with the inclusion (48) in place of (6).
Let , be finite-dimensional, , , and assume (6) has a solution. If
then for every run of Algorithm 3.1, and for every run of Algorithm 3.2, converges to a solution of (6).
With the operator (20) and the error-free step of Algorithm 3.1:
Remark 3.2 (Theorem 3.3 with affine, i.e. in (2)) and Theorem 5.3 (the analogue for composite terms, with (i) replaced by ) are included as draft theorems.
Theorem 3.3 is the convergence guarantee behind the common practice of running the Chambolle–Pock iteration and its relaxed variants at the critical step size . It covers relaxation parameters up to and summable errors in both proximity operators. It applies directly to the discrete models of imaging and statistics, which are finite-dimensional. Theorem 5.3 extends it to any finite number of composite terms in parallel.
None of the statements of this paper is formalized on the platform. Machine-checked convergence proofs for primal–dual splitting are not available in Mathlib. The mission would produce the first ones, together with two standalone tools of general use: the inexact Krasnosel'skii–Mann theorem (Lemma 4.1), and Polyak's recursive-inequality lemma (Lemma 4.6), which is a standard tool for stochastic and inexact iterations.
The usual proof treats the iteration as a proximal-point or forward–backward step in the space with the inner product . That argument needs strictly positive, which is exactly what fails when : then has a nontrivial kernel, is only a seminorm, and weak convergence in the -geometry says nothing about the components of in . The proof replaces the iteration by its "shadow" on , uses that factors through , and recovers the full iterates through continuity of and a recursive inequality. The last step requires strong convergence of the shadow sequence, which is where finite dimension enters. Infinite-dimensional versions require different arguments and are not claimed here.
Spaces are real inner product spaces with CompleteSpace; the goal and Theorem 5.3 add FiniteDimensional. Functions in take values in EReal and satisfy the published predicate IsProperClosedConvex (never , finite somewhere, lower semicontinuous, convex epigraph). The conjugate is an EReal supremum. Proximity operators are maps , satisfying the published minimisation predicate IsProx for and ; such maps exist and are unique for functions. The subdifferential is the published IsSubgradient. Runs of the algorithms are predicates on pairs of sequences with arbitrary initial point, and the limit is chosen after the run. "" for a series is divergence of its partial sums, "" is summability of a nonnegative series, and convergence in the goal is norm convergence.
The standing assumptions of pp. 3–4 are hypotheses: , and (6) has a solution. The paper's other standing assumption, that problem (1) has a minimiser, follows from the second and is omitted. In the milestones, the operators and are plain maps on . The projector is not built: "" is stated as "", which is equivalent because is self-adjoint. Each milestone drops finite dimension, so it is stated at least as strongly as on the page.
The strict inequality would make the goal a corollary of the weaker Theorem 3.2 with an extra finite-dimensional upgrade. The goal keeps . Weak convergence in place of norm convergence, an chosen after , or a solution of (6) fixed before the run would each weaken the theorem, and all are excluded.
Useful infrastructure includes: firm nonexpansiveness of for EReal-valued functions; -ness of the conjugate and Moreau's identity; maximal monotonicity of plus a skew operator; and the inexact Krasnosel'skii–Mann theorem. All of it can be reused for Theorems 3.1 and 3.2 of the same paper, and for Douglas–Rachford and three-operator splitting. Proofs of individual milestones are welcome independently of the goal.
In 1935 Hassler Whitney asked which properties of linear dependence among the columns of a matrix can be stated without reference to the matrix at all. His answer, On the Abstract Properties of Linear Dependence (American Journal of Mathematics 57, 1935), introduced the matroid: a finite set together with a rank function obeying three short postulates. The notion now underlies combinatorial optimization (the greedy algorithm is optimal exactly on matroids, and matroid intersection and partition generalize bipartite matching and arborescence packing), graph theory (graphic and cographic matroids), coding theory and the study of linear representations over finite fields.
A defining feature of the subject is that the same structure can be axiomatized in several apparently unrelated ways: by rank, by independent sets, by bases, by circuits. Each axiom system is convenient for different arguments, and passing between them, a so-called cryptomorphism, is routine in practice. Whitney's paper is where these equivalences first appear. Part I, §§2–4 and §6 (pp. 510–514), derives the basic properties of rank from the rank postulates, deduces from them the postulates for independent sets, and shows that the two systems are equivalent. This mission formalizes that first equivalence.
Let be a finite set of elements . Following Whitney, write for , for the union and for the intersection of subsets; is the number of elements of .
A rank system is a function on the subsets of satisfying
The nullity of is , and is independent when . The increment of (3.1) is , written when .
An independence system is a predicate "independent" on the subsets of satisfying
From an independence system one recovers a rank by letting be the number of elements in a largest independent subset of . In the Lean development these objects are IsRankSystem, nullity, Delta, indepOfRank, IsIndepSystem and rankOfIndep, all in the namespace WhitneyMatroid.RankIndep.
Both translations and both round trips are part of the goal: Whitney's conclusion is not only that each system implies the other but that "the definitions of the rank and the independence or dependence of any subset of agree under the two systems".
The equivalence makes the rank function and the family of independent sets two descriptions of one object. Every later result of Whitney's paper, and of matroid theory generally, moves between them without comment: the circuit postulates of §5 and §8, the base postulates of §7 and the duality of §§11–13 are all phrased through rank or independence as convenient. Theorem 3 is the submodularity of rank, the property that connects matroids to submodular function minimization and polymatroids; here it is derived from the purely local postulates (R₁)–(R₃), which constrain the rank only under the addition of one or two elements.
On the formal side, Mathlib defines Matroid through independent sets (with constructors from other axiom systems) and proves submodularity of its rank; the platform has submodularity for Mathlib matroids (FamousTheorems.matroid_rank_submodular_7a). Neither starts from Whitney's local rank postulates. What this mission adds is a machine-checked derivation of the global properties of rank from (R₁)–(R₃) and of Whitney's original equivalence, stated for his own postulates, so that the later missions of this series, which work from the same postulates, rest on a verified foundation. The result itself has been settled since 1935; the open work is the formal proof.
The postulates (R₂) and (R₃) are local: they speak about adding at most two elements to a set. Monotonicity and the bound follow by adding elements one at a time, but the submodular inequality relates arbitrary sets, and nothing in (R₃) mentions more than two new elements. The gap between the local and the global statement is the substance of Lemmas 3, 4 and Theorem 3, and the deduction of (I₂) depends on it.
In the converse direction the rank is defined as a maximum over independent subsets, while (I₂) only augments a set from an independent set with exactly one element more; (R₃) for the derived rank is a statement about three sets that are not given in that form. The round trips are where the two halves meet, and each depends on the global properties of the first half rather than on the postulates alone.
Elements form a type α with [Fintype α] [DecidableEq α]; subsets are Finset α, and the matroid is the whole type. Ranks, nullities and increments take values in ℤ, so differences never truncate; Whitney allows any number, but (R₁) and (R₂) force nonnegative integers. Postulate (I₂) is stated in Whitney's form with N'.card = N.card + 1, not the general augmentation for . Postulates (R₂), (R₃) keep their hypotheses . Lemmas 3, 4 and Theorem 3 are stated for arbitrary subsets ; Lemma 1's monotonicity for arbitrary , the form in which the paper uses it. rankOfIndep is the supremum of cardinalities over the independent members of the powerset.
The paper takes for granted that the empty set is independent in system (I). Without that hypothesis, the predicate declaring nothing independent satisfies (I₁) and (I₂) vacuously, the supremum defining the rank returns , and the round trip fails; the goal therefore assumes independent in part 2 and proves it in part 1. A formalization in terms of Mathlib's Matroid would make the goal a restatement of library facts, since Mathlib's matroids are independence systems by construction; the goal is deliberately about the postulates as predicates on functions and on families of sets.
A complete development needs only finite set combinatorics (Finset.card, induction on finite sets, Finset.sup). The derived lemmas (monotonicity, submodularity, (I₂)) are reusable for any later work from Whitney's rank postulates, including the circuit-postulate equivalence of the companion mission. A bridge from rank systems to Mathlib's Matroid (via IndepMatroid.ofFinset) would be a welcome addition but is not part of the goal. Proofs of the milestones in any order are welcome; Theorem 3 and the §4 deduction are the natural first targets.
Mathlib.Data.Matroid (matroids via independent sets; IndepMatroid.ofFinset). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matroid/Basic.htmlAbstract dynamic programming, in the form developed by Denardo (1967) and Bertsekas (1977), studies sequential decision problems through a single monotone mapping : the cost of using control at state when the future is valued by the function . Chapters 2–5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), analyze this model when policies are arbitrary selectors and is defined on all extended-real functions on .
That generality breaks down as soon as the state and control spaces are uncountable. A stochastic control problem on Borel spaces needs measurable policies, so that the expected cost is an integral rather than an outer integral, and the functions on which acts must be measurable for the same reason. Chapter 6 of the book introduces a generalized abstract model in which the policies are drawn from a prescribed class and is only defined on a prescribed class of functions. The examples on p. 94 are the models of Part II: universally measurable policies with lower semianalytic costs (Chapters 8–9), analytically measurable policies (Section 11.2), and the semicontinuous models of Definitions 8.7–8.8. Chapter 6 is the bridge that lets the abstract results of Part I be invoked for these models.
The data are a state space , a control space , nonempty constraint sets , and three restricted classes: sets of functions , where is the set of all functions , and a set of selectors with . The mapping is monotone: in implies . For and ,
A policy is a sequence with every ; their set is . Given with , the -stage and infinite-horizon costs are
and the optimal costs are and . For a stationary policy write .
Five standing conditions tie the classes together: A.1 (every control is the value of some ), A.2 ( is closed under and under adding constants), A.3 ( is closed under every , , and under adding constants), A.4 (-minimizing selectors for , , exist in ), and A.5 ( and are closed under pointwise limits). Assumption asks for a closed subset of the space of bounded real functions with the sup norm , containing and invariant under on and under on , such that every exists and is real, each is -Lipschitz on , and every -fold composition is a -contraction on for some .
Under A.1–A.5 and : is the unique fixed point of in , with and ; each , , is the unique fixed point of in ;
a stationary is optimal iff ; and for every some stationary policy in satisfies .
In attack order:
The other results of Sections 6.2–6.3 are posed in the mission as separate theorems:
Proposition 6.4 is the statement that makes value iteration, Bellman's equation and stationary -optimal policies available for discounted problems whose admissible policies are restricted, for instance to measurable ones. Without it, each measurable model would need its own fixed-point argument. The finite-horizon Propositions 6.1–6.3 play the same role for the dynamic programming algorithm , and their hypotheses (, exact selection) are exactly what Chapters 7–8 verify for universally measurable policies.
The book states Propositions 6.4 and 6.5 without proof (p. 97), referring to the proofs of Chapter 4; Propositions 6.1–6.3 are justified by "nearly verbatim repetition" of Chapter 3. A formalization therefore supplies proofs that are only indicated in print, and checks that A.1–A.5 really suffice for each step of the Chapter 3–4 arguments. None of these results has a machine-checked proof that we know of; the companion missions of this series formalize the unrestricted special case (, ) of Chapters 3 and 4.
The Chapter 4 proof of Proposition 4.2 applies the contraction mapping theorem to on . Here the obvious transcription fails at two points. First, maps into itself but only maps into itself, so the fixed-point theorem must be applied on two different sets, and these are closed only because of A.5. Second, every argument that picks a near-minimizing selector at each state must produce a selector in : pointwise choices are no longer allowed, and A.1, A.4 and the exact selection assumption are the only sources of admissible selectors. Proofs of Chapter 3–4 that build a policy state by state cannot be copied.
Functions on are S → EReal. is a total Lean function, but monotonicity is assumed only on and every statement evaluates only at functions of . is limUnder; Assumption makes the limit exist. is Mathlib's ; a bound between extended-real functions means both are real everywhere and , which is how the book's convention reads a norm of a difference. No statement adds values of opposite infinite sign, so Mathlib's EReal addition agrees with the book's wherever it is used. and are infima over only, the -optimality notions keep the book's two-case form at , and is a positive integer.
The chapter collapses to Chapters 3–4 if or is built in; here , and are arbitrary and constrained only by A.1–A.5, and is never defined as a fixed point.
A complete development needs the -step contraction mapping theorem on a closed subset of , monotonicity lemmas for and , and the restricted-class versions of Propositions 3.1–3.4 and 4.1–4.4. These are reusable for the Borel models of Chapters 8–9. Proofs of any milestone, and sorry-free lemmas about the Assumption contraction, are welcome.
Linear programming, with , is the basic model of operations research, and the complexity of solving it is a central question of algorithm theory. Interior-point methods follow the central path: primal–dual pairs with and for every , as the path parameter decreases to . A classical short-step method needs iterations, each solving a linear system with the matrix , for a total of roughly operations or more.
Cohen, Lee and Song (J. ACM 68(1), 2021; arXiv:1810.07896) showed that linear programs can be solved in time (for the current values of the matrix multiplication exponent and its dual ), matching the cost of multiplying two matrices. The analysis has two halves: a data structure that maintains the projection matrix lazily, and the stochastic central path method, which replaces each Newton step by a sparse random step and proves that the iterates still stay close to the central path. This mission formalizes the second half.
Timeline: Karmarkar's projective method (1984) gave the first polynomial interior-point method; Renegar (1988) gave the path-following bound; Vaidya (1989) reduced the per-iteration cost with low-rank updates; Lee and Sidford (2014–2015) reduced the iteration count to ; Cohen, Lee and Song (STOC 2019, J. ACM 2021) reached ; van den Brand (2020) derandomized the result.
Vectors are in and products, quotients and roots of vectors are coordinatewise. For and vectors , means for all ; for a scalar is defined likewise. The number of variables is and has full row rank .
The potential is , evaluated at with ; it is small exactly when every is close to .
StochasticStep (Algorithm 1) takes positive , a direction , a sampling parameter and the output of a data structure with . It rescales to , (), draws a sparse vector with independent coordinates, with probability and otherwise, and computes the step through the projection . The draw is repeated until and are at most ; the output is .
Main (Algorithm 2) sets , , , , starts at , and in each iteration sets , takes the direction
runs StochasticStep, and falls back to a deterministic ClassicalStep whenever .
For every iteration , almost surely Assumption 4.1 holds for the input of iteration (in particular and ), almost surely the resampling loop of iteration succeeds with positive probability, and
The paper writes ; its proof gives the constant .
Lemma A.1 (variance of a product), Lemma 4.12 (properties of ), Lemma 4.2 (explicit step), Lemma 4.3 and Claim 4.7 (moments and success probability of the sampled step), Lemma 4.8 (moments of ), and Lemma 4.13:
Lemma 4.14 is what makes the randomized method usable: the iterates stay in the -neighbourhood of the central path along the whole run, and the expensive fallback is rare enough that its expected cost, , is negligible. The paper's cost bound (Lemma 4.16) and its main theorem rest on it. The same potential-based "stochastic central path" analysis was reused in later solvers, for instance for empirical risk minimization (Lee, Song and Zhang, COLT 2019).
The result is proved in the paper; no machine-checked version exists. A formalization pins down the probabilistic model that the paper leaves implicit (independence of the sampled coordinates, the law of the resampling loop, a data structure and fallback that see only the past) and checks the constants, several of which are tight against printed slack (Remark 4.4).
The running-time claims of the paper (Theorem 2.1's expected time , Lemma 4.16, Section 5) are not part of this mission: they live in an arithmetic cost model that Lean does not have. The accuracy guarantee of Theorem 2.1 (Lemma A.6, ClassicalStep from [57]) is also outside the mission.
The obvious argument would bound each quantity under the product law of the sparse direction. But StochasticStep resamples, so the step actually taken is distributed according to that law conditioned on a success event, and expectations and variances shift. A second difficulty is that is controlled only in expectation, while Assumption 4.1 must hold surely at every iteration; this is reconciled by the deterministic ClassicalStep fallback, which caps at , and by an induction over iterations of under the trajectory law. Claim 4.7 needs a Bernstein inequality, which Mathlib does not yet provide.
Coordinates are Fin n, vectors Fin n → ℝ, a Matrix (Fin d) (Fin n) ℝ with A.rank = d, and the natural logarithm. is written out as ; is stated coordinatewise. The sampled direction has law Measure.pi of two-point laws; the step taken by StochasticStep has that law conditioned (ProbabilityTheory.cond) on the success event, and every , of Lemmas 4.3, 4.8 and 4.13 is under this conditioned law. mp.Query is replaced by its value ; the data structure and ClassicalStep are arbitrary measurable functions , of the history with the only properties the paper uses. The trajectory is Mathlib's Ionescu-Tulcea measure, with kernels equal to the step law of Main. is the number of variables of the program the loop runs on.
Deviations from the page, all recorded in the items: Assumption 4.1 is used with instead of the printed , because Main sets to exactly that value; is instantiated as , the constant of the paper's proof; the conclusions of Lemma 4.14 are stated for every iteration index rather than while ; at the second term of is . No hypothesis is imposed.
A trivializing formalization is ruled out: every statement that integrates against the conditioned law also concludes that this law is a probability measure (so it cannot be the zero measure), the goal concludes that each resampling loop succeeds with positive probability, the oracles , cannot see the coins of the current iteration, and the goal is about the whole iterated process from the initial point, not one step from an arbitrary law.
Contributions welcome: a Bernstein inequality for bounded independent sums, conditional-law lemmas for cond of Measure.pi, and Markov-kernel measurability for the step law; these are reusable beyond this mission.
The neutral theory of molecular evolution holds that much of the genetic variation observed at the molecular level is caused by selectively neutral mutations rather than by selection. To test it against data one needs the distribution of allele frequencies that a neutral model predicts, and in practice that distribution has to be compared with a sample from the population, never with the whole population. Ewens (Ewens 1972) derived the equilibrium distribution of allele counts under the infinite alleles model, now called the Ewens sampling formula; it underlies classical tests of neutrality and appears throughout combinatorics and probability as the law of the cycle type of an Ewens-distributed random permutation and of the Chinese restaurant process.
Chapter 7 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) obtains the infinite alleles model as a limit of the reversible migration processes of Chapters 2 and 6, and uses reversibility to answer questions about allele ages and fixation. The mission formalizes the finite, combinatorial results of that chapter.
Timeline. Kimura and Crow (1964) introduced the infinite alleles model. Ewens (1972) found its equilibrium sampling distribution (7.6). Kingman (1978, J. London Math. Soc.) characterized the consistency of random partitions under sampling, the property Theorem 7.1 asserts for the Ewens family. Kelly (1979, Chapter 7) derived (7.6) as a limit of reversible migration processes, and the consistency and the allele-age results from the reversibility of a labelled population process.
A population consists of individuals, each carrying an allelic type. Its description is , where is the number of allelic types carried by exactly individuals, so that
For a real parameter , the Ewens distribution on descriptions is
where is the binomial coefficient for real . In the infinite alleles model, individuals die at rate , each death is followed by the birth of an offspring of a uniformly chosen survivor, and the offspring is a mutant of an entirely new type with probability ; then (7.6) is the equilibrium distribution with (7.5).
A random sample of size without replacement is a uniformly random -element subset of the labelled individuals, each of the subsets being equally likely; the sample has a description in the same sense.
The number of individuals carrying one given allele performs a random walk on with intensities
An allele is quasi-fixed when it is the only allele present ().
If and the population description is distributed as , then a random sample of size drawn without replacement has description with probability , the same being used for both sizes:
The results. Consistency under sampling is what makes the Ewens formula usable as a statistical model: the predicted distribution for an observed sample does not depend on the unknown population size, only on . Kelly deduces from it the sufficiency of the number of alleles in a sample for and the heterozygosity (Exercises 7.1.5, 7.1.8). The formula (7.9) gives the equilibrium frequency of the oldest allele, and Theorem 7.9 gives the quasi-fixation probability from which the mean time between quasi-fixations follows (Corollary 7.10).
Formalizing them. All four results are classical and proved; none has a machine-checked proof on the platform or in Mathlib as of this writing. The mission produces a reusable formal Ewens distribution over integer partitions, a definition of sampling without replacement by counting labelled subsets, and an absorption probability for an explicit birth–death walk. Proofs independent of Kelly's process argument are welcome.
The book's proof of Theorem 7.1 is a process argument: in a population whose size fluctuates between and , a drop in size acts as a random deletion, and the truncated equilibrium (7.7) restricted to each size gives and . Turning that into a statement about finite sets requires the equilibrium of a truncated reversible process, which is not available here, so a formal proof must either build that process or find a direct combinatorial route. A direct route has to relate, for each description of the sample, the number of -subsets of a labelled population with a given description to products of binomial coefficients, and sum the result against (7.6); the bookkeeping over partitions is where the work lies. Theorem 7.9 needs a solution of the first-step equations of a non-symmetric walk and the identification of that solution with a hitting probability defined as a limit.
Nat.Partition n, with the multiplicity of the part ; the product in (7.6) runs over . The real binomial coefficient is the published definition AppliedComb.GenFun.binomReal.Fin M with allelic types Fin M → ℕ; the description of a labelled set is computed from the labelling. The sampling probability is times the number of -subsets whose restricted labelling has the given description. It is not defined by a formula on descriptions, and a definition that removed individuals one at a time in proportion to class sizes (the book's proof route) is ruled out as a definition because it presupposes the reduction the proof must supply.Contributions of general partition and sampling lemmas (counting subsets with a given description, the generating function identity ) are reusable beyond this mission.
The bullwhip effect is the observation that the variability of orders grows as one moves up a supply chain, from the retailer to the wholesaler, the distributor and the factory, even when customer demand is stable. It was documented in industry practice by Lee, Padmanabhan and Whang (Management Science, 1997), who identified demand forecasting as one of its main causes. Amplified order variability raises the safety stock, capacity and transportation costs of every upstream firm, so the question of how large the effect is, and what reduces it, is central to supply chain management.
Chen, Drezner, Ryan and Simchi-Levi (Management Science 46(3), 2000) quantified the effect for a retailer that forecasts with a moving average and follows an order-up-to policy. Their §3 asks whether sharing customer demand information with every stage removes the effect. Theorem 3.1 (the companion mission of this series) shows that it does not; Theorem 3.2, the goal of this mission, gives the lower bound for the chain in which no demand information is shared.
Time is indexed by the integers . The retailer faces i.i.d. demand
where the error terms are independent and identically distributed from a symmetric distribution with mean and variance .
Single-stage policy (§2). With observations, a lead time , a safety factor and a constant , the retailer forms the moving-average estimates
raises its inventory position to the order-up-to point , and so orders . Orders may be negative: excess inventory is returned without cost.
Decentralized chain (§3). Stages form a serial chain; stage 1 is the retailer, and is the lead time between stages and . No stage sees customer demand except the retailer. Stage forecasts from the orders it receives,
uses the order-up-to point , and orders
For every stage and every period ,
The bound is the paper's, with its explicit constants. The paper asserts no tightness for this theorem, and none is claimed.
For the single-stage policy with any safety factor and any constant ,
This is the i.i.d. case of the paper's Theorem 2.2. With and the single-stage orders are the stage-1 orders of the chain, so Eq. (6) contains the case of the goal.
The result. Theorem 3.2 is half of the paper's comparison between centralized and decentralized information. When demand information is shared, the amplification from the retailer to stage in the i.i.d. case equals (Eq. (8)), which grows additively in the lead times. Without sharing, the lower bound (7) is a product over stages and grows multiplicatively. The paper concludes that centralizing demand information "can significantly reduce the bullwhip effect", and that the gap widens as one moves up the chain. Eq. (6) is the single-stage statement that forecasting with a moving average alone already amplifies variability, by a factor depending only on the ratio .
Formalizing it. The paper gives no proof of Theorem 3.2; it refers to Ryan (1997, PhD thesis) and to Chen et al. (1998). A machine-checked proof would therefore supply the first self-contained, verified argument for the multiplicative bound. The Gaussian special case of Eq. (6) is already formalized on Prove2Me, in the Snyder–Shen chapter on the bullwhip effect (SupplyChainTheory.bullwhip_signal_processing at ); that statement assumes Gaussian errors, whereas this mission assumes only symmetry, mean and variance . Neither the multistage bound nor the symmetric-error version of Eq. (6) has a formal proof.
The natural first idea is induction on the stage: treat the orders of stage as the demand of stage and apply the single-stage bound. That step fails, because the single-stage bound is a statement about i.i.d. demand, and the orders reaching stage are not i.i.d.: they are autocorrelated, and stage 's moving average of those orders interacts with the correlation in a way that can raise or lower the variance. Whether the product bound survives depends on controlling that interaction at every stage. For Eq. (6), the safety-stock term is a nonlinear function of the demands, and only symmetry of the errors, not normality, is available to control its interaction with the linear part of the order.
All objects live in the namespace ChenBullwhip.Decentralized.
IIDDemand P is the demand model on a probability space : a constant mu, sigma > 0, and errors eps : ℤ → Ω → ℝ that are measurable, mutually independent (iIndepFun), identically distributed, symmetric (eps t and -eps t have the same law), in , with mean and variance sigma ^ 2. Demand is D t = mu + eps t. Variances are Mathlib's ProbabilityTheory.variance.SingleStage defines , , , and of §2; is a free real parameter, as the paper does not fix it.Chain defines the forecasts and the orders by recursion on the stage, with the convention , so that stage 1 orders . The recursion is not printed in the paper; it is the §2.2 order identity applied to a stage whose incoming demand is , as the sequence of events on p. 440 describes.Disclosed hypotheses not on the page: (a moving average needs an observation), (the paper divides by ), and square-integrable errors (Mathlib's variance is off ). The paper's model (1) asks ; since affects no variance, no sign condition is imposed. Lead times are natural numbers. The statements hold in every period , with no stationarity hypothesis.
Trivializing formalizations are excluded: the orders are computed from the demands, not posited processes with a given covariance; the variances are genuine because every random variable involved is square integrable; and the ratio's denominator is .
A complete development needs variance and covariance calculus for finite linear combinations of independent variables, and, for Eq. (6), the vanishing of the covariance between an odd and an even function of a symmetric random vector. Both are reusable well beyond this mission. Proofs of either target, and general lemmas on variances of linear filters of i.i.d. sequences, are welcome.
SupplyChainTheory.*).A disjunctive normal form (DNF) is a disjunction of terms, each term a conjunction of Boolean literals. An unambiguous DNF has pairwise disjoint terms: no Boolean assignment satisfies two different terms. This restriction makes several tasks easy. In particular, the cited open-problem entry records polynomial-time algorithms for weighted satisfiability on unambiguous DNFs and for unweighted falsifiability. The unresolved boundary is weighted falsifiability: can one find a high-weight assignment outside the union of the terms, without enumerating all assignments?
This question is relevant to the complexity of negating compact representations of Boolean functions. Amarilli's entry observes that, since unambiguous DNFs are d-DNNFs, a polynomial-time negation procedure for d-DNNFs would yield a polynomial-time solution to weighted falsifiability on unambiguous DNFs by applying weighted satisfiability to the negated representation. Conversely, if weighted falsifiability for unambiguous DNFs—or even for d-DNNFs—is NP-hard, then, unless , d-DNNFs cannot be negated in polynomial time. These are implications stated by the source, not results established by this mission.
The question appears on Albertine Amarilli's open-problem list. The entry cites a Theoretical Computer Science Stack Exchange question by Mikaël Monet and credits him with helping prepare the entry. It records two partial tractability results: weighted satisfiability with binary weights, and weighted falsifiability when the variable weights are unary. The entry gives no date for when the problem was posed or last seen open, so this description does not assign one. The linked discussion is useful context, not a novelty or resolution certificate.
Let be exactly the variables occurring in the DNF. The formal input declares this finite universe by its size ; validity requires every declared variable to occur in at least one literal. An input DNF is a finite list of terms, and each term is a finite list of signed variable indices. An assignment is a function . A positive literal is true when ; a negative literal is true when . A term is true when all its literals are true, and the DNF is true when at least one term is true. Thus the empty DNF is false and an empty term is true.
The input also contains one positive integer weight for each variable and a positive threshold . The weight of an assignment is
The DNF is valid for this problem when every literal index is below and every pair of distinct terms is mutually unsatisfiable. The decision question is whether there exists an assignment that falsifies the DNF and has weight at least .
For valid unambiguous DNF inputs with positive binary-encoded weights and threshold, the decision problem asking whether a satisfying assignment has weight at least has a deterministic polynomial-time algorithm. This is the weighted-satisfiability baseline recorded in the source entry. It is a separate result from the goal below.
For the same valid DNF model, when each variable weight is encoded in unary, weighted falsifiability has a deterministic polynomial-time algorithm. The threshold remains binary-encoded in this formalization. The source entry records this unary-weight restriction as tractable.
For arbitrary positive binary-encoded variable weights and a positive binary-encoded threshold, determine whether one fixed deterministic Turing machine and one polynomial time bound decide weighted falsifiability for every valid input. The machine must be correct on all valid instances; its running-time bound is uniform and measured in the length of the explicit input code. No witness output is required.
The two partial results are reference points, not assumptions from which the goal is claimed to follow. The goal is the open binary-weight case; it must not be replaced by the satisfiability problem or by the unary-weight restriction.
Input, semantics, validity, and serialization definitions
├── binary-weight weighted satisfiability (source baseline)
├── unary-weight weighted falsifiability (source baseline)
└── binary-weight weighted falsifiability (open goal)
Each branch shares the same finite DNF model and correctness predicates. The arrows indicate required definitions and scope, not a claim that either partial theorem implies the open goal.
A positive result would give a uniform algorithm for finding whether a disjoint union of Boolean subcubes omits any sufficiently heavy point, even when weights are represented compactly in binary. A negative complexity result would identify a sharp obstruction to efficient complement-related operations on these representations. The exact-weight version (asking for weight exactly ) is a different problem and is outside this mission's scope; the goal here is specifically weight at least .
Formalizing the question fixes the universe of variables, signed-literal semantics, unambiguity condition, threshold direction, input encoding, and computational model. It also makes the unary and satisfiability baselines comparable to the binary-weight goal without treating a finite search or a candidate implementation as a complexity proof. No solution is supplied or presumed here.
The direct search over all assignments is exponential in . Counting satisfying assignments is enough to settle ordinary falsifiability, but a weighted threshold partitions assignments by exponentially many possible total weights when the weights are binary. The unary dynamic program therefore does not by itself give a polynomial bound in the binary input length. Conversely, solving weighted satisfiability on the DNF does not answer whether a heavy assignment lies outside it. The task is to settle that gap without silently replacing binary magnitude by unary size.
The Lean model uses Input, an explicit variable count, a list of signed-index terms, a weight list, and a threshold. validInput requires exactly one positive weight per variable, positive weights and threshold, in-range literal indices, that every declared variable occurs in the formula, and pairwise unsatisfiable distinct terms. The finite assignment type is Fin n → Bool; unused variables remain part of the input. The decision predicate is existential and exact.
The binary code includes the variable count, every list count and delimiter, all signed indices, all weights, and the threshold. Natural-number payloads use canonical binary digits with an explicit unary length prefix. The unary-weight code changes only the variable-weight payloads to unary; formula data and threshold remain binary. The complexity statements use Mathlib's bundled deterministic Turing.TM2ComputableInPolyTime model, with a single machine and polynomial bound in the chosen code length. This formalization does not claim refinement to JSON, CPython, or any runtime implementation. Human review should check the encoding/decoder round-trip and the source correspondence before launch.
The reusable definitions are the finite DNF semantics, weighted assignment score, validity predicate, binary/unary encoders, and exact decision predicates. Formalizing the two cited partial results is part of the mission's milestone path; neither is evidence that the binary-weight goal is solved.
Many queues observed at well-chosen instants are Markov chains on the nonnegative integers. For the single-server queue with Poisson arrivals and general service times (M/G/1), D. G. Kendall showed in 1951 that the number of customers left behind at successive departure epochs is such a chain, the imbedded Markov chain (Kendall 1951; Kendall 1953). Whether the queue settles into a steady state, keeps returning to empty without settling, or grows without bound is then a question about this chain: is it ergodic, null recurrent, or transient?
F. G. Foster's 1953 paper (doi:10.1214/aoms/1177728976) answers this question by first proving general criteria for an irreducible chain on , stated as solvability conditions for linear inequalities in the transition matrix, and then applying them to the M/G/1 and GI/M/1 chains. Theorem 2 of the paper is the drift condition now known as Foster's criterion, the starting point of the Lyapunov-function method for the stability of queues and stochastic networks (Meyn and Tweedie 2009). This mission is the M/G/1 half of the paper.
Timeline:
A Markov chain on the states is given by a transition matrix : and for every row . Write for the probability that the chain started in first reaches (for , first returns to ) at step . The chain is irreducible if every state can be reached from every other, and aperiodic if for every state the return times have greatest common divisor . A state is recurrent if and transient if ; a recurrent state is ergodic (positive recurrent, "recurrent-nonnull") if in addition its mean recurrence time is finite. The mean first-passage time from to is .
The M/G/1 matrix is built from a sequence of positive numbers summing to one ( is the probability of arrivals during one service):
that is, and, for , when and otherwise. The traffic intensity is
the mean number of arrivals per service.
The goal leaves arbitrary apart from positivity and normalization; in particular is allowed and falls in the transient case.
The result. The classification is the stability theorem for the M/G/1 queue: for the departure-epoch queue length has a stationary distribution, which is what the Pollaczek–Khinchine formula describes; for the queue empties infinitely often but has no steady state; for it grows without bound. The general criteria behind it (Theorems 2, 4, 5) apply to any chain on the nonnegative integers and are reused in the companion GI/M/1 mission and throughout queueing and Markov-chain stability theory.
Formalizing it. All results here are proved on paper (Kendall and Foster, 1951–1953, with Theorems 3 and 7 classical lemmas from Feller). None of them is known to have a machine-checked proof against a Lean development of countable-state Markov chains. The mission produces such proofs on the published discrete-chain vocabulary (transition matrices, first-passage probabilities, return probabilities, positive recurrence), together with the general Foster criteria as reusable theorems. Theorem 2 is already posed as an open platform theorem and is reused here.
The queue-specific part of the argument is short once the general criteria are available; the weight of the mission is in those criteria. They relate qualitative properties of an infinite chain (ergodicity, recurrence, transience) to solvability of infinite systems of linear inequalities, and this needs limit behaviour of the -step probabilities and of hitting probabilities of state , none of which follows from finite-state arguments. Two further points resist the naive approach. The converse directions (ergodic , recurrent ) need exact identities for mean first-passage times, not just bounds, and these must be handled in because the means may be infinite. And the boundary case (null recurrence) separates the two equivalences: an argument that only compares the mean drift with , such as a law of large numbers for the increments, cannot tell recurrence from transience there.
QueueingFundamentals.Foundations.TransitionMatrix (entries P.p i j, rows summing to as a HasSum), with its firstPassage, returnProb, Irreducible, Aperiodic and PositiveRecurrent. "Ergodic" is P.PositiveRecurrent; aperiodicity is the paper's standing assumption and is not folded into it a second time.i ≠ 0.mg1Matrix k : ℕ → ℕ → ℝ; the goal and the §3 display quantify over every TransitionMatrix P with P.p = mg1Matrix k. Such a P exists for every admissible k (checked in a sorry-free local file for ).Summable or HasSum); Theorem 3's equation (6) is written as in together with finiteness of the , .Ruled out: as a real tsum (which is for a divergent series and would call a heavy-tailed chain ergodic); defining "ergodic" or "recurrent" through the existence of Lyapunov or drift functions (which would make the criteria tautological); a goal over a matrix that need not exist.
Contributions welcome: proofs of the general criteria (Theorems 2–5) on the published chain vocabulary, the limit theorem for irreducible aperiodic chains, first-step analysis for hitting times, and Theorem 7 as a lemma on probability generating functions; all of these are reusable beyond this mission.
Temporal-difference (TD) learning estimates the value function of a Markov chain — the expected discounted sum of future rewards from each state — from a single stream of observed transitions, without knowing the transition probabilities. With a linear function approximator the value of state is represented as for a feature vector and a parameter . Classical TD() updates by stochastic approximation, and its behaviour depends on a step-size schedule that must be tuned.
Bradtke and Barto (Machine Learning 22, 1996) replaced the stochastic-approximation update by a least-squares solve: LS TD (Eq. (11)) recomputes at every step as the instrumental-variable least-squares solution of the empirical consistency condition. The method, later generalized as LSTD() by Boyan (Machine Learning 49, 2002), is the basis of least-squares policy iteration and of the "LSTD" methods in standard reinforcement-learning texts (Sutton and Barto, Reinforcement Learning, 2nd ed., 2018, §9.8). Its appeal is that it has no step size; the question this mission formalizes is whether it nonetheless converges, with probability one, to the true parameter.
Timeline. Sutton (1988) introduced TD(). Watkins and Dayan (1992) and Tsitsiklis (1994) proved probability-one convergence of tabular TD(0) and Q-learning. Bradtke and Barto (1996) proved probability-one convergence of LS TD on absorbing chains (Theorem 1) and on ergodic chains (Theorem 2). Tsitsiklis and Van Roy (IEEE TAC 42, 1997) proved convergence of linear TD() with general features on ergodic chains.
A finite Markov chain on a finite nonempty set is a matrix with and . A transition earns reward ; the expected reward out of is . For a discount factor the value function is
The chain is ergodic (Kemeny and Snell) if every state can be reached from every state: for all there is with . An invariant distribution is a probability vector with ; write .
Each state has a feature vector ; is the matrix with rows . The true parameter is a vector with for all .
The algorithm (Figure 3) starts at an arbitrary state , lets the chain move , and after transitions computes
the sums running over the transitions observed so far.
If is ergodic, (1) is linearly independent, (2) each has dimension , and (3) , then is finite and, from any initial law,
The goal leaves the chain, the rewards, the features and the initial law arbitrary.
The result. Theorem 2 shows that an LS TD learner running on one long trajectory recovers the exact value function whenever the features can represent every function on the states, with no step-size schedule. It is the step-size-free counterpart of the tabular TD(0) convergence theorems and the starting point for the later analysis of LSTD with fewer features than states, where the limit is the TD fixed point rather than . Lemma 5 is the general identification of that fixed point as the almost-sure limit of LSTD.
Formalizing it. The result is proved in the paper; it has not been machine-checked. A formalization adds three things the paper delegates: the strong law of large numbers for occupation times of a finite irreducible Markov chain, which the paper cites to Kemeny and Snell and which is not in Mathlib; the per-state transition frequencies used in the first sentence of the proof of Lemma 5; and the linear algebra of the limit. The first is reusable well beyond reinforcement learning.
The algebra is short once the empirical averages in (11) are known to converge. The difficulty is probabilistic: the averages are over a dependent sequence, so the ordinary strong law of large numbers does not apply. Two facts are needed: that the fraction of time in each state converges to almost surely for any starting law, including periodic chains, where itself does not converge; and that, among the visits to , the fraction followed by a move to converges to , which needs the strong Markov property at successive visit times. Neither follows from convergence of the chain's distribution, and neither holds for a chain started at a fixed state without an argument that every state is reached.
X with Fintype, DecidableEq, Nonempty, a row-stochastic matrix P : Matrix X X ℝ (structure Chain), rewards R : X → X → ℝ, features φ : X → Fin m → ℝ. Condition (2) is m = Fintype.card X; condition (1) is LinearIndependent ℝ φ.tsum is on a divergent series, so "θ* is finite" is stated as convergence of the series together with existence of with . is existential, never defined as Lemma 5's limit.Needed infrastructure: the strong law for occupation times of a finite irreducible chain under an arbitrary initial law (milestone 1), the strong Markov property at visit times, positivity of the invariant distribution of an irreducible chain, and the invertibility of for . Contributions to any of these, as standalone lemmas, are welcome.
A supplier who sells to a retailer at a per-unit wholesale price above her own production cost induces the retailer to order less than an integrated firm would. This effect, double marginalization, goes back to Spengler (1950) and is the standard benchmark against which supply chain contracts are judged: a contract coordinates the channel if it makes the decentralized decisions coincide with the integrated optimum. Revenue-sharing contracts, as used in the video-rental industry, coordinate the channel; the plain wholesale-price contract does not. Whether a supplier should bother with the administrative cost of revenue sharing depends on how much the wholesale-price contract actually loses and how much of the remaining profit the supplier keeps.
Cachon and Lariviere answer that question for a retailer whose revenue depends only on the quantity ordered, in Section 4.1.1 of their working paper Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations (June 2000; the 2005 Management Science version renumbers and revises the material). They show that the answer is governed by the curvature of the marginal revenue curve, and they compute it exactly for a one-parameter family. The source is the June 2000 working paper, whose results are unnumbered; every item cites its section, page and display.
A supplier produces at unit cost and sells to a single retailer. The retailer's expected revenue from units is , where , is strictly concave and differentiable on with derivative (the marginal revenue), is differentiable on with derivative , the product is viable (), and a finite quantity is optimal ( for some ). The supply chain profit is ; the integrated quantity maximizes over .
Under a wholesale-price contract with price , the retailer orders to maximize . Each order is induced by exactly one price, , so the supplier can be thought of as choosing . Her profit, the retailer's profit, and their sum are then
Following the paper, is assumed decreasing, which makes unimodal. The supplier's optimal quantity to induce maximizes over , and is her optimal wholesale price. The efficiency of the contract and the supplier's profit share are
In the α-family, for and , so : marginal revenue is convex for , linear for and concave for .
For and , the quantities and are the unique maximizers of and on , the profit share is , and
a quantity that does not depend on , is strictly increasing in , tends to as and to as .
The general milestones turn the paper's area argument (the triangle under the tangent to marginal revenue at ) into three comparisons: convex marginal revenue makes the wholesale-price contract worse for the chain and leaves the supplier at most two thirds of a smaller pie, concave marginal revenue the opposite. The α-family makes the trade-off exact: efficiency never falls below , while the supplier's share moves much faster than efficiency, which is the paper's argument for why revenue sharing is most attractive when marginal revenue is convex.
These results are proved on paper but, to our knowledge, not machine-checked anywhere; Mathlib has no supply chain contract theory. The formalization provides a reusable single-retailer wholesale-price model, a checked version of the convex/concave tangent comparisons, and a corrected statement of the α-family's monotonicity (see the scope section).
The general comparisons are short on paper but rest on a picture: they need the first-order condition at an interior maximizer, the tangent-line inequality for a convex or concave derivative, and the fundamental theorem of calculus for a function whose derivative is known only on a half-line and one-sided at . Strictness needs a strictly positive integrand on a nondegenerate interval.
The α-family is where the analysis is not routine. The closed forms involve real powers with exponents and , which must be combined carefully. The limit as is classical, but the monotonicity of on all of is not a one-line derivative sign check: the derivative mixes with rational terms, and its sign has to be established uniformly near and near .
Quantities and prices are real numbers. "Optimal" always means a maximizer over all admissible quantities (IsMaxOn on , or on in the α-family, as the page restricts), never a root of a first-order condition. The derivative of the general model is linked to by a one-sided derivative hypothesis on ; is required only on , since for it blows up at . In the α-family the marginal revenue is deriv of , not a separate function, and is assumed (implicit on the page: and ). Efficiency and profit share are real divisions; their denominators are positive at the optimal quantities.
Deviations from the page, all disclosed in the items:
A trivializing formalization is ruled out: the efficiency in the goal is the ratio of profits computed from at the maximizers, not a definition equal to , and the maximizers are characterized as unique argmaxes rather than assumed.
Welcome contributions: proofs of the general tangent comparisons, which are reusable for any concave revenue model; the real-analysis lemmas on ; and the α-family closed forms.
Impulse control models an agent who acts on a random system through discrete interventions, each with a fixed cost: inventory replenishment, cash management, exchange-rate interventions by a central bank. With two agents whose objectives conflict, the problem becomes a nonzero-sum stochastic differential game with impulse controls. Before the work of Aïd, Basei, Callegaro, Campi and Vargiolu (Math. Oper. Res. 45(1), 2020; preprint arXiv:1605.00039), such games had no general verification theorem and few explicit equilibria; the paper supplies both. Its main application, formalized in this mission, is a game between two central banks with different targets for an exchange rate, a two-player version of the exchange-rate control models of Bertola, Runggaldier and Yasuda and of Cadenillas and Zapatero (references [10], [12] of the paper). The paper proves that this game has an explicit one-parameter family of Nash equilibria of threshold type, with closed-form payoffs.
The state is a real process. Without interventions it is , where is a standard real Brownian motion and . Player 1 may shift it up by impulses , player 2 down by impulses :
Player 1 earns the running payoff , player 2 earns , with . An impulse costs its author and pays the opponent . Payoffs are discounted at rate . The standing assumptions are , , and .
A strategy of player is a pair : an open continuation region and a continuous impulse map . Player intervenes when the state leaves , applying the impulse ; player 1 has priority when both want to act. This rule defines the controlled process and the interventions inductively. Player 's payoff is
A pair is -admissible, , when these random variables are integrable, has all moments, and neither player's interventions accumulate in finite time. A Nash equilibrium is an admissible pair from which no player gains by deviating to any strategy that keeps the pair admissible.
The explicit objects are , and
From the zero of and a free parameter , the formulas (4.20)–(4.21) give thresholds , targets , coefficients , the functions and the piecewise candidates of (4.6). These are linear outside and equal inside.
For every and every initial state , the threshold strategies
form an -admissible Nash equilibrium, and
Milestones 1–3 are deterministic real analysis; milestone 4 and the goal are probabilistic.
The result gives explicit equilibria, with explicit thresholds and payoffs, for a nonzero-sum stochastic game with impulse controls. Such games rarely have closed-form solutions. The equilibria form a continuum indexed by : equilibrium payoffs are not unique, and every equilibrium in the family is a translate of a fixed interval policy. The explicit formulas also support the comparative statics of Section 4.4, where the continuation region widens as the fixed cost grows.
Proposition 4.7 is proved in the paper by applying its verification theorem (Theorem 3.3) to . The admissibility estimate (4.26) is written out only for initial states ; the general case is said to be similar. As far as is known, none of these results has a machine-checked proof. A formal proof would check every regularity, pasting and admissibility condition. It would also yield a reusable pathwise construction of impulse-controlled Brownian motion.
The deterministic milestones need careful algebra with nested logarithms and square roots. Proving Lemma 4.6 requires the global shape of , which needs the sign pattern of from Proposition 4.2, not only local conditions at the thresholds.
The goal is harder. The Nash inequality must hold against every admissible deviation: any open continuation region and any continuous impulse map, not only threshold strategies. Comparing payoffs therefore needs a verification argument, namely Itô's formula for a function that is only piecewise and across the thresholds, applied along a process with an unbounded number of jumps, plus a localisation that uses the moment condition (2.8). Admissibility needs a renewal-type bound on the discounted number of interventions, built from i.i.d. exit times of Brownian motion from an interval.
The Lean development lives in the namespace ImpulseGames.LinearGame.
Model with the proposition Model.Standing. The added hypothesis appears in every statement that uses : with , which the standing assumptions allow, has no zero in and the family (4.20) does not exist.IsBrownianReal W P on a probability space, with time in . Definition 2.2 is formalized pathwise: exit times in with , the tie rule favouring player 1, and for the tail of each impulse control. No SDE or stochastic integral appears in any statement; the uncontrolled dynamics are .Two slips of the page are corrected. First, the paper's impulse maps are not -valued on all of ; they are replaced by and , which agree with them wherever each player acts. Second, in Lemma 4.6 the maximiser (4.23) is not unique when , in the opponent's intervention region (all impulses tie there). The statement asserts maximality everywhere and uniqueness outside that region.
A complete development needs: elementary real analysis for milestones 1–3; a pathwise theory of piecewise-defined processes; an Itô formula for Brownian motion with , piecewise- functions; and exit-time estimates for Brownian motion. The last two are reusable well beyond this mission. Proofs of the deterministic milestones are welcome independently of the stochastic part.
Sequential decisions often change the distribution of future states. A planner choosing an action today must account for both its immediate reward and the later rewards made possible by the resulting state. The mathematical question is whether an optimal rule can be chosen once and reused at every stage, even when a competing plan may randomize and use the entire observed history. In Discounted Dynamic Programming, Blackwell studies this question on general Borel state and action spaces, beyond the finite models in which a direct comparison of actions is available.
The paper distinguishes several strengths of optimality. For each distribution of the initial state, an approximately optimal stationary plan exists, but a single plan that is approximately optimal at every initial state need not exist in a general Borel problem. Essential countability of the actions restores uniform approximate stationary optimality; essential finiteness yields exact stationary optimality. These are different mathematical claims, and the mission keeps their different quantifiers visible. Blackwell 1965, pp. 227, 229, 232–234.
A state is an element of a nonempty standard Borel space , and an action is an element of a nonempty standard Borel space . The transition kernel gives a probability distribution for the next state after action in state . The reward may depend on that next state ; it is bounded and Borel measurable. Future rewards are discounted by with . These are the objects of Blackwell’s Sections 2–3. Blackwell 1965, pp. 227–228.
A plan assigns a probability distribution of actions to each possible history before a decision. At stage , that history contains completed state-action pairs and the current state. Thus plans may randomize and depend on earlier states and actions. A Markov plan instead uses a Borel function at each stage; a stationary plan uses the same function at every stage and is denoted . Starting from state , the plan has discounted expected return
Here and are the state and action at stage . The comparison class for an optimal plan is all such plans, including randomized and history-dependent ones. Blackwell 1965, pp. 228–229.
Two actions are equivalent at state when they have the same reward for every next state and the same transition measure . An action set is essentially countable by a Markov plan if, for every , one of the actions is equivalent to at . It is essentially finite by that plan if has a countable Borel partition such that, for , one of is equivalent to every action at . A finite action set is a special case. Blackwell 1965, pp. 233–234.
For a probability distribution on and , -optimality asks for a stationary with
Theorem 6(b) asserts that such an always exists. Under essential countability, Theorem 7(a) obtains a stronger, uniform -optimality statement: for every there is a stationary with for all . Its other targets identify the optimal return with the fixed point of the operator and with the unique bounded solution of the optimality equation . Blackwell 1965, pp. 232–234.
The mission’s goal is Theorem 7(b). Under essential finiteness, it asks for a stationary with exact optimality:
The milestone list also includes the paper’s operator identity, approximate selection result, contraction criterion, generated-plan comparison, and upper-bound criterion. Each has its own source index and statement. Blackwell 1965, pp. 231–234.
The exact result says that, under a condition weaker than a globally finite action set, repeated use of one measurable state-based rule matches or exceeds the return of every adaptive randomized plan. It is a structural result about what information and randomization can add to discounted control. The preceding approximate results specify what can still be guaranteed when that condition is relaxed; Blackwell’s examples show that the distinctions cannot simply be ignored. Blackwell 1965, pp. 229–230, 234.
Blackwell proved these statements in 1965. The formalization work here is to give machine-checked proofs for the Borel-space model and its full comparison class, together with reusable definitions of history-dependent kernels, returns, stationary rules, and Bellman operators. The draft theorem statements compile as Lean declarations, but their proofs remain open. The milestone results are intended to make both the final theorem and its supporting measure-theoretic objects independently usable.
On an uncountable Borel action space, the pointwise supremum of available action values does not automatically come with a Borel action selector. Choosing a maximizing action separately at each state may fail to define a measurable rule, and a supremum need not be attained. Also, a Markov or stationary comparison cannot by itself certify optimality against plans that depend on full histories. These issues are real in the paper’s examples: general Borel problems may lack an -optimal plan, and a given plan need not be uniformly approximated by a Markov plan. Blackwell 1965, pp. 229–230.
The Lean model uses nonempty StandardBorelSpace types for and . “Baire function” is read as Borel measurable on these metrizable spaces. The problem stores a Markov transition kernel, a bounded measurable real reward on , and ; is included. A plan contains a probability kernel on each finite history, and the return is the actual absolutely convergent series of expected one-stage rewards. The first decision is indexed by in Lean, corresponding to the paper’s index . The finite history law is assembled through kernel composition products, and a stationary rule is represented by deterministic kernels. The integrals and series therefore express the paper’s expected return, including the cases where the reward depends on the next state.
For the operator results, means bounded and measurable real functions. The suprema defining and the optimal return are real suprema over nonempty families bounded by the reward and discount; they are used only in that setting. The abstract operator in Theorem 5 maps into itself. The action equivalence predicate uses the paper’s explicit equality of reward functions and transition laws; the later “i.e.” phrasing on p. 234 is weaker when interpreted as equality of operators alone. A partition piece may be empty, and Lean’s piece corresponds to the paper’s , with rules .
An optimality claim here always compares with every randomized history-dependent plan. Restricting that quantifier to Markov or stationary plans would trivialize the target. A complete development needs measure-theoretic facts about history laws and their bounded integrals, the discounted series, measurable partitions and selections, and the sup-norm contraction of bounded Borel functions. The history-law and bounded-function infrastructure can be reused outside this mission. Contributions to those foundations and to the numbered milestone theorems are welcome.
In network design games, selfish users build a shared network and split the cost of every edge among the users of that edge. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 38 (2008), DOI 10.1137/070680096) studied the fair connection game, in which the cost of an edge is shared equally (the Shapley value) among its users. In this game the worst equilibrium can cost times the optimum, so the relevant measure is the price of stability: the ratio between the cheapest pure Nash equilibrium and the optimal centralized design. Their Theorem 2.1 bounds it by the harmonic number in every directed graph, and that bound is tight for directed graphs.
For undirected graphs the paper notes that is not tight and calls the correct bound "an interesting open problem". Its Section 4 settles the smallest case: two players with a common terminal. The general theorem gives there; Claim 4.1 improves this to , and a three-node example shows that is the right value.
Timeline. Rosenthal (1973) showed that congestion games have pure Nash equilibria through a potential function. Anshelevich et al. (FOCS 2004; journal version 2008) introduced the price of stability for the fair connection game, proved the bound and the two-player undirected bound treated here. Subsequent work studied the undirected multi-player case, which remains without a matching upper and lower bound in general.
Let be a finite undirected simple graph, with a cost on every edge . There are two players, a common terminal and personal terminals . A strategy of player is a set of edges that connects with : in the graph , and lie in the same connected component. A profile is a pair of strategies.
Under fair cost sharing each edge is paid for equally by the players using it. With the number of players whose strategy contains , player pays
A pure Nash equilibrium is a profile in which no player can lower its payment by switching to another strategy while the other player's strategy stays fixed. The total cost of a profile is the cost of the network it builds,
For a set of edges write . For a profile , the quantities , and split the total cost into the private and the shared parts.
The game is an instance of a congestion game, with per-user latency on edge ; the mission builds on the published congestion-game layer CongestionPoA.AsymSum.Model.
If the game has a profile, then some pure Nash equilibrium satisfies
Moreover, in the three-node example (nodes , edges of cost , edge of cost , with ) the cheapest pure Nash equilibrium costs exactly and the optimum costs exactly , so the ratio approaches .
The result shows that the price of stability of fair cost sharing depends on the network: the bound, tight for directed graphs, is not tight for undirected ones even with two players. It is the first undirected bound below and the starting point for the later study of undirected fair network design, where the question for many players is still open.
The theorem is proved in the paper; this mission formalizes it. A search of the Prove2Me library found no formalization of the price of stability of fair connection games. Beyond the theorem itself, the mission produces a reusable undirected layer over the congestion-game library: connectivity strategies stated with Mathlib's graph reachability, fair cost sharing as a congestion game, and the total-cost functional. A checked proof of the potential inequality (4.1) is the two-player case of the potential argument behind Theorem 2.1.
The obvious argument starts from an optimal solution, follows improving moves to an equilibrium and compares potentials. For two players this only yields the factor : the potential counts shared edges with weight , so a potential inequality alone cannot rule out an equilibrium in which both players share expensive edges. The improvement to needs a second inequality, (4.2), obtained from a specific deviation of each player in the equilibrium, and that deviation is valid only because of the undirected structure: the private parts of the two optimal paths together connect with , and the deviating player can then follow the other player's equilibrium route to . Making this connectivity claim precise for edge sets rather than drawn paths is where the formal work lies. It holds when the optimal strategies are inclusion-minimal, which is why the deviation milestones carry that hypothesis.
Fintype with decidable equality; edges are unordered pairs Sym2 V; the graph is a SimpleGraph V. Edge costs are a real function c with 0 ≤ c e for every e.i : Fin 2 (the paper's players 1 and 2 are 0 and 1) is a Finset of edges contained in G.edgeSet such that t i and s are Reachable in SimpleGraph.fromEdgeSet. Strategies are not restricted to paths.CongestionGame from CongestionPoA.AsymSum.Model with latency ; profiles, player costs and pure Nash equilibria are that library's IsProfile, cost and IsPureNash.Contributions welcome: a proof of the potential inequality (finite improvement paths in the two-player fair game), the graph-theoretic lemma that the symmetric difference of two simple paths with a common endpoint connects their other endpoints, and a computation of the three-node example.
Dynamic programming (DP) solves sequential decision problems by backward recursion: compute the optimal cost of the last stage, then of the last two stages, and so on. For problems with finitely many states and controls and real-valued costs, the recursion obviously gives the optimal cost. Applications are rarely like that. Control spaces are continuous, costs can be unbounded or infinite, the criterion can be multiplicative (risk-sensitive exponential cost) or worst-case (minimax), and the set of policies is an infinite product of function spaces. In this setting the DP recursion can fail to produce the optimal cost.
Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996), Part I, separates the order-theoretic content of DP from the measure theory. It works with an abstract monotone mapping that covers deterministic, stochastic, multiplicative-cost and minimax problems at once, following Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15 (1977). Chapter 3 answers the finite-horizon questions: when does the DP algorithm give the -stage optimal cost, and when do optimal or nearly optimal policies exist? This mission is the first of a series formalizing the book. Later chapters (contraction models, monotone increase and decrease models, the Borel models of Part II) are built on the model fixed here.
Let (states) and (controls) be sets, and for each let be a nonempty control constraint set. Write and let be the set of all functions , ordered pointwise. A mapping is given, subject to the Monotonicity Assumption: implies for all , .
A selector is a function with for all . A policy is a sequence of selectors. Define
and let be the -fold composition of . A terminal function with for all is fixed. The -stage cost of and the -stage optimal cost are
A policy is uniformly -stage optimal if each tail is -stage optimal, and -stage -optimal if where and where .
The three conditions on used in the chapter are F.1 (continuity of along nonincreasing sequences with ), F.2 (there is with for all ), and F.3 (a quantitative selection property with a constant ).
Under F.1, if for all and ; or under F.2, if for all and :
and under F.2, for every there is with .
The identity says that an infimum over an infinite-dimensional policy space equals nested one-dimensional infima. Every numerical use of finite-horizon DP depends on it, and so do the infinite-horizon results of later chapters, which pass to the limit in . Corollary 3.3.1 and Proposition 3.4 give the existence of optimal policies, and Propositions 3.6 and 3.7 verify the abstract hypotheses for two models outside standard expected additive cost.
These results are proved in the book; none of them is formalized. Mathlib has no abstract DP model, and the platform's finite-horizon results (Bertsekas, Dynamic Programming and Optimal Control, Prop. 1.3.1 and the minimax DP algorithm) assume finite disturbance and constraint sets and real costs. They are special cases, not this theory. The finite-horizon results of the 1977 paper (Lemma 3.1 here, on compact sublevel sets, and Corollary 3.1.1, the F.1′ case) are already posed on the platform and are not posed again.
The obvious argument interchanges the infimum over policies with the composition of operators: . The inequality follows from monotonicity alone. The reverse inequality is the content. Taking a near-minimizing selector at each stage requires either passing a limit inside (F.1) or bounding how errors at later stages propagate through (F.2, F.3). Both steps break at infinite values. With there may be no -optimal policy at all (Counterexample 4 of the book). Without F.1 or F.2 the identity itself fails (Counterexamples 1–3). A proof must therefore track separately the states where the optimal cost is , which is why F.3 and the definition of -optimality have two cases.
The model is a structure Model S C with fields U, U_nonempty, H : S → C → (S → EReal) → EReal and the monotonicity proof. Policies are ℕ → Selector, with selectors as a subtype of S → C. is m.T^[N], and is a recursion that applies first. All values lie in EReal. The book's convention never arises in Propositions 3.1–3.4, which only add real numbers to extended reals. The minimax and multiplicative mappings implement it explicitly (badd, and an expectation that returns when the positive part diverges). Every theorem assumes and . Assumptions F.1–F.3 are predicates on the model. F.2 is also available with a named constant (F2With) so that Propositions 3.6 and 3.7 can carry the book's constants and .
is defined as an infimum over policies of the composed operators, never through , so the goal is not true by definition. A formalization in which already contains an infimum over controls would make Proposition 3.1 hold by rfl, and this one rules that out.
Proving the goal needs elementary EReal order arithmetic, iterated infima over subtypes, and pointwise selection of near-minimizers via choice. Proposition 3.6 additionally needs monotone and dominated convergence for countable sums in ℝ≥0∞. The model and operator definitions are reusable by the later missions of the series (contraction, monotone increase and decrease models). Proofs of any milestone, and reusable EReal lemmas about shifting by real constants, are welcome.
Iterative methods for optimization and equation solving on a smooth constraint set (orthogonal matrices, fixed-rank matrices, spheres, Stiefel and Grassmann manifolds) compute an update vector in the tangent space at the current iterate and then have to return to . The Riemannian exponential map does this along geodesics, but computing it means solving an ordinary differential equation. The notion of retraction, introduced by Adler, Dedieu, Margulies, Martens and Shub (IMA J. Numer. Anal., 2002) and developed in the book of Absil, Mahony and Sepulchre (Princeton, 2008), captures what such a return map needs for Newton's method to keep its local quadratic convergence and for gradient methods to converge: smoothness, , and first-order agreement with the exponential.
Absil and Malick (SIAM J. Optim., 2012; HAL hal-00651608v2) give a general recipe for building retractions on submanifolds of a Euclidean space: move tangentially from to , then come back to along a prescribed family of admissible directions. This mission formalizes that recipe, Theorem 4.2 of the paper ("retractors give retractions"), together with the two lemmas its proof rests on.
Let be a Euclidean space of dimension (in the paper's examples, with the Frobenius inner product). A set is a submanifold of dimension if around every it is a coordinate slice: there are an open neighbourhood of and a diffeomorphism of onto an open subset of with . Throughout, .
The tangent space is the linear subspace of of tangent directions of at , the normal space is its orthogonal complement, and the tangent bundle is .
A map from to is a retraction around (Definition 2.1) if, on a neighbourhood of in , it is of class , satisfies , and has derivative at . It is a retraction on if this holds around every point.
A retractor (Definition 4.1) is a map , defined on a neighbourhood of the zero section of , with values in the Grassmann manifold of -dimensional linear subspaces, such that for every . Given , set and let
The theorem asserts both that the point-to-set map is single-valued near the zero section and that it is a retraction there.
Near there is one and only one smallest with ; ; and is a retraction around , hence on .
On a neighbourhood of the zero section, for a unique linear depending on .
If and for all , then for all .
Theorem 4.2 reduces the construction of a retraction to the choice of a smooth field of subspaces transverse to the tangent space at . The orthographic retraction () and the projective retraction () are both instances, as are the gnomonic, orthographic and stereographic projections on the sphere. Theorem 4.9 then certifies, by a check at only, that a retraction agrees with the exponential to second order, which matters for the superlinear convergence of Riemannian trust-region and Newton methods. Lemma 4.7 goes beyond an earlier result on tangential parameterizations (reference [28, Th. 3.4] of the paper) by giving regularity jointly in , not only in (Remark 4.4 of the paper).
The results are proved in the paper. None of them is machine-checked: Mathlib has the implicit function theorem and smooth manifolds, but no embedded submanifolds of a Euclidean space with their tangent and normal bundles, no retractions, and no smooth Grassmannian-valued maps. The work here is to formalize the known proof and to build this layer, which every later mission of this series (projective, spectral, fixed-rank and Stiefel retractions) also needs.
The statement is an implicit-function argument, but the obvious one does not apply directly. The unknown lives in the normal space , which moves with , and ranges over the tangent bundle, a submanifold of rather than an open set of a vector space. The equation has to be read in charts of the bundle, which costs one derivative; the uniqueness given by the implicit function theorem holds only locally in , and turning it into "the smallest ", or "the nearest point of ", requires excluding far-away intersection points. For a general retractor, the subspace also moves, and has to be written as a graph over the normal space with a dependence before a second implicit-function argument applies.
is a finite-dimensional real inner product space E, is Module.finrank ℝ E, and are natural numbers with and (the latter inside the submanifold definition). The coordinate slice uses an open partial homeomorphism E → EuclideanSpace ℝ (Fin n), in both directions, with 0-based coordinates. is the span of Mathlib's tangent cone (chart-free), its orthogonal complement. Retractions and retractors are total maps on constrained only on with open; "of class on a subset of " is ContDiffOn on that set. A Grassmannian-valued map is when its orthogonal projector is, and the dimension of is part of the definition. The set-valued uses the published nearest-point predicate RandomGradFree.Nonsmooth.IsMetricProjection. In Lemma 4.8, is extended by on so that it is an operator on . Theorem 4.9 assumes , the standing assumption of the definition of second-order retractions (display (2.3)), and reads the page's "" as for all .
The goal is not satisfied by exhibiting some retraction: it requires the nearest-point set to equal a singleton (so it is nonempty) and that very to be a retraction. Theorem 4.9 requires the curve to be twice differentiable, so a junk second derivative of does not satisfy it.
A complete development needs: finite-rank facts for tangent spaces of slices (), smoothness of , charts of and of the Whitney sum , ContDiffOn on submanifolds, and local orthonormal frames of a smooth field of subspaces. All of these are reusable beyond this mission. Contributions to any of them, and proofs of the two lemmas, are welcome.
Many large convex programs have the form "minimize a strictly convex function subject to linear equations ". Examples are entropy maximization under moment constraints, the estimation of a matrix with prescribed row and column sums (the matrix-scaling or RAS problem of transportation and input–output analysis), and least-norm solutions of linear systems. When is large and sparse, methods that touch one equation at a time are attractive: each step needs only one row of .
L. M. Bregman's 1967 paper (doi:10.1016/0041-5553(67)90040-7) introduced such a method. §1 defines a "relaxation" for finding a common point of closed convex sets , in which each step replaces the current point by its -projection onto one set: the minimizer of a distance-like function over that set. §2 chooses from the objective itself, with the gradient of ; this function is now called the Bregman divergence. Theorem 3 of the paper, the target of this mission, shows that with this choice the relaxation does more than find a feasible point: started at a suitable point, its limit minimizes over the feasible set. The resulting row-action methods underlie later work on entropy optimization and matrix balancing (Censor and Zenios, Parallel Optimization, 1997) and the Bregman-projection techniques of modern optimization.
Work in the Euclidean space with inner product . Let be a convex set with closure and interior . Let be strictly convex and continuously differentiable over , with gradient at , and continuous over . Let be an matrix with nonzero rows and . The problem (2.1)–(2.3) is
with feasible set , assumed nonempty. A point of minimizing over is a solution.
The function (1.4) is
and also denotes the hyperplane . The paper assumes that satisfies its conditions I–VI of §1 with respect to these hyperplanes; among them, condition II provides, for every , a -projection minimizing over . It also assumes condition (2): if and , then .
A relaxation sequence with control starts at and sets . The control is any sequence of row indices. Finally,
is the set of points of at which the gradient lies in the row space of .
Assume that the -projection of every point of onto every lies in . For every control and every relaxation sequence with that converges to a point ,
Convergence of the sequence is a hypothesis; the theorem says what the limit is, whichever control produced it.
An additional item states Note 2: the point and the multiplier in (2.7)–(2.8) are unique.
Theorem 3 converts a feasibility algorithm into an optimization algorithm for equality-constrained convex programs. Each step solves a one-dimensional problem (the multiplier of a single equation), so the method scales to systems with very many equations, and with the controls of Theorems 1–2 of the same paper it gives a complete algorithm. Specializations include iterative proportional fitting for entropy objectives and Kaczmarz-type projections for .
The theorem and its proof are classical and have been reproved many times, but no machine-checked proof is known to exist. A formalization produces a verified bridge between three standard pieces of convex analysis: first-order optimality on an affine set, the supporting-hyperplane inequality for a differentiable convex function extended to the closure of its domain, and the passage of a Lagrange condition to a limit. Each is reusable in other row-action and mirror-descent developments.
The obvious argument says: the limit is feasible, and the gradient at every iterate lies in the row space of , so the limit satisfies the Karush–Kuhn–Tucker conditions. Two steps of this argument fail as stated. First, the gradient is only known on , the limit may lie on the boundary of (or outside , in ), and need not extend continuously there, so the multipliers need not converge and no Lagrange condition holds at the limit. Lemma 3 must therefore reach optimality without a gradient at . Second, the Lagrange condition (2.7) at an iterate requires the projection to be an interior minimizer, which is why the theorem carries the hypothesis that preserves ; on the boundary of a minimizer over need not satisfy (2.7).
The space is EuclideanSpace ℝ (Fin p), rows are vectors a i, and is the real inner product. The gradient is explicit data tied to by HasGradientWithinAt f (g x) S x for and continuous on ; is not assumed open, and Mathlib's gradient is not used. The relevant explicit choices are:
lam.The goal does not conclude that the relaxation converges; a statement asserting convergence is a different, unproved theorem. Equally, it must not be weakened to a fixed control, to an open , or to a limit assumed to lie in : any of these would trivialize the passage to the limit that the theorem is about.
A complete development needs the first-order condition for a local minimum on an affine hyperplane, the gradient inequality for , , and an induction along the relaxation sequence. Proofs of the milestones and of Note 2 are welcome independently.
A reproducing kernel Hilbert space is a Hilbert space of functions on a set in which every point evaluation is continuous; the function that represents evaluation at is its reproducing kernel. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404, DOI 10.1090/S0002-9947-1950-0051437-7) gave the general theory of these spaces, which today underlies kernel methods in statistics and machine learning, Gaussian-process regression, and the Bergman and Szegő kernels of complex analysis.
Part I of the paper studies how kernels behave under the basic operations on classes of functions: sums, inclusions, products, restrictions, and limits. §9 treats limits. Its case A concerns a decreasing sequence of classes with increasing norms, defined on an increasing sequence of sets. The application in the paper's Part II is the computation of kernels of a domain by approximation from simpler domains: when a domain is exhausted by an increasing sequence of subdomains, the kernels of the subdomains converge to the kernel of the whole domain. This mission formalizes §9, Theorem I and the steps of its proof.
Let be an arbitrary set and subsets with union . For each let be a complex Hilbert space of functions on , with norm , in which point evaluations are continuous; , for , is its reproducing kernel, characterized by and
with the scalar product linear in . For and , denotes the restriction of to . The standing assumptions of §9 A (p. 362) are:
together with the existence of every kernel . For two kernels on a set , means that is a positive matrix: for all finite families , . is the restriction of to .
The limit class is the set of functions on such that (1°) every restriction belongs to and (2°) .
Under the standing assumptions there is such that, whenever ,
and is the reproducing kernel of with the norm
The result. Theorem I turns a monotone family of function spaces into a single space and identifies its kernel as the pointwise limit of the kernels. It reduces the computation of a kernel on a large set to kernels on an exhausting sequence of subsets, the method Aronszajn uses in Part II for Bergman-type kernels of plane domains. With for all (explicitly allowed on p. 362) it gives the limit of a decreasing sequence of kernels on one set as the kernel of the intersection class with the limit norm. The milestones (4)–(6) are quantitative: (5) bounds the distance between restricted kernel sections by the decrease of the diagonal values, which yields strong convergence of in every .
Formalizing it. The theorem is classical and proved in the paper; to our knowledge no machine-checked proof exists. Mathlib has the RKHS class, the operator-valued kernel, the positive semidefiniteness of kernels and the Moore–Aronszajn construction RKHS.OfKernel, but nothing about restrictions of an RKHS to a subset, the order between kernels, or limits of sequences of reproducing kernel spaces. This mission produces those statements on Mathlib's RKHS vocabulary over , with kernels on varying domains.
The kernels live on different sets , so convergence is not convergence of a sequence of functions on one set: a pair enters the sequence only from the first containing both. The identification of the limit class needs three separate facts: that with the limit norm is a Hilbert space (the limit of norms must be shown to come from a scalar product, and completeness requires passing to the limit in two indices), that , and that reproduces. The natural first idea, to embed all in one space and take an intersection, fails: the are spaces of functions on different sets, and their norms differ, so there is no common ambient Hilbert space; the comparison goes only through restriction and the inequalities (3). Eq. (4) itself uses §7, Theorem II (a contractively included Hilbert subclass has a dominated kernel) and the restriction theorem of §5, neither of which is in Mathlib.
H n with [InnerProductSpace ℂ (H n)] [CompleteSpace (H n)] [RKHS ℂ (H n) (E n) ℂ], a space of functions on the subtype E n; the set is a type X with no topology, measure or nonemptiness assumption.kernelFn H x y is Mathlib's RKHS.kernel H x y 1. Mathlib's inner product is conjugate-linear in the first slot, so Aronszajn's is ⟪g, f⟫_ℂ.IsDecreasingRKSequence; every statement takes it as a hypothesis. Restriction is pointwise agreement on . Indexing starts at .KernelLE K₁ K := (Matrix.of K - Matrix.of K₁).PosSemidef, with Mathlib's positive semidefiniteness over an arbitrary index type (finitely supported vectors).ComplexOrder, which also asserts that these values are real.Tendsto).RKHS.OfKernel K₀ and then asserts that its kernel is would be a tautology (RKHS.kernel_ofKernel); the goal instead characterizes the space by its functions and norm, as the paper does.Needed infrastructure, reusable beyond this mission: restriction of an RKHS to a subset (§5), the dominated-kernel theorem for contractive inclusions (§7, Theorem II), and the passage from a convergent sequence of norms to a convergent sequence of scalar products. Proofs of any milestone, and of these general facts as separate lemmas, are welcome.
Mathlib/Analysis/InnerProductSpace/Reproducing.lean (the RKHS class, RKHS.kernel, RKHS.OfKernel). https://github.com/leanprover-community/mathlib4Reproducing kernel Hilbert spaces are the function spaces of kernel methods in statistics and machine learning (Gaussian-process regression, support vector machines, kernel mean embeddings), of the Bergman and Szegő spaces of complex analysis, and of the theory of positive-definite functions. In all of these, bounded operators on the space (covariance operators, integral operators, projections onto subspaces, multiplication operators) are handled through functions of two points rather than through abstract operators. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404) gives, in its §11, the dictionary between bounded operators on a space with a reproducing kernel and their kernels, and characterizes the kernels of bounded symmetric operators with prescribed bounds. Aronszajn credits the ideas of the section to E. H. Moore.
Let be an arbitrary set and let be a class of complex-valued functions on that forms a complex Hilbert space with scalar product , linear in and conjugate-linear in . A reproducing kernel of is a function such that, for every , the function belongs to and
Such a kernel exists exactly when every point evaluation is continuous.
For a bounded linear operator on , with adjoint defined by , the kernel of is
the value at of the element of . By the reproducing property, for every and , so is determined by .
A function is a positive matrix if for every finite family of points and complex numbers . For two arbitrary functions on , one writes if is a positive matrix. A bounded operator is symmetric if , and positive if for every . A symmetric has lower bound and upper bound if
A kernel is hermitian symmetric if .
For an arbitrary hermitian symmetric function and real numbers :
The function is not assumed to have ; that membership is part of what the condition yields.
Theorem I identifies, by finite quadratic-form inequalities alone, which functions of two points are kernels of bounded symmetric operators and with which spectral bounds. It reduces statements about operators (boundedness, positivity, operator inequalities ) to statements about finitely many evaluations of kernels, the form in which they are checked in practice, for instance when a covariance or integral operator is shown to be bounded and positive from its kernel. The milestones make the correspondence a usable calculus: adjoints become conjugate transposes, composition becomes a scalar product in the middle variable, and limits of operators become limits of kernels.
All of these results are proved in the paper. None is formalized: Mathlib has reproducing kernel Hilbert spaces (RKHS), adjoints, positive operators and positive semidefinite matrices over arbitrary index types, but no kernel of an operator and none of the statements above. The mission produces machine-checked proofs of the §11 dictionary and of Theorem I.
The necessity half of Theorem I and milestones (3), (6), (4) follow from the reproducing property. The sufficiency half is where the work is: is an arbitrary function, and the hypothesis is only about finite families of points. One has to produce an operator on all of . The obvious attempt, defining on the dense span of the functions by the kernel and extending by continuity, needs the bound on that span, which does not follow directly from the two one-sided inequalities on the diagonal forms. The positivity of and does not by itself give the membership , which the definition of the kernel of an operator requires. In milestone (7), positivity of an operator is a statement about all of , while positivity of the kernel only sees finite combinations of kernel functions; the passage between them uses density of these combinations.
RKHS ℂ H X ℂ: a complex Hilbert space H whose elements are functions X → ℂ on an arbitrary type X (no topology, no measure, not assumed nonempty), with continuous evaluations. The scalar kernel is the series' shared definition AronszajnRK.Sum.kernelFn H x y := RKHS.kernel H x y 1; the function is the element RKHS.kerFun H y 1.L : H →L[ℂ] H is opKernel L x y := (adjoint L) (kerFun H y 1) x. Mathlib's ⟪u, v⟫_ℂ is conjugate-linear in u, so the paper's is ⟪g, f⟫_ℂ, and every formula with a scalar product or a bar has been rewritten in that order. On a one-point with , and , the kernel is .Matrix.PosSemidef of Matrix.of Λ over the index type X (finitely supported test vectors, ComplexOrder on ℂ); no finiteness of X is assumed.IsSelfAdjoint L. "Positive" in (7) is ∀ f, 0 ≤ ⟪f, L f⟫_ℂ in ComplexOrder (real and nonnegative), without assuming self-adjointness, as in the paper. The bounds in Theorem I are bounds of the quadratic form, m‖f‖² ≤ Re⟪f, L f⟫ ≤ M‖f‖², not of the operator norm. The paper does not assume and neither does the statement: for both sides hold exactly when and .H, and that the kernel of L₁ ∘L L₂ is their scalar product.⟪v, Lₙ u⟫ → ⟪v, L u⟫ for all u, v; uniform convergence is ‖Lₙ − L‖ → 0 in operator norm.HilbertBasis with arbitrary index types, and the double limit is taken along growing finite sets of indices in both variables. For systems indexed by this contains the paper's over ; the general form also covers finite-dimensional spaces. The second sentence of Theorem III (kernels in correspond to operators of finite norm) needs the direct product and is not stated.RKHS, RKHS.kerFun_inner, RKHS.kerFun_dense, RKHS.posSemidef_kernel, ContinuousLinearMap.adjoint, ContinuousLinearMap.IsPositive and isPositive_iff_complex, HilbertBasis, Matrix.PosSemidef. Contributions welcome: a general lemma that a function with is the kernel of an operator , and the inclusion theorem , both reusable beyond this mission.In a network design game each player must connect its terminals in a graph whose edges carry fixed costs, and the cost of an edge is split among the players that use it. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 38 (2008)) studied the fair (Shapley) split, in which the users of an edge pay equal shares. That game is a congestion game in the sense of Rosenthal (Int. J. Game Theory 2 (1973)), so it has an exact potential and pure Nash equilibria always exist.
Section 6 of the same paper turns to weighted players: player has a weight (a traffic volume, a bandwidth demand, a share of ownership) and pays for each edge it uses a share proportional to its weight. The equal-split potential is then lost, and the paper notes that weighted games with three or more players need not have a pure Nash equilibrium at all (Chen and Roughgarden, Network design with weighted players, SPAA 2006). Theorem 6.3 identifies a natural class in which equilibria survive: all players share one source and one sink. For that class it shows more than existence. The simplest decentralized procedure, letting players in turn switch to a cheapest route, always stops, and where it stops is an equilibrium.
A finite directed multigraph has a finite set of arcs; each arc has a tail and a head vertex, and parallel arcs between the same two vertices are allowed. Fix a source and a sink . A simple – path is a sequence of arcs (), each starting where the previous one ends, beginning at , ending at , and visiting no vertex twice; it is identified with its arc set . Write for the finite set of these paths.
The weighted single-commodity game has a finite set of players; player has a weight , arc has a fixed cost , and every player's strategy set is . In a profile let
be the total weight on arc . Player pays
A profile is a (pure) Nash equilibrium if no player can lower its payment by switching alone to another path.
A best-response move of player replaces by a path that minimises 's payment given the other players' paths, provided this strictly lowers 's payment. Best-response dynamics is any sequence of profiles in which each profile arises from the previous one by a best-response move of some player.
For every such game with and :
The goal asserts only termination and existence; it fixes no bound on the length of a run.
For a profile define the marginal cost of a path, , and the tuple of all values , , sorted increasingly. With strictly positive arc costs:
The theorem gives a guarantee about dynamics, not only about existence: in single-commodity weighted network design, any order in which players take turns playing best responses reaches a stable outcome in finitely many steps. This places the single-commodity case on the positive side of the boundary drawn by the nonexistence examples for general weighted games. The tuple of sorted path costs is a potential that is not a single number, a device that applies to other games without an exact potential.
The result is proved in the paper; it has no machine-checked proof that this mission is aware of. A formal development contributes a reusable layer for weighted cost-sharing games (payments, best responses, Nash equilibria on arbitrary strategy families), a treatment of simple directed paths in multigraphs as strategy sets, and a lexicographic termination argument over sorted lists of extended reals. The goal is stated for nonnegative costs, as in the paper's model, while the printed proof uses positive costs; closing that gap is part of the work.
The obvious route, finding a real-valued function that every improving move decreases, is unavailable: the paper notes that Rosenthal's potential is not a potential once weights are added, and that improving moves can increase it. Termination must instead come from an ordinal quantity, a whole sorted list compared lexicographically, and the move of one player changes the marginal costs of every path that shares an arc with the old or the new route, in both directions.
The argument also depends on the shape of the strategy sets. Two distinct simple – paths are never nested as arc sets; with walks that repeat vertices, or with arbitrary strategy families, the comparison between a path's marginal cost before and after a deviation can fail. Arcs of cost zero create a further gap: is on an unused free arc, and the strict inequalities of the proof degenerate, so the nonnegative-cost goal needs more than the printed argument.
Finset of arcs; the strategy family of every player is the finite set of arc sets of simple – paths (a list of consecutive arcs with distinct visited vertices). There are no paths when .IsStandard); the milestones (6.1) and the lexicographic decrease assume .ℝ≥0∞): an unused arc of positive cost contributes . Computing it in the reals, where , would make unused paths free and the milestones false.Contributions welcome: lemmas on simple paths in multigraphs (non-nestedness), the multiset-to-sorted-list lexicographic comparison, and the treatment of zero-cost arcs.
We establish the polynomial simulation needed for WordRAM-based NP proofs. It reuses the same machines and Cook–Levin definitions, with uniform programs, logarithmic word widths, and standard bit input/output.
The targets cover function outputs and verifier verdicts, including loading and serialization costs.
This adapts Cook–Reckhow’s Theorem 2(a), pp. 361–363, to Hagerup’s bounded-word operations, including multiplication; no particular simulation exponent is prescribed.
Mean field games (MFG), introduced by Lasry and Lions and by Huang, Caines and Malhamé, describe Nash equilibria of very large populations of identical rational agents. The equilibrium is a coupled system: a backward Hamilton–Jacobi–Bellman equation for the value function of a representative agent and a forward Fokker–Planck equation for the density of the population. In the planning problem, proposed by P.-L. Lions, both the initial density and the final density are prescribed, and one asks for a cost structure under which the population moves from one to the other. This is a mean field analogue of optimal transport.
Achdou, Camilli and Capuzzo-Dolcetta (hal-00465404, SIAM J. Control Optim. 2012) propose finite-difference schemes for the planning problem. Mission I of this series treats the existence of a solution of the discrete planning scheme. Since the two boundary conditions on make the discrete system hard to solve directly, the paper also introduces a penalized scheme, in which the initial condition is replaced by a penalty ; for each this is a standard discrete MFG system with a unique solution. This mission formalizes the paper's §3.2: the penalized solutions converge, as , to a solution of the planning scheme.
Fix integers , , a horizon and a viscosity ; put and . The grid consists of the points , (periodic indices). A grid function is a real function on ; time levels are .
The planning scheme (18) asks for families with, for ,
, and . The penalized scheme (20)–(23) has the same two equations, for , , and in place of .
Under the hypotheses of Theorem 1, for every sequence , every choice of penalized solutions , and every limit in ,
If is strictly convex, the whole sequence converges to the unique solution of (43)–(46) with .
In 3–5 the constant depends on , and the data, never on .
Proposition 4 justifies the penalized scheme as a way to compute solutions of the discrete planning problem. The penalized system has a standard initial–terminal structure that Newton's method (the paper's §4) handles well. The planning system does not, because it prescribes two conditions on and none on . The estimates of Propositions 2–3 and Corollary 1 also give a rate: the initial mismatch of the penalized density is .
The results are proved in the paper. None of them has been machine-checked: the platform holds no formalization of mean field games, of their finite-difference schemes, or of the Lasry–Lions monotonicity argument. A complete development would yield a reusable library of the monotone finite-difference operators on the discrete torus, a formal Lasry–Lions uniqueness argument for discrete MFG systems, and a template for compactness-plus-uniqueness convergence proofs in finite dimension.
Compactness of the densities is free, since is compact. Passing to the limit in the scheme needs only continuity of , and . The substance lies in the two uniform estimates.
All objects live in the namespace MFGPlanning.Penalized.
ZMod Nh × ZMod Nh (periodicity is built in), time levels are Fin (NT + 1), and the four momentum components are Fin 4 indices 0, …, 3.EReal, so unbounded suprema are .Three trivializing formalizations are ruled out. The constants in Propositions 2–3 and Corollary 1 are quantified before and before the solution. The goal quantifies over every sequence and assumes no convergence of and no limit solution. Its part 2 does not assume convergence of .
The existence of a solution of the planning scheme (Theorem 1) is posed in mission I and not restated here. A solver of Proposition 2 will need it once mission I's goal is proved. The existence and uniqueness of solutions of (20)–(23) are quoted by the paper from Achdou–Capuzzo-Dolcetta (2010) and are not items. Welcome contributions include discrete summation-by-parts lemmas on the torus, the discrete comparison principle for monotone schemes, and the Poincaré-type inequality on zero-mean grid functions.