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?
Prediction with expert advice asks a learner to predict a binary label on each of a sequence of trials, after seeing the predictions of a pool of candidate functions, and to make few more mistakes than the best member of the pool. Littlestone and Warmuth's The Weighted Majority Algorithm (Inform. and Comput. 108, 1994) gave the deterministic algorithm WM and its randomized variant WMR, and proved worst-case bounds that hold for every sequence of trials, with no probabilistic assumption on the data. Their §8 asks how good such bounds can possibly be when the data contain anomalies: disagreements with a candidate function, counted relative to the best-fitting member of the pool. Such disagreements can arise from noise in the instances or labels, or from instances that do not determine the label.
For the randomized algorithm WMR the expected number of mistakes grows, by Corollary 6.1 of the paper, at rate per anomaly, which tends to as . Theorem 8.2 shows that no randomized learner, however it is built, can do better than rate : an adversary who fixes the sequence in advance can force half the noise-free optimum plus one expected mistake per anomaly. Together with the deterministic counterpart, Theorem 8.1 (rate ), it locates the cost of label noise in online learning exactly. Mistake-bound lower bounds of this kind are a standard reference point for the analysis of online classification and of the expert-advice algorithms descended from WM (Cesa-Bianchi and Lugosi, Prediction, Learning, and Games, 2006).
Timeline: Littlestone (1988) characterized the optimal noise-free mistake bound by complete mistake trees (the Littlestone dimension); Littlestone and Warmuth (FOCS 1989; journal version 1994) introduced WM and WMR and proved Theorems 8.1 and 8.2.
Let be an arbitrary domain and a pool of functions , finite or infinite. A trial is a pair with and ; a sequence of trials is a finite list , in which an instance may repeat with different labels. The number of anomalies of with respect to is , and is the collection of sequences for which some has at most anomalies.
A deterministic algorithm maps the past trials and the current instance to a predicted label; counts its wrong predictions, and
A randomized algorithm uses random choices independent of the sequence. On a fixed sequence its behaviour at trial is summarized by , the probability that it predicts given the preceding instances and labels and the current instance; its expected number of mistakes is , and
the infimum ranging over all maps from (past trials, current instance) to .
For every pool with and every integer ,
Both sides live in ; when the statement says .
"For any pool of functions there exists a complete -mistake tree" ([Lit88]). On the platform this is the proved Lemma 21.7 of Shalev-Shwartz and Ben-David, , together with Lemma 21.6, for every ; a tree shattered by is a complete mistake tree.
The theorem shows that the expected-mistake bound of WMR is optimal in its dependence on the number of anomalies: its coefficient of approaches , and no randomized learner achieves a smaller one on every pool with two or more functions. It also quantifies the advantage of randomization: the deterministic rate is (Theorem 8.1), the randomized rate is , and the noise-free term halves. The lower bound is obliviously adversarial, since the sequence is chosen before any coin is tossed, so it applies equally to the stronger model in which the adversary adapts to the learner's predictions.
The result has been proved since 1994. To our knowledge it has no machine-checked proof; the platform holds the Littlestone-dimension characterization of the noise-free optimum (Shalev-Shwartz and Ben-David, Chapter 21) but no statement about anomalies or randomized lower bounds. This mission formalizes the definitions of anomalies, and , and the theorem.
An adversary against a randomized learner cannot react to its predictions: the whole sequence, instances and labels, must be fixed in advance, so the adaptive adversary that proves the deterministic bound is not directly available. The lower bound must instead come from the learner's prediction probabilities, which depend only on the sequence prefix; the content of the theorem is that this information is enough to construct, for every learner, one fixed sequence that stays inside while forcing the stated expected count. Taking the infimum over learners inside an extended-real supremum over sequences of every length adds bookkeeping when is infinite.
Sequences are Fin T → X × Bool for every T : ℕ. Deterministic algorithms, the mistake count, shattered trees and the Littlestone dimension are reused from the published definition UnderstandingML_Online (OnlineAlg, mistakes, ShattersTree, ldim, soa); randomized algorithms are its OnlineAlgR X := List (X × Bool) → X → ℝ restricted by IsRandAlg to values in , and the expected mistake count is its cumLoss. is a natural number. takes values in ℕ∞ and in ℝ≥0∞; the paper's "minimum" is read as an infimum. is F.Nontrivial, which admits infinite pools.
The reduction of randomized algorithms to probability maps is the main modelling choice: on a fixed sequence the expected number of mistakes of any algorithm whose randomization is independent of the sequence equals , and every map with values in is realized by such an algorithm, so the two infima coincide. Dropping the constraint , or quantifying only over deterministic algorithms, gives a different quantity and is ruled out.
Needed: the definitions above, and the existence of a complete -mistake tree, available through the proved platform theorems on ldim and soa. Lemmas relating mistakes along a path of a shattered tree to ldim, and a reusable statement that an oblivious adversary can force expected loss per trial, would serve other lower bounds in the Littlestone–Warmuth series and in online learning generally. Contributions of such lemmas are welcome.
Many security-relevant inputs are noisy and do not repeat exactly: fingerprint minutiae, iris codes, lists of personal preferences, the set of features extracted from a document. A cryptographic key derived from such an input must be reproducible from a later, slightly different reading, without storing the input itself. Dodis, Ostrovsky, Reyzin and Smith (SIAM J. Comput. 38(1), 2008; arXiv:cs/0602007) introduced secure sketches for this purpose: public helper data that lets the holder of a nearby reading recover the original exactly, while revealing as little as possible about it.
When the input is a set of features, the natural distance is the size of the symmetric difference. Juels and Sudan proposed the fuzzy vault for this setting (Des. Codes Cryptogr. 38, 2006). Section 6.2 of Dodis et al. gives a simpler, deterministic variant, the improved Juels–Sudan sketch (Construction 5), whose storage and entropy loss are both for -element subsets of an -element universe, independent of . The paper's Theorem 6.1 is the analysis of that construction. This mission formalizes it.
Laws and average min-entropy. A random variable is identified with its law. For a pair ,
which equals , the average min-entropy of §2.4: the negative logarithm of the best probability of guessing after seeing .
Secure sketches. Let be a set with an integer-valued distance . A pair of procedures is an average-case -secure sketch (Definitions 3 and 4) if
The difference is the entropy loss.
The metric. For a finite universe with , is the set of -element subsets of with .
Construction 5. Identify with a finite field of elements and let .
The Lean development names these charPoly, sketchCoeffs, sketch, pHigh, Step3Cond and recover, and the metric SDifS with distance sdifDist, in the namespace FuzzyExtractors.ImprovedJS.
For every finite field with elements, all and every real ,
The goal is uniform in : the entropy loss does not depend on the input distribution.
The paper's argument on p. 21 splits into four steps, each a milestone:
A fifth, off the goal's path, records Step 2's remark that the sketch consists of the first elementary symmetric polynomials of , up to sign.
The security half is the entropy bound: since takes at most values, (the paper cites its Lemma 3.1, which is posed in the first mission of this series and is not restated here).
The result. Theorem 6.1 gives a secure sketch for set difference whose sketch length and entropy loss are , which the paper shows is essentially optimal when (§6.2, via Lemma C.1 and a constant-weight code bound). It improves the original fuzzy vault, whose entropy loss the paper analyses in Appendix D and finds good only when the stored data is very large. Through the paper's generic composition with randomness extractors (Lemma 4.1), it yields fuzzy extractors for set-valued inputs in large universes, the regime of biometric feature sets.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists on Prove2Me or, to our knowledge, elsewhere. A formal proof combines three pieces of reusable infrastructure: a probabilistic layer (average min-entropy of laws on arbitrary types, and the chain-rule-type bound for a function with few values), the combinatorics of symmetric differences of equal-size sets, and the algebra of Reed–Solomon unique decoding (a low-degree polynomial is determined by its values on enough points). Each of these is useful beyond this mission.
No step is deep; the difficulty is in the bookkeeping. The correctness argument relies on exact degree accounting: must agree with in every coefficient of degree at least , so that the remainder has degree at most , and the uniqueness count ("two candidates agree on at least points") requires the threshold to be at least ; the paper's sentence says "more than", which does not support the argument as written. The roots of must be shown to form exactly the set , with no multiplicities lost. The security half needs the average min-entropy of a joint law with a deterministic, -valued component bounded uniformly over all auxiliary variables, including those with infinite or uncountable range, where sums are infinite sums of extended nonnegative reals.
Conventions committed to in Lean:
PMFs; the procedures are kernels M → PMF S, here deterministic (PMF.pure). Average min-entropy is the joint form above, logarithms base 2, and the auxiliary ranges over an arbitrary ι : Type (a superset of the paper's ), never restricted to finite types.[Field 𝔽] [Fintype 𝔽], with = Fintype.card 𝔽; the paper's " is a prime power" is then automatic.degree < s - t, so when .A formalization that checks only correctness, drops or trivializes the entropy clause, or lets see itself, would not be Theorem 6.1. The goal states both clauses through the definition of an average-case secure sketch, with given only and the sketch.
Contributions welcome: proofs of the milestones, a general lemma bounding average min-entropy loss by the logarithm of the number of sketch values (the paper's Lemma 2.2(b) and Lemma 3.1), and Reed–Solomon uniqueness lemmas stated for reuse.
Monotone comparative statics asks when the optimal choice of an agent moves in a predictable direction as a parameter of the problem changes: does a firm hire more of every input when the output price rises, does a monopolist raise its price when its marginal cost rises? Topkis (1978) gave a cardinal answer: if the objective is supermodular in the choice and has increasing differences in , the set of maximizers is nondecreasing in . Milgrom and Shannon (1994) replaced these conditions by ordinal ones, quasisupermodularity and the single crossing property, and showed in their Monotonicity Theorem that the ordinal conditions are both necessary and sufficient for the argmax to be monotone in the parameter and the constraint set.
Supermodularity is therefore never necessary for monotone comparative statics. Theorem 10 of Milgrom and Shannon identifies a setting where it is: when the objective must keep the ordinal properties after adding an arbitrary linear price term (or subtracting an arbitrary nonnegative cost ), the only objectives that qualify are the supermodular ones. This is the situation of a price-taking firm whose revenue or cost is linear in its activity levels, and the result explains why supermodularity is the natural assumption in such models even though the ordinal theory does not require it.
Let be a lattice: a partially ordered set in which every two elements have a least upper bound (join) and a greatest lower bound (meet). On the order is componentwise, so and are the componentwise maximum and minimum; on a product the order is the product order. For , .
A function is supermodular if for all . It is quasisupermodular if, for all , (i) implies , and (ii) implies .
Let be a partially ordered set and . The function has increasing differences in if for the difference is nondecreasing in . It has the single crossing property in if for all and , implies , and implies . The function is quasisupermodular in if is quasisupermodular for every , and nondecreasing in if is nondecreasing for every .
In the Lean development the domain is Fin n → ℝ, is curried as f : (Fin n → ℝ) → ℝ → ℝ, is p ⬝ᵥ x, and supermodularity and increasing differences are the published Supermodularity.Monotonicity.SupermodularOn and IncreasingDifferencesOn with the domain Set.univ.
Let . Then
and, if is nondecreasing in ,
Here " is supermodular" means supermodular on the lattice , jointly in .
The result. The Monotonicity Theorem shows that the ordinal conditions are exactly what monotone comparative statics needs for a single objective. Theorem 10 shows that the cardinal conditions are exactly what is needed for a family of objectives closed under linear prices. It separates two questions that are often conflated: whether a particular optimization problem has monotone solutions (ordinal), and whether a model's monotonicity conclusion is robust to the prices or costs the modeller adds to it (cardinal). The second sentence specializes to the economically common case of nonnegative input costs, where the restriction to is offset by the monotonicity of .
Formalizing it. The result is proved in the paper, with the converse direction given in detail only for the step "supermodular in " and the remaining cases left as "similar arguments". The mission produces machine-checked proofs of both equivalences, including the cases the paper does not write out: the recovery of increasing differences from the single crossing property under all price perturbations, and the recovery under the sign restriction . No part of Milgrom and Shannon's paper was found formalized on the platform when this mission was drafted; Topkis's supermodularity theory is partly available on the platform as the Supermodularity.* series.
The forward direction is a chain of short implications. The content is in the converse: from purely ordinal information about many functions one must recover a cardinal inequality. The single crossing property and quasisupermodularity only compare values of one function at two points, so a single perturbation can never yield an inequality between sums of four values; the argument must choose, for each violating configuration, a price vector that makes two of the four values tie, and the choice must be compatible with the sign constraint in the second statement. That compatibility is where the hypothesis that is nondecreasing in enters, and without it the second equivalence fails. A second subtlety is the decomposition of joint supermodularity on into supermodularity in and increasing differences in , which the paper uses without statement; the platform does not yet have it.
Fin n → ℝ with Mathlib's pointwise order and lattice operations; is arbitrary. The product carries Mathlib's product order.QuasiSupermodularOn and SingleCrossing are shared with the two sibling missions on Milgrom and Shannon's Theorems 4 and 8 and will be merged with them. A lemma decomposing supermodularity on a product lattice into supermodularity in each factor and increasing differences would be reusable well beyond this mission; contributions of such general lattice lemmas are welcome.Inventory pooling lets several locations serve their combined demand from one stock of goods. Classical newsvendor analysis predicts lower optimal cost when pooling reduces demand variation, but the reduction can vanish when demands are perfectly correlated. Xuanming Su asks whether that conclusion survives when managers make noisy stocking decisions rather than always choose the optimum. In the published 2008 article, Bounded Rationality in Newsvendor Models, the decision noise follows a continuous logit model, in which better quantities are chosen more often. Proposition 7 gives conditions under which pooling strictly lowers expected cost, including a case where classical pooling has no cost gain. Su, 2008
The question matters for multilocation inventory systems because an order quantity is a decision as well as a response to demand. Pooling changes both the distribution of demand faced by the system and the number of independently chosen orders. A comparison based only on optimal costs leaves the second change out. This mission isolates the paper's mathematical claim about the combined effect of demand and decision variation. Su, 2008, §9
There are locations. Demand at location is normally distributed with mean and standard deviation . The total demand has normal law with mean and standard deviation . An order of against a realized demand incurs holding cost for unsold units and backlog cost for unmet demand. Its expected cost is . The decentralized system incurs one such cost at each location; the pooled system orders once for total demand. The published InventoryControl_newsboy definition supplies this Gaussian expected cost, with the same orientation of holding and backlog penalties as Su's equations (29) and (31). Su, 2008, p. 584
For an expected profit function on a decision set , the logit choice density is proportional to on , where is a common bounded-rationality parameter. Larger spreads choices more widely; smaller positive concentrates them near high-profit choices. For normal demand, the decision domain is all of . With and , expected profit differs from minus expected cost by a constant independent of the order. The same logit law is therefore obtained from utility . The random behavioral order is denoted at location and for the pool. Su, 2008, pp. 571–572, 584
The goal is Proposition 7. Under positive holding and backlog costs, one common positive , at least two locations, positive individual standard deviations, and
the claim is
The first standard-deviation inequality is automatic for the sum of jointly normal demands. The second excludes a total demand whose standard deviation is smaller than an individual location's. The result still includes perfect positive correlation, where the first inequality is an equality. Su, 2008, Proposition 7, p. 585
Five milestones record the source's route to that comparison: invariance of the choice distribution under an order-preserving affine change of quantity (Lemma 1), invariance under an additive shift in utility (Lemma 2), standardization of the Gaussian newsvendor objective (equation (63)), the optimum of the canonical standard-normal newsvendor and the nonpositivity of its profit, and the comparison of its expected values at different positive scales. The milestone text preserves the wording of the printed article; the precise Lean conditions and corrections are stated with the items. Su, 2008, pp. 572, 587–588
The strict inequality separates two mechanisms of pooling. Demand aggregation can reduce variability, while a single pooled order also avoids accumulating the costs of several noisy decisions. Proposition 7 shows that the latter mechanism can make the cost reduction strict even when perfect correlation removes the usual variance benefit. It provides a condition that can be checked from individual and total standard deviations, rather than requiring an explicit covariance matrix in the final comparison. Su, 2008, pp. 584–585
The result is proved in the paper; the remaining task is a machine-checked formalization of its definitions and argument. The Gaussian expected-cost object is already published on Prove2Me, while the continuous logit law and this behavioral pooling theorem are new to this mission. The invariance statements and canonical profit comparison are reusable wherever a continuous logit rule acts on a transformed one-dimensional objective.
The usual pooling comparison evaluates cost at an optimal order. Here each system draws its order from a different continuous probability law, and the cost to compare is averaged over those choices. Comparing with alone does not compare the logit distributions; in particular, it gives equality under perfect positive correlation while the target is strict. A formal development must also show that the normalizing integrals and the resulting cost expectations are genuine finite integrals for every set of parameters covered by the theorem.
The Lean model uses Mathlib's real Gaussian law with variance and the published InventoryControl_newsboy.newsboyCost for equations (29) and (31). It records the choice density, CDF, expectation, canonical profit, and behavioral expected cost as separate definitions. The behavioral density uses on ; the utility shift from profit is covered by Lemma 2. The theorem specifies normal marginals and a normal total with mean and standard deviation . Every jointly normal demand vector in the paper yields these laws, and the final comparison uses no further feature of its joint distribution.
The conditions , , and are standing readings needed for the continuous choice law on the unbounded domain. Proposition 7 additionally states and : for one location the alleged strict comparison becomes equality, while zero variance makes the paper's continuous density on a point support undefined. Lemma 1 requires positive affine scale because a negative scale reverses CDF order, and its two invariance lemmas require a finite positive normalizer. Equation (66) is read with , as dictated by the surrounding formulas; the printed display drops the word “min.” These corrections and the cost-based choice convention are recorded item by item in the moderation notes.
No optimizer is supplied as a free variable, and no zero normalizer is allowed to turn a logit expectation into a trivial zero. Useful solver contributions include proofs that the cost-based logit normalizer and expected cost are integrable, Gaussian change-of-variables lemmas, and the strict scale comparison. These analytic facts can serve other continuous-choice models.
The queue has identical servers, a general arrival process, and independent service times with a common distribution . In the Halfin–Whitt regime the number of servers and the offered load grow together, so that the fraction of delayed customers stays strictly between and . This is the standard asymptotic model of large call centers and service systems (Halfin and Whitt, Operations Research 29, 1981, doi:10.1287/opre.29.3.567). For exponential service times the diffusion limit has been known since 1981; for general service distributions the queue length is no longer Markov, and its limit requires a different device.
Reed (Annals of Applied Probability 19, 2009, arXiv:0912.2837) supplied that device. The number in system satisfies a nonlinear convolution equation, (2.8) on p. 9 of the paper, in which the only nonlinearity is the term . Section 3 of the paper isolates that equation as a deterministic regulator map: a map that takes an input path to the unique solution of the equation. Its fluid limit (Theorem 4.1) and diffusion limit (Theorem 5.1) are both obtained by applying this map, through the continuous mapping theorem, to the limits of simpler free processes. The regulator map plays here the role that the one-sided reflection map plays in conventional heavy-traffic theory.
Timeline:
A path is a function . It is càdlàg if it is right continuous everywhere and has a finite left limit at every . is the set of càdlàg paths. For the supremum metric on is .
Let be a cumulative distribution function on , that is, for a probability measure , and let . Write . For an input , the regulator equation (3.1) asks for a path with
The integral runs over the closed interval , so an atom of at counts. The regulator map sends to the solution . The paper applies it with , the service-time distribution: for the fluid-scaled queue and for the diffusion-scaled one.
The proof works with the operator and the successive approximations , of (A.3).
carries the Kolmogorov σ-algebra, the one generated by the evaluations , . In the Lean development the objects are IsCadlag, supNorm, Dpath, SolvesRegulator, psi and picard.
Assume . Then there is a map with the following properties:
The constant is not fixed. The proof gives , but the goal asserts only its existence.
Proposition 3.1 is the deterministic core of the paper. Uniqueness makes the queue length a well-defined function of its free process. Lipschitz continuity in the topology of uniform convergence on compacts carries convergence of the inputs over to convergence of the outputs. Measurability is needed because the inputs are random: it makes the output a random element of , so that the continuous mapping theorem applies. Without the proposition neither Theorem 4.1 nor Theorem 5.1 can be stated in the form the paper gives. Example 1 and Corollary 5.1 are the two explicit solutions the paper extracts from it: a periodic, discontinuous sawtooth, and a constant.
The proposition is proved in the paper's Appendix (pp. 32–36). As far as the platform's records show, none of it has been formalized. The mission produces a machine-checked version with every convention fixed. It also corrects the statement: as printed, the proposition fails when is the unit mass at , because the equation then reads . With and this has no solution. The goal therefore carries the hypothesis . That hypothesis holds for every service distribution of mean on , which is the only case the paper uses. It also covers the mixed cases that fall between the two cases of the printed proof, such as an atom at together with mass elsewhere.
Theorems 4.1 and 5.1 themselves, which are weak convergence in with the Skorohod topology, are not part of this mission.
The equation is a Volterra equation with a nonlinear but -Lipschitz integrand. The first idea is to treat it as a contraction in . That fails: the kernel has total mass , so on the operator is only nonexpansive, not contractive. The contraction has to be recovered locally, from windows of length on which puts mass less than . This works only if such windows exist, and they do not exist when is a point mass at .
Atoms are the second difficulty. With atoms, is càdlàg but not continuous, and the closed-interval convention matters at every step. The third is measurability. The map is not continuous in for the Skorohod topology when has atoms, so the paper splits into its continuous and discrete parts.
ℝ → ℝ, and only its values on are constrained or read. Every equation is asserted for , and every uniqueness claim is equality on (Set.EqOn … (Set.Ici 0)). is the structure Dpath of càdlàg paths.Set.Icc 0 t, so it includes an atom at , and mass on never enters.Infrastructure. A complete development needs the following, all reusable beyond this mission:
The related platform objects are of other shapes:
ChenWhitt93.Reflection.Basic (IsCadlagOn, vector-valued paths on ) and EthierKurtz_HasCadlagPaths (processes indexed by ) define càdlàg paths in other settings.BellmanDP.Inventory.renewal_equation_exists_unique is a linear renewal equation with a density kernel of mass below .Contributions are welcome on any milestone, in any order. The windowed estimates (milestones 2–4) and the measurability step (milestone 5) are independent of each other.
Many linear programs that arise in combinatorial optimization ask only whether a convex set contains a point satisfying a family of nonnegative linear constraints. In the fractional covering problem the constraints have the form with : the fractional relaxation of set cover, the Held–Karp lower bound for the travelling salesman problem, and the cutting-stock relaxation all have this shape. General-purpose LP methods solve such problems exactly but slowly. Plotkin, Shmoys and Tardos showed that when a fast subroutine can optimize a linear function over the convex set, a Lagrangean-relaxation scheme with an exponential potential finds an approximate solution with a number of subroutine calls that depends on a width parameter and on the accuracy, not on the dimension of the set (Plotkin, Shmoys, Tardos, Cornell ORIE TR 999, 1992; journal version Math. Oper. Res. 20(2), 1995).
The covering half of that paper (§3) is the object of this mission. It is the template for later covering and mixed packing–covering solvers, including those of Garg and Könemann (SIAM J. Comput. 2007) and Young (FOCS 2001).
Fix integers , . Let be a real matrix with nonnegative entries and rows , write , let with , and let be a nonempty convex set contained in the nonnegative orthant.
The Lean names match: rowVal, lam, WidthBound, IsMaxOracle, C1, C2, dualY, potential, improveCover, initCover, coverAlgorithm, in the namespace FracPackCover.Covering.
For every instance as above, every width bound , every exact maximization oracle and every , the covering algorithm stops after at most
calls to subroutine (7), and either returns with , or reports that no has , correctly. This is the paper's with the constants of its proof.
In the order the proof uses them:
Theorem 3.7 says that approximate fractional covering is no harder, in subroutine calls, than about linear optimizations over , plus lower-order terms in . In §6 of the paper this yields fast approximation algorithms for covering-type relaxations such as the Held–Karp bound and the bin-packing and cutting-stock relaxations, where is a product of simple sets and the subroutine is a minimum-spanning-tree or knapsack computation. The result also certifies infeasibility: when the algorithm reports that no exact solution exists, the dual vector at hand proves it.
The result has been proved since 1991 and has been reproved in several later frameworks. As far as is known, it has not been machine-checked. A formal development contributes the explicit constants and a precise statement of the driver, which the paper gives only in prose. It also provides a reusable Lean account of exponential-potential methods with an optimization oracle.
The obvious argument tracks the potential and stops when it is small. This does not work directly, because is tied to , and the guarantee depends on staying close to throughout. Lemma 3.4 controls that, and it is a statement about the reachable states of a while loop, not about an arbitrary point. Two further points are delicate. Unlike packing, condition is not scaled by , so and give -optimality only when is near ; the first phase must first raise from by repeated doubling. And the cost of -scaling is bounded only because each phase starts from a -optimal point, which requires carrying Lemma 3.1 across phase boundaries. The bookkeeping that turns per-call bounds into a single explicit , over a fuel-bounded run, is substantial.
Rows are Fin m with [NeZero m], coordinates Fin n; is a Matrix (Fin m) (Fin n) ℝ; is a Set (Fin n → ℝ), convex, nonempty and in the nonnegative orthant. is a Finset.inf' over the rows. Conventions committed to:
some (result, oracle calls) when they stop within the fuel. Each while-test that reaches the check costs one oracle call; the loop body reuses that answer. The goal asserts that the run with fuel stops; it does not assume termination.initCover, firstPhase and scalingPhases with .A trivializing formalization is ruled out: the goal requires the run to return an outcome within the stated number of oracle calls, for every exact oracle and every width bound, and each outcome must be correct.
A complete development needs elementary real analysis (the second-order bound for ), geometric-decay counting arguments, and induction over fuel-bounded loops. The potential-decrease and termination lemmas are reusable for the packing and general missions of the same paper. Proofs of any milestone, and alternative arguments with better constants, are welcome.
Lagrangian duality turns a constrained minimization problem into the maximization of a dual function over multipliers. For convex programs the duality is clean: under mild conditions the dual optimal value equals the primal one, and an optimal multiplier vector exists. Computationally, however, the ordinary Lagrangian has a well-known defect. Knowing an optimal does not tell where the primal optimum is, because the minimizers of over typically include points that are not optimal and not even feasible. A linear program is the extreme case: is then often constant.
The penalty Lagrangian (also called the augmented Lagrangian) of Hestenes, Powell and Rockafellar repairs this defect. R. T. Rockafellar's 1973 paper Math. Programming 5, 354–373 develops its duality theory for convex programs in an arbitrary real vector space. This mission formalizes the "exactness" part of that theory, §3 of the paper: for , minimizing the penalty Lagrangian at an optimal multiplier gives exactly the optimal solutions of the original problem. The paper puts it as "a strong property whose well-known absence for has been a serious impediment to computational approaches based on duality" (p. 362). Together with the smoothness of the dual function (Theorem 3.2, another mission of this series), this property is what justifies the method of multipliers as an algorithm for constrained optimization.
Timeline. Hestenes (1969) and Powell (1969) proposed the multiplier method for equality constraints. Rockafellar (1973, this paper) gave the inequality-constrained penalty Lagrangian below and its convex duality theory. Bertsekas's monograph Constrained Optimization and Lagrange Multiplier Methods (1982) systematized the theory.
Let be a real vector space, a nonempty convex set, and convex functions. The problem is
A point is feasible if it lies in and satisfies the constraints. The optimal value "inf in (P)" is the infimum of over the feasible points, an element of . An optimal solution is a feasible with for every feasible .
For (no sign restriction), and , the penalty Lagrangian is
The ordinary Lagrangian is for , and otherwise. The dual objectives are and . Problem maximizes over .
In Lean these are Lr, L0, gr, g0, primalValue, dualValue, IsNormal, IsDualOptimal, IsKTVector, IsSaddle, IsOptimal and KuhnTuckerConditions, in the namespace PenaltyLag.Exact.
Assume (P) is normal, is a dual optimal solution, and . Then for every
The result. Theorem 3.5 turns a constrained problem into an unconstrained one with no loss of exactness. Once an optimal multiplier is known, every minimizer of over solves (P), and conversely. Section 4 of the paper builds the computational scheme on this: maximize the smooth concave function over , then minimize over . For the ordinary Lagrangian the corresponding statement is false (p. 363), so the theorem marks precisely what the quadratic penalty term adds. Corollary 3.4 records the other half of the picture: in Kuhn–Tucker vectors and saddle points, behaves exactly like .
Formalizing it. All results are proved in the paper, partly by citation of Rockafellar's Convex Analysis (§§28–30, 36). On the Prove2Me platform, saddle-point characterizations exist only for the ordinary Lagrangian on (for instance ConvexOptimization.lagrangian_saddle_iff_strong_duality, and Beck's Theorem 2.7 as FirstOrderOpt.ConvexTheory.saddle_point_sufficient / saddle_point_necessary). This mission adds the penalty Lagrangian, convex sets in an arbitrary real vector space, extended-real dual values, and the exactness theorem itself. None of these statements is known to us to be machine-checked elsewhere.
The "if" direction is the substantive one. A minimizer of is not known to be feasible; feasibility must come from maximality of in the dual. The natural argument for breaks at exactly this point: is affine on the orthant, and minimality in gives no information about . For the link is the differentiability of the dual function with (Theorem 3.2), which is posed in another mission of this series and is not available as a platform result. Every statement involves extended-real dual values on a vector space with no topology, so must be handled at each step.
AddCommGroup E, Module ℝ E), as in the paper; no norm or topology is used.Set E. Each statement assumes the paper's standing hypothesis (p. 358): convex and nonempty, convex on .E → ℝ, and only their values on enter. Constraint indices are Fin m (0-based), with a separate argument.EuclideanSpace ℝ (Fin m).EReal-valued. An infeasible (P) has value , and off .Lr at is not .The solver needs the representation , weak duality, the envelope formula and differentiability of (Theorem 3.2), and a convex-duality fact for normal programs. Those parts are reusable beyond this mission, and proofs of the paper's Theorem 3.2 in this setting are welcome as auxiliary results.
A pseudorandom number generator replaces repeated random sampling with a deterministic update of a small state. Its useful lifetime depends on the length and structure of the resulting orbit. In Marsaglia and Zaman’s 1991 paper, the subtract-with-borrow generators use only digit subtraction and a one-bit borrow while attaining cycles that can be almost as long as the whole set of digit tuples. The mathematical question is exact: which fraction encodes an output sequence, when does an arbitrary seed enter a cycle, and how long is that cycle?
This mission concerns the paper’s first subtract-with-borrow rule, called Method 1 in §4.5. The paper also studies a second rule that reverses the order of the two subtracted digits. Its modulus and period analysis differ. The distinction matters because the same state format supports both rules while their arithmetic claims are different.
Choose an integer base and lags . A state is a row of digits and one borrow bit, , where each is in and . The leftmost digit is the oldest. One update discards it, shifts the remaining digits left, and appends a new digit. Put . If , the appended digit is and the new borrow is zero. If , the appended digit is and the new borrow is one. Write this deterministic map as .
The digits emitted after the seed obey modulo , with updated at each step. The associated modulus is . For , write for the th digit after the point in the base- expansion of , with . The digit stream is read in reverse order when it is matched to an expansion: the latest generated digit in a finite block is the first fractional digit. A state is strictly periodic when it is already on a cycle under ; otherwise it may pass through a transient before reaching one.
Two states have period one: and . These are the trivial seeds. They are exceptions to the order-of-base period formula. A third useful object is the multiplicative order , the least positive for which . Since , the base is coprime to this modulus.
For prime and any nontrivial seed , the goal identifies the minimal state period after the transient:
The assertion includes both that is on a cycle and that its period is exactly the order. It makes no primitive-root assumption. If is a primitive root modulo , the right side specializes to , the full period discussed in §3 of the paper.
The milestones state that the fractional digits of have least period when and are coprime to ; that a primitive root yields digit period ; that the two trivial seeds are precisely the fixed points; and that every seed reaches a cycle after at most updates. They also formalize the reverse-digit relation for every finite generated block and the paper’s Method 1 inequalities that classify nontrivial seeds already on a cycle. These targets use the paper’s own claims in §§4.1, 4.3, and 4.5 rather than an arbitrary decomposition of the goal.
The result converts the orbit-length problem of a digit-and-borrow machine into a multiplicative-order calculation in a finite residue ring. A prime modulus and a primitive base produce a nontrivial cycle of length ; a nonprimitive base still has the exact order-of-base period. The seed classification separates states already on that cycle from states with an initial transient. These statements are what allow a proposed numerical parameter set to be assessed mathematically before the generator is used.
Marsaglia and Zaman proved these results in the cited paper. This mission asks for machine-checked Lean proofs of the statements, starting from an explicit finite-state update. The reusable output includes exact base- digit arithmetic, links between digit periods and multiplicative order, and methods for reasoning about the eventual cycles of finite-state digit generators. The present proposal consists of compiled statements and definitions; the theorem bodies are open proof targets.
Finiteness alone shows that every state eventually repeats, but it gives neither the bound of steps nor the exact cycle length. Likewise, observing that a generated digit block matches a prefix of some fraction does not by itself identify one period for the whole state orbit. The proof must keep track of the borrow bit and the direction in which the digit block is read. It must also show that a nontrivial seed does not collapse to one of the two fixed states. The source’s integer tableaux explain the arithmetic link, but turning their finite strings into a statement uniform over every seed and every block length is the main formalization challenge.
Lean represents digits by Fin b, the borrow by Fin 2, and the row by a function on Fin r. Lean index zero is , so the digit used in the update, , has index . The update branches on an ordinary integer comparison before any natural-number subtraction can truncate a negative value. The modulus is a natural number, and with makes an exact subtraction. The th fractional digit is computed by an exact quotient and remainder; only has the mathematical meaning used in the theorems. The generated stream is one-based, and the first digit beyond the seed is .
The paper’s “after a few iterations” is pinned to its stated upper bound “at most .” Its “period” is the minimal positive state period of , not a mere period divisor or the period of an arbitrarily selected digit window. “Appropriately chosen” parameters mean a prime for the goal and exclusion of the two named fixed seeds. The reverse-digit milestone permits the numerator to depend on the finite endpoint, as the tableau argument does. No seed is excluded from the at-most- milestone.
The discussion on pp. 473–474 prints the Method 1 seed inequalities in the opposite direction from the Method 1 listing on p. 472. The Lean seed-classification milestone uses the p. 472 directions, which agree with the step map on p. 466 and with direct finite checks. The §5 claim that every five-tuple except the patterns appears once in the special full cycle is left for a later extension. The other subtraction order, its modulus , and the paper’s large parameter certificates are outside this mission.
An encoding that merely asserts the existence of some period, allows an impossible seed hypothesis, or replaces the update by a different subtraction order would make the goal vacuous or change the result. The intended development needs Mathlib’s ZMod, multiplicative order, finite iterations, periodic points, and natural-number quotient and remainder. Contributions proving the numbered milestones, strengthening their arithmetic interfaces, or closing the goal are in scope.
Many algorithms for graphs and finite metric spaces begin by placing the points in a geometric space and then working with the geometry. Euclidean space is the most convenient target: distances there are controlled by inner products, so the question "where should the points go?" becomes a question about matrices. Linial, London and Rabinovich (Combinatorica 15 (1995)) made this viewpoint systematic and drew algorithmic consequences from it, among them the approximate multicommodity max-flow/min-cut theorem treated in a companion mission.
A finite metric space rarely embeds in Euclidean space without changing some distances. The natural measure of the damage is the distortion, and the least distortion of a space is a basic invariant in metric geometry and in the analysis of approximation algorithms. Section 3.1 of the paper (pp. 221–225) shows that is the value of a semidefinite program, so that it can be approximated in polynomial time, and Corollary 3.5 turns the dual of that program into a complete list of certificates that bound from below.
Timeline. The isometric case () is classical: Schoenberg (1935) and Young–Householder (1938) characterised the finite metric spaces that embed isometrically in Euclidean space by positive semidefiniteness of an associated matrix; the paper cites this as its Remark 3.7. Bourgain (1985) proved that every -point metric space embeds in Euclidean space with distortion . Linial, London and Rabinovich (1995) gave the semidefinite characterisation of for every (Corollary 3.5) and showed that the bound is tight for constant-degree expanders.
Let be a finite set of points and a semi-metric: , , is symmetric and satisfies the triangle inequality. Distinct points may be at distance zero, as the paper allows. Write .
For , the space embeds in a Euclidean space with distortion at most if there are and with
where is the Euclidean norm (Definition 2.1, p. 218). The Lean predicate is EmbedsEuclidean d c.
is the cone of real symmetric positive semidefinite matrices indexed by . For a matrix , the condition says that every row of sums to zero. The trace pairing of two matrices is .
For a finite semi-metric space and , embeds in a Euclidean space with distortion at most if and only if for every with
The sums run over ordered pairs. The statement is exact: distortion at most is attained, not approached.
The result. Corollary 3.5 makes the least Euclidean distortion a dual object: every positive semidefinite with zero row sums is a certificate that , and the corollary says that the best such certificate is exact. Lower bounds on distortion in later work, for expanders, hypercubes and other families, are proved by exhibiting such a , often a graph Laplacian. The same duality is the basis of the semidefinite relaxations used for sparsest cut and related problems.
Formalizing it. The result is proved in the literature, but nothing of it is machine-checked. A formal development produces three reusable pieces: the Gram-matrix description of Euclidean point configurations up to distortion, self-duality of the positive semidefinite cone under the trace pairing (not in Mathlib), and a theorem of alternatives for a specific semidefinite feasibility problem, where no constraint qualification can be assumed for free.
The direction from an embedding to the inequalities is short. The difficulty is the converse. "By convex programming duality" is not automatic for semidefinite systems: theorems of alternatives for cone programs can fail when the image of the cone under the relevant linear map is not closed, so the step that turns "no feasible " into an explicit certificate needs an argument specific to this system. A second subtlety is that the left side asks for an embedding with distortion exactly at most ; a separation argument that only produces embeddings with distortion for every does not prove the statement.
X (Fintype, DecidableEq); is not otherwise used. The semi-metric is a function d : X → X → ℝ with the axioms bundled in IsPseudometric.EuclideanSpace ℝ (Fin m) with m existentially quantified. Distortion is the contractive form of Definition 2.1 with both inequalities; with only one of them the zero map or a large scaling would make every space embed, so that reading is ruled out.Matrix.PosSemidef (symmetric by definition); is Q.mulVec (fun _ => 1) = 0. Both hypotheses on are needed: without zero row sums the all-ones matrix, and without semidefiniteness , would violate the inequality for every space with two points at positive distance.Proofs of any milestone, alternative proofs of the goal, and reusable lemmas on the positive semidefinite cone are welcome.
A retailer who stocks a perishable or storable product each period must choose an order-up-to level without knowing the demand distribution. Worse, demand is censored: when the shelf empties, the retailer observes sales, not demand. Huh and Rusmevichientong (Math. Oper. Res. 34(1), 2009) proposed the Adaptive Inventory Management (AIM) algorithm, a projected stochastic subgradient method that uses only the censored observation "was there stock left at the end of the period?". They proved that its average expected cost converges to the cost of the optimal newsvendor level at rate , with no parametric assumption on demand.
In the non-perishable case, where leftover stock carries over, the main convergence theorem (Theorem 2, p. 7) requires the step-size scale to satisfy , where is a known lower bound on mean demand. Section 3.2 of the paper removes this requirement. Its Theorem 8 bounds the excess cost of AIM for every step scale , at the price of a hitting time and a busy period in the bound. This mission formalizes Theorem 8 and the steps of its proof.
Demands are independent, nonnegative, identically distributed, with finite positive mean and otherwise unknown law. The holding cost is per unit left over and the penalty is per unit of unmet demand. The newsvendor cost of stocking up to is
and the newsvendor quantity is . The manager knows an upper bound .
AIM, non-perishable case. Fix and a starting target . Put , . In period the step is , the observed slope is if and otherwise, and
The target follows the gradient step. The implemented level can exceed it because stock that has already been bought cannot be returned. The excess-cost term is
Auxiliary processes. Let . For a real :
For , the proof uses and .
For every and every with ,
The statement makes no moment assumption on demand. It is stated with the paper's explicit constants, and both expectations on the right may be infinite.
The result. The cost of AIM relative to the newsvendor benchmark splits as . Stochastic subgradient descent controls for every , so Theorem 8 is the remaining step in showing that AIM converges at rate without any knowledge of a lower bound on mean demand. The first term of the bound is whenever is finite, and Lemma 9 gives that under a finite fourth moment. The second term is whenever is finite, and the paper's Proposition 4 gives that under a finite sixth moment. The result therefore removes the one piece of prior information about demand, other than , that the non-perishable analysis needed.
Formalizing it. The paper's proof is complete and short, but it moves between expectations of random indices, pathwise couplings and renewal arguments, and the statements of Theorem 8 and Lemma 9 contain the slips recorded below. None of these results has a machine-checked proof. The mission produces a checked AIM recursion, a pathwise domination of excess inventory by a queue, and hitting-time and busy-period bounds for random walks with nonnegative i.i.d. decrements.
The argument behind Theorem 2 dominates by a queue whose inflow is below the mean demand. For large the inflow exceeds in early periods, so the queue is unstable at first and its busy periods are not controlled by a stationary queue. A direct bound on through busy periods of fails, because may never empty when . The proof therefore separates a random initial stretch, which ends at the first time after that empties, from the remainder. The two parts are bounded by different processes. The random index sits inside the sums, so the expectations have to be handled with that dependence.
CappedBaseStock_Model (DemandLaw, the i.i.d. path measure demandPathLaw). Its law has finite and strictly positive mean. The cost and are the published backorderCost and newsvendorLevel of LostSalesOrderUpTo.Asymptotic.Backorder. Both are reused, not redefined.d (t-1). AIM is a deterministic recursion on the path, and depend on only. Levels are real numbers, and is evaluated at nonnegative levels.A lattice is the set of integer combinations of linearly independent vectors in . Many computational problems — factoring polynomials over , simultaneous diophantine approximation, integer programming in fixed dimension, breaking knapsack cryptosystems, and the analysis of lattice-based cryptography — reduce to finding a good basis of a given lattice: one whose vectors are short and nearly orthogonal. In 1982 A. K. Lenstra, H. W. Lenstra, Jr. and L. Lovász gave a polynomial-time algorithm that turns any basis into a reduced one, now called the LLL algorithm (Math. Ann. 261, 1982). It was the key step of their polynomial-time factoring algorithm for , and it has since become a standard tool of computational number theory, combinatorial optimization and cryptanalysis.
This mission formalizes the algorithm itself, as described in (1.15) of the paper, and the paper's proof (1.23) that it terminates and returns a reduced basis of the input lattice. A companion mission of the same series treats the properties of reduced bases ((1.6)–(1.12)); a third treats the factoring application (Sect. 2).
Let be linearly independent and ; the form a basis for . The Gram–Schmidt vectors and coefficients are defined by
The basis is reduced if for and for .
The algorithm keeps a current basis and a subscript , starting at . While it performs one step:
The algorithm stops when . Before and after every step the situation (1.16)–(1.17) holds: the first vectors satisfy both conditions of reducedness among themselves.
The termination proof uses the Gram determinants (), the potential , and the minimum .
For every basis of ():
every reachable state with admits a step, and every reachable state has a reduced basis for .
For with , : the number of case-1 steps satisfies ; the identities (1.27)–(1.29) making the common denominators; and throughout.
The termination theorem is what makes reduced bases computable: the bounds of (1.6)–(1.12) on reduced bases are useful only because the algorithm produces such a basis from any input, and the factoring algorithm of Sect. 3 calls it as a subroutine. The explicit count is the step bound behind the paper's operation count (1.26).
On the formal side, Mathlib has Gram–Schmidt orthogonalization and Minkowski's convex body theorem, but no lattice basis reduction. A verified LLL implementation exists in Isabelle/HOL (the Archive of Formal Proofs entry A verified LLL algorithm, 2018), with its own algorithm description and representation. No Lean 4 formalization of the paper's algorithm or its termination proof exists, as far as could be determined. The result is proved; what is open here is its formalization.
The naive termination argument — "each case-1 step makes a vector shorter" — fails: case 1 can lengthen , and moves back and forth. The paper's argument needs a potential that decreases by a fixed factor in case 1 and is invariant in case 2, the identity to see that only moves, and a lower bound on depending only on . That lower bound rests on the Hermite-type estimate that a lattice of rank with Gram determinant has a nonzero vector with , which is not in Mathlib and must be derived from the geometry of numbers for sublattices of lower rank. The invariant (1.16)–(1.17) requires tracking how the Gram–Schmidt data of the first vectors change under a swap and under the size reductions of case 2.
is EuclideanSpace ℝ (Fin n), with Lean indices for the paper's ; is Mathlib's unnormalised InnerProductSpace.gramSchmidt, and is (1.3) verbatim. A state is a pair with stored as the paper's subscript; and are recomputed from , so the update formulae (1.22) are consequences, not definitions. One step is a relation: "the integer nearest to " is any integer with , so every tie rule is covered. The loop of case 2 picks the largest bad index , as on the page, and runs until (1.21) holds. The relation follows the text of (1.15), not Fig. 1 (which never visits and stops at ). The standing hypotheses are and linear independence of the input basis.
A trivializing formalization is excluded: termination alone would hold for a relation that never fires, so the goal also asserts that a step exists at every reachable state with , and a sorry-free sanity file exhibits both cases firing for . The goal does not mention , or , which appear only in milestones.
Not formalized: the operation count and binary-length bound of (1.26), which need a cost model; the bounds (1.30)–(1.34) on intermediate states and the bounds "throughout the course of the algorithm" on p. 524, which concern states inside a step; and Remark (1.37). Contributions welcome: a reusable Hermite-constant bound , Gram determinant identities, and invariance of Gram determinants under unimodular changes.
A multicommodity flow problem asks to route several commodities simultaneously through a capacitated network, each from its own source to its own sink. For a single commodity, the max-flow min-cut theorem of Ford and Fulkerson says that the largest routable flow equals the capacity of the smallest separating cut. For many commodities the natural analogue fails: the max-flow can be strictly smaller than the min-cut, already for four commodities (Okamura and Seymour, 1981). Leighton and Rao asked how large the gap can be, and showed that for uniform demands it is at most logarithmic in the number of nodes. The result turned the min-cut, an NP-hard quantity, into something approximable by a linear program, and became the basis of the first polylogarithmic approximation algorithms for sparsest cut, balanced cut, minimum feedback arc set, crossing number and VLSI layout (Leighton–Rao, J. ACM 1999).
Timeline:
A network is a finite set of nodes with a capacity for every pair; the pair is an edge when . For with complement , the cut capacity is the total capacity of the edges joining to . As in the paper, the network is assumed connected: for every nonempty proper .
In the uniform multicommodity flow problem (UMFP) every unordered pair of nodes is a commodity with demand one. A routing of value sends units between every pair simultaneously, so that the total flow of all commodities over each edge, in both directions together, is at most its capacity. The max-flow is the largest such (the concurrent max-flow).
The min-cut (sparsest cut) of the UMFP is
the minimum over cuts of the cut capacity divided by the demand separated by the cut. The quantity is the ratio cost of the cut.
The milestones use the dual objects. A distance function assigns a nonnegative length to each edge; is then the shortest-path distance, , and the total weight is . The distance constraint (5) is , summed over unordered pairs. A set of nodes has radius at most if some centre reaches all its nodes by walks inside the set of length at most . Throughout, .
for every uniform multicommodity flow problem: there is one absolute constant such that for every connected network with nodes. The goal fixes no constant, so it is the form any improved argument would still prove.
and : Theorem 2 with the constant its proof produces.
The theorem says that the LP relaxation of uniform sparsest cut has integrality gap , and the expander example of §2.1 (Theorem 1) shows this is tight. Combined with the cut-finding argument, it gives an -approximation for sparsest cut and, through the paper's Section 3, approximation algorithms for balanced separators, minimum cut linear arrangement, crossing number, VLSI layout area, feedback arc set and the emulation of networks. Region-growing decompositions of the kind in Lemma 3 reappear in low-diameter decompositions, multicut (Garg–Vazirani–Yannakakis), and metric embedding.
The result is proved; no machine-checked proof of it is known. A formalization would provide: concurrent multicommodity flow and its LP dual on finite graphs, the uniform sparsest cut, a verified region-growing decomposition, and the max-flow min-cut gap theorem itself. The LP-duality milestone, which the paper cites rather than proves, is a reusable piece of flow theory in its own right.
The upper bound is a counting argument. The lower bound is the content. The natural idea, rounding an optimal dual distance function by a threshold and cutting the long edges, does not work: the paper notes (p. 797) that no thresholding rule is known that always yields a good cut, because edges with large distance need not form a sparse cut. Any argument must convert the fractional dual into a single cut while losing only a factor against the total weight , which requires a global property of the distance function rather than the lengths of individual edges. The LP-duality step needs a correct dual for the concurrent flow problem with shortest-path distances, which Mathlib does not provide off the shelf.
V is a Fintype with decidable equality; capacities are a symmetric nonnegative real function vanishing on the diagonal, and the graph is the simple graph of pairs with positive capacity. Goal-level statements assume 2 ≤ Fintype.card V and connectivity in the form for every nonempty proper (the paper's standing assumption, p. 789).Contributions welcome: proofs of any milestone; a general LP-duality theorem for concurrent multicommodity flow, reusable for the product and directed variants; and a general region-growing lemma.
A component may be exposed to shocks that arrive at random times. Its chance of lasting for a given time depends both on how often shocks arrive and on how likely it is to survive successive shocks. Reliability calculations often begin with the latter, discrete sequence, while replacement and life-testing questions concern the resulting lifetime distribution. Esary, Marshall, and Proschan study how a property imposed on the shock sequence appears in the continuous lifetime law. Their Theorem 3.1 gives several such inheritance results; this mission targets its increasing-hazard-rate assertion (Esary, Marshall, and Proschan 1973, Theorem 3.1).
An increasing hazard rate (IHR) means that the remaining life of a component that has survived to age becomes stochastically shorter as increases. This is a concrete way to express wear-out. The paper treats “increasing” as weakly increasing throughout, so a constant hazard rate is included (Esary, Marshall, and Proschan 1973, pp. 628, 631).
Shocks arrive according to a homogeneous Poisson process with rate . Let be the probability that the component survives the first shocks. The sequence starts at and satisfies for the target theorem. The probability of failure on the st shock is . At a nonnegative time , the chance of exactly shock arrivals is . The survival function of the component is therefore the Poisson mixture
and the paper sets for . At positive times its density is . The failure-on-shock sequence and the positive-time density are both part of the mission because the paper compares their shape as well (Esary, Marshall, and Proschan 1973, (2.1)–(2.3)).
A nonnegative sequence is PF₂ here when its successive ratios decrease weakly, wherever those ratios are defined. For the survival probabilities this says decreases with . A survival function is IHR when, for each , the survival ratio decreases with age wherever it is defined. These are the discrete and continuous conditions connected by the target (Esary, Marshall, and Proschan 1973, Definition 2.3 and p. 631).
The goal is Theorem 3.1(3.2):
It covers any nonnegative, weakly decreasing shock-survival sequence with and a positive Poisson rate. It does not fix a finite number of shocks or a special survival law (Esary, Marshall, and Proschan 1973, p. 632).
The milestone list includes the positive-time density formula (2.3), the upper bound in (2.5), the derivative estimate from the proof of (3.1), and that proof's sign-change claim for . It culminates in Theorem 3.1(3.1), which says that PF₂ failure-on-shock probabilities give a PF₂ positive-time density. These are statements made explicitly by the authors and form the neighboring shape result and the estimates cited in the proof of the IHR goal (Esary, Marshall, and Proschan 1973, pp. 628–629, 632–633).
The mission also poses, outside the milestone list, the other inheritance results of the same section and of §6 whose formulation uses the same objects:
where is the condition of Murthy and Lientz, strictly weaker than PF₂. Theorem 6.1 specializes to independent shock magnitudes, (exponential, IHR or DHR as is constant, decreasing or increasing in ), and Theorem 6.2 shows that a random threshold, , always gives a logarithmically convex density on (Esary, Marshall, and Proschan 1973, pp. 632, 634, 647).
The target makes a discrete reliability assumption useful for continuous-time decisions. One may model or estimate the sequence from how the component responds to successive shocks and then infer an ageing property of its lifetime under Poisson arrivals. The conclusion is about residual lifetime at every age, not just its mean or one tail probability. The companion PF₂-density statement shows that the same transfer applies to failure-on-shock probabilities and the resulting continuous density (Esary, Marshall, and Proschan 1973, Theorem 3.1).
The 1973 results are proved in the paper. In this mission the Lean statements compile as open theorems; their mathematical proofs are still to be formalized. A completed development would make the Poisson-series model, its density, and the discrete-to-continuous shape claims reusable in later formalizations of shock and wear models. The other missions in this paper's series consider cumulative damage, first passage under wear, and random thresholds using related ideas.
The survival function mixes infinitely many shock counts. Each count has its own time-dependent Poisson weight, so a decreasing ratio of adjacent terms does not give the desired comparison of survival ratios by a termwise inequality. The paper invokes a variation-diminishing property of a totally positive Poisson kernel for the corresponding shape arguments (Esary, Marshall, and Proschan 1973, p. 633). A formal proof must also justify differentiation and rearrangement of the infinite series, including sequences that reach zero after finitely many shocks.
The Lean model uses real-valued functions for , , and , with the shock count indexed from zero. The Poisson mixture is the definition of ; no random lifetime is introduced in place of it. The value for negative time follows (2.1). IHR is expressed for all real ages by cross-multiplying the survival-ratio comparison. With , this includes the boundary at zero without an atom there. PF₂ sequence and density conditions are also cross-multiplied. This gives the paper's ratio statements wherever denominators are positive and retains the natural zero-survival cases without using real division by zero.
The source treats as probabilities, takes , and restricts variables to avoid zero denominators; Lean states the rate, nonnegativity, weak monotonicity, and the ratio convention explicitly. Formula (2.3) is represented by the derivative identity at positive time. The bound (2.5) is , equivalent to the hazard-rate statement wherever survival is positive. The sign-change milestone excludes a strict positive–negative–positive pattern at increasing positive times, matching the authors' “at most two, in the order negative, positive, negative” wording. These conventions prevent an empty IHR statement or a trivial result caused by totalized division.
A complete proof needs reusable facts about convergence and differentiation of Poisson-weighted series and about preservation of sign patterns under the Poisson kernel. Contributions to that infrastructure, the density and hazard estimates, and the PF₂ transfer are in scope, as are the further results above. For those, the reversed classes are stated on the life-distribution domain: DHR compares ages only, because Theorem 3.2 allows , an atom at the origin; a logarithmically convex density is the reversed cross-multiplied PF₂ inequality for on . Mean residual lives and mean lives are computed in (they are infinite when ), and their ratios are taken only where . In Theorem 6.1 only the numbers enter, and "exponential" includes the rate ; in Theorem 6.2 the shock and threshold laws are probability measures on with no mass on . The paper's further remark that a survival function needs is not imposed: none of the theorems uses it.
Pricing a financial derivative, estimating a risk measure, or computing any expected functional of a stochastic differential equation (SDE) by simulation runs into two errors at once: the statistical error of averaging finitely many sampled paths, and the discretisation bias of replacing the exact SDE solution by a numerical scheme with a positive timestep. With the Euler scheme and independent paths, the mean-square error behaves like , so a root-mean-square accuracy requires paths of steps each: a cost of order .
Giles' Multilevel Monte Carlo path simulation (Operations Research 56(3), 2008) showed that combining simulations on a geometric hierarchy of timesteps reduces this cost to order for the Euler scheme with a Lipschitz payoff, and to , the cost of an unbiased estimator, when the level differences have fast-decaying variance. The two-level case is due to Kebaier (2005), who reduced the cost to order ; Heinrich's multilevel method for parametric integration (2001) is a precursor. The paper's Theorem 3.1 is stated abstractly, in terms of four rate conditions, and has since been applied to SDEs, SPDEs, Markov chains and nested simulation; the survey of Giles (Acta Numerica 2015) traces this development.
Fix an integer refinement factor and a horizon , and let the timestep of level be , . On a probability space, let be the quantity of interest (in the paper, a functional of the solution of an SDE driven by a Brownian path) and its approximation with timestep . Since
the method estimates each term independently. For each level and sample size , is an estimator of () or of () built from samples, with computational complexity . The multilevel estimator is , its total complexity is , and its mean-square error is .
The hypotheses are four rate conditions, with constants and : (i) (weak convergence order ); (ii) equals or (unbiasedness of each level); (iii) (variance decay rate ); (iv) (cost proportional to samples times steps).
There is a constant such that for every there are and with
The constant is uniform in ; its value is not part of the goal.
The milestones are the displayed steps of the paper's proof, in its order: the choice of the finest level and the resulting two-sided bound (6) on ; the bound on the squared bias; the geometric bound (7) on ; and, for each of the three regimes , , , a choice of with a bound on the variance (using the geometric bounds (8) and (9) in the last two) and an explicit cost bound with an explicit constant . In case the bound on the number of levels is a separate milestone.
The theorem turns the multilevel idea into a complexity statement: whenever a discretisation has weak order and its level corrections have variance decay , the cost of accuracy is known up to a constant. It identifies as the parameter governing the method, explains where the effort is spent (coarse levels for , fine levels for ), and is the template that later multilevel analyses (Milstein schemes, multi-index Monte Carlo, randomised MLMC) follow and refine.
The result is proved in the paper and widely reused. To our knowledge it has no machine-checked proof. The mission produces one: a Lean statement of the abstract theorem and of each step of the proof, with the paper's explicit constants. Its probabilistic content is light (linearity of expectation, the bias-variance decomposition, Bienaymé's identity for independent variables); most of the work is careful real analysis with ceilings, logarithms and real powers.
No single step is deep; the difficulty is bookkeeping under exact constants. The obvious argument "choose , choose " is asymptotic. The theorem demands, for every , an exact bound with a constant independent of . This forces the integer ceilings in and to be controlled explicitly (each ceiling adds one sample per level, whose total cost is (7)), the number of levels to be bounded by a multiple of , and the three geometric series to be summed with constants independent of . The strict inequality is not delivered by the paper's own choice in case , where both halves give only ; a solver must adjust the sample sizes.
, and the level estimators are arbitrary real random variables on a probability space ; the SDE and its discretisation enter the theorem only through (i)–(iv), so they are not modelled. This makes the statement more general, not weaker. Expectations are Bochner integrals and is Mathlib's variance. The conventions are:
Real.rpow, is Int.ceil for and Nat.ceil for (whose arguments are positive).A formalization in which the cost is defined as , in which (ii)–(iv) hold only for one fixed sample size, or in which the MSE and cost bounds are proved for different and , is a different and weaker theorem and is ruled out by the statement.
Infrastructure needed: geometric-series bounds with real ratios, floor and ceiling estimates for logarithms, and Bienaymé's identity (Mathlib's IndepFun.variance_sum). The bias-variance decomposition for variables is reusable beyond this mission. Proofs of individual milestones, and alternative proofs of the goal, are welcome.
Retailers selling several related products can change prices as inventory runs down. A sale of one product changes the stock available in later periods, while changing its price also shifts demand toward or away from the other products. Dong, Kouvelis, and Tian study these linked decisions for substitute product variates under a multinomial logit customer choice model. Their 2009 article gives an exact characterization of the optimal dynamic price vector when each in-stock variate can have its own price. The characterization separates a product's inventory opportunity cost from a margin shared across all products, which makes the result more informative than an opaque Bellman maximization.
The mission isolates Theorem 1 of that article. The paper also studies restricted policies that require a unified price or fixed prices for some variates; those results are separate missions in this series. The present target concerns the fully flexible dynamic policy of §3.1, with the model and conventions of §2.
There are product variates, indexed by , with finite quality parameters . Time is the number of periods remaining, so it counts down to zero. The inventory state has nonnegative integer coordinates, and is the set of variates still in stock. At most one customer arrives during a period, with probability satisfying . Inventory is not replenished. The retailer chooses a finite, nonnegative price for each in-stock variate. An out-of-stock variate receives the paper's null price and contributes no demand.
An arriving customer chooses among the in-stock variates and the no-purchase option. The multinomial logit model assigns deterministic utility to variate and utility to no purchase, with positive scale . Its probabilities are
Let be the maximum expected revenue from state with periods remaining and zero terminal value . A sale of variate moves the inventory to . Its marginal inventory value is when . For a continuation value , the one-period objective is current expected sales revenue plus the expected continuation revenue after a sale or no sale. The Bellman value takes its supremum over all finite nonnegative price vectors. Equation (5) rewrites that objective as , where is the probability-weighted marginal revenue.
Theorem 1 asks for a unique common margin satisfying
For every in-stock variate, the price must be feasible and attain the Bellman maximum. The margin also satisfies . These claims hold for every inventory state, including an empty in-stock set. They are the main target of Theorem 1, equations (9)–(10).
For each , let be the unique margin equation root at the same inventory state , with periods remaining. The remaining clause of Theorem 1 states
The milestones track the paper's equation (5) and Steps 1–5 of its Appendix A argument: marginal inventory value, the mapping between prices and choice probabilities, concavity in probability coordinates, existence of the margin, optimal choice probabilities, and the one-period value identity.
The result turns a coupled dynamic program into a precise pricing characterization. It says that differences in optimal prices across products reflect differences in their marginal inventory values; the remaining margin is common. The value identity quantifies the expected revenue earned over the remaining horizon, and the explicit maximizer removes ambiguity about whether the Bellman supremum is attained. These conclusions support the paper's comparisons with restricted pricing policies and its later discussion of how quality and inventory scarcity affect prices Dong, Kouvelis, and Tian (2009).
The result is proved in the article. This mission contributes a Lean statement of the full theorem, its model, and seven named intermediate targets. The draft declarations compile against the pinned Mathlib environment; their proofs remain open. A complete formalization would provide reusable finite MNL choice probabilities, inverse price and probability identities, and a Bellman model for substitute-product inventory. The paper's economic conclusions should be recovered from those formal statements, rather than from a weakened existence claim.
The direct one-period objective in the price vector is not quasiconcave, as the paper notes on p. 323, so a local condition on prices alone does not establish global optimality. The price vector also ranges over an unbounded set, and a supremum could conceal a boundary or attainment issue. Finally, one extra unit of stock changes future probabilities across all products, not just the revenue of that product. These interactions make nonnegative marginal inventory value and the global optimality assertion substantive parts of the result. The probability-space objective is concave on its positive domain, but the printed Appendix A claim of strict concavity on the full domain is stronger than that function permits; uniqueness concerns the normalized choice-probability slice.
Lean represents products by Fin n, inventories by functions Fin n → ℕ, and time by a natural number counting remaining periods. The model assumes and . The set filters positive inventory coordinates; an out-of-stock variate is removed from every choice-probability sum, so its null price need not be encoded as a finite real. The objective's no-sale continuation term is counted once, following equations (5) and (22), despite the ambiguous bracket placement in printed equation (3). In-stock prices are finite and nonnegative. Off-stock coordinates of the displayed candidate vector are set to zero and do not affect demand.
Lean's natural-number subtraction in is used only for , where it subtracts exactly one unit. The Bellman value uses a real sSup, whose default on a badly bounded set could otherwise obscure the theorem. The goal and final milestone therefore require an explicit maximizing price vector and equality between the value and its objective. The margin root is stated as unique and every root is covered; it is not hidden behind a choice operator. Equation (11) quantifies over all roots for at one fixed , not along a sample path. No assumption that or is nonempty is added to the goal. The price–probability mapping and interior optimality milestones assume nonempty where the paper's positive-simplex argument requires it.
A complete development needs finite-sum algebra, real exponential and logarithm facts, concavity on products of real function spaces, and boundedness and attainment facts for the Bellman objective. The MNL probability and inverse-map facts can serve later pricing models; the dynamic value and marginal-stock lemmas serve inventory-control formalizations. Contributions that prove these statements or isolate reusable analytic lemmas are within scope. The statement must retain both the Bellman maximizer and the value identity, so a default sSup value cannot turn the goal into a trivial equality.
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.
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.