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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. A high-probability approximation guarantee is a separate claim requiring an explicit probability bound. The optimum includes entangled states. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
Network design problems often ask for a cheap spanning tree in which no vertex is overloaded: in multicast and overlay networks the degree of a node bounds the number of copies it must forward, and in physical networks it bounds the number of ports. The minimum bounded degree spanning tree problem asks for a minimum-cost spanning tree whose degrees respect given bounds. Deciding whether a graph has a spanning tree of maximum degree 2 is already the Hamiltonian path problem, so exact solutions are out of reach, and the question becomes how little the bounds and the cost must be relaxed.
Some problems also impose lower bounds: a vertex that must serve as a hub, or a leaf-avoidance requirement, asks for degree at least . Singh and Lau (STOC 2007) showed that the iterative rounding method they used for upper bounds extends to both kinds at once: a spanning tree of cost at most the LP optimum whose degree at every vertex lies in .
Timeline. Fürer and Raghavachari (1994) found a spanning tree of maximum degree at most in the unweighted case. For costs, Goemans (FOCS 2006) obtained cost at most OPT with degrees at most . Singh and Lau (STOC 2007) improved this to , which is the best possible additive violation unless P = NP, and gave the extension to lower and upper bounds formalized here. The journal version appeared in J. ACM 62(1), 2015.
Let be a finite simple graph with edge costs ; no sign or triangle inequality is assumed. Let be a forest on with no edge in common with . A set is an -tree if is a spanning tree of , and is the number of edges of at . Integer lower bounds are given on and integer upper bounds on . The minimum bounded degree connecting tree problem asks for a cheapest -tree with on and on ; with it is the spanning-tree problem.
The supernodes are the vertex sets of the components of , isolated vertices included, and is the family of unions of supernodes. For , and are the edges with both endpoints in , the edges with exactly one endpoint in , and . The linear relaxation LP-MBDCT minimizes subject to
MBDCT Algorithm2 (Figure 5 of the paper) repeats: if is a spanning tree, stop; otherwise take a basic optimal solution , delete the edges with , move one edge with (if any) into and lower and by one at its endpoints, and otherwise remove from and one vertex whose support degree is at most two.
For every well-formed instance whose LP is feasible, MBDCT Algorithm2
The statement fixes no constants beyond the paper's , and it is uniform over every choice of basic optimal solution, 1-edge and removed vertex.
In the order the proof uses them: Lemma 5.3 (a basic solution is determined by a laminar family of tight sets and tight lower and upper degree rows, with ); Claims 5.4, 5.7, 5.8 and 5.9 (special supernodes, cut sizes, the value on the edges between the members of , and when a set is special); Lemma 5.6 (every set of keeps at least three tokens, exactly three only if it is special or ); and Lemma 5.1 (a basic solution has an edge with or a vertex of with support degree two).
The theorem gives, in one algorithm, a tree that is no more expensive than the LP lower bound and whose degrees miss both bounds by at most one. For the pure upper-bound problem it implies the guarantee, which cannot be improved to unless P = NP, since a Hamiltonian path is the case . With lower bounds it also covers prescribed minimum degrees.
The result is proved in the paper; no machine-checked proof of it, or of any iterative rounding analysis, is known to exist. No platform item treats bounded-degree spanning trees or iterative rounding; the nearest related item is the open Williamson–Shmoys minimum-degree spanning tree local-search goal, which concerns a different, unweighted problem. Formalizing this mission requires the extreme-point structure of the spanning tree polytope with degree constraints (uncrossing to a laminar family), the token counting argument, and the induction over the algorithm's recursion, all of which are reusable for other iterative rounding results.
The obvious argument rounds an optimal LP solution once. It fails: an optimal vertex may be entirely fractional, and no single rounding keeps both the cost and the degrees. The algorithm instead re-solves the LP after each change, and its correctness rests on Lemma 5.1, that every extreme point of the current LP has an integral edge or a vertex with support degree two. That lemma is a counting statement about extreme points: the rank bound from a laminar basis must be contradicted by a token distribution. With upper bounds only, every set of the laminar family can collect four tokens. With lower bounds a set may collect only three, and the proof must characterize those sets (special sets, Definition 5.5) and show by linear independence that the remaining cases cannot occur. A second difficulty is that the guarantee concerns the final tree after many iterations, so the degree accounting must survive the changes of , , , and along the run.
Vertices form a Fintype; edges are elements of Sym2 V with no loops, and , are finite sets of edges with acyclic and disjoint from . LP vectors are functions on Sym2 V that vanish off . Right-hand sides are computed in , degree bounds are integers, and the subtour rows range over nonempty (at the literal row would make the LP empty). A basic solution is a feasible that is the only vector on satisfying with equality every constraint tight at , including the tight rows . Supernodes are never contracted: the paper's contraction of a supernode with one active vertex is a proof device, and all of §5.1's notions are stated on the original instance.
The paper's loose phrases are made explicit as follows.
Two trivializations are ruled out. Existence of a cheap tree with degrees in is not the target: the statement is about the algorithm's outputs and quantifies over all of them. And a run that never terminates does not satisfy the goal, which requires a run to exist and every run to be bounded.
Contributions are welcome at every level: the laminar uncrossing argument (Lemma 5.3), which is reusable for any spanning-tree LP with degree rows; the counting claims; and the invariants of the recursion.
Functional limit theorems in queueing and applied probability are rarely proved from scratch. A limit theorem is established once for a primitive process, such as a random walk, a cumulative input or a renewal-reward process, and then transferred to the quantities of interest through the continuous mapping theorem: if in a function space and is continuous at almost every path of , then . The method works only if the functions in use are known to be continuous, and in which topology.
Ward Whitt's 1980 paper supplies these facts for composition, addition, the supremum, the reflecting barrier, the inverse or first passage time, and time reversal. This mission covers §7, the first passage time. Its role in applications is direct: the counting process of a renewal process is the first passage time of the partial-sum process. A limit theorem for cumulative work can therefore yield one for the number of completed jobs, and a limit theorem for a cumulative input can yield one for the time it takes to reach a level, when the mapping theorem's hypotheses hold.
Timeline. Skorohod (1956) introduced the topologies and on the space of right-continuous paths with left limits. Vervaat (1972) studied functional central limit theorems for processes with positive drift and their inverses, and Whitt (1971) studied weak convergence of first passage time processes. Whitt's 1980 paper restates continuity (Theorem 7.1) and adds the result: the map is continuous at every strictly increasing path (Theorem 7.2), although it is not -continuous on its whole domain.
A path is a function . It belongs to when it is right-continuous and has a left limit at every .
If , is strictly increasing, and in , then
The theorem says that every strictly increasing path is a continuity point of the first passage time map for . It fixes no constants, so a sharper variant of a milestone does not invalidate it.
The result. Theorem 7.2 lets functional limit theorems pass to first passage times when the limit has strictly increasing paths. The typical case is the fluid limit of a cumulative process, with . Together with the composition results of §3, it supports Theorem 7.3's centered inverse limit: if , , , has no positive jumps, and in , then in . This is one step from a central limit theorem for partial sums to one for counting processes. Theorem 7.4 shows a limitation: convergence of both the centered supremum and the centered inverse in forces a continuous limit.
Formalizing it. The results are proved and classical, but none of them has a machine-checked proof. The mission produces the topology on in Lean, the first passage time map with its basic properties, and the comparison between , and . That infrastructure is reused by every later formalization that goes through counting processes or the topology, including the planned wave of §§3–7 corollaries in this series.
The first passage time map is not -continuous. On p. 82 the paper gives paths in whose inverses converge only in : a flat stretch of the limit becomes a jump of , which the inverses of the approximating paths approach through two separate jumps. Inverting the time changes of the convergence cannot handle that split, because matches jumps one to one. The hypothesis that is strictly increasing excludes flat stretches of the limit. The technical weight lies in completed graphs and their parametric representations, which Mathlib does not have, and in the restriction to compact intervals at continuity points of the limit.
Ici 0. All convergences are sequential, which is equivalent because the spaces are metrizable (Theorem 2.6). Membership of every path in is part of each convergence.Contributions welcome: the general theory of parametric representations (existence, and the comparison with and ), which is reusable for any result. Alternative proofs of Theorem 7.2 that avoid are also welcome.
Many problems in statistics, signal processing and machine learning minimize the sum of a smooth loss and a convex, nonsmooth, separable regularizer: smooth optimization with -regularization, bound-constrained optimization, the group Lasso and, through duality, support vector regression are special cases listed in §1 of the paper discussed below. For such problems, methods that update one coordinate, or one small block of coordinates, at a time are often the method of choice, because each update is cheap and exploits separability.
Paul Tseng and Sangwoon Yun (Math. Program. Ser. B 117 (2009) 387–423) introduced the coordinate gradient descent (CGD) method for this class: at each iteration it minimizes a quadratic model of the smooth part plus the exact nonsmooth part over a chosen block of coordinates, then takes an Armijo step. Their paper proves global convergence (Theorem 1) and, under a local error bound, linear convergence (Theorems 2 and 3). This mission is the second of a three-mission series on the paper; it targets the linear convergence theorem for the cyclic (Gauss–Seidel-type) choice of blocks.
The analysis follows Luo and Tseng's error-bound framework for smooth constrained problems (Ann. Oper. Res. 46 (1993) 157–178), which established linear rates for feasible descent methods without strong convexity. Tseng and Yun extend that framework to a nonsmooth convex term.
Let carry the Euclidean norm , let , and for let be the subvector of coordinates in . The problem (1) is
where , is proper, convex and lower semicontinuous, and is continuously differentiable on an open set containing .
Given , a nonempty block and a symmetric positive definite matrix , the direction (6) is
The CGD method starts at , chooses at each iteration a block and a matrix , computes , and sets . The Armijo rule takes as the largest element of with
with and . The restricted Gauss–Seidel rule (12) asks for indices (the set ) such that the blocks used during each cycle are pairwise disjoint and cover . is block-separable with respect to if .
The analysis uses three assumptions: is -Lipschitz on (22); Assumption 1, with ; and Assumption 2. Writing for the set of stationary points of and for the full direction with , Assumption 2 says (a) and the local Lipschitzian error bound holds on every level set wherever ; (b) stationary points with different objective values are at least a fixed distance apart.
Under (22), Assumptions 1 and 2, the restricted Gauss–Seidel rule, block-separability of with respect to every , and Armijo steps with and :
No rate constant is fixed: the goal asserts the shape of the convergence, so it is not invalidated by sharper constants.
Lemma 4 (Hölder dependence of the subproblem's solution on its linear term), Lemma 5(a) (a per-block variational inequality), Lemma 5(b) (an explicit stepsize at which the Armijo test passes), Theorem 1(f) (Armijo stepsizes bounded away from zero, , ), and Theorem 2(a) (the residual at the start of a cycle is bounded by the step lengths of the cycle).
Theorem 2(b) gives a linear rate for a block coordinate method on a nonsmooth, possibly nonconvex composite problem without strong convexity: the rate follows from the error bound, which holds for a large class of problems studied in §6 of the paper (the third mission of this series).
The theorem is proved in the paper; none of it has been machine-checked, as far as a search of the Prove2Me library shows. Formalizing it requires a reusable treatment of extended-valued convex functions through their effective domains, of the coordinate-restricted proximal subproblem, and of the Armijo rule for composite objectives. The milestones Lemma 4 and Lemma 5 are self-contained facts about this subproblem and are reusable for other proximal coordinate methods.
The classical route to a linear rate, as in Luo and Tseng's smooth analysis, derives from the error bound, where is the limit value. With a nonsmooth this inequality is not available: the authors say so on p. 405, and work with in place of the quadratic term. A second obstacle is that the error bound controls the full residual , while each iteration only computes a block direction at a different point; relating the two over a cycle needs the disjointness of the blocks in the restricted rule and block-separability of . Neither the global analysis nor the error bound alone gives the rate.
is EuclideanSpace ℝ (Fin n), with 0-based coordinates. The extended-valued is encoded as a pair: its effective domain and its finite values on , with "proper convex lsc" given by the published definition ProxNewton.Inexact.IsProperClosedConvex; is never evaluated off , and every statement carries membership in explicitly. The direction is the unique minimizer of (6) when and (chosen by Classical.epsilon), and runs of the method carry the minimizer property itself. The Armijo rule takes the first admissible exponent . is a strictly increasing map with . Stationarity is for all , in liminf form. In Assumption 2, is the infimum distance and "for any " is "for every real " (equivalent, since the condition is empty below ). Q-linear convergence includes convergence of the sequence; R-linear convergence is with . The rates in the goal are along , as the paper states.
Explicit choices relative to the printed text:
A statement that replaces Assumption 2 by strong convexity, claims a rate along the whole sequence rather than along , or asserts the Q-linear contraction without convergence to a limit is not this theorem and is out of scope.
Lemma 1, the claim after (10), Lemma 3 and Theorem 1(a), which the proof also uses, are milestones of the first mission of this series and are not restated here. Theorem 3 (the same conclusion along the whole sequence for the Gauss–Southwell-q rule) is not included: its proof is omitted in the paper. Contributions welcome: proofs of the milestones, and general facts about the coordinate-restricted proximal subproblem (existence and uniqueness of , optimality conditions) that the milestones rely on.
A G/GI/N queue has identical servers, a general arrival process, a first-come-first-served waiting room and i.i.d. service times with a general distribution of mean . In the Halfin–Whitt regime the number of servers grows while the traffic intensity approaches at rate ; this is the standard asymptotic model for large call centers, where a positive fraction of customers wait but waiting times are short. Halfin and Whitt (Oper. Res. 1981) obtained a diffusion limit for exponential service times. Reed (arXiv:0912.2837, Ann. Appl. Probab. 2009) proved the corresponding limit for general service times: the centred and scaled queue length converges (Theorem 5.1) to the solution of a nonlinear stochastic convolution equation, (5.33) below.
Equation (5.33) is written in terms of an infinite-server limit, and it is not evident from its form that it reduces to the Halfin–Whitt diffusion when service is exponential. Section 5.5 of the paper gives a second representation, Corollary 5.2, in which the convolution against is replaced by a convolution against the renewal function of . With exponential service the renewal function is , and the representation becomes the Halfin–Whitt diffusion. This mission formalizes Corollary 5.2 and the renewal-theoretic steps of its proof.
Timeline. Halfin–Whitt (1981): exponential service, diffusion limit. Reed (2009): general service with finite mean; Corollary 5.2 links the general limit back to 1981. Karlin–Taylor (1975) and Ross (1983): the renewal-type equation and the renewal equation that the proof cites.
Let be a probability measure on with mean (the service-time law), its distribution function and its tail. The equilibrium distribution is
Let be the -fold convolution of (the law of the th renewal epoch ). The renewal measure is and the renewal function is , the expected number of renewals by time .
A path is càdlàg on if it is right continuous at every with finite left limits at every ; only its values on matter. Fix a càdlàg driving path (in the paper , (5.40)) and . Write and . The two equations are
All Stieltjes integrals are over the closed interval .
For every service law , every càdlàg and every :
and (5.41) has a càdlàg solution that is unique on among càdlàg paths.
The result. Corollary 5.2 expresses the many-server diffusion limit as an equation that is linear in the driving process and whose only nonlinearity is the idle-server term . This is how the paper verifies that its general-service limit agrees with Halfin and Whitt's for exponential service, and the paper's sequel interprets the integral term as the limiting idle time of the servers. Uniqueness in (5.41) also yields the paper's remark that , the solution of (5.41).
The formalization. The result is proved in the paper, but only partly written: the printed proof shows that the solution of (5.33) satisfies (5.41), while the converse and the uniqueness are asserted. The mission states both. It also produces, independently of queueing, the renewal measure of a law on with possible atoms, its finiteness on bounded sets, the renewal equation and the solution of renewal-type equations, and the identity ; none of these is in Mathlib or published on the platform. To our knowledge nothing in this mission has a machine-checked proof.
The forward direction is formal once (5.42)–(5.43) is available, but (5.42)–(5.43) itself needs the renewal measure to be finite on bounded intervals when may have an atom at , and the uniqueness half needs an argument that does not assume the kernel has mass below one on any window starting at . The converse direction, (5.41) (5.33), cannot be read off the printed proof, because (5.41) is not an equation of renewal type in . The uniqueness of (5.41) is not a contraction argument either: the atom of at has mass , which may exceed , so a naive Picard estimate on fails.
negPart.BellmanDP.Inventory.renewal_equation_exists_unique (a renewal equation with a density kernel of mass below ); ChenWhitt93.Reflection.Basic (càdlàg paths on ). Reusable output: the renewal measure, (5.39) and (5.42)–(5.43) serve any renewal-theoretic development. Alternative proofs of the converse and of uniqueness are welcome.Nonparametric regression estimates the regression function from i.i.d. observations without assuming a parametric form. The simplest such estimates are local averages: to predict at a point , average the responses of the sample points closest to . Nearest neighbor rules of this kind go back to Fix and Hodges (1951) for classification and are still a standard baseline in statistics and machine learning.
Before 1977, consistency results for such estimates assumed regularity of the distribution of : a density, continuity of the regression function, or bounded support. C. J. Stone's paper Consistent nonparametric regression (Ann. Statist. 5 (1977) 595–645) proved that suitable nearest neighbor estimates are consistent in for every joint distribution of with . This property, now called universal consistency, is the subject of the first chapters of Györfi, Kohler, Krzyżak and Walk, A Distribution-Free Theory of Nonparametric Regression (Springer, 2002), where Stone's theorem is the organising result.
This mission formalizes Theorem 2 of Stone's paper, the universal consistency of nearest neighbor weights. Mission I of the series formalizes the general criterion (Theorem 1) that the proof applies; mission III treats conditional quantiles.
Let be i.i.d. random vectors in with an arbitrary law . A weight function assigns to the query point and the sample numbers , . It is a probability weight function if and . Given i.i.d. pairs with real, the estimate of is
The sequence is consistent if, whenever the pairs are i.i.d. with the given law of , and , one has .
Scales and metrics. A scale is a nonnegative function , , and its pseudometric is
The choice gives the Euclidean metric; the sample standard deviations of the coordinates give a unit-free one. The sequence is regular (p. 599) with constants if for every coordinate of with a nondegenerate law, is bounded in probability for any two such coordinates, and condition (7) holds: interchanging and changes by a factor in whenever the th coordinates of do not all coincide.
Nearest neighbor weights. Let with and for . The weight of is
where is the number of other sample points strictly -closer to than and the number at the same distance: the th closest point receives , and tied points share the average of the coefficients of their ranks. The uniform -NN rule is for .
For every law of and every regular sequence of scales,
Uniform, triangular and quadratic -NN weights with , satisfy both conditions (Corollary 3).
Theorem 2 established that a local averaging estimate can be consistent with no assumption on the distribution of beyond the moment condition on . The same argument, through Theorem 1, became the standard template for proving universal consistency of kernel, partitioning and nearest neighbor estimates, and of the classification rules derived from them (Devroye, Györfi and Lugosi, A Probabilistic Theory of Pattern Recognition, 1996). The constant of Proposition 11 is an early instance of the cone-covering bound on how many points can have a given point among their nearest neighbors, a lemma that reappears throughout nearest neighbor theory.
The result is proved (1977), and textbook proofs exist. Mathlib contains no formalization of Theorem 2, of Stone's criterion, or of the cone-covering lemma. A formal development would supply reusable infrastructure: nearest neighbor weights with averaged ties, the exchangeability argument behind Proposition 11, and consistency of weighted averages for i.i.d. data encoded through kernels.
The obvious argument estimates by a continuity argument around , which needs a density or continuity of and is unavailable here. The difficulty is condition (1) of Stone's criterion: a single sample point may be a nearest neighbor of many query points, so is not obviously comparable to for arbitrary and arbitrary (atoms, singular parts, unbounded support). The bound must hold uniformly in and in the distribution, with a data-dependent metric whose scale changes when and are interchanged. Ties in , which have positive probability when has atoms, must be handled by the averaged weights (8), not by an index tie-break.
Points live in EuclideanSpace ℝ (Fin d). The i.i.d. sequence is the coordinate process of Measure.infinitePi, coordinate 0 being ; sample indices are 0-based, coefficients keep the paper's 1-based index. "Whenever the pairs are i.i.d." is encoded by quantifying over every Markov kernel (the conditional law of given ), with pairs distributed as and . Expectations of nonnegative quantities are lower Lebesgue integrals in ; convergence in probability is TendstoInMeasure; limits of probabilities are taken in .
Standing assumptions and additions, each disclosed in the item statements:
No statement corrects the print.
The goal is stated as consistency over all kernels and all , for an unrestricted law : it is not stated through Corollary 1's three conditions nor through , and no density, moment or support hypothesis on is present, so a proof cannot reduce to a special case.
A complete development needs: exchangeability of finite i.i.d. samples under the product measure, the finite cone cover of , the strong law of large numbers (Proposition 9's proof), and Stone's criterion (mission I). Contributions proving any milestone, the cone-cover existence lemma, or the transfer of exchangeability through infinitePi are welcome.
Primal-dual interior-point methods are the standard algorithms for linear, second-order-cone and semidefinite programming. Their best-known variants keep the iterates in a narrow neighbourhood of the central path and take short or moderately long steps whose length is fixed in advance. Practical codes instead take long steps and recentre only when needed. Nesterov and Todd (SIAM J. Optim. 8 (1998) 324–364) developed a common theory of primal-dual methods for all self-scaled cones, the class that contains the nonnegative orthant, the second-order cone, the cone of positive semidefinite matrices, and their products. Section 7 of that paper analyses a predictor-corrector method whose neighbourhood is defined by the functional proximity measure , the conic version of the Tanabe–Todd–Ye potential. The predictor may move arbitrarily far from the central path, as measured by , and a Newton corrector brings the iterate back.
Timeline:
Let with the Euclidean inner product, and let be a closed convex cone that is pointed and has nonempty interior. Its dual cone is . A -self-concordant logarithmically homogeneous barrier for is a self-concordant function on that tends to at the boundary and satisfies and . Its conjugate is . is self-scaled if, for all , and . For and , the scaling point satisfies .
The problem is with dual , where is surjective. A triple is strictly feasible if , and both equality constraints hold. With the functional proximity measure is
and it vanishes exactly on the central path. The neighbourhood is . The affine-scaling direction solves , , . The centering direction solves the same system with right-hand side . One Newton step moves by , with , where is the uniform proximity measure and .
One iteration of Algorithm 7.1 starts from . It takes the largest predictor step along the affine-scaling direction with , then applies Newton steps until the iterate is back in .
Let with and . There are constants , depending only on and , such that one iteration of Algorithm 7.1 on any self-scaled cone satisfies
and the corrector reaches after Newton steps, where . The constants are left existential, as on the page.
In the paper's order, the milestones are:
Theorem 7.1 gives an iteration bound for a method whose predictor neighbourhood can be as wide as desired, with a bounded number of corrector steps per iteration. Inequality (7.3) also lets the step adapt to the problem: in the paper's normalisation the predictor step is at least of the order of the square root of the maximal feasible step. The same bounds apply to the narrow-neighbourhood predictor-corrector method of Section 6. One theorem covers linear, second-order-cone and semidefinite programming, with no reformulation through matrices.
The result is proved in the paper. No machine-checked proof of it, or of any of the self-scaled-barrier estimates it rests on, is known. Formalizing the proof produces a reusable library of local norms, σ-measures and third-derivative bounds for self-scaled barriers, and of the proximity measures of primal-dual methods.
A naive argument would bound the predictor step with the usual self-concordance estimate . That bound loses a factor and cannot give (7.2) or (7.3). What is needed is the sharper self-scaled bound (3.14), in which one factor is the smaller norm . It in turn depends on the cone being self-scaled: must be negative semidefinite for , and the scaling point must exist. The other obstacle is that the change of along the affine-scaling direction must be computed exactly, not just estimated. That is the parallelogram rule (Theorem 3.11), an identity special to self-scaled barriers. The corrector bound needs a lower bound on the Newton decrement that holds uniformly outside , which (4.28) supplies.
Spaces. The dual space is identified with through the inner product. Which local norm is meant is carried by the function used:
lnorm G v u and dnorm G v u, with or ;sigma C c u , with the cone and the centre fixed by the paper's four cases.Each two-form measure uses its first printed form.
Standing assumptions. Every statement assumes that is a proper cone and that is a -self-scaled barrier, and it also states , which the paper derives. The barrier includes explicit nondegeneracy of , which also follows from the other axioms. The conjugate is a supremum over and is only evaluated on . Assumptions (2.4)–(2.5) are implied by the strictly feasible points that the statements start from.
Scaling points, directions and steps are predicates given by their defining equations; nothing is computed by inverting a matrix.
Corrections to the page. Two printed slips are corrected, and both are disclosed:
Ruling out trivial versions. The goal does not assume any of the following; they are milestones, not hypotheses:
The constants are quantified before the cone, the barrier and the data, so they cannot depend on them. The predictor step is the largest step whose whole segment stays strictly feasible.
Out of scope. No self-scaled barrier, existence of scaling points (T*3.2 of [NT97]), or result of Nesterov–Nemirovskii is formalized here. These and the central-path duality theorem (Theorem 4.1) are external results. Proofs that build them are welcome, as is a non-vacuity witness for the goal on the orthant of .
Random partitions of the positive integers are the common language of population genetics, Bayesian nonparametrics and the theory of coalescent processes. When a sample of genes, customers or particles is grouped into classes, the grouping is a partition, and in most models its law is exchangeable: it does not depend on the labels. The best-known example is the Ewens sampling formula of population genetics (Ewens 1972); Kingman's representation theory (Kingman 1978) describes all exchangeable random partitions of .
Pitman's two-parameter family of exchangeable partitions, the partitions (Pitman 1995; Pitman and Yor 1997), contains Ewens' family as and is the partition counterpart of the two-parameter Poisson–Dirichlet distribution. Theorem 12 of Pitman 1999 shows that two natural random operations act on this family in a dual way: merging blocks of an partition according to an independent exchangeable partition (coagulation) and splitting each block of an partition by independent exchangeable partitions (fragmentation) produce the same joint law of a fine and a coarse partition. The paper uses it to describe the Bolthausen–Sznitman coalescent (Bolthausen and Sznitman 1998).
Timeline. 1972: Ewens' sampling formula, the case . 1978: Kingman's correspondence between exchangeable partitions and random mass partitions. 1995: Pitman introduces exchangeable partition probability functions and the formula (15). 1997: Pitman and Yor study the two-parameter Poisson–Dirichlet law. 1999: this paper proves the coagulation–fragmentation duality (Theorem 12) and its sharper converse, by reduction to an identity between explicit formulas. The duality is treated again in Pitman's lecture notes Combinatorial Stochastic Processes (2006).
A partition of a set is a collection of disjoint nonempty blocks whose union is the set. Write for the partitions of and for those of ; the restriction of to keeps the nonempty sets . carries the -algebra generated by the . Writing lists the blocks in increasing order of least elements.
A random partition of is exchangeable with EPF if for every and every partition of ,
For and the EPF is
with factors of and cancelled before evaluation when or . An partition is an exchangeable random partition with EPF .
Coagulation (Definition 5): for and , the -coagulation of has blocks . is a -coagulation of if, given , it is the -coagulation of for an independent with EPF . Fragmentation (Definition 11): is a -fragmentation of if, given , restricted to the -th block of equals restricted to that block, for independent with EPF . In Lean these are coag, frag, pdEPF and IsEPFLaw in LambdaCoalescent.CoagFrag.Setting.
For , , , the following are equivalent: (i) is an partition and is a -coagulation of ; (ii) is an partition and is an -fragmentation of . Formally, with laws of EPFs :
for every measurable .
Theorem 12 identifies one law of a nested pair of exchangeable partitions from both ends. Read from (i) to (ii), it shows that coagulating an partition by an independent partition yields an partition; read backwards, that an partition fragmented by partitions yields an partition. Through Kingman's correspondence it gives Corollary 13 on Poisson–Dirichlet laws, and with it connects the two-parameter family with Ewens' family. In the paper it is the tool for describing the Bolthausen–Sznitman coalescent through Poisson–Dirichlet laws. The sharper form shows the parameter relations (64) are forced.
The theorem has been proved since 1999. What this mission adds is a machine-checked development: exchangeable random partitions of with their EPFs, the coagulation and fragmentation kernels, and the reduction of identities between laws on to identities between finite-dimensional formulas. None of these objects is in Mathlib, and no formalization of the duality is known.
The algebraic heart, the EPF identity, is a finite computation with rising factorials. The difficulty is measure-theoretic and combinatorial. A law on must be pinned down by its values on the cylinder events . Computing under the coagulation kernel requires that the blocks of meeting are exactly the first blocks in order of least elements, and that the induced partition of has law given by the EPF; under the fragmentation kernel it requires the independence of the and that the restriction of an exchangeable partition to an arbitrary finite set (not an initial segment ) is governed by the same EPF. The converse in Lemmas 34 and 35 needs the bookkeeping that the formula on refining pairs exhausts total mass. Lemma 9 is an existence theorem for a projective family of laws, which the paper cites rather than proves.
A partition of is an equivalence relation on Lean's (PInf := Setoid ℕ), a partition of one on Fin n; labels shift by one, which preserves the order of least elements, and block indices are 0-based. The -algebra on PInf is generated by the coordinates , equivalently by the . Coagulation is stated with (Definition 5's case ). The EPF is the cancelled form
equal to (15) for ; this is needed because at . Conditional laws "for all " are encoded as joint laws, and equalities of laws are stated on preimages of measurable sets, so no Measure.map of an unproved-measurable map appears. Fragmenting partitions are one sample of Measure.infinitePi (fun _ => κ). In the sharper form, is written as , since PAR allows .
Not formalized: the stick-breaking characterization (12)–(13) in Lemma 9, Corollary 13 and Kingman's correspondence, and the auxiliary fact "", which as printed fails at .
A formalization in which no measure satisfies IsEPFLaw (pdEPF α θ) would make Theorem 12 and Lemmas 34–35 vacuous; Lemma 9 rules this out and must be proved for the parameters used, not assumed.
Infrastructure needed: cylinder-set uniqueness on PInf, the law of the restriction of an exchangeable partition to a finite set, block enumeration by least elements, and rising-factorial algebra (ascPochhammer). The partition, EPF and kernel definitions are reusable for any work on exchangeable partitions, Chinese restaurant processes or -coalescents. Proofs of Lemma 9, of Lemmas 34–35 and of the EPF identity are each welcome as independent contributions.
Many problems in optimization and equilibrium modelling reduce to a system of nonsmooth equations with locally Lipschitz but not differentiable: reformulations of nonlinear complementarity problems, variational inequalities and Karush–Kuhn–Tucker systems through the function or piecewise smooth maps. Newton-type methods for such systems replace the Jacobian by a directional derivative or a generalized Jacobian and globalize with a line search on the residual .
Global convergence theory for these methods typically shows that every accumulation point of the iterates is a zero of (or a stationary point of ). That leaves open whether the whole sequence converges. L. Qi's 1993 paper in Mathematics of Operations Research (DOI 10.1287/moor.18.1.227) answers this with an attraction theorem: a zero with a nondegenerate directional derivative, once approached, captures the whole sequence of any descent method whose steps are controlled by the residual.
Timeline. Robinson (1987) introduced the B-derivative (as recounted on p. 229 of Qi's paper); Pang (1990, DOI 10.1287/moor.15.2.311) proposed the damped B-derivative Newton method and proved a global convergence theorem under strong conditions at the limit point; Han, Pang and Rangaraj (1992, DOI 10.1287/moor.17.3.586) gave two further globally convergent descent algorithms; Qi and Sun (1993, DOI 10.1007/BF01581275) developed the semismooth Newton method. Qi's 1993 §5 shows that, for convergence of the entire sequence to a zero, BD-regularity at that zero suffices for all three methods, without semismoothness.
Throughout, is locally Lipschitz and is the Euclidean norm. The directional derivative of at in direction is the one-sided limit
is directionally differentiable at if this limit exists for every , and B-differentiable at if moreover
is BD-regular at if it is directionally differentiable there and for every .
A descent direction method produces iterates with step sizes and directions , and is monotone in the residual:
A point is a limiting point of if some subsequence converges to it.
The damped Newton method (Algorithm 4.1) is the special case where solves and is chosen by the Armijo rule on .
Let be locally Lipschitz and B-differentiable, a descent direction method satisfying (5.1), and a limiting point of with and BD-regular at . If there are such that implies and
then
The result. Global convergence theorems for line-search methods usually stop at "every accumulation point is a zero". The attraction theorem upgrades that to convergence of the entire sequence whenever the zero is BD-regular, under assumptions that are checked locally and that hold for several algorithms at once. For the damped Newton method it removes the semismoothness assumption needed for the superlinear local theory, at the price of saying nothing about the rate. The same pattern (local error bound plus residual-controlled steps gives capture) recurs in the convergence analysis of Levenberg–Marquardt and projection-type methods.
Formalizing it. The result is proved in the paper; to our knowledge none of it has been machine-checked. The formalization needs the one-sided directional derivative and B-differentiability, the passage from BD-regularity to a uniform constant, and the trapping argument for sequences with cluster points. These pieces are reusable for any convergence proof of nonsmooth Newton-type methods.
The obvious argument says: near , steps are small because is small, so the iterates cannot leave. This fails as stated: a small residual at does not by itself prevent from being far from , and without a lower bound of in terms of the iterates could drift along a set where is small. The step that needs work is the error bound (5.5), which requires a uniform constant from the pointwise condition , valid in a whole neighbourhood of and not only along the directions the iterates happen to take. The set must also be chosen so that both its defining inequalities are preserved, which ties the radius to the residual through .
Points of are EuclideanSpace ℝ (Fin n); norms are 2-norms; is allowed. The directional derivative is the published one-sided NonsmoothNewton.Local.dirDeriv; every statement that evaluates it does so at a point where existence is assumed (BD-regularity, B-differentiability), so the junk value of an undefined limit never enters. "Limiting point" is a cluster point of the sequence, not its limit. Condition (5.2) is assumed only for iterates within of , as on the page.
Standing assumption and added hypotheses:
A trivializing formalization is ruled out: the goal does not assume that converges, that is bounded, that (5.2) holds globally, or that is semismooth; the hypotheses are jointly satisfiable (for , , , ).
Definitions needed: directional differentiability, B-differentiability, BD-regularity, and for Corollary 5.2 the norm function, the Armijo test (4.1) and runs of Algorithm 4.1. Contributions to the general theory of one-sided directional derivatives of locally Lipschitz maps (Lipschitz continuity and positive homogeneity of ) are welcome and will serve the companion missions of this series.
In a labor market where firms hire sets of workers and salaries are negotiated pair by pair, the natural stability notion is the core: an assignment of workers to firms, with salaries, that no firm and group of workers can improve upon by agreeing among themselves. Kelso and Crawford (Econometrica 50 (1982) 1483–1504) proved that the core is nonempty, and that an ascending salary-adjustment process reaches it, when every firm regards workers as gross substitutes (GS): raising some workers' salaries never makes a firm withdraw an offer from a worker whose salary has not risen. The condition later became central to the theory of matching with contracts, combinatorial auctions and Walrasian equilibrium with indivisible goods (Gul and Stacchetti, J. Econ. Theory 87 (1999); Hatfield and Milgrom, Amer. Econ. Rev. 95 (2005)).
The question this mission addresses is whether (GS) is needed at all. Section 6 of the paper answers it with a concrete market with two firms and three workers in which every other assumption of the paper holds, each firm's technology is even subadditive, and the core is empty.
There are workers and firms , both finite. Worker 's utility of working for firm at salary is ; firm produces with the set of workers , and its profit at the salary vector is
A set is demanded at if it maximizes . Each pair has a reservation salary .
An allocation assigns each worker to a firm with salary ; . It is individually rational if and for all , . A firm and a set of workers strictly improve upon it if some salaries give every strictly more utility than at the allocation and give firm strictly more profit than . A core allocation (definition D3 of the paper) is an individually rational allocation that no such coalition can strictly improve upon. When salaries vary continuously, the range over .
The example. Workers ; firms ; ; (equation (23)); and
Firm is firm with workers and interchanged. In Lean, noCoreMarket : Market (Fin 3) (Fin 2) is this market, techJ and techK are the two technologies, and Market.IsCore anySalary is D3 with real salaries.
The goal then follows by the symmetry of the example.
The paper's existence results (Theorems 1 and 2: the salary-adjustment process converges to a core allocation; a strict core allocation exists with continuous salaries) all assume (GS). This example shows that the assumption cannot simply be dropped, and that the weaker and more familiar condition of subadditivity does not replace it once there are three or more workers, although it does with two (p. 1500). It is the reason gross substitutes, rather than a convexity-like condition on technologies, became the standard hypothesis for existence of equilibrium with indivisibilities.
The result is proved in the paper by a short computation. It has not been machine-checked before: nothing of this paper was on Prove2Me before this series. The mission contributes a checked counterexample, a general efficiency lemma for core allocations with transferable utility (milestone 3), and the computational facts about firm that show (GS) fails. The paper's further remark that the example also has no competitive equilibrium relies on the core–equilibrium equivalence of p. 1487 and is not part of this mission.
This is mission 7 of a series on the same paper; missions 1–6 treat the salary-adjustment process (1), the continuous strict core (2), one-sided markets (3), the firm-optimal allocation (4), comparative statics (5) and the characterization of (GS) for identical workers (6). This mission does not depend on them.
The obstacle is the quantifier over all allocations with real salaries: emptiness of the core is a claim about infinitely many candidates, and checking finitely many salary vectors proves nothing. A direct attempt to find an improving coalition for each allocation by case analysis on salaries does not close, because which coalition improves depends on the salaries. The printed inequality (24) also carries a sign misprint ( in place of ), and copying it would break the contradiction.
0, 1, 2 : Fin 3; firms are 0, 1 : Fin 2. and .A trivializing formalization is ruled out: the core includes individual rationality and real-valued coalition salaries, the technologies are the printed tables, milestones 1, 2 and 4 have no hypotheses, and the hypotheses of milestones 3 and 5 are each satisfiable.
Contributions welcome: proofs of each milestone, and a statement and proof of the symmetry (workers , firms ) used to exclude the second efficient assignment.
Adding a firm changes the offers available to workers; removing a worker changes the pool from which firms hire. In markets with salary bargaining, those changes can alter both assignments and pay. Kelso and Crawford asked whether the direction of the change can nevertheless be predicted at the outcome selected by their salary-adjustment process. Their 1982 paper studies firms that may hire groups of workers whose joint product need not be the sum of individual products. Theorem 5 gives two comparative-statics conclusions for that setting: a new firm leaves each worker at least as well off, and retaining a worker leaves each firm at least as well off.
The result follows the paper's finite-termination and firm-optimality results for the salary-adjustment process. Its comparison is specific to the process equilibrium under the no-ties conditions of Section 5; the paper does not claim that every core allocation moves in the same direction. This mission is the fifth of seven on the paper. Mission 1 concerns termination and the discrete core, mission 2 the continuous strict core, mission 3 a one-sided market, mission 4 firm optimality, mission 6 returns to workers and gross substitutes, and mission 7 the example without a core. The statements here are drafted independently of the other missions' unpublished declarations. None of this paper's statements was previously available on Prove2Me when the series was planned.
A market has a finite set of workers and a finite, nonempty set of firms. Worker 's utility from employment at firm for salary is . Firm produces from a set and earns profit . Workers care about their own firm and salary; the firm's product may depend on the whole set it hires. Every worker–firm pair has a starting salary , and permitted salaries increase by a common unit : for .
Each round of the salary-adjustment process records permitted salaries, offers from firms, and one tentatively accepted offer for each worker who receives any. Firms choose profit-maximizing sets of workers at current permitted salaries and repeat offers that were not rejected. A worker keeps a favorite available offer. A rejected worker–firm offer causes that pair's permitted salary to rise by next round. The process stops when no offer is rejected. An allocation assigns each worker one firm and a salary at that firm; an outcome is the allocation read from a stopping round. The paper calls this a process equilibrium.
An allocation is in the discrete strict core when each worker's salary is permitted and meets the starting salary, each firm's profit is nonnegative, and no firm together with a set of workers can make every participant weakly better off and at least one strictly better off using permitted salaries. The weaker discrete core excludes coalitions that make everyone strictly better off. The paper assumes workers' utilities are continuous and strictly increasing in salary; marginal product (MP) makes hiring an additional worker at the starting salary weakly profitable; no free lunch (NFL) sets the product of the empty set to zero; and gross substitutes (GS) lets a firm keep workers whose salaries did not rise when other workers' salaries increase. Section 5 adds no-ties conditions (NTW) for workers and (NTF) for firms relative to discrete-core allocations. These assumptions and their domains come from Sections 2 and 5.
The preliminary target is the paper's Corollary to Theorem 4: under these assumptions, all legal runs that stop have the same outcome. A second target is the new-firm-on-the-block process claim stated in the proof of Theorem 5: starting from the original market's final salaries, its outcome is a firm-optimal discrete strict core allocation of the augmented market.
The goal is Theorem 5. Write , and for stopping outcomes in the original market, the market augmented by one firm, and the market without one named worker. The two conclusions are
The first comparison concerns every original worker's utility. The second concerns every original firm's profit. The augmented market retains the original firms' technologies, utilities and starting salaries, and the diminished market restricts those data to workers other than the removed one. All three markets use the same and satisfy the conditions of Theorem 4.
The theorem gives a direction for the effects of entry and worker exit even though assignments and salaries may both change and a firm's product may depend on its entire workforce. The comparisons are individual: every worker is covered by the entry conclusion and every firm by the exit conclusion. Process uniqueness makes these comparisons well-defined despite the choices of favorite sets and favorite offers that a legal run may make.
The mathematical claims were proved in the 1982 paper; the Lean statements in this mission are open proof obligations. The formal development would give reusable finite-market definitions of demand, gross substitutes, core blocking, and an explicit adjustment run. It would also make precise how outcomes in markets with different agent sets are compared. The Corollary and the new-firm process result are separate proof targets. Completing them would support the goal while keeping the paper's two comparative-statics conclusions together.
Firm entry changes which firm can make the best offer, and worker exit changes which subsets of workers a firm can hire profitably. A direct pointwise comparison of old and new assignments has no fixed correspondence: a worker may switch firms and a firm may hire a different group. Comparing arbitrary strict-core allocations is also insufficient, because Theorem 5 concerns the specific outcome chosen by the adjustment process. The formal proof must account for all legal tie choices and show that the identified stopping outcomes have the required utility and profit order. The paper's proof uses two modified processes; its take-my-marbles process raises the removed worker's salary to a value that need not belong to the discrete salary grid on which (GS) was assumed. This is a genuine modeling boundary for that intermediate statement.
Workers and firms are finite Lean types, with at least one firm. Salaries, utilities and products are real-valued; is positive. An allocation assigns every worker to a firm, as the paper's does. Option F represents firm entry: some j is an original firm and none is the entrant. The diminished worker set is the subtype of workers unequal to the removed worker. Gross substitutes is imposed only on the grid vectors each market permits, and (NTW) and (NTF) quantify over discrete-core allocations. Each theorem's assumptions explicitly include utility regularity, MP, NFL, GS, NTW and NTF wherever the paper says “the conditions of Theorem 4.” Section 5 allows starting salaries to vary independently of unemployment utility, so the reservation-salary equation from Section 2 is not imposed.
“The equilibrium” is represented by the outcome at any stopping round of any legal run; the Corollary states why this does not depend on those choices. “Converges in finite time” in the new-firm milestone means that each legal continuation has some stopping round. NFB's initial offers are fixed to the old firms' final offers and an offer from the new firm to every worker, a reading of the first round that NFB1 leaves implicit. The take-my-marbles convergence claim is not drafted because its off-grid starting salary requires a separate convention or a stronger GS assumption. These commitments exclude a vacuous market condition, a continuous-price substitution for the discrete theorem, and a comparison of unrelated markets. Contributions that establish the Corollary, the NFB claim, or the three-market comparison under these definitions are welcome; lemmas about demand and core allocation can be reused across the series.
Prediction with expert advice asks how a learner should combine the forecasts of a pool of prediction algorithms when nothing is assumed about the data: the instances and labels may be chosen by an adversary, and the learner's performance is compared with that of the pool. Littlestone and Warmuth's The Weighted Majority Algorithm (Inform. and Comput. 108, 1994) introduced the multiplicative-weights master algorithm WM for binary pool predictions and proved that its number of mistakes is at most logarithmic in the pool size plus a constant times the mistakes of the best pool member. The same multiplicative update now underlies boosting, online convex optimization and approximate solvers for linear programs and zero-sum games (Arora, Hazan, Kale 2012).
In many applications the pool members do not output a bit but a degree of confidence in , while the master must still commit to a binary decision. Section 5 of the paper treats exactly this setting with the algorithm WMG, and shows that WM's mistake bound survives unchanged.
A nonempty pool of prediction algorithms is run on a finite sequence of trials. In trial the pool member predicts , the master predicts , and then the binary label is revealed. The master keeps a non-negative weight per pool member, with positive initial weights. Write
and , the total weight after the last trial.
WMG with parameter predicts if and if ; at either prediction is allowed. A mistake is a trial with , and is the number of mistakes. An update step multiplies every weight by a factor
with . WMG executes an update step in every trial, or only in mistake trials; more generally (footnote 8 of the paper) in every mistake trial and possibly in others. Outside update steps the weights do not change. When the are binary, WMG coincides with WM.
For every run of WMG with , whatever the tie-breaking, the update criterion and the factors in (5.1), if then
The bound involves only the total weights, not the losses of individual pool members; Corollary 5.1 of the paper, which compares with the total absolute loss of each pool member, follows from it and from the lower bound in (5.1).
The paper gives two proofs of Theorem 5.1, one through each milestone; the second also uses Lemma 5.2, the potential lemma shared with the continuous master WMC, which is posed in the companion mission on WMC.
Theorem 5.1 says that the master's mistake count is controlled by how much total weight the pool loses, with the same constant as for binary pools. With equal initial weights it gives Corollary 5.1: WMG makes at most mistakes for every pool member , so pool members may report graded confidences at no cost in the master's guarantee. The same weight-potential argument is the template for the randomized master WMR of §6 and for later analyses of exponential weights.
The result is classical and proved in the paper. What this mission adds is a machine-checked statement and proof against the paper's own model: a relation that covers both update criteria, all tie-breaks at and the whole interval of admissible factors, rather than a single deterministic instance. No formalization of WMG or of Theorem 5.1 is known; the platform's existing weighted-majority results (Hazan's textbook version) concern binary experts, unit initial weights and a fixed update factor.
The obvious argument, copied from WM, tracks the weight of members predicting and the weight of members predicting . With predictions in a member supports both outcomes, and the update factor is only constrained to an interval, so the two-bucket bookkeeping must be redone for fractional contributions. The factor's upper bound is affine in , while the natural exponential factor is convex; the argument must use the right one of the two bounds of (5.1). A further subtlety is the case : a factor may be , the total weight can vanish, and both the logarithmic bound and the weighted average degenerate.
Fin n with , and the trials are Fin T, all trials of the sequence; weights are w : ℕ → Fin n → ℝ, with w 0 the initial and w T the final weights.Real.rpow (so ).Real.log is used.Real.log 0 = 0 would turn the paper's vacuous bound into the false claim ; with it, no Lean junk value enters the statement.A complete development needs only finite sums, real logarithms and real powers from Mathlib. Proofs of either milestone, of the existence of a run for every input (using Lemma 5.1, ), and of Corollary 5.1 on top of the goal are welcome.
A random discrete distribution is a random sequence of frequencies with . Such sequences model the relative sizes of species in a large population, of allele classes in population genetics, of cycles of a random permutation, of prime factors of a random integer, and of the excursion intervals of a Brownian motion or Bessel process. The two-parameter Poisson–Dirichlet family , , , contains Kingman's one-parameter law (Ewens sampling formula, random permutations) and the law of the ranked jumps of a stable subordinator. It is the reference prior in Bayesian nonparametrics (the Pitman–Yor process) and the reference model in the combinatorics of random partitions.
J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator (Ann. Probab. 25 (1997)), extend what was known for and to the whole family. This mission formalizes one of their results: an identity (Proposition 19, p. 867) that describes the law of the largest frequency under through the law of the largest frequency under .
Timeline. McCloskey (1965) showed that sampling from discovers the frequencies in the stick-breaking order of independent variables. Dickman (1930) found the distribution of the largest prime factor; Vershik (1986) recorded it as the case , of an equation of this form. Engen (1978) introduced the two-parameter stick-breaking scheme for . Perman, Pitman and Yor (1992) and Pitman (1996) proved that this scheme is the size-biased permutation of the ranked frequencies for the whole parameter range (Proposition 2 here). Pitman and Yor (1997) derived (52) for all , .
Fix and . Let be independent random variables, having the beta distribution , with density on for , . Break a stick of length one:
Let be the ranked values of the pieces . The law of is (Definition 1, p. 857); denotes probability for this construction.
A random variable is a size-biased pick from if for every : it is the frequency of the species of an individual drawn at random. A size-biased permutation continues the sampling without replacement, (2) and p. 857. A sample from is a random index with (113).
In Lean all sequences are ℕ → ℝ, 0-based (V ω 0 is ); the objects are stick, ranked, IsStickLaw, HasPD, IsSizeBiasedPick, IsSizeBiasedPerm, IsSample, deleteAt, insertAt in the namespace PoissonDirichlet.MaxDensity.
For , , the variable lies in almost surely and
The result. The law of under has no closed form. Identity (52) is a functional equation in the parameter: on the last factor equals one and the density is explicit; on it is expressed through the law of under on . Specialised to , it is Dickman's equation for the largest prime factor of a random integer and for the longest cycle of a random permutation. The size-biased tools of the milestones (Corollary 3, (6), Propositions 34 and 35) are the standard way to compute with and its partition structure.
Formalizing it. All results here are proved in the literature; none is formalized. Mathlib has the beta distribution, infinite product measures, independence and conditional expectation, but no random discrete distributions, no ranking of a countable sequence, and no size-biased sampling. The mission produces these objects and the first theorems about them: the identification of the stick-breaking scheme with the size-biased permutation of the ranked frequencies (cited by the paper, not proved there), the structural distribution, and the density identity.
The obvious obstacle is Proposition 2: the identification of the stick-breaking order with the size-biased order of the ranked values is a statement about conditional probabilities given an infinite sequence, it is only cited in the paper, and its proof (Perman–Pitman–Yor, Pitman) goes through exchangeable partitions or Poisson point processes. Everything else in the mission rests on it. A second obstacle is the events themselves: coincides with only because the pieces are almost surely distinct, and conditioning on needs the independence of the renormalised tail from , which is not a pointwise identity but a statement about infinite product measures. Reading (52) off the page as a pointwise identity of densities is not enough: densities are defined only almost everywhere.
The parameter range , of Definition 1 is a hypothesis of every statement; is included. A sequence "has the distribution" (HasPD) if it is a.e.-measurable and, for some law of independent beta variables as in Definition 1 (IsStickLaw), for every measurable . Ranked values are defined with Set.encard, so infinitely many large terms are never counted as zero. Conditional probabilities are conditional expectations of indicators; size-biased picks, permutations and samples are measurable random variables, an assumption the page makes implicitly. Expectations of nonnegative functions are lower Lebesgue integrals. The density identity is an equality of measures on Borel subsets of , with two probability spaces for the two parameter values. Indices are 0-based. Insertion (p. 881) is defined with the index for the shifted tail, where the page prints .
The formalization rules out the trivial readings: no Measure.map of a possibly non-measurable map (which would be the zero measure), no Set.ncard in the ranking, no Bochner integral of a possibly non-integrable function (whose value would be ), no limUnder, and no dropped parameter range. Corollary 3 quantifies over every pick from every sequence, not over the stick-breaking construction where it is the hypothesis. A sorry-free check shows that IsStickLaw is inhabited for every admissible , so HasPD is not vacuous.
Contributions are welcome at every level: measurability of ranked, the law of the renormalised stick tail (infinite product measures), Proposition 2 through exchangeable partitions, and the recursion of the uniqueness statement, which is pure measure theory. The definitions are reusable by the other missions of this series.
The Shapley value (Shapley 1953) is the most widely used single-valued solution of cooperative games with transferable utility. It is usually justified axiomatically, from cooperative principles. A recurring question in game theory, sometimes called the Nash program, asks whether cooperative solution concepts can also be recovered from the strategic behaviour of players in a non-cooperative game.
Section 6 of Monderer and Shapley, Potential Games (Games and Economic Behavior 14, 1996), gives such a recovery through the notion of a potential game, the central object of that paper. With every solution , vector of outside options and TU game it associates a simple non-cooperative participation game, in which each player decides whether to join. The Shapley value is then characterised, among efficient solutions, as exactly the solution for which every such participation game is a potential game. The characterisation rests on the potential of a TU game introduced by Hart and Mas-Colell (1989), whose marginal contributions are the Shapley value; Monderer and Shapley connect that cooperative potential to the strategic one of their paper.
Let be a finite set of players.
A game in strategic form has strategy sets and payoff functions on . Writing for the profile with player 's strategy replaced by , a function is an exact potential if
for every , every and all (condition (2.2) with unit weights). A game with an exact potential is a potential game.
For a coalition , is the space of TU games on : real functions on the subsets of with . A solution assigns to every a payoff vector . It is efficient if for every and every . For , is its restriction to the subsets of . The Shapley value of is
Given a solution , a vector and , the participation game has player set and strategy sets . Player either stays out (0) and receives , or participates (1). With the set of participants at the profile ,
For , is the profile in which exactly the members of participate.
In Lean these are IsPotential, IsPotentialGame, Solution, IsEfficient, shapleyOn, joiners (), profileOf () and participationPayoff, all in the namespace MondererShapley.Participation.
For every efficient solution , every and every ,
An efficient is the Shapley value on all of iff is a potential game for every .
Theorem 6.1 is a local characterisation: for a single game it identifies the Shapley value of all subgames of through a property of one non-cooperative game, for any outside options . Theorem 6.2 turns it into a global axiomatisation of the Shapley value among efficient solutions, with "every participation game has a potential" in place of the usual symmetry, null-player and additivity axioms. It links the cooperative potential of Hart and Mas-Colell to the strategic potentials of Monderer and Shapley, and through the latter to the existence of pure equilibria and the convergence of improvement dynamics in the participation games.
Both theorems are proved in the paper, on the basis of Hart and Mas-Colell's Theorem A. To the curators' knowledge no machine-checked proof exists: neither the Hart–Mas-Colell potential nor its identification with the Shapley value of subgames is formalized on Prove2Me or in Mathlib. A complete development therefore formalizes the paper's reduction (milestones 1–3) and, as its substantial part, the Hart–Mas-Colell characterisation (milestone 4), which is reusable for any later work on cooperative potentials, consistency and the Shapley value.
Milestones 1–3 are bookkeeping on profiles in ; the obstacle is the identification of the potential of a game on with a function of coalitions, which is a translation between two indexings rather than an idea. The substance is milestone 4, which is Hart and Mas-Colell's Theorem A specialised to the subgames . The condition (6.3) speaks of marginal differences of an unknown function on coalitions, while the Shapley value is a closed weighted sum over subsets of whose weights depend on ; relating the two requires a genuine combinatorial identity over the subset lattice of every coalition, in both directions, and efficiency of on every subgame is used essentially. Unfolding the definitions does not suffice for either direction.
ι with decidable equality; the strategy set is Bool (false = 0, true = 1). is Function.update ε i x.Finset ι; a TU game is w : Finset ι → ℝ, with "" encoded as w ∅ = 0 and only the values on subsets of meant. A solution is ψ : Finset ι → (Finset ι → ℝ) → ι → ℝ, ψ S w standing for ; only the coordinates are read. This admits solutions that look at values of w outside , so the Lean statements cover every solution of the paper and more; " is the Shapley value on " is ∀ S, ∀ i ∈ S, ψ S v i = shapleyOn S v i.shapleyOn is supplied: the paper uses the Shapley value without defining it. Its weights use , the size of the subgame's player set.v ∅ = 0 is kept as the meaning of (without it, efficiency does not constrain ψ S v); and the potential is an exact potential on all of , not only on profiles of a special form.The probability that a sum of independent random variables exceeds a large level is a central quantity in large deviation theory. It appears, for example, when relating tail assumptions on individual summands to the tail of their sum. For summands with light (exponentially decaying) tails, exponential bounds are often effective. For heavier tails, a large value of the sum can instead be produced by one large summand. Nagaev's survey studies bounds that make the contribution of such summands explicit.
S. V. Nagaev's survey Large deviations of sums of independent random variables, Ann. Probab. 7 (1979) collects upper bounds of this type. Its best-known result, the Fuk–Nagaev inequality (Theorem 1.3, p. 749), bounds from above by plus an explicit term built from truncated moments. Upper bounds alone do not show that the one-summand term is necessary. At the end of §1 (pp. 758–759) the paper gives a complementary lower bound that needs neither identical distributions nor regular variation of the tails, only centred summands with finite variances. This mission formalizes that lower bound and the steps of its proof.
Timeline. Fuk and Nagaev (1971) proved truncation inequalities of this kind; the survey refers to that paper for the proofs of its Theorems 1.1 and 1.2 (p. 752). A. V. Nagaev (1969) obtained the asymptotics of Theorem 1.9 (p. 753) for identically distributed, centred summands with tails , , slowly varying; in the range where one summand dominates, the survey's own argument gives , display (1.46), p. 756. The lower bound treated here (1979, p. 759) drops both the identical-distribution and the regular-variation hypotheses in exchange for explicit constants (, and in place of ).
Let be a probability space and independent real random variables on it. The paper writes
Throughout, is the level (p. 747). For an index , the sum without the -th summand is
and the one-big-summand probability is
the probability that the sum reaches while is the only summand that does.
In the Lean development these are S n X, Sj n X j, Bn2 P X and Pj P X x j, in the namespace NagaevLD.LowerBound.
Assume for every and . Then for
The result. Set beside the Fuk–Nagaev upper bound, the lower bound shows that in the range the probability is at least a fixed fraction of a one-summand term, , for any centred summands with finite variances. It is valid for every and every family of independent, centred, square-integrable summands, with no asymptotic regime and no tail regularity. It is a non-asymptotic counterpart of the asymptotics for regularly varying tails, and it indicates that the term in upper bounds of Fuk–Nagaev type cannot be removed.
Formalizing it. The result is proved in the 1979 paper; the local Prove2Me catalogue search found no exact formal statement of this bound. A formal proof would produce a reusable lower bound for tails of sums of independent variables and the decomposition (1.57) into one-big-summand events, which applies to any family of real random variables.
The individual steps are short. The step that needs care is the bound on : it requires the event to be independent of the event , which is generated by the other summands. Deriving this from mutual independence of means grouping the summands into and its complement and passing to a function of the complementary block. The first Chebyshev bound similarly needs the variance of to equal , again by independence of a sub-family. A naive union bound for one alone does not give the sum over : the decomposition into the disjoint events of (1.57) is what makes the sum appear.
X : Fin n → Ω → ℝ on a probability space, measurable and mutually independent (iIndepFun); the paper's are X 0, …, X (n-1). Probabilities are P.real of sets, with , and exactly as printed.MemLp (X i) 2 P). Mathlib's variance returns for a variable that is not square integrable, so without this hypothesis could be while the summands have infinite variance, and the goal would be false. is stated as .Random discrete distributions — a random sequence of nonnegative frequencies summing to one — model the relative sizes of species in a population, of cycles in a random permutation, of excursion intervals of a Markov process, and of clusters in Bayesian nonparametric models. The two-parameter Poisson–Dirichlet law is the family that contains Kingman's one-parameter law (Ewens sampling, random permutations) and the law of ranked excursion lengths of a stable subordinator. J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator (Ann. Probab. 25 (1997)), developed its distribution theory systematically. In Bayesian nonparametrics the same family appears as the Pitman–Yor process prior.
A basic quantitative question about any random discrete distribution is the size of its -th largest atom. This mission formalizes the paper's answer for : every moment as one explicit integral.
Timeline. The moment formula for (Corollary 18 below) was known before 1997 (references [63, 73, 25, 50] of the paper). The Laplace transform of under was obtained, in different settings, by Darling (1952) and Lamperti (1961) for and by Wendel (1964) for . Perman, Pitman and Yor (1992) proved that has density a constant times relative to . Pitman and Yor (1997) combined these into Proposition 17.
Fix and . Let be independent with , the law with density on . Break a unit stick:
and let be the ranked values of the . The law of is (Definition 1); denotes expectation under it.
For and the paper introduces
Under the local time exists almost surely. From one derives , (with ) and . Finally
The Lean declarations Xseq, pdConst, and expIntE are in PoissonDirichlet.Moments; the other objects come from the frozen shared PoissonDirichlet.Ratio and PoissonDirichlet.Wendel modules.
For , , with , and ,
Two consequences close the list: (50), , and Corollary 18, the formula
The ranked frequencies of have no tractable joint density; their one-dimensional laws are known only through transforms. Proposition 17 makes every moment of computable by a single quadrature, for all parameters at once. It yields the large- decay (50), in mean, and recovers the classical formula in the limit . The intermediate statements, the conditional Wendel formula and the joint moments , are used elsewhere in the paper (Proposition 16, Lemma 29).
All statements are proved in the 1997 paper, except Proposition 14, which the paper quotes from Perman, Pitman and Yor (1992). To our knowledge none of them has been machine-checked. A formal development would produce the first verified construction of the Poisson–Dirichlet family in Lean, together with reusable facts about stick-breaking with beta variables, ranked rearrangements of sequences, and the Laplace-transform representation of negative moments.
The identity (86) and the final integration are elementary. The difficulty lies upstream. The naive route, computing from the stick-breaking definition, fails: is the -th ranked value of the , and ranking destroys the product structure of the beta variables. The paper instead works under , where the ranked sequence is the normalized sequence of points of a Poisson random measure (equivalently, transformed arrival times of a unit Poisson process). Proposition 14 is itself a deep change-of-measure result about stable subordinators, and the existence of the local time is an almost sure limit theorem. Neither has any counterpart in Mathlib.
Sequences are indexed from in Lean: the paper's is V ω (n-1), and statements "for " quantify over k : ℕ with . is defined exactly as Definition 1, with independent beta coordinates (Mathlib's betaMeasure) and the ranked values defined with Set.encard. The law is stated through preimages, so no measurability of the ranking map is presupposed. The local time is carried as a random variable together with its defining almost sure limit (24). Expectations of quantities that may be infinite are lower integrals. The conditional expectation of Proposition 26 is stated through its defining property, for every nonnegative measurable test function of . The parameter ranges , (and at ) are hypotheses wherever the page has them. Two hypotheses are added and disclosed: in Proposition 17 and in Lemma 27. Without them the printed -integrals diverge and is evaluated at a pole or a negative argument, while the left sides are finite. Both follow from the printed hypotheses when (resp. ).
Trivializing encodings are ruled out: no law is written as an image measure of a possibly non-measurable map, no count uses Set.ncard, no limit uses limUnder, is not defined as , and every Bochner integral in a statement is of an integrable function under the stated hypotheses, so no statement holds because of a junk value .
A complete development needs: infinite products of beta laws, the ranked rearrangement and its measurability, the Poisson-process representation of (Proposition 10), and the change of measure of Proposition 14. These are reusable beyond this mission. Proofs of the general identity (86), of the gamma–independence milestone, and of Lemma 27 from its milestones are welcome independently.
A value for cooperative games assigns to every game a payoff vector, chosen by axioms rather than by bargaining. Shapley's value (1953) does this for finite games with side payments, and Aumann and Shapley (Values of Non-Atomic Games, 1974) extended it to games with a continuum of players, where it is given by a diagonal formula: a player's value is the average of their marginal worth along the diagonal from the empty coalition to the grand coalition. Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6(1), 1981, doi:10.1287/moor.6.1.1) brings this formula to finitely many players who may participate in coalitions at fractional rates, and characterises it by axioms in §8.
The result matters in cost allocation: the Aumann–Shapley price mechanism (Billera, Heath and Raanan 1978; Mirman and Tauman 1982) shares the cost of a bundle of products by exactly this diagonal formula, applied to a smooth cost function of the quantities produced. Theorem 8.1 is the finite-player, fuzzy-coalition version of the axiomatic justification behind that mechanism.
There are players . A fuzzy coalition is a vector , where is the rate at which player participates; an ordinary coalition is its indicator vector , and is the grand coalition.
A smooth fuzzy game is a coalitional worth function that is continuously differentiable and satisfies . These form the space , a Banach space under the norm .
A sequence of fuzzy values is a family of continuous linear operators satisfying three axioms.
The core of a game with side payments is the set of with and for every (§2 (4)).
There exists a unique sequence of fuzzy values, given by the diagonal formula
For every linear with ,
where is the transpose of . If is concave and positively homogeneous, then is the unique element of the core.
These are the steps of the proof in the paper (pp. 10–11), in attack order:
The result. Theorem 8.1 singles out the diagonal formula among all ways of valuing smooth fuzzy games, using only efficiency, anonymity and invariance under merging players into types. Property (5) shows that the value transforms correctly under every linear change of coordinates fixing the grand coalition. The core statement links the value to stability: for concave homogeneous games (for instance, market games), the value is the only allocation no fuzzy coalition can improve upon. Through Owen's extension, the classical Shapley value is recovered as a special case.
Formalizing it. The theorem is proved in the paper, briefly, and its proof leans on an unproved density claim and on a short appeal to atomicity. A formalization makes the uniqueness argument complete: in particular, how atomicity, which only allows nonempty types, determines the value of a monomial in which some player has exponent . No machine-checked version of the Aumann–Shapley diagonal formula or its axiomatisation is known to us. Mathlib has the Stone–Weierstrass theorem for continuous functions but no density of polynomials on a cube; the latter is reusable well beyond game theory.
Existence (milestones 1–2) is calculus: differentiation under the integral sign and the chain rule. The difficulty sits in uniqueness. The first idea, computing on monomials by symmetry alone, fails as soon as the exponents differ: symmetry relates only games that are permutations of each other. Atomicity relates games with different numbers of players, and its types must be nonempty, so a player with exponent cannot simply be merged away. Uniqueness on all of then needs density of polynomials in the norm, not merely the uniform norm: without continuity in the norm, linear maps that agree on polynomials can disagree elsewhere, and the theorem is false.
Fin n, fuzzy coalitions and payoff vectors are Fin n → ℝ, and the cube is Set.Icc 0 1 in the product order.Fin n → Fin m. The symbols are .Supermodularity.Cooperative.ShapleyValue, whose formula is (7) re-indexed by . The Cornet extension of the same remark is left out because it is not on the boundary of the cube.Infrastructure that a complete development needs, and that is welcome as separate contributions: approximation of functions on a cube by polynomials; differentiation under the integral sign for the diagonal integral; Euler's identity and the supergradient inequality for concave homogeneous functions.
Random equations of the form , with a random function independent of , describe the stationary laws of many stochastic recursions: perpetuities in insurance and finance, the stationary law of ARCH-type volatility models, random difference equations , and the stationary workload of certain queueing and storage models. When acts like multiplication by a random variable for large , and for some , the solution has power-law tails: . This is the implicit renewal theorem of Goldie (Ann. Appl. Probab. 1991, Theorem 2.3), which recovers and extends Kesten's 1973 theorem on random difference equations.
A tail asymptotic alone says nothing about how fast approaches . For tail estimation, for the accuracy of extreme-quantile approximations used in risk management, and for second-order regular variation, the rate matters. Section 3 of the same paper answers this: under an exponential moment condition slightly beyond the Cramér condition, the error has an explicit second-order term determined by the zeros of , where is a tilted law of , plus a remainder .
Timeline: Kesten (1973) proved power tails for random difference equations; Grincevičius (1975) developed an implicit-renewal approach; Stone (1966) decomposed exponentially decaying renewal measures into an absolutely continuous part with explicit asymptotics and a finite part; Ganelius (1962) proved the Tauberian remainder theorem used to unsmooth; Goldie (1991) combined these into the rate result formalized here.
Let be a probability space carrying independent real random variables and . Fix with (the Cramér condition, (2.3)) and with (3.3).
The tilted law of is the probability measure on , computed on . Its transforms are for real and for complex ; for a function , . Convolution powers are , , and the renewal measure is . A law is spread out when some convolution power has a nonzero absolutely continuous component; (3.4) asks this of the conditional law of given .
Set and
with and defined the same way for the lower tail. The strip is , and denotes a positively oriented closed contour in enclosing every zero of in .
If, in addition, for some , with , absolutely continuous and , and on , then implies
with the analogous statement for ; and if with independent of , the integrability hypotheses may be replaced by . The theorem also asserts that is a spread-out probability measure.
Theorem 3.2 turns the first-order tail asymptotic of the implicit renewal theorem into an expansion: the second-order terms are finitely many terms of the form times oscillating factors, one family for each zero of with , and their form does not depend on the unknown law of . It applies to every random equation covered by the implicit renewal theorem once the stronger moment condition holds, including perpetuities and the random difference equation. Theorem 3.1 is of independent use: it is an explicit-rate version of Stone's decomposition of renewal measures with exponential moments.
The results are proved in the paper; none is formalized. Mathlib has the Fourier transform on the real line, convolution of measures, and rectangle Cauchy theorems, but no renewal theory, no Stone decomposition, and no Tauberian remainder theorem. Formalizing the mission produces a machine-checked renewal density expansion and a checked Beurling–Ganelius theorem, both reusable outside this paper.
The first-order theorem follows from the key renewal theorem applied to . That route gives no rate: the key renewal theorem has no remainder, and the integrability hypothesis yields but not , so a remainder cannot be read off directly even with a spread-out step law. The proof therefore works with a smoothed version of , where Stone's decomposition with the contour expansion of the renewal density gives an remainder, and has to unsmooth. Unsmoothing is the Tauberian step: it requires a one-sided regularity condition on the unsmoothed function, verified for and for the contour term, and costs half the exponent. The contour expansion itself requires showing that has finitely many zeros in the strip and handling their orders through residues.
All objects live in the namespace GoldieRenewal.Rates. Random variables are measurable maps on a probability space; almost surely; independence is IndepFun. Tail probabilities are real numbers P.real {ω | t < R ω}. Moments such as and are lower Lebesgue integrals in . The transforms and are Bochner integrals at complex arguments with the sign of the paper. Asymptotic statements use Asymptotics.IsBigO and IsLittleO along atTop.
The contour. A contour is the positively oriented boundary of an axis-parallel rectangle whose closure lies in and whose interior contains every zero of in ; the contour integral is the sum of the four edge integrals (RectangleIntegral, from the published ResidueCalcOnRectangles_defs). Expansions are stated for every such rectangle.
The variable in (3.8) and (3.10). The paper prints in the contour term, but its proof establishes the expansion in the logarithmic variable . The targets are stated with , which is what the proof gives. With the printed the contour term would decay exponentially and the statement would claim , which is not what is proved. Hypothesis (3.7) is printed with and is read with .
Excluded trivializations. The contour term may not be dropped; the hypotheses do not exclude zeros of in ; and the contour must enclose all zeros in the strip, not a chosen subset.
Theorem 9.6 is stated for a complex-valued kernel and a finite strip width ; the application with follows by restricting to a finite strip. Lemma 9.5 carries an added hypothesis that the density of has compact support, which the proof uses and the application provides.
Contributions welcome: renewal-measure infrastructure (convolution powers, Blackwell-type limits), Fourier analysis of measures at complex arguments, residue computations on rectangles, and Tauberian remainder theory. Each is reusable well beyond this paper.
A forward equation evolves from an initial random value, while a backward equation is constrained by a terminal random value. When the two unknown processes appear in both equations, these boundary conditions can be incompatible. Such coupled systems occur in stochastic control, where a state moves forward and a cost or adjoint variable is determined backward. Antonelli's 1993 paper studies existence and uniqueness for a class of backward–forward stochastic differential equations and gives explicit examples showing why its smallness assumption on the coefficients cannot be discarded (Antonelli 1993, §§1 and 3).
This mission formalizes the first of those examples. It is a deliberately small two-equation system: both integrators are ordinary time, the coefficients are deterministic, and the Lipschitz constant is one. Nevertheless, the system has no solution when the time horizon reaches one. The claim identifies a genuine boundary for the paper's existence result rather than a failure caused by exotic stochastic integration. Antonelli presents it immediately after the existence theorem to show what can go wrong beyond the theorem's coefficient bound (Antonelli 1993, Theorem 3.1 and Example 1).
Fix a probability space and a filtration . The filtration satisfies the usual hypotheses: it is right-continuous, and contains every subset of every -null set. Let be a deterministic horizon. The initial random variable is -measurable, and the terminal random variable is -measurable. Both are integrable and strictly positive almost surely. These choices specialize the filtered space and input assumptions of §3 to Example 1 (Antonelli 1993, pp. 777, 785, 790).
The unknowns are two real-valued stochastic processes and . Their norm is
Thus a solution is a pair in of adapted processes satisfying a forward integral equation and a backward conditional-expectation equation almost surely at each time . Under the usual hypotheses every -class solution has such a representative, so this is the paper's solution class. The system uses and the constant input process . In this specialization, the measure used in the paper is , and the variation control process is (Antonelli 1993, (3.1)–(3.3), pp. 785–786).
The forward coefficient is and the backward coefficient is . Each has Lipschitz constant one with respect to . The absolute value is part of the example: it appears in the forward equation and does not appear in the backward equation (Antonelli 1993, (3.6)–(3.7), p. 790).
For every horizon and all data satisfying the assumptions above, there is no pair satisfying
This is Example 1's conclusion, including the boundary case (Antonelli 1993, pp. 790–791).
The milestones follow the four statements written in the example: representations of and in terms of each other, positivity and passage to the linear system (3.8)–(3.9), the martingale identity for their sum, and the identity for its constant mean . Their full text and page provenance are attached to the milestone list. The goal remains nonexistence for every ; it does not assert a particular formula for a solution.
The preceding existence theorem assumes a coefficient bound that becomes in this time-integrator case. Example 1 has and shows that the system can fail to have a solution as soon as that strict inequality fails. At , the obstruction is already present, so replacing by would lose part of the paper's conclusion (Antonelli 1993, p. 791).
A formalization would make the failure precise for the same solution class used by the paper. The current mission contains compile-checked Lean statements and definitions; the theorem proofs are still open. A complete development would also provide reusable statements about jointly measurable conditional-expectation versions, finite-horizon time integrals of processes, and martingales arising from coupled equations. These can support the paper's neighboring existence and nonsingular-example missions.
The main difficulty is the coupling between the two boundary conditions. The forward equation starts at , while the backward equation ends at ; neither equation can be treated as an independent ordinary differential equation. The absolute value in the forward coefficient also prevents the coupled system from being treated as a linear system at the outset. A second difficulty for Lean is that conditional expectation is defined only up to almost-sure equality at each fixed time, whereas the solution equations are equalities over time and probability together. The formal statement must connect these two kinds of almost-everywhere equality without strengthening the theorem to an identity at every time on every sample path.
Time is represented by , with only used in the norm. Time integration is Lebesgue integration on ; endpoints have zero mass. The norm is an extended nonnegative lintegral, so a nonintegrable process cannot be assigned the value zero by a real-valued integral's fallback convention. The random variable inside each conditional expectation is required to be integrable. The conditional-expectation process is a jointly measurable version whose value at each time agrees almost surely with the conditional expectation. The solution predicate asks, for each , that and be -measurable, that the two equations hold -almost surely, and that the time integrands be integrable along almost every path. Any -class solution can be replaced by such a representative, and the conditional-expectation version, so non-existence in this class is non-existence in the paper's class. For the Lipschitz coefficients in this example, finite norm gives pathwise integrability almost surely for the time integrals used in the equations.
The paper calls and “positive.” Here that means strictly positive almost surely. The weaker nonnegative reading would admit the zero pair when both data are zero and would falsify the target. Integrability of makes explicit §3's standing bound on the constant input process. The completeness and right-continuity of the filtration are also explicit. The solution class and equations are defined for general ; the restriction belongs only to the nonexistence theorem. For example, on a one-point probability space with , , the deterministic pair , solves the equations on . This rules out a definition that makes all solutions impossible by construction.
The development needs Mathlib's filtration, conditional expectation, probability measure, and integration APIs. Contributions proving the milestone statements or supplying reusable lemmas for their and martingale interfaces fit the mission. No semimartingale stochastic integral is required for this example.
A backward stochastic differential equation (BSDE) prescribes the terminal value of an adapted process instead of its initial value. Pardoux and Peng (1990) proved existence and uniqueness for Lipschitz coefficients, and BSDEs have since become a standard tool in stochastic control, mathematical finance and the probabilistic treatment of semilinear PDEs. El Karoui, Kapoudjian, Pardoux, Peng and Quenez (1997) introduced the reflected BSDE, whose solution is constrained to stay above a given obstacle process. Reflected BSDEs describe the price of American options in nonlinear markets (El Karoui, Pardoux and Quenez 1997), Dynkin games (Cvitanić and Karatzas 1996), and obstacle problems for parabolic PDEs.
In §7 of the 1997 paper the coefficient is assumed concave. Then the solution of the reflected BSDE is the value of a game: one player chooses a stopping time, the other chooses a control that sets the discount rate and the change of measure, and the value does not depend on which player moves first. This mission formalizes that statement (Theorem 7.2) and the results its proof uses.
Let carry a -dimensional standard Brownian motion , fix a horizon , and let be the natural filtration of augmented by the -null sets. Write for the square-integrable -measurable random variables, for the progressively measurable processes with , and for those with .
The data are a terminal value ; a coefficient , , , with for every and Lipschitz in with a constant ; and a continuous progressively measurable obstacle with and . A solution of the reflected BSDE is a triple of progressively measurable processes with , , , and
where is continuous, nondecreasing, and : pushes up only when touches .
For , is the set of stopping times with . When is concave, its conjugate is
The admissible controls are the bounded progressively measurable with . Each gives the affine coefficient , its reflected BSDE solution , the process solving , , and the payoff
For every and , , and
The last equality, the interchange of the two essential extrema, is the minimax content.
Theorem 7.2 identifies the solution of a nonlinear reflected BSDE with the value of a zero-sum game between a stopper and a controller. In finance, with the driver of a pricing rule under constraints or ambiguity, it says that the nonlinear price of an American claim is the worst case, over a family of discount rates and changes of measure, of linear American prices; and the stopper may announce the stopping rule first without changing the value. Concave drivers include the hedging equations with different borrowing and lending rates. The representation reduces questions about the nonlinear equation to a family of linear ones, which is how monotonicity, convexity and stability properties of nonlinear American prices are usually derived.
All four results and the goal are proved in the paper, with references to standard convex analysis and a measurable section theorem for two steps. None of them has a machine-checked proof. Mathlib has Brownian motion, filtrations, stopping times and conditional expectation, but no stochastic integral; the mission uses the Itô integral of the published Peng1990.SMP.Stochastic layer. A formal proof would give, beyond the theorem, a reusable comparison theorem for reflected BSDEs, a Snell-envelope representation for linear reflected BSDEs, and a measurable selection of supergradients along a process.
The inequality for each control is a direct consequence of comparison, since . The difficulty is the reverse inequality, which needs a single admissible control that attains the conjugate representation along the solution for almost every . Choosing a supergradient pointwise is easy; choosing it progressively measurable, bounded, and with square integrable is a measurable-selection problem. The interchange of ess inf and ess sup does not follow from a general minimax theorem: the family is not compact and the payoff is not convex–concave in any usable topology. It uses a specific stopping time, the first time touches , together with comparison on the random interval before it. Proposition 7.1 requires the linear change of variables , whose transformed equation lacks the square integrability of the original one, so the Snell-envelope argument has to be rerun with weaker moments.
L2F (progressive in place of predictable); and the obstacle condition are lower Lebesgue integrals in .MultiperiodRisk.Bellman.EssInf, and the essential supremum is its mirror image.Several formalizations of the goal would make it trivial, and each is ruled out. The conjugate is not a real-valued supremum, which takes a junk value when unbounded. The essential infimum over is not a pointwise infimum. The interchange of ess inf and ess sup is not dropped. The coefficient is a random field , not a deterministic or Markovian one.
The closing gloss of Theorem 7.2, that the triple is optimal, is not stated separately; milestone 4 is its control half. Contributions are welcome on a continuous version of the Itô integral, Itô's formula for products with , the Snell envelope in continuous time, and measurable selection of supergradients; all of these are reusable beyond this mission.
The Nelder–Mead simplex method (Nelder and Mead, 1965) is a derivative-free method for unconstrained minimization. It keeps a simplex of points in and replaces the worst vertex by a reflected, expanded or contracted trial point, using only comparisons of function values. It is one of the most widely used methods in practice, available in standard numerical libraries and scientific software, and it is also known for having very little supporting theory. McKinnon (1998) gave a strictly convex function in dimension 2 on which the method converges to a nonstationary point.
Lagarias, Reeds, Wright and Wright (1998) gave the first convergence results for the method as originally stated. In dimension 1 they proved that, for a strictly convex function with bounded level sets, both endpoints of the Nelder–Mead interval converge to the minimizer when (their Theorem 4.1). For the standard reflection coefficient they proved more: the convergence is eventually M-step linear, with a number of steps that depends only on the expansion and contraction coefficients (their Theorem 4.2). This mission formalizes that rate result and the move-sequence lemmas it rests on.
Let . A one-dimensional simplex is a pair of vertices ordered so that : is the best and the worst vertex. The method has four coefficients satisfying
This mission fixes , so (2.1) becomes , , . The trial points are
With , , and so on, one iteration is:
A shrink replaces by . The worst vertex is discarded and the accepted point joins ; it becomes the best vertex exactly when . Iterating from a nondegenerate initial pair () gives the run , and . A contraction means an outside or inside contraction.
Under each move multiplies the diameter by a fixed factor: for a reflection, for an expansion and for either contraction. The paper's bracketing index (its Lemma 4.2) is the first iteration with . Two integers control the move sequences after :
For all and there is an integer such that for every , every strictly convex with bounded level sets and every nondegenerate ordered , the index exists and
The goal fixes no value of ; the paper's proof gives one, but any depending only on and proves the theorem.
Theorem 4.2 is a rate statement for a method whose global behaviour is mostly unexplained. It shows that in dimension 1 with the method behaves like a bracketing line search: once the minimizer is bracketed, the interval shrinks geometrically, and the number of iterations per halving is bounded independently of and of the starting interval. With the standard coefficients , the value of constructed in the paper's proof is . The intermediate lemmas describe which move sequences the method can produce after the minimizer is bracketed.
The paper's results are proved; to our knowledge none of them has a machine-checked proof. This mission produces a formal model of the one-dimensional method with the paper's tie-breaking rules, and formal statements of the rate theorem and its supporting lemmas. Proving them is the remaining work, including the one-dimensional bracketing and proximity results of the paper's §4.2, which the proofs use and which are posed as a separate mission of this series.
The rate does not follow from a per-iteration bound: a reflection keeps the diameter and an expansion multiplies it by , so the diameter can grow for several consecutive iterations. A contraction-only argument fails for this reason. The theorem needs a bound on how long the method can avoid contracting and on how much expansion can happen between two contractions. Both bounds come from strict convexity applied along the line through the current interval, together with the location of the minimizer relative to the vertices (the proximity property of §4.2), and they must hold uniformly in . Making the constants uniform, so that and depend only on and , is the delicate part. Before no such control holds, which is why the theorem only speaks about .
The state is an ordered pair p : ℝ × ℝ with p.1 the best vertex and p.2 the worst vertex ; run f 1 χ γ σ p0 k is , and moveAt f χ γ σ p0 k is the type of iteration . The coefficient is substituted into the algorithm. The ordering rule is the paper's insertion rule (new point first iff , ties to the higher index); the printed formula contradicts the paper's own example on p. 118 and is read as its words describe. The expansion step accepts the better of and , the outside contraction is accepted on , the inside contraction on .
Standing assumptions carried by every statement: (2.1) with ; strictly convex on (StrictConvexOn ℝ Set.univ f); bounded level sets ( bounded for every ); and nondegenerate and ordered. Corollary 4.1 prints only ; the remaining conditions of (2.1) are the section's standing assumptions. is the natural-number ceiling ; is computed by a bounded search over , which loses nothing for . The uniformity of in Theorem 4.2 and of in Lemma 4.8 is encoded by quantifier order: they are chosen after and before , , .
The goal's conclusion includes the existence of the bracketing index (the paper's Lemma 4.2), so the halving claim cannot hold vacuously for a run that is never bracketed; a statement that lets depend on or is a different and much weaker theorem and is ruled out by the quantifier order.
A complete development needs: the one-dimensional facts about strictly convex functions (the paper's Lemma 4.1), the absence of shrink steps under strict convexity (Lemma 3.5 for ), the bracketing and proximity lemmas of §4.2, and the move-sequence and diameter-product arguments of §4.3. The model of the one-dimensional method and the convexity lemmas are reusable for the series' first mission (convergence of both endpoints). Proofs of individual milestones, and of the §4.2 lemmas as local results, are welcome.
A steady-state simulation produces a single long output path , and the quantity of interest is its long-run mean . The central difficulty of simulation output analysis is that the observations are correlated, so the classical confidence interval needs a consistent estimate of the time-average variance constant , which is hard to obtain. The method of standardized time series (STS), introduced by Schruben (1983) and put on a general footing by Glynn and Iglehart (Math. Oper. Res. 15 (1990)), avoids estimating : it divides the centred sample mean by a functional of the whole sample path that scales like , so that cancels in the limit. Batch means, the area estimator and other procedures used in simulation software are all instances of this construction.
Cancelling has a price. Glynn and Iglehart show (their Corollary 4.16) that every STS interval has asymptotic expected length at least , the length of the interval that knows , and (4.23) that this bound is the infimum over all admissible . This mission formalizes the next question the paper asks and answers: is the infimum attained? Proposition 4.26 says it is not, and the companion results quantify the residual randomness of the interval length.
is the space of continuous real functions on with the uniform metric and its Borel -algebra; , and . For , is the set of points at which is not continuous. On a probability space , is a standard Brownian motion, viewed as a random element of .
Assumption (2.1). There are finite constants and such that in , where
The class (2.3) consists of the measurable with
With and chosen so that , the interval (2.10) is an asymptotic confidence interval for , of width .
For every there is no such that, for some ,
By the paper's discussion before (4.25), attaining the lower bound of Corollary 4.16 with some requires (4.25); the goal therefore says that the bound is attained by no . The goal is stated in terms of (4.25) and not of the limit (4.24), so it does not depend on the expected-length machinery of Corollary 4.16.
The result closes the expected-length analysis of STS intervals: the bound is the exact infimum over but no single standardization reaches it, so every STS procedure is strictly worse, in expected length, than the interval with known . The companion results explain why: is never degenerate, so converges to a nondegenerate random limit and the interval length fluctuates at order , while intervals built on a consistent estimator of (the regenerative method, Proposition 4.34) fluctuate only at order . This is the quantitative trade-off a practitioner faces when choosing between STS and variance-estimation methods.
The paper's results are proved; none of them is formalized. The mission produces machine-checked versions of a support property of Wiener measure on (every path started at is in the support), which is reusable well beyond simulation, and of the deterministic step that turns such a support property into everywhere-discontinuity of a functional.
The goal's statement is elementary, but its proof needs a quantitative fact about Brownian paths: the law of charges every uniform ball around every path in . The natural first attempt, using that is continuous -almost everywhere and constant almost surely on , fails without this fact, because almost-sure statements say nothing about any particular path . Mathlib provides Brownian finite-dimensional laws and independent increments, but no small-ball or support estimate for Brownian motion in the uniform metric, so (4.27) has to be built from scratch. A second subtlety is that (4.25) is given for one only; the homogeneity (2.3i) is what upgrades it to all scales, and that upgrade is what makes the range of near unbounded.
Proposition 4.32 needs, in addition, the passage from weak convergence of to convergence of second moments under uniform integrability, in the space .
C(unitInterval, ℝ) with its sup norm; is dist. Mathlib has no measurable structure on it at this commit, so the Borel -algebra is declared in the mission's definitions file.IsBrownianReal. "Measurable" in means Borel measurable.The goal is a negation of an existence statement, so it would be trivially true if were empty or if the Brownian hypothesis were unsatisfiable. Neither holds: contains the batch-means functionals of the paper's Example 3.1 (p. 5), and the goal assumes nothing about small balls, (4.27) or continuity of . Those appear only as milestones.
Contributions welcome: the support theorem for Brownian motion in (milestones 1–2), any of the deterministic steps, and the moment-convergence argument of Proposition 4.32.
A retailer with limited shelf or screen space must choose which subset of its products to show each arriving customer. Which assortment earns the most depends on customer preferences, and those are unknown at first: the seller learns them from the purchases it observes. This is dynamic assortment selection, and it is a standard model in online retail and revenue management. Agrawal, Avadhanula, Goyal and Zeevi (Oper. Res. 67(5), 2019; preprint arXiv:1706.03880v2) study it under the multinomial logit (MNL) choice model as the MNL-Bandit problem. They propose an epoch-based upper-confidence-bound policy (Algorithm 1) that needs no prior knowledge of the parameters.
Their worst-case guarantee (Theorem 1) is regret of order . Many instances are easier than the worst case: the best assortment beats every other feasible assortment by a fixed margin. For such well-separated instances, earlier policies obtained logarithmic regret, but only when told a lower bound on that margin:
This mission formalizes the paper's §6.1, which shows that the same parameter-free Algorithm 1 adapts to the separation.
There are products with known revenues and unknown attraction parameters . The no-purchase option has weight . Offered an assortment , a customer buys with probability and buys nothing with probability (2.1). The expected revenue of is
Feasible assortments form a family defined by totally unimodular constraints (2.3). Assumption 4.1 asks that for all and that be closed under taking subsets.
A policy chooses from the past choices. The regret after customers is , where maximizes over (2.6).
Algorithm 1 works in epochs: epoch offers one assortment until a customer buys nothing. It keeps three statistics for each product :
The next epoch offers an assortment maximizing the MNL revenue computed with in place of .
The separation of an instance is the gap between the optimal and the second-best expected revenue among feasible assortments,
The analysis uses the threshold (6.2), with , and . It also uses good epochs: those in which every lies above and within the confidence width of Lemma 4.1.
There are absolute constants such that for every instance satisfying Assumption 4.1 with , every tie-breaking rule and every ,
The constants are not fixed, so the goal survives any improvement of them.
Under the cardinality constraint : .
The result. Theorem 3 shows that one policy is simultaneously near-optimal in the worst case (Theorem 1, , matched by the lower bound of Theorem 2 up to logarithms) and logarithmic on separated instances. It does so without being told , which the separation-based policies of Rusmevichientong et al. and Sauré–Zeevi require. Under a cardinality constraint, Corollary 6.1 matches the order of Sauré–Zeevi's bound.
Formalizing it. The theorem is proved in the paper (Appendix C), and no machine-checked version exists. A formal proof has to make several things precise:
Two printed details need care, and the formal statements fix them: Appendix C defines good epochs with "or" where both inequalities are meant, and Lemma 6.2's proof skips one case.
The counting part looks routine but depends on indexing. The bounds that are good at the end of epoch select the assortment of epoch , so "a good epoch offering a sub-optimal set" pairs two consecutive epochs. A per-product count of under-sampled epochs is then off by one per product, so the printed bound does not follow from the statement of Lemma 6.1 by counting alone.
The probabilistic part is the harder one. The per-epoch purchase counts are geometric with mean only conditionally on adaptively chosen assortments. The confidence statements must hold uniformly over a random number of samples, and the regret must be converted from customers to epochs, whose lengths are random and truncated at . A union bound over all epochs costs a factor , and that factor has to stay within the claimed .
Products are Fin N (0-based), and choices are Option (Fin N) with none the no-purchase option. A policy maps the past choices to an assortment. The law of a length- history is the product of MNL probabilities, so every expectation is a finite sum. Revenue is the published ChoiceCDLP.MNL.mnlObjective v r 1, and is a Finset.sup' over the nonempty family . Algorithm 1 is defined as an explicit state machine and never reads . Ties in its argmax are broken by an arbitrary selector, and every statement quantifies over all selectors.
Standing assumptions carried by every statement:
Disclosed conventions:
The constants are quantified before every other object. A constant depending on , or would make the theorem say only that regret is finite. The policy is pinned to Algorithm 1, not to any optimistic rule.
Contributions are welcome at every level:
Improve deterministic integer 3SUM to time in the foundation mission’s word-RAM model.
The existing Corollary 26 routine admits the tighter bound . Keep and change the grouping parameter to , implemented using the integer root of of order . Balancing the instance costs and scans gives an Exact Triangle saving of , and the verified 3SUM reduction gives time.
The supporting theorem establishes every rational exponent , including . This changes the algorithm’s grouping parameter and improves the earlier cutoff . All other model definitions and the shared reduction lemmas are reused.
Prove deterministic time for 3SUM on polynomially bounded integers, using the same word-RAM model and definitions as the foundation mission.
The existing uniform Exact Triangle bound has saving . The verified 3SUM reduction yields time, so every fixed rational exponent above is attainable, including . This mission sharpens the bound extracted from the existing algorithm.
The supporting theorem covers all rational ; it does not assert an exact bound. The proof reuses the shared, proved APSP and 3SUM lemmas from Anthropic’s formalization.
Many games have several strict Nash equilibria, and equilibrium analysis alone does not say which one a population will settle on. Harsanyi and Selten (1988) proposed risk dominance as a selection criterion for games: of two strict equilibria, select the one whose basin is "larger" in a precise payoff sense. That criterion is axiomatic. H. Peyton Young's The Evolution of Conventions (Econometrica, 1993) derives a selection from a dynamic model instead: boundedly rational players with finite memory, incomplete information about the past and occasional mistakes. Its Theorem 3 says that, in games, the dynamic selection and risk dominance coincide.
Timeline.
A finite game has players with finite strategy sets and payoffs . Fix a memory and a sample size with . A state is the sequence of the last plays (strategy-tuples), oldest first; a successor of drops the oldest play and appends a new one. In each period each player draws a sample of of the recorded plays and chooses a best reply to it (maximizing total payoff against the sampled plays). The choice probabilities form a best-reply distribution: exactly when is a best reply to some sample of size . This gives adaptive play , display (1).
With mistakes, each player independently experiments with probability and then plays with probability . This gives the perturbed chain of display (2). It has a unique stationary distribution . A state is stochastically stable if . A convention is repetitions of a strict pure Nash equilibrium. With the longest shortest best-reply path to a strict equilibrium, a strict equilibrium is generically stable if its convention is stochastically stable for all sufficiently large and all with .
For a game in normal form, with Row's payoffs and Column's satisfying , , , , set
weakly risk dominates if .
This holds for every game in normal form, for every best-reply distribution and every admissible experimentation.
Theorem 3 gives a dynamic foundation for risk dominance: an equilibrium selection criterion defined from payoffs alone is the long-run outcome of a decentralized learning process with sampling and rare mistakes. It requires no symmetry between the two player roles. Theorem 2 makes stochastic stability computable: a limit of stationary distributions is reduced to a minimum-weight arborescence over recurrent classes. That reduction is what the computation, and later applications of the method to bargaining and contracting, rely on. The equivalence of the -form with the product form of Harsanyi and Selten is elementary algebra and is not a target here.
The results are proved in the paper. To our knowledge none of them has a machine-checked proof. The mission produces formal statements of the model (adaptive play, its perturbation, stochastic stability, resistance and stochastic potential) that are reusable for other stochastic-stability results. Closing the goal also requires formalizing Young's finite version of the Freidlin–Wentzell theorem, the subject of the companion mission The Evolution of Conventions II.
The paper's argument has two hard parts. The first is Theorem 2: identifying the limit of requires the Markov chain tree theorem (the stationary distribution of an irreducible chain as a ratio of sums over spanning in-trees) together with an order-of-magnitude analysis in . The second is the exact resistance . The page constructs a path with that many mistakes (Table 1), but the matching lower bound, that no combination of mistakes by both players does better, is only asserted. It needs an argument about the first period in which some player's best reply switches. A naive count of single-player mistake runs gives only the upper bound. The tie case of (5) also matters: equality makes strategy 2 a best reply, which is why the ceiling and not the floor appears.
Players are a finite type and strategies finite types. A state is Fin m → (∀ i, S i) with position 0 the oldest play. A sample is a set of positions, and a best reply maximizes the summed payoff against the sampled plays. Transition matrices are Matrix H H ℝ. Stochastic stability is a one-sided limit of the stationary distributions of , over the admissible range , . Resistances are natural numbers on successor pairs. Recurrent classes are the essential classes of , and -trees are parent maps on the set of classes that reach the root. "" is the natural-number inequality . In the game, players and strategies are Fin 2, with the paper's written as 0, 1.
Two corrected slips are recorded in the statements. On p. 68 the recurrent classes are "of " for , and on p. 77 "the process defined in (1)" is .
Trivializing formalizations are ruled out. Stochastic stability is defined from stationary distributions, not from resistances, and generic stability is defined from stochastic stability, not from versus . Both definitions quantify over every best-reply distribution and every admissible rather than a fixed sampling law. "Sufficiently large " is an eventual statement with a threshold, not "for some ".
A complete development needs Markov chain stationary distributions on finite spaces, the Markov chain tree theorem, limits of rational functions of , and the combinatorics of sampling in games. The perturbation theory (milestones 1–3) is reusable for any finite stochastic-stability model. Contributions to the tree theorem and to the two resistance computations are particularly welcome.
Related platform work: stochastic fictitious play (StochFictPlay.*, Hofbauer–Sandholm) and calibrated learning to correlated equilibrium (CalibratedCE.*, Foster–Vohra) study other learning dynamics in games. The sibling missions The Evolution of Conventions I (Theorem 1, convergence of adaptive play) and II (Theorem 4, regular perturbations of Markov chains) formalize the results this mission's milestones invoke.