Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Airlines, hotels and rail operators sell many products (an itinerary combined with a fare class) that share a network of finite resources (flight legs, room-nights). When customers choose among whatever products are on offer, the firm's control is no longer "accept or reject a request for product " but which set of products to offer at each moment. The exact dynamic program for this problem is intractable for realistic networks, so practice and theory rely on a deterministic approximation, the choice-based deterministic linear program (CDLP) of Gallego, Iyengar, Phillips and Dubey (2004), which decides for how long each offer set should be offered.
The CDLP has one variable per offer set, so variables for products, and it is solved by column generation. Knowing in advance which offer sets can never receive positive time in an optimal solution cuts this search space. Liu and van Ryzin (MSOM 2008) extended the single-leg notion of an efficient offer set from Talluri and van Ryzin (Management Science 2004) to networks and showed that only efficient sets are used by an optimal CDLP solution. This mission formalizes that section of their paper (§5).
A network has legs and products . Product earns revenue , and the 0–1 incidence matrix records which legs product uses. An offer set is a subset . When is offered, an arriving customer buys product with probability , where for , and buys nothing with probability , with . The expected revenue per arriving customer and the vector of expected capacity consumption are
An offer set is inefficient if some convex weights , , over all offer sets satisfy
otherwise is efficient.
With arrival probability per period, capacities and a horizon of length , the CDLP is
where is the total time during which is offered. Its dual has prices on the legs and on time. Finally, the frontier function is
In the Lean development these objects are ChoiceNetwork m n (with revenue and consumption), IsEfficient, IsCDLPFeasible / cdlpObjective / IsCDLPOptimal, and frontier, all in the namespace ChoiceCDLP.Efficient.
If is an optimal solution of the CDLP and is an offer set with , then is efficient:
The statement covers every optimal solution, not only basic ones.
Proposition 4 says that efficiency is a property of every offer set an optimal CDLP solution actually uses. Inefficient sets can therefore be removed from the column space of the CDLP, and Proposition 3 describes the remaining sets as the maximizers of revenue net of leg prices, which is the pricing subproblem of column generation. The paper also uses Proposition 4 to argue that its asymptotically optimal policy (Proposition 2 of the same paper) uses only efficient sets. Proposition 5 gives the partial order of efficient sets in the network, the analogue of the total order that drives nested policies in the single-leg model.
The results are proved in the paper; none of them has a machine-checked proof. A formalization provides a checked statement of the network notion of efficiency and its price characterization, which the single-leg results already on the platform do not cover (there is a scalar), and a checked link between LP duality for the CDLP and the structure of its optimal solutions.
The paper's proof of Proposition 4 appeals to "the optimal basis" of the CDLP, while the statement is about every optimal solution, including non-basic ones, so the simplex-tableau argument as written does not cover the statement; the existence of optimal dual prices with the required reduced-cost properties has to be established for an arbitrary optimal solution. The "only if" half of Proposition 3 is argued in the paper by a supporting hyperplane to the concave function at , followed by an informal argument that the hyperplane's slope is nonnegative; may lie on the boundary of , where a supporting hyperplane of a concave function need not exist in the naive sense, and the sign argument is stated in one line. Concavity of is the concavity of an LP's optimal value in its right-hand side, which the paper cites from Bertsimas and Tsitsiklis without proof and which Mathlib does not provide.
Fin n and Fin m; offer sets are Finset (Fin n), so sums over "all " are sums over Finset.univ. All quantities are real. Vector inequalities (, , , ) are componentwise, and is dotProduct.sSup) over attainable mixed revenues; on the set is nonempty (the weight concentrated on the empty offer set is feasible because ) and bounded above by , so it is the paper's maximum.A retailer or an airline chooses which products to offer, and customers choose among what is offered. The assortment problem asks for the offer set that maximizes expected revenue when customer choice follows a given probabilistic model. Under the multinomial logit model the answer has a simple shape: an optimal assortment is revenue ordered, i.e. it consists of all products whose revenue exceeds some threshold (Talluri and van Ryzin, 2004). The multinomial logit model treats all products as equally substitutable, and nested logit models relax this by grouping products into nests whose utilities are correlated.
The -level nested logit model organizes the products as the leaves of a tree with levels, each level refining the grouping of the previous one (for instance category, brand, size). Li, Rusmevichientong and Topaloglu (Oper. Res. 63(2), 2015) characterized an optimal assortment under this model for every . Timeline: the one-level case (multinomial logit) is due to Talluri and van Ryzin (2004); the two-level case with an arbitrary number of nests is due to Davis, Gallego and Topaloglu (2014); Li, Rusmevichientong and Topaloglu (2015) treat arbitrary depth . This mission formalizes the 2015 characterization and the three statements of §4 of that paper that lead to it.
There are products and a no-purchase option . A product tree is a finite rooted tree with levels whose leaves are exactly the products: the leaves lie at depth , and leaf is a child of the root. Each node other than the root has a parent ; is the set of its children, and is the set of leaves below . Each nonleaf node carries a nest parameter , with . Each product carries an attractiveness , and each product a revenue .
An assortment is a set ; the no-purchase option is always available. The preference weight of a node is defined bottom-up: at an offered product leaf, at a product leaf that is not offered, , and at a nonleaf node
so . A customer at a nonleaf node moves to child with probability . The expected revenue from a customer at node is at an offered product leaf, at an unoffered leaf and at leaf , and
at a nonleaf node. The assortment problem is
Given an optimal assortment , the thresholds are computed top-down by
and the local problem at node is
For every product tree and parameters in the ranges above, and for every optimal assortment with its thresholds ,
The corollary says that an optimal assortment is determined by one comparison per product: a product is offered exactly when its revenue reaches a threshold attached to its parent node. Within each group of sibling products the optimal assortment is therefore revenue ordered, which reduces the search from subsets to a structured family, and it is the basis of the paper's polynomial-time algorithm (§5). For one level it recovers the revenue-ordered result for multinomial logit, and for two levels the characterization of Davis, Gallego and Topaloglu (2014). Theorem 4.2, the synthesis of local solutions, is the property that makes a bottom-up dynamic program over the tree correct.
The result is proved in the paper; the proofs of Proposition 4.1 and Theorem 4.2 are in its online appendix. No machine-checked version of any nested logit assortment result is known to exist. A formalization would give a verified statement of the model itself (recursive preference weights with real exponents, conditional revenues, top-down thresholds), which is reusable for the paper's pricing results and for other tree-structured choice models.
The objective is a nested ratio of sums raised to fractional powers, neither concave nor monotone in the offer set, so the usual exchange argument for revenue-ordered sets does not apply directly: adding a product to a nest changes that nest's weight, and through the exponents the weight of every ancestor. The thresholds are defined from an optimal assortment that is not known in advance, so every statement is a property of an unknown optimum rather than a computation. The local problems couple across levels only through these thresholds, and relating the optimum of the problem at a node to the optima at its children is the step that requires work. A proof that tries to compare with product by product meets the fact that and may differ at ties.
The tree is a structure ProductTree n with a finite node type, a root, a parent map, a depth function (root at depth , children one level deeper, all depths at most , product leaves at depth exactly , leaf a child of the root) and an injective leaf map Fin (n + 1) → Node. Assortments are finsets of Fin (n + 1) not containing ; the no-purchase leaf always contributes . Preference weights use Real.rpow, so gives . Conventions fixed in Lean and silent on the page:
StandingEta);x / 0 = 0 on the page's ); in this value yields ;A trivializing formalization is ruled out: the thresholds are not free parameters or computed from , and the conclusion is optimality of against every assortment, not an existence statement.
A complete development needs facts about the recursive definitions (unfolding at leaves and nonleaf nodes, , disjointness of the of siblings), monotonicity and concavity properties of on from Mathlib, and induction over the tree by depth. Tree-induction lemmas and the model layer are reusable by the companion pricing mission. Contributions of a proof of any milestone, of alternative proofs of Theorem 4.2, and of the special cases and are welcome.
A seller who does not know its demand curve has to learn it from the sales it makes. Each price it charges earns revenue now and also produces information for later. This learning-and-earning problem is basic to revenue management and online retail. The most common heuristic is certainty-equivalence pricing: fit the demand model by least squares, then charge the price that would be optimal if the fit were exact. The heuristic can fail. Its prices may settle at a wrong value, so that estimation stops improving, a phenomenon called incomplete learning (Lai and Robbins 1982; den Boer and Zwart 2013). The regret then grows linearly in the horizon.
Keskin and Zeevi (2014) first show that no policy can have regret below order (the subject of the first mission in this series). They then give two simple, checkable conditions on a policy's price path that guarantee regret of order . The conditions cover a whole family of modified least squares policies, including the "MLE-cycle" policy of Broder and Rusmevichientong (2012) and the "controlled variance" policy of den Boer and Zwart. This mission formalizes those sufficient conditions (Theorem 2 of the paper).
A seller charges prices , , in periods and observes the demand
The unknown parameter lies in a rectangle with . The demand shocks are i.i.d. with mean and variance , and they are light-tailed: for , for some . The expected revenue is , maximized at the myopic price . The model assumes for all .
A pricing policy charges a constant and then , where is a measurable function of the history with values in . The regret of under is
After periods the empirical Fisher information is . The least squares estimate is , and the truncated estimate is the Euclidean projection of onto . The information metric is with . The greedy least squares price in period is .
Let , let , and let satisfy, almost surely for all ,
Then there is a finite with
The goal fixes no constant. It asserts only the rate .
The result. Theorem 2 turns the design of a near-optimal learning policy into two pathwise constraints on the price sequence. Condition (i) requires enough price dispersion to keep learning. Condition (ii) requires the policy to stay close to the greedy price so that it keeps earning. Any least squares variant that satisfies both constraints is optimal up to a logarithmic factor, and together with the lower bound this fixes the minimax rate of the problem. The constrained-ILS and decaying-perturbation policies of §3.3 are certified this way, and the same template reappears in the paper's incumbent-price and multiproduct results.
Formalizing it. The theorem is proved in the paper. It has no machine-checked proof, and the platform has no dynamic-pricing results so far. A formalization would contribute a reusable model of adaptively chosen designs with a least squares estimator, an exponential concentration bound for least squares under adaptive prices (Lemma 3), and the regret decomposition. The formalization also checks the paper's constants: one of them, in Lemma 2, is misprinted (see Formalization scope).
The prices are chosen by the policy from past noise, so the regression design is random and adapted. The classical fixed-design analysis of least squares does not apply, and neither does a union bound over a fixed set of designs. Lemma 3 needs a tail bound for that is uniform over all directions in the plane and holds only on the event where is large, with noise that is only light-tailed rather than Gaussian or bounded. Converting the eigenvalue of into the scalar (Lemma 2) is elementary but easy to get wrong, as the misprinted constant shows. Summing the per-period bounds into the rate is where conditions (i) and (ii) interact.
Periods are indexed from . The noise is a family ε : ℕ → Ω → ℝ on a probability space, with ε t used in period . The price process of a policy is built by recursion from the noise, which realises the paper's law on demand sequences. A policy is a family of measurable maps from histories Fin t → ℝ × ℝ of (demand, price) pairs into , and it sees neither nor the noise. Expectations are Bochner integrals of bounded measurable functions. Probabilities are ENNReal values. Real.log is the natural logarithm. The least squares estimate uses Mathlib's matrix inverse, which is on singular matrices. Every statement uses only where , which is equivalent to . The truncation onto is coordinatewise clamping, the Euclidean projection onto a rectangle. The smallest eigenvalue is the infimum of the Rayleigh quotient over unit vectors. Constants sit in the paper's quantifier positions: after and in the goal; before the policy in Lemma 3.
Corrections of the printed statements.
Trivializing formalizations ruled out. Hypotheses that no policy can satisfy (conditions required at ) are excluded by the form. A policy type that could read or the noise is excluded by construction. Junk values of the matrix inverse and of never enter a hypothesis or conclusion.
A complete development needs the price-process recursion and its measurability, exponential supermartingales for adaptively weighted sums of light-tailed noise, a covering argument on the unit circle, and the layer-cake formula for . The model, the least squares estimator and Lemmas 2–3 can be reused for the incumbent-price variant (mission IV of this series) and for other least-squares-based pricing and bandit policies. Contributions of any milestone are welcome, and Lemma 3 on its own is a useful statement.
A group of agents must choose one alternative from a set (whether to build a public project, who receives an object, which of several policies to adopt). Each agent privately knows how much each alternative is worth to them, and money can be transferred. A designer who wants the welfare-maximizing alternative must ask the agents for their valuations, and must set payments so that no agent gains by misreporting, whatever the others report. This requirement, dominant strategy incentive compatibility, does not depend on what agents believe about one another, which is why it is the standard robustness benchmark in public economics, auction design and algorithmic game theory.
The Vickrey–Clarke–Groves (VCG) mechanisms solve this problem for every efficient decision rule. The central question of Chapter 7 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), is whether they are the only solution, and what can be implemented in dominant strategies at all.
Timeline:
There is a finite set of agents and a set of alternatives. Agent has a type from an abstract set . If alternative is chosen and agent pays , agent 's utility is . A type vector is ; omits agent , and replaces agent 's type by .
A direct mechanism consists of a decision rule and transfer rules . It is dominant strategy incentive-compatible (DSIC) if for all , and ,
A decision rule is efficient if maximizes over at every . A mechanism is VCG if is efficient and every agent's transfer has the form
for some function of the other agents' types. The chapter also uses positive association of differences (PAD: if and every agent's utility advantage of over every other alternative strictly increases from to , then ), flexibility (the range has at least three elements), ex post individual rationality and ex post budget balance ().
If every is a convex subset of a Euclidean space and every is convex and continuous on , then every DSIC mechanism with an efficient is a VCG mechanism: for each there is with
The goal leaves , the number of agents and the dimensions free; it asserts only the form of the transfers.
Every numbered result of Chapter 7 except Proposition 7.6 (see Formalization scope):
Corollary 7.1 turns the VCG construction from one solution into the complete answer. Any question about efficient dominant-strategy mechanisms (revenue, budget balance, individual rationality) reduces to a question about the functions . With Proposition 7.10 it gives a necessary and sufficient condition for efficient, budget-balanced dominant-strategy implementation. That condition fails in bilateral trade, and the failure does not use individual rationality. Roberts' theorem plays the same role for inefficient rules: on unrestricted domains, weighted welfare maximization is essentially all that can be implemented.
All of these results are proved in the literature, and none is formalized. The platform has VCG incentive compatibility and weak monotonicity for valuation-based types (the Algorithmic Game Theory IV mission). It has no uniqueness theorem, no revenue equivalence for multidimensional convex types, no Rochet theorem and no Roberts theorem. The book proves Corollary 7.1 from Proposition 7.3, but proves 7.3 itself only by reference to Krishna and Maenner. It states Roberts' theorem without proof.
The uniqueness claim does not follow from incentive compatibility alone. With finitely many types it is false, because any transfers inside the gaps left by the incentive constraints work (Börgers §5.8). The work lies in showing that, along every segment in the convex type set, an agent's equilibrium utility is pinned down by the decision rule. The equilibrium utility is a pointwise supremum of convex functions, one for each report, and the chosen alternative can change at uncountably many points of the segment. A differentiable envelope argument is therefore not directly available. At the boundary of the type set, convexity alone does not prevent upward jumps, which is why continuity is part of the hypotheses. Roberts' theorem needs a separate, combinatorial analysis of the sets of utility differences at which each alternative is chosen, and flexibility is essential there.
Agents form a finite type ι with decidable equality. Types are arbitrary types Θ i, and utilities are u : ∀ i, A → Θ i → ℝ. The profile is Function.update θ i θ'. is the product Others Θ i over j ≠ i, so each and is a function of the others' types only; a constant or a function of the full profile would change the theorem. In the goal and Proposition 7.3, is a convex set S i in EuclideanSpace ℝ (Fin (d i)).
Deviations from the page, each forced by a counterexample recorded in the item's natural-language statement:
The trivializing formalization to avoid is proving Proposition 7.4 (VCG DSIC) in place of the goal (DSIC efficient VCG). A development that proves the goal needs reusable infrastructure: convex functions restricted to segments, absolute continuity of continuous convex functions on compact intervals, and an envelope theorem for suprema of convex functions. Proofs of Rochet's and Roberts' theorems in this abstract setting are also welcome.
A firm that sells a product repeatedly and does not know how demand responds to price must learn the demand curve and profit from it at the same time. This is the learn-and-earn or dynamic pricing with demand learning problem. It is a standard model in revenue management, and it is one of the simplest settings where exploration and exploitation have to be traded off in a continuous action space.
The paper behind this mission is N. Bora Keskin and Assaf Zeevi, Dynamic Pricing with an Unknown Demand Model: Asymptotically Optimal Semi-Myopic Policies, Operations Research 62(5):1142–1167, 2014 (doi:10.1287/opre.2014.1294). For a linear demand model with two unknown parameters, it proves a lower bound on the regret of every pricing policy. It then gives simple conditions under which least-squares-based policies attain that bound up to a logarithmic factor. This mission is the first of a series on the paper, and its target is the lower bound (Theorem 1).
Timeline. Earlier work had already obtained -type lower bounds for dynamic pricing under demand uncertainty:
Keskin and Zeevi (2014) prove the bound when both the intercept and the slope of the demand curve are unknown. Their argument uses the Van Trees inequality instead (p. 1146).
Prices lie in an interval with . In period the seller charges and observes the demand
The demand shocks are i.i.d. with .
The parameter is unknown to the seller. It lies in a rectangle
The expected single-period revenue is , and it is maximized at . The model assumes that this optimal price lies in the open interval for every .
A pricing policy is a constant first price together with measurable maps . Each sends the observed history to , and the seller charges . The policy sees neither nor the shocks.
The regret of over periods under is
The worst-case regret is .
The proof also uses the empirical Fisher information and the row vector .
In Lean, the model is the structure KeskinZeevi.LowerBound.Model. The noise hypothesis is the shared definition RobustBooking.Shared.GaussianNoise (measurable, mutually independent shocks, each with law ). The other objects are Policy, pricePath, regret, worstRegret, sqErr (the expected squared pricing error ) and infoQuad (the scalar ).
There is a finite constant , depending only on the model, such that
The goal states only the order with an unspecified constant. The paper's explicit constant is not part of the target.
The result. Theorem 1 sets the benchmark for the whole paper. A policy is called asymptotically optimal when its regret grows no faster than , up to logarithmic factors. Theorem 2 of the paper then gives sufficient conditions under which least-squares pricing policies meet this benchmark. Without Theorem 1, those upper bounds would have nothing to be optimal against.
The lower bound also explains a well-known failure. Greedy (myopic) least-squares pricing can stop learning and suffer linear regret, and this happens precisely when the information on the right side of (14) stops growing.
Formalizing it. The result is proved on paper but has not been formalized; no dynamic pricing or learn-and-earn regret result is on the platform yet. A formal proof needs a Van Trees (Bayesian Cramér–Rao) inequality for an adaptively generated sample, which Mathlib does not have, and a machine-checked version of the elementary recursion that turns (A3) into . The model layer (policies driven by noise, regret, worst-case regret) is shared with the three later missions of the series.
The bound must hold for every measurable, history-dependent policy. So it is a statement about a sequential experiment whose design adapts to the data, not about one fixed estimator.
The usual two-point argument (Le Cam or Kullback–Leibler) perturbs one parameter at a time. It yields only when a single parameter is uncertain, and here both and are unknown. The information a policy gathers about the optimal price is itself tied to how far its prices stray from that price. That self-reference is what inequalities (A2) and (A3) express, and it has to be handled uniformly in and in the horizon.
Finset.range T, and sums are Finset.Ico 1 T.Fin t → ℝ × ℝ of (demand, price) pairs. A policy is a structure with measurable rules valued in .The Van Trees step (A1) of the proof of Lemma 1 is not a milestone. It needs Fisher information and a prior density on , and neither is in Mathlib. Contributions of a Van Trees inequality for this Gaussian model are welcome, as is a formal proof that (A3) implies the bound. The first is reusable for other lower-bound missions of the series, and the second is elementary but careful real analysis. The multiproduct generalization (Theorem 5, §4) is outside this mission.
Almost every screening, auction and regulation model asks the same preliminary question: which allocation rules can be made incentive-compatible by some choice of payments? In the one-dimensional models of auction theory and nonlinear pricing the answer is monotonicity: higher types must receive higher allocations. Many applications are not one-dimensional, though. Examples are multi-object auctions, multi-product pricing, and lotteries over several outcomes. For those, a characterization that uses no structure at all is needed. Rochet (1987) gave one: an allocation rule is implementable exactly when it is cyclically monotone, a condition that originates in Rockafellar's characterization of subdifferentials of convex functions. Later work on dominant-strategy implementation, the "weak monotonicity" literature of algorithmic mechanism design, and revenue equivalence all build on it.
This mission formalizes Chapter 5 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): all nine numbered results of the chapter.
Timeline. Rockafellar (1970, Theorem 24.8) characterized the cyclically monotone maps between vector spaces as the subgradient selections of convex functions. Rochet (1987) extended the idea to arbitrary alternatives and types with quasi-linear utility and proved that implementability is exactly cyclical monotonicity. Krishna and Maenner (2001) proved revenue equivalence on convex type spaces with utilities convex in the type. Bikhchandani, Chatterji, Lavi, Mu'alem, Nisan and Sen (2006) showed that for finitely many alternatives, weak monotonicity (the two-type case of cyclical monotonicity) already suffices on rich, order-based domains. Saks and Yu (2005) proved the same on convex domains.
A designer and one agent choose an alternative from a set . The agent has a type in a nonempty set . With utility function , her payoff from when she pays is . Neither nor carries any structure.
A direct mechanism is a decision rule and a transfer rule . It is incentive-compatible if for all . A decision rule is implementable if some makes it incentive-compatible. It is weakly monotone if for all pairs of types. It is cyclically monotone if for every finite sequence of types with ,
A complete and transitive order of induces a partial order on types: if values every -higher alternative strictly more, relative to an -lower one, than does, and neither type distinguishes -indifferent alternatives. The type set is one-dimensional if any two distinct types are -comparable, and bounded if all utility differences lie in for some . It is rich if, for some reflexive and transitive relation , every function with is some type's utility function. A mechanism is individually rational with outside option if every type does at least as well as with and no payment.
for arbitrary , nonempty and .
Rochet's theorem turns the existence of payments, an infinite system of linear inequalities in unknowns , into a condition on the decision rule alone. It underlies the characterization of implementable rules in multidimensional screening, the taxation principle, and the dominant-strategy characterizations of Chapter 7 (applied agent by agent). Propositions 5.4–5.6 recover the "monotone allocation" results of the one-dimensional chapters from it. Proposition 5.8 is the general form of the payoff-equivalence lemmas used for optimal auctions.
All results are classical and proved on paper, except Propositions 5.7 and 5.8, whose proofs the book omits and refers to the literature. None of them is formalized on Prove2Me. The platform's algorithmic-game-theory series has the weak-monotonicity half in a multi-agent valuation model (types are valuations ), not the abstract-type statement, and has no cyclical-monotonicity or Rochet result.
Necessity is a two-line telescoping argument. Sufficiency needs a transfer rule built from the decision rule, and the first idea fails: prices attached to alternatives chosen pair by pair (which weak monotonicity supplies) need not be globally consistent. Figure 5.1 of the book gives a three-type example that is weakly monotone but not implementable. The transfer must come from a supremum over all finite chains of types starting at a fixed type. The supremum is finite only because of cyclical monotonicity, and no finiteness, compactness or boundedness is available. Proposition 5.8 needs an envelope argument along segments in without differentiability. Proposition 5.7 needs a combinatorial argument that uses richness of the domain.
Alternatives and types are arbitrary Lean types A, Θ with Nonempty Θ, and the utility is u : A → Θ → ℝ. A cycle of length is a map Fin (m+1) → Θ with equal first and last entries, and its summands are indexed by Fin m. Relations are predicates A → A → Prop. For Propositions 5.3 and 5.8, types form a subset S of Ω → ℝ (resp. Fin n → ℝ) used as a subtype. Lotteries are stdSimplex ℝ Ω, and the subgradient inequality is required only at points of S.
The explicit statements are fixed as follows:
Two statements are corrected from the page, each with a counterexample to the literal version recorded in its item:
Both directions of Rochet's theorem are required. The necessity half alone, or a version with finite , finite or bounded utilities, is a different and much weaker theorem and does not close the goal.
The development needs finite telescoping sums, suprema of sets of reals (sSup with an explicit bounded-above argument), convex functions on sets and one-dimensional convex analysis (Proposition 5.8). The definitions file is reusable for Chapters 6–8 of the series. Contributions of alternative proofs, for example Proposition 5.6 through Rochet's theorem, are welcome.
Bayesian mechanism design assumes that the designer knows a common prior from which every agent's beliefs about the others are derived. Chapter 4 of Börgers' An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015, DOI 10.1093/acprof:oso/9780199734023.001.0001) drops that assumption. The designer is unwilling to rely on anything about what agents believe about each other, and therefore requires that truth telling be optimal for every type whatever the other agents report (dominant strategy incentive compatibility) and that participation be worthwhile after all reports are known (ex post individual rationality). The chapter revisits the three examples of Chapter 3 (single unit auctions, public goods, bilateral trade) and asks which mechanisms survive these requirements.
The answer differs sharply between examples. In auctions nothing is lost: an expected-revenue-maximizing auction can be implemented in dominant strategies. With a budget constraint, the class collapses. For a public good shared by two agents, the only dominant-strategy, ex post individually rational mechanisms that exactly balance the budget are fixed cost shares; in bilateral trade they are fixed-price mechanisms. These results go back to the dominant-strategy literature on public goods (Serizawa 1999, Econometrica) and on bilateral trade (Hagerty and Rogerson 1987, Journal of Economic Theory), as the book's §4.5 records (p.93), and they explain why simple posted-price and cost-sharing rules are common in practice.
Every agent has a type in an interval. In the auction and the public good examples the interval is with ; is the set of type vectors, and is without its -th entry. A direct mechanism asks every agent to report a type and maps the reports to an outcome.
A mechanism is dominant strategy incentive-compatible if for every agent, every true type, every false report and every report profile of the others, truthful reporting yields at least as much utility. It is ex post individually rational if every type's utility at every type vector is at least its outside option: for buyers and public good agents, (keeping the good) for the seller. A canonical mechanism (Definitions 4.3–4.5) allocates according to strictly increasing continuous scores and charges each agent the smallest report with which the outcome would have been the same.
For and a decision rule whose production set is closed, a direct public good mechanism is dominant strategy incentive-compatible, ex post individually rational and ex post budget balanced if and only if there are with and, for all ,
Both directions are part of the goal; the "only if" direction is the content.
Proposition 4.4 shows that the optimal auctions of Chapter 3 remain available without any assumption on beliefs, while Propositions 4.8 and 4.12 show that under exact budget balance, dominant strategy implementation forces rules that ignore reported valuations except through a yes/no participation decision. Together they mark the boundary between settings where the Bayesian and the belief-free approaches coincide and settings where the belief-free requirement is severe. This contrast motivates the robust mechanism design of Chapter 10.
These results are proved in the book: Propositions 4.5 and 4.8 in full, the others with proofs omitted or "analogous". No machine-checked proof of them appears on the platform or in Mathlib. The platform has a single-parameter characterization in a different model (AGT.single_parameter_characterization: valuation profiles, win sets, normalized losers' payments) and the second-price dominance fact; neither covers public goods, bilateral trade, budget balance or randomized allocations. The mission would add a machine-checked belief-free counterpart of Chapter 3, including the two characterization theorems whose printed proofs leave cases to the reader.
The characterizations (Propositions 4.2, 4.5, 4.9) are standard single-agent arguments applied to every profile of the others. The goal is harder. Proposition 4.5 describes each agent's incentives separately, for each report of the other agent, with thresholds and payments that may vary with that report. Budget balance couples the two agents' payments at every type vector. The step that fails when attempted naively is going from "a threshold for each " to "one fixed threshold for each agent": the thresholds may lie outside the type interval, several degenerate configurations occur (an agent whose report never matters, a good that is always or never produced), and the printed proof treats the degenerate cases by assuming and leaves one of them "analogous". The closedness hypothesis is what makes the relevant minimal types exist; without it the boundary of the production set is not determined. Proposition 4.12 has the same structure with the seller's orientation reversed.
Fin 2 for the goal, and a pair (θS, θB) : ℝ × ℝ for bilateral trade. A deviation is Function.update θ i x for θ ∈ Θ; quantifying over θ ∈ Θ quantifies over .sInf/sSup of sets that are nonempty and closed whenever they are used.Contributions welcome: proofs of the characterization milestones (4.2, 4.5, 4.9), which the goal and Proposition 4.12 use; a proof of the goal covering the degenerate cases the book leaves to the reader; and the three-agent counterexample of p.90 as a separate statement.
Stock exchanges, commodity markets and trading platforms are institutions for trade between parties who each know something the other does not. The simplest version is bilateral trade: one seller, one buyer, one indivisible good, and each side privately knows its own value. The question is whether any trading institution can make the two trade exactly when trade is efficient, with both taking part voluntarily and without a subsidy from outside. Myerson and Satterthwaite (1983) showed that, apart from trivial cases, none can. The result is one of the basic impossibility theorems of economic theory. It explains why bargaining under private information is inefficient, and it is the benchmark every later analysis of double auctions and market design compares against.
This mission formalizes Section 3.4 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): the impossibility theorem, the pivot-mechanism argument that proves it, the second-best and profit-maximizing trading mechanisms, and the uniform example.
Timeline. Vickrey (1961) noted the tension between efficiency and budget balance in markets with private values. Chatterjee and Samuelson (1983) studied the sealed-offer double auction and its linear equilibrium for uniform values. Myerson and Satterthwaite (1983) proved the impossibility for general independent distributions with overlapping supports, and computed the second-best mechanism; for uniform values it coincides with the Chatterjee–Samuelson linear equilibrium. Börgers (2015) gives the pivot-mechanism proof formalized here.
A seller owns one indivisible good; a buyer may buy it. The seller's value has distribution with density on ; the buyer's value has distribution with density on . The two intervals are nondegenerate and may differ, and the values are independent. The seller's utility is if she sells for and if she keeps the good and receives ; the buyer's is if he buys and pays , and otherwise.
A direct mechanism is a trading rule on and transfers (received by the seller) and (paid by the buyer). Conditioning on one agent's type gives the interim trade probabilities , the interim transfers , and the interim utilities and . The mechanism is incentive-compatible if truthful reporting is a Bayesian equilibrium, individually rational if and for all types, ex post budget balanced if for every , and ex ante budget balanced if . A first-best trading rule trades when and not when , with any choice at ties. The seller's virtual cost is and the buyer's virtual valuation is ; the distributions are regular if both are increasing.
An incentive-compatible, individually rational and ex post budget balanced direct mechanism with a first-best trading rule exists if and only if
for some , exact budget balance , and the incentive-compatible payments with binding participation of and .
The theorem locates the source of inefficiency in bilateral bargaining in private information itself, not in any particular bargaining protocol: no mechanism, however clever, achieves efficient voluntary trade without a subsidy. It is the reason efficiency in markets is studied as a limit (large double auctions approach efficiency as the number of traders grows), and why a trading platform's fee structure is analyzed as a second-best problem. The pivot-mechanism argument is the same one that proves the impossibility of first-best public-goods provision (Proposition 3.7), so the two formalizations share their structure.
All results of this section are classical and proved on paper. None is formalized on Prove2Me, and Mathlib has no mechanism-design library. The platform has the Chatterjee–Samuelson linear equilibrium as an open statement about one particular game; this mission states results about all mechanisms. A complete development yields a reusable one-dimensional envelope/payoff-equivalence library for two agents with differently oriented types (the seller's incentive constraint runs from high types down), and the Lagrangian optimality argument for a linear objective under a single linear constraint.
The obvious attempt to prove impossibility looks for a contradiction between incentive compatibility and budget balance state by state. That fails: incentive compatibility and participation are interim constraints, so any single state admits budget-balanced transfers consistent with them, and the contradiction exists only after integrating over the prior. Two points need care. The seller's orientation is reversed: her trade probability is decreasing and her participation constraint binds at the highest type. And the deficit of the pivot mechanism must be shown to have positive probability, which uses that the supports overlap in a set with nonempty interior. The optimal-mechanism results additionally need that the trading rule implied by a Lagrange multiplier satisfies the monotonicity constraint, which is where regularity enters, and that a multiplier exists which makes the budget constraint bind.
A type vector is a pair θ : ℝ × ℝ with θ.1 the seller's and θ.2 the buyer's value. The prior is Lebesgue measure on with density . Densities are measurable, strictly positive on the closed supports and integrate to one; nothing else, such as continuity, is assumed. The trading rule is real-valued with values in on (deterministic, as in Definition 3.9). The measurability the book omits (Ch. 2 note 2) is built into the admissible class: , , are measurable with integrable transfers. "Increasing" is weak monotonicity, the book's convention.
Explicit formulas the statements carry: the first-best rule (3.61) with free tie rule, the pivot transfers of Definition 3.10, the rule (3.70) with parameter , the exact budget equation of Proposition 3.13 (ii), the payment formulas and , the profit rule , and the thresholds and .
The goal quantifies over every first-best trading rule and imposes budget balance as the ex post equality . Dropping budget balance, weakening it to , or fixing one tie rule would give a different, and in the first case false, statement. The pointwise "if and only if … for all " characterizations of Propositions 3.13–3.16 are stated with necessity almost everywhere, since an optimal trading rule is determined only up to null sets. For Proposition 3.14 necessity is also restricted to : under weak regularity that tie set can have positive probability, and profit does not depend on the trading rule there.
Contributions welcome: proofs of the milestones, a two-agent payoff-equivalence lemma for the seller's reversed orientation, and a sorry-free construction of the pivot mechanism's integrability facts.
Whether a community can finance a shared project out of voluntary contributions, when each member knows only her own benefit from it, is one of the founding questions of mechanism design. Bayesian mechanism design began with mechanisms for the provision of public goods: d'Aspremont and Gérard-Varet (1979) and Arrow (1979) showed that the efficient decision can be made Bayesian incentive compatible with a budget that balances in every state, provided agents cannot opt out. Once participation is voluntary, this is no longer possible, and Güth and Hellwig (1986) studied the best mechanism under that constraint. The same tension between efficiency, incentives, voluntary participation and budget balance drives the Myerson–Satterthwaite theorem for bilateral trade, which the next mission of this series formalizes.
This mission formalizes Section 3.3 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), which treats the public goods problem in the independent private values model with a continuum of types. The section proves an impossibility theorem for first best provision and then characterizes the best mechanisms that respect the budget: the welfare-maximizing (second best) mechanism and the profit-maximizing one, with a worked two-agent uniform example.
A community of agents , , decides whether to produce an indivisible, nonexcludable public good, , at cost . Agent pays a transfer and obtains utility . Her type is private information, drawn independently across agents from a distribution with density , strictly positive on the common support , . The type space is and .
A direct mechanism is a decision rule and transfer rules . For agent reporting , is the probability of production and the expected transfer, taken over the other agents' types, and . The mechanism is incentive compatible (IC) if for all , and individually rational (IR) if for all . It is ex post budget balanced if for every , and ex ante budget balanced if this inequality holds after integrating both sides against .
Welfare is . The first best decision rule is if and otherwise; a first best mechanism uses and transfers that add up to exactly in every state. The pivot mechanism uses and
The virtual valuation is , and is regular if is strictly increasing.
In the two cases on the right, producing is efficient for every type vector or for none; in every other case efficient provision cannot be financed voluntarily.
the budget binds, , and . 6. Proposition 3.9 (profit maximization): under regularity, the profit-maximizing IC and IR mechanism produces iff , with the same formula for . 7. Proposition 3.10 (Example 3.3: , uniform types on , ): the second best produces iff , where is the unique root in of if , and if . 8. Proposition 3.11 (same example): the profit maximizer produces iff .
Proposition 3.7 says that with voluntary participation no mechanism both takes efficient production decisions and pays for them, outside the degenerate cases. It is the reason the rest of the section, and much of the applied literature on public goods, studies constrained optimum mechanisms: Proposition 3.8 describes what the best budget-respecting mechanism gives up (it undersupplies the good, producing only when valuations exceed a bound strictly above the cost), and Proposition 3.9 quantifies the further distortion under a monopoly supplier. The example makes the three thresholds explicit and comparable.
All results of the section are classical and proved in the book, several of them only sketched there (Proposition 3.9 is stated without proof; Proposition 3.8 invokes an infinite-dimensional Kuhn–Tucker theorem whose applicability is not checked). None of them is formalized in Lean. The mission produces a machine-checked account of the envelope and revenue-equivalence arguments with interim expectations over independent types, a checked pivot-mechanism deficit computation, and a checked Lagrangian characterization; the uniform example additionally certifies the book's arithmetic.
The naive argument for the goal fails at the first step: a mechanism that implements with a balanced budget in every state is not obviously comparable to one that is only IC and IR, because IC constrains interim expectations while budget balance is ex post. The impossibility needs a reduction of the whole class of IC, IR mechanisms with rule to a single extremal one, which requires the payoff equivalence formula for interim utilities and an exact integral identity for expected revenue in terms of virtual valuations. The strict deficit of the pivot mechanism then needs a case analysis over which agents are pivotal and a positive-probability argument. For Proposition 3.8, pointwise maximization of a Lagrangian is not enough: one must show the multiplier exists and is positive, that the maximizer satisfies the monotonicity constraint, and that uniqueness holds only up to null sets.
Agents are Fin N with ; types are vectors in Fin N → ℝ; the type distribution is the product of the marginal measures on , which encodes independence. and integrate the decision and transfer rules against this distribution with agent 's coordinate overwritten by her report. Decision rules are deterministic, with values in on , as in Definition 3.4. Ties in the first best rule produce, as in the book's note 2 to Chapter 3; the second best and profit-maximizing rules use strict inequalities, as printed.
The book omits measurability and the existence of conditional expectations; the class of direct mechanisms here requires and each to be Borel measurable, each integrable, and each conditional expectation of given one agent's type to exist. The characterizations in Propositions 3.8–3.11 are stated in two directions: the stated rule, for every , is sufficient; necessity holds for almost every , since changing on a null set of type vectors changes nothing that is optimized. The explicit formulas the mission commits to are: the pivot transfers above; the second best rule with multiplier and the binding budget identity; ; the cubic for ; for ; and for the profit maximizer.
A trivializing formalization of the goal takes "first best" to mean only the decision rule ; the pivot mechanism would then be a witness in every case, so first best here also requires transfers adding up to exactly in every state.
Reusable infrastructure includes interim expectations over independent product distributions, the payoff and revenue equivalence lemmas for IC mechanisms, and the virtual-valuation identity for expected revenue; these are shared with the auction and bilateral trade chapters of the series. Contributions to any milestone, and to general lemmas about product measures with densities on boxes, are welcome.
A seller with one indivisible good and several potential buyers, each of whom privately knows how much the good is worth to them, has to choose a selling procedure: a posted price, an English auction, a sealed-bid auction with a reserve price, or something more elaborate. Which procedure raises the most expected revenue? Myerson's answer (Myerson 1981) is the foundation of optimal auction design. It underlies reserve-price setting in practice, the analysis of sponsored-search and ad-exchange auctions, and the modern algorithmic mechanism design literature, which treats Myerson's auction as the benchmark against which simple and approximately optimal auctions are measured.
This mission formalizes Section 3.2 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), the textbook treatment of Myerson's result in the independent private values model with Bayesian incentive compatibility. It is the second mission of a series covering the book.
Timeline. Vickrey (1961) showed that the second-price auction makes truthful bidding a dominant strategy and compared auction formats. Myerson (1981) characterized the revenue-maximizing mechanism for independent private values with possibly asymmetric distributions; Riley and Samuelson (1981) obtained the symmetric case and the optimal reserve price independently. The revelation principle in the Bayesian form used here goes back to Myerson (1979) and Dasgupta, Hammond and Maskin (1979).
There are potential buyers . Buyer values the good at ; if he receives it and pays his utility is , and otherwise . The seller's utility is . The valuations are independent; has cumulative distribution function and density with on the common support , where . The type space is and the joint density is .
A direct mechanism asks buyers to report their types and consists of an allocation rule , where , and payment rules . Its interim quantities are the expected allocation probability, payment and utility of buyer conditional on his own type:
The mechanism is incentive-compatible if for all (truth-telling is a Bayesian Nash equilibrium) and individually rational if for all . The virtual valuation of buyer is
and the distribution is regular if is strictly increasing.
Under regularity, among all incentive-compatible and individually rational direct mechanisms, a mechanism maximizes the seller's expected revenue exactly when, for every buyer ,
the allocation identity holding for almost every ; and such a mechanism exists.
The theorem identifies the revenue-maximizing selling procedure among all procedures, not among a parametric family: by the revelation principle, no auction format, however elaborate, and no equilibrium of it can beat the mechanism of Proposition 3.4. Its consequences include the optimality of first- and second-price auctions with reserve price when buyers are symmetric, the revenue equivalence of standard auction formats, the fact that an asymmetric optimal auction may sell to a buyer without the highest value, and the monopoly inefficiency that the optimal seller sometimes withholds the good. The envelope characterization of Bayesian incentive compatibility (Proposition 3.2) is the tool reused throughout the rest of the book, in public goods provision, bilateral trade and dynamic screening.
The result is classical and fully proved in the literature. What is missing is a machine-checked version at this generality: asymmetric distributions, an arbitrary lower support end , Bayesian (interim) rather than dominant-strategy constraints, and optimality over all incentive-compatible and individually rational mechanisms. Existing formalizations on the platform treat the i.i.d. case with values on .
The obvious argument maximizes the virtual surplus pointwise and declares victory, but this ignores that the seller's feasible set is constrained by monotonicity of every ; the pointwise maximizer is feasible only because regularity makes increasing, and that has to be proved for the interim probabilities, which integrate over the other buyers' types. The revenue identity links interim payments, which integrate over the other buyers' types, to an integral over the whole type space weighted by the virtual valuation, and it is only valid for mechanisms whose lowest types' payments are pinned down. The necessity direction requires showing that ties and zero virtual values are null events, which rests on strict monotonicity of every and on the absolute continuity of the type distribution. Finally, the envelope step requires convexity and almost-everywhere differentiability of , with care at the endpoints of the type interval.
Buyers form a finite type with at least two elements. The prior is the measure on with density on and no mass outside it; each is measurable, strictly positive on and integrates to ; . Allocation and payment rules are total functions whose values on are constrained, and , are prior expectations with the -th coordinate fixed. "Increasing" is weak monotonicity, as in the book; regularity is strict monotonicity of on (Assumption 3.1).
The following conventions are committed to:
The envelope and payoff-equivalence lemmas, and the revenue identity, are reused in later missions of this series, so proofs of the milestones are welcome independently of the goal.
A seller with one good and one buyer whose valuation she does not know faces the simplest problem of mechanism design: choose a selling procedure, anticipating that the buyer will act in his own interest given what he knows. The textbook answer, "post the monopoly price", is usually derived by optimizing over prices alone. The question that opens Börgers' An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015, doi:10.1093/acprof:oso/9780199734023.001.0001) is whether the seller could do better with anything else: negotiation, lotteries, menus of price–probability pairs, or any extensive game she can commit to.
Chapter 2 answers this for one buyer, and in doing so introduces the tools the rest of the book, and most of auction theory, reuse: the revelation principle, the envelope characterization of incentive compatibility, payoff and revenue equivalence, and the virtual valuation. The book's exposition of §2.2 follows Manelli and Vincent (2007), and the nonlinear pricing model of §2.3 is due to Mussa and Rosen (1978, doi:10.1016/0022-0531(78)90085-6); both attributions are the book's own (§2.5, p.29).
The buyer's type is his valuation for the good. His utility is if he receives the good and pays , and if he only pays . The seller's belief about is a cumulative distribution function with density on an interval , , with throughout and .
A direct mechanism is a pair , : the buyer reports a type , receives the good with probability and pays . Write . The mechanism is incentive-compatible if for all , and individually rational if for all . The seller's expected revenue is .
For the extreme-point argument, denotes the space of functions on with the norm, and the set of increasing functions with values in . A point of a convex set is an extreme point if for every at least one of , lies outside .
In the nonlinear pricing model of §2.3 the good is divisible, quantity costs the seller with , and the buyer's utility is , with , , , and . The seller maximizes expected profit . The distribution is regular if the virtual valuation is increasing.
If , then the mechanism
maximizes expected revenue among all incentive-compatible, individually rational direct mechanisms. The comparison class contains every randomized rule with values in ; the statement fixes no distribution and no constant.
Proposition 2.5 says that the elementary monopoly price is not a restriction of the seller's options but the solution of the unrestricted design problem, including every lottery and every indirect procedure. Its one-buyer argument is the template for Myerson's optimal auction (Chapter 3 of the book), whose revenue formula is the multi-buyer form of Lemma 2.4. Proposition 2.6 exhibits the two standard features of screening, no distortion at the top and downward distortion below, which recur in regulation, insurance and contract theory.
All results of the chapter are classical and proved in the book. None of them is formalized on Prove2Me, and Mathlib has neither the revelation principle, the envelope lemma for incentive-compatible mechanisms, nor a maximum principle for linear functions on compact convex sets (Mathlib has the Krein–Milman lemma, IsCompact.extremePoints_nonempty, but not Bauer's maximum principle). The mission therefore produces the first machine-checked foundation for the one-agent screening model on which chapters 3, 4 and 11 of the book build.
The obvious argument for the goal compares the posted price with other posted prices; that comparison is one line and is not the theorem. The content is the comparison with randomized mechanisms: an arbitrary increasing with values in may do better than every deterministic threshold rule unless one shows that expected revenue is linear in and that its maximum over the infinite-dimensional set is attained at an extreme point. That step needs compactness of in and a maximum principle on compact convex sets in a normed space, neither of which is finite-dimensional linear programming. The envelope step (Lemma 2.3) needs absolute continuity of a convex function on a closed interval, including its endpoints, where need not be differentiable. For Proposition 2.6 the pointwise maximizer of the virtual surplus must be shown to be monotone and to satisfy incentive compatibility, which is where regularity enters.
Types are real numbers; every function of the type is a total function and every condition quantifies over only. "Increasing" means weakly increasing (the book's note 3). The distribution is a structure carrying the density , positive and integrable on with total mass , and tied to it by . No measurability or integrability hypothesis is placed on mechanisms: incentive compatibility makes monotone and bounded and measurable, so every expected revenue is a genuine integral.
The explicit formulas are part of the statements: the posted-price mechanism of Proposition 2.5 with ; the payment formulas of Lemmas 2.3–2.4 and Proposition 2.2; in Lemma 2.5; and in Proposition 2.6 the two-case rule for and the payment . The goal fixes , for existence and quantifies over every incentive-compatible, individually rational completion at the tie.
The space is of almost-everywhere classes, because the book's "norm" on bounded functions vanishes on null functions; is the set of classes with an increasing -valued representative, and Lemma 2.7 is an almost-everywhere statement, as the book's notes 4–6 already indicate. Proposition 2.4 is stated for a nonempty compact convex set in a real normed space and a linear map continuous on that set. The revelation principle models a general mechanism as the buyer's reduced strategy set, an arbitrary type, with a purchase probability and an expected payment for each strategy.
A goal that compared the posted price only with other posted prices, or only with deterministic mechanisms, would be trivial and is excluded: the competitors range over all incentive-compatible, individually rational direct mechanisms with valued in .
Reusable beyond this mission: the one-agent envelope and revenue-equivalence lemmas (needed again in Chapters 3, 4 and 11), compactness of monotone functions in , and the maximum principle for linear functions on compact convex sets. Contributions to any of these are welcome.
Wasserstein distributionally robust optimization replaces an unknown data-generating distribution by the set of all distributions within a prescribed optimal-transport distance of a reference distribution, typically the empirical distribution of training samples. The inner problem of every such model is a linear optimization over this set: maximize the expectation of a loss function over all probability measures in a Wasserstein ball. The same problem appears when classification, clustering or generative models are regularized against overfitting to the training samples (Kuhn et al. 2019, Blanchet & Murthy 2019, Gao & Kleywegt 2016).
Whether this problem has a finite value, whether that value is attained, and whether it is attained by a measure with few atoms determine whether it can be solved by finite-dimensional optimization. Earlier answers appeared under differing hypotheses. Wozabal (2012) used the Richter–Rogosinski theorem to obtain solutions on at most atoms, Owhadi & Scovel (2017) improved this to , and Gao & Kleywegt (2016) obtained the sharp bound through first-order optimality conditions of the dual problem. Yue, Kuhn & Wiesemann (2022) give short, self-contained proofs of weak compactness, finiteness, attainment and -sparsity under conditions that are easy to check. This mission formalizes that paper.
Let be a proper metric space: every closed ball is compact. Such a space is complete and separable. is the set of Borel probability measures on , with the weak topology of convergence against bounded continuous functions.
For and , a coupling is a measure on with marginals and . The set of couplings is . The Wasserstein distance is
It is defined for every pair of probability measures, and it is for some pairs. The Wasserstein ball of radius around is . A measure has a finite -th moment if for some .
Given an upper semicontinuous , the paper studies
under the standing assumption that for every in the ball at least one of and is finite. The integral is . The optimal value is finite if it is neither nor , and attained if some achieves it.
Let with distinct , and . Suppose there are , and with for all . Then there exist and with such that
The bound cannot be improved in general (Kuhn et al. 2019, Example 5).
A further item, Observation 1, shows that properness is necessary: if every Wasserstein ball over a Polish space is weakly compact, the space is proper.
Theorem 4 turns problem (3) with an empirical reference measure into a finite-dimensional problem over support points and weights. Many reformulations and algorithms for Wasserstein DRO rest on this sparsity. Theorems 2 and 3 give checkable growth conditions for finiteness and attainment, and their hypotheses differ only in whether the growth exponent is or strictly smaller. The paper cites Kuhn et al. 2019, Example 4 for an instance with a finite but unattained value. Theorem 1 is a compactness statement for Wasserstein balls over a non-compact space, of use well beyond optimization.
All results are proved in the paper. None is known to be formalized. Mathlib has Prokhorov's theorem, tightness and the weak topology on probability measures, but no Wasserstein distance on a general metric space, no couplings, and no theory of extreme points of moment sets. Formalizing this paper builds those foundations.
The ball is not weakly closed in an obvious way: is only lower semicontinuous for weak convergence. Tightness has to come from a moment bound (Lemma 1), which needs the triangle inequality for on measures without finite moments. The integral is not weakly upper semicontinuous for unbounded , so compactness alone does not give attainment. That failure is exactly what the example with growth of order shows. For sparsity, the natural idea is Carathéodory or Richter–Rogosinski: marginal constraints, one cost constraint and one optimality condition give moment conditions, one atom too many. Reaching needs an extreme-point argument for an infinite-dimensional linear program, a separate case for an inactive cost constraint, and attainment for a relaxation whose feasible set is not obviously compact.
The Lean development lives in the namespace WassersteinLinOpt.Ball. carries [MetricSpace X] [ProperSpace X] [MeasurableSpace X] [BorelSpace X], and is ProbabilityMeasure X with its standard topology. Weak compactness is IsCompact, which agrees with the paper's sequential notion because is metrizable. wassersteinDist is valued in ℝ≥0∞, with couplings given by Measure.map Prod.fst/Prod.snd, and the ball is wassersteinDist p μ ν ≤ ENNReal.ofReal r with 0 < r. The objective quasiIntegral is computed in EReal from two lower Lebesgue integrals, and the optimal value is an EReal supremum. Every theorem about (3), (10) or (11) carries the paper's quasi-integrability hypothesis, because EReal evaluates to . "Finite" means ≠ ⊤ ∧ ≠ ⊥. "Attained" means a member of the feasible set whose value equals the supremum. The feasible set of (11) requires Integrable (φ i) γ, so the Bochner integral's value on non-integrable functions cannot create feasible points. Extreme points of a set of measures are defined directly, because measures form a cone and not a real vector space. atoms means Fin (N+1)-indexed points and non-negative weights.
A formalization that replaces the extended-real objective by a Bochner integral, drops the quasi-integrability or hypotheses, weakens "attained" to "the supremum is finite", or replaces " atoms" by "finitely supported" states a different theorem. None of these is acceptable. Solvers must not add hypotheses such as the triangle inequality for or existence of optimal couplings; these are facts to prove.
A complete development needs the triangle inequality and lower semicontinuity of , existence of optimal couplings, density of finitely supported measures in , continuity of marginal maps, and the extreme-point theory of moment sets. All of these are reusable beyond this mission, and contributions of any of them are welcome.
Assumptions of Physics by Gabriele Carcassi and Christine A. Aidala (book, v3.0, 2025) is a programme to derive the mathematical structures of physical theories from explicit physical requirements. Part II, "Physical Mathematics", begins (Chapter 1) by making precise what it means for a statement to be experimentally verifiable, and shows that a single physical requirement (only countably many tests can be run in an indefinite amount of time) is enough to force the familiar structures of point-set topology onto the space of outcomes of any experiment. This mission formalizes that chapter. It is the first mission of a series on the book; all declarations live in the namespace AssumptionsOfPhysics so that later missions can build on them.
A logical context is represented by its set of possible truth assignments, and a statement (up to logical equivalence) by its truth set . Negation, conjunction and disjunction are complement, intersection and union; the certainty is and the impossibility is ; " is narrower than " means , and are compatible when .
An experimental domain is a family of statements that contains and , is closed under finite conjunction and countable disjunction, and has a countable basis : every element of is obtained from by finite conjunctions and countable disjunctions. Its theoretical domain is the closure of under negation, finite conjunction and countable disjunction. A possibility is a non-impossible that, for every , is either narrower than or incompatible with it; denotes the set of possibilities. The verifiable set of a statement is , and the natural topology on is the topology generated by . A domain is decidable if it is closed under negation.
The chapter's results identify the open sets of a topology with verifiable statements and its points with complete experimental answers (possibilities). Second countability and the axiom are thereby derived rather than assumed, and the cardinality bound limits which mathematical objects can carry experimental meaning. Later chapters of the book (domain combination, properties and quantities, ensemble spaces) rely on these facts. The results are proved informally in the book; no machine-checked formalization of them is known to the drafters. A formalization fixes the precise hypotheses under which they hold (for instance, whether a basis must be countable in Propositions 1.46, 1.48 and 1.60) and provides a reusable library for the rest of the series.
The individual statements are elementary, but several of the book's proofs are informal about two points that a formal proof must handle. First, the possibilities must be shown to cover the space of assignments and to be atoms of ; the book argues through minterms of a countable basis, which needs a "disjunctive normal form" for countably generated families. Second, the natural topology is defined via arbitrary unions while experimental domains are only closed under countable disjunction; showing that every open set is still of the form (Proposition 1.57) requires a second-countability / Lindelöf-type argument rather than direct closure.
Statements are subsets s : Set Ω of an arbitrary type Ω (possibly empty); the experimental domain is the structure ExperimentalDomain Ω, whose field stmts is the family . Generation by finite conjunction and countable disjunction (FinConjCountDisj) includes the empty conjunction and the empty disjunction ; generation with negation (NegFinConjCountDisj) includes . Possibilities form the type D.Possibility, which carries the natural topology as an instance; topological notions (SecondCountableTopology, T0Space, T1Space, DiscreteTopology) are Mathlib's. The primitive notion of verifiability (Axiom 1.27) is not modelled separately: membership in is what all results of the chapter use. Statements involving "a basis" quantify over every basis (countable or not), as in the source. Contributions of reusable lemmas, in particular a disjunctive-normal-form lemma for countably generated families of sets, are welcome.
Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) solves a discrete gold-mining process: a single machine can be used in one of two mines, each use extracts a fixed fraction of the gold remaining in that mine, and each use carries a fixed risk of destroying the machine. Maximizing the expected total gold leads to an index rule: work the mine whose ratio of expected yield to risk is larger. Chapter VIII, A Continuous Stochastic Decision Process, passes to continuous time. Decisions are taken at every instant, and effort may be divided between the mines. The optimal policy is characterized by first-order conditions on switching functions, the objects of Pontryagin's later maximum principle.
It is also an early continuous-time index policy of the kind later central to bandit theory. Chapter VIII treats two mines, then a third decision that works both mines at once.
Mine A holds units of gold and mine B holds . At time a proportion of the machine's effort goes to A and to B (Eq. (7.3)). With the gold remaining, the probability that the machine still works and the expected gold mined, the process is defined by Eq. (7.2):
with , , , . The mining rates and the failure rates are positive. The objective is the expected total gold .
In the three-choice problem (§ 12) a third decision removes gold from A at rate and from B at rate , and fails at rate . A control is a triple with (Eq. (12.2)). For a horizon , the switching functions of Eq. (12.5) are computed along a control. For instance,
They measure the first-order gain from shifting effort towards each decision at time . The linear forms
and the quantity (Eqs. (13.2)–(13.3)) organize the analysis.
For the two-choice process, the maximum of is attained by the policy
The formal statement asserts that some admissible control follows this rule along its own trajectory, and that every such control maximizes over all measurable controls with values in .
Theorem 1 gives a closed-form optimal feedback policy for a continuous-time stochastic scheduling problem. The policy depends only on the slope , and on the line it is a mixed (chattering) policy: the discrete optimum becomes a mixture in the continuous limit. Lemmas 1–5 are a hand-made maximum principle for controls that enter linearly, read almost everywhere. "Theorem 8" says exactly when a composite decision is useless: means that removes gold at a higher failure cost than an equivalent mixture of and .
On the formal side, none of these results is formalized anywhere. Mathlib has no theory of controlled differential equations or of necessary conditions for optimal control. The platform's maximum principles (BertsekasDP.pontryagin_minimum_principle, VectorSpaceOpt.pontryagin_minimum_principle) assume smooth dynamics and a finite horizon with differentiable costs. They do not cover this process, with measurable controls and an improper-integral objective. A formal proof of Theorem 1 would be a complete optimality proof for a continuous-time index policy with chattering controls. The book's argument for Theorem 1 is partly informal; a complete proof, by that route or another, is the target.
The optimization is over an infinite-dimensional set of measurable controls on an infinite horizon, and the objective is not concave in the control. The first-order conditions of §§ 8–9 are necessary, not sufficient, so they do not by themselves prove that the rule is optimal. The book's argument combines them with qualitative facts (the rule is used thereafter once used above the line, and is preferred near the -axis). Making this rigorous requires comparing an arbitrary control with the rule, not just perturbing near an optimum. It is also not known in advance that an optimal control exists, so arguments of the form "let be optimal" need an existence step or a direct comparison. For the lemmas, the switching functions must be shown absolutely continuous, with the derivative formulas (13.1) holding almost everywhere, before "equal on an interval" can be turned into " on the interval".
0, 1, 2 for .Useful infrastructure: the derivative formulas (13.1) for the , a first-variation lemma for under bounded perturbations of a measurable control, and a comparison principle for deteriorating projects. The last is reusable for other continuous-time index policies. Proofs of any milestone, and alternative arguments for Theorem 1, are welcome.
The optimal inventory problem asks how much of an item to stock when demand is random, ordering costs money, and running short costs more. Arrow, Harris and Marschak formulated it as a sequential decision problem in 1951 (Optimal inventory policy, Econometrica 19), and Dvoretzky, Kiefer and Wolfowitz studied its structure in 1952–53. Chapter V of Richard Bellman's Dynamic Programming (1957) treats the problem through a single functional equation for the minimal expected discounted cost. It shows that when ordering and shortage costs are proportional to quantity, the optimal policy is described by one number, a constant stock level , computed from the demand distribution alone.
This result is an early form of the base-stock (order-up-to) policy. Base-stock policies are the standard structure in periodic-review inventory theory: Karlin (1958), Scarf's theorem (1960) and Veinott (1965) extend it. Chapter V is also a worked example of a point the book makes throughout: the method of successive approximations determines the shape of an optimal policy, and not only its existence.
A single item is stocked over an unbounded sequence of periods. At the start of a period the stock is . The decision maker orders up to a level , at cost with . A demand then arrives, with probability density : for , , and . If , the next period starts with stock . If , the excess is bought at the penalty rate and the next period starts with stock . Costs one period ahead are multiplied by a discount factor .
Write for the minimal expected discounted cost from stock . Enumerating the cases gives Bellman's equation (5.1):
A policy assigns an order-up-to level to each stock . It is optimal when attains the minimum. The mission takes the equation itself as the model; no stochastic process is built.
The equation has exactly one solution among measurable functions bounded on . If , the equation
has exactly one root , and for every the minimum is attained at
If , the minimum is attained at : never order.
is its absolute minimum.
The theorem reduces an infinite-horizon stochastic control problem to a scalar equation. Rewriting it as gives the critical-fractile form familiar from the newsvendor problem, with the discount factor entering the fractile. The level depends on the demand law only through its distribution function, and the policy does not depend on the current stock except through . This is what makes the policy implementable and its parameters estimable from data, the point Bellman makes in § 1. Theorem 3 shows the same structure over a finite horizon, with levels that rise as more periods remain. Theorem 4 marks where the structure starts to depend on the demand density.
As far as a search of the platform shows (queries recorded in the mission files), none of these results has a machine-checked proof. Base-stock theorems on the platform, Veinott's multi-product theorem and Gallego–Özer's advance-demand model, use discrete periods, different excess-demand conventions and different state spaces. They do not cover a continuous-demand, lost-sales-at-penalty, discounted functional equation. Formalizing Chapter V would produce an explicit solution of a nonlinear integral equation of renewal type, a uniqueness theorem for that equation, and a Lean treatment of the renewal equation that other applied-probability missions can reuse.
Two steps resist the obvious argument. First, the minimization is over the unbounded set , and the unknown enters through a convolution with . The operator is a contraction on bounded functions, which settles uniqueness in the bounded class. Uniqueness among functions bounded only on finite intervals (Chapter IV's class) is not a contraction statement, because the minimization reaches arbitrarily far to the right. Second, optimality of for requires to be nondecreasing on . There is defined only implicitly, as the solution of a renewal-type equation, and this monotonicity is a positivity statement about that solution, not a consequence of the first-order condition. Checking that the first-order condition holds at is not enough, and neither is checking that the candidate function satisfies the equation at the single level .
Functions are ℝ → ℝ; only their values on enter. Integrals over are Lebesgue integrals and are interval integrals. The equation is stated with an infimum (IsGLB), as Chapter IV writes it, and every policy statement asserts that the minimum is attained (IsLeast) at the stated level. Uniqueness is asserted on (Set.EqOn … (Set.Ici 0)). Solution classes require measurability. This is the standing convention that makes meaningful; without it a non-measurable function would make the integral default to . "" is read as positivity on .
Conventions and corrections, each stated in the items:
A trivializing formalization is ruled out. The goal does not assume the stated policy is optimal, does not assume is given, and does not take as a hypothesis. It asserts the existence of the root, the existence and uniqueness of the solution, and attainment of the minimum at for every .
Theorems 2 (two items, joint density), 5 (one-period delivery lag) and 6 (strictly convex ordering cost) are not part of this mission. Theorem 2 is printed with a sign error in (6) and garbled marginals. Theorem 5 states no hypotheses. Theorem 6's (9b) contradicts itself at . Welcome contributions include a Lean library for the renewal equation (existence by successive approximation, positivity, differentiation under the convolution), which Theorem 9 needs and which is independent of inventory theory, and the contraction estimate for on bounded measurable functions.
Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) treats the stochastic gold-mining process, the first stochastic multi-stage decision process of the book whose optimal policy can be written down in closed form. There Bellman introduces decision regions, the sets of states at which a given first choice is optimal, and where he obtains an index rule: at every state, compute one number per alternative and choose the largest. The same kind of rule was later developed in general form as the Gittins index for multi-armed bandits (Gittins 1979), and the gold-mining process is an early instance of what that literature calls a deteriorating bandit, in which each alternative's index can only decrease when it is used.
Bellman first described the process in his 1954 survey The theory of dynamic programming, with the two-mine index rule stated as Eq. (8.3), and it appears on Prove2Me in a mission on that paper. The book gives the full chapter: existence and uniqueness, the rule for two mines, its extension to several outcomes per use and to any number of mines, the finite-horizon process, and a stability estimate.
Two mines, Anaconda and Bonanza, hold amounts of gold and . A single machine is used in one mine at a time. Used in Anaconda, it mines the fraction of the gold there and stays in working order with probability , or is destroyed without mining anything with probability . Bonanza has the corresponding data and . Before each use the operator chooses a mine (choice A or B), and the process stops when the machine is destroyed. The aim is to maximize the expected total amount of gold mined.
The expected return under an optimal policy satisfies the functional equation
where is the return of an A-choice followed by optimal continuation and that of a B-choice. The -stage returns are and . The A-region of a value function is the set of points of the closed quadrant where the A-branch attains the maximum; the B-region is defined in the same way.
In the generalization, a use of mine has outcomes: outcome occurs with probability , yields and leaves in the mine, and is the probability that the machine is destroyed. With mines the equation is
"The solution" of an equation always means its unique solution in the class of functions bounded in every rectangle , (or every box ), per Bellman's footnote 7.
Under , , , , equation (4) has a unique solution bounded on boxes, and at every state any index maximizing
attains the maximum in (4). Ties among the maximizers may be broken arbitrarily.
The index rule reduces the choice among mines to computing numbers. Each one depends only on its own mine, as the ratio of immediate expected gain to immediate expected loss. Without the theorem, an optimal policy for the -stage process is a word in letters whose number of candidates grows like . The finite-horizon theorems show that the same rule is exactly optimal for every horizon beyond a finite , and the stability theorem bounds how much the solution moves when the equation is perturbed.
Theorem 2's content is also the target of the 1954-paper mission, where it is stated for the supremum of expected returns over choice sequences. Those statements (BellmanTheoryDP.GoldMining.gold_mining_decision_rule, …optimal_return_functional_equation) are included here as reference items. They concern a different object: the book's theorems are about the unique bounded solution of (5.1), and the two coincide once (5.1) is known to characterize the optimal return. None of the chapter's results has a machine-checked proof on the platform yet. The -mine rule (Theorem 4) and the finite-horizon results (Theorems 5 and 6) are not stated anywhere on the platform.
The equation for the boundary between the regions involves the unknown function , so equating the two branches of (5.1) does not by itself locate the boundary. Comparing the orders "A then B" and "B then A" determines the index line, but only on the assumption that there are just two regions. Bellman's Figure 1 shows why that assumption carries real content: homogeneity alone only makes the regions unions of sectors, which could alternate. The assumption is not automatic either. In § 13 a third, compromise choice is added, and a counterexample shows that the three-choice problem need not have the analogous three-sector structure. For the finite-horizon process the boundary ray of generally differs from the index line, and Theorems 5 and 6 are statements about how it differs.
Namespace BellmanDP.GoldMining. Values are real functions ℝ → ℝ → ℝ (two mines) or (Fin n → ℝ) → ℝ (n mines); equations are imposed only on the closed quadrant or orthant, and uniqueness means agreement there. Mines are Fin n with added (with no mine the maximum in (4) is empty). Outcomes are Fin K (Theorem 3's ). A maximum over two branches is max, and a maximum over mines is encoded as "every alternative is at most and one equals it". The class "bounded in any rectangle" is BoundedOnRectangles, and for mines it is BoundedOnBoxes. The -stage returns are goldIter N, with goldIter 0 = 0 so that goldIter 1 is the book's .
Choices made explicit:
A statement of the index rule that assumes the index policy's return satisfies (5.1) and calls it "the solution" without the bounded-class uniqueness would prove nothing about optimality. Here every theorem is about solutions in the bounded class, whose uniqueness is Theorem 1 (and part of the goal).
Contraction estimates on rectangles (Theorems 1 and 7) are reusable across the other functional-equation chapters of this series. Proofs of the goal via general index theory are welcome, provided they discharge the statements as written.
Many optimization routines contain an inner step that maximizes a function of one variable whose values are expensive to compute: a line search inside a multivariate method, a tuning parameter chosen by simulation, a stage of a dynamic program in which each evaluation requires solving a subproblem. When the only structural information is that the function has a single peak, the natural question is how to place the evaluations so that the peak is pinned down as tightly as possible with a fixed budget. Richard Bellman's Dynamic Programming (1957) takes up this question in Chapter I, § 22, as an illustration of the functional-equation method, and answers it with the Fibonacci numbers.
Timeline.
Let . A function is strictly unimodal with maximum at if is strictly increasing on and strictly decreasing on . No continuity is assumed, and the peak may sit at an endpoint. The point is then the unique maximizer of .
A search procedure is a finite decision tree. At each internal node it names a point at which is evaluated and moves to a subtree chosen by the observed value ; at a leaf it announces a closed interval . The -th evaluation point may depend on all values seen so far, but on nothing else about . The cost of the procedure on is the number of evaluations along the path that determines.
The procedure locates the maximum on within unit length using at most values if, for every strictly unimodal on with maximum at , it evaluates at most times and announces with and . Write for the set of lengths for which such a procedure exists, and following Bellman's Eq. (22.1),
The book's Fibonacci numbers are , for (in Lean, bookFib).
In the discrete version, is defined on the points , strictly increasing up to its maximizer and strictly decreasing after it. is the largest for which some procedure evaluates at most values and then names exactly, for every such .
The supremum is not attained once (with two evaluations every length is searchable, the length is not), which is why the statement is about the supremum rather than a maximum.
The result. Theorem 11 is an exact minimax statement: evaluations shrink the interval of uncertainty for the peak of a unimodal function by a factor of at most , and no adaptive rule, however clever, does better. It certifies Fibonacci search as optimal and golden-section search as asymptotically optimal, which is the reason these methods are the default line searches when derivatives are unavailable. Eq. (22.4) quantifies the rate: twenty evaluations give four decimal digits.
Formalizing it. The theorem has been proved since 1953; the work here is a machine-checked proof of the full minimax statement over all adaptive procedures, including the lower bound. That half is a statement about every decision tree and requires an adversary argument, which is exactly the kind of reasoning that is informal in the book and easy to get wrong. The discrete Theorem 12 is misprinted in the book (see below), so a formal proof also settles the correct values. We are not aware of an existing formalization of the optimality of Fibonacci search in Lean or another proof assistant. The Binet formula and the ratio limit are in Mathlib for Mathlib's indexing (Real.coe_fib_eq, tendsto_fib_succ_div_fib_atTop); milestone 6 only transfers them to the book's indexing.
The upper bound must hold for every procedure, not only for procedures that follow the "compare two points, discard a piece, keep the surviving point" pattern of the book's figures. A procedure may place its second point depending on the first value, may re-evaluate points, may evaluate outside , and may branch on the exact values rather than on their order. The book's argument tacitly restricts to that pattern, so the lower bound has to be established for arbitrary trees, where the information carried by exact values, repeated or wasted evaluations and branch-dependent placements all have to be accounted for. The bookkeeping is delicate because the surviving sets are half-open or open intervals, and whether the endpoints are included decides that the supremum is not attained.
The naive attempt of proving a bound only for "one new point per step inside the current bracket" procedures does not prove the goal: the goal quantifies over all decision trees.
ℝ → ℝ, constrained only on ; evaluations outside are allowed and useless.bookFib with ; in Mathlib's indexing is Nat.fib (n + 1). The goal is stated for every ; the book calls a convention, and in this model agrees with it.IsLUB, never as "a procedure exists for ", which is false for . Theorem 12 is stated with IsGreatest, which asserts that the maximum exists.Many routing problems come with a hard limit on distance or time rather than a requirement to visit everything. A repair crew with a fixed shift wants to service as many stations as possible; a vehicle with a fixed range wants to cover as many customers as possible. The budgeted prize-collecting traveling salesman problem captures this: given edge costs and a budget, find a closed tour of cost at most the budget that visits as many vertices as possible. Paul, Freund, Ferber, Shmoys and Williamson met the problem in work with New York City's bikeshare system (Paul et al., Math. Oper. Res. 2020).
The problem is NP-hard, and the question is how close a polynomial-time algorithm can come to the optimum. Before this paper, the best guarantee for the rooted tour version was , obtained from the orienteering algorithm of Chekuri, Korula and Pál (reference [6] of Paul et al.), with running time . Paul et al. give a parameterized primal-dual algorithm with guarantee exactly 2, in the style of the Goemans–Williamson primal-dual method for prize-collecting Steiner trees and tours (Goemans and Williamson, SIAM J. Comput. 1995). The analysis rests on one upper bound on the optimum, Theorem 1 of the paper, which this mission formalizes.
An instance consists of an undirected graph on a finite vertex set, not necessarily complete, edge costs , a budget and a root . A feasible tour is a closed walk in that starts and ends at and whose cost, the sum of over its edges counted with multiplicity, is at most . Vertices may be revisited. The tour's vertex set is written .
A dual vector assigns a real number to every . For an edge , means that has exactly one endpoint in . The potential of is
and is neutral when .
The primal-dual subroutine PD(), for a parameter , starts with , no tight edges, and every singleton an active component. It raises at unit rate for all active components at once, until an event happens: either an active set becomes neutral and is marked inactive, or the dual constraint of an edge between two different components becomes tight. In that case is added to the forest and the two components merge into one active component. The process stops when no set is active. Simultaneous events are processed in an arbitrary order. The family collects every set that was ever active, including for zero time, and .
In the Lean development the instance is BudgetedPCTSP.Rooted.Instance, tours are
SimpleGraph.Walks from r to r, the potential is potential, and PD() is the event
relation PDStep with final states IsCompleteRun. The family is sPlus.
Fix . PD() has a complete run. For every complete run, under every order of breaking ties, every feasible tour with vertex set , and the minimal set of containing :
In the order a proof would take them:
Theorem 1 is the dual-fitting half of the paper's 2-approximation. Together with the lower bound on the tour the algorithm builds (Theorem 2), and the threshold choice of (Lemma 2), it yields the main result, Theorem 3: the parameterized primal-dual algorithm is a 2-approximation for the rooted budgeted prize-collecting TSP. The paper extends the analysis to the weighted, tree and unrooted variants in Section 8, stating that the proofs continue to hold.
The result is proved in the paper; it has not been formalized. This mission produces a precise, checkable model of a Goemans–Williamson-style moat-growing process: a discrete event semantics for a continuous dual-ascent process, with every tie-breaking order admitted. That model is reusable for the rest of the paper (the threshold analysis, the tour construction and Theorem 3) and for other primal-dual approximation algorithms built on the same process, such as prize-collecting Steiner tree.
The paper states the process continuously and argues about it informally ("raise uniformly … until"). A proof must turn the invariants it relies on into statements about every reachable state of a discrete process in which event times are recomputed after each event and ties are broken arbitrarily. The paper gives one-sentence justifications for dual feasibility and laminarity and a two-line proof of Lemma 1; none of them addresses zero-length events, ties, or the fact that the next event time is only known to be nonnegative once these same invariants hold. Laminarity has to hold for the whole family of ever-active sets, not only for the current partition.
In the goal itself, the step that goes beyond bookkeeping is a counting argument. It relates the dual mass of sets inside the minimal set to how often a closed walk crosses those sets. A closed walk is a list of edges with repetitions, not a set, and the obvious set-based count does not apply to it directly.
SimpleGraph on a Fintype vertex type with decidable equality. Costs are a
real function on Sym2 V, nonnegative on edges; budget ; a root . Unit prizes only.
The weighted problem (Theorem 4), the tree problem (Theorem 5) and the unrooted problem
(Section 8) are out of scope.Finset V, tight edges and the family
. One step raises all active duals by the minimum event time and processes
one event whose time is . Any tied event may be chosen, so every statement quantified
over complete runs holds for every tie-breaking order, as the paper's Theorem 1 does ("for any
fixed "). The pruning phase, which produces the tree , is not modelled; no statement
here uses .Chapter I of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) opens the book with a multi-stage allocation process: a resource is divided, stage after stage, between two activities, each of which yields an immediate return and leaves behind a depleted remainder that is re-divided at the next stage. The chapter uses this process as its prototype for "a number of multi-stage processes, of diverse origin, but similar analytic structure" (§ 8, p. 11), and the techniques it introduces here — the functional equation of the infinite process, successive approximations, approximation in policy space, transfer of convexity and concavity through the recurrence, and a stability estimate — reappear throughout the book and in the later theory of Markov decision processes.
When the number of stages is large, Bellman replaces the finite sequence of recurrences by a single equation for the infinite process. As the book stresses (p. 11), this replacement is only useful once one knows that the equation has a solution and possesses "no extraneous solutions". This mission formalizes that existence and uniqueness theorem and the chapter's main structural results that rest on it.
A quantity is split into , assigned to a first activity with return , and , assigned to a second activity with return . After the stage the first allocation has been reduced to and the second to , and the process continues with the quantity . Writing
the total return of the infinite process satisfies the allocation equation (Bellman's (8.1))
The standing hypotheses of Chapter I, Theorem 1 are:
The successive approximations from an initial function are . A policy is a function with ; its return is the total of the stage returns obtained by using at every stage.
In Lean all objects live in the namespace BellmanDP.Allocation: allocT is , allocM is , AllocationHyp g h a b bundles the three hypotheses, IsAllocationSolution g h a b f is the equation with the maximum attained, allocIter is the sequence , and policyReturn is the return of a policy.
Under the three hypotheses, there is a function with
this is continuous on , and every solution continuous at with value there coincides with on .
Theorem 1 is what gives meaning to "the solution" of the allocation equation, which every later result of the chapter refers to. Without the side condition at uniqueness fails: when , every constant function and the indicator of solve the equation. Theorems 2 and 3 turn the existence proof into computational procedures (value iteration and policy improvement), and Theorem 3's monotonicity is the prototype of the policy-improvement property. Theorems 4 and 5 are the first structural results on optimal policies — all-or-nothing allocation under convex returns, a unique interior-or-boundary allocation under strictly concave returns — and Theorem 9 bounds the error made by replacing a return function with a simpler approximation.
These are classical results with published proofs in the book. No machine-checked version of any of them is known to this mission; the work is to formalize the proofs, building reusable infrastructure for functional equations of the form with a contracting transition .
The equation is not a contraction in the supremum norm on : and may be unbounded, so no global Banach fixed-point argument applies. Control comes instead from the shrinking of the argument, , which propagates a local estimate near out to every finite interval, and the summability hypothesis (1b) is what makes the resulting series converge uniformly on bounded sets. Uniqueness cannot come from a norm estimate either; it rests on continuity at alone. The maximum in the equation must be shown to be attained, which requires continuity of the limit function; the book notes (p. 13) that the monotone argument for nonnegative gives only a supremum. For Theorems 4 and 5, convexity and concavity must be carried through each approximation and preserved in the limit, and strict concavity must be recovered for the limit, where a pointwise limit of strictly concave functions is only concave.
ℝ → ℝ; only their values on enter any hypothesis or conclusion. Continuity at is one-sided (ContinuousWithinAt f (Set.Ici 0) 0), and uniqueness is equality on .IsGreatest of , so a solution attains its maximum at every . The maxima inside definitions (, , the triangle maximum of Theorem 9) are real suprema (sSup) of images of compact nonempty sets of continuous functions, which equal the book's maxima under the stated hypotheses.Welcome contributions: a general existence-and-uniqueness theorem for equations with , and a lemma that parametric maxima over of continuous functions are continuous in .
This is the fourth mission of the series on Assumptions of Physics by G. Carcassi and C. A. Aidala (book, v3.0, 2025), formalizing the axiomatic core of Part II, Chapter 4, "Ensemble spaces". The chapter proposes three physically motivated axioms (ensemble, mixture, entropy) that every space of statistical states should satisfy, covering classical probability distributions and quantum density operators alike, and derives from them structure that is usually postulated, for example that mixtures can be "un-mixed" (cancellativity). That is the first step towards embedding ensembles in a vector space. Unlike missions II and III, this mission does not depend on earlier missions.
An ensemble space is a , second countable topological space with a continuous mixing operation (, ) that is idempotent, commutative and associative, and a continuous entropy . The entropy is strictly concave, with equality iff , and bounded above by for a universal function . Two ensembles are orthogonal, , when this bound is saturated, and mixtures preserve orthogonality. An ensemble is a component of if with ; two ensembles are separate if they have no common component. The mixing entropy is .
Cancellativity is what allows affine combinations with negative coefficients, the origin, in this framework, of the vector-space embedding of ensembles (Theorem 4.94) and of negative quasi-probabilities such as Wigner functions. It holds in classical and quantum statistics, and here it is derived from continuity and strict concavity of the entropy instead of being postulated. The results are proved informally in the book; no machine-checked formalization is known to the drafters.
The convex-space axioms are stated in a two-sided associativity form, so every rearrangement of mixtures must be derived from it. The book's proof of cancellativity first propagates the equality from one coefficient to all of by an iteration , and then uses a limit together with continuity of mixing and of the entropy. Strict concavity has to be applied only to non-trivial coefficients.
The structure EnsembleSpace I E bundles Axioms 4.4, 4.7 and 4.55 for a topological space E; mixing coefficients are elements of Mathlib's unitInterval. Real coefficient expressions in the associativity axiom pass through clampI, the projection , and lie in on the stated domain. The universal function is a parameter. Orthogonality is saturation of the upper bound for every . Strict concavity is required for only, since at equality is automatic. The book's Proposition 4.67 uses for , which follows from universality of (any space with two distinct ensembles forces it); the milestone carries this as an explicit hypothesis. Items 3 and 4 of Proposition 4.116 in the book use the normalization from Theorem 4.59; item 3 is stated with and item 4 is omitted. Hull operators, the vector-space embedding (Theorem 4.94), boundedness of lines (Theorem 4.105), the entropic geometry and the standard classical/quantum models (Propositions 4.5, 4.9, 4.56) are left for later missions.
Many optimization problems in operations research are posed on an expectation: a two-stage or multistage stochastic program minimizes , where is convex but nonsmooth and the expectation cannot be computed exactly. What can be computed is a stochastic subgradient, a random vector whose mean is a subgradient of . The stochastic subgradient method replaces the exact subgradient in the classical method by such a random vector. It was introduced by Yu. M. Ermoliev and N. Z. Shor in 1968 and developed by Ermoliev, Nurminski and others into a standard tool of stochastic programming; the same scheme, under the name stochastic (sub)gradient descent, underlies most of large-scale machine learning.
This mission formalizes Section 2.6 of N. Z. Shor, Minimization Methods for Non-Differentiable Functions (Springer 1985): the almost-sure convergence theorem for the stochastic subgradient method (Theorem 2.19), together with two deterministic results of the same section on perturbed and restarted variants of the subgradient method (Theorems 2.18 and 2.20).
Timeline, as recorded in the book:
is -dimensional Euclidean space with inner product . A vector is a subgradient of at if for all ; is the set of minimum points of .
Stochastic subgradient method. Fix a probability space with a filtration , a deterministic starting point , stepsize rules and random vectors . The iterates are
In the book's notation : a random vector whose expectation, given the state at step , is a subgradient of at . In the Lean development the iterates are stochIter h G x₀ k ω.
Perturbed subgradient method (Shepilov). Given a subgradient selection , points with , and steps : .
Restarted method (Bazhenov). For a function that is almost differentiable (Lipschitz on bounded sets, differentiable almost everywhere, with gradient continuous where it exists) and a selection of almost-gradients (limit points of gradients at nearby points of differentiability), with : take the normalized step and restart from whenever leaves (resetIter).
Let be convex with a unique minimum point . Suppose is a subgradient of at , , and almost surely , , . Then
Theorem 2.19 is the basic justification of stochastic subgradient methods: without computing or any exact subgradient, the method reaches the minimizer with probability one, under stepsize conditions that are met by . It is the nonsmooth convex counterpart of the Robbins–Monro theorem and the prototype of the almost-sure convergence results for stochastic quasi-gradient methods used in stochastic programming. Theorem 2.20 shows that the deterministic method tolerates summable errors in the point where the subgradient is evaluated, which is what allows subgradients to be approximated by finite differences (Section 1.3). Theorem 2.18 extends the convergence of the normalized method to local minima of a class of nonconvex functions.
All four results are proved in the literature. To the best of the platform search (September 2026), none is machine-checked: the platform has almost-sure convergence theorems for smooth stochastic approximation under ODE-type hypotheses (Borkar–Meyn) and in-expectation bounds for stochastic gradient descent, neither of which covers this recursion. A formal proof of the goal would give a reusable almost-sure convergence argument for nonsmooth stochastic methods on top of Mathlib's martingale theory.
The deterministic proof of convergence of the subgradient method compares with along the whole trajectory. With random directions this comparison holds only in conditional expectation, and the term is not controlled pathwise. Taking expectations of the one-step inequality and summing gives only bounds on , which do not yield almost-sure convergence. Moreover the stepsize depends on the random iterate, so the conditions and hold only almost surely, not uniformly, and the iterates need not be square-integrable. Identifying the almost-sure limit as requires using the uniqueness of the minimizer to bound away from zero outside a neighbourhood of .
In Theorems 2.18 and 2.20 the difficulty is that the distance to is not monotone: steps taken near the solution, or with a perturbed subgradient, can increase it, and a restart can move the iterate far away.
EuclideanSpace ℝ (Fin n); is real-valued (finite everywhere); convexity is ConvexOn ℝ Set.univ f; uniqueness of is a separate hypothesis.∀ᵐ ω ∂μ, Tendsto (fun k => ‖x k ω - x*‖) atTop (𝓝 0).MeasureTheory.condExp), filtrations, and almost-sure convergence of -bounded (sub/super)martingales; the supermartingale convergence theorem the book cites from Doob is used from Mathlib, not restated. A Robbins–Siegmund-type lemma for nonnegative almost-supermartingales would be the natural reusable contribution. The almost-differentiability and subgradient definitions duplicate drafts of other missions in this series.Queueing control problems (admission control, routing, service rate selection) are naturally modelled as Markov decision chains with a countably infinite state space and unbounded costs, for instance a holding cost that grows with the queue length. For such models the long-run average cost criterion is often the relevant one, and the central question is whether an optimal stationary policy exists and can be computed from an average cost optimality equation (ACOE). Chapter 7 of Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037) develops a verifiable set of conditions, the (SEN) assumptions, under which an average cost optimality inequality (ACOI) holds and yields an optimal stationary policy. The inequality may be strict (Example 7.3.1), and an optimal policy may induce a Markov chain without positive recurrent states.
Sections 7.4 and 7.5 answer two practical questions: when is the ACOI in fact an equation, and how can (SEN) be checked in a concrete model? The answer culminates in the (BOR) assumptions, which require only one well-behaved stationary policy and the finiteness of a set of low-cost states.
According to the book's bibliographic notes (p. 163): the (BOR) assumptions modify a line of development due to Borkar (SIAM J. Control Optim. 22, 1984, and 27, 1989; monograph 1991) and are weaker than his original conditions; the proof that (BOR) implies (SEN) is from Cavazos-Cadena and Sennott (Oper. Res. Letters 11, 1992), and the version of (BOR) used here is from Sennott (Prob. Eng. Inform. Sci. 7, 1993). Proposition 7.5.5 and the (CAV*) assumptions go back to Cavazos-Cadena (Kybernetika 25, 1989); Proposition 7.5.3 and Corollary 7.5.4 to Sennott (Oper. Res. 37, 1989).
A Markov decision chain consists of a countable state space , finite nonempty action sets , nonnegative finite costs and transition probabilities . A policy may use the whole history and randomize. For the discount value function is , the infimum of ; the average cost of is and the minimum average cost is . All of these lie in .
For a distinguished state the relative value is . The (SEN) assumptions are: (SEN1) is bounded on ; (SEN2) for a finite function ; (SEN3) for a finite constant . Under (SEN), is a finite constant, and a limit function is a pointwise limit of along some . The ACOI and ACOE read
For a nonempty set the first passage time is . The class consists of the policies that, from , enter with probability one in finite expected time ; adds a finite expected first passage cost . A (randomized) stationary policy is standard if the Markov chain it induces has and for every ; it then has a single positive recurrent class and a finite constant average cost .
Assume (BOR): (BOR1) a standard policy exists; (BOR2) for some the set is finite; (BOR3) every can be reached from by some . Then (SEN) holds and every limit function satisfies the ACOE; every average cost optimal stationary policy has a positive recurrent state in
at most positive recurrent classes and no null recurrent class; and a policy realizing the minimum in the ACOE satisfies for every .
Theorem 7.5.6 reduces the verification of the ACOE for a queueing model to three checks that do not involve the discount value function: exhibit one stationary policy with finite mean return times and costs to a fixed state (typically a stable "serve at maximal rate" policy), check that low costs occur on a finite set (automatic when the holding cost grows without bound, Corollaries 7.5.9–7.5.10), and check reachability of finitely many states. Its conclusions go beyond existence: optimal stationary policies induce chains with positive recurrent classes located in a known finite set, and ACOE-realizing policies reach them in finite expected time and cost. This is what makes value iteration and approximating-sequence methods in later chapters of the book applicable to these models.
The results are proved in the book. The present mission produces machine-checked statements of the first passage calculus for general (history-dependent, randomized) policies, of (SEN) and limit functions, and of the chain of implications from (CAV*) to the ACOE. No machine-checked version of these statements is known.
The obvious approach to the ACOE is to pass to the limit in the discount optimality equation. Exchanging this limit with requires a dominating function, and (SEN2) only gives a pointwise bound whose expectation may be infinite; Fatou's lemma then yields only the inequality. Obtaining equality requires tracking first passages to sets and showing that the discrepancy vanishes along them, which in turn needs finiteness of that is not assumed but has to be derived. On the recurrence side, the average cost criterion is a limit superior of Cesàro averages over a countable state space, and mass can escape to infinity; the finiteness of the set is what prevents an optimal policy from spending its time in transient or null recurrent states, and turning that into positive recurrence requires the renewal-type identities of Appendix C.
States form a countable type ; action sets are nonempty Finsets; costs are in ℝ≥0; transition probabilities are ℝ≥0∞-valued with row sums one on admissible actions. Policies are general: a history is a state sequence and an action sequence, and all probabilities and expectations (hitting probabilities, , , , ) are computed from the history probabilities of the process. , , and take values in ; when is missed with positive probability; the first passage time satisfies . and are in the extended reals, with the book's convention that a function bounded below has an expectation in . Limit functions are real valued. Positive recurrence, communicating classes and steady state probabilities are the notions for the chain induced by a (randomized) stationary policy. is the average cost of from .
A formalization in which the ACOE is asserted for some convenient function instead of every limit function, or in which is a natural-number cardinality that vanishes on infinite sets, would trivialize part of the goal; the statements quantify over all limit functions and use Set.encard.
A complete development needs: history-dependent policies and their path laws on countable spaces; first passage decompositions (strong Markov property at ); Abelian limits of ; Fatou and dominated convergence for series; and the renewal reward theorem for positive recurrent classes (Appendix C of the book). The first passage and Markov chain layer is reusable beyond this mission. Proofs of individual milestones, and sharper statements of the Appendix C facts they use, are welcome.
Queueing control problems (admission control, routing, service-rate selection, flow control) are naturally posed as Markov decision chains with a denumerably infinite state space, such as the number of customers in a buffer, and are usually judged by their long-run average cost per unit time. When the state space is finite, Chapter 6 of Sennott's book shows that an average cost optimal stationary policy always exists. On a countable state space this fails: Section 7.1 of the book gives examples in which no average cost optimal policy exists, and one in which no stationary policy comes within a given distance of the minimum average cost. The question addressed by this mission is under which verifiable conditions on the discounted value functions a countable-state model has a constant minimum average cost and an optimal stationary policy.
Timeline, following the book's bibliographic notes (p. 163). The book names Taylor (1965) and Derman (1966) as earlier pivotal work and Ross (1968), and his 1983 textbook, as the direct predecessor. Sennott (1989, Operations Research 37) weakened Ross's assumptions to cover models with unbounded costs, and proved the main result of Section 7.2; the (SEN) assumptions of Chapter 7 are the cleaner version of Sennott (1993). Cavazos-Cadena (1991) gave the example, adapted as Example 7.3.1 of the book, showing that under these assumptions the optimality inequality can be strict. The weaker (H*) assumptions of Section 7.7 appear, in a slightly different form, in Sennott (1995). Part (iv) of Theorem 7.2.3 is new in the book.
A Markov decision chain (MDC) has a countable state space , for each state a finite nonempty action set , a nonnegative finite cost , and transition probabilities with . A policy chooses the action at time at random according to a distribution that may depend on the whole history ; a stationary policy always chooses in state .
For an initial state , the -horizon cost is , the average cost is , and the minimum average cost is over all policies. A policy is average cost optimal if . For the discounted value function is . All these quantities lie in .
Fix a distinguished state and put . The (SEN) assumptions are:
A limit function is a pointwise limit of along some sequence . If is a stationary policy realizing the discount optimality equation , a limit point is a stationary policy with for large , for each , along some .
Under (SEN), there is a finite constant independent of ; limit functions exist, satisfy and the average cost optimality inequality (ACOI)
every stationary policy realizing the minimum is average cost optimal with and ; every limit point of discount optimal stationary policies is average cost optimal and satisfies the corresponding inequality for an associated limit function; and the average cost of any optimal policy is a limit, not only a limit supremum.
Theorem 7.2.3 is the existence theorem the rest of Chapter 7 builds on (p. 128): the ACOE results of Section 7.4, the (BOR) and (CAV) sufficient conditions of Section 7.5, and the worked queueing models of Section 7.6 all work under (SEN) and invoke it. It justifies computing an average cost optimal policy for a queueing model as a limit of discount optimal policies, and it shows that the minimum average cost is the Abelian limit of the normalized discounted value.
The results are proved in the book and in Sennott (1989, 1993, 1995), but none of them has a machine-checked proof: Mathlib has no Markov decision processes, and the platform's average cost results concern finite state spaces or Borel models with different assumptions. The formalization produces a general-policy, countable-state MDC development with extended-real values, reusable by the later missions of this series.
On a finite state space the relative value functions are bounded and the Abelian limit can be controlled directly. Here is bounded above only by a function that may be unbounded, so passing to the limit in the discounted optimality equation cannot use dominated convergence, and in general only an inequality survives in the limit; Example 7.3.1 shows that the inequality in the ACOI can be strict. Showing that a policy realizing the ACOI is optimal requires control of for a function that is unbounded above, and part (iv) requires comparing the limit inferior and limit superior of Cesàro averages for an arbitrary, possibly history-dependent optimal policy.
The state space is any countable type ([Countable S]); actions form a type with finite nonempty Finset action sets; costs are ℝ≥0; transition probabilities, costs over time and value functions are ℝ≥0∞. Policies are general: randomized and history dependent, with histories encoded as finite state and action sequences and the process law built by an explicit recursive product. Finite horizon costs have terminal cost , as the chapter prescribes.
The relative value is computed in EReal, never through a truncated real subtraction: a state with gives , so (SEN2) cannot hold through a junk value, and (SEN1) is a bound by a finite constant that itself forces . Sums and expectations of real functions are extended reals, computed as positive part minus negative part; they are never Bochner integrals and never default to when not summable. The limit is the filter 𝓝[<] 1. Limit functions and limit points follow Definition 7.2.2 literally, over arbitrary sequences in , and the (SEN), (H), (H*) sets are predicates carrying their witnesses and .
A development that bounds only as a free function, rather than the one built from the infimum over all policies, or that quantifies only over stationary policies in , proves a different and weaker theorem and does not count.
Needed infrastructure: the law of the controlled process under a general policy, monotone and Fatou-type limit interchanges for countable sums, the Abelian inequality (Proposition 6.1.1 of the book), and the existence and optimality of discount optimal stationary policies (Theorem 4.1.4). The MDC layer and these two results are shared with other missions of the series; contributions to them are welcome.
Service parts (spares for aircraft, machines, and networks) are typically managed item by item with a one-for-one replenishment policy, the policy: every unit withdrawn to meet a demand triggers an order for one replacement, so the inventory position stays at the stock level . A firm stocking thousands of such items at one location has to choose all the stock levels together, trading a budget on inventory investment against a service measure. Chapter 3 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) sets up the three standard service measures (fill rate, ready rate, expected backorders), shows which of them have the convexity that optimization needs, and solves two multi-item stocking problems: minimum expected backorders under an investment budget, by Lagrangian relaxation justified by Everett's theorem, and maximum average fill rate, by a greedy marginal-analysis rule.
The Lagrangian method goes back to Everett (Operations Research 1963); the search for the multiplier in one-constraint problems of this kind is Fox and Landi (Operations Research 1970); the compound Poisson model is Feeney and Sherbrooke (Management Science 1966). The same separable Lagrangian structure underlies the multi-echelon METRIC-type models later in the book.
A single item is stocked at one location, demand not met from stock is backordered, and customer orders arrive as a Poisson process of rate . An order is for units with probability , where and the mean order size is finite (compound Poisson demand; simple Poisson demand is ). Resupply times have mean . The steady-state probability that units are in resupply is
where is the probability that orders total units. In this mission is the definition of the model, not a consequence of Palm's theorem. The mean lead-time demand is , and the book also writes .
For a stock level :
Forward differences are and ; discrete convexity means .
With items, unit costs and budget , Problem 4 (3.40) is
For a multiplier , the item-wise criterion defines as the least with , and .
For every , each exists and
for every vector of nonnegative integer stock levels. That is, is optimal for Problem 4 at budget . This is what the book asserts by combining Theorem 10 (p. 57, with the remark on p. 58) and the criterion of p. 61, and it is the basis of its bisection algorithm (p. 63). The goal fixes no numerical constant.
The goal reduces a coupled integer program over thousands of items to one scalar search: for a fixed multiplier each item is solved by a single scan of its distribution function, and each multiplier yields a point on the exact efficient frontier of expected backorders against investment. Milestone 8 does the same for fill rates on the region where they are concave, and milestone 1 explains why that region, , is imposed in practice. Milestone 4 is the identity that turns an investment budget into the constraint of Problem 4.
All results are proved in the book (Theorem 10 with a complete proof; the others by short derivations, the greedy optimality by a sketch). None of them is formalized, as far as the platform shows: there is no Everett-type Lagrangian sufficiency theorem, no compound Poisson backorder function, and no discrete marginal-analysis optimality result. The mission produces a reusable layer for later chapters: the compound Poisson steady-state law with its backorder function, and the Lagrangian machinery the book reuses for multi-echelon systems.
The algebra of first differences is elementary; the difficulties are elsewhere. is an infinite series whose convergence rests on the finiteness of the mean order size, and exchanging the difference with the sum, and identifying with , requires manipulating a doubly infinite sum over order counts and convolution powers. Existence of requires that the compound Poisson probabilities sum to one. For milestone 8 the obvious argument ("greedy is optimal for concave separable objectives") fails for knapsack constraints with unequal costs at arbitrary budgets; it holds only at the budgets the greedy run generates, and only on the region where every is concave; dropping the floor constraints makes it false.
Stock levels are natural numbers; probabilities, rates, costs and multipliers are reals. The compound Poisson law is a structure with fields , an order-size distribution with , , , and summable (the finite mean is added: without it is infinite). Expected on-hand inventory is the finite sum . Items are indexed by an arbitrary finite type (nonempty where a maximum over items is taken).
Pinnings and deviations, each stated in the item's Formalization Note:
A trivializing formalization is ruled out: the goal is stated for the book's own backorder function built from the compound Poisson law, not for an arbitrary convex function nor for a defined through its differences.
Welcome contributions: summability and normalization lemmas for the compound Poisson law, a general discrete Lagrangian lemma for separable objectives, and proofs of the milestones in any order.
Stochastic quasigradient (SQG) methods minimize an expectation over a constraint set when neither nor its gradient can be computed, only random vectors whose conditional mean is (close to) a subgradient. They are the workhorse of stochastic programming and, under the name stochastic gradient descent, of large-scale statistical learning. The classical convergence theory, going back to Robbins and Monro (1951) and to Ermoliev's quasi-Féjer analysis, asks the stepsizes to be chosen in advance with , , . Uryasev, in Chapter 18 of Numerical Techniques for Stochastic Optimization (Ermoliev and Wets, eds., 1988), points out that such programmed rules are slow in practice, and that practitioners want adaptive stepsizes computed on line from the observed directions.
Timeline:
Let be nonempty, convex and compact, its diameter, and convex on an open convex set , with subdifferential . The projection is the point of nearest to . On a probability space, the SQG method generates
from , where the direction is a stochastic quasigradient: with , a bias , and the -algebra induced by .
The adaptive stepsize rule of the chapter is, for fixed , and ,
The step grows when consecutive moves point the same way and shrinks otherwise. The weighted (Cesàro) averages are
The sequence is Cesàro convergent when converges to the solution set.
Chapter 17 (Pflug) uses the same method for over a closed convex , with from i.i.d. and stepsizes adapted to .
Under (18.15), (18.16) and (18.17), almost surely,
and if a.s., then and all accumulation points of are minimizers, almost surely.
Theorem 2 is a convergence guarantee for a stepsize rule that is computed from the run itself. It needs no square summability of the steps, and it tolerates a nonvanishing bias at a cost linear in the bias. This is the regime of practical SQG codes; §18.4–18.5 of the chapter discuss implementation and numerical experiments. Theorem 1 isolates the reason: Cesàro convergence needs only and . It also allows a stepsize that depends on the current direction, provided consecutive steps have ratio tending to .
The volume proves none of the probabilistic results in full. Theorem 1 of Chapter 18 is cited from Uryasev's earlier report. Theorem 2 has an outline proof that reduces it to Theorem 1. Chapter 17 gives a sketch through the Robbins–Siegmund lemma. None of these results is formalized. The mission produces machine-checked statements of all of them, with the misprints of the page resolved, and it separates the pathwise part of the Theorem 2 argument (steps 1 and 2, which are deterministic) from the martingale part (Theorem 1).
The obvious route to a.s. convergence is the quasi-Féjer or Robbins–Siegmund argument. It controls and needs , which is exactly what is not available here. The averaged analysis has to show that the martingale term is almost surely, and that is , when the stepsizes are themselves random. Under condition (2) of Theorem 1, is not even measurable with respect to the -algebra of the conditional expectation. So , and the standard decomposition breaks. For the adaptive rule, the stepsizes are coupled to the iterates through the exponent. Neither nor is given, and both must be derived path by path.
is EuclideanSpace ℝ (Fin n). Sequences are indexed from . Chapter 17 is shifted by one against the page: its , , become indices . Conditional expectations are Mathlib's condExp with respect to the history -algebras of the definition file. Every bound is written out as "for every , eventually ", or in (18.17) as a bound with . Expectations of squared norms are lower Lebesgue integrals. The deterministic proof steps (items 5 to 8) are stated for one sample path.
Readings of the page, each recorded in the item's Formalization Note:
No explicit constants replace an O(·) or an unspecified "C": every constant appears in the book's statements.
A trivializing formalization states Theorem 2 for arbitrary stepsizes satisfying (18.10)–(18.13), which is Theorem 1 again. Here the stepsizes are tied to the iterates by (18.5), and the of (18.17) is the of the rule.
Needed infrastructure: a Robbins–Siegmund almost-supermartingale lemma, which Mathlib does not have; a strong law for martingale differences with random weights (Kronecker's lemma in its stochastic form); nonexpansiveness of the projection onto a closed convex set; and nonemptiness of the subdifferential of a finite convex function on an open set. The first two are reusable across stochastic approximation. Contributions of any of the milestones, or of these lemmas as separate theorems, are welcome.