Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Cryptographic keys must be uniformly random and reproducible exactly. Many secrets people actually possess are neither: a biometric reading (an iris code, a fingerprint template), a long passphrase recalled with typos, or the correlated bits two parties obtain from a quantum channel are noisy, so two readings of the same secret differ in a few positions, and they are not uniform. Fuzzy extractors, introduced by Dodis, Ostrovsky, Reyzin and Smith (arXiv:cs/0602007; SIAM J. Comput. 38(1), 2008), turn such a secret into a nearly uniform key that can be regenerated from any sufficiently close reading, using public helper data that does not compromise the key.
The construction for the Hamming metric is the one most used in practice and in later work on biometric key derivation and physically unclonable functions. Its history is short. Juels and Wattenberg's fuzzy commitment (CCS 1999) shifted an error-correcting code onto the secret but was analysed only for uniform inputs. The syndrome of a linear code had been used for information reconciliation in quantum key agreement (Bennett, Bessette, Brassard, Salvail and Smolin, J. Cryptology 1992). Dodis et al. defined secure sketches and fuzzy extractors for arbitrary entropy distributions, introduced average min-entropy to handle side information, and proved the bound formalized here. This mission is the first of four drawn from that paper.
All logarithms are base 2. A random variable is identified with its law. For a random variable , the min-entropy is . For a pair , the average min-entropy of given is
the adversary's chance of guessing after seeing , on a log scale. The statistical distance is , and is uniform on .
The space is , where is a finite additive group with elements, , and is the Hamming distance, the number of positions where and differ. A code with codewords is an code if distinct codewords are at distance at least ; its dimension is , so .
A secure sketch is a pair of randomized procedures with whenever . It is an average-case -secure sketch if for every pair with . A fuzzy extractor has with , and whenever . It is an average-case -fuzzy extractor if
A family of functions into is universal if for all .
For every code, every , every and every natural number
there is an average-case -fuzzy extractor.
Theorem 5.2 says that the only costs of tolerating Hamming errors are the redundancy of the code, bits, and the bits that any extractor loses. Appendix C of the paper shows the redundancy term cannot be avoided for uniform inputs, so for optimal codes the construction is optimal there. The average-case form matters for composition: it remains valid when the adversary holds side information correlated with the secret, which is the situation of every protocol that uses the key afterwards or reuses the reading.
Formalizing it produces machine-checked versions of the leftover hash lemma in its average-case form, the basic calculus of average min-entropy, and the code-offset and syndrome sketches. These are the standard tools of information-theoretic cryptography, used well beyond fuzzy extraction (privacy amplification, randomness extraction, information reconciliation). All results are proved in the paper; as far as is known, none of them has a formal proof in Lean or on this platform.
The obvious route bounds the leakage of the sketch with min-entropy and then applies an extractor to conditioned on each sketch value. That fails: conditioned on a particular sketch value, may have far less min-entropy than average, so a worst-case extractor has nothing to work with on some values, and paying for those bad values costs an extra error term (Corollary 4.2). The average-case notions exist to avoid this loss, and the chain must be kept average-case at every step. In Lean the work is in the probability bookkeeping: computing laws of pairs and triples formed by independent coin flips, rearranging them, and bounding sums of maxima over possibly infinite auxiliary types, together with the leftover hash lemma itself, which Mathlib does not provide.
Random variables are their laws, Mathlib PMFs; pairs are joint laws and randomized procedures are kernels whose coins are independent of everything else. Average min-entropy is written in the equivalent joint form , which needs no conditioning on null events. The auxiliary variable ranges over every type, not only finite ones. Logarithms are Real.logb 2; is Fin ℓ → Bool; is Fin n → F with Mathlib's hammingDist.
Explicit choices:
A trivializing formalization is ruled out: the security clause quantifies over every auxiliary type and every joint law meeting the entropy bound, and are constrained exactly as in the paper, and the universal hash family is constructed inside the goal (a supporting item states that universal families exist), never assumed.
Contributions welcome: proofs of any milestone; general lemmas on PMF marginals, statistical distance and average min-entropy, which are reusable across all four missions of this paper and in other information-theoretic cryptography; and the leftover hash lemma as a standalone result.
Retailers often sell several variates of one product (colours, sizes or flavours of an otherwise identical item) from a fixed stock over a short season, with no replenishment. Customers substitute among the variates and the no-purchase option, so the price of one variate changes the demand for all of them, and the stock of each variate changes the value of selling the others. Dong, Kouvelis and Tian (M&SOM 2009) model this joint pricing and inventory problem with multinomial logit (MNL) choice and characterize optimal dynamic prices in closed form up to a scalar equation.
Many sellers do not price variates individually: apparel, sporting goods and airline examples are cited in the paper (Liu and Milner 2006) of unified dynamic pricing, where one price is charged for all variates and changed over time. Proposition 1 of the paper gives the optimal unified price and the optimal revenue in the same form as the paper's main result for variate-specific prices. Comparing the two quantifies how much revenue is lost by restricting to a common price, which is the purpose of the paper's §5.
There are variates, . Variate has quality index , the no-purchase option has utility , is the MNL scale parameter, and in each period one customer arrives with probability . Time counts the remaining periods, so the season runs and ends at .
An inventory level is . The in-stock set is , and is the inventory after one sale of variate . Out-of-stock variates are not offered. At the price vector , an arriving customer buys variate or nothing with the MNL probabilities
Under unified pricing the decision in each period is one price charged for every in-stock variate. The unified value function , the maximal expected revenue from remaining periods, satisfies and
with evaluated at . Write for the marginal value of a unit of variate , and
For and , the equation
has a unique solution ; the price
is nonnegative and optimal, with ; and
where solves the equation of period at the same inventory . The statement asserts attainment of the maximum, not only a value for .
The proof in Appendix A proceeds through a one-variable problem. For marginal values let . The milestones are: the rewriting (23)–(24) of the optimality equation as an attained ; the derivatives of , and in the common price; the first-order conditions (25)–(26) with and at a stationary point; the second-order condition, giving exactly one stationary point, which is the global maximizer of on ; the formula with and the equation for ; uniqueness of the root of the margin equation, with root ; and the displayed revenue sum at the same inventory.
Proposition 1 reduces a dynamic program over a high-dimensional inventory state to a scalar root-finding problem per state and period, and gives the optimal revenue as a sum of margins. It shows that the full dynamic pricing result (Theorem 1 of the paper) survives the restriction to a common price, with the individual marginal values replaced by their quality-weighted average , and the qualities replaced by the aggregate . This is what makes the paper's numerical comparison of unified, static and full dynamic pricing in §5 computable.
The result is proved in the paper; it has not been formalized. A formalization produces a checked version of the MNL derivative calculus, of the quasiconcavity argument for the common-price objective, and of the backward induction, and it closes a step the printed proof leaves implicit: that the maximizer over all real prices is nonnegative, so that it is feasible for the constrained problem.
The one-period objective is not concave in the price, so neither a concavity argument nor a direct appeal to a compactness theorem gives a unique maximizer. Negativity of the second derivative at stationary points is a local statement; the existence of a stationary point and its being the global maximum on all of do not follow from it alone.
The second difficulty is the constraint . The paper solves the unconstrained problem. Showing that needs a property of the unified value function, nonnegativity of the weighted marginal value, which the paper does not state. The obvious argument, increasing in inventory term by term, does not apply verbatim when a variate leaves the in-stock set, because the choice set itself changes.
Finally, a supremum in Lean is a real number even when not attained; the value identity is only meaningful together with attainment, which the goal states explicitly.
The model is one definition file, SubstitutePricing.Unified.Model: a structure with , , , , ; assumptions , ; inventories ; the in-stock set as a Finset; MNL probabilities with sums over only (the paper's null price is modelled by removal from the choice set); and the unified value function by recursion on , as a real sSup over . The equation (3) is read with the no-purchase term outside the sum over variates, as the paper's (5) and (22) use it.
Committed conventions and restrictions:
A statement about alone, without the attainment and feasibility of , would be trivially satisfiable by a junk supremum and is ruled out by the goal's form.
Infrastructure needed: derivatives of MNL probabilities, a quasiconcavity or unique-critical-point lemma for one-variable functions, a root lemma for , and a monotonicity property of the unified value function. The MNL derivative calculus and the root lemma are reusable for the companion missions on full dynamic pricing and mixed pricing from the same paper. Contributions on any milestone, and on the nonnegativity of , are welcome.
A controller of a finite Markov chain often cares about more than one long-run quantity: an inventory manager wants a high average profit while keeping the long-run fraction of stock-outs below a target; a communication network maximizes throughput subject to bounds on average delay or power. Such problems are constrained Markov decision problems: maximize one average reward while other averages, all linear in the long-run frequencies of state-action pairs, are kept below given bounds. Unlike unconstrained problems, they need not have a pure stationary optimal policy, and in general not even a stationary one.
Derman (Finite State Markovian Decision Processes, 1970, Ch. 7) treated the case in which every stationary policy induces a chain with one ergodic class, and solved it by linear programming. Derman and Veinott (1972) proposed a decomposition algorithm for the general multichain case, remarking that until the faces of the relevant polytope are known, routine use of the simplex method is not possible. Section 4.7 of Kallenberg's 1983 monograph (CWI repository) describes that polytope explicitly for the multichain case and derives from one linear program an optimal Markov policy, with conditions under which a stationary optimal policy can be read off. Kallenberg notes that Veinott knew the characterization of the polytope by 1973.
A finite Markov decision model has a finite state set , for each state a finite nonempty set of actions, rewards and transition probabilities with . A policy chooses, at each time , an action in at random, with probabilities that may depend on the entire history . Special classes are the Markov policies (the rule at time ignores the past), the stationary policies , written (one rule , with and , at every time), and the pure stationary policies , written with . All policies form the class .
Fix an initial distribution : and , with zeros allowed. The expected state-action frequencies in the first periods are
is the set of limit points of , and the class of policies with exactly one limit point . For a class , collects the limit points of all , giving , , (for ), and . For a stationary , , is its Cesàro limit, and .
The polytope is the set of for which some satisfies
Given constraint data and , the constrained problem (4.7.5) is , with the lim inf of the average expected reward, and the linear program (4.7.6) maximizes over 's constraints together with .
Every limit point of the expected state-action frequencies of any policy lies in the polytope , and every point of is such a limit point.
The goal identifies the set of achievable long-run behaviours of a multichain Markov decision process with a polytope given by linear equations. Any objective and any constraints that are linear in the frequencies then become one linear program (Theorem 4.7.3), and optimal policies are recovered from its solution. This is the basis of the linear programming approach to constrained average-reward control, later developed by Altman (Constrained Markov Decision Processes, 1999) and others.
The results of this section are proved in the monograph; none has a machine-checked proof. The mission produces a formal account of state-action frequencies under history-dependent policies on a finite model, their limit points, and the multichain LP polytope. The unichain special case is related to Derman's statements posed on the platform (DermanSeqDecisions.LinProg.*, completely ergodic models); the multichain statements here are not posed elsewhere.
The inclusion needs a limit point of a history-dependent policy to satisfy the second family of equations, which involves the auxiliary vector ; for stationary policies comes from the deviation matrix, but a general policy has no such matrix. The reverse inclusion cannot be obtained by realizing each with a stationary policy: Example 4.7.1 of the book exhibits a model where , and a point of that is not an extreme point of . The natural candidate, the stationary rule , is not defined on states with , and filling in there does not in general reproduce (Theorem 4.7.5 gives conditions under which it does). In the converse direction, frequencies of general policies need not converge, so arguments must work with all limit points, not with a limit.
MarkovDecisionProcesses_AverageReward (reference item): StationaryMDP S A with finite state type S, a common finite action type A, a nonempty admissible Finset per state, rewards, and transition rows that sum to one; policies are its AvgHRPolicy, history-dependent and randomized. Frequency vectors are indexed by the admissible pairs.limUnder of the Cesàro means ; its existence is the book's Theorem 2.4.1(i) and is not assumed as a hypothesis.IsUnichainMatrix (any two recurrent states communicate); Assumption 4.7.1 is IsUnichain.A complete development needs Cesàro limits of stochastic matrices (Theorem 2.4.1), the stationary-policy correspondence of §4.3, a separating hyperplane in finite dimension, and the Derman–Strauch construction of a Markov policy matching a mixture of policies (Theorem 2.5.1). The frequency and limit-point infrastructure is reusable for any average-reward model on a finite state space. Proofs of any milestone, and of the auxiliary facts above as separate theorems, are welcome.
Martingale inequalities compare what a fluctuating process does along a path with how large its successive increments are. Such estimates are used in probability and harmonic analysis because a martingale can represent information revealed step by step, while its square function measures accumulated fluctuation. In his 1973 Wald Memorial Lectures, Burkholder developed distribution function inequalities that cover many choices of size measure at once, extending the power norm comparisons treated earlier in the paper. Burkholder, 1973
The target of this mission is Theorem 15.1 of that paper: a two sided comparison for every convex function of moderate growth. The paper attributes the decomposition of a martingale into small and large jumps to Davis, and cites a convex comparison lemma introduced in earlier work and subsequently treated by Garsia and Neveu. These attributions matter to the scope of the mission: the decomposition and lemma are separate, named milestones, while Burkholder's printed two sided inequality is the goal. Burkholder, 1973, §§14–16
Work on a probability space with an increasing sequence of sub sigma fields . A real martingale is observed from time onward. Following the paper, put in the formulas for its differences: and for . This convention differs from the index zero value required for a Lean martingale, which is discussed below.
The square function and maximal function are pathwise quantities:
Either quantity can be infinite. Their finite versions stop at : sums the first squared differences, and takes the maximum through time . For a positive exponent , the paper writes . The notation means the expectation of a nonnegative transform of a nonnegative random variable .
A function of moderate growth is a nondecreasing continuous with and
for some nonnegative growth constant . The target adds convexity on finite nonnegative arguments. The examples and for satisfy these conditions. The paper sets aside as trivial; the Lean statements allow it because every displayed comparison still holds.
The goal is precisely the form printed as Theorem 15.1:
The constants depend only on , and are uniform over the probability space, filtration, martingale, and particular choice of with that growth bound. The statement includes both sides; the paper writes a proof for the right side and says the left side follows by the same pattern. No integrability or boundedness is imposed on or on the two expectations. Burkholder, 1973, Theorem 15.1, pp. 33–34
The milestones record the paper's good lemma, Doob's cited maximal estimate, the predictable jump inequalities of §12, the quasi subadditivity of , Davis's decomposition and its jump bounds, and the convexity lemma of §16. The latter compares a sum of nonnegative random variables with the sum of their conditional expectations. Its two Neveu statements are retained as cited intermediate targets. These results identify distinct mathematical interfaces that a solver can formalize and reuse; the milestone text is transcribed from the indicated pages of the article.
The theorem lets one replace the expected convex transform of a path's maximum by the expected transform of its quadratic fluctuation, up to constants controlled by a single growth parameter. Choosing recovers the comparison displayed after Davis's decomposition; choosing a convex power gives the power cases. The assertion is useful even when one or both expectations are infinite, because it gives a uniform relation across the whole class of admissible martingales and functions. Burkholder, 1973, §§14–15
The result is proved in the paper. This mission asks for a machine checked Lean proof of the known theorem and of the selected statements that support it. The definitions for square and maximal functions, moderate growth, and nonnegative conditional projections can be reused in other martingale comparisons. A previously posed platform theorem about Robbins–Monro noise sums has the shape of one power function instance, but its process and time window differ; it does not supply this general result.
The size of a single martingale increment can dominate both a maximum and a square function. A direct comparison of the two pathwise expressions therefore gives no uniform expectation bound for arbitrary martingales and convex . The §12 estimates require predictable control of jumps, while the target has no such hypothesis. Davis's decomposition exposes the small and large jump contributions as different objects, and the §16 convexity lemma is needed to compare the conditional terms arising from large jumps. Convexity is essential for that lemma and for Theorem 15.1; the §12 good statements themselves assume only moderate growth. Burkholder, 1973, §§12, 14–16
Lean uses Mathlib's Martingale f ℱ P for a process indexed by natural numbers. The article begins at and uses only in its difference formulas. The definitions of , , , and therefore read positive indices and insert zero in the article's formulas; Lean's actual is the compatible conditional expectation extension needed by Mathlib. Davis's partial sums also begin at , and the decomposition theorem specifies the index zero extensions for its two martingales.
The square function, maximal function, norm, and all nonnegative expectations take values in . This retains unbounded sample paths and nonintegrable expectations. For a nonnegative variable , is the extended conditional expectation condLExp, so a nonintegrable cannot silently become zero. Davis's signed is integrable, so its real conditional expectation uses Mathlib's ordinary conditional expectation. Predictable bounds such as and the resulting claims are stated almost everywhere at each positive index.
The Lean predicate for moderate growth states the doubling law at zero and infinity as well as positive finite ; zero is automatic from , and the endpoint at infinity follows by continuity in the nontrivial case. Convexity is read from finite real arguments. The zero function is included. A valid formalization must retain both inequalities in the goal and choose its constants before the martingale and ; choosing constants after the data would make the goal much weaker.
The development needs finite and infinite square function sums, maximal functions, stopping and tail events, Mathlib martingales, conditional expectations, and convexity on the nonnegative reals. Contributions proving or improving any of the named milestones are welcome, including independent proofs of the cited Doob and Neveu statements. No extra boundedness or integrability assumption should be inserted into the goal to simplify a proof.
A large matrix, or a large graph, can be approximated in a weak but useful sense by a short sum of very simple pieces. Frieze and Kannan (Combinatorica 19 (1999) 175–220) proved that every real matrix is, up to an error small in the cut norm, a sum of at most cut matrices (constant on a combinatorial rectangle, zero elsewhere). This "weak regularity lemma" gives polynomial-time approximation schemes for dense instances of Max-Cut and other problems, with a number of pieces that is polynomial in , in contrast to the tower-type bounds of Szemerédi's regularity lemma.
Section 8 of the paper states the same decomposition for functions on the unit square, where the rows and columns of the matrix are replaced by the continuum . This continuous form became the weak regularity lemma for graphons (symmetric measurable functions ) in the theory of dense graph limits developed by Lovász, Szegedy, Borgs, Chayes, Sós and Vesztergombi in the 2000s (Lovász–Szegedy 2006; Lovász, Large Networks and Graph Limits, 2012), where it is a standard step in proving compactness of the graphon space under the cut distance.
Let carry Lebesgue measure . Let be Lebesgue measurable with
For measurable the rectangle integral is
and the cut norm is , the supremum over measurable . The measure of is written .
A cut function , for measurable and a real , is the function equal to on and to elsewhere. Given cut functions , the error after of them is
In the Lean development these are rectInt f S T, l2Norm f, cutFun S T d and cutFunSum Ss Ts d in the namespace FriezeKannan.Continuum, on the type Sq = unitInterval × unitInterval.
For every measurable with and every there exist cut functions with
The number of cut functions depends on alone, not on .
The result. Theorem 12 says that the space of square-integrable kernels is, in the cut norm, uniformly approximable by step functions of bounded complexity: rectangles suffice, whatever is. Refining the rectangles into a common partition gives a partition of into at most parts on which is close to a step function in cut norm, which is the weak regularity lemma for graphons. It is the ingredient behind compactness of graphon space, the approximation of graph parameters by sampling, and the equivalence of cut distance and left convergence in dense graph limit theory.
Formalizing it. The theorem is proved in the paper and in textbooks; this mission produces a machine-checked version. As far as the platform's catalog shows, no cut-norm decomposition of functions on is formalized there, and Mathlib has no graphons or cut norm. The definitions here (rectangle integrals, cut functions, the cut norm as a bound over measurable rectangles) are a reusable starting point for graph-limit results.
The paper's computations are short; the difficulty of a complete formalization is in the measure theory: the error must be shown square integrable at every stage (cut functions with measurable sets are bounded and measurable); integrability of and over follows from square integrability on a probability space; the product measure of is ; and the case must be excluded from the hypothesis rather than assumed. A naive attempt that bounds the cut norm by an approximation through step functions gives no bound on in terms of alone.
unitInterval with its Lebesgue measure, and is the product type unitInterval × unitInterval with the product measure. Sets are subsets of unitInterval, so no side condition appears.MemLp f 2, whose almost-everywhere strong measurability is measurability for the completed Lebesgue measure; no Borel Measurable f hypothesis is added. l2Norm f is the square root of ; it is the true norm under MemLp f 2, which every theorem about it assumes for the function whose norm is being lowered.(volume S).toReal, finite on .Fin s; is the empty sum.Contributions welcome: proofs of the three milestones and of the goal, and general lemmas on set integrals over measurable rectangles of unitInterval × unitInterval and on MemLp of finite sums of indicator functions, which are reusable beyond this mission.
The rate at which a finite Markov chain approaches equilibrium depends on its eigenvalues. For a reversible chain, an upper bound on the second largest eigenvalue gives a lower bound on the spectral gap, which is one of the quantities used to study relaxation toward stationarity. Diaconis and Stroock asked how to estimate this eigenvalue using the geometry of transitions rather than computing the whole spectrum. Their 1991 paper gives an answer in terms of paths through the graph of positive transitions, and compares it with other geometric estimates Diaconis and Stroock, 1991.
This mission covers the first estimate in that paper, Proposition 1, together with the alternative parameter of Proposition 1′ and the random-walk specialization in Corollary 1. These results are known mathematical theorems. The work here is to state their exact finite, reversible setting in Lean and make their formal proofs available as reusable spectral estimates. The paper's examples show why the path selection matters: two choices for the same chain can give substantially different bounds Diaconis and Stroock, 1991, §2.
Let be a finite state space and let be the transition probability from to . Assume that is irreducible and reversible with respect to a stationary probability distribution . The edge measure is . Thus identifies an available edge of the transition graph. Because the chain is irreducible, every state has positive stationary mass and distinct states can be connected by such edges Diaconis and Stroock, 1991, §1A–B.
For each ordered pair of distinct states , choose a path from to . A path may revisit a vertex, but cannot use an unordered edge twice. Write for the whole choice of paths. The weighted path length is . Here a traversal has an orientation, and in the congestion formula means that the path traverses the directed edge in that orientation. The congestion parameter of (1.5) is
with the maximum over directed edges for which . The paper also defines , where is the ordinary number of edges Diaconis and Stroock, 1991, pp. 37–38.
The variance of a real function is . Its Dirichlet energy is . If , let denote the second largest real eigenvalue of , below the simple eigenvalue Diaconis and Stroock, 1991, pp. 36–37.
For every admissible path system ,
The mission's milestones are the pairwise expression for variance, the paper's per-path Cauchy–Schwarz inequality, the resulting , and the variational characterization (1.2) of the spectral gap. The last is the proved theorem MarkovMixing.dirichlet_gap, which states (1.2) for centered functions of unit squared norm, a normalization under which the ratio in (1.2) is unchanged, and adds that the infimum is attained Diaconis and Stroock, 1991, pp. 37–38.
Proposition 1′ states using the alternative congestion parameter. For a connected simple graph , Corollary 1 specializes Proposition 1 to simple random walk, with stationary distribution . If , is the maximum number of edges in a chosen path, and is the maximum number of selected paths traversing a directed edge, its bound is
The paper states Proposition 1′ without a separate proof and derives Corollary 1 from the graph's transition probabilities Diaconis and Stroock, 1991, pp. 38–39.
The result converts information about a path family into a numerical spectral-gap estimate. This lets a solver analyze a chain through its transition graph when an exact diagonalization is inconvenient. The graph corollary makes the quantities especially concrete: number of edges, maximum degree, longest selected path, and how many selected paths share an edge. Such estimates are one ingredient in quantitative convergence bounds for reversible chains Diaconis and Stroock, 1991, §§1D, 2.
The finite-chain vocabulary for stochasticity, stationarity, reversibility, eigenvalues, variance, and Dirichlet energy is already published in the MarkovMixing layer. The mission adds the paper's edge-simple path system and its two congestion parameters, then formalizes the source's statements against that vocabulary. The path definitions and pairwise variance identity can be reused in other canonical-path arguments; the three claims from pp. 37–39 still need machine-checked proofs in this mission. The variational spectral-gap theorem used as a milestone is already proved on Prove2Me Levin, Peres and Wilmer, 2009, §13.3.
The challenge is to account for each selected path without changing the congestion constant. Paths are indexed by ordered endpoints, edges in the maximum are directed, and the paper permits repeated vertices while forbidding repeated edges. Counting traversals with the wrong orientation, or allowing an edge to repeat, changes the parameter that appears in the final bound. The graph case also depends on keeping the number of paths through an edge separate from path length; replacing either with a coarser graph quantity would give a different theorem Diaconis and Stroock, 1991, §1B.
The state space is a finite Lean type, is a real matrix, and is a real-valued probability vector. A path is a list of vertices. Its traversed directed edges are successive vertex pairs; the edge-simple rule compares those pairs as unordered edges. One path is chosen for each ordered pair , and values of never enter the formulas. The maximum over positive directed edges is implemented as a real supremum over a finite subtype. On an empty index set that expression has Lean's default value zero; irreducibility and exclude this case in the eigenvalue results.
The standing assumptions are stochasticity, irreducibility, stationarity, and detailed balance. The goal and its companion eigenvalue estimates also require because the second largest eigenvalue is undefined for a one-state chain. The variance identity needs only a probability distribution, while the per-path estimate uses only a positive-edge walk. The graph corollary assumes connectedness and at least two vertices; it derives the chain properties from the graph as the paper does. The mission does not assume the desired Poincaré inequality or the spectral conclusion as hypotheses.
The main proof obligations concern the pathwise inequality, the finite reindexing that produces the paper's exact , and the eigenvalue bound. Contributions that establish those claims, the graph specialization, or the alternative estimate fit the stated scope. The shared Markov-chain definitions and the path vocabulary are intended to support later results of the same paper.
Many dense combinatorial optimization problems (Max-Cut, graph bisection, quadratic assignment on dense instances) have objective functions that are sums of matrix entries over rectangles . If a matrix can be replaced by a simple surrogate that agrees with it on every rectangle up to a small error, such problems can be solved approximately on the surrogate. Frieze and Kannan's paper Quick approximation to matrices and applications (Combinatorica 19 (1999) 175–220) supplies this surrogate: a sum of a bounded number of cut matrices. Their decomposition is a "weak" form of Szemerédi's regularity lemma whose number of pieces grows only like , against a tower-type bound for Szemerédi's lemma. It underlies constant-time sampling algorithms for dense instances, the theory of graph limits (the cut distance of Lovász and Szegedy), and the cut-norm approximation algorithm of Alon and Naor.
Timeline:
Let and be finite sets, , , and let be a real matrix. For , write
The Frobenius norm is , and the cut norm is .
For , and , the cut matrix has entry on and elsewhere; it has rank at most one. A cut decomposition of width writes
with error matrix . In the Lean development these are blockSum, frobNorm, cutNorm, cutMatrix and cutSum in the namespace FriezeKannan.CutDecomp.
For every real matrix and every there are cut matrices such that satisfies
Theorem 7 says that the width needed to approximate a matrix on all rectangles, with error measured against , depends on only, not on or . Since , it gives a cut decomposition with , the error of the paper's algorithmic Theorem 2. It is the existence statement behind the paper's constant-time approximation schemes for dense Max-Cut and Max-SNP problems and behind its pseudo-regular partitions of graphs (§5.1), and it is the matrix form of the weak regularity lemma used throughout the theory of dense graph limits.
The result is proved in the paper, by an elementary argument. Its formalization adds a machine-checked weak regularity lemma for real matrices with explicit constants, stated in a form (finite index types, block sums, cut matrices) that downstream developments in graph limits, property testing and approximation algorithms can import. To the best of the curators' knowledge it has no machine-checked proof; Mathlib contains Szemerédi's regularity lemma for graphs but not this matrix decomposition or the cut norm of matrices.
The obvious decomposition, one cut matrix per nonzero entry, achieves but has width ; the content is that width suffices uniformly in the dimensions. Bounding the error on a single rectangle is easy; bounding it on all rectangles at once, with an error that scales as rather than as , is the point. The bound is also against the Frobenius norm of the original matrix , not of the current error, so the argument must track a single global quantity across all steps. In Lean, the main friction is bookkeeping: real casts of cardinalities inside square roots, the division by , and the identification of the squared Frobenius norm with a double sum.
R, C with decidable equality; subsets are Finsets, and is the cardinality cast to . Empty or is allowed.frobNorm); Mathlib's scoped matrix norms are not used. The cut norm is a genuine maximum over the finite nonempty set of pairs of subsets.Fin s; is allowed (for or no cut matrix is needed). No nonemptiness, disjointness or sign condition is imposed on , , .A finite Markov chain repeatedly applies a transition rule to move among a finite set of states. Its stationary distribution is a probability law that the transition rule leaves unchanged. For algorithms that sample from a target distribution, and for random walks used to model a system, a central question is how long a chain started from one state takes to resemble its stationary law. Diaconis and Saloff-Coste study how a logarithmic Sobolev inequality controls this approach to equilibrium. Their paper develops finite-chain functional inequalities and applies them to mixing bounds, product chains, and concrete walks. Diaconis and Saloff-Coste, 1996.
Theorem 3.7 gives a starting-state bound in a weighted quadratic distance. Its dependence on the initial state's stationary mass is a double logarithm, while the final convergence term is governed by the spectral gap. This separates two effects: reaching a distribution that is no longer sharply concentrated, and then reducing its remaining deviation from stationarity. The paper also distinguishes general chains from reversible ones, with different constants in the first time scale. Diaconis and Saloff-Coste, 1996, pp. 719 and 723–724.
Let be a finite state space. A transition matrix assigns nonnegative numbers whose sum over is one for every . A probability vector is stationary when for every ; here every is strictly positive. The chain is irreducible when every state can reach every other state in some finite number of steps. It is reversible when for all states . These conditions are the paper's standing finite-chain setting. Diaconis and Saloff-Coste, 1996, pp. 700–702 and 714.
For a real function on , write and . Its weighted -norm is . The Dirichlet form used here is the ordered bilinear expression . It is generally not symmetric for a nonreversible chain. The spectral gap is the variational quantity . The log-Sobolev constant is , where . Diaconis and Saloff-Coste, 1996, pp. 701, 705–706, 714.
The continuous-time heat kernel averages all discrete step counts with Poisson weights. If the chain starts at , then is the probability of being at at time . Its density relative to stationarity is . Thus measures the weighted quadratic deviation of the time- law from . Diaconis and Saloff-Coste, 1996, p. 702.
The milestones include the spectral-gap decay of Lemma 2.4, the heat-flow moment identity of Lemma 2.5, the power inequalities of Lemma 2.6, and the derivative formula (3.2). The two hypercontractivity clauses of Theorem 3.5 state that when for a general chain, or when for a reversible chain, with and . These are separate source statements and remain separate milestones. Diaconis and Saloff-Coste, 1996, pp. 706–707, 719–721.
The goal is Theorem 3.7. For a state with and any , it asserts
For a reversible chain, the same bound holds with in place of . The theorem specifies these times exactly; no broader range of times is built into the goal. Diaconis and Saloff-Coste, 1996, p. 723, Theorem 3.7.
The goal turns two chain constants into an explicit convergence estimate for every eligible starting state. It provides a way to assess a chain whose initial law is a point mass, where the initial density can be large when is small. The reversible clause records the paper's stronger time bound under detailed balance. The preceding milestones expose the general spectral and hypercontractive results as reusable statements for other mixing questions. Diaconis and Saloff-Coste, 1996, pp. 719 and 723–724.
These statements are proved in the 1996 paper; this mission asks for machine-checked proofs of the specified formal statements. Published finite-chain definitions for stochasticity, stationarity, irreducibility, detailed balance, weighted expectation and variance, and the heat kernel are already available. The variational gap, log-Sobolev constant, entropy functionals, and this theorem family are the remaining local formalization work. Their individual proof status on the platform can evolve independently after the proposal is launched.
The immediate spectral-gap estimate reduces the deviation exponentially, but by itself retains a factor tied to the size of the initial point-mass density. That gives a dependence on , rather than the double logarithm in Theorem 3.7. The stronger bound requires control of how the heat operator changes norms, including the distinction between reversible and nonreversible chains. A formal proof must keep the bilinear Dirichlet arguments in their printed order and handle a real exponent that varies with time. Diaconis and Saloff-Coste, 1996, pp. 706–707, 719–724.
The Lean state space is a finite type, is a real matrix, and is a real-valued stationary probability vector positive at every state. Irreducibility is explicit in the Section 3 statements; reversibility is an additional premise only for the corresponding clauses. The heat kernel is the published Poissonized semigroup. The local and are variational real infima, and operator norm claims are expressed as inequalities for every function. Discrete eigenvalue-based gap definitions are not substituted for the paper's .
The goal's condition gives a meaningful double logarithm, and irreducibility in this finite setting gives positive gap and log-Sobolev constants on every state space where the goal is applicable. The positive stationary mass makes the density quotient meaningful. Nonnegative or positive function premises follow the source's power and derivative statements; no arbitrary sign-changing real powers are used. The Lean conventions for zero logarithm terms and for real infima are documented with the definitions. This excludes trivial conclusions from totalized logarithms, division by zero, or empty variational sets.
The development invites proofs of the seven target theorems and reusable finite-state lemmas about the semigroup, weighted norms, entropy, and variational constants. The definitions remain local to this paper's mission series because the published Markov-chain substrate provides the general finite-chain model, while the variational quantities and normalization here are tied to these source statements.
The multiarmed bandit problem asks how to allocate a single resource, one play per period, among several alternative projects whose states evolve only while they are worked on. It models the scheduling of jobs on one machine, the sequencing of research projects, and the design of sequential clinical trials. Gittins and Jones (1974) showed that the problem with discounted rewards is solved by an index policy: compute for every project a number depending only on that project's current state, and always work on a project of greatest index. Weber's paper (Ann. Appl. Probab. 2 (1992)) gives a short proof of this theorem through fair and prevailing charges, and uses the same accounting to derive bounds on how much any other policy loses.
In practice the optimal policy is often not the one used: indices may be expensive to compute, or a simpler heuristic may be preferred. A bound on the loss of an arbitrary policy, computable along that policy's own trajectory, tells a practitioner how far from optimal the chosen heuristic is. This mission formalizes the first such bound of the paper, Theorem 2, which Weber attributes to Glazebrook (1990).
Timeline. Gittins and Jones (1974) and Gittins (1979) proved optimality of the index policy by an interchange argument. Whittle (1980) gave a proof through a retirement option. Glazebrook (1982) bounded the suboptimality of a policy in terms of Gittins indices only; Glazebrook (1990) gave the sharper bound stated here as Theorem 2. Weber (1992) rederived it from the prevailing-charge accounting and added the index-gap bound (Theorem 3) and the submodularity of the optimal value (Theorem 4).
There are bandits. Bandit has a state at each epoch . At each epoch the gambler plays one bandit , receives the reward , and the state of bandit moves according to a Markov kernel ; the states of all other bandits stay unchanged. Rewards are nonnegative and uniformly bounded, and future rewards are discounted by a factor with . A policy chooses , possibly at random, as a function of everything observed so far. Its value from the initial states is
The fair charge of a state is the per-play charge at which a gambler holding a single bandit in state , free to stop at any time, would only just break even. Equivalently it is the largest ratio of expected discounted reward to expected discounted time over stopping times . Weber's Gittins index is . The prevailing charge of bandit at time is the least fair charge seen so far on that bandit, . A Gittins policy plays at each epoch a bandit of greatest index; Theorem 1 of the paper says it is optimal.
For a Gittins policy , every policy and every initial state vector ,
The result. Inequality (6) bounds the loss of an arbitrary policy by a quantity observed along that policy's own trajectory: at each epoch, how far the reward collected falls below the greatest prevailing charge. A policy that plays a bandit of greatest prevailing charge whenever possible and collects its charge as reward loses nothing, which recovers Theorem 1. The bound is the basis of Glazebrook's analysis of near-optimal heuristics for bandit and stochastic-scheduling problems, and of the index-gap bound (7) of Theorem 3, which is the second mission of this series.
Formalizing it. Theorem 1 of the paper (optimality of the Gittins policy) is already formalized and proved on Prove2Me as BanditAlgorithm.gittins_index_theorem (Shuze Chen, following Lattimore and Szepesvári, Theorem 35.9), together with the finite-horizon prevailing-charge accounting and the charge-stack interleaving lemmas (Harry_Xu). Theorem 2 itself has no machine-checked proof. This mission produces the infinite-horizon forms of the charge accounting, (5) and its equality case for the Gittins policy, and the realisation-wise comparison of greatest prevailing charges, and combines them into (6). Missions 2 (Theorem 3, the index-gap bound) and 3 (Theorem 4, submodularity of the optimal value) of this series state the paper's other results on the same model; none of the three relies on the others.
The paper's proof is one sentence: combine (5) with the realisation-wise observation. The two pieces live on different probability spaces. Inequality (5) and the equality for the Gittins policy are expectations under the law of each policy's own history, while the comparison of greatest prevailing charges is made on a fixed realisation of each bandit's state sequence. Transferring the deterministic comparison into an inequality between expectations under two different policies needs a coupling under which every policy sees the same per-bandit state sequences, so that the prevailing-charge stacks are the same random objects under and . The naive approach, comparing the two laws round by round, fails: the round- histories of and have different distributions, and no pointwise inequality holds between them. The infinite-horizon statements also require controlling the terminal retirement potential, which vanishes only in the discounted limit.
The development uses the published BanditAlgorithm model (GittinsIndex, GittinsTerminalPotential, GittinsPrevailingChargeValue, GittinsChargeInterleaving). Conventions committed to:
gittinsIndex (the ratio (4)); is a new definition weberIndex. The goal uses and the factor , as in (6); milestones 1 and 3 use , as the paper does.IsGittinsIndexPolicy (with probability one it plays an arm of greatest index, ties arbitrary). The goal does not assume such a policy exists; a one-armed instance shows the hypotheses can be met.Replacing by in (6) would weaken the bound by the factor , and dropping the boundedness of rewards would let the published value be a junk ; neither is the paper's statement, and both are ruled out by the conventions above.
Contributions welcome: the infinite-horizon limits of the published finite accounting, a coupling of all policies on independent per-bandit state sequences, and the deterministic comparison of greatest exposed charges, which is reusable for any interleaving argument on nonincreasing sequences.
School and university timetabling is one of the oldest applications of combinatorial optimization. In his invited review An introduction to timetabling (European Journal of Operational Research, 1985), D. de Werra opens with the class–teacher model: classes meet teachers for a prescribed number of one-period lectures, and the lectures must be placed into periods or days so that no class and no teacher is overloaded. Every richer timetabling model of the review (preassignments, unavailabilities, course scheduling) is built on top of this one, and the review keeps returning to its graph-theoretic reading as an edge-colouring problem in a bipartite multigraph.
The model comes in three levels of demand. The daily problem asks for a clash-free timetable. The weekly problem asks for an assignment of lectures to days within daily load limits. The balanced weekly problem asks, in addition, that the load of every class and every teacher be spread as evenly as possible over the week, and that the lectures of each class–teacher pair be spread evenly too. The last one is the practical requirement that a teacher should not have all four lectures with one class on Monday.
Timeline (as cited in the review).
There are classes and teachers . The requirement matrix is an matrix of nonnegative integers: is the number of lectures class must have with teacher . Write for the total load of class and for that of teacher . For nonnegative integers and , and are the floor and ceiling of the rational .
A schedule over periods or days is an array of nonnegative integers (, , ) that places every lecture exactly once:
In the Lean development these are IsCT1 R p x, IsCT2 R p a b x and IsCT3 R p x, with the floor and ceiling written lo s p and hi s p and the totals rowSum R i, colSum R j.
The statement fixes no constant: it asserts that perfectly balanced weekly timetables always exist.
The result. Proposition 2.3 says that the balancing requirement costs nothing: whatever the requirement matrix, the week can be organised so that each class and each teacher has an essentially constant daily load and each class–teacher pair is spread evenly. It contains König's edge-colouring theorem (take at least the maximum degree, so every daily load is at most one) and the weekly Proposition 2.2 as special cases. Combined with Proposition 2.1 applied to each day, it reduces weekly timetabling to independent daily problems, which is the decomposition the review recommends ("one may start by solving the weekly problem … and then solve separately the resulting daily problems", p. 154). In graph language it is the existence of equitable edge colourings of bipartite multigraphs, a standard tool in scheduling and in the theory of edge colourings.
Formalizing it. All results of this mission are classical and proved in the literature; none of them is formalized on the platform. Mathlib contains Hall's marriage theorem but not König's edge-colouring theorem for bipartite multigraphs, and not balanced or equitable colourings. A complete development gives a machine-checked König edge-colouring theorem in matrix form, the matrix-rounding step with simultaneous row, column and entry bounds, and the balanced-colouring theorem itself.
Each family of constraints alone is easy: spreading a single number evenly over days, or a single row total, is a matter of division with remainder. The difficulty is that one array must satisfy (1), (8), (9) and (10) simultaneously, so that the per-entry roundings must add up to correct roundings of every row total and every column total on every day. Rounding each entry independently breaks the row and column constraints, and greedy day-by-day choices can leave a remainder that no longer fits the bounds. The crux is integrality: the rational average satisfies every bound on every day, but the problem asks for integers, and an integral one-day slice must round all entries, all row totals and all column totals consistently.
Classes, teachers and days are Fin m, Fin n, Fin p; and are natural-number valued, which is the paper's " integer". Constraint (4) of CT1 is written . Floors and ceilings are Nat.floor and Nat.ceil of the rational quotient. In (8) and (9) they are applied to the row and column totals, never summed entrywise. The minimum number of days uses Finset.sup, whose empty value is , and is stated as an equivalence ("solvable over days iff ") rather than as an infimum.
Disclosed choices:
The formalization does not admit a trivial reading: CT3 requires all four constraint families at once, (1) is an equality, and the sanity checks show both that the Figure 1 data satisfy CT3 and that CT1 is not satisfiable for and .
Useful infrastructure, reusable beyond this mission: integral flows with lower bounds, or total unimodularity of bipartite incidence matrices; König's edge-colouring theorem for bipartite multigraphs; floor and ceiling arithmetic for natural-number quotients. Proofs of any milestone, alternative proofs of the goal, and a sorry-free proof of the Figure 1 instance are all welcome.
A committee that chooses one alternative by voting would like a voting procedure under which no member can gain by misreporting their preferences. Such a procedure is called strategy-proof. Gibbard (Econometrica 41, 1973) and Satterthwaite (J. Econ. Theory 10, 1975) proved independently that, once at least three outcomes are possible, the only strategy-proof procedures are dictatorial. The result is the starting point of the theory of strategy-proof mechanisms: it is why mechanism design restricts preference domains (single-peaked preferences, quasi-linear utilities) or allows randomization.
This mission formalizes Theorem 1 of Satterthwaite's paper, in the version circulated as Northwestern University CMS-EMS Discussion Paper No. 122 (revised December 12, 1974). Its formulation has one feature that the textbook version lacks: the hypothesis is on the range of the procedure, not on the whole alternative set, and the dictatorship is accordingly relative to that range.
A committee has a finite set of individuals and a finite set of alternatives. In a strict committee every individual's ballot is a strong order on , a ranking without ties; means that ranks strictly above . The set of strong orders is , and a ballot set is .
A strict voting procedure assigns to each ballot set a single alternative . Its range is the set of alternatives it selects at some ballot set, and , so .
Individual can manipulate at if some ballot gives
an outcome strictly prefers by the standard of the original ballot. The procedure is strategy-proof if no individual can manipulate it at any ballot set.
The procedure is dictatorial if some individual exists such that, at every ballot set , is the element of the range that ranks highest. It is fully dictatorial if in addition and partially dictatorial if .
The proof uses three further notions. Condition U requires that if every ranks the same above all other elements of , then . The procedure is weak alternative-excluding if , and strong alternative-excluding if in addition it satisfies Condition U. Finally is the restriction of to a subset .
For a strict committee with and ,
Theorem 1 characterizes the strategy-proof strict voting procedures completely: given , they are exactly the procedures that let one individual pick, from a fixed menu , their favourite element. The classical statement assumes the procedure can select every alternative; Theorem 1 shows that excluding alternatives from the menu does not help, since a procedure with any menu of at least three alternatives is still governed by one individual. The paper's correspondence theorem with Arrow's social welfare functions (its Theorem 2) and its extension to ballots with indifference (Theorem 1') build on this statement.
The full-range case is on the platform already: AGT.gibbard_satterthwaite (Theorem 9.8 of Nisan–Roughgarden–Tardos–Vazirani, Algorithmic Game Theory) is proved and states that an incentive compatible social choice function onto at least three alternatives has a dictator; it is included here as a reference item and is exactly the case of Lemma 5. The open item MechanismDesign.SocialChoice.gibbard_satterthwaite (Börgers, Proposition 8.1) poses the full-range equivalence. Theorem 1 contains both as the special case . What this mission adds is the range-restricted statement and the paper's own route to it: the induction on the number of individuals for three alternatives (Lemmas 2–4) and the reduction of a procedure with a proper range to its range (Lemma 6 and (27)–(28)). The paper only sketches Lemma 4 and defers the induction on to Satterthwaite's dissertation, so the formal development fills these gaps.
The "if" direction is immediate. For the "only if" direction the natural first idea is to apply the full-range theorem to the procedure viewed as a map into . This fails as stated: the procedure is still defined on rankings of all alternatives, and nothing yet says that its choice ignores how individuals rank alternatives outside . That is the content of Lemma 6, which needs strategy-proofness and Condition U; only after it does the procedure factor through rankings of , and only then is the factor itself strategy-proof. The full-range case itself is the classical theorem, whose known proofs (via Arrow's theorem, or by pivotal-voter arguments) are combinatorial and long.
ι and A; = Fintype.card ι, = Fintype.card A, and the individuals of Lemmas 3–4 are Option ι, with none the individual .agt_social (namespace AGT): a ballot is a relation r with IsStrictTotalOrder A r, r x y is the paper's , and strategy-proofness is AGT.IncentiveCompatible, which is the paper's definition (1) on .Set.ncard. Theorem 1 assumes and ; holds automatically, so is not a separate hypothesis.Two encodings would trivialize the goal and are excluded: a range taken over all relation profiles (junk values would make meaningless), and a dictatorship that only constrains ballot sets at which the dictator's overall favourite lies in , or that asks for the dictator's favourite in all of (false whenever ). The bound is needed: a procedure with two possible outcomes, such as majority vote between two fixed alternatives, is strategy-proof and not dictatorial, and an imposed procedure () is dictatorial only vacuously.
Contributions are welcome at every milestone, and the restriction-to-range step (Lemma 6 and (27)–(28)) is reusable for any statement that transfers results from full-range to range-restricted procedures.
Many limit theorems of probability in Banach spaces, among them the strong law of large numbers and the law of the iterated logarithm for vector-valued random variables, reduce to sharp estimates of the tail probability
for independent random variables with values in a Banach space . For many years these estimates were obtained with martingale methods, and they were not optimal. Chapter 13 of M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces (Publ. Math. IHÉS 81, 1995), explains how the isoperimetric inequalities of the earlier chapters, in particular control by points (Theorem 3.1.1), give such estimates with explicit constants.
Timeline. M. Ledoux observed (unpublished note on Gaussian randomization, reference [L] of the paper) that for Gaussian sums one may split into its conditional mean given plus a deviation, and that the conditional mean has a monotonicity property that replaces positivity arguments ([L], Eq. (13.1)–(13.2) of the paper). Ledoux and Talagrand used this to characterize the Banach-valued random variables satisfying the law of the iterated logarithm (1988). The resulting conviction that an isoperimetric principle was at work led to Talagrand's 1989 isoperimetric theorem (Ann. Probab. 17), superseded in the 1995 paper by Theorem 3.1.1. Ledoux–Talagrand, Probability in Banach Spaces (1991), Theorem 6.17, proves a variant of the bound formalized here that also allows truncation of the variables.
Let be a real Banach space with dual , and let be independent (not necessarily identically distributed) -valued random variables. Let be Rademacher signs: independent, independent of , with . Following the paper, write
where is expectation in the signs only. The conditional mean is . The weak variance of a point is
The decreasing rearrangement is the -th largest norm, and is the sum of the largest norms.
For sets , the -point distance of is
For let and with copies of .
With and , for all integers , and ,
The goal keeps the paper's explicit constants.
The result. Theorem 13.4 bounds the tail of a Rademacher sum in an arbitrary Banach space using three quantities only: the mean , the weak variance , and the law of the largest summands. No moment assumption on the beyond these is needed, and are free parameters to optimize. By symmetrization, such bounds are the main input for the law of large numbers and the law of the iterated logarithm in Banach spaces, for the integrability of sums, and for comparison of moments.
Formalizing it. The result is proved in the paper (and in a different form in Ledoux–Talagrand 1991). It is not formalized: Mathlib has independence, product measures and the dual of a normed space, but no Rademacher sums in Banach spaces and none of Talagrand's isoperimetric inequalities. The mission yields a machine-checked statement of the vector-valued tail bound with explicit constants, connected to the -point inequality (Theorem 3.1.1, posed in mission IV of this series) and to the concentration of for bounded (Theorem 13.2, posed in mission IX).
The obvious approach controls by its mean plus a concentration term. Bounded-difference (martingale) inequalities do not work here: the increments are , which can be unbounded and heavy-tailed, so the resulting bound depends on rather than on the much smaller weak variance . Concentration for the signs conditionally on (Theorem 13.2) gives the weak variance, but at scale , a random quantity. The difficulty is to make both the conditional mean and uniformly controlled on most of the space, at the cost of discarding only a few large summands; a single-point isoperimetric inequality does not supply this.
CompleteSpace W, MeasurableSpace W and BorelSpace W; is W →L[ℝ] ℝ with the operator norm. is a real ⨆ over the dual unit ball, which is nonempty and bounded above by .Fin N → W with = Measure.pi μ for laws μ i (independent, not identically distributed). Signs are Fin N → Bool under the platform's uniform measure Komlos.spMeasure N (referenced). The joint law is the product of the two. Coordinates are 0-based; the rearrangement index is 1-based as in the paper.∫⁻) in , so they need no integrability hypothesis, and makes the goal hold with an empty event. Probabilities are in , so or makes the corresponding term .ℕ∞-valued, and no Bochner integral of a possibly non-integrable function appears.Needed infrastructure: Rademacher sums in Banach spaces, order statistics of finitely many reals, the -point inequality on general product spaces, and Theorem 13.2 for Bernoulli variables. The rearrangement and the -point distance can be reused elsewhere. Contributions are welcome on any milestone, and on proving Proposition 13.3 from a stated form of Theorem 13.2.
A random walk in a random environment on moves one step right with probability and one step left with probability from site , where the are themselves i.i.d. random variables. In his 1975 paper, F. Solomon (Ann. Probab. 3(1):1–31, DOI 10.1214/aop/1176996444) decided recurrence and transience of this walk and computed its speed. Section 4 of the paper isolates a piece of that analysis: the conditional mean time for the walk to cross one bond, given the environment.
Fix the environment, make reflecting, and let be the mean first-passage time from to . Conditioning on the first step gives with , and satisfies a linear recursion with random coefficients (p. 28). The sum is, up to an affine change, the expected time to reach level in that environment. Recursions of the same form, with i.i.d. coefficients, are the random difference equations studied by Kesten (Acta Math. 131, 1973) and Vervaat (Adv. Appl. Probab. 11, 1979); they recur in queueing (waiting-time recursions), insurance (discounted cash flows, "perpetuities") and the analysis of stochastic algorithms.
Let be a probability space and independent, identically distributed, nonnegative real random variables. The system of difference equations (4.1) is
In the Lean development Z σ n ω is defined by this recursion (module SolomonRWRE.DiffEq.System), so it is a function of and needs no existence hypothesis. Unfolding gives the closed form (4.3), .
The mean is (nu P σ); need not be integrable, and is allowed. The products are (rho), and the block sums of the proof are
the sums of the products of consecutive 's inside . For one step of the proof the sequence is extended to a two-sided i.i.d. family (module TwoSided), with .
The goal fixes nothing beyond the paper's hypotheses: any law on , integrable or not. Both cases are almost-sure limits.
If then a.s. and converges in law to ; if the series diverges, in probability; when is defined, the two cases are and .
The result. Theorem (4.4) gives the almost-sure growth rate of the cumulative mean passage time of a random walk in a random environment: linear with slope when , superlinear otherwise. This is the averaged counterpart of the speed law of §1 of the paper (Theorem (1.16)), where the limiting speed is exactly the reciprocal of . The superlinear case is the starting point of the paper's §4 limit laws for (Lemma (4.5) to Theorem (4.9)), which are stated without proof. Lemma (4.2) concerns the single variable , and its dichotomy is a statement about perpetuities .
Formalizing it. The theorem has been proved since 1975; what this mission adds is a machine-checked proof. No result about random difference equations, random products, or this paper is on the platform. The proof needs, for a nonnegative stationary ergodic sequence with possibly infinite mean, the almost-sure convergence of averages in . That convergence is not in Mathlib in this form (Mathlib has the i.i.d. strong law for integrable variables, ProbabilityTheory.strong_law_ae), and Birkhoff's pointwise ergodic theorem is posed on the platform as an open item (Birkhoff1931.tendsto_birkhoffAverage_condExp). A completed mission therefore leaves behind a nonnegative, infinite-mean ergodic theorem for block products of i.i.d. sequences, which is reusable well beyond this paper.
The obvious argument fails at independence. is a sum of products sharing the factor , so are neither independent nor stationary, and no law of large numbers applies to them directly. The regrouping into produces sums of -dependent block products, which are stationary but not independent, so the i.i.d. strong law does not apply either. Moreover there are such groups at time , so letting and grow together needs a uniform argument: Fatou's lemma gives only the lower bound. The upper bound requires a different object, , which is stationary because it looks infinitely far into the past, and it exists only because makes the backward series converge. A second trap is the infinite-mean case: may be non-integrable, and every integrability-based ergodic or strong-law statement must be adapted to nonnegative variables with values in .
σ : ℕ → Ω → ℝ; the hypotheses (IsIIDNonneg) are on (the shifted family n ↦ σ (n + 1)): measurable, pointwise nonnegative, mutually independent (iIndepFun), and identically distributed with (IdentDistrib). is unused and unconstrained.∫⁻). A Bochner integral would return for a non-integrable , which would put and make the goal false; this trivializing reading is excluded by the definition of nu.ENNReal.ofReal, which loses nothing because . In the case , is computed in and is finite.Finset.Icc 1 n); in the upper limit uses natural-number subtraction, which gives the empty sum for .IsIIDNonnegZ on σ : ℤ → Ω → ℝ; is computed from its restriction to . This mirrors the page's "without loss of generality"; the goal keeps the one-sided family.TendstoInDistribution; "" is for every ; is the difference of the -valued expectations of its positive and negative parts, required not to be both infinite, with .Contributions welcome beyond the milestones: an ergodic theorem for nonnegative stationary sequences with values in ; the identity ; and the construction of a two-sided i.i.d. extension of a one-sided sequence, which turns milestone 5 into a statement about the goal's sequence.
A renewal process models the successive replacements of an article that fails and is replaced at once: light bulbs, machine components, the inter-arrival times of a queue. The central quantity is the renewal function , the expected number of replacements up to time . Long-run average costs of maintenance and inventory policies, the throughput of regenerative systems and the rates in renewal–reward arguments are all read off the growth of . W. L. Smith's survey Renewal Theory and Its Ramifications (J. R. Statist. Soc. B, 1958) organized the field around this function and opened with its oldest general limit result, the elementary renewal theorem, proved in full in §1.2 (pp. 245–247).
Timeline.
Let be a probability space and real random variables that are mutually independent, identically distributed, non-negative, and not almost surely zero: . Lifetimes equal to zero with positive probability are allowed.
In Lean these are IsRenewalProcess P X, S X n, N X t, H X P t, mu1 X P, zeta X t and trunc Δ X in the namespace SmithRenewal.Elementary.
with and when . No moment beyond the first is assumed, and not even the first: the infinite-mean case is part of the goal.
The result. The elementary renewal theorem is the law of large numbers for the renewal function: in the long run renewals occur at mean rate . It is the basis of the renewal–reward theorem, of long-run average cost formulas for replacement, maintenance and inventory policies, and of rate computations for regenerative queues. The sharper results of Smith's survey — Blackwell's theorem (1.2) and the key renewal theorem (1.3) — refine it and reduce to it on averaging.
Formalizing it. The theorem has been proved since 1941; what this mission adds is a machine-checked development of the continuous-time, real-valued renewal process in Lean, which Mathlib does not contain. Mathlib has the strong law of large numbers, independence and identical distribution, but no renewal counting process, no Wald identity and no renewal function. The platform holds a proved discrete Erdős–Feller–Pollard theorem for integer renewal sequences, a different statement about a different object; to the curators' knowledge the elementary renewal theorem for general non-negative lifetimes has not been formalized.
The almost-sure statement is close to the strong law, since . The obvious next step, taking expectations, fails: almost-sure convergence does not imply convergence of means, and has no evident integrable dominating function. The exact relation (1.1) involves a sum with a random number of terms stopped at , and by itself it bounds from one side only, because the residual lifetime can have infinite mean. When the relation is unavailable altogether, yet the theorem still claims a limit. Throughout, is a priori allowed to be infinite on a null set and to be infinite, so finiteness itself is part of what must be established.
X : ℕ → Ω → ℝ, with the paper's as X 0, X 1, …. IsRenewalProcess P X bundles measurability, mutual independence (iIndepFun), IdentDistrib (X i) (X 0), non-negativity at every sample point, and P {X 0 = 0} < 1. Strict positivity is not assumed.ℕ∞ of ; it is for and may be on a null set.ENat.toNat; on the null event this is , which never affects an expectation.trunc Δ X, never separate formulas.Ruled out. A goal restricted to , a renewal function defined through or the renewal equation, or a real-valued ratio with in (where and an infinite integral becomes ) would each be a different, weaker or trivially true statement; none of them is the goal.
Needed infrastructure and welcome contributions. A Wald identity for stopping indices of i.i.d. sums with values in ; the comparison of a renewal count with a negative binomial count; uniform-in- moment bounds for ; and the lim inf/lim sup squeeze in . The renewal process definitions and the Wald identity are reusable for Blackwell's theorem, the key renewal theorem and renewal–reward arguments. Alternative proofs of the goal (Feller's Tauberian route, a uniform-integrability argument) are welcome as long as they prove the stated goal.
An arbitrator choosing an outcome for several people can ask them about their preferences, but the answer to that question may affect the outcome. A person who expects to gain from a false report may give one. Roger Myerson's 1979 paper puts this incentive problem inside a bargaining model: the arbitrator may randomize over collective choices, and an allocation is considered feasible only if some mechanism makes truthful reporting an equilibrium. The paper then applies a weighted Nash bargaining criterion to the resulting set of feasible interim payoffs. The mission formalizes the existence and uniqueness result for that criterion, along with the finite Bayesian model on which it depends.
The issue matters whenever an agreement is selected using information known privately to its participants. If the arbitrator evaluates a payoff vector that can arise only when somebody has a reason to lie, that vector cannot serve as a credible bargaining alternative under the model's own behavior assumption. Myerson's feasible set keeps the behavioral constraint visible when the group compares agreements. This mission addresses the paper's Theorems 1 and 3 and the claims between them that establish the relevant sets and their reference point.
Let be a nonempty finite set of players. Player has a nonempty finite type set , and the group has a nonempty finite set of possible choices. A type profile is . The utility is player 's payoff when choice occurs and is the true profile. A nonnegative function on type profiles, summing to one, is the common prior. Write for the probability that player has type , and for the posterior probability of conditional on that type. Every is positive, so the conditional probabilities are defined.
A choice mechanism asks each player for a response and assigns a probability to each choice at each response profile . For the direct mechanisms used here, the response set of player is : a response is a claimed type. The probabilities are nonnegative and sum to one for each response profile. If a player whose true type is instead reports , while the others report truthfully, the player's conditional expected utility is . The posterior weights true profiles; the mechanism sees the profile with only coordinate replaced by ; and utility is evaluated at the true profile .
The mechanism is Bayesian incentive-compatible when for every player and pair of types. Its interim payoff vector has one coordinate for every player-type pair. The set contains the vectors attained by all direct choice mechanisms; contains those attained by Bayesian incentive-compatible direct choice mechanisms. Theorem 1 says is nonempty, convex, compact, and contained in . The nonemptiness claim includes the mechanism that selects each choice with probability , independent of all reports.
Fix a conflict outcome : the choice that occurs if bargaining fails. Its conflict payoff vector gives each player type the conditional expected utility from that fixed choice. A constant mechanism selects regardless of reports. It is incentive-compatible and generates , so . The individually rational incentive-feasible set is
For , the generalized Nash product of equation (18) is
A bargaining solution is a vector in that maximizes over that set. Myerson's Theorem 3, the goal of this mission, says that if the constant conflict mechanism is not incentive-efficient—that is, an incentive-compatible mechanism strictly improves every player-type payoff over it—then exactly one such vector exists:
The milestones follow the paper's claims: the uniform mechanism is incentive-compatible; has the four properties in Theorem 1; the conflict vector belongs to ; every Nash-product maximizer strictly improves each conflict payoff when such improvement is feasible; and every implementing mechanism is incentive-efficient. The final claim concerns a mechanism that realizes the maximizing vector. It does not assert uniqueness of that mechanism.
Theorem 1 supplies a feasible set that respects truthful reporting. Theorem 3 selects a unique interim payoff vector from that set after a conflict outcome is specified. It thereby gives a well-defined allocation criterion for the paper's finite Bayesian collective choice problems. Myerson also observes that several mechanisms may implement the same solution. The allocation, rather than a unique mechanism, is the object selected by the theorem.
The result was proved in the 1979 paper. The work here is a machine-checked statement and, for solvers, a proof of that known result and its supporting claims in Lean. The mission's statements are open proof targets; the source paper's proof is not claimed to have been formalized already. A related platform item on Nash's two-player axiomatic characterization concerns a solution function on compact convex subsets of . It is a distinct result and supplies neither this paper's Bayesian model nor Theorem 3.
The set of all real-valued functions on choices and reports is much larger than the set of mechanisms: probabilities must be nonnegative and sum to one at every report profile. Bayesian incentive compatibility adds inequalities involving the true and reported type in different positions. Theorem 1 requires these constraints to give the compact, convex set of attainable interim payoffs, rather than merely a formal collection of payoff functions.
The Nash product also has a boundary: an individually rational vector may match the conflict payoff in one coordinate, making its product zero. Theorem 3's hypothesis has to rule out a zero maximum before uniqueness of an interior maximum can be concluded. The weights matter in that uniqueness statement, and the result ranges over all player-type coordinates, not only one aggregate payoff per player. Restricting the maximization to an arbitrary small subset, fixing two players, or assuming a positive maximum would change the theorem.
Lean represents players, each type set, and choices as finite nonempty types. Type profiles are dependent functions ; interim vectors are real functions on the disjoint union , with the product topology. A mechanism is a real function subject to explicit nonnegativity and sum-to-one constraints. Both and quantify only over functions satisfying those constraints. Conditional beliefs use the common prior in equations (3)–(4), and positive marginal probabilities make every denominator meaningful without requiring positive probability for each full profile. The positivity of every is an assumption the paper makes implicitly by dividing by it in (3); it is a field of the problem structure, not a hypothesis of the theorems. The subjective reading of and that the paper permits on p. 63, the response-plan equilibria of Section 3, and the numerical example of Section 6 are outside this mission.
Strict dominance means a strict gain for every player type. The constant mechanism, conflict vector, and individually rational set are defined from the problem data. The conflict vector is defined by equation (16), while its equality with the constant mechanism's payoff is a theorem item. The product uses real powers with the paper's marginal weights and is compared only on , where each base is nonnegative. A solution is a maximizer property; it is not chosen in advance or supplied as a theorem hypothesis. These choices exclude vacuous encodings of incentive efficiency, unrestricted mechanisms, and a maximization domain that already contains only a nominated winner.
A complete proof development needs finite sums and products, continuous and convex maps on finite-dimensional real spaces, compactness of the constrained mechanism set, and facts about positive weighted real powers or logarithms on the strictly positive region. The model definitions can be reused for the paper's separate revelation-principle mission; this mission also welcomes proofs of the explicit claims about the uniform mechanism, the conflict mechanism, and product maximizers.
A product made by a chain of operations can carry stock in front of every operation, between every pair of them, and as finished goods. Each such inventory point buffers demand uncertainty, and each costs money to hold. Kenneth F. Simpson, Jr. asked which of these points should carry stock at all, and how much, in In-Process Inventories, Operations Research 6 (1958) 863–873. His answer is that the cheapest configuration is an extreme one: every inventory point is either kept full or eliminated.
The paper is the origin of what is now called the guaranteed-service model of multi-echelon inventory theory.
There are operations in series. Operation has a processing time . Behind each operation is an inventory point that promises to fill any order within a service time . The incoming service time (from raw materials) and the outgoing one (to the customer) are fixed constants; the intermediate service times are the decision variables. Inventory must protect against demand over the time , and under the paper's demand model its holding cost is proportional to the square root of that time. With constants and the total inventory cost is equation (9):
Its domain is the set of points with every variable nonnegative and every radicand nonnegative:
is a polyhedron cut out by affine inequalities. A vertex of is an extreme point: a point of that is not the midpoint of two distinct points of . An inventory with has zero average stock; one with is full.
For any constants and with ,
This is the paper's sentence "the minimum of the function occurs at one of the vertices of ", read as existence of a vertex minimizer. It fixes no constant and no particular vertex.
The p. 870 rephrasing, "for an optimal system, the service time for every nonvanishing inventory is zero", is already proved on the platform as SupplyChainTheory.gs_all_or_nothing (Snyder–Shen Theorem 6.5) and is included as a reference item. Under the dictionary stage , , , that statement is Simpson's model case .
THEOREM I turns a continuous optimization over the polyhedron into a comparison over its finitely many vertices, and in Simpson's model these are the all-or-nothing configurations. Each vertex has a physical reading as a mode of operation: which inventories are kept full and which operations are tightly coupled (THEOREM II). The property is what makes guaranteed-service models tractable by enumeration or dynamic programming in later work.
The result is proved in the paper, by an induction on faces. It has not been machine-checked. A formal development adds a checked statement of the theorem for general constants (the paper's model fixes ), an exact account of which hypotheses are needed (the positivity of the is essential, see below), and a checked vertex count for the model case. The existing platform theorem gs_all_or_nothing covers the model case in the all-or-nothing form; THEOREM I with general constants and the vertex characterization are not yet on the platform.
The domain is given by inequalities, while the conclusion is about its extreme points, which are never listed: with general constants the vertices of have no closed form, and may be lower-dimensional or have coinciding facets. Any argument therefore has to connect an inequality description of a polyhedron with its extreme-point structure, which in the paper's own text is treated informally ("faces", "edges", "an -fold repetition"). LEMMA I and LEMMA II are stronger than the existence statement: they exclude minimizers in the interior of and in the relative interior of a face, and they become false as soon as some vanishes, so they cannot follow from concavity alone. THEOREM II, though described on the page as "examine the definitions", requires an exact reindexing of the operations, processing times and cost coefficients after one variable is removed.
The sign hypothesis cannot be dropped: with , , , , , , the function on is convex and its only minimizer is the interior point .
All declarations live in SimpsonInv.Vertex. With variables a point of is S : Fin m → ℝ, and Lean index holds the paper's ; extVec S0 Sn S i returns the paper's for every , including the constant ends. The constants are sequences ℕ → ℝ, read only at indices . The space Fin m → ℝ carries the product topology, which is the Euclidean one, so interior is the paper's interior. A vertex is an element of Set.extremePoints ℝ D; a minimizer is IsMinOn f D v with .
Added hypotheses, each disclosed in its item: for (from equation (8); weakened to for concavity and dropped for existence and THEOREM II); where a minimum is asserted; at least one variable for LEMMA I and at least two for LEMMA II; and only for the vertex count, as in the paper's model. The page's "-dimensional polyhedron" is not imposed: the goal is stated for every nonempty . "On the boundary of the faces" (LEMMA II) is encoded by at least two independent active inequality normals, including when inequalities coincide.
Real.sqrt returns on negative inputs, so is never compared outside . Minimizing over all of , or replacing the vertex set by a hand-listed finite set of points, would trivialize or falsify the goal and is ruled out: the goal quantifies over Set.extremePoints ℝ D and compares only on . THEOREM II compares the original cost with the same cost function applied to new data ( operations, , ), not with a substituted copy of the original.
A complete development needs compactness and extreme-point facts for polyhedra given by inequalities and concavity facts for square roots and powers of affine maps; both are reusable well beyond this mission. Proofs of any milestone, and reusable lemmas on polyhedra given by inequalities, are welcome.
An online learner predicts a binary label for each instance before seeing that instance's correct label. Its guarantee is usually measured by its worst possible number of mistakes against a target function. Such guarantees can differ greatly across target functions: an algorithm might learn one target quickly while taking much longer on another. Littlestone and Warmuth's analysis of the Weighted Majority Algorithm asks which collections of individual mistake guarantees can coexist for one deterministic learner. In Section 7 of their 1994 paper, they isolate a condition under which these guarantees obey a strict numerical constraint. The condition concerns how the target functions vary together over the instance domain, so the result applies without a probability distribution on instances or labels.
The theorem also supports the paper's comparison between arbitrary deterministic learners and Weighted Majority. Given individual mistake bounds, its inequality is the numerical condition that makes a suitable initial weighting of the target functions possible in Theorem 7.1 and Corollary 7.1 of the same paper. The present mission centers on the inequality itself, which is independent of a particular implementation of Weighted Majority.
Let be an instance domain, possibly finite or infinite, and let be a finite family of target functions. A trial presents an instance to a learner, asks it to predict either or , and then reveals a label. A finite sequence is consistent with when each revealed label equals at that trial's instance. The learner may use the current instance and the complete history of earlier labeled trials when predicting; it does not see the current label first. No sampling or independence assumption is made.
The family is shattered by its domain when every pattern appears as the vector of function values at some instance:
This is a dual notion of shattering. The familiar VC condition asks whether a class of functions realizes every labeling of chosen instances. Here the domain realizes every joint value pattern of a chosen family of functions. The two conditions should not be interchanged.
Let be any deterministic online learner. Write for the supremum of the number of mistakes made by over every finite sequence consistent with . Since mistake counts are natural numbers, a finite supremum is an attained natural-number maximum. The theorem assumes each is finite. In the Lean representation, this is a separate finiteness condition on each target's extended-natural mistake bound.
The goal is Theorem 7.2 of Littlestone and Warmuth, pp. 244–245. For every domain, every finite family shattered by that domain, and every deterministic online learner with finite individual mistake bounds,
The inequality is strict. Replacing it by a weak inequality would lose the stated result and the threshold used in the paper's later comparison with Weighted Majority. The theorem quantifies over the learner itself; it does not select a specially behaved learning rule.
Lemma 7.1 concerns positive real numbers with integral adjacent quotients. When a positive target is no larger than their sum and is integral, some prefix sums exactly to . Lemma 7.2 concerns positive powers of two with integer exponents. If a power lies at least as high as each individual weight and at most as high as the total weight, some subset sums exactly to . Both statements and their exact source wording are recorded as the mission's milestones; they are the numbered arithmetic results used in Theorem 7.2.
The theorem limits the set of claims that one deterministic learner can make simultaneously. Small contribute large terms to the sum, so a learner cannot have arbitrarily small worst-case mistake counts for all members of a domain-shattered family. This is a worst-case statement about every finite consistent trial sequence, rather than an average-case statement about a chosen data distribution. The paper's Corollary 7.1 uses the resulting inequality to select initial weights for a Weighted Majority comparison, but that later algorithmic statement is outside this mission's goal.
Formalizing this result adds a reusable dual-shattering predicate and an exact constraint on per-target online mistake bounds to the existing online-learning definitions. The paper proves the theorem, while the mission's Lean goal and its two milestone lemmas are open proof obligations. The separate published online-learning module provides the definitions of deterministic predictors, trial histories, mistake counts, and extended-natural worst-case bounds; it does not already prove this theorem.
For a single target, an arbitrary learner may have a small finite mistake bound. The difficulty is relating those bounds across different targets without placing extra restrictions on the learner. Domain shattering gives the adversary control over the simultaneous predictions of all functions at an instance, but the labels of one trial sequence must still remain consistent with a target. A simple count of targets or of possible patterns does not directly produce the strict weighted sum, particularly when the different are unequal. The two arithmetic lemmas address exact sums of structured weights; the main theorem must also connect such weights to the learner's worst-case mistakes.
The function family is indexed by Fin n, with zero-based Lean indices corresponding to the paper's . The domain is an arbitrary type and may be infinite. Labels and predictions are Bool. ShatteredByDomain states that every Boolean pattern is realized by some domain point. The published UnderstandingML_Online definition gives OnlineAlg X Bool, finite trial histories, mistakes, and mistakeBound. The latter is valued in and ranges over all finite sequences labeled by the target. Each is converted to a natural number only after assuming its bound is finite. The powers and their finite sum are real numbers. The conclusion is the empty sum ; the shattering predicate itself then requires an instance to realize the unique empty pattern.
The two milestones use real-valued weights. Lemma 7.1 assumes because the source refers to . Lemma 7.2 represents the source's integral base-two logarithms by equations with integer , which also enforce positivity. Its maximum hypothesis is written pointwise, so an empty family is harmless: the other inequality cannot hold. A coordinate family on is verified locally to satisfy the shattering predicate, ruling out a vacuous encoding of that central assumption. Contributions proving either arithmetic milestone or the main theorem within these exact definitions are in scope.
A Nash equilibrium is a joint choice of strategies at which no player can improve their own expected payoff by changing their strategy alone. This gives a testable notion of stable behavior for a finite game, including games in which the players' aims differ. Nash's two-page 1950 note established the existence of such a point for finite games by organizing each player's best replies into a single correspondence and using a fixed-point theorem. The note identifies several properties of that correspondence and ends by comparing equilibrium payoffs in zero-sum and general games. Those claims, stated together in Nash's published note, are the subject of this mission.
The existence conclusion itself already has a proved formal statement, AGT.nash_existence, in the game vocabulary used here. The remaining claims explain what the fixed-point argument acts on: which profiles are related by countering, why countering sets are usable as values of a correspondence, and what their fixed points mean. Keeping those statements explicit makes the 1950 argument legible independently of the existence theorem's proof.
There is a finite set of players. Each player has a finite, nonempty set of pure strategies. A pure-strategy profile chooses one element of every , and is player 's payoff. A mixed strategy assigns a nonnegative real weight to each element of , with weights summing to one. The space of mixed profiles is the product of these finite probability simplices.
Players randomize independently. Thus the probability of a pure profile under is , and player 's expected payoff is
For a strategy of player , write for the payoff obtained by replacing only coordinate of . A profile counters if and, for every player , its coordinate gives that player the highest expected payoff available against the other players' coordinates of :
The countering correspondence assigns the set to each . Its graph comprises the pairs with and . A fixed point is a profile belonging to ; Nash calls it an equilibrium point.
The goal states the three properties of that Nash uses, along with the identification of its fixed points:
The milestone list follows the claims in the note: the payoff functions are polylinear and continuous; the correspondence maps mixed profiles to nonempty subsets of mixed profiles; its values are convex; its graph is closed in the sequential formulation Nash writes; and self-countering is equilibrium. A separate closed-set formulation records the graph property in the product topology.
The note also asserts a distinction about payoffs. In a two-person zero-sum game, where on every pure profile, any two equilibria have the same expected payoff for each player:
For general games, this can fail. A companion target asks for a finite two-person game with two equilibria having different expected payoffs.
The correspondence theorem records the precise conditions on which Nash's application of Kakutani's fixed-point theorem rests. Nonempty convex values and a closed graph make the fixed-point route applicable to the mixed-strategy space; the fixed-point clause says why its output is an equilibrium of the game rather than only a topological point. The zero-sum companion separates the common value of a two-person zero-sum game from the possible range of equilibrium payoffs in a general game. These consequences and the comparison appear in Nash's note.
The equilibrium existence theorem is already proved as the referenced AGT.nash_existence. What remains here is to formalize the correspondence properties and the payoff comparison as their own auditable statements, using that theorem's published game definitions. The claims are known results from 1950; their appearance as goals means proofs of these particular statements are still to be supplied in this development.
The payoff of a player depends on every player's strategy, while countering compares only one changed coordinate at a time. The relevant set of maximizers is therefore indexed by the countered profile, and all players' choices must fit into one countering profile. Establishing closedness requires passing the payoff comparisons and the probability-vector conditions through limits of profiles. The zero-sum equality concerns arbitrary pairs of equilibria, which need not use the same strategies; an argument based only on the existence of an equilibrium cannot give it. For general games, a single equilibrium says nothing about whether another equilibrium has a different payoff.
The Lean development uses a finite player type ι, finite pure-strategy types S i, real payoffs u, and the published definitions AGT.IsLottery, AGT.IsMixedProfile, AGT.expectedPayoff, and AGT.IsMixedNash. The goal and nonempty-value milestone require each S i to be nonempty. The note's probability distributions implicitly require this; the player type itself may be empty. A mixed profile is a tuple of finite real weight vectors, with no measure-theoretic integration or hidden normalization. In the two-person claim, players are 0, 1 : Fin 2.
Convergence is in the ordinary product topology of the real coordinate spaces. The sequence index is because the note also uses for the number of players. Counters u P Q requires to be a mixed profile and compares with every mixed deviation against ; this rules out arbitrary weight vectors and comparisons against the wrong opponents. Neither continuity nor the existence of a best response is assumed in the goal: those properties are targets. The definition layer and the payoff continuity and polylinearity results can be reused by other finite-game formalizations.
The newsvendor problem is the basic single-period inventory model: a decision maker orders units before a random demand is observed, pays per unit of unmet demand and per unit left over, and minimizes the expected cost . When the distribution of is known, the optimal order is the quantile of . In practice the distribution is unknown and only a sample of past demands is available; the standard data-driven order is the sample average approximation (SAA), the quantile of the empirical distribution.
R. Levi, G. Perakis and J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights (Operations Research 63(6), 2015), ask how many samples guarantee that the SAA order is -optimal with high probability. Levi, Roundy and Shmoys (2007) gave a distribution-free bound. Levi, Perakis and Uichanco show that, asymptotically in , the right measure of difficulty is a single scalar of the demand law, the weighted mean spread at the critical quantile, and that for the class of log-concave demand distributions (normal, uniform, exponential, logistic, Laplace and many others used in inventory theory) this scalar is bounded below by . That uniform bound turns a distribution-dependent sample-size guarantee into one that holds for every log-concave demand, and is markedly tighter than the distribution-free one.
This mission formalizes the bound (Proposition 2) and the chain of lemmas the paper uses to prove it. The source is the authors' accepted manuscript of the paper (MIT DSpace), cited by its own page numbers.
Fix costs , and the critical ratio . A demand law is given by a probability density : measurable, nonnegative, with . Its cdf is , and its quantile is
The absolute mean spread (AMS, Definition 1) at is the gap between the conditional means above and below ,
and the weighted mean spread (WMS, Definition 2) is .
A density is log-concave (Definition 3) if is concave on its support. Equivalently, for all and ; this form allows to vanish outside an interval.
For a log-concave and a point with , the number is a supergradient of at , written , if for all with . The paper splits the class of log-concave densities into the subclasses of densities with quantile , and , and minimizes the AMS over each subclass (problem (11)). The minimizer is the truncated exponential density
and zero elsewhere (display (12)), with AMS in closed form.
The Lean development uses the names IsPdf, cdfOf, quantileOf, ams, IsLogSupergradient, tildeF and zStar for these objects, in the namespace DataDrivenNV.WMS.
For every log-concave density ,
The statement has no further hypothesis: no moment condition, no continuity, no restriction on .
The proposition is what makes the paper's log-concave sample-size bound (Theorem 4) parameter-free: the probability that the biased SAA order is -optimal is, asymptotically, at least (Theorem 3), and Proposition 2 replaces the unknown by . A manager who only knows that demand is log-concave can then size a sample without estimating any parameter of the law.
The result is proved in the paper; nothing about it is open. As far as is known it has no machine-checked proof. Formalizing it produces a checked lower bound for an inventory-theory quantity together with reusable facts about log-concave densities on the line: exponential envelopes from a supergradient, the quantile-and-slope constraints of Lemma 1, and the comparison of conditional means behind the Domination Lemma.
The definitions are elementary, but the proof passes through an infinite-dimensional optimization problem over a class of densities. The obvious first step, "the AMS is minimized by the most concentrated density", has no direct meaning without fixing the density value and the slope of at the quantile; after fixing them, one needs the envelope of Lemma 2, a stochastic comparison (Lemma 3) and an explicit integral of a truncated exponential. The Domination Lemma as printed is false (a density whose support has a gap to the right of is a counterexample), so it is formalized under the hypothesis that the dominating density is positive exactly on an interval around , which is how Proposition 1 uses it. The case (uniform minimizer) and the two boundary values of (one-sided exponential minimizers) are not covered by the closed form (12) and must be handled separately in a proof of the goal. Finally, Lemma 1 rests on the monotonicity of the failure rate and the reversed hazard rate of log-concave laws, which must be proved from log-concavity.
Densities are functions ℝ → ℝ with IsPdf f (measurable, nonnegative everywhere, integrable, total integral 1); the law of is never introduced separately. Log-concavity is the published definition ConvexOptimization.LogConcaveOn Set.univ f (power form, zeros allowed). Concavity of Real.log ∘ f is not used, because Real.log 0 = 0 would treat as off the support. The quantile is an sInf; for its defining set is nonempty and bounded below. The AMS is the difference of two ratios of integrals. At the quantile both denominators are positive, and the goal and Proposition 1 assume no integrability of , since log-concave densities have exponential tails. The value is taken pointwise; lies in the interior of the support, where a log-concave density is continuous.
Conventions and disclosed departures from the page:
Assumption 1 of the paper (monotonicity of beyond ) and the continuity assumption of §3 are hypotheses of Theorems 3–4 only and are not used here. A formalization in which or takes a junk value (a non-integrable , a zero denominator) would make the goal trivially true or false; the hypotheses above exclude this, and no statement assumes the conclusion of another.
Contributions welcome: proofs of the milestones in any order; general lemmas on log-concave densities on (exponential tails, integrability of moments, monotone hazard rates, continuity in the interior of the support); and the boundary cases of problem (11).
Monotone sequences of random elements arise wherever a quantity can only grow: cumulative work or queue contents under a monotone recursion, the iterates of a monotone operator applied to a random initial state, or the successive approximations produced by coupling constructions in which each stage dominates the previous one. When the values live in a partially ordered space rather than on the real line (vectors with the coordinatewise order, functions with the pointwise order, measures with a stochastic order), the classical fact that a bounded nondecreasing real sequence converges no longer applies directly, and one needs a statement about which modes of convergence are automatic.
Kamae, Krengel and O'Brien answer this in Section 6 of Stochastic Inequalities on Partially Ordered Spaces (Ann. Probab. 5 (1977) 899–912). Their Theorem 6 shows that, for a nondecreasing sequence in a partially ordered Polish space, three modes of convergence that are in general strictly ordered by strength (tightness of the laws, weak convergence of the laws, convergence in probability) coincide, and it identifies exactly when almost sure convergence joins them. The paper announces an application of Theorem 6 to a new pointwise ergodic theorem in a forthcoming paper of Krengel. This mission formalizes Theorem 6 and its proof steps; the source is the published Annals of Probability version, and printed page numbers equal PDF page numbers plus 898.
Let be a Polish space with metric : a complete separable metric space. It carries a closed partial ordering , meaning a partial order whose graph is a closed subset of , and its Borel -algebra. These are the paper's standing assumptions (Sec. 1, p. 899).
Let be a probability space and measurable maps (random variables) that are nondecreasing: for every . Write for the distribution of . The four modes of convergence are:
The space satisfies condition (17) if for all sequences with for every , implies . In Lean this is Regular17 E, and the modes are LawsTight, LawsConvergeWeakly, ConvergesInProbability and ConvergesAS.
For every probability space and every nondecreasing sequence of random variables in ,
and
The result. Without monotonicity, tightness gives only weakly convergent subsequences (Prokhorov), and weak convergence of laws says nothing about the random variables themselves. Theorem 6 says that order removes both gaps: tightness of the marginal laws of a monotone sequence already produces a limiting random variable, in probability. Its second part gives an intrinsic, checkable criterion on the ordered space, condition (17), for upgrading this to almost sure convergence, and the Remarks show the criterion is not automatic. Coordinatewise-ordered satisfies (17), so there all four modes coincide for monotone sequences.
Formalizing it. The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. Mathlib has tightness, Prokhorov's theorem in one direction, weak convergence of probability measures and convergence in measure, but no results relating these modes for order-monotone sequences. The mission produces a formal proof of all four implications and of the characterisation by (17), together with a formally verified example of an ordered Polish space violating (17).
The obvious argument for (i) ⇒ (iii) imitates the real line: on each the sequence is monotone and lies in a compact set "most of the time", so it should converge. Two things fail. First, the sequence need not stay in one compact set: tightness controls each separately, and a fixed may leave infinitely often; only the subsequence of visits to is relatively compact. Second, there is no supremum available in a general partial order, so the real-line argument for the existence of a limit has no analogue, and without the closedness of the order the statement is false. Turning the pointwise statement into convergence in probability then requires a uniformity argument across . For the second part, the natural attempt to pass from a subsequence converging almost surely to the whole sequence fails without (17), which is the content of the counterexample.
The space carries [MetricSpace E] [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] [PartialOrder E] [OrderClosedTopology E]. Second countability is equivalent to separability for metric spaces, and OrderClosedTopology is exactly a closed partial ordering. The closed order cannot be dropped: (i) ⇒ (iii) fails without it. Conventions committed to:
ProbabilityMeasure, stated through integrals of bounded continuous functions (equivalent to Mathlib's topology on probability measures for measurable ).TendstoInMeasure to a measurable limit; the a.s. limit in (iv) need not be measurable.Type; "(iv) is also equivalent" is encoded as (iv) ⇔ (iii). The quantifier over all probability spaces and all nondecreasing sequences is essential: for one fixed sequence the "only if" direction is false, and fixing would make the statement about one space rather than about .A trivializing formalization is ruled out: no hypothesis forces the sequence to be constant, the modes are not defined in terms of each other, and the second part quantifies over every probability space and sequence.
Reusable infrastructure: the four modes of convergence for random elements of a metric space, and the identification of limits through closed orders. Contributions welcome: proofs of the standard implications (iv) ⇒ (iii) ⇒ (ii) ⇒ (i) in Polish spaces, the milestone proofs, and a proof that coordinatewise satisfies (17).
In a finite game, a referee can recommend one action privately to each player according to a joint distribution. The recommendations may be correlated: learning one's own recommendation can convey information about the others'. A correlated equilibrium is a distribution for which no player gains, in expectation, by replacing a particular recommendation with another action. This solution concept uses the same payoff data as a strategic-form game but allows more joint distributions than independent mixed strategies. Hart and Schmeidler's Theorem 1 establishes that at least one such distribution exists for every finite game, with no assumptions on the payoffs beyond being real-valued. Their paper uses the finite result as the starting point for existence results with infinitely many players and, later, compact strategy spaces. Hart and Schmeidler (1989)
The authors explain that the standard route passes through a mixed Nash equilibrium: independent equilibrium strategies induce a correlated distribution. The finite theorem here is the same existence conclusion expressed directly through recommendation inequalities, which are linear in the joint distribution. That distinction matters for the later sections of the paper, where the authors examine games with infinitely many players, including an example with a countably additive correlated equilibrium but no Nash equilibrium. Hart and Schmeidler (1989), pp. 18, 21–22
Let be a finite player set. Each player has a finite, nonempty set of pure strategies, and a pure profile is a tuple in . The real number is player 's payoff at . For a player , write for all coordinates except and for the profile obtained by replacing the th coordinate with . A probability vector on is a function with for every and . These are exactly the paper's finite-game and probability-vector conventions. Hart and Schmeidler (1989), pp. 18–19
Suppose the referee draws with probability and privately tells player only . For every recommended action and alternative action , the incentive inequality is
When the recommendation has zero probability, this inequality holds automatically. Thus no conditional probability needs to be defined in that case. A probability vector satisfying every such inequality is a correlated equilibrium. The inequalities include , whose left-hand side is zero. Hart and Schmeidler (1989), p. 19, condition (1)
The mission's goal is the paper's Theorem 1, with its definition of correlated equilibrium kept explicit:
Here denotes the set of probability vectors on the finite set . The quantified payoffs are arbitrary real functions; the result specifies neither a unique equilibrium nor a particular equilibrium distribution. The milestone list records the paper's auxiliary-game correspondence, its finite minimax criterion, the nonnegative-matrix lemma, equation (2), and the final product-strategy identity. The lemma is linked to the already proved platform theorem CalibratedCE.Forecast.flow_conservation_solvable, which states the equivalent balance equations for a nonnegative matrix indexed by a nonempty finite set. Hart and Schmeidler (1989), pp. 19–20
The result guarantees feasibility of the complete system of recommendation inequalities for every finite payoff table. It is stronger as a foundation than checking an equilibrium in one game: later arguments can invoke the result after restricting a larger game to finite strategy sets. Hart and Schmeidler do exactly that in their infinite-game existence theorems. The finite theorem is already known mathematically; the task here is to give its particular statement and proof structure reusable, machine-checked declarations. Hart and Schmeidler (1989), pp. 20, 22, 24
The platform already has the general finite-game lottery vocabulary in agt_games and a proved mixed Nash-existence theorem, AGT.nash_existence. It also has AGT.IsCorrelatedEquilibrium in swap-function cost notation, AGT.swap_regret_correlated_equilibrium for approximate equilibria, and Aumann 1987's finite-probability-space model. Those results provide related notions and consequences. With and costs , the swap-function form of AGT.IsCorrelatedEquilibrium is equivalent to condition (1), since a switching rule can be optimized separately for each recommendation; the mission nevertheless states condition (1) as printed. The finite Minimax Theorem invoked on p. 19 is proved on the platform as AGT.zero_sum_minimax (a saddle-point statement for matrices indexed by Fin (m+1) and Fin (n+1), in another Mathlib environment), so the minimax milestone is the consequence the paper draws from it rather than the theorem itself. This mission fixes Hart and Schmeidler's payoff-maximizing condition (1) directly, with its recommendation-specific inequalities and auxiliary-game steps. The linked flow-conservation theorem was formalized in the Foster–Vohra series; its balance equations have the same content as the lemma on p. 19 after expanding the coefficients of an arbitrary vector . Hart and Schmeidler (1989), p. 19
The inequalities must hold simultaneously for every player and every recommended-action/deviation pair. Choosing a distribution that makes one inequality hold does not ensure the others: the same weights occur in several constraints. An arbitrary product distribution can fail even in a two-player coordination game. Passing through an existing mixed Nash equilibrium proves existence, but gives no formal account of the paper's own finite minimax and nonnegative-matrix claims. The proof obligations here include the exact correspondence between the conditional recommendation constraints and an auxiliary two-person game, plus the algebra of a product of playerwise probability vectors. Hart and Schmeidler (1989), pp. 18–20
Players are a finite Lean type ; is a finite, nonempty type, and . The profile space is the dependent product . The expression is Function.update s i t, and summing over with the th coordinate fixed to is represented by summing over profiles satisfying . Probability vectors use the published AGT.IsLottery: nonnegative real weights whose finite sum is one. No measure-theoretic integral or conditional probability appears in this finite mission. The auxiliary minimizing player's pure strategies form one set of triples , with one probability vector over all triples. Hart and Schmeidler (1989), p. 19
Nonemptiness of each is required: an empty strategy set would leave no probability vector on . The player set itself may be empty; then has one profile and the incentive conditions have no instances. The generic minimax milestone separately assumes that both of its pure-strategy sets are nonempty, so solvers must handle the playerless goal directly. Equality decisions are computational instances for finite enumeration, not restrictions on mathematical games. The correlated-equilibrium definition includes normalization and all incentive inequalities; it is not defined to hold automatically. The goal is the existence of a probability vector satisfying condition (1) itself, not a restatement through AGT.nash_existence that would make it a corollary of Nash's theorem. A sorry-free local check exhibits a correlated point mass in a two-player coordination game and another point mass that violates an incentive inequality. Contributions to the finite minimax criterion, its connection to the published balance theorem, and the sum rearrangement in the product-strategy milestone are all useful beyond this one goal.
A birth-and-death process describes a population in which each individual independently gives birth and dies at given rates. Kendall's 1948 paper (doi:10.1214/aoms/1177730285) solved the process with arbitrary time-dependent rates and, in its §4, introduced a second random variable alongside the population size: the cumulative population , the number of individuals that have ever been alive up to time . Kendall gives two readings. If is the number of current cases of a disease, is the total number of cases recorded so far, and for an epidemic that is almost certain to die out, measures its overall severity. If is the viable count of a bacterial population, is the total count, in which living and dead organisms are not distinguished.
The question of this mission is the exact distribution of for the simplest transient process, with constant rates. Kendall answers it in §5 by solving a first-order partial differential equation for the joint generating function of . The resulting law involves central binomial coefficients, the same numbers that count the total progeny of a critical binary branching process.
Let and be constants. In the simple birth-and-death process with these rates, a population of size moves to at rate and to at rate . It starts from one ancestor, . The cumulative population starts at and shares all the positive jumps of , so it never decreases. The process is transient (dies out with probability one) when .
Write for the joint law of and
for its generating function (30). Kendall shows that satisfies
and solves it with the roots of the quadratic (49), :
Setting forgets , so generates the law of . Finally
The Lean names are disc, alpha, beta, psi, x, Q and SolvesPDE, in the namespace KendallBD.Cumul.
For :
The result. The law (52) gives the full distribution of the total size of a transient linear birth-and-death population, not only its moments: the probability that the ancestor dies childless, the tail behaviour, and the dichotomy between the subcritical case (finite mean , geometric-type tail with ratio ) and the critical case (heavy tail, infinite mean). In the epidemic reading this is the distribution of the final size of a minor outbreak; it is also the total-progeny law of the embedded binary Galton–Watson tree (Harris 1963).
Formalizing it. The result is classical and proved, but it is not formalized anywhere known to this mission. A formal proof would combine three separate pieces: the explicit solution of a first-order PDE by characteristics, checked as a classical solution on the region where a probability generating function lives; a limit that selects one root of a quadratic; and the binomial series of together with its boundary value at . The companions make the moments (48), which §4 derives by a separate route, a consequence of the law.
Checking that (50) satisfies (31) is calculus once the derivatives exist. The obstacles are elsewhere. First, the roots must be ordered as , which fails at when (the roots are then and ): every statement about , , has to be made for , and the law is identified from the power series on that interval. Second, the normalization is a statement at the boundary of the series for ; at this is , the edge of the disc of convergence, where convergence of the series is not automatic and where the value uses . For the same series sums to , so the hypothesis is essential. Third, the asymptotic in the balanced case needs the asymptotics of central binomial coefficients.
All objects are real functions; the process and the joint law are not constructed, exactly as in the paper. "The law of " is read, as on p. 11, as the coefficients of the generating function , and is tied to the process through the equation (31) and the boundary condition (32). The committed conventions are:
Real.sqrt the nonnegative root;SolvesPDE: both partial derivatives exist as HasDerivAt facts and satisfy the equation, never an equation between deriv values;A goal that only asserted the power series identity would be a different and easier theorem with no birth-and-death content; the goal therefore ties to of (50) and to the equation (31)–(32).
A complete development needs the binomial series for with real coefficients (Mathlib has Nat.centralBinom and general binomial series, and the platform has the generating function of the central binomial coefficients as a proof tool), the boundary behaviour of a power series with nonnegative coefficients, and Stirling-type asymptotics of . These are reusable well beyond this mission. Contributions proving any milestone or companion, or the series lemma on its own, are welcome.
Every pure integer program can be relaxed, by dropping the nonnegativity of the basic variables of an optimal linear-programming basis, to a problem over a finite Abelian group: find nonnegative integers , one for each nonzero group element, with . R. E. Gomory's 1969 paper Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2 (1969) 451–558) studies the convex hulls of the solutions of these group equations, the corner polyhedra, and the master polyhedron that contains all of them as faces. These polyhedra are the source of the group-theoretic approach to cutting planes: their faces are valid inequalities for every integer program with the same group, and their vertices are the candidate optimal solutions of the group relaxation.
The paper's first section shows that every vertex of such a polyhedron is an irreducible solution, and remarks (p. 460) that the converse fails in general: a typical group has many irreducible solutions that are not vertices. Section 3F identifies a family of groups where the two notions coincide, which is what makes the vertices of these polyhedra countable in closed form.
Let be a finite Abelian group written additively, with zero , and . For the group equation is
The master polyhedron is the convex hull in of its nonnegative integer solutions (for the solution is excluded). A vertex is an extreme point of .
A nonnegative integer vector is irreducible if any two integer vectors with and are equal. A finite set of group elements is independent if with integers forces for each .
The groups of §3F are those in which every nonzero element has order 2, the groups , or every nonzero element has order 3, the groups .
If every nonzero element of has order , with or , and , then for every nonnegative integer solution of the group equation
and the support of such a vertex is an independent set.
THEOREM 23 turns a polyhedral question into a combinatorial one for the elementary Abelian 2- and 3-groups: the vertices of are read off from independent subsets of the group and residues below . Gomory uses this on pp. 506–507 to count all vertices of all exactly and to derive their asymptotic number. It also marks the boundary of the general picture: groups with elements of other orders have irreducible solutions that are not vertices.
The result has been proved since 1969; no machine-checked proof exists. The mission produces a Lean statement and, once solved, a verified proof of the theorem together with the general fact that vertices of the master polyhedron are irreducible, a reusable layer for the other group-polyhedron results of the same paper. Two sentences of the printed proof (p. 506) are false as written (see Formalization scope); formalization records their corrected forms.
The direction "vertex irreducible" holds in every group and is a midpoint argument. The difficulty is the converse: showing that an irreducible solution cannot be written as a proper convex combination of other solutions, which are infinitely many and unbounded. The natural route, exhibiting a linear objective that uniquely minimizes, does not work with the objective printed on the page: solutions with the same support as but larger entries are tied with it. The argument must control those solutions through the arithmetic of residues modulo , and this is where the exponent 2 or 3 is used; the analogous residue statement fails for .
{g : G // g ≠ 0}; integer solutions are -valued and cast to ; vertices are Set.extremePoints ℝ of the convex hull of the cast solutions.convexHull, extremePoints_convexHull_subset), and finite sums in Abelian groups. Contributions welcome: any of the milestones, and a general lemma that a unique minimizer of a nonnegative linear function over the integer solutions is a vertex.A loss network carries calls that require capacity on one or more links. A call is accepted only when every required link has enough free circuits; otherwise it is lost. This makes the traffic on different links dependent even when calls on different routes arrive independently. Network operators need to know where capacity constraints bind and how offered traffic is converted into carried traffic. Kelly's 1991 survey develops a continuous optimization problem that identifies a characteristic flow vector and gives a linkwise description of blocking in this setting. Kelly, Loss networks (1991), §§1.2 and 2.1.
The paper begins with the equilibrium distribution of the discrete network and uses a continuous relaxation when analyzing its likely state. The resulting primal problem is useful beyond the original probability calculation because it links route flows, capacity constraints, and a convex dual. Theorem 2.8 collects the existence, uniqueness, and correspondence statements for these descriptions. This mission targets that theorem and the intermediate claims Kelly states in §2.1. Kelly (1991), pp. 327–329.
There are finitely many links and finitely many routes . Link has circuits, and one call on route uses circuits there, with a nonnegative integer. Calls request route at positive offered rate . The matrix need not be a zero–one incidence matrix: one call may use more than one circuit on a link. Kelly's fixed-routing model and its general integer matrix are described in §1.2. Kelly (1991), p. 321.
A real route-flow vector is primal feasible if for every route and for every link. The objective is
with at . The primal optimum maximizes over precisely this feasible set. This is the continuous problem (2.1), rather than an optimization over the integer-valued network state. Kelly (1991), p. 327, (2.1).
A nonnegative vector assigns one multiplier to each link. The dual objective is
A blocking vector has . Its carried route flow is . The conditions on say that the total carried flow through link equals when , and is at most when . The multiplier and blocking coordinates are related by , equivalently . These are equations (2.3), (2.6), and (2.7). Kelly (1991), p. 328.
The goal first asserts that the primal problem has exactly one optimizer. Every blocking solution must describe that same optimizer:
It also asserts that a blocking solution exists, and that it is unique if has rank , the number of links. Finally, the transformations and give a bijection between all blocking solutions and all dual optima. The formal goal includes both directions and both inverse identities, even when the dual optimizer is not unique. Kelly (1991), p. 329, Theorem 2.8.
The milestone list follows Kelly's stated progression: unique primal attainment; the Lagrangian maximum and the dual value in (2.2); feasibility and complementary slackness in (2.4)–(2.5); the substitution (2.6); dual attainment; both directions of the blocking–dual correspondence; and strict convexity plus uniqueness under full row rank. One direction of the correspondence is an existing, proved platform theorem, KellyStochasticNetworks.dual_optimum_conditions; it is referenced directly. The other direction remains a new target. Kelly (1991), pp. 327–329.
The theorem makes the carried flow uniquely determined even when several blocking vectors or dual optimizers describe it. Under full row rank, it also identifies a unique linkwise blocking vector. Its correspondence lets a statement in the flow language be translated to a statement in the multiplier language without selecting a preferred optimizer. The interpretation following Theorem 2.8 explains the linkwise condition: positive blocking occurs only on a saturated link. Kelly (1991), p. 329, discussion after Theorem 2.8.
The mathematical result was proved in the source paper. The work here is to obtain machine-checked proofs of its exact finite-dimensional statements. The published Kelly–Yudovina definition KellyStochasticNetworks.dualObjective already represents the dual formula, and its proved optimum-conditions theorem supplies one direction of the correspondence. The remaining development would give reusable facts about separable entropy objectives, nonnegative linear capacity constraints, complementary slackness, and exponential coordinate changes. Those facts can support later loss-network formalizations without changing this mission's target.
The boundary requires care: the objective has a continuous value there, but its logarithmic derivative does not. Thus a calculation that differentiates the objective throughout the closed nonnegative cone does not justify the printed differentiability sentence on p. 327. Dual existence is another boundary issue. A nonnegative capacity permits , while the paper's stated growth of the dual objective in every nonnegative coordinate can fail at that input. Any formal argument for the complete theorem must cover these domains accurately. Full row rank controls uniqueness of the dual coordinates; without it, the paper explicitly allows nonunique blocking solutions. Kelly (1991), pp. 327–329.
Lean represents links by Fin J, routes by Fin R, and by natural numbers, and , , , and by real numbers. The primal feasible set includes both coordinatewise nonnegativity and every link-capacity inequality. The dual optimum is minimal over the nonnegative orthant, using the published dual objective. The finite sums and products have their usual empty-index values; no hidden nonemptiness assumption is imposed. Matrix rank is taken over the reals and compared with , so the rank condition is full row rank.
The goal assumes and for every route and link. Positive rates give the logarithm in the primal objective its intended meaning. Positive capacities exclude a degeneracy in the dual-attainment and blocking parts of the theorem. The value at is the continuous extension ; no differentiability assertion at that boundary is part of the formal target. Blocking values belong to , so the inverse logarithm is evaluated on a positive number. A flow optimum always ranges over the exact primal feasible set, and a blocking solution always ranges over the full conditions (2.7); neither can be replaced by an arbitrary vector with a convenient equation.
A complete proof may require finite-dimensional convex analysis, strict concavity of the entropy term, attainment on a closed feasible set, the dual first-order condition, and facts about exponentials, logarithms, products, and matrix rank. The definitions and theorems are kept separate so work on these pieces can be reused. Contributions proving either a milestone or a reusable supporting lemma are in scope.
A loss network is a model of a circuit-switched network: telephone networks, and more generally any system in which a request seizes several resources at once and is lost if any of them is unavailable. Exact loss probabilities in such networks are given by a product-form distribution over a state space whose size grows exponentially with the number of routes, so practitioners compute an approximation instead: the Erlang fixed point, also called the reduced-load approximation. It pretends that links block independently, computes the traffic offered to each link after thinning by the other links, and applies Erlang's single-link formula link by link. Reduced-load approximations of this kind recur throughout §§3–4 of Kelly 1991, where they appear as limits of networks with fixed and with alternative routing.
An approximation defined by a fixed point equation raises an immediate question: does the equation have exactly one solution? Under fixed routing it does, and Kelly's Theorem 3.7 (Ann. Appl. Probab. 1991, p. 338, citing Kelly 1986, reference [33] of the paper) proves it by identifying the fixed point with the optimum of a strictly convex program, the revised dual problem. The convex characterization is specific to fixed routing; the paper notes (p. 337) that for networks with dynamic routing and control nonuniquely determined behaviour can occur.
There are links, link having circuits, and a finite set of routes . A call on route uses circuits of link , and calls on route arrive as a Poisson stream of rate .
Erlang's formula (1.1) gives the blocking probability of a single link with circuits offered Poisson traffic of intensity :
The Erlang fixed point equations (3.1)–(3.2) for the vector of link blocking probabilities are
The utilization function is defined by the implicit relation (3.4),
the mean number of busy circuits on a single link whose blocking probability is .
The revised dual problem (3.5) is
and its stationarity conditions (3.6) are
The revised dual differs from the dual problem (2.3) of §2, whose optimum gives the limiting blocking probabilities of a large network, only in its last term: becomes .
The revised dual problem (3.5) has an optimum , every optimum equals , and
The goal states the characterization, not only the existence and uniqueness of the fixed point: the solution is for the optimum of (3.5).
The theorem turns a nonlinear system of equations into a smooth strictly convex minimization over the nonnegative orthant. Uniqueness of the fixed point follows at once, and the program gives a computational handle: any convex-minimization method computes the Erlang fixed point, without relying on the convergence of repeated substitution. The comparison with the dual problem (2.3) also explains the approximation: (3.6) relaxes the conditions (2.7), which force a link's carried traffic to equal its capacity before it can block, into a smooth relation in which blocking grows with carried traffic as Erlang's formula prescribes (Remark 3.8).
On Prove2Me, existence and uniqueness of the fixed point alone is already the Proved theorem KellyStochasticNetworks.erlang_fixed_point_unique (Kelly–Yudovina, Stochastic Networks, Theorem 3.20), referenced by this mission. Also referenced: KellyStochasticNetworks.erlang_strictMono (Proved: and are strictly increasing for ) and KellyStochasticNetworks.erlang_mean_busy_circuits (Proved: the mean number of busy circuits is , the reading of as a utilization). What this mission adds is the revised dual problem itself, the utilization function , and the identification of the fixed point with the optimum of (3.5); none of these is formalized on the platform.
The function is defined only implicitly, through the inverse of , so every property of the objective of (3.5) passes through properties of Erlang's formula: monotonicity, continuity, and the limit as . Differentiating needs continuity of , which must be derived from the inverse.
The paper's sentence "strictly convex: it thus has a unique minimum" covers only uniqueness. Existence of a minimizer on the unbounded set is a separate fact, a growth estimate for the integral terms, and it is part of milestone 4. The first term of (3.5) is not strictly convex when has rank less than , so strict convexity must come from the separable integral terms. Finally, optimality over yields only one-sided conditions at coordinates with ; that (3.6) is an equality there uses .
Lean namespace KellyLossNetworks.RevisedDual. Links are Fin J, routes Fin R, the incidence matrix is A : Fin J → Fin R → ℕ, rates ν : Fin R → ℝ, capacities C : Fin J → ℕ, following the published Kelly–Yudovina definitions. Every statement assumes and ; the paper uses both without stating them, and a link with makes (3.4) meaningless, since .
Erlang's formula is the published KellyStochasticNetworks.erlang and the fixed point equations (3.1)–(3.2) are the published KellyStochasticNetworks.ErlangFixedPoint, whose factor is Lean's total inverse; milestone 6 shows that no solution in reaches . Solutions are sought in , as on p. 338.
is defined by choice: for a with , and if none exists. For , the is unique, and that (3.4) holds is milestone 1, a theorem, not an axiom built into the definition. Values at or are placeholders that no statement uses. The integral in (3.5) is the interval integral . An optimum of (3.5) is a whose objective value is at most that of every .
A trivializing formalization is ruled out: replacing by any closed form other than the one fixed by (3.4) (for instance , the fluid utilization of Remark 3.8) would change the problem and reduce (3.5) to the dual (2.3); and the goal asserts the identification rather than restating the existence and uniqueness that is already Proved.
A complete development needs: inverse-function arguments for a strictly increasing continuous map of , derivatives of interval integrals with continuous integrands, strict convexity of separable sums, and first-order optimality conditions for convex functions on the nonnegative orthant. The facts about Erlang's formula and about are reusable in any reduced-load analysis. Proofs of individual milestones are welcome independently.