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?
Many stochastic models produce a stationary quantity that solves a random equation , with a random map independent of . The random difference equation (perpetuities in insurance and finance, the ARCH and GARCH volatility models, random walks in random environments), the Lindley equation of queueing theory, and the random recurrences behind probabilistic analyses of algorithms are all of this form. In these models the law of is rarely explicit, while the decay of its tail is what governs ruin probabilities, extreme values and buffer overflows.
Kesten (1973) showed that the stationary solution of has a power-law tail when for some , by a long argument specific to that equation. Goldie (1991) separated the renewal-theoretic core of the phenomenon from the particular equation: the implicit renewal theorem (Theorem 2.3) gives the power-law tail of any random variable whose tails are comparable to those of , with an explicit formula for the constant. Kesten's theorem and the tail results for several other random equations then follow by checking one integrability condition. The theorem is the standard entry point to the subject, reproduced in the monograph of Buraczewski, Damek and Mikosch (2016).
Timeline:
Let be a probability space and , two independent real random variables. No equation is assumed for .
A probability law on is arithmetic if it is concentrated on a lattice for some , and nonarithmetic otherwise. Fix . The Cramér-type conditions on are
Under them, is finite and positive (Lemma 2.2), with .
The tails of enter through two tail-comparison conditions
and the constants
In the Lean development these are CramerConditions κ (P.map M), cramerMean, TailCondPlus, TailCondMinus, Cplus, Cminus and Ctwo, in the namespace GoldieRenewal.Implicit.
Let satisfy the Cramér-type conditions and let be independent of .
Case 1 ( a.s.): (2.8) implies , and (2.9) implies , as .
Case 2 (): (2.8) and (2.9) together imply
The relation means , including .
Lemma 2.2 (negative drift of , ); Lemmas 9.1–9.2 (smoothed integrable functions are directly Riemann-integrable); Lemma 9.3 (a Tauberian step from averaged to pointwise tails); the renewal equation (9.8) and its key-renewal limit in Case 1; the Case 2a step law (9.11) with mean and nonarithmetic (9.12)–(9.13), and the renewal identity (9.15); the reduction (9.16) of Case 2b to Case 1.
The theorem turns a question about an unknown law into a question about integrability. For a random equation it suffices to compare with , which is often a moment computation; this yields power tails, with constants given by expectations, for perpetuities, Lindley-type equations, random polynomial and maximum equations (Goldie 1991, §§4–8). The explicit constant also decides when the tail is genuinely of order : the theorem has content only when , since otherwise .
The theorem has been proved for thirty years; it is not formalized in any proof assistant known to the mission. A formal development would provide reusable infrastructure absent from Mathlib: direct Riemann integrability, renewal measures of walks on the whole line, the two-sided key renewal theorem (Athreya, McDonald and Ney 1978), and a Tauberian lemma for monotone tails. The sibling missions on Kesten's theorem and on rates of convergence are built on the same setting.
The obvious argument writes as a telescoping sum along the multiplicative walk and applies the key renewal theorem to the result. It fails at three points. First, the function the key renewal theorem would be applied to, , is only integrable under (2.8), not directly Riemann-integrable, and the key renewal theorem is false for general integrable functions; so no conclusion about itself follows directly. Second, when takes both signs, alone is not a random walk that controls : the sign of decides which tail of is involved, so the walk is Markov-modulated. Third, the walk lives on the whole line and may jump to (when ), so renewal theory on , the version in most textbooks, does not apply.
IsProbabilityMeasure P; M, R measurable real random variables; independence is IndepFun R M P. In (9.16) the copy lives on the same space, with IdentDistrib M' M P P and iIndepFun of .P.map M; the moments are lower Lebesgue integrals in . The conditional law in (2.5) conditions on before taking , so Lean's Real.log 0 = 0 never enters; is an extended real with .P.real {ω | t < R ω} with the paper's strict inequalities. (2.8), (2.9) are IntegrableOn … (Set.Ioi 0); the constants are Bochner integrals, used only under the corresponding integrability hypothesis.Tendsto (fun t => t ^ κ * P.real {…}) atTop (𝓝 C).Three formalizations would trivialize the goal and are excluded: reading "" as a ratio (which is false when ); assuming (which forces ); and placing a key-renewal-theorem conclusion among the hypotheses.
Contributions welcome: proofs of any milestone; a general two-sided key renewal theorem for nonarithmetic laws with positive mean (reusable beyond this mission); Mathlib-quality lemmas on direct Riemann integrability and renewal measures.
Many operators of harmonic analysis are bounded on by an orthogonality argument but fail to be bounded on ; what survives at is a weak-type estimate . For singular integrals the standard route to such an estimate is the Calderón–Zygmund decomposition, which splits a function at height into a bounded part and a part supported on a small set. Martingale theory has the same need: square functions, martingale transforms and maximal operators of martingales are bounded on for orthogonality reasons, and their behaviour on -bounded martingales is the delicate endpoint.
R. F. Gundy (1968) supplied the martingale analogue: an -bounded martingale can be written as the sum of three martingales, one bounded in , one whose differences are absolutely summable in , and one that is non-zero only on an event of small probability (Gundy 1968). Gundy's construction used several stopping times. In his 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Burkholder 1973), D. L. Burkholder gave a simplified version of the decomposition in which only one stopping time is used, with explicit constants , and . This mission formalizes that version, Theorem 4.1 of the lectures, together with the facts its proof rests on.
Timeline:
Let be a probability space and a nondecreasing sequence of sub--fields of . A martingale relative to is a sequence of integrable random variables with -measurable and . Its difference sequence is with , i.e. , (the convention is ).
The maximal function is , the square function is , and is its -th partial version. For ,
and is -bounded when . For , the exit time (with ) is the first index at which exceeds ; , , denote evaluation at the random index, with .
The Lean development names these objects dseq (), sqFnN/sqFn (, ), maxFnN/maxFn (, ), pNorm (), exitTime () and valAt/sqFnAt (evaluation at an index in ), all in the namespace BurkholderDFI.Gundy.
For every -bounded martingale and every there are martingales relative to the same -fields, with difference sequences , such that
The three bounds hold together; each alone is trivial ( satisfies the first two, the first and last).
with equality on the left for martingales.
The result. The decomposition is the standard device for passing from to weak-type estimates for martingale operators: an operator that is bounded on , controlled by total variation on the second piece, and local in the sense that it vanishes where the third piece vanishes, is of weak type . Applications of the decomposition are given in Gundy's papers of 1968 and 1969 (On the class , martingales, and singular integrals, Studia Math. 33), which the lectures cite for this purpose. The explicit constants , , make every such weak-type constant explicit.
Formalizing it. The theorem is classical and proved; the remaining work is its formalization. As far as is known, no machine-checked proof of Gundy's decomposition, of Lemma 2.1, or of the weak-type maximal inequality in the form (1.5) for real martingales exists in Mathlib or on this platform. Mathlib provides almost-everywhere convergence of -bounded submartingales and Doob's maximal inequality for nonnegative submartingales; the stopped-value bound for unbounded stopping times, the square-function identity of Lemma 2.1 and the decomposition itself are new. The milestones are shared with other missions of this series (Lemma 2.1 is also used for Burkholder's weak-type square function inequality and his exponential estimates), so each proof is reused.
The obvious attempt imitates the Calderón–Zygmund cut directly: truncate at height , or stop it when it first exceeds . Neither produces the required pieces. Truncation destroys the martingale property, and whatever restores it adds terms that must themselves be controlled in the right norm. Stopping at the exit time produces a martingale bounded by only up to the overshoot at the exit, which is not bounded and lives on an event that is small only in probability. The estimate (4.2) is therefore not a consequence of boundedness; it needs a quantitative square-function bound for the martingale up to the exit, which is the content of Lemma 2.1, and that lemma in turn needs the limit and the stopped values on — so Doob's convergence theorem cannot be avoided.
Processes are functions f : ℕ → Ω → ℝ with a Mathlib Filtration ℕ and Mathlib's Martingale/Submartingale. The paper indexes from ; Lean's index is never read by any quantity in the statements, which use the paper's convention . Mathlib's martingale definition additionally constrains ; this is no restriction, since every martingale indexed from extends this way. The goal asserts that are Mathlib martingales for the same filtration as , and the identity is required for .
Further committed conventions:
A formalization in which the existential could choose its own filtration, or in which the norms were Bochner integrals (which vanish on non-integrable functions), would trivialize the goal; both are excluded by the statement above.
Infrastructure needed: stopped values at unbounded stopping times and their bound; square-function identities for stopped martingales (orthogonality of martingale differences up to a stopping time); conditional-expectation compensators of predictable truncations. The definitions file is shared with the other eight missions of this series and is reusable for any work on discrete-time square and maximal functions. Proofs of the milestones, alternative arguments, and sharper constants are all welcome.
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.
Retailers of seasonal goods, home builders selling out a development, and airlines and cruise lines selling promotional fares all face the same operational question: inventory is fixed, the selling season is finite, and the price can be changed only rarely. Menu costs, advertising commitments and customer goodwill often restrict a seller to a single price change. The question is then when to change the price, and, if both a lower and a higher price are available, in which direction.
Feng and Gallego (Management Science 41(8), 1995) answered this for Poisson demand. Their §4 treats a single markdown (Theorem 1) and a single markup (Theorem 2). This mission formalizes their §5, the markup-or-markdown problem: the seller starts at a middle price and has one opportunity to move either down or up. The paper shows that the optimal policy is again described by time thresholds that depend only on the remaining stock, now two per stock level. The paper builds on the deterministic and fluid analysis of Gallego and van Ryzin (1994), where arbitrarily many price changes are allowed, and is the starting point of a literature on limited-price-change revenue management surveyed by Bitran and Caldentey (2003).
There are three prices . At price demand is a Poisson process of intensity , and at of intensity , with
all prices and intensities positive. Lowering the price raises both the sales rate and the revenue rate. Salvage value is zero. Note that in this section is the lower price; the initial price is .
A seller with units and time-to-go sells at and may switch once, to or to . Write for the demand process at and for that at .
where is the set of stopping times of the history of with and almost surely.
Under the paper's assumption for every , there are strictly increasing sequences , with
such that , where for and otherwise. The excess equals on and on . Each solves
with and . The thresholds are and .
Theorem 3 says that the two-directional problem has the same simple structure as the one-directional ones. With units left and time-to-go , the seller marks down at once when falls below , marks up at once when exceeds , and otherwise keeps the price. Because the thresholds increase with the stock, the policy reduces to a table of numbers, which the paper computes for a housing example (Table 5). The theorem also quantifies the value of flexibility: in that example, allowing either direction adds about $1,500 over the markdown-only policy and about $7,000 over the markup-only policy.
Lemma 3 and the verification Lemma 1 are reusable beyond this mission. Lemma 3 is a sign-change property of differences of Poisson tail sums, of the kind that drives threshold results in revenue management. Lemma 1 is a sufficient condition for the value of an optimal stopping problem driven by a Poisson process. The paper's results are proved with pen and paper only; none of them has a machine-checked proof. The formalization adds a precise statement of Lemma 1, whose printed hypotheses are insufficient (see the scope section), and an explicit record of which threshold facts Theorem 3 depends on.
The value is the supremum over stopping times of a continuous-time process, and the obvious approach, dynamic programming over the stock, needs the value one stock level down. The thresholds at stock are defined through , so the structure must be propagated from one stock level to the next, and several properties have to propagate together. One must know that again has a single sign change, which requires to be increasing beyond . One must also know that is positive up to and eventually negative, so that is finite, and that . These facts concern three different price pairs at once: , and . A direct comparison of with the two one-directional value functions fails, because the optimal direction itself depends on the stock and the time-to-go. The verification step needs a pathwise fundamental theorem of calculus for the Poisson-driven process, which is where the regularity hypothesis on matters.
QueueingFundamentals_Foundations_ArrivalProcess. The rate enters through the hypothesis IsExpInterarrivals P lam T, and enters only through its law: the sum is written through its Poisson law. is the class of real-valued stopping times of the σ-algebras generated by the counts , , with and almost surely.HasDerivAt. Threshold sequences are indexed from . Every infimum is a real sInf paired with the nonemptiness of its set. , , , and the thresholds are existentially quantified and tied together by the theorem's equations, so the existential determines the paper's objects. The page's assumption is a hypothesis of the goal, as on the page.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.
An airline may offer a low promotional fare while seats remain available, then raise the fare as departure approaches. The choice is dynamic: a sale changes both the number of seats left and the benefit of waiting. The same decision appears for hotel rooms and theater seats. Feng and Gallego study a policy with two fixed prices and at most one price change, while allowing the switching time to depend on actual sales rather than a calendar date chosen in advance. Their 1995 paper proves that this adaptive problem has an inventory-dependent threshold rule. This mission isolates the markup case, in which the second price is higher than the first.
The two-price restriction has a practical role. A seller may know the fare classes it can offer while still needing to decide when to close the promotional class. The result identifies a sequence of time thresholds that can be computed for the chosen price pair. It is therefore a structural claim about an optimal policy, not a choice of numerical prices or a claim that two prices optimize over every possible price menu.
There are items and units of time-to-go. At price , sales requests follow a Poisson counting process with rate . Each request sells one item while stock remains. The paper assumes that demand falls as price rises and that the lower price has the higher revenue rate. Thus the markup case has
The salvage value at the end of the horizon is zero. A fixed switch at time charges first and afterwards. Its expected revenue, denoted , is
The two counts in the last term are independent, so their sum has Poisson mean . This is the expression in §3 of the paper. In particular, is the revenue from increasing the price immediately.
An admissible switching time uses only the history of sales at ; it lies between zero and and cannot wait past stock exhaustion. The optimal value is the supremum of expected revenue over these stopping times. The stopping decision may react to sales before the change, but it cannot anticipate future requests. This distinction matters because a deterministic switch time generally has less information than an adaptive one.
The goal is Theorem 2 on pp. 1382–1383. Define the switching function
There are thresholds with , and is increasing. A continuation premium gives the value
For , below and is zero at or above it; . The function satisfies and the differential equation , where . The remaining thresholds are the first nonnegative zero of and the first positive zero of :
The milestones reproduce equation (17), the markup half of Lemma 2, and Lemma 1. Together they identify the Poisson derivative identity, the sign change of , and the verification criterion used to relate a candidate value to optimal stopping. The paper proves the mathematical result; the mission asks for machine-checked proofs of these formal statements.
The threshold sequence tells a seller when increasing the price immediately is optimal, conditional on the stock still available. The value formula also gives the benefit of continuing at the promotional price when time-to-go lies below the threshold. The statement preserves the paper's weaker word “increasing” for : it asserts monotonicity and does not require strict monotonicity of either sequence. The full theorem includes the recursive equations for and , so a proof of a threshold-shaped region alone would leave part of the source result unformalized.
Formalization would add a reusable optimal-stopping model built from a Poisson arrival process, a fixed-switch revenue function, and a verification lemma. The arrival process already has a published definition; the switching model and the theorem statements here are new drafts. The theorem is established in the 1995 article, while its Lean proof remains to be supplied.
The immediate-switch comparison has a single sign change, but the optimal decision also depends on revenue already earned and on the value of unsold stock after each possible sale. For , the relevant forcing term is , so the sign of alone does not locate the optimal switching threshold. A direct fixed-time comparison likewise does not establish optimality among stopping times that react to observed sales. These are the main obstacles the formal proof must address.
The Lean model uses natural-number stock, nonnegative real time, positive real prices and rates, and an imported counting process built from independent exponential interarrival times. A rate is attached to each price. The history of the first process defines the stopping-time class; the second process enters through its Poisson law after a switch. The supremum ranges over admissible stopping times, and the payoff is bounded and measurable under the stated process law. The definition writes sales before switching as , equal almost surely to for admissible times. The probability-measure assumption is explicit, though the exponential interarrival law entails it.
Lean assigns a default value to an empty real infimum. The theorem explicitly asserts that each defining zero set for , , and is nonempty; it also keeps in the definition of , since . Continuity of at zero connects its boundary value to its differential equation. Lemma 1 includes its missing initial, zero-stock, obstacle, and local-Lipschitz assumptions, all required by its printed proof. The paper's word “bounded” in Lemma 2 is retained in the milestone quotation but replaced by the positive lower bound it uses; is unbounded as stock grows. These choices are recorded for review in the moderation notes.
The goal derives optimality from the demand and price assumptions. It does not assume the verification conditions, the sign change, or the revenue identity as premises. Contributions to the Poisson tail calculus, stopping-time measurability and boundedness, threshold zero sets, and verification argument are within scope and can be reused in related finite-inventory pricing models.
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 .Given a reference probability distribution and a set of probability distributions, the minimum discrimination information problem asks for the member of closest to in Kullback–Leibler divergence. It is the basis of Kullback's information-theoretic approach to statistics (Kullback 1959), of the maximum-entropy principle of statistical physics (Jaynes 1957), and of large-deviation theory, where Sanov's theorem identifies the rate function of an empirical distribution with exactly this minimum. The most common constraint sets are defined by prescribed expectations , and the classical answer is that the minimizer is an exponential family member, with density with respect to .
That answer was usually justified by Lagrange multipliers, which presuppose that a minimizer exists. Csiszár's paper (Ann. Probab. 1975) treats the problem geometrically, with I-divergence in the role of squared Euclidean distance, and its last result, Theorem 3.3, proves existence and the exponential form at once for unbounded constraint functions, under a hypothesis on the exponential moments of the .
Timeline:
All distributions (PD's) live on one measurable space . The I-divergence of from is
where is the density of with respect to ; it takes values in and vanishes only for . The variation distance is for any PD dominating both. If is a convex set of PD's containing some with , a with
is the I-projection of on .
Fix real-valued measurable functions on . For (Euclidean -space) the moment set is the set of PD's with , . Further:
If is open in , then for every point of the interior of the I-projection of on exists and
for some constant and some .
Theorem 3.3 gives existence of maximum-entropy (minimum discrimination information) distributions under finitely many moment constraints with unbounded constraint functions, which covers the usual exponential families of statistics (normal, gamma, Poisson moment constraints) where boundedness fails. It identifies the minimizer's form without assuming a minimizer exists, and the Remark identifies the natural parameters as the gradient of the optimal value, the sensitivity interpretation of Lagrange multipliers. These facts underlie the duality between moment and natural parameters of exponential families and the rate functions of Cramér and Sanov type.
The result is proved, in this paper and (under a slightly weaker hypothesis) by Čencov. None of it is formalized: Mathlib has the Kullback–Leibler divergence of measures (InformationTheory.klDiv) and tilted measures, but no I-projection, no existence theorem for constrained minimizers of KL divergence and no exponential-form characterization. The mission produces a machine-checked version of the existence and form theorem, together with the general steps it uses (the parallelogram identity, convergence of minimizing sequences in variation, continuity of exponential-moment expectations under KL convergence).
The obvious argument fails at the first step: the moment set is convex but not closed in variation when the are unbounded, since is not continuous in variation. A minimizing sequence therefore converges in variation to some (as in Theorem 2.1), but nothing places in : mass can escape to where is large. Ruling this out needs quantitative control of , which in turn requires knowing the form of before knowing is feasible; the interplay with the convexity of and the openness of is where the work lies. A Lagrange-multiplier argument is not available: it presupposes a minimizer and differentiability that are part of the conclusion.
Measure X with IsProbabilityMeasure; the I-divergence is Mathlib's klDiv : ℝ≥0∞, which for probability measures equals (1.1) with the conventions , , .Fin k → ℝ with its product (Euclidean) topology; "inner point" is the topological interior. is allowed.sInf over a possibly empty set.A complete development needs: Radon–Nikodym calculus for klDiv (the identity (2.6) ), Pinsker's inequality (available on the platform as a reference item), lower semicontinuity of klDiv under convergence in variation, completeness of the space of PD's in variation, and supporting hyperplanes of finite-dimensional convex functions. The KL parallelogram identity, Lemma 3.1 and the variation-distance facts are reusable well beyond this mission. Contributions on any milestone, and on these infrastructure lemmas, are welcome.
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.