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?
Programs often reveal information through the memory locations they touch, even when the contents of those locations are hidden. An oblivious RAM simulation aims to conceal this access pattern. Goldreich and Ostrovsky studied the cost of doing so for arbitrary RAM programs and showed that the access sequence itself imposes a lower bound on simulation overhead. Their 1996 paper gives an upper-bound construction as well as the lower-bound theorem targeted here. The issue matters when a storage observer can see which addresses are accessed but must learn nothing about the program's private requests.
Theorem 6.1 of the paper states that simulating steps requires at least the initial memory size and, asymptotically, a multiple of accesses. Its proof introduces a simpler ball-and-cell game that grants the player more information and freedom than the RAM simulation. The mission formalizes that game and its lower bound. This makes the combinatorial content of the published argument a precise theorem about randomized behavior and visible observations. The paper's earlier Theorem 1.2.2 on p. 437 is labeled informal and has a different explicit bound; the target here is Theorem 6.1 on pp. 469–470.
There are numbered balls and numbered cells. Cell initially contains ball , and a player's hand is empty. Each cell can hold at most one ball and the hand can hold at most balls. In one access, the player names a cell and secretly takes its ball into a nonfull hand, places one held ball into an empty cell, or leaves the cell unchanged. Taking from an empty cell and placing into an occupied cell are illegal. The observer sees the named cell at each access but not the hidden operation. A run of accesses is written , and its visible sequence is .
A request sequence names a ball for each of rounds. A run satisfies if it is legal and there are indices such that ball is in the player's hand after the first accesses. Equal indices are permitted: several rounds may finish after the same access. The player may know the entire request sequence in advance. That assumption is part of the paper's game, and the paper notes that its lower bound does not require an online player.
A randomized player assigns each request sequence a probability distribution over finite runs. It is correct if every run with positive probability satisfies its requests. It is oblivious if the distribution of is identical for every pair of request sequences of length . Thus the observer cannot infer the requested balls from the accessed cells, even statistically. These conditions quantify over all request sequences, not a selected input or a single deterministic access pattern.
For every correct oblivious player and every run in the support of its response, the mission targets
where and depend only on the fixed hand size . This is the paper's form, with representing the number of initially occupied memory words. It asserts a bound on every possible run, rather than only on average access count. No numerical constant is prescribed by the paper.
The milestones record the first-round bound, the at-most- count of legal hidden action sequences compatible with a visible sequence, and the implication from obliviousness that one visible sequence can serve every request sequence. They then state the corrected finite counting bounds
These preserve the paper's non-strict round ends. The milestone source text records the published formulas, while the formal statements and descriptions identify the corrections.
The result limits how cheaply a simulator can hide a program's memory access pattern when the observer sees addresses. In the game, a player is even allowed to remember the entire ball placement without cost, know the future requests, and randomize its actions. A lower bound under these permissive conditions applies to the more constrained access-pattern problem that motivated the game, subject to the paper's reduction from simulation to the game. The term also accounts for the initially occupied memory, independently of the asymptotic term.
The theorem is a published mathematical result, but the mission's Lean declarations are statements with proof holes until solvers supply machine-checked proofs. Formalizing the game creates reusable definitions for legal hidden operations, request satisfaction, randomized players, and visible distributions. Formalizing the corrected counting targets also makes explicit a discrepancy in the printed proof rather than silently relying on an invalid intermediate inequality.
The main difficulty is accounting for requests when several rounds end at the same access. The paper's observation that a fixed -access run serves at most request sequences is false under its own non-strict indices. A run that fetches every ball it can hold may answer many later rounds without making another access. Likewise, the alternative binomial count in footnote 29 assumes distinct completion points and fails when . The final asymptotic result still has a valid corrected counting target, but a proof cannot quote the published intermediate formulas literally. Randomized behavior adds another precise requirement: equality of visible distributions must support conclusions about runs with positive probability for each request sequence.
The Lean carrier is the paper's ball-and-cell game from §6, rather than the interactive RAM machine model of §2. The game relaxes the simulation by giving the player free memory of ball locations and advance knowledge of requests. Balls, cells, and rounds use finite types Fin m and Fin t; these are zero-based encodings of the paper's and round labels. Action steps are counted from one, with the initial state at step zero. PMF represents the player's discrete probability distributions, and equality of PMF.map visible represents observer independence. Every positive-probability run must be legal and satisfy its requests. The visible and hidden sequences have the same finite length .
The two printed estimates and are false: with and , taking both balls in two accesses satisfies all request sequences, while the printed product is . Footnote 29's also vanishes in this example. The formal milestones use Nat.multichoose q t to accommodate repeated round ends; at its value is defined directly, so no negative binomial upper index is used. The logarithm in the goal is the natural logarithm, and a threshold handles small .
Correctness and legality are part of the player type, so an unrestricted sequence of cell names cannot satisfy the mission by bypassing the hand and cell rules. Obliviousness uses equality of full distributions, and the goal quantifies over every supported run. The required development includes finite-state transition reasoning, finite combinatorial counts, PMF support and mapping, and real logarithm estimates. These components, especially the game interface and support lemmas, can be reused by later access-pattern formalizations.
A cooperative game with side payments assigns to each coalition of players the total payoff it can secure on its own and share freely among its members. The core is the set of ways of dividing the payoff of the grand coalition that no coalition can improve upon. It is the basic stability notion of cooperative game theory and of its applications in operations research: cost allocation for shared facilities, network design, inventory pooling and linear production games all ask whether a core allocation exists and what it looks like.
The core can be empty, and the question of when it is not was answered independently by Bondareva (1963) and Shapley (1967): the core is nonempty exactly when the game is balanced, a linear-programming condition on weighted families of coalitions. Scarf (1967) extended the existence half to games without side payments, and Billera (1970) recast balancedness for those games.
Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6(1), 1981) reads these results through fuzzy coalitions, in which each player participates at a rate between 0 and 1. In §6 every game on a family of coalitions is extended to a concave positively homogeneous function of fuzzy coalitions, and the Bondareva–Shapley theorem becomes a statement about that extension. This mission formalizes §2 and §6 of the paper: the core of a fuzzy game with side payments, its superdifferential description, and Proposition 6.1.
Let be the set of players. A coalition is identified with its characteristic vector , and . A fuzzy coalition is a vector , where is the rate at which player participates.
A fuzzy game with side payments is a worth function with that is positively homogeneous, for . Homogeneity extends from to the orthant . Its core is
the allocations that no fuzzy coalition blocks. The superdifferential of at is .
A usual game with side payments is given by a family of nonempty coalitions that contains and every singleton , and by a worth for each . Its core is the set of with and for every . For , is the set of nonnegative weights , , with for each player , and
The game is balanced if .
The first half is the Bondareva–Shapley theorem for an arbitrary family . The second identifies the core of the discrete game with the core of the fuzzy game .
Proposition 6.1 is the standard criterion for the existence of core allocations in transferable-utility games. In operations research it is the tool behind core results for linear production games, flow games, facility location and inventory games: one exhibits a family of balancing weights, or the absence of one, and reads off whether a stable cost or profit allocation exists. Aubin's version adds that a balanced game's core is the superdifferential of a concave function, so it is described by convex analysis and, when is smooth at , reduces to a single point given by the gradient.
The result is classical and proved in the literature. To our knowledge, no machine-checked proof of the Bondareva–Shapley theorem exists in Mathlib or on this platform: the platform has results on cores of convex (supermodular) games, which are a different hypothesis. The mission therefore produces a first formal proof of the theorem for a general family of coalitions, the superdifferential description of the fuzzy core, and the minimality of the concave extension . The definitions (fuzzy coalitions, balances, ) are reusable by later missions on games without side payments and on values of fuzzy games.
The inclusion and the necessity of balancedness are short computations with the balancing weights. The difficulty is sufficiency: from , a core allocation has to be produced. This is an existence statement for a system of linear inequalities, and it needs a duality or separation argument. Mathlib's finite-dimensional linear programming duality and separation theorems do not apply off the shelf, because is a supremum over a polytope of weights indexed by coalitions, and its attainment and finiteness must be established first. Proposition 2.1 similarly needs the existence of supergradients of a concave function at an interior point and their compactness, which are not packaged for functions defined only on an orthant.
Players are Fin n; multiutilities and fuzzy coalitions are Fin n → ℝ with the coordinatewise order, and the cube is Set.Icc 0 1. The commitments are:
DifferentiableAt at the interior point , and is the vector of partial derivatives.Balancedness is the equation with built from the balances of §6 (3)–(4); a formalization that defines "balanced" through the core, or takes to be an envelope already known to agree with the core, makes the goal empty and is ruled out. Contributions welcome: proofs of the milestones, a general Bondareva–Shapley lemma for finite families of coalitions, and supergradient existence for concave functions on convex sets with nonempty interior.
A probability forecast is useful only when its stated frequencies bear a stable relation to outcomes. If a forecaster repeatedly announces a 70% chance of rain, calibration asks whether rain occurs on about 70% of those days. This is a minimal reliability requirement for probabilistic prediction, even though calibration alone does not rank every pair of forecasts by usefulness. Foster and Vohra study the difficulty of obtaining this property when the weather sequence is chosen in response to a forecaster's past behavior. A deterministic rule can be forced into a persistent calibration error; the article shows how randomized forecasts evade that obstruction when Nature sees past forecasts but cannot see the current random draw. Foster and Vohra, 1998.
The work sits at an intersection of sequential probability forecasting and repeated games. Its opponent can adapt to the whole observed history, including the forecaster's earlier random outcomes. The simultaneity of each round matters: before choosing that round's wet or dry outcome, Nature knows the distribution of the next forecast but not which forecast is realized. The paper's main result is about a specified forecasting rule constructed from regret balances, rather than merely the existence of some successful randomized strategy. Foster and Vohra, 1998, §§3, 5.
Timeline. Dawid (1982) proposed calibration as a criterion for sequential probability forecasts and showed that a coherent Bayesian expects to be calibrated (doi). Oakes (1985), with Dawid's accompanying comment, showed that no deterministic forecaster is calibrated against every outcome sequence: Nature may rain exactly when the forecast is at most (doi). Foster and Vohra circulated the present randomized construction from 1994 (received August 1994, published 1998); their 1997 Games and Economic Behavior paper used a calibrated forecaster built on the same pairwise-regret flow equations to reach correlated equilibria (doi). Hart and Mas-Colell (2000) later turned the same internal-regret quantities into regret matching (doi).
At round , the outcome is for wet and for dry. The forecaster selects a probability from the finite grid , where is a positive integer. A forecast is represented by the binary probability vector ; the second coordinate is the forecast chance of rain. The forecaster chooses with probability . The Brier loss of that possible forecast is .
After rounds, counts the realized forecasts equal to , and is the observed fraction of wet outcomes on those rounds. The quadratic calibration score is
A forecast never issued has zero count and contributes zero. The paper also uses a weighted calibration score , in which the realized indicator that was chosen is replaced by its conditional probability . Its weighted count is , and its weighted wet frequency is when the denominator is positive.
For grid points and , the pairwise regret is the positive part of the cumulative weighted reduction in Brier loss that would result from replacing by on rounds weighted by . The algorithm chooses its next distribution so that the regret flow out of each equals the flow into :
These equations use only regret from previous rounds. They specify a distribution after every possible history, including histories created by Nature's adaptive choices. Foster and Vohra, 1998, §5.
The target is Theorem 1: for every , choose and let the forecaster follow the regret-flow equations. Against every adaptive Nature, the realized score eventually satisfies
The time after which the inequality holds may depend on the forecaster, Nature, and . The statement fixes the algorithm and the grid scale; a general existence theorem would leave out its central content. Foster and Vohra, 1998, Theorem 1 and §6 Corollary.
The milestones record the source's attack path: solvability of the flow equations, a history-adapted forecaster satisfying them, the counting-process bounds and convergence of in probability, the algebraic link between calibration and regret, the bound on the smoothed regret potential, and the deterministic bound on . Theorem 3's last constant is written as and the corollary's horizon as ; the printed constants are inconsistent with the paper's grid points and its derived rate, respectively. The provenance and corrections are recorded with those milestones. Foster and Vohra, 1998, §6.
The result gives a concrete randomized forecaster whose realized empirical frequencies remain reliable even when outcomes react to past forecasts. The game model includes fixed outcome sequences as a special case, but its adaptive Nature can condition future choices on every earlier realized forecast and outcome. The theorem therefore identifies a particular sequential rule, its finite forecast grid, and the information boundary under which its guarantee holds. Foster and Vohra, 1998, §§3, 5–6.
The published Foster–Vohra 1997 formalization already supplies reusable definitions of finite probability vectors, history laws, pairwise regret, and calibration scores, together with a proved finite flow-conservation theorem. This mission extends that substrate to the 1998 paper's Brier-loss grid algorithm. Theorem 1 and its supporting results are proved on paper but not yet formalized; the earlier formal existence theorem for some calibrated forecaster does not establish this algorithm's guarantee, which is the content of the goal.
The weighted score is controlled by quantities known from the chosen mixtures, while depends on the actual random draws. A direct deterministic bound on therefore does not follow from the regret equations. The gap requires a quantitative comparison of realized counts and weighted counts under an adaptive history law, followed by a passage from those count errors to the nonlinear calibration score. The regret itself has a positive-part kink, so its aggregate bound is stated through the paper's smoothed potential. Foster and Vohra, 1998, §6.
The Lean model uses binary outcomes, grid indices Fin (k + 1), and histories ordered from oldest to newest. Rounds start at index : the paper's in round is the regret over the preceding indices. Forecast and outcome are drawn independently conditional on the past by the published histLaw; Nature is any map from complete past histories to a probability distribution on the two outcomes. The forecast rule is likewise a map from histories to grid distributions. For each earlier round it reads only that round's prefix, so the current outcome cannot influence its mixture.
The goal uses the realized quadratic score calibScore2Hj h 1, whose second vector coordinate is the wet probability. The map is injective for . The weighted score is a separate definition used in supporting results. A forecaster satisfying the flow equations is shown to exist by a milestone, so the goal's algorithm hypothesis has content. The statement covers adaptive Nature; replacing Nature by a fixed sequence or replacing by would change the claim.
Every theorem requiring the grid has the explicit condition. Deterministic calibration bounds assume binary outcomes and probability-vector weights; the history-law theorems obtain these properties from Fin 2 and PMF. When a weighted count is zero, Lean's division convention gives weighted wet frequency ; nonnegative weights make its numerator zero as well. At horizon , the weighted calibration score is . The probability event is measured with the history law's outer measure in . Reusable work includes finite-history martingale estimates, weighted calibration comparisons, and finite regret-potential bounds.
The core of an exchange economy is the set of allocations that no group of consumers can improve upon by trading only among themselves. The Walras equilibria (competitive equilibria) are the allocations supported by a price system at which every consumer maximizes preference on a budget set. Every Walras equilibrium is in the core, but for a fixed finite economy the core is usually much larger. Edgeworth (1881) conjectured that the core shrinks to the competitive allocations as the number of traders grows; Debreu and Scarf (1963) proved this for replica economies, and Aumann (1964) proved exact equality for an atomless continuum of traders.
Jean-Pierre Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6 (1981) 1–13) gives a third route to the same conclusion, with a fixed finite number of consumers. Coalitions are allowed to be fuzzy: a consumer may join with any rate of participation between 0 and 1. Once all fuzzy coalitions may block, the core of the economy, now called the fuzzy core, is exactly the set of Walras equilibria (Theorem 4.1, p. 6). The paper presents this as a slight modification of the Debreu–Scarf theorem; in Remark 4.2 it observes that Debreu–Scarf's replica coalitions correspond to the rational points of the cube .
This mission formalizes §4 of the paper. It is the fourth mission of a series on the paper; the others treat the cores of fuzzy games with and without side payments and the values of smooth fuzzy games.
There are consumers and commodities. Consumer consumes bundles in , ranks them by a preference relation (with strict part ), and owns a set of possible initial endowments. Each is closed, convex and comprehensive: whenever and , also .
A fuzzy coalition is a vector ; is the rate at which consumer participates, and is the set of participants. The coalition disposes of the endowments
and its allocations are the families of bundles with ; this set is . The allocations of the whole economy are , .
An allocation is in the fuzzy core if there is no nonzero fuzzy coalition and allocation with for every .
The income of consumer at prices is , and the budget set is . An allocation is a Walras equilibrium if some price satisfies, for every ,
Assumption (1) of §4 requires each preference to be continuous and convex, with for ; no consumer to be satiated; and each to contain a vector with all coordinates strictly positive.
Under assumption (1),
The remaining step of the paper, from milestone 3 to the existence of the equilibrium price, is stated there only as "by known arguments" and is left to the solver as part of the goal.
The result. Theorem 4.1 is a core equivalence theorem for an economy with finitely many consumers and no replication or continuum of traders. It identifies the competitive allocations as exactly the allocations that are stable against partial coalitions. It also makes visible which coalitions matter: Remark 4.1 attributes the equivalence to the fact that all fuzzy coalitions are allowed to form, so that the set of coalitions is convex. The same fuzzy-coalition device underlies the nonemptiness results for cores of fuzzy games in §5–§7 of the paper.
Formalizing it. The theorem is proved in the paper, in one paragraph that defers its final step to "known arguments". To our knowledge neither the theorem nor the Debreu–Scarf or Aumann core equivalence theorems have been formalized in Lean. A complete development provides a reusable model of an exchange economy with preference relations and comprehensive endowment sets, a checked argument from separation to equilibrium prices, and a template for the classical core equivalence theorems.
The inclusion of the Walras equilibria in the fuzzy core is a budget computation. The converse is the content of the theorem: from the mere absence of improving fuzzy coalitions, a single price vector must be produced that works for all consumers simultaneously. Separating consumer by consumer gives one price per consumer, not a common one, so the coalitional structure has to enter before any price exists. Once a candidate price is available, it still has to be shown nonnegative, each equilibrium bundle has to exhaust its owner's income, and no bundle in a budget set may be strictly preferred; each of these uses a different part of assumption (1), and the paper leaves all three to "known arguments". The incomes may be for prices with negative coordinates, so finiteness at the equilibrium price is part of the conclusion, not an assumption.
Consumers are Fin n, commodities Fin l; an allocation is a function Fin n → Fin l → ℝ, a price a vector Fin l → ℝ, and . A single definitions file (FuzzyGames.Walras.Basic) holds the economy, its assumptions, , , the fuzzy core, incomes, budget sets, Walras equilibria and the sets .
The formalization commits to the following readings, each recorded in the items' Formalization Notes:
EReal), so that is represented and never replaced by a default value.A trivializing formalization is ruled out: the assumptions are satisfiable, and a sorry-free check (one consumer, one commodity, , ) verifies them together with a Walras equilibrium, so neither side of the goal is empty by construction.
Contributions welcome: proofs of the milestones, a separation-to-prices lemma for comprehensive endowment sets, and general facts about complete continuous convex preferences on , which are reusable for any general equilibrium development.
Many decisions are made before their objective coefficients are known. A planner may know the feasible decisions and the form of a linear optimization problem, but must predict its cost vector from available features. Squared prediction error measures how close a forecast is to the eventual coefficients; it need not measure the quality of the decision chosen with that forecast. Elmachtoub and Grigas define a loss based on the excess realized cost of the resulting decision, then introduce a convex surrogate, SPO+, for training prediction rules Elmachtoub and Grigas, 2020, §§2–3.
The central population question is whether minimizing the surrogate still selects predictions that minimize the decision loss when the full data distribution is available. Their Theorem 1 answers this under conditions on the feasible region and the conditional distribution of costs Elmachtoub and Grigas, 2020, p. 21. The result concerns the loss itself, before sample size, model capacity, or an algorithm for fitting a predictor enter the picture.
A feasible region is nonempty, compact, and convex. Given a cost vector , a decision incurs cost . The nominal value, optimal-decision set, and support function are
An optimization oracle returns one element of for each , without a tie-breaking rule. For a predicted cost and realized cost , the unambiguous SPO loss uses the worst realized decision among all decisions optimal for the prediction:
This is Definition 2 of the paper. Its SPO+ loss, Definition 3, is
The factor is fixed by the paper's surrogate. Proposition 3 states that SPO+ upper-bounds SPO, is convex in , and has the explicit subgradient Elmachtoub and Grigas, 2020, pp. 17–18.
Let denote an observed feature, its probability law, and the conditional law of given . Their joint law is . A measurable predictor maps each to a cost prediction . The population risks and are expectations over of the corresponding losses at , as in displays (11) and (12) Elmachtoub and Grigas, 2020, p. 20. There is no prescribed parametric predictor class.
Write . Under Assumption 1, the optimal-decision set is a singleton for almost every ; each conditional law is centrally symmetric about and continuous on all of ; and has nonempty interior. The goal says that every measurable minimizer of SPO+ population risk satisfies
This is the paper's Fisher-consistency statement, including its stronger identification of every SPO+ minimizer with the conditional mean Elmachtoub and Grigas, 2020, Theorem 1. The goal does not assert that a minimizer exists.
The milestone list follows the paper's numbered results: Proposition 3's pointwise upper bound, convexity, and subgradient; Proposition 6's mean minimizer and uniqueness claims for a single cost law; and both directions of Proposition 5, which relate SPO risk minimizers to decisions optimal at the mean Elmachtoub and Grigas, 2020, pp. 18, 22–23. The single-law propositions have no feature variable.
Theorem 1 identifies a condition under which a convex training objective preserves the population target of the decision loss. Its identification statement is stronger than merely saying that one selected SPO+ minimizer is SPO-optimal: all SPO+ minimizers agree almost surely with conditional mean cost. The propositions isolate what this depends on. Proposition 6 concerns the surrogate risk, while Proposition 5 connects a prediction's optimal-decision set to the true risk.
The result was proved in the cited preprint and published in Management Science in 2022; this mission asks for a Lean proof of that known result, not a new consistency theorem. A completed development would provide reusable definitions for cost-based decision losses and a checked account of the distributional assumptions needed for uniqueness. The published oracle predicate is already available on the platform; the two losses, risks, and distributional predicates are introduced here.
The SPO loss may jump when a predicted cost admits more than one optimal decision. Its definition takes the maximum realized cost over that whole decision set. Consequently, showing that a prediction selects one mean-optimal decision does not by itself control the SPO loss; Proposition 5's converse requires a singleton set. The surrogate is convex but generally not differentiable, because the support function of need not be differentiable. Establishing the unique population minimizer also depends on how the cost law covers the space: absolute continuity by itself permits a bounded-support law for which nearby predictions tie. These are substantive issues in moving from the single-cost-law statements to an almost-sure claim about measurable predictors Elmachtoub and Grigas, 2020, §4 and Appendix B.
The code represents by EuclideanSpace ℝ (Fin d) and by its standard inner product. Every theorem assumes the paper's nonempty compact convex . Real infima and suprema encode the attained minima and maxima on . An oracle is an explicit parameter satisfying the published SPOBounds.Natarajan.IsOracle predicate; it is not given an extra measurability or tie-breaking assumption. The SPO loss is the paper's unambiguous Definition 2, which differs from the oracle-dependent loss in the published module.
Expected losses are extended nonnegative integrals, so an infinite risk remains infinite. Conditional costs are represented by a Markov kernel , and the joint law by . Integrability of costs makes the conditional and joint means finite. Central symmetry means equality of the conditional law with its reflection . Assumption 1.3, “continuous on all of ,” is pinned to absolute continuity with respect to Lebesgue measure and full support, meaning every nonempty open set has positive probability. This full-support condition is needed for Proposition 6(b)'s uniqueness claim: a continuous law confined to a small ball supplies a counterexample to the weaker reading.
The risks range over all measurable predictors, as display (12) requires. A Bochner integral for an arbitrary nonintegrable loss, a restricted hypothesis class, the oracle-dependent SPO loss of Definition 1, or absolute continuity without full support would change or trivialize the target. Contributions to the support-function, measurable-risk, and conditional-law infrastructure are useful beyond this mission; the seven numbered proposition parts provide its immediate formalization targets.
Nonlinear conjugate gradient methods minimize a smooth function using only function values, gradients and a handful of vectors of storage. That makes them a standard tool for large-scale unconstrained optimization, where quasi-Newton matrices do not fit in memory. Each method is fixed by a scalar , and the classical choices (Fletcher–Reeves, Polak–Ribière–Polyak, Hestenes–Stiefel) have been analysed by many authors. Their convergence proofs normally require the strong Wolfe line search, and often a bounded level set. Many other unconstrained methods, by contrast, are proved convergent under the weaker standard Wolfe conditions.
In 1999 Y. H. Dai and Y. Yuan (SIAM J. Optim. 10 (1999) 177–182) proposed a new formula,
the numerator of Fletcher–Reeves over the denominator of Hestenes–Stiefel. They proved that the resulting method converges whenever every step satisfies the standard Wolfe conditions, under assumptions on that do not include a bounded level set. The method is now known as the Dai–Yuan method.
Timeline.
Write , , , . The inner product of is and the Euclidean norm. Fix line-search constants .
A step along a direction from is a standard Wolfe step if
and a strong Wolfe step if (1.7) holds together with (1.8).
Algorithm 2.1 starts at with and stops if . At iteration it picks a standard Wolfe step , sets , stops if , and otherwise sets
Assumption 3.1 at requires three things. First, is bounded below on . Second, is continuously differentiable on a neighbourhood of the level set . Third, there is with
In the Lean development these objects are levelSet, Assumption31 f x1 N L, StdWolfe, StrongWolfe, betaDY, IsDYIteration, IsDYRun, IsDYRunStrong, IsDescentWolfeMethod and LiminfGradZero, all in DaiYuanCG.Conv.Setting.
Under Assumption 3.1 at , a run of Algorithm 2.1 either terminates at a stationary point or satisfies
The goal is the non-terminating branch: for every implies (3.7).
A companion item, not a milestone, states §4's observation (p. 181): under strong Wolfe steps, and .
The result. Theorem 3.3 answers the question posed in §1 of the paper, whether some conjugate gradient method converges under the standard Wolfe conditions, and it does so without a bounded level set. Weakening the line search matters in practice: a standard Wolfe step is easier to find than a strong one, and the convergence theory now matches what quasi-Newton codes already had. The descent property (3.9) holds at every iteration without any restriction on other than .
Formalizing it. The theorem has a complete published proof; nothing here is open. To our knowledge neither the theorem nor the Zoutendijk condition under these hypotheses has a machine-checked proof. The mission produces three things: a formal Wolfe line-search vocabulary over EuclideanSpace; a Zoutendijk lemma whose assumptions are local to a neighbourhood of the level set, so other descent methods can reuse it; and the Dai–Yuan convergence proof itself.
The algebra of (2.5)–(3.17) is short. The analytic difficulty is in Lemma 3.2. The Lipschitz bound (3.1) applies only on , so it cannot be applied to an arbitrary step until the iterates are known to lie there. The finite decrease at each step must also control an infinite series, which is why the global lower bound on matters. A global Lipschitz constant or a bounded level set would simplify this issue. Both are assumptions the paper does not make, and §4 points out that avoiding the bounded level set is part of the result.
A second point is that is only well defined because (1.10) gives once is a descent direction. Descent of in turn depends on the value of through (2.5), so these properties depend on each other across iterations.
EuclideanSpace ℝ (Fin n) and is Mathlib's gradient f x. All sequences are maps ℕ → _ indexed from ; index is unconstrained and never used.Summable or ¬ Summable of the terms shifted to start at .A seller with distinct items faces consumers, each of whom wants at most one item. Choosing item prices to maximise revenue in this setting is the unit-demand envy-free pricing problem, introduced by Rusmevichientong and studied in algorithmic game theory and revenue management since the mid-2000s. Optimal prices are hard to compute in general, so the guarantees of simple pricing rules matter. The simplest such rule is uniform pricing: put one price on every item and choose to maximise revenue.
Aggarwal, Feder, Motwani and Zhu (ICALP 2004) and Guruswami, Hartline, Karlin, Kempe, Kenyon and McSherry (SODA 2005) analysed uniform pricing; in the min-buying model it recovers a fraction of the optimum, a bound Berbeglia and Joret attribute to Aggarwal et al. Berbeglia and Joret (arXiv:1606.01371, Algorithmica 2020) observed that the min-buying problem is a special case of assortment optimisation under a regular discrete choice model, and that uniform pricing then coincides with the revenue-ordered assortments heuristic. Their general guarantee for that heuristic yields a second bound for uniform pricing, in terms of the spread of the valuations rather than the number of consumers. This mission formalizes that bound (Corollary 4.7) together with the reduction it rests on (Theorem 4.6).
Unit-demand min-pricing (). There are items and consumers , . Consumer is interested in a set and has a valuation . Given a price assignment , consumer buys a cheapest item of if its price is at most , and nothing otherwise. The seller's revenue is
the optimum is , and uniform pricing earns . Write and for the extreme valuations.
Regular choice models. A finite product set carries choice probabilities for , , with no-purchase probability . The model is regular if (i) all probabilities are nonnegative, (ii) for , (iii) , and (iv) for and every . With revenues , an assortment earns and . If are the distinct revenues and , revenue-ordered assortments earn .
The reduction. From a instance the paper builds , , and , where spreads probability one over the set of pairs with , and minimal among the pairs of whose item lies in .
The bound is the paper's "approximates the optimum revenue to within a factor of , ", stated in product form.
The corollary gives a uniform-pricing guarantee that is independent of the number of consumers and items: when valuations lie within a factor of each other, a single price recovers a fraction of the optimum, which improves on whenever . More broadly, Theorem 4.6 places inside the class of regular choice models, so every guarantee proved for revenue-ordered assortments under regularity transfers to uniform pricing.
All results here are proved in the paper. Nothing in this mission is formalized elsewhere as far as a search of the platform shows: there is no regular choice model, no problem and no revenue-ordered guarantee on Prove2Me. The mission produces the reduction as reusable infrastructure, a machine-checked version of the paper's Lemma 4.5 (whose appendix proof is an informal repair argument), and the first formal guarantee for uniform pricing.
The reduction is where the work sits. Regularity hinges on the no-purchase case of axiom (iv): enlarging an assortment can only make nonempty, never empty, and this must be checked for the specific sets whose definition depends on the whole of . The revenue identities require tracking the minimum over of a price function obtained from an assortment, including items absent from , which receive the paper's "" price. Lemma 4.5 is needed to make the optimum of the uncountable pricing problem coincide with that of a finite assortment problem, and the statement is about a supremum over a continuum of price vectors whose attainment is not obvious. Theorem 3.2 has to relate the optimum to threshold sets of an arbitrary regular model, where products may share revenues and the optimal assortment need not be a threshold set.
The naive route of comparing uniform pricing to the optimum directly, consumer by consumer, does not give a bound in terms of ; the reduction to a regular model is what supplies it.
X and M, with Nonempty M (). Valuations satisfy as a field of the instance; the paper says "non-negative", but its reduction () and its ratio need positivity.Finset C; RO is a maximum over the threshold sets only. Distinct revenues are sorted 0-based (Fin k), with handled as a separate case.Real.log applied to ratios .A retailer with a large catalogue but a limited display (a web page, a shelf, a search result) must decide which assortment of products to show each arriving customer. Customers choose among the displayed products or leave without buying, and the retailer does not know their preferences in advance; it learns them only from the purchases it observes. This is the MNL-Bandit problem of Agrawal, Avadhanula, Goyal and Zeevi (arXiv:1706.03880v2; Operations Research 67(5), 2019), in which customer choices follow the multinomial logit model, the workhorse of revenue management and marketing.
The same paper gives an epoch-based upper-confidence-bound policy whose regret is at most of order (its Theorem 1). This mission formalizes the matching lower bound, the paper's Theorem 2: under a constraint that at most products be displayed, no policy can have regret smaller than order on every instance. Lower bounds of this kind are what certify that an algorithm is near-optimal rather than merely good.
Timeline. The square-root lower bound for -armed bandits goes back to Auer, Cesa-Bianchi, Freund and Schapire (2002), presented in the survey of Bubeck and Cesa-Bianchi (arXiv:1204.5721, 2012). Rusmevichientong, Shen and Shmoys (2010) and Sauré and Zeevi (2013) minimized regret under MNL choice with explore-then-exploit policies, obtaining and bounds for instances whose best and second-best assortments are well separated. Agrawal et al. (2017–2019) proved the instance-independent lower bound formalized here; Chen and Wang (2017) later obtained when .
There are products. An instance consists of a no-purchase weight , attraction parameters with , and revenues . At each period the seller offers an assortment and observes a choice , where means no purchase. Under the multinomial logit (MNL) model,
and choices are independent across periods given the offered sets. The expected revenue of is .
A policy chooses from the past assortments and choices, possibly at random. It satisfies the -cardinality constraint if always. Its regret over periods is
where maximizes over assortments of at most products.
A randomized instance is a probability distribution over instances with common known revenues and a common no-purchase weight; the regret against it is averaged over the hidden attraction parameters, the choices and the policy's randomization.
There is an absolute constant such that for all , and there is a finitely supported randomized instance, chosen before the policy, such that every policy respecting the -cardinality constraint satisfies
The constant is not fixed; any positive value suffices.
The paper proves Theorem 2 in two cases.
Items 1–3 serve the case , which the paper reduces to a multi-armed bandit through the instance of Definition 5.2 ( products in groups of , one hidden group with larger attraction). Items 4–5 serve the case through the two-point instance of Definition E.1.
The theorem shows that the growth of regret in assortment learning cannot be improved, and that the dependence on the number of products is polynomial: when the display size is fixed, the UCB policy of the same paper is optimal up to logarithmic factors (Remark 4). It separates what learning under the MNL model costs from what the combinatorics of the assortment adds, and the reduction it uses, simulating an assortment algorithm inside a bandit algorithm, is reusable for other choice-model bandits.
The result is proved in the paper, with its proof in Appendix E. To our knowledge neither the theorem nor its lemmas have been machine-checked. A formal proof has to repair several printed slips: Lemma 5.1's hypotheses do not exclude close to , where the bound fails; the proof of Lemma E.2 uses a form of Pinsker's inequality with a wrong constant; Lemma E.1 states one direction of the divergence and computes the other; and the constants of the case do not match. The formal statements here carry the corrected hypotheses, each disclosed in its note.
The obvious argument fails at the reduction. The bandit lower bound is a statement about algorithms that pull one arm per round, while an assortment policy offers products at once and sees a choice among them. Transferring the bound requires simulating MNL feedback from Bernoulli coins (Algorithm 2 of the paper), whose loop has a random length, and then relating the regret of the simulated assortment algorithm over a random number of calls to the bandit regret over pulls. The paper does this in expectation, and the constants have to be tracked through the random horizon.
A second difficulty is that the lower bound must hold for every policy, including randomized ones, against a single randomized instance fixed in advance. Bounding the regret of each deterministic policy separately is not enough unless the instance does not depend on the policy, which the statement requires. The change-of-measure steps (Lemmas E.2 and E.5) need a chain rule for the divergence between laws of adaptively generated histories.
Products, periods and arms are 0-based (Fin n); a choice is Option (Fin n) with none the no-purchase alternative. Histories have finite length , laws of histories are explicit products of policy weights and MNL (or Bernoulli) probabilities, and every expectation is a finite sum, so no measurability or integrability side conditions arise. The no-purchase weight is explicit (Definition 5.2 has ). is a maximum over the finite, nonempty family .
Policies are behavioural: at every history they give a probability vector over assortments, which by Kuhn's theorem covers the paper's admissible policies with external randomization. The randomized instance is a finite list of instances with nonnegative weights summing to one; every support point has the same revenues and no-purchase weight, which are known to the seller. The quantifiers are in the paper's order: the constant first, then , then the randomized instance, then every policy. A formalization with the policy quantified before the instance, with allowed, with varying known revenues across hidden support points, or with only deterministic policies, would be weaker and is ruled out.
Hypotheses added to the printed statements: and in Theorem 2 (the claim fails for and ); , , in Lemma E.1; , , in Lemma E.2; , , in Lemma 5.1. Lemmas E.4 and E.5 use Definition E.1's , with and so the instance is defined. Lemma E.5 is stated, as in its proof, for deterministic policies.
The development reuses three published definitions: the MNL revenue ChoiceCDLP.MNL.mnlObjective, the Bernoulli divergence RegretBandits.Stochastic.klBern, and the discrete Kullback–Leibler divergence FoundationsRL.GeneralDM.klDivDiscrete (valued in ). Proved platform results useful to solvers include Pinsker's inequality (BanditAlgorithm.pinsker_inequality_total_variation), the Bernoulli bound (BanditAlgorithm.bernoulli_relative_entropy_le_sq_div_of_add_le_one) and a divergence decomposition for bandits. A chain rule for the divergence of finite adaptive histories, and a formal version of the simulation of Algorithm 2, would be reusable beyond this mission; both are welcome as supporting lemmas.
Grover's algorithm (Grover 1996) finds a marked item among with queries, a quadratic speed-up over any classical algorithm. Whether quantum computers can do substantially better on search, and so solve NP-type problems by brute force in polynomial time, was settled in the negative by Bennett, Bernstein, Brassard and Vazirani (arXiv:quant-ph/9701001, SIAM J. Comput. 26(5), 1997): relative to a random oracle, a quantum algorithm needs queries to decide whether a string has a preimage. The bound matches Grover's algorithm up to a constant factor, and its hybrid argument is one of the two standard lower-bound methods of the field, together with the polynomial method (Beals et al. 1998) and the adversary method (Ambainis 2000).
Timeline:
A -query algorithm acts on vectors , where is the set of query strings, the set of answers (an additive group) and a finite workspace. A basis configuration with is querying ; is not querying. For an oracle the oracle operator is
The algorithm consists of a unit vector , unitaries that do not depend on the oracle, and a set of accepting configurations. With oracle its states are ; the acceptance probability is the squared norm of the accepting part of . The query magnitude of in is (Definition 3.2). The algorithm decides a property if it accepts with probability at least when the property holds and at most when it fails.
In the main theorem with bitwise addition, and the oracle is a uniformly random function . The question is whether belongs to .
The constant is existential, matching the theorem's hypothesis ; and do not depend on the workspace or the algorithm.
The theorem shows that the quadratic speed-up of Grover's algorithm cannot be improved for unstructured search, and that relative to a random oracle ; any quantum algorithm for NP-complete problems must use the structure of the problem. Theorem 3.3 and Corollary 3.4 isolate the constraint unitary evolution places on "quantum parallelism" and are reused across quantum lower bounds, including the permutation bound of the companion mission (Theorem 3.6).
The results are proved on paper and, to our knowledge, have no machine-checked proof. The mission produces a formal query model with an XOR oracle, a formal hybrid argument, and the lower bound with its constants checked. Two printed bounds are wrong by constant factors (below); the formal statements carry the corrected constants, and a formal proof settles them. Grover's matching upper bound is on the platform as Grover.search_succeeds_bounded, for a phase oracle and one fixed algorithm.
The obvious argument — each query reveals one bit about where the preimage is, so queries are needed — fails for quantum algorithms, which query all strings in superposition at once. The difficulty is to bound how much a superposition of queries can learn, which requires controlling the accumulated effect of small changes across unitary steps, and then converting a bound on states into a statement about the probability of failure over random oracles, where the set of sensitive strings depends on the oracle.
The paper's oracle quantum Turing machines are replaced by the query model above, the model its proofs use. Every oracle QTM running steps is a -query algorithm: oracle answers on lengths other than are fixed and absorbed into the unitaries, as the proof fixes them, and the input is absorbed into . Queries return the full value ; one Boolean query is two full-value queries, so the goal implies the Boolean-oracle bound with halved. Strings are Fin n → ZMod 2; states are EuclideanSpace ℂ (Option X × R × W); probabilities over oracles are counting fractions over all functions; total variation distance is the paper's without the factor .
Corrections: Theorem 3.3 is printed with conclusion , which fails (one query string, , distance at ; machine-checked); the true bound is . Corollary 3.4 is printed with , which fails (16 strings, , ); the true bound is . The printed constant in the proof of Theorem 3.5 does not support the step even with the paper's own count; the goal states an existential constant, and works with the corrected Corollary 3.4. The closing probability- argument over countably many machines and the class statement about are not formalized.
A formalization in which algorithms query at every step on every branch (no sector), only one side of the bounded-error condition is tested, or the probability is taken over a set of oracles that excludes the hard instances, proves a weaker theorem and is ruled out by these definitions.
Needed infrastructure: norms of finite-dimensional complex vectors, unitaries as linear isometry equivalences, finite counting of functions. The query model and the hybrid argument are reusable for any quantum query lower bound.
A convention is a pattern of behaviour that is customary because everyone expects everyone else to follow it: driving on the right, or which party yields at a narrow bridge. Peyton Young's The Evolution of Conventions (Econometrica 61 (1993) 57–84) asks how such a pattern can emerge from decentralized play. The players have limited memory and limited information, and nobody coordinates them. The paper's model, adaptive play, is now a standard dynamic of learning in games. It is the starting point of the stochastic-stability theory of equilibrium selection (Foster and Young 1990; Kandori, Mailath and Rob 1993), which builds on the perturbation theory of Freidlin and Wentzell (1984).
This mission covers the first half of the paper: §3 (the model) and §4 (convergence when the players make no mistakes). Before mistakes can be added and stochastically stable conventions selected, the unperturbed process must be shown to settle at all. Theorem 1 gives the condition under which it does.
Let be a game with finitely many players , a finite nonempty strategy set for each player, and payoffs for strategy tuples . Write for with player 's strategy replaced by .
If is weakly acyclic and , then for every best-reply distribution and every initial state ,
Theorem 1 identifies a class of games, the weakly acyclic ones, in which boundedly rational players who best-reply to small random samples of the past almost surely lock in to a strict pure equilibrium. The paper's examples of weakly acyclic games (p. 63) are pure coordination games and games with common interests in which no two strategy tuples are payoff equivalent. Absorption is in behaviour, not just in empirical frequencies. Example 2 shows that this fails for fictitious-play-like complete sampling, so the sampling ratio is a real ingredient. The absorbing states identified in the first milestone are the states among which the stochastic-stability analysis of the paper's later sections selects.
The result is proved in the paper. To the best of our knowledge no machine-checked version exists. The mission asks for a formal proof of Theorem 1 and its milestones for an arbitrary best-reply distribution. That generality is the paper's own: non-uniform sampling is explicitly allowed. A formal proof also pins down the memory bookkeeping in the paper's proof (look-backs of , and periods), which the text checks only in words.
Adaptive play is a finite Markov chain. The obvious route through the generic theory of absorbing chains requires showing that a convention is reachable from every state, and that is where the argument becomes delicate. A best-reply path in the game cannot be followed directly: each player only sees a random sample, and the players who are not moving must keep playing their old strategies. The proof gets around this by having the non-moving players keep sampling older parts of the history, so those parts must still be in memory. This is what forces the bound . A uniform, state-independent constant is then needed to turn reachability into almost-sure convergence.
Players form a finite type ι, strategies a family of finite nonempty types S i, and payoffs u : ι → (∀ i, S i) → ℝ. A state is Fin m → ∀ i, S i with position 0 the oldest play. A best-reply distribution is any p : ∀ i, H → S i → ℝ with the stated support. All statements quantify over every such p. Adaptive play is a Matrix H H ℝ, and "converges almost surely to a convention" is stated through matrix powers. That is equivalent to almost-sure absorption because conventions are absorbing. The condition is in ℕ. is an sInf on ℕ that is never empty under weak acyclicity.
The display (1) on p. 62 reads "the right-most element of ". The formalization uses the right-most element of the successor , the only reading under which the rule is meaningful.
The goal cannot be satisfied trivially. The sampling law is not fixed, the conclusion is a limit equal to from every initial state (not "with positive probability" or "along some path"), and the hypotheses are jointly satisfiable, for example by a coordination game with uniform sampling. A best reply to a sample uses the joint empirical distribution of the sampled plays, not independent marginals.
A complete development needs elementary Markov-chain facts about matrix powers and absorbing sets, plus combinatorics of shifted histories. These parts are reusable for any finite-memory learning dynamic. Proofs of individual milestones are welcome independently.
Related platform work: stochastic fictitious play in potential games (StochFictPlay.*, Hofbauer–Sandholm 2002) and calibrated learning to correlated equilibrium (CalibratedCE.*, Foster–Vohra 1997) formalize other learning dynamics. The perturbed process and the selection of risk-dominant conventions are the subject of the sibling missions The Evolution of Conventions II and III.
A retailer of style goods — seasonal clothing, newspapers, anything that loses most of its value when the selling period ends — must decide before the season how many units to stock, knowing demand only as a probability distribution. Units left over are liquidated at a loss; units short are sales forgone. This single-period trade-off is the newsvendor problem, and its solution, the critical-fractile rule, is one of the first results of stochastic inventory theory.
In practice the retailer also sets the price, and the price moves the demand distribution. T. M. Whitin's 1955 paper Inventory Control and Price Theory (DOI 10.1287/mnsc.2.1.61) is one of the first to put the two decisions into one model. Its Section 3 restates the critical fractile for a given price, then lets the demand distribution depend on the unit profit and asks for the unit profit and stock that jointly maximize expected profit. For one explicit family of demand laws it solves the problem in closed form. This joint price-setting newsvendor problem later grew into a large literature (Mills 1959, Karlin and Carr 1962, and the survey of Petruzzi and Dada 1999), which cites Whitin's model as its starting point.
There is one selling period. Stock is on hand at its start. Each unit sold earns the unit profit ; each unit left over at the close is liquidated at the unit liquidation loss .
Demand depends on the unit profit through its mean. The mean demand is the linear function
where is the unit profit at which demand falls to zero and is the reciprocal of the slope of the line relating unit profit and amount demanded. Demand decreases in , so , and the admissible unit profits are . At unit profit , demand has the rectangular (uniform) distribution on .
The expected marginal profit of the -th unit is , the probability that it sells weighted by the unit profit, and the expected marginal loss is , the probability that it does not sell weighted by the liquidation loss. The expected profit of stocking units at unit profit is the area between them,
which is the expected profit on sales minus the expected liquidation loss. The equilibrium stock is
With
one has , and for all and all
with equality only at . The formula for involves only and : the optimal unit profit is independent of the demand slope .
SupplyChainTheory.chain_optimal_fractile and enters as a reference.The goal is a complete closed-form solution of a joint pricing-and-stocking problem under uncertainty: one price and one stock level, explicitly, with a proof that no other pair does as well. The independence of the optimal unit profit from says that, in this family, the scale of the market does not affect the optimal margin; only the ratio of the zero-demand margin to the liquidation loss does. Footnote 7 relates the optimum to the classical monopoly rule (unit elasticity) in the limit of a negligible liquidation loss.
Whitin's derivation is calculus on closed forms and was never stated as a theorem with hypotheses. He calls the stationary point of (15) "the optimal " without checking that it is a maximum, that it is global, or that the stock beyond the support of demand cannot do better. The formalization fixes all three: the goal is a statement of global, unique optimality over the whole admissible region. No machine-checked proof of this result, of the price-setting newsvendor, or of the uniform-demand newsvendor exists on the platform; the general critical-fractile rule (8) is the only part of Section 3 already proved there.
The expected profit is defined from the demand law, so the closed forms (11) and (13) must be derived from the uniform distribution — probabilities of half-lines under a conditioned Lebesgue measure, and an interval integral of the resulting piecewise-linear functions. They hold only on the support of demand; beyond the marginal profit is and the marginal loss is , and the global statement must cover that region too.
The pricing step is where the paper is loose. Setting the derivative of (14) to zero gives a quadratic with two real roots, and a stationary point of a function on an open interval need not be its maximum. The goal asks for the global maximum over and its uniqueness, and asks that it be the global maximum of the joint problem, not only of the reduced function .
All quantities are real numbers; stock is continuous, as in the paper's calculus. Mean demand is meanDemand k P₀ P = k * (P - P₀) and the paper's sign convention is kept: is a hypothesis of every statement, as are and (or where is not fixed). The demand law is ProbabilityTheory.cond volume (Set.Icc 0 (2 * μ)); and use and ; is an interval integral defined for every .
The paper's loose phrases are read as follows. "Equation (9) may be solved for " becomes uniqueness of the root of on ; "the equilibrium value of " becomes the unique maximizer of over ; "differentiating (14)" becomes a HasDerivAt statement with the explicit derivative for , together with the equivalence with (15); "solving (15) gives the optimal " becomes the goal's joint global maximum with equality case; "independent of " is the shape of the formula for ; "as becomes large relative to , the optimal elasticity approaches unity" becomes a limit as with fixed.
Defining by the closed form (13) instead of from the demand law would make milestones (11) and (13) tautologies and would change the model beyond the support of demand; this formalization rules that out. The paper's goodwill loss belongs to the fixed-price model of (8) and does not appear in .
A complete development needs the uniform distribution's tail probabilities, interval integrals of piecewise-linear functions, and one-variable calculus for the quadratic and the cubic ; the uniform-law lemmas are reusable for any newsvendor problem with uniform demand. Proofs of the milestones, and alternative arguments for the goal, are welcome.
SupplyChainTheory.chain_optimal_fractile).Economic lot sizing asks how to meet a known sequence of demands while deciding when to set up production and how much to carry forward. It is a basic deterministic inventory problem: a setup has a fixed cost, production has a per-unit cost, and inventory may be held for later demand. Recomputing every possible next production period in the standard backward dynamic program takes a quadratic number of candidate comparisons. Wagelmans, Van Hoesel and Kolen use the geometry of cumulative-demand points to identify which candidates can affect the minimum. Their Section 2 gives the threshold rule targeted here. Wagelmans, Van Hoesel and Kolen (1992)
The paper notes independent related work by Aggarwal and Park and by Federgruen and Tzur. The published Prove2Me items for Federgruen and Tzur formalize a forward recursion and its minimal optimal predecessor lists. They address the same planning problem through different state variables; the backward value and efficient periods of this mission are new objects. Wagelmans, Van Hoesel and Kolen (1992), p. S145
A planning horizon consists of periods , with , and an extra terminal period . In period , a known demand must be met without backlogging. The final demand is positive, ; a trailing zero-demand period could otherwise be deleted. A production setup costs , and every unit produced in that period has a marginal cost . The sign of is unrestricted. Holding costs have been absorbed into these transformed marginal costs, as in Section 1 of the paper. Define the remaining demand , with . If production at covers demand until the next production period , then units are produced. Wagelmans, Van Hoesel and Kolen (1992), pp. S146–S147
The backward value starts at and follows Equation (1). At positive demand, it minimizes over . When , skipping setup and using is an additional choice. The paper identifies with the optimal cost from onward using the cited zero-inventory property. This mission takes Equation (1) as the definition of ; it does not formalize the separate equivalence with the original production-plan formulations. Wagelmans, Van Hoesel and Kolen (1992), p. S147
For a fixed , plot the finite points for . Their lower convex envelope is a piecewise linear graph. Its endpoints and places where its slope changes are breakpoints; the corresponding period indexes form the efficient set . Write for the next larger index in . The consecutive-point ratio is . These objects have no optimization over production policies hidden in their definitions. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150
Proposition 1 says every candidate outside can be removed without changing the minimum:
The endpoint and slope claims establish the geometry used in this reduction. Proposition 2 compares neighboring efficient periods using and . Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S149
The selected period is the first efficient index whose ratio falls below the current marginal cost, with the terminal period as fallback:
The goal asserts that the full candidate minimum is attained there and that the algorithm's resulting assignment equals :
This states the mathematical choice and value; it does not assert a time bound. Wagelmans, Van Hoesel and Kolen (1992), pp. S149–S150
The result reduces a finite dynamic-programming minimum to the vertices of a lower envelope and gives an explicit threshold for choosing a minimizing vertex. It explains which future production period the backward recursion may select even when marginal costs are negative or some intermediate demands are zero. The paper uses ordered slopes to implement the selection efficiently; a solver proving the statements here establishes the mathematical correctness of that selection independently of a particular list representation. Wagelmans, Van Hoesel and Kolen (1992), pp. S148–S150
The paper's result is proved in print. The Lean statements are open proof obligations in this proposal. A complete development would add reusable finite lower-envelope facts, including vertex dominance and the order of adjacent slopes, as well as a machine-checked treatment of the zero-demand tie convention. The previously published forward-algorithm items do not supply these backward-recursion facts.
A candidate point can have a smaller value than a neighboring point yet still fail to minimize for a given . Comparing raw values alone therefore cannot identify the selected period. The lower envelope must retain exactly the points that can support a line of slope , and their consecutive ratios must be ordered. Zero demand creates repeated abscissae; without a representative rule, a ratio may have denominator zero and the successor is ambiguous. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150
Periods are natural numbers starting at ; is the terminal sentinel. Demands, setup costs, marginal costs and values are real numbers. Finite minima use attained Finset.inf', with nonempty domains. The effective score omits the common setup cost . No sign restriction is imposed on . The efficient set is determined by a finite chord test for lower-envelope vertices: points on a chord are excluded, and at identical abscissa and height the earliest period is retained. This makes explicit the paper's zero-demand replacement convention on p. S150. The successor is used only on nonsentinel efficient periods; there its denominator is positive. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150
The algorithm's printed Iterations use where is required; the Lean statement uses , matching the preceding display and the numerical table. The zero-demand branch explicitly includes skipping setup. The selector is the ratio-threshold rule, rather than an argmin, and the efficient set is the actual lower-envelope vertex set rather than all periods. A finite zero-demand example and Tables I–II are used as verification data. The paper's bound, the binary-search implementation, the amortized list updates, the Wagner–Whitin specialization and the final production-plan construction are outside this mission: they require additional algorithm-state and cost-model statements. Wagelmans, Van Hoesel and Kolen (1992), pp. S149–S152
Inventory calculations often take the selling price as fixed, while price calculations often treat the cost of supplying demand as independent of the order policy. Whitin's 1955 model connects the two decisions in one annual-profit calculation. A merchant chooses both the price charged to customers and the size of each replenishment order. Changing the price changes annual demand; changing demand changes the number of orders, inventory carrying cost, and therefore the economic lot size. This makes the selling price and the inventory decision parts of the same optimization problem. Whitin's paper gives a compact example in which the connection can be written down explicitly.
The mission concentrates on Section 2, the stationary-demand model for a stable item. Section 3 of the paper studies style goods under uncertain sales and belongs to a separate mission. The result here concerns a deterministic annual demand curve and continuous order quantities, so a solver can focus on the interaction between a classical economic order quantity calculation and a price first-order condition.
The price is a real number . Annual demand is the linear function , where and are given real constants. A feasible price has . The paper does not require in its displayed model, so the formal statements leave the slope unrestricted. Negative is the economically usual decreasing-demand case; in other regimes a joint maximum may simply fail to exist.
The merchant pays a fixed setup cost whenever an order is placed. The purchase cost per unit is , and the annual carrying charge for one unit kept in stock is , where is a carrying-rate factor. If units are ordered each time, average stock is and the annual number of orders is . A per-unit operating cost is incurred on annual demand, and is an annual fixed cost. The resulting total variable cost and two-variable annual profit are
Only pairs with and are feasible. For a fixed demand level, the economic lot size is . Substituting it into profit gives Whitin's reduced profit
The paper uses for annual profit in this section. The Lean development calls the two-variable function profit and the function after optimizing reducedProfit.
The first target is the unique lot-size minimum in Eq. (3), followed by its value in Eq. (4):
Equality in the inequality holds only at . The next target is the necessary stationarity condition in Eqs. (6)–(7): when and the derivative of at is zero,
The goal joins these steps at a global joint maximum. If a feasible pair maximizes over all feasible price and lot-size pairs, then and satisfies the cubic. The goal is an implication about any joint maximizer; it does not assert that one exists for every demand curve. The cubic is a necessary condition only. Its algebraic roots may include prices that fail the original first-order equation or fail to maximize profit.
The result gives a concrete relation between a price chosen to maximize annual profit and the ordering cost and carrying charge of the inventory system. The lot-size formula alone optimizes cost at a fixed demand rate. The cubic makes the demand response to price and the resulting inventory cost visible in the price condition. It also specifies what can be inferred from the calculation: an optimal price must satisfy the equation, while selecting an optimum from candidate roots remains a separate question.
The paper already supplies the mathematical result. The formalization task is to represent the joint optimization and verify its necessary conditions in Lean, together with the cost identity on which the reduced-profit expression rests. The published Prove2Me definition InventoryControl_eoq already provides the classical EOQ cost and square-root quantity; this mission uses its cost function and adds Whitin's demand curve and profit. Related inventory results for backorders and multilevel systems describe different models and do not replace the targets here.
At a fixed price, choosing the lot size involves both a term proportional to and one proportional to . The optimality statement needs a global inequality and a unique equality case, not merely the observation that a derivative vanishes. After substituting that quantity, the reduced profit contains a square root of the demand curve. Its derivative is meaningful on positive demand, and turning its stationarity equation into the displayed cubic loses information when an equation is squared. A proof therefore has to preserve the implication from optimality to the cubic without promoting all cubic roots to optima.
The model uses real prices, real demands, and real lot sizes; it does not round order quantities to integers. The hypotheses make explicit the positive cost and carrying-charge conventions of Section 2. Neither nor is assigned a sign, and no sign is imposed on or . The conditions and apply to every cost or profit comparison. They exclude Lean's total value for division by zero and the zero value assigned by Real.sqrt to a negative argument. The goal quantifies over every feasible pair in a joint maximum of the original profit, so optimizing is part of its content. Defining profit only by the reduced formula would erase that claim.
The definitions comprise linear demand, total variable cost, two-variable profit, and reduced profit. The classical EOQ cost comes from the existing InventoryControl_eoq definition; the model-specific layer is small and can be reused in further work on pricing with inventory costs. The theorem targets welcome proofs of the global lot-size inequality, the minimized-cost identity, the stationary cubic, and their combination at a joint maximizer. The paper's quantity-discount footnote is outside this scope because it leaves the revised purchase and carrying-cost model unspecified.
Policy improvement is one of the two classical ways of solving a Markov decision problem: start from a policy, compute its return, and change the decision wherever another action looks better against that return. Howard (1960, Dynamic Programming and Markov Processes) introduced it for finite state and action spaces, and Blackwell (1965) proved it for discounted problems on Borel spaces. A related routine combines two given policies instead of improving one: at each state, follow whichever policy has the larger return there. Eaton and Zadeh (1962, J. Basic Eng. Ser. D 84, 23–29) proved that this combination of two stationary policies is at least as good as both in the negative case with finite state and action spaces (as credited on p. 889 of Strauch's paper).
Strauch's paper Negative Dynamic Programming (Ann. Math. Statist. 37 (1966) 871–890) treats the negative case: all one-stage returns are non-positive (costs) and there is no discounting. This case covers stochastic shortest-path and optimal-stopping problems with positive costs, where expected total returns may be and the contraction arguments of the discounted case are not available. Section 9 of the paper shows that both improvement routines remain valid there, for arbitrary randomized history-dependent policies on Borel spaces, and that they fail in the positive case (Examples 4.2 and 9.1 of the paper).
Timeline:
The state space and the action space are non-empty Borel sets. The law of motion is a probability kernel from to , and the return is a Borel function with whose one-step expectation is finite at every . There is no discounting ().
A policy chooses the -th action from a probability kernel that may depend on the whole history . The expected return from the initial state is
the sum of the expected one-stage returns. For a terminal reward that depends on the history , is the expected return of following for stages and then receiving .
Given two policies and , their continuation returns at a history are
the expected returns from stage on if , respectively , is used from on with its own kernels fed the full history. The switching policy uses on and on its complement. In Lean these objects are contReturn, IsSwitch, wmax (for ), InH (for ) and I, in the namespace NegativeDP.Switching.
For all policies , the switching rule defines a policy , and every such satisfies
With and the switching policy:
Theorem 9.2 (Howard): if then . Corollary 9.1: the switching theorem for Markov policies, comparing and at the current state. Corollary 9.2 (Eaton–Zadeh): for stationary , the rule where and elsewhere satisfies .
Theorem 9.3 yields an improvement step that needs only the returns of two policies, not an optimality equation or a value function. Its Markov and stationary forms give policy-combination results usable for stochastic shortest-path and positive-cost problems, and together with Theorem 9.2 they justify policy-iteration schemes in the negative case on general state spaces. Example 9.1 of the paper shows that no comparable routine exists in the positive case, so the sign assumption is essential.
The results are proved in the paper. No machine-checked version of any of them exists, for the negative case or on Borel spaces; the related items on Prove2Me treat finite or discounted models. This mission produces the statements in Lean over Blackwell's published model of history-dependent plans, a construction of continuation returns from an arbitrary history, and terminal rewards that depend on the whole history.
The argument of the discounted case, which passes to the limit through the vanishing tail , is not available: with the terminal term does not vanish, and returns may be . Comparing and at the current state only is not enough either: for history-dependent policies the continuation returns depend on the whole history, and the switching set must be shown to be Borel in the history before the switching rule is even a policy. The induction also requires integrating extended-real terminal rewards against the history law and identifying the integral of the one-step operator with the next-stage expected return.
DiscountedDP.Stationary.Plan (one Markov kernel per decision, on Hist S A n). Decisions are numbered from in Lean, so Lean's index is the paper's stage .EReal values computed as minus the lintegral of the loss ; Bochner integrals and toReal are never used, so a return of is not silently turned into . is the sum of stage expectations, equal to by monotone convergence.IsSwitch, not constructed. A statement "every switching policy satisfies the bound" would hold vacuously if no plan satisfied the rule; the goal therefore also asserts that a switching plan exists, which is the content of the paper's "define by". The same pattern is used in Corollaries 9.1 and 9.2 (the rule defines a measurable decision rule).Contributions welcome: measurability of continuation returns in the history (needed for the existence part), the identification of the history law with the continuation law from the initial state, and a Chapman–Kolmogorov identity for the continuation kernels. These are reusable in any development on history-dependent policies over Borel spaces.
School and university timetabling is one of the oldest applications of combinatorial optimization. In the class–teacher model, classes and teachers must be brought together for a prescribed number of lectures, each lecture occupies one period, and nobody can be in two places at once. With no further side constraints the model reduces to edge colouring of a bipartite multigraph and is solved exactly by König's theorem. Real instances, however, come with preassignments (a class and a teacher must meet at a fixed period) and unavailabilities (a teacher or a class cannot be scheduled at some periods). With these, deciding whether a daily timetable exists is NP-complete, as the paper records citing Even, Itai and Shamir (1976).
D. de Werra's invited review An introduction to timetabling (European Journal of Operational Research 19, 1985) surveys this landscape. In its §2.2 it isolates one restricted case that is easy: when every teacher is available during at most two periods, a limited backtracking method finds a timetable or proves that none exists (Proposition 2.4, attributed to [9], Even–Itai–Shamir). The Remark that follows recasts the procedure as a decision method for stable sets of half the vertices in graphs with a perfect matching, which is the 2-satisfiability problem in graph form.
There are classes , teachers and periods of one day. After removing the preassigned lectures, lectures of class with teacher remain; is exactly when class is available and not preassigned at period ; is exactly when teacher is available and not preassigned at period . A timetable (a solution of CT4) is a array with
A possible schedule of is the slice of a candidate array that satisfies the constraints involving alone. The conflict graph has one node per pair (teacher, possible schedule); two nodes are linked when they are different schedules of the same teacher or put the same class in the same period. When each teacher has exactly two schedules, they are written and , and in Lean the nodes are (j, true) and (j, false) of Fin n × Bool.
The limited backtracking works on such a graph. The implications of a set of chosen nodes form the least set containing such that whenever is in it and is linked to a node of another teacher, the other node of 's teacher is in it. A state is either , with the nodes fixed so far, or . From , for any teacher not yet fixed and any first choice of its node:
For every and every graph on in which and are linked for all :
All four clauses range over every run of the nondeterministic procedure.
Proposition 2.4 identifies a polynomial special case inside a scheduling problem that the paper cites as NP-complete in general (Even–Itai–Shamir [9]). The correctness of the procedure is what makes that special case tractable. Milestones 1 and 2 reduce the timetabling instance to a graph question, and the goal settles the graph question. Milestone 4 is the reason the method needs to undo only the last decision. It is the graph form of the autarky principle of 2-SAT solving: a closed, consistent partial assignment can always be kept. Milestone 5 extends the method from timetables to any graph with a perfect matching.
On the formal side, no machine-checked treatment of this reduction or of the backtracking argument exists on the platform; 2-SAT, unit propagation and autarky have no items there either. The statements are proved in the paper only in prose, and the propagation and autarky arguments are compressed into a few sentences. A formal proof makes the invariants explicit: what is closed, what is independent, and why a contradiction after a reversed decision is global.
Soundness of a successful run is an invariant argument. Soundness of failure is the hard part. The naive argument "both choices for lead to a contradiction, hence no timetable" is wrong in general backtracking, because an earlier decision might be at fault, and full backtracking would revisit it. The proof has to show that an earlier permanent decision never needs revisiting. This requires that the set of fixed nodes is closed under implications and independent, so that no unscheduled teacher is linked to it. This invariant must be maintained through both the keep and the reverse moves. Termination and progress are routine but must be stated: without them the correctness clauses hold for a procedure that never moves. On the CT4 side, the reduction must check that the class constraint with splits exactly into per-teacher availability and pairwise disjointness of schedules.
Fin m, Fin n, Fin p; variables are Bool.Step with one constructor for each of keep, reverse and fail, so the choice of teacher and of first schedule stays arbitrary.SimpleGraph, IsIndepSet, IsNIndepSet, Subgraph.IsPerfectMatching, Relation.ReflTransGen and Acc. The autarky lemma (Milestone 4) and the propagation lemma (Milestone 3) are reusable for any 2-SAT-type development. Proofs of the milestones, and a bridge from the CT4 instance to the abstract graph on Fin n × Bool in the exactly-two-schedules case, are welcome.A minimax theorem asserts that for a real function of two variables the order of optimization does not matter:
In game theory it says that a two-person zero-sum game has a value; in optimization it is the engine behind Lagrangian duality, robust optimization (exchanging the decision and the adversary) and distributionally robust and online-learning bounds, where a worst case over a family of distributions is exchanged with a minimization over decisions.
Most minimax theorems require linear structure: concave in and convex in on convex sets. K. Fan observed that a much weaker, purely order-theoretic condition suffices, which he called concavelike and convexlike, and which makes sense on sets with no linear structure at all. This is the setting needed when the strategy sets are, for instance, sets of stopping times, of measurable policies, or of combinatorial objects whose mixtures are only "dominated" by another member of the set.
Timeline:
Let and be arbitrary sets and a real-valued function; is the maximizing variable and the minimizing one.
In each definition the witness depends only on the two given points and on , never on the point of the other space. The two values compared are the extended reals
which may be . In the Lean development these are Concavelike f, Convexlike f, ConcaveConvexlike f, supInf f and infSup f in the namespace SionMinimax.KneserFan. The inequality always holds; the theorems assert the reverse.
If is a compact topological space, is concave-convexlike, and is upper semicontinuous for each , then
No structure on and no linear structure on are assumed.
The paper itself states that 4.2 is a special case of 4.1′, which in turn follows from the finite-dimensional minimax theorem. Sion's own minimax theorem (Theorem 3.4 and its Corollary) is already formalized on the platform as FamousTheorems.sion_minimax_theorem and is included in the mission as a reference item.
The Kneser–Fan theorem is the standard minimax theorem for settings without a natural linear structure. Its finite-reduction form (4.1, 4.1′) isolates the only place where topology enters: compactness and semicontinuity are used solely to replace (or ) by a finite set, after which the argument is finite-dimensional. Statements of this kind are used to exchange the order of optimization in robust and distributionally robust optimization, in statistical decision theory (existence of least favourable priors, Wald's complete-class theorems) and in learning theory, where the adversary's set is a space of distributions and the learner's set is a space of hypotheses with no convex parametrization.
The theorem is classical and fully proved in the literature. No machine-checked proof of it is known in Mathlib or on the platform: Mathlib contains Sion's quasi-concave-convex theorem (Topology/Sion.lean) and the platform has the bilinear and quasi-convex cases, but neither covers concavelike-convexlike functions, which are independent of quasi-concave-convex ones. This mission produces machine-checked versions of all four §4 statements in the extended reals, including the degenerate cases where values are infinite.
The obvious reduction, "replace by its convex hull and apply a linear minimax theorem", is unavailable: and are bare sets, so there is no convex hull and no mixed strategy to form. Concavelikeness only promises that a mixture of two strategies is dominated by some third strategy, and this has to be iterated to finite mixtures and combined with a separation argument in for a finite .
The second difficulty is bookkeeping: the minimax values live in , the threshold is real, and may be unbounded, so every step comparing a real with or must handle infinite values; a real-valued supremum would silently replace them by .
CompactSpace M; for 4.2′, carries one with CompactSpace N. No Hausdorff, metric or linear structure is assumed.UpperSemicontinuous (fun μ => f μ ν) (resp. LowerSemicontinuous (fun ν => f μ ν)) on the whole compact space.EReal-valued (⨆ μ, ⨅ ν, (f μ ν : EReal) and its dual); the threshold in 4.1, 4.1′ is a real number compared through the coercion; the finite sets are Finsets chosen after .Nonempty M ∨ Nonempty N. When all printed hypotheses hold vacuously (take or ), yet and , so the printed statements fail only in that corner. When exactly one of the sets is empty both sides coincide and that case is kept. No printed slip is corrected; the milestone texts are verbatim.EReal suprema of real-valued families; these are reusable for any minimax result without linear structure. Contributions proving the milestones independently, or deriving 4.1′ from the referenced Sion theorem by embedding into a simplex, are welcome.A fixed-time traffic signal is set by two numbers per phase: how long the green lasts and, through the other phase's green, how long the red lasts. Traffic engineers in the early 1950s set signals by Adams' formula, the shortest cycle that can clear the arriving traffic, on the working assumption that the shortest feasible cycle also gives the least delay. J. G. Wardrop's 1952 paper Some theoretical aspects of road traffic research (DOI 10.1680/ipeds.1952.11259), the paper that also introduced the two Wardrop principles of route choice, tested that assumption analytically for a two-phase signal with uniform arrivals. Appendix IV shows that the shortest cycle is optimal only under an explicit condition on the flows, and gives the optimal cycle when the condition fails. Its numerical example (p. 339) lengthens the cycle by 75 per cent and reduces the overall mean delay by 11 per cent, a case that arises when one phase serves a minor road.
The question was taken up by F. V. Webster's 1958 delay formula and optimum-cycle rule for random arrivals, which became the standard practice; the deterministic two-phase analysis here is its uniform-flow precursor.
A two-phase signal serves two streams. For phase :
The totals are , , and the cycle time . Vehicles do not accumulate indefinitely on phase when the green, less its lost time, can clear one cycle's arrivals: . Equality on both phases (both greens saturated) gives Adams' formula
The flow-weighted average delay at the intersection is
Appendix IV changes variables to the effective-red fractions and . With
one has , the no-accumulation conditions become and , and
The feasible region is . Its corner is the minimum cycle (12). The phases are labelled so that .
Put
For , and :
At , , so the second formula gives the minimum cycle. This boundary case belongs to the page's final “if this condition is not satisfied” clause.
Adams' formula (12) and the minimality of its cycle; the change of variables from (16) to ; and the translation into the original quantities: iff , iff , and the delay-minimizing cycle when .
The result gives a closed-form test for whether the minimum cycle is the delay-optimal cycle of a two-phase fixed-time signal with uniform flows, and the optimal cycle when it is not. It shows that the common assumption, shortest cycle equals best cycle, can fail, and identifies when: the test depends on the flow ratios and on which phase is the heavier one in the sense of . In the failing case the optimum keeps the minor phase saturated and lengthens only the major phase's green.
The result is proved on the page by a short calculus argument. It has not been machine-checked anywhere known to this mission. The formal work is to establish the global optimality claims behind the page's local reasoning, to pin down the hypotheses the page uses silently (positivity of flows and lost times, the capacity condition, the phase labelling), and to correct the printed slips listed under Formalization scope. The reparametrization and the original-quantity forms tie the abstract statement back to signal settings.
The page argues locally: at the corner both partial derivatives are negative, and "the only possible changes in and are reductions", so is a minimum. Negative partial derivatives at a corner of the region show that no small reduction helps; they do not by themselves exclude a better point far from the corner. The global claim needs a property of on the whole region , not just at one point. The second case has the same issue: the page locates a critical point on the edge and needs, in addition, that no interior or other boundary point does better. The algebra of the corner criterion is routine; the global minimality is the step that carries the content.
All quantities are real numbers. The objects are delayT lam mu x y , feasibleXY xi eta , cornerD , edgeRoot , the maps xiOf, etaOf, lamOf, muOf from the flows to , and avgDelay16, the right side of (16). Derivatives are stated with HasDerivAt on the one-variable sections of ; minimality is the explicit inequality for every .
Conventions and added hypotheses, each presupposed by the page:
The goal is stated in alone, which is all Appendix IV uses; the companions connect them to the flows.
Printed slips, corrected in the Lean and named in each item: for in the expression for (p. 359); the range "" for (p. 359); "" for in the original-quantity form of (p. 359); and "", "", "" for , , (p. 358).
Stating the goal as "the partial derivatives at are negative" would replace the theorem by its mechanism; the goal is minimality over the whole feasible region. Not covered: the delay formula (13) and its heuristic derivation in Appendix III, the approximation (14), and the rounded numerical example of p. 339.
Contributions are welcome on every milestone and companion. General facts about functions of the form on the half-plane are reusable beyond traffic signals.
Planning a road improvement requires an estimate of how traffic will redistribute over the routes affected. Because speed falls as flow rises, sending every vehicle along the route that is quickest today changes which route is quickest. J. G. Wardrop posed the question in its simplest setting in 1952: a given flow chooses among alternative routes between one origin and one destination, and the journey time on each route rises with the flow on it. He proposed two criteria for the resulting distribution. The first, equal journey times, became known as Wardrop's first principle or user equilibrium: "the journey times on all the routes actually used are equal, and less than those which would be experienced by a single vehicle on any unused route." It describes the state in which no driver can shorten their trip by switching routes, and it is the equilibrium notion behind traffic-assignment models and the theory of selfish routing.
Timeline:
There are routes, . Route has two positive constants: , its journey time when no additional traffic uses it, and , the additional flow at which its speed would drop to zero. When an additional flow uses route , its journey time is
This form comes from a linear speed/flow relation on each route. A feasible split of the total flow is a vector with and . A feasible split satisfies the equal-times criterion with common time when
Write for the routes whose empty-route time is below . In Lean these objects are routeTime b p i x, IsFeasible p Q q, IsEqualTimes b p Q q t and usedSet b t, all in the namespace WardropTraffic.EqualTimes.
For every , and , the split is feasible and satisfies the equal-times criterion with common time if and only if
This states which routes are used, the flow on each, and the relation between the total flow and the common journey time. The milestones are the steps of Wardrop's derivation:
If , there is exactly one pair satisfying the criterion. This formalizes the paper's closing sentence, that the solution is found "by picking out the value of which corresponds to the given ".
The result. For parallel routes with journey times (22), the equilibrium is explicit. The common time is the root of a single scalar equation (24), and the flows follow from by (23). The derivation also shows a threshold structure: a route is used if and only if its empty-route time is below the equilibrium time. Adding flow raises , and the routes enter the set in use one at a time, in increasing order of . This structure is what the paper's second criterion (minimum average time, the next mission of this series) is compared with.
Formalizing it. The result is classical and its proof is elementary; it has not been machine-checked. The platform has the existence of a Wardrop equilibrium on general networks for delay functions that are total, continuous and increasing on , with no closed form. That model excludes the vertical asymptote of (22) at and has no empty-route time . This mission adds the closed-form characterization for Wardrop's own model, both directions of it, and the existence and uniqueness of the split, including the corner cases that the printed criterion leaves open.
Each step is short. The difficulty is in the boundaries. The paper labels the routes so that and speaks of "the first routes", with . A faithful formal version has to say what happens at , at ties among the , at (no route is used), and at a route used near capacity. The printed criterion says "less than" for unused routes, yet the derivation's own case split allows equality. With the strict comparison, an equal-times split fails to exist at the values of where coincides with some . The companion's uniqueness requires : at every is a common time of the zero split. Existence requires a continuity and monotonicity argument for the right-hand side of (24) as a function of .
Fin D, and all quantities are real.The development needs only the definitions above and basic real analysis (the intermediate value theorem for the companion). The model of a finite family of parallel routes with hyperbolic journey times is reusable for the minimum-average-time criterion. Proofs of the milestones, of the goal and of the companion are welcome.
A firm that holds a single stock of a product often serves customers of different priority: military and civilian requisitions, contract and spot customers, emergency and routine orders for spare parts. When stock runs short, it must decide not only how much demand to satisfy but whose. Satisfying a low-priority order now may leave the firm unable to serve a high-priority order that arrives later in the same replenishment cycle. Inventory rationing asks for the optimal rule.
Veinott (Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13 (1965)) studied a model with demand classes, but fixed in advance the rule that a lower class is served only when every higher class has been served in full, and gave conditions on the costs under which that rule is optimal. Topkis (Management Science 15 (1968), 160–176) dropped the fixed rule and characterized the optimal rationing policy within a replenishment period. Theorem 1 of that paper is the target of this mission. It extends the author's earlier two-class analysis; the two-class case was later partly rediscovered by Evans and by Kaplan. Critical-level rationing policies of this kind are a standard object in the later literature on multi-class inventory systems.
A period between two replenishments is divided into intervals, indexed backwards: interval has intervals after it, so the period starts in interval and ends in interval . Demand comes in classes , with class the most important. At the start of interval the firm holds stock and faces the outstanding demand vector : the backlog carried in plus the new demand , whose law on has finite means. Demands of different intervals are independent.
The firm chooses the vector of demand left unsatisfied, with , so that units remain in stock, where . It pays the penalty and the holding cost . A fraction of the unsatisfied demand is carried into the next interval: , with meaning complete backlogging and lost sales. At the end of interval the salvage cost is charged. The standing assumptions are:
The minimal expected cost of the last intervals and its expectation satisfy
with .
For a class , with its unit vector, the critical rationing level is if is strictly decreasing on , and is the smallest minimizer of on otherwise. With , the rationing level policy leaves unsatisfied
In words: going down from class , it serves as much of each class as it can without letting the stock fall below that class's critical level.
Suppose for every . Then
In attack order:
A companion item states the paper's remark that with a linear ordering cost the optimal order is .
Theorem 1 reduces the -dimensional rationing decision in each interval to numbers, which are computed from one-dimensional convex minimizations. Under complete or no backlogging this is the structural result that the rest of the paper builds on: the monotonicity of the levels in time (Theorem 2), the reduction of the backlog case to a single-interval problem (Theorem 3), and the multi-period ordering policy (Theorem 4). The hypothesis on is sharp in the sense the paper shows: for an example on pp. 165–166 has no optimal policy of this form.
The theorem is proved in the paper, but no part of it is machine-checked. A formal development would contribute a reusable treatment of finite-horizon dynamic programs whose value function is defined by an infimum and an expectation over an orthant, with convexity and continuity propagated through the recursion. It would also contribute the comparative statics of critical-level policies.
The obvious argument proves optimality of the rationing level policy by induction from convexity alone. That is not enough. Convexity gives a one-dimensional problem in (by (6) and Lemma 4). But identifying its minimizer with the class-wise critical levels requires the marginal value of class- demand to be independent of the demand of the less important classes, which is part (c). Part (c) is false when , so the induction must carry (a), (b) and (c) together and use at every step. A second difficulty is analytic: is an infimum and an expectation, and before any structural argument starts the value functions must be shown to be finite, attained, continuous and integrable on the closed orthant (Lemma 2).
Fin n; the paper's class is index , so class is the largest index and (b) is Antitone. Intervals are natural numbers counted backwards, as in the paper. Vectors are Fin n → ℝ with the pointwise order.sInf), and by a Bochner integral against . Every statement about , is restricted to and (or ). Lemma 2's attainment and integrability conjuncts are what identify these values with the paper's.WithTop ℝ, with . They are specified by the predicate IsCriticalLevel: strictly decreasing for , smallest minimizer otherwise. They are never computed by a real sInf, which would give the junk value when no minimizer exists.Airline and hotel revenue management sells one perishable resource (seats on a flight, rooms on a night) through several fare products at different prices. The classical models of Littlewood (1972), Belobaba (1989) and Lee and Hersh (1993) assume independent demand: a customer who wants fare class either buys class or leaves, whatever else is on offer. Under that assumption the optimal booking policy is nested by fare order: at any time the firm opens a top segment of the fare ladder, and closes classes from the cheapest upwards as capacity becomes scarce.
Real customers substitute. If the cheap fare is closed, some buy up; if a mid-priced fare is open, some buy down. Talluri and van Ryzin (working paper 2001; published as Management Science 50(1), 2004) model this with a general discrete choice model: the firm chooses which set of fares to offer, and a customer buys product with probability . Their §3 asks when the fare-order nesting of the independent model survives under choice behaviour. They give a characterization (Theorem 2, the subject of mission 2 of this series) and verify it for two models: the independent demand model (Proposition 5) and the multinomial logit (MNL) model (Proposition 6). The MNL model is the standard choice model in travel demand forecasting and marketing (Ben-Akiva and Lerman, 1985), so Proposition 6 says that the fare-order structure airlines already implement remains optimal under the most widely used substitution model.
There are fare products with revenues . A choice model assigns to each offer set numbers with and for ; the remainder is the no-purchase probability. Write for the purchase probability and for the expected revenue.
The complete sets are , , with . A choice model has the nesting-by-fare-order property (Definition 4) if
In the single-resource dynamic program, for the marginal value of capacity, so condition 2 says that the optimal offer set is always a top segment of the fare ladder.
The MNL model with preference weights and no-purchase weight is
The independent model is for . A set is dominated (Definition 1) if some randomization over offer sets has no larger expected purchase probability and strictly larger expected revenue, or strictly smaller purchase probability and no smaller revenue.
This leaves the fares unrestricted: condition 2 quantifies over all ordered value vectors , so the goal holds for every fare ladder at once.
The result. Proposition 6 turns a structural question about an exponentially large dynamic program (the firm chooses among offer sets in every period) into the familiar one-dimensional policy of opening fares from the top. For MNL demand, the optimal control is described by protection levels, which is how airline reservation systems already operate; the paper's later remark (17) gives the opening condition for fare . Without it, a firm whose customers substitute according to MNL would have no guarantee that fare-ordered nesting is not leaving revenue on the table.
Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission produces a checked proof of Proposition 6, a checked sufficiency direction of Theorem 2 that applies to any choice model, and the independent-demand case (Proposition 5). The literal wording of Proposition 6 ("the only nondominated sets are the complete sets") is false when fares tie; the mission records the corrected statement under strictly decreasing fares.
The obvious approach compares an incomplete set directly with a single complete set, and it fails: under MNL, adding a fare changes every other fare's probability through the common denominator, so no single complete set need match 's purchase probability while selling at least as much of every high fare. A comparison through randomizations over complete sets is needed, and a weight that matches 's total purchase probability does not, for a general choice model, match the individual product probabilities as well. The final comparison must also hold for every ordered value vector , including vectors with negative entries, for which the empty set can be the only optimum.
Products are Fin n (index for fare ); a choice model is P : Finset (Fin n) → Fin n → ℝ with the published RevenueManagement.IsChoiceModel (nonnegativity, total at most one) plus SupportedOn P ( off , the model's convention on p. 5). is complete n k = {j | j.val < k} for ; the empty set counts as complete, and the mixture weights are indexed by . The page indexes complete sets as ; without , condition 2 fails for every model when all , where only is optimal. The order is Antitone x. The paper's weight is written , since λ is reserved in Lean.
Standing hypotheses and pins: MNL weights (); for the independent model and , so that it is a probability function; strictly decreasing fares StrictAnti r for the nondominated-set companion only, because with and the incomplete set is nondominated.
The goal is the full Definition 4 with both conditions; it may not be weakened to condition 1 alone, to condition 2 for nonnegative , or to a statement that assumes condition (ii) of Theorem 2 or the existence of . The "Moreover" sentence of Propositions 5 and 6 (nested allocation policies, Definition 3) is not formalized. Theorem 2's sufficiency half is restated here because draft items cannot import the drafts of mission 2; the definitions of complete sets and the property are shared verbatim with that mission.
Contributions welcome: proofs of the milestones, a general summation-by-parts lemma for majorized vectors (reusable beyond this mission), and the converse of Theorem 2 via Farkas' lemma.
A minimax theorem asserts that, for a function of two variables,
Such equalities are the basis of zero-sum game theory, of Lagrangian duality in optimization, of robust optimization, and of minimax lower bounds in statistics and online learning. Maurice Sion's 1958 paper On general minimax theorems proved the version most often cited today: and convex subsets of topological vector spaces, one of them compact, quasi-concave and upper semicontinuous in , quasi-convex and lower semicontinuous in .
Sion's theorem itself is already machine-checked: Mathlib's Sion.minimax proves it, following the elementary argument of Komiya (1988), and the platform holds it as FamousTheorems.sion_minimax_theorem. Sion's own proof is different. It runs through an open-cover form of the Knaster–Kuratowski–Mazurkiewicz (KKM) theorem, a Helly-type fact about points in low dimension, and a lemma about minimal finite covers (Lemma 3.3). That route has not been formalized. This mission formalizes its ingredients, with Lemma 3.3 as the goal.
Timeline:
Let be a real topological vector space: a real vector space with a topology for which addition and scalar multiplication are continuous. A set is convex if it contains the segment between any two of its points. The convex hull of a set is the smallest convex set containing it.
A real function on a convex set is quasi-concave on if every superlevel set is convex, and quasi-convex if every sublevel set is convex. It is upper semicontinuous (u.s.c.) on if every strict sublevel set is open in the topology inherits from ; lower semicontinuous (l.s.c.) is the mirror notion.
Let be a finite set, a real number, and a real function on . Say that has property P if for each there is a with , and that is minimal for P if no proper subset of has P.
An -dimensional simplex with vertices is the convex hull of affinely independent points.
Let be nonempty and convex, finite, and quasi-concave and u.s.c. on for each . If is minimal for P, then
The lemma makes no compactness or finite-dimensionality assumption on ; that generality is what lets Sion apply it on the convex hull of a finite set inside an arbitrary topological vector space.
Sion's Theorem 3.4 and the Corollary on p. 174 (the minimax theorem) enter the mission as the existing, proved platform item FamousTheorems.sion_minimax_theorem.
Lemma 3.3 is a finite, one-sided statement that already contains the full strength of the quasi-concave case: a finite family of "threats" , none of which can be dropped, can be beaten simultaneously by one point . On p. 174 Sion derives the minimax theorem from Lemma 3.3 and Lemma 3.3′ by reducing open covers to minimal finite ones, alternately on each side. Theorem 3.1 is an open-set KKM theorem with a convexity condition on complements, a covering principle of independent use in fixed-point theory and equilibrium existence. Remark 3.6 shows that the semicontinuity hypotheses are not decorative.
On the formal side, the minimax theorem is proved in Mathlib by another route, so nothing in this mission is needed to know that Sion's theorem is true. What the mission adds is the infrastructure of the original proof: a KKM-type theorem (absent from Mathlib and from the platform), a Helly-type statement about points, and the minimal-cover lemma. None of these has a machine-checked proof today. A formalized open KKM theorem is reusable for Fan's lemma, for Gale–Nikaido–Debreu type existence results and for other covering arguments.
The obvious approach to Lemma 3.3 is induction on , using quasi-concavity to combine points that are good for subfamilies. It fails because quasi-concavity gives control over superlevel sets only, so the union of two "bad" sets is not controlled, and nothing forces two partial witnesses to have a common improvement on the segment between them. The lemma is genuinely topological: without upper semicontinuity it is false (Remark 3.6 exhibits the resulting failure of the minimax equality).
The topological content sits in Theorem 3.1. Neither Mathlib nor the platform has a KKM theorem (the platform has Brouwer's fixed-point theorem), and the passage from the classical closed-set KKM theorem to the open-set form, and from a simplex inside a possibly non-Hausdorff topological vector space to the standard simplex, both need care: the topology induced on a finite-dimensional subspace need not be the Euclidean one.
[AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], the class of Mathlib's Sion file. No Hausdorff or finite-dimensionality assumption is made. The paper never names the ambient space; "convex set" is read as a convex subset of such a space.QuasiconcaveOn, QuasiconvexOn, UpperSemicontinuousOn, LowerSemicontinuousOn, all relative to the set or .Finset ι; values off are irrelevant. Minimality is "no strict sub-Finset has property P".Module.finrank).EReal; "cannot be removed nor appreciably weakened" is informal and omitted.Contributions welcome: a formal KKM theorem (closed and open versions), Theorem 3.2 from Mathlib's Convex.helly_theorem, and proofs of the milestones in any order.
Markets for indivisible goods, in which each participant owns one unit and wants one unit (houses, kidneys in paired donation, dormitory rooms, school seats), cannot be analysed with the convexity assumptions of classical general equilibrium theory. Shapley and Scarf (1974) introduced the housing market to ask whether the two central solution concepts of exchange economies survive indivisibility: the core (allocations no coalition can improve upon by trading among itself) and competitive equilibrium (allocations supported by prices at which every trader optimizes within his budget). Their paper (doi:10.1016/0304-4068(74)90033-0) gives two proofs that the core is nonempty. The first (Section 4) shows that the associated game without side payments is balanced and invokes Scarf's theorem; that is the companion mission of this series. The second (Section 6) is a constructive argument the authors attribute to David Gale, the top trading cycles method, which also produces competitive prices. This mission formalizes the second.
Timeline.
A finite set of traders each brings one indivisible good; "item " is the good of trader . Preferences are a real matrix : trader prefers item to item when and is indifferent when . Ties are allowed, and only comparisons matter.
An allocation is a bijection ; trader receives item . For a coalition , an -permutation reshuffles the items of among the members of . The allocation is a core allocation if there is no nonempty and -permutation with for every .
Prices are competitive for if each trader , selling his own item for , can afford , i.e. , and no item with is better for him than .
For , a top trading cycle for is a nonempty whose members can be arranged in a cycle so that each likes the good of at least as well as any other good in . A top-trading-cycle partition is
with a top trading cycle for and each a top trading cycle for . In Lean the partition carries stage : N → Fin p and the successor map next : N → N.
For every market and every top-trading-cycle partition with successor map , the allocation is a core allocation, and for every choice of prices
on the goods of it is competitive. The paper asserts that "a set of competitive prices exists"; its argument works for every such choice, and the goal states that.
For the matrix the unique competitive payoff is at equal prices, while the allocation with payoff is a core allocation that is competitive at no prices.
The result gives the existence of a core allocation of every housing market by an explicit construction, and shows that this allocation is competitive, so the competitive solution is nonempty even though goods are indivisible and preferences may have ties. The Section 7 example shows that the inclusion of competitive allocations in the core is strict in general. Under strict preferences, the outcome of the construction is the basis of the matching-market literature: uniqueness of the strong core (Roth–Postlewaite), strategy-proofness (Roth), and the school-choice and kidney-exchange mechanisms built on top trading cycles.
The mathematics is classical and proved. The formalization adds a machine-checked statement of the weak-preference version with the paper's strict blocking notion and its price argument, which existing formal developments do not cover. The closest platform items are AGT.house_core_unique, the strict-preference refinement (Roth–Postlewaite: with strict preferences and weak blocking the core is exactly one allocation), and the school-choice items SchoolChoice.TTC.*. Neither is this statement: the first assumes strict total orders and a different blocking notion, under which the core can be empty once ties are allowed, and says nothing about prices; the second concerns another model with priorities.
Each step is short on paper; the work is in the bookkeeping. The cycle allocation must be shown to be a bijection of from the stage-by-stage cycle structure; the "chain of best-liked goods that eventually must come back to some earlier element" must be turned into a cycle whose members each get a best good in , with ties handled by a choice rather than by a unique top choice; and the first-stage argument must be carried out with the coalition's reshuffling restricted to its own goods. A tempting shortcut, assuming strict preferences or using a union of cycles at a stage, proves a different statement and is ruled out by the definitions.
N with decidable equality; no nonemptiness is assumed (the empty market has the empty partition). The matrix A : N → N → ℝ has no hypothesis, so ties are allowed.σ : N → N rather than zero-one matrices. This loses nothing: a coalition in which all members are strictly better off gives each member exactly one item of the coalition (owning nothing is ranked below everything), and an allocation leaving a trader without an item is blocked by that trader alone.next, every member reaching every other by iterating next. A one-trader cycle with next i = i is allowed (footnote, p. 114).A convex program is useful in practice only if its optimal value responds reasonably to small changes in the data. Lagrangian and Fenchel duality theory makes this precise: the dual problem attains its optimum and has no duality gap exactly when the primal value function does not fall off infinitely steeply under small perturbations. A constraint qualification is a checkable condition on the data that guarantees this good behaviour; Slater's condition (a strictly feasible point) is the best-known example in finite dimensions.
R. T. Rockafellar's 1967 paper Duality and Stability in Extremum Problems Involving Convex Functions (Pacific J. Math. 21 (1967) 167–187) develops Fenchel-type duality for the problem of minimizing in general locally convex spaces. It introduces the notion of a stably set problem, shows that stability is equivalent to strong duality with an attained dual optimum (its Theorem 3), and gives in Theorem 1 a general sufficient condition for stability. Theorem 1 is the infinite-dimensional analogue of Slater's condition and is the form in which the result is usually applied: one exhibits a single point where is finite and is finite and continuous.
Timeline. Fenchel (1951) proved the duality theorem for in under relative-interior conditions. Brøndsted (1964) and Moreau (1966–67) extended conjugate duality to paired locally convex spaces. Rockafellar's 1967 paper (this mission) added the linear map , the perturbation function , the notion of stability, and Theorem 1. The perturbational approach was later systematized in Rockafellar's Conjugate Duality and Optimization (SIAM, 1974).
Let and be real locally convex Hausdorff topological vector spaces and a continuous linear map. Let and .
and its perturbations are : minimize , for . The perturbation function is , so . is consistent if .
Suppose there exists such that is finite at and is finite and continuous at . Then
The neighbourhood is left unspecified, as in the paper.
The result. Combined with the paper's Theorem 3, Theorem 1 yields: if is finite at some where is finite and continuous at , then , with the dual maximum attained. This is the standard sufficient condition for Fenchel–Rockafellar duality in infinite dimensions, used in calculus of variations, optimal control, and the convex analysis of integral functionals. The continuity half of Theorem 1 says that the optimal value depends continuously on translations of the constraint data near the unperturbed problem, a basic sensitivity statement.
Formalizing it. The theorem is proved (1967) and appears in many textbooks, but there is no machine-checked version on this platform. Mathlib contains continuity criteria for real-valued convex functions on open sets of normed or finite-dimensional spaces (ConvexOn.continuousOn_tfae, ConvexOn.continuousOn_interior), but nothing for extended-real-valued convex functions on general topological vector spaces, no perturbation function, and no notion of a stably set problem. A complete development would provide reusable infrastructure: the epigraph-interior continuity criterion for -valued convex functions and the elementary calculus of one-sided directional derivatives.
The obvious argument says: is continuous at , so is bounded above near , hence is continuous at and its directional derivatives are bounded. Two steps of this fail without care. First, the passage from "bounded above near a point" to "continuous" requires convexity of (Lemma 2 of the paper, proved in the companion mission) and a continuity criterion valid in an arbitrary topological vector space, with values in ; the normed-space proofs in Mathlib do not apply. Second, may take the value , and the derivative may be in some directions; the bookkeeping of extended-real arithmetic (where is not defined mathematically and is given a junk value in Lean) has to be done honestly. Finally, upper bounds on must be converted into lower bounds, which is where the second inequality of (4.6) enters; an upper bound alone does not give stability.
All values are in Lean's EReal. Convexity is convexity of the epigraph with real second coordinate (the paper's definition, p. 170); concavity is convexity of . Properness is stated as in the paper. The perturbation function is the EReal infimum ⨅ x, f x - g (A x - z); under properness the undefined form never arises. The directional derivative (4.3) is the lower limit of the difference quotient along , which equals the paper's limit whenever it exists (always, for convex with finite). "Unstably set" quantifies over all neighbourhoods of and all real , with allowing . "Stably set" is together with "not unstably set", so is stably set, as the paper says on p. 176. Continuity is with respect to the order topology of EReal, and "continuous at " is continuity of itself at that point, not of its restriction to .
The paper's standing setting (§3) includes dual spaces , the adjoint and the conjugates . Neither Theorem 1 nor its proof uses them, so they are omitted and the theorem is stated for every pair of real locally convex Hausdorff spaces, which includes every paired setting. The lower and upper semicontinuity of and are standing hypotheses of the paper and are kept, although the proof does not use them. Inequality (4.6) is stated for an arbitrary convex function finite at , the generality in which the paper invokes it. No statement was repaired.
A definition of "stably set" that already presumed finiteness or continuity of near , or that tested the derivative only in a fixed set of directions, would make the first conclusion of Theorem 1 trivial; the definition used here is the paper's p. 175 definition verbatim, applied to an arbitrary function . The definitions are local to this mission; the companion missions on Theorem 3 and Theorem 6 of the same paper define the same objects in their own namespaces. Contributions are welcome on the milestones in any order, and in particular on a general continuity criterion for extended-real-valued convex functions on topological vector spaces, which is reusable well beyond this mission.
Bin packing asks for the minimum number of unit-capacity bins into which a list of items with sizes in can be packed. It is one of the basic NP-hard problems of combinatorial optimization and operations research, and its stochastic version, where the item sizes are random, has a large literature (Coffman and Lueker, Probabilistic Analysis of Packing and Partitioning Algorithms, 1991). A first question about the random optimum is how strongly it concentrates around its typical value.
A short history of that question, as Talagrand recounts it on p. 151 of the source:
This mission formalizes that chapter.
Let and . A point is a list of item sizes. A packing into bins is a map with for every bin . The bin packing number is the least for which a packing exists ( bins always suffice; when ).
Further notation, as in Lean (TalagrandConc.BinPacking):
l2Norm);levelSet);U, V, convexDist);secondMoment);IsMedian).For every median of and every with ,
The goal keeps the paper's explicit constants , and .
The result. Theorem 6.5 shows that the random optimum fluctuates on the scale rather than . For small items () this is much sharper than the martingale bound, and it is the scale of the fluctuations of , which is a lower bound on . Chapter 6 is also the first application in Part II of the paper, and its scheme recurs in the later chapters: a deterministic lemma relating the functional to of a level set, a tail bound for an auxiliary factor, and Theorem 4.1.1 to finish.
Formalizing it. The result is proved (Talagrand 1995; Rhee 1994 by another route). No machine-checked proof is known to exist: the platform has no random bin packing statement and no general- form of Talagrand's convex distance inequality. A complete development gives a checked concentration bound for an NP-hard combinatorial optimum, plus a bin-packing layer (the optimum as a minimum over assignments, Lemma 6.1, monotonicity in the item set) that other formalizations can reuse.
The obvious route is a bounded-differences argument: changing one item changes by at most one. That route yields only the exponent , because it cannot see that small items change little. Replacing the Hamming geometry by one weighted by item sizes is the point. The weights depend on the point itself, so no fixed weighted Hamming distance works. The convex hull distance controls every weighting at once, and the resulting factor is random and must be controlled separately (Lemma 6.3). In Lean, the further difficulty is the probabilistic input: Theorem 4.1.1 / Eq. (4.1.2) for a general (non-finite) is not available, and the convex-hull minimax step (Lemma 4.1.2) behind Lemma 6.2 must be formalized too.
unitInterval. Coordinates are Fin N (0-based). is Measure.pi (fun _ : Fin N => μ) for μ : Measure unitInterval with IsProbabilityMeasure μ. No density is assumed.sInf {k : ℕ | IsPacking x k}, an exact minimum over assignments Fin N → Fin k, not a heuristic such as First Fit. Zero-size items are allowed, as in the paper.ℝ≥0∞ with the Euclidean norm written out ( for an empty set; Mathlib's default norm on Fin N → ℝ is the sup norm). Lemma 6.2 is stated in ℝ≥0∞.ℝ≥0∞-valued. Every event in the statements (, ) is Borel. The paper's measurability convention matters only inside the proofs.sInf.An experimenter can draw observations from two populations and , one at a time, and wants the sum of the observations to be as large as possible. The populations might be two treatments, two seed varieties or two manufacturing processes; their means are unknown. Each draw both earns a reward and tells the experimenter something about the population it came from. This is the two-armed bandit problem. Herbert Robbins posed it in its modern form in his 1952 address to the American Mathematical Society, Some aspects of the sequential design of experiments, the paper usually credited with founding the field.
Section 2 of that paper asks a basic question (display (12), p. 532): is there any sampling rule whose average reward per draw approaches the larger of the two means, whatever the populations are? Robbins answers yes, for any two populations with finite means, using one explicit rule: forced sampling along a sparse schedule, greedy choice otherwise. This mission formalizes that answer.
Timeline:
Population has distribution function and population has , with expectations
assumed to exist, i.e. to be finite (display (1), p. 529). Nothing else is assumed about and .
A sampling rule draws one at a time; the population of the -th draw may depend on , and given that choice is a fresh draw from the chosen population. Write . The loss of after draws (display (9), p. 531) is
the average shortfall per draw compared with someone who knows the better population and samples only from it.
The forcing schedule (display (13), p. 532) is a pair of disjoint, strictly increasing sequences of positive integers
of density zero: the fraction of the integers that are an or a tends to .
The rule : at draw , sample if is an , sample if is a , and otherwise sample if the mean of the previous observations from is strictly larger than the mean of the previous observations from , and if it is not (a tie goes to ).
For every pair of populations with finite means and every forcing schedule,
The goal is about the specific rule and every schedule, not about the mere existence of a rule. It contains no rate and no constant, so it stays valid when the rule is analysed more finely.
The goal follows from (15) by the definition (9); the paper's chain is (14) ⇒ (15) ⇒ (16).
The result. The theorem answers question (12) and shows that "learning while earning" costs nothing in the long run, per draw, under no assumption beyond finite means: no bounded support, no variance, no parametric family. It is the first consistency result for an adaptive allocation rule, and it fixes the benchmark later refined by logarithmic-regret theory. In modern terms, a forced-exploration greedy policy has regret on every two-armed bandit with integrable rewards.
Formalizing it. The paper gives no proof; it says the results "can be shown". A machine-checked proof records the argument in full. The platform already has finite-horizon regret bounds for -greedy with bounded rewards (FoundationsRL.Bandits.epsilon_greedy_regret_bound), consistency in the stronger Lai–Robbins sense as a definition (ConsistentBanditPolicy), and a forced-sample tail bound for the Lasso bandit (BastaniBayati.LassoBandit.forced_sample_estimator_tail). None of these covers a deterministic greedy rule, almost-sure convergence, or unbounded rewards with only a first moment, and none of them proves (14)–(16).
The obvious argument is: each population is sampled infinitely often because of the forced draws, so each running mean converges by the strong law, so greedy eventually picks the better population, and the forced draws are negligible. Two steps are not routine.
First, the strong law applies to i.i.d. sequences, while the observations from arrive at random, history-dependent times. The values seen from have to be identified, in law, with an i.i.d. sequence that is independent of the times at which they are used.
Second, passing from (14) to (15) needs uniform integrability of , and only first moments are available. No second moment is assumed, so variance bounds are not available.
When greedy need not settle on either population; the statement must hold anyway, and an argument that waits for greedy to "lock in" does not cover this case.
The populations are a published two-armed BanditAlgorithm.StochasticBandit 2. is arm 0 and is arm 1; and are banditArmMean. A rule is a published BanditPolicy 2, and is the integral against the published infinite-horizon law banditTrajMeasure, whose coordinate is the paper's draw . Explicit readings of the paper's phrases:
Integrable. This is the only assumption on the populations: the class of the paper is left arbitrary, and is allowed.#({1,…,n} ∩ (range a ∪ range b)) / n → 0 in . The sequences are infinite and 0-indexed (a 0 = 1, b 0 = 2).∀ᵐ under the trajectory law, and "lim" is Tendsto … atTop along .Trivializing formalizations are excluded. Without integrability the means and expectations are junk zeros; this is ruled out by the integrability hypothesis. Replacing by "there exists a rule" would weaken the goal to (12). Finite forcing sets would make the statement false.
The needed infrastructure is a representation of the adaptive sampling process by per-population i.i.d. reward sequences, the strong law along random subsequences, and a uniform-integrability argument for averages under only a first moment. All three are reusable for other forced-exploration and greedy policies. Contributions of these general lemmas as separate theorems are welcome.